Step
*
1
of Lemma
eclass2-eclass1-classrel
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
⊢ uiff(↓∃f1:B ─→ bag(C)
∃b:B. ((↓∃b:A. (b ∈ X(e) ∧ (f1 = (f loc(e) b) ∈ (B ─→ bag(C))))) ∧ b ∈ Y(e) ∧ v ↓∈ f1 b);↓∃a:A
∃b:B
(a ∈ X(e)
∧ b ∈ Y(e)
∧ v ↓∈ f loc(e) a
b))
BY
{ (RW (ReTopC ClassRelStepC) 0 THEN Auto) }
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
\mvdash{} uiff(\mdownarrow{}\mexists{}f1:B {}\mrightarrow{} bag(C)
\mexists{}b:B
((\mdownarrow{}\mexists{}b:A. (b \mmember{} X(e) \mwedge{} (f1 = (f loc(e) b)))) \mwedge{} b \mmember{} Y(e) \mwedge{} v \mdownarrow{}\mmember{} f1 b);\mdownarrow{}\mexists{}a:A
\mexists{}b:B
(a \mmember{} X(e)
\mwedge{} b \mmember{} Y(e)
\mwedge{} v \mdownarrow{}\mmember{} f loc(e) a
b))
By
(RW (ReTopC ClassRelStepC) 0 THEN Auto)
Home
Index