Step
*
2
of Lemma
extend-A-open-box_wf
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ((∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
13. f1 : A-face(X;A;I;alpha)
14. f2 : A-face(X;A;I;alpha)
15. z : Cname
16. (z ∈ I)
17. ¬(z ∈ J)
18. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
19. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
20. ¬(x = z ∈ Cname)
21. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ ((∀y:nameset([z / J]). ∀c:ℕ2. (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈[f1; [f2 / bx]].¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈[f1; [f2 / bx]].(fst(f) ∈ [x; [z / J]]))
∧ (∀f1,f2∈[f1; [f2 / bx]]. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
BY
{ TACTIC:(RepeatFor 2 (ParallelOp -10) THEN Auto) }
1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. (∀f∈bx.(fst(f) ∈ [x / J]))
13. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
26. y : nameset([z / J])
27. c : ℕ2
⊢ (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
2
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. (∀f∈bx.(fst(f) ∈ [x / J]))
13. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
14. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
15. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
16. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
3
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ (∀f∈[f1; [f2 / bx]].(fst(f) ∈ [x; [z / J]]))
4
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f∈bx.(fst(f) ∈ [x / J]))
16. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ (∀f1,f2∈[f1; [f2 / bx]]. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : \mBbbN{}2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. \mneg{}(x \mmember{} J)
11. l\_subset(Cname;J;I)
12. ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2)))
13. f1 : A-face(X;A;I;alpha)
14. f2 : A-face(X;A;I;alpha)
15. z : Cname
16. (z \mmember{} I)
17. \mneg{}(z \mmember{} J)
18. A-face-name(f1) = <z, 0>
19. A-face-name(f2) = <z, 1>
20. \mneg{}(x = z)
21. (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f) \mwedge{} A-face-compatible(X;A;I;alpha;f2;f))
\mvdash{} ((\mforall{}y:nameset([z / J]). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}[f1; [f2 / bx]]. A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}[f1; [f2 / bx]]. A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}[f1; [f2 / bx]].\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}[f1; [f2 / bx]].(fst(f) \mmember{} [x; [z / J]]))
\mwedge{} (\mforall{}f1,f2\mmember{}[f1; [f2 / bx]]. \mneg{}(A-face-name(f1) = A-face-name(f2)))
By
Latex:
TACTIC:(RepeatFor 2 (ParallelOp -10) THEN Auto)
Home
Index