(* ------------------------ *) ⊢
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;
+ [ napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*)
+ | napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)
+ | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
+ | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
+ napply (or_prop1 …)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop2 … F …));
+ napply or_prop2
+ | #p; #q; nnormalize;
+ napply (.= (or_prop3 … G …));
+ napply or_prop3
]
-| intros; split; simplify;
- [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
- |1: apply ((†e)‡(†e1));
- |2,4: apply ((†e1)‡(†e));]]
-qed.
+##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
+nqed.
-definition OA : category2.
+(*
+ndefinition OA : category2.
split;
[ apply (OAlgebra);
| intros; apply (ORelation_setoid o o1);