* #ri #rs #ti #ts <max_rew //
qed.
+lemma max_idem: βc. c = (c β¨ c).
+* #ri #rs #ti #ts <max_rew //
+qed.
+
(* Basic inversion properties ***********************************************)
lemma max_inv_dx: βri,rs,ti,ts,c1,c2. β©ri,rs,ti,tsβͺ = (c1 β¨ c2) β
<max_rew #H destruct /2 width=14 by ex6_8_intro/
qed-.
+(* Main Properties **********************************************************)
+
+theorem max_assoc: associative β¦ max.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<max_rew <max_rew //
+qed.
+
(* Properties with test for constrained rt-transition counter ***************)
lemma isrt_max: βn1,n2,c1,c2. ππβ¦n1, c1β¦ β ππβ¦n2, c2β¦ β ππβ¦n1β¨n2, c1β¨c2β¦.
qed-.
(* Properties with shift ****************************************************)
-(*
-lemma max_shift: βc1,c2. (βc1) β¨ (βc2) = β(c1β¨c2).
+
+lemma max_shift: βc1,c2. ((βc1) β¨ (βc2)) = β(c1β¨c2).
* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
<shift_rew <shift_rew <shift_rew <max_rew //
qed.
-*)