set(auto).
%assign(order,kbo).
%set(fold_eq).
%assign(max_weight,5).
%set(sos_queue).
%set(para_into_left).
%set(para_from_units_only).
%set(para_into_units_only).
%set(para_all).

formula_list(sos).

all y (cat(nil,y) = y).
all a all x all y (cat(cons(a,x),y) = cons(a,cat(x,y))).

%THEOREM: cat(x,nil) = x
% proof follows
% base 
%proved by contra
%-(cat(nil,nil) = nil).
%STEP proof
% assume base
%cat(nil,nil)=nil.
% step
%proved by contra
-(all x (cat(x,nil) = x -> (all a (cat(cons(a,x),nil) = cons(a,x))))).

% ASSUME THEOREM PROVED
%all x (cat(x,nil) = x).

%THEOREM: cat(x,cat(y,z)) = cat (cat(x,y),z)
%proof follows
%base
%proved by contra
%-(all y all z(cat(nil,cat(y,z)) =  cat(cat(nil,y),z))).
%step
%proved by contra
%-(all x all y all z (cat(x,cat(y,z)) = cat(cat(x,y),z) ->
%        (all a (cat(cons(a,x),cat(y,z)) = cat(cat(cons(a,x),y),z))))).

%ASSUME THEOREM
all x all y all z (cat(x,cat(y,z)) = cat(cat(x,y),z)).   

% DEFINITION: snoc
all a (snoc(nil,a) = cons(a,nil)).
all a all b all x (snoc(cons(b,x),a) = cons(b,snoc(x,a))).

%THEOREM: snoc(x,a) = cat(x,cons(a,nil)).
% base
%proved by contra
%-(snoc(nil,a) = cat(nil,cons(a,nil))).
%base as lemma
snoc(nil,a) = cat(nil,cons(a,nil)).
%step: proved by contra
%-(all x all a (snoc(x,a) = cat(x,cons(a,nil)) -> 
%    (all b (snoc(cons(b,x),a) = cat(cons(b,x),cons(a,nil)))))).
%ASSUME THEOREM
all x all a (snoc(x,a) = cat(x,cons(a,nil))).
% th: snoc(cat(x,y),a) = cat(x,snoc(y,a))
% the base case as axiom
%proved by contra
%-(all a all y (snoc(cat(nil,y),a) = cat(nil,snoc(y,a)))).
% base assumed
(all a all y (snoc(cat(nil,y),a) = cat(nil,snoc(y,a)))).
% step 
%proved by contra
%-(all x all a all y ((snoc(cat(x,y),a) = cat(x,snoc(y,a))) ->
%               (all b (snoc(cat(cons(b,x),y),a) = cat(cons(b,x),snoc(y,a)))))).

(all x all a all y (snoc(cat(x,y),a) = cat(x,snoc(y,a)))).


rev(nil) = nil.
all a all x (rev(cons(a,x)) = snoc(rev(x),a)).

%THEOREM: rev(snoc(x,a)) = cons(a,rev(x))
%base
%proved by contra
%-(all a (rev(snoc(nil,a)) = cons(a,rev(nil)))).
%base assumed
%(all a (rev(snoc(nil,a)) = cons(a,rev(nil)))).
%step 
%by contra
%-(all x all a ((rev(snoc(x,a)) = cons(a,rev(x))) ->
%              (all b (rev(snoc(cons(b,x),a)) = cons(a,rev(cons(b,x))))))).

% ASSUME THEOREM PROVED
all x all a ((rev(snoc(x,a)) = cons(a,rev(x)))).

%THEOREM: rev(rev(x)) = x
%base
%proved by contra
%-(rev(rev(nil)) = nil).
%base as lemma
%(rev(rev(nil)) = nil).

%step
%proved by contra
%-(all x ((rev(rev(x)) = x) -> (all a (rev(rev(cons(a,x))) = cons(a,x))))).
% ASSUME THEOREM PROVED
all x (rev(rev(x)) = x).

%THEOREM: rev(cat(x,y)) = cat(rev(y),rev(x))
%base
%proved by contra
%-(all y (rev(cat(nil,y)) = cat(rev(y),rev(nil)))).
% assume base
%(all y (rev(cat(nil,y)) = cat(rev(y),rev(nil)))).
%step
%proved by contra
%-(all x all y ((rev(cat(x,y)) = cat(rev(y),rev(x))) ->
%        (all a (rev(cat(cons(a,x),y)) = cat(rev(y),rev(cons(a,x))))))).
%ASSUME THEOREM PROVED
all x all y (rev(cat(x,y)) = cat(rev(y),rev(x))).

all a (-in(a,nil)).
all a all x (in(a,cons(a,x))).
all a all b all x (a != b -> (in(a,cons(b,x)) <-> in(a,x))).

%-(all a all b all x (in(a,cons(b,x)) <-> (a=b | in(a,x)))).
(all a all b all x (in(a,cons(b,x)) <-> (a=b | in(a,x)))).

nat(0).
all x (nat(x) -> nat(s(x))).

all x (lt(0,s(x))).
all x all y (lt(x,y) -> lt(s(x),s(y))).
all x (- (lt(s(x),0))).

all x all y ((x = y | lt(x,y)) <-> leq(x,y)).

seq(nil).
all a (nat(a) -> (all x (seq(x) -> seq(cons(a,x))))).
all x (seq(x) <-> (x = nil | (exists a y (seq(y) & x = cons(a,y))))).

ordered(nil).
all a (nat(a) -> ordered(cons(a,nil))).
all a all b ((nat(a) & nat(b)) ->
              (all x ((ordered(cons(b,x)) & leq(a,b)) <-> 
                      ordered(cons(a,cons(b,x)))))).

%th ordered(cons(a,x)) -> ordred(x)
%-(all a (nat(a) -> (ordered(cons(a,nil)) -> ordered(nil)))).
%(all a (nat(a) -> (ordered(cons(a,nil)) -> ordered(nil)))).

%-(all x (all a (nat(a) -> 
%                     ((ordered(cons(a,x)) -> ordered(x)) ->
%                      (all b (nat(b) -> 
%                            (ordered(cons(a,cons(b,x))) -> 
%                             ordered(cons(b,x))))))))).

(all x (all a (nat(a) -> 
                     ((ordered(cons(a,x)) -> ordered(x)) ->
                      (all b (nat(b) -> 
                            (ordered(cons(a,cons(b,x))) -> 
                             ordered(cons(b,x))))))))).

%th in(a,insert(b,x)) <-> a=b | in(a,x)
%-(all a all b (in(a,insert(b,nil)) -> (a = b | in(a,nil)))).

%THEOREM ordered(cons(a,x)) -> (all b (in(b,x) -> leq(a,b)))
%-(all a (ordered(cons(a,nil)) -> (all b (in(b,nil) -> leq(a,b))))).
%all a (ordered(cons(a,nil)) -> (all b (in(b,nil) -> leq(a,b)))).
%-(all a all c (ordered(cons(a,cons(c,nil))) -> 
%               (all b (in(b,cons(c,nil)) -> leq(a,b))))).

%-(all x all a ((ordered(cons(a,x)) -> (all b (in(b,x) -> leq(a,b)))) ->
%               (all c ((ordered(cons(a,cons(c,x)))) ->  
%                       (all b (in(b,cons(c,x)) -> leq(a,b))))))).


%all a (insert(a,nil) = cons(a,nil)).
%all a all b all x (leq(a,b) -> insert(a,cons(b,x)) = cons(a,cons(b,x))).
%all a all b all x (-leq(a,b) -> insert(a,cons(b,x)) = cons(b,insert(a,x))).

%THEOREM ordered(insert(a,x))
%base
%proved by contra
%-(ordered(nil) -> (all a (ordered(insert(a,nil))))).
%base as lemma
%(ordered(nil) -> (all a (ordered(insert(a,nil))))).
%step
%proved by contra
%-(all x 
%      ( ((ordered(x)) -> (all a (ordered(insert(a,x))))) -> 
%        (all b ((ordered(cons(b,x))) 
%             -> (all a (ordered(insert(a,cons(b,x))))))) )).
%ASSUME THEOREM
%all a all x (ordered(insert(a,x))).

%all a (noccur(a,nil) = 0).
%all a all x (noccur(a,cons(a,x)) = s(noccur(a,x))).
%all a all b all x (a != b -> noccur(a,cons(b,x)) = noccur(a,x)).

end_of_list.

%list(sos).

%-noccur(1,cons(2,cons(1,(cons(1,nil))))) = y |  $ans(y).
%end_of_list.

% exercises
% transform to cluasal
% finish ordered proof
% finish perms proof
