first [apply refl | assumption]]]
qed.
+(*
definition full_subset: ∀s:REL. Ω \sup s.
apply (λs.{x | True});
intros; simplify; split; intro; assumption.
cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
assumption]
qed.
-
+*)
+axiom daemon: False.
(* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) ?(*(Ω \sup V)*).
+cases daemon; qed.
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
- intros; simplify; split; intro; cases H1; exists [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H \sup -1)‡#); assumption]
- | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
- [ apply (. #‡(#‡H1)); cases x; split; try assumption;
- apply (if ?? (H ??)); assumption
- | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
- apply (if ?? (H \sup -1 ??)); assumption]]
+ intros; simplify; split; intro; cases H; exists [1,3: apply w]
+ [ apply (. (#‡e)‡#); assumption
+ | apply (. (#‡e ^ -1)‡#); assumption]
+ | intros; split; simplify; intros; cases H; exists [1,3: apply w]
+ [ apply (. #‡(#‡e1)); cases x; split; try assumption;
+ apply (if ?? (e ??)); assumption
+ | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
+ apply (if ?? (e ^ -1 ??)); assumption]]
qed.
+(*
(* the same as □ for a basic pair *)
definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
intros; constructor 1;
[ 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.
+*)
+
+include "o-algebra.ma".
+
+definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (SUBSETS o1) (SUBSETS o2).
+ intros;
+ constructor 1;
+ [
+ |
+ |
+ |
+ |
+ |
+ |
+ ]
qed.
\ No newline at end of file