Step
*
1
1
of Lemma
memory-class3-classrel
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ B ─→ B
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ B ─→ B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. ¬↑first(e)
16. v : B
⊢ uiff(↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b (tr1 o X1) || (tr2 o X2) || (tr3 o X3)
then ∃f:B ─→ B. (f ∈ (tr1 o X1) || (tr2 o X2) || (tr3 o X3)(pred(e)) ∧ (v = (f b) ∈ B))
else v = b ∈ B
fi );↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3
then (∃a1:A1. (a1 ∈ X1(pred(e)) ∧ (v = (tr1 loc(e) a1 b) ∈ B)))
∨ (∃a2:A2. (a2 ∈ X2(pred(e)) ∧ (v = (tr2 loc(e) a2 b) ∈ B)))
∨ (∃a3:A3. (a3 ∈ X3(pred(e)) ∧ (v = (tr3 loc(e) a3 b) ∈ B)))
else v = b ∈ B
fi ))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
THEN SquashExRepD
THEN (SplitOnHypITE (-1) THENA Auto)
THEN Repeat ((RWO "member-parallel-class-bool" (-1) THENA Auto))
THEN Repeat ((RWO "member-eclass-eclass1" (-1) THENA Auto))
THEN ExRepD) }
1
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ B ─→ B
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ B ─→ B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. ¬↑first(e)
16. v : B
17. b : B
18. b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
19. f : B ─→ B
20. f ∈ (tr1 o X1) || (tr2 o X2) || (tr3 o X3)(pred(e))
21. v = (f b) ∈ B
22. ↑(pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3)
⊢ ↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3
then (∃a1:A1. (a1 ∈ X1(pred(e)) ∧ (v = (tr1 loc(e) a1 b) ∈ B)))
∨ (∃a2:A2. (a2 ∈ X2(pred(e)) ∧ (v = (tr2 loc(e) a2 b) ∈ B)))
∨ (∃a3:A3. (a3 ∈ X3(pred(e)) ∧ (v = (tr3 loc(e) a3 b) ∈ B)))
else v = b ∈ B
fi )
2
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ B ─→ B
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ B ─→ B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. ¬↑first(e)
16. v : B
17. b : B
18. b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
19. v = b ∈ B
20. ¬↑(pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3)
⊢ ↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3
then (∃a1:A1. (a1 ∈ X1(pred(e)) ∧ (v = (tr1 loc(e) a1 b) ∈ B)))
∨ (∃a2:A2. (a2 ∈ X2(pred(e)) ∧ (v = (tr2 loc(e) a2 b) ∈ B)))
∨ (∃a3:A3. (a3 ∈ X3(pred(e)) ∧ (v = (tr3 loc(e) a3 b) ∈ B)))
else v = b ∈ B
fi )
3
.....truecase.....
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ B ─→ B
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ B ─→ B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. ¬↑first(e)
16. v : B
17. b : B
18. b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
19. (∃a1:A1. (a1 ∈ X1(pred(e)) ∧ (v = (tr1 loc(e) a1 b) ∈ B)))
∨ (∃a2:A2. (a2 ∈ X2(pred(e)) ∧ (v = (tr2 loc(e) a2 b) ∈ B)))
∨ (∃a3:A3. (a3 ∈ X3(pred(e)) ∧ (v = (tr3 loc(e) a3 b) ∈ B)))
20. (↑pred(e) ∈b X1) ∨ (↑pred(e) ∈b X2) ∨ (↑pred(e) ∈b X3)
⊢ ↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b (tr1 o X1) || (tr2 o X2) || (tr3 o X3)
then ∃f:B ─→ B. (f ∈ (tr1 o X1) || (tr2 o X2) || (tr3 o X3)(pred(e)) ∧ (v = (f b) ∈ B))
else v = b ∈ B
fi )
4
.....falsecase.....
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ B ─→ B
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ B ─→ B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. ¬↑first(e)
16. v : B
17. b : B
18. b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
19. v = b ∈ B
20. ¬((↑pred(e) ∈b X1) ∨ (↑pred(e) ∈b X2) ∨ (↑pred(e) ∈b X3))
⊢ ↓∃b:B
(b ∈ loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
∧ if pred(e) ∈b (tr1 o X1) || (tr2 o X2) || (tr3 o X3)
then ∃f:B ─→ B. (f ∈ (tr1 o X1) || (tr2 o X2) || (tr3 o X3)(pred(e)) ∧ (v = (f b) ∈ B))
else v = b ∈ B
fi )
Latex:
Latex:
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. B : Type
6. init : Id {}\mrightarrow{} B
7. tr1 : Id {}\mrightarrow{} A1 {}\mrightarrow{} B {}\mrightarrow{} B
8. X1 : EClass(A1)
9. tr2 : Id {}\mrightarrow{} A2 {}\mrightarrow{} B {}\mrightarrow{} B
10. X2 : EClass(A2)
11. tr3 : Id {}\mrightarrow{} A3 {}\mrightarrow{} B {}\mrightarrow{} B
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. \mneg{}\muparrow{}first(e)
16. v : B
\mvdash{} uiff(\mdownarrow{}\mexists{}b:B
(b \mmember{} loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);\mlambda{}loc.\{init loc\})(pred(e))
\mwedge{} if pred(e) \mmember{}\msubb{} (tr1 o X1) || (tr2 o X2) || (tr3 o X3)
then \mexists{}f:B {}\mrightarrow{} B. (f \mmember{} (tr1 o X1) || (tr2 o X2) || (tr3 o X3)(pred(e)) \mwedge{} (v = (f b)))
else v = b
fi );\mdownarrow{}\mexists{}b:B
(b \mmember{} loop-class-memory((tr1 o X1) || (tr2 o X2) || (tr3 o X3);\mlambda{}loc.\{init loc\})(
pred(e))
\mwedge{} if pred(e) \mmember{}\msubb{} X1 \mvee{}\msubb{}pred(e) \mmember{}\msubb{} X2 \mvee{}\msubb{}pred(e) \mmember{}\msubb{} X3
then (\mexists{}a1:A1. (a1 \mmember{} X1(pred(e)) \mwedge{} (v = (tr1 loc(e) a1 b))))
\mvee{} (\mexists{}a2:A2. (a2 \mmember{} X2(pred(e)) \mwedge{} (v = (tr2 loc(e) a2 b))))
\mvee{} (\mexists{}a3:A3. (a3 \mmember{} X3(pred(e)) \mwedge{} (v = (tr3 loc(e) a3 b))))
else v = b
fi ))
By
Latex:
(RepeatFor 2 ((D 0 THENA Auto))
THEN SquashExRepD
THEN (SplitOnHypITE (-1) THENA Auto)
THEN Repeat ((RWO "member-parallel-class-bool" (-1) THENA Auto))
THEN Repeat ((RWO "member-eclass-eclass1" (-1) THENA Auto))
THEN ExRepD)
Home
Index