(* Basic properties *********************************************************)
lemma max_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
(* Basic properties *********************************************************)
lemma max_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.