set(auto).
%assign(order,kbo).
%set(fold_eq).
%assign(max_weight,20).
%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 all z (cat(x,y,z) -> cat(cons(a,x),y,cons(a,z))).

all x y z xy yz xyz ((cat(x,y,xy) & cat(xy,z,xyz) & cat(y,z,yz)) -> 
                     cat(x,yz,xyz)).

%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).



rev(nil,nil).
all a x y z((rev(x,y) & cat(y,cons(a,nil),z)) -> rev(cons(a,x),z)).

%th: rev(rev(x)) = x
%base
%proved by contra
%-(exists y (rev(nil,y) <-> rev(y,nil))).
%base as lemma

%step
%proof by contra
-(all x ((exists y (rev(x,y) <-> rev(y,x))) ->
         (all a (exists y (rev(cons(a,x),y) <-> rev(y,cons(a,x))))))).

%(all x ((exists y (rev(x,y) <-> rev(y,x))) ->
%         (all a (exists y (rev(cons(a,x),y) <-> rev(y,cons(a,x))))))).

end_of_list.
