% fof( nil_in_list, axiom, list(nil) ). % fof( cons_in_list, axiom, ![X,XS] : (list(XS) => list(cons(X,XS))) ). fof( nil_cons_disjointness, axiom, ![X,XS] : nil!=cons(X,XS) ). fof( cons_injectivity, axiom, ![X,Y,XS,YS] : cons(X,XS)=cons(Y,YS) => (X=Y & XS=YS) ). fof( concat_nil, axiom, ![XS] : concat(nil,XS)=XS ). fof( concat_cons, axiom, ![X,XS,YS] : concat(cons(X,XS),YS)=cons(X, concat(XS,YS)) ). fof( reverse_nil, axiom, reverse(nil)=nil ). fof( reverse_cons, axiom, ![X,XS,YS] : reverse(cons(X,XS))=concat(revese(XS), cons(X,nil)) ). % an instance of induction scheme fof( assocP_def, axiom, ![YS,ZS,XS] : ( assocP(YS,ZS,XS) <=> (concat(XS,concat(YS,ZS)) = concat(concat(XS,YS),ZS)) )). fof( assocP_ind, axiom, ![YS,ZS] : ( (assocP(YS,ZS,nil) & (![XS,X] : assocP(YS,ZS,XS) => assocP(YS,ZS,cons(X,XS)))) => ![XS] : assocP(YS,ZS,XS) )). % an instance of induction scheme fof( revP_def, axiom, ![XS] : ( revP(XS) <=> (reverse(reverse(XS))=XS) )). fof( revP_ind, axiom, (revP(nil) & (![XS,X] : revP(XS) => revP(cons(X,XS)))) => ![XS] : revP(XS) ). % fof( concat_assoc, conjecture, ![XS,YS,ZS] : concat(XS,concat(YS,ZS)) = concat(concat(XS,YS),ZS) ). fof( reverse_reverse_id, conjecture, ![XS] : reverse(reverse(XS))=XS ).