apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
qed.
-(*
-definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+definition extS: ∀X,S:REL. ∀r:X ⇒_\r1 S. Ω^S ⇒_1 Ω^X.
(* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
intros (X S r); constructor 1;
[ intro F; constructor 1; constructor 1;
[ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
| intros; split; intro; cases f (H1 H2); clear f; split;
- [ apply (. (H‡#)); assumption
- |3: apply (. (H\sup -1‡#)); assumption
+ [ apply (. (e^-1‡#)); assumption
+ |3: apply (. (e‡#)); assumption
|2,4: cases H2 (w H3); exists; [1,3: apply w]
- [ apply (. (#‡(H‡#))); assumption
- | apply (. (#‡(H \sup -1‡#))); assumption]]]
- | intros; split; simplify; intros; cases f; cases H1; split;
+ [ apply (. (#‡(e^-1‡#))); assumption
+ | apply (. (#‡(e‡#))); assumption]]]
+ | intros; split; simplify; intros; cases f; cases e1; split;
[1,3: assumption
|2,4: exists; [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H\sup -1)‡#); assumption]]]
+ [ apply (. (#‡e^-1)‡#); assumption
+ | apply (. (#‡e)‡#); assumption]]]
qed.
-
+(*
lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
intros;
unfold extS; simplify;
[ apply (. e^-1 a2 w); | apply (. e a2 w)] assumption;]
qed.
-interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) r).
-interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) r).
-interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) r).
+definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x.
+
+interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) (foo ?? r)).
+interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) (foo ?? r)).
+interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) (foo ?? r)).
definition image_coercion: ∀U,V:REL. (U ⇒_\r1 V) → Ω^U ⇒_2 Ω^V.
intros (U V r Us); apply (image U V r); qed.
exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]]
qed.
-theorem minus_star_image_id: ∀o:REL. (fun12 ?? (minus_star_image o o) (id1 REL o) : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
+theorem minus_star_image_id: ∀o:REL.
+ ((id1 REL o)⎻* : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
intros; unfold minus_star_image; simplify; intro U; simplify;
split; simplify; intros;
[ change with (a ∈ U); apply f; change with (a=a); apply refl1
| cases f1; cases x1; apply f; assumption]
qed.
+
(*
(*CSC: unused! *)
theorem ext_comp:
| cases H; clear H; cases x1; clear x1; exists [apply w]; split;
[2: cases f] assumption]
qed.
+*)
+
+axiom daemon : False.
theorem extS_singleton:
- ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
+ ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x.
intros; unfold extS; unfold ext; unfold singleton; simplify;
- split; intros 2; simplify; cases f; split; try assumption;
- [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
- assumption
- | exists; try assumption; split; try assumption; change with (x = x); apply refl]
-qed.
-*)
+ split; intros 2; simplify; simplify in f;
+ [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file