From 8300e0de4b379e9ab9f2ce00d3f9e3d93c8bd943 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Dec 2009 17:33:30 +0000
Subject: [PATCH] Porting of Sambin's stuff started. Everything is now
 automatically enriched using hints. It seems to work quite smoothly.

---
 .../matita/nlibrary/overlap/o-algebra.ma      | 489 ++++++++++++++++++
 1 file changed, 489 insertions(+)
 create mode 100644 helm/software/matita/nlibrary/overlap/o-algebra.ma

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
new file mode 100644
index 000000000..eae842c44
--- /dev/null
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -0,0 +1,489 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "sets/categories2.ma".
+
+(*
+interpretation "unary morphism comprehension with no proof" 'comprehension T P = 
+  (mk_unary_morphism T ? P ?).
+interpretation "unary morphism1 comprehension with no proof" 'comprehension T P = 
+  (mk_unary_morphism1 T ? P ?).
+
+notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
+for @{ 'comprehension_by $s (λ${ident i}. $p) $by}.
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension_by $s (λ${ident i}:$_. $p) $by}.
+
+interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p = 
+  (mk_unary_morphism s ? f p).
+interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p = 
+  (mk_unary_morphism1 s ? f p).
+*)
+
+(* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
+   lattices, Definizione 0.9 *)
+(* USARE L'ESISTENZIALE DEBOLE *)
+nrecord OAlgebra : Type[2] := {
+  oa_P :> setoid1;
+  oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
+  oa_overlap: binary_morphism1 oa_P oa_P CPROP;
+  binary_meet: binary_morphism1 oa_P oa_P oa_P;
+(*CSC:  oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
+  oa_one: oa_P;
+  oa_zero: oa_P;
+  oa_leq_refl: ∀a:oa_P. oa_leq a a; 
+  oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
+  oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
+  oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
+(*CSC:  oa_join_sup: ∀I:setoid.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = (∀i:I.oa_leq (p_i i) p);*)
+  oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
+  oa_one_top: ∀p:oa_P.oa_leq p oa_one;
+  oa_overlap_preservers_meet: ∀p,q:oa_P.oa_overlap p q → oa_overlap p (binary_meet p q);
+(*CSC:  oa_join_split:
+      ∀I:SET.∀p.∀q:I ⇒ oa_P.
+       oa_overlap p (oa_join I q) = (∃i:I.oa_overlap p (q i));*)
+  (*oa_base : setoid;
+  1) enum non e' il nome giusto perche' non e' suriettiva
+  2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
+  oa_enum : ums oa_base oa_P;
+  oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q
+  *)
+  oa_density: 
+      ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
+}.
+
+interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
+
+notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
+for @{ 'overlap $a $b}.
+interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
+
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
+non associative with precedence 50 for @{ 'oa_meet $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
+non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+
+(*notation > "hovbox(∧ f)" non associative with precedence 60
+for @{ 'oa_meet $f }.
+interpretation "o-algebra meet" 'oa_meet f = 
+  (fun12 ?? (oa_meet ??) f).
+interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
+  (fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)).
+*)
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
+non associative with precedence 50 for @{ 'oa_join $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 
+non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
+
+(*CSC
+notation > "hovbox(∨ f)" non associative with precedence 60
+for @{ 'oa_join $f }.
+interpretation "o-algebra join" 'oa_join f = 
+  (fun12 ?? (oa_join ??) f).
+interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
+  (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
+*)
+(*definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q); 
+  apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; lapply (prop12 ? O (oa_meet O BOOL));
+   [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
+   |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
+   | apply Hletin;]
+  intro x; simplify; cases x; simplify; assumption;]
+qed.*)
+
+interpretation "o-algebra binary meet" 'and a b = 
+  (fun21 ??? (binary_meet ?) a b).
+
+(*
+prefer coercion Type1_OF_OAlgebra.
+
+definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q); 
+  apply (∨ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; lapply (prop12 ? O (oa_join O BOOL));
+   [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
+   |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
+   | apply Hletin;]
+  intro x; simplify; cases x; simplify; assumption;]
+qed.
+
+interpretation "o-algebra binary join" 'or a b = 
+  (fun21 ??? (binary_join ?) a b).
+*)
+(*
+lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
+(* next change to avoid universe inconsistency *)
+change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O);
+intros;  lapply (oa_overlap_preserves_meet_ O p q f);
+lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+[3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
+qed.
+*)
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
+non associative with precedence 49 for @{ 'oa_join $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 
+non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
+notation < "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
+
+notation > "hovbox(∨ f)" non associative with precedence 59
+for @{ 'oa_join $f }.
+notation > "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
+
+(*interpretation "o-algebra join" 'oa_join f = 
+  (fun12 ?? (oa_join ??) f).
+interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
+  (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
+*)
+nrecord ORelation (P,Q : OAlgebra) : Type[1] ≝ {
+  or_f :> P ⇒ Q;
+  or_f_minus_star : P ⇒ Q;
+  or_f_star : Q ⇒ P;
+  or_f_minus : Q ⇒ P;
+  or_prop1 : ∀p,q. (or_f p ≤ q) = (p ≤ or_f_star q);
+  or_prop2 : ∀p,q. (or_f_minus p ≤ q) = (p ≤ or_f_minus_star q);
+  or_prop3 : ∀p,q. (or_f p >< q) = (p >< or_f_minus q)
+}.
+ 
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+
+interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star ? ? r).
+interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus ? ? r).
+interpretation "o-relation f*" 'OR_f_star r = (or_f_star ? ? r).
+
+
+ndefinition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
+#P; #Q; @ (ORelation P Q); @
+ [ napply (λp,q.p = q)
+ | #x; napply refl1
+ | #x; #y; napply sym1
+ | #x; #y; #z; napply trans1 ]
+nqed.
+
+unification hint 0 ≔ P, Q ;
+  R ≟ (ORelation_setoid P Q)
+(* -------------------------- *) ⊢
+    carr1 R ≡ ORelation P Q.
+
+ndefinition or_f_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
+ (unary_morphism1_setoid1 P Q).
+ #P; #Q; @
+  [ napply or_f
+  | #a; #a'; #e; nassumption]
+nqed.
+
+unification hint 0 ≔ P, Q, r;
+ R ≟ (mk_unary_morphism1 … (or_f …) (prop11 … (or_f_morphism1 …)))
+(* ------------------------ *) ⊢
+  fun11 … R r ≡ or_f P Q r.
+
+nlemma ORelation_eq_respects_leq_or_f_minus_:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → ∀x. r⎻ x ≤ r'⎻ x.
+ #P; #Q; #a; #a'; #e; #x;
+ napply oa_density; #r; #H;
+ napply oa_overlap_sym;
+ napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
+ napply (. ?‡#)
+  [##2: napply (a r)
+  | ngeneralize in match r in ⊢ %;
+    nchange with (or_f … a' = or_f … a);
+    napply (.= †e^-1);
+    napply #]
+ napply (. (or_prop3 …));
+ napply oa_overlap_sym;
+ nassumption.
+nqed.
+
+nlemma ORelation_eq2:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → r⎻ = r'⎻.
+ #P; #Q; #a; #a'; #e; #x;
+ napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
+  [ napply e | napply e^-1]
+nqed.
+
+ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
+ (unary_morphism1_setoid1 Q P).
+ #P; #Q; @
+  [ napply or_f_minus
+  | napply ORelation_eq2]
+nqed.
+
+unification hint 0 ≔ P, Q, r;
+ R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
+(* ------------------------ *) ⊢
+  fun11 … R r ≡ or_f_minus P Q r.
+
+nlemma ORelation_eq_respects_leq_or_f_star_:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → ∀x. r* x ≤ r'* x.
+ #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
+ nchange with (or_f P Q a' (a* x) ≤ x);
+ napply (. ?‡#)
+  [##2: napply (a (a* x))
+  | ngeneralize in match (a* x);
+    nchange with (or_f P Q a' = or_f P Q a);
+    napply (.= †e^-1); napply #]
+ napply (. (or_prop1 …));
+ napply oa_leq_refl.
+nqed.
+
+nlemma ORelation_eq3:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → r* = r'*.
+ #P; #Q; #a; #a'; #e; #x;
+ napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
+  [ napply e | napply e^-1]
+nqed.
+
+ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
+ (unary_morphism1_setoid1 Q P).
+ #P; #Q; @
+  [ napply or_f_star
+  | napply ORelation_eq3] 
+nqed.
+
+unification hint 0 ≔ P, Q, r;
+ R ≟ (mk_unary_morphism1 … (or_f_star …) (prop11 … (or_f_star_morphism1 …)))
+(* ------------------------ *) ⊢
+  fun11 … R r ≡ or_f_star P Q r.
+
+nlemma ORelation_eq_respects_leq_or_f_minus_star_:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → ∀x. r⎻* x ≤ r'⎻* x.
+ #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
+ nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
+ napply (. ?‡#)
+  [##2: napply (a⎻ (a⎻* x))
+  | ngeneralize in match (a⎻* x);
+    nchange with (a'⎻ = a⎻);
+    napply (.= †e^-1); napply #]
+ napply (. (or_prop2 …));
+ napply oa_leq_refl.
+nqed.
+
+nlemma ORelation_eq4:
+ ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
+  r=r' → r⎻* = r'⎻*.
+ #P; #Q; #a; #a'; #e; #x;
+ napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
+  [ napply e | napply e^-1]
+nqed.
+
+ndefinition or_f_minus_star_morphism1:
+ ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) (unary_morphism1_setoid1 P Q).
+ #P; #Q; @
+  [ napply or_f_minus_star
+  | napply ORelation_eq4]
+nqed.
+
+unification hint 0 ≔ P, Q, r;
+ R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
+(* ------------------------ *) ⊢
+  fun11 … R r ≡ or_f_minus_star P Q r.
+
+(*CSC:
+ndefinition ORelation_composition : ∀P,Q,R. 
+  binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
+#P; #Q; #R; @
+[ #F; #G; @
+  [ napply (G ∘ F);
+  | apply rule (G⎻* ∘ F⎻* );
+  | apply (F* ∘ G* );
+  | apply (F⎻ ∘ G⎻);
+  | intros; 
+    change with ((G (F p) ≤ q) = (p ≤ (F* (G* q))));
+    apply (.= (or_prop1 :?));
+    apply (or_prop1 :?);
+  | intros;
+    change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q))));
+    apply (.= (or_prop2 :?));
+    apply or_prop2 ; 
+  | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q))));
+    apply (.= (or_prop3 :?));
+    apply or_prop3;
+  ]
+| intros; split; simplify; 
+   [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
+   |1: apply ((†e)‡(†e1));
+   |2,4: apply ((†e1)‡(†e));]]
+qed.
+
+definition OA : category2.
+split;
+[ apply (OAlgebra);
+| intros; apply (ORelation_setoid o o1);
+| intro O; split;
+  [1,2,3,4: apply id2;
+  |5,6,7:intros; apply refl1;] 
+| apply ORelation_composition;
+| intros (P Q R S F G H); split;
+   [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
+     apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
+   | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
+   | apply ((comp_assoc2 ????? F G H)^-1);
+   | apply ((comp_assoc2 ????? H* G* F* ));]
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
+qed.
+
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
+
+definition ORelation_setoid_of_arrows2_OA: 
+  ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
+
+prefer coercion Type_OF_objs2.
+*)
+(* alias symbol "eq" = "setoid1 eq". *)
+
+(* qui la notazione non va *)
+(*CSC
+nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
+ intros;
+ apply oa_leq_antisym;
+  [ apply oa_density; intros;
+    apply oa_overlap_sym;
+    unfold binary_join; simplify;
+    apply (. (oa_join_split : ?));
+    exists; [ apply false ]
+    apply oa_overlap_sym;
+    assumption
+  | unfold binary_join; simplify;
+    apply (. (oa_join_sup : ?)); intro;
+    cases i; whd in ⊢ (? ? ? ? ? % ?);
+     [ assumption | apply oa_leq_refl ]]
+qed.
+
+nlemma overlap_monotone_left: ∀S:OAlgebra.∀p,q,r:S. p ≤ q → p >< r → q >< r.
+ #S; #p; #q; #r; #H1; #H2;
+ apply (. (leq_to_eq_join : ?)‡#);
+  [ apply f;
+  | skip
+  | apply oa_overlap_sym;
+    unfold binary_join; simplify;
+    apply (. (oa_join_split : ?));
+    exists [ apply true ]
+    apply oa_overlap_sym;
+    assumption; ]
+qed.*)
+
+(* Part of proposition 9.9 *)
+nlemma f_minus_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
+ #S; #T; #R; #p; #q; #H;
+ napply (. (or_prop2 …));
+ napply oa_leq_trans; ##[##2: napply H; ##| ##skip |
+  napply (. (or_prop2 … q …)^ -1);(*CSC: why q?*) napply oa_leq_refl]
+nqed.
+ 
+(* Part of proposition 9.9 *)
+nlemma f_minus_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
+ #S; #T; #R; #p; #q; #H;
+ napply (. (or_prop2 … (R⎻* p) q)^ -1); (*CSC: why ?*)
+ napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop2 …)); napply oa_leq_refl]
+nqed.
+
+(* Part of proposition 9.9 *)
+nlemma f_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R p ≤ R q.
+ #S; #T; #R; #p; #q; #H;
+ napply (. (or_prop1 …));
+ napply oa_leq_trans; ##[##2: napply H; ##| ##skip | napply (. (or_prop1 … q …)^ -1); napply oa_leq_refl]
+nqed.
+
+(* Part of proposition 9.9 *)
+nlemma f_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R* p ≤ R* q.
+ #S; #T; #R; #p; #q; #H;
+ napply (. (or_prop1 … (R* p) q)^ -1);
+ napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop1 …)); napply oa_leq_refl]
+nqed.
+
+nlemma lemma_10_2_a: ∀S,T.∀R:ORelation S T.∀p. p ≤ R⎻* (R⎻ p).
+ #S; #T; #R; #p;
+ napply (. (or_prop2 … p …)^-1);
+ napply oa_leq_refl.
+nqed.
+
+lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
+ intros;
+ apply (. (or_prop2 : ?));
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
+ intros;
+ apply (. (or_prop1 : ?)^-1);
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
+ intros;
+ apply (. (or_prop1 : ?));
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
+ intros; apply oa_leq_antisym;
+  [ apply lemma_10_2_b;
+  | apply f_minus_image_monotone;
+    apply lemma_10_2_a; ]
+qed.
+
+lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
+ intros; apply oa_leq_antisym;
+  [ apply f_star_image_monotone;
+    apply (lemma_10_2_d ?? R p);
+  | apply lemma_10_2_c; ]
+qed.
+
+lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
+ intros; apply oa_leq_antisym;
+  [ apply lemma_10_2_d;
+  | apply f_image_monotone;
+    apply (lemma_10_2_c ?? R p); ]
+qed.
+
+lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
+ intros; apply oa_leq_antisym;
+  [ apply f_minus_star_image_monotone;
+    apply (lemma_10_2_b ?? R p);
+  | apply lemma_10_2_a; ]
+qed.
+
+lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
+ intros; apply (†(lemma_10_3_a ?? R p));
+qed.
+
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
+qed.
+
+lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
+ intros; split; intro; apply oa_overlap_sym; assumption.
+qed.
\ No newline at end of file
-- 
2.39.2