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

%Ri represents the step_i relation, RRi the paths

formula_list(sos).

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

%RRi includes = (but not necessarily Ri) and is transitive
all X Y (X=Y -> RR1(X,Y)).
all X Y (X=Y -> RR2(X,Y)).
all X Y Z (RR1(X,Y) & RR1(Y,Z) -> RR1(X,Z)).
all X Y Z (RR2(X,Y) & RR2(Y,Z) -> RR2(X,Z)).

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

%weak commutativity
all X Y Z (R1(X,Y) & R2(X,Z) -> (exists J (RR2(Y,J) & RR1(Z,J)))).

%IH: any i_step beyond x we have commutativity
all X Y Z ((R1(x,X) | R2(x,X))
& RR1(X,Y) & RR2(X,Z) -> (exists J (RR2(Y,J) & RR1(Z,J)))).

%assume that x is not commutative, whereas IH
-(all Z Y (RR1(x,Y) & RR2(x,Z) -> (exists J (RR2(Y,J) & RR1(Z,J))))).

end_of_list.