set(hyper_res).
set(ur_res).
set(prolog_style_variables).
set(output_sequent).
clear(print_kept).
clear(print_given).
clear(print_back_sub).
assign(max_proofs,5).


%R represents the step relation, RR the paths

formula_list(sos).

%reflexivity and symmetry of =, transitivity not needed
all X (X=X).
all X Y (X=Y -> Y=X).

%RR includes = and R and is transitive
all X Y (X=Y -> RR(X,Y)).
%all X Y (R(X,Y) -> RR(X,Y)). %not needed!
all X Y Z (RR(X,Y) & RR(Y,Z) -> RR(X,Z)).

%any path has either length 0 or starts with a step
all X Y (RR(X,Y) -> (X=Y | (exists I ( R(X,I) & RR(I,Y))))).

%local confluence
all X Y Z (R(X,Y) & R(X,Z) -> (exists J (RR(Y,J) & RR(Z,J)))).

%assume that x is not confluent, whereas IH holds
-(all Y Z (RR(x,Y) & RR(x,Z) -> (exists J (RR(Y,J) & RR(Z,J))))).

%IH: we have confluence any step beyond x 
all X Y Z (R(x,X) & RR(X,Y) & RR(X,Z) -> (exists J (RR(Y,J) & RR(Z,J)))). 

end_of_list.