apply (if ?? (e ^ -1 ??)); assumption]]
qed.
-(*
(* minus_image is the same as ext *)
theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
intros; unfold image; simplify; split; simplify; intros;
[ change with (a ∈ U);
- cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
+ cases e; cases x; change in f with (eq1 ? w a); apply (. f^-1‡#); assumption
| change in f with (a ∈ U);
- exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
+ exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]]
qed.
theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
intros; unfold minus_star_image; simplify; split; simplify; intros;
- [ change with (a ∈ U); apply H; change with (a=a); apply refl
- | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
+ [ change with (a ∈ U); apply f; change with (a=a); apply refl1
+ | change in f1 with (eq1 ? x a); apply (. f1‡#); apply f]
qed.
+alias symbol "compose" (instance 2) = "category1 composition".
theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
- intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
+ intros; unfold image; simplify; split; simplify; intros; cases e; clear e; cases x;
clear x; [ cases f; clear f; | cases f1; clear f1 ]
exists; try assumption; cases x; clear x; split; try assumption;
exists; try assumption; split; assumption.
∀A,B,C,r,s,X.
minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
- [ apply H; exists; try assumption; split; assumption
- | change with (x ∈ X); cases f; cases x1; apply H; assumption]
+ [ apply f; exists; try assumption; split; assumption
+ | change with (x ∈ X); cases f1; cases x1; apply f; assumption]
qed.
+(*
(*CSC: unused! *)
theorem ext_comp:
∀o1,o2,o3: REL.