Step
*
2
3
1
2
2
1
2
1
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))
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. f1 : A-face(X;A;I;alpha)
17. f2 : A-face(X;A;I;alpha)
18. z : Cname
19. (z ∈ I)
20. ¬(z ∈ J)
21. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
22. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
23. ¬(x = z ∈ Cname)
24. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
25. j : ℕ(||bx|| + 1) + 1
26. ¬(j = 0 ∈ ℤ)
27. ¬(j = 1 ∈ ℤ)
28. k : ℕ
29. k < ||J|| + 1
30. (fst(bx[j - 2])) = [x / J][k] ∈ Cname
31. ¬(k = 0 ∈ ℤ)
⊢ k + 1 < ||[x; [z / J]]|| c∧ (J[k - 1] = [x; [z / J]][k + 1] ∈ Cname)
BY
{ D 0 }
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. ∀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. f1 : A-face(X;A;I;alpha)
17. f2 : A-face(X;A;I;alpha)
18. z : Cname
19. (z ∈ I)
20. ¬(z ∈ J)
21. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
22. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
23. ¬(x = z ∈ Cname)
24. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
25. j : ℕ(||bx|| + 1) + 1
26. ¬(j = 0 ∈ ℤ)
27. ¬(j = 1 ∈ ℤ)
28. k : ℕ
29. k < ||J|| + 1
30. (fst(bx[j - 2])) = [x / J][k] ∈ Cname
31. ¬(k = 0 ∈ ℤ)
⊢ k + 1 < ||[x; [z / J]]||
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. ∀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. f1 : A-face(X;A;I;alpha)
17. f2 : A-face(X;A;I;alpha)
18. z : Cname
19. (z ∈ I)
20. ¬(z ∈ J)
21. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
22. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
23. ¬(x = z ∈ Cname)
24. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
25. j : ℕ(||bx|| + 1) + 1
26. ¬(j = 0 ∈ ℤ)
27. ¬(j = 1 ∈ ℤ)
28. k : ℕ
29. k < ||J|| + 1
30. (fst(bx[j - 2])) = [x / J][k] ∈ Cname
31. ¬(k = 0 ∈ ℤ)
32. k + 1 < ||[x; [z / J]]||
⊢ J[k - 1] = [x; [z / J]][k + 1] ∈ Cname
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>)
13. (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>)
14. (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>))
15. (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2)))
16. f1 : A-face(X;A;I;alpha)
17. f2 : A-face(X;A;I;alpha)
18. z : Cname
19. (z \mmember{} I)
20. \mneg{}(z \mmember{} J)
21. A-face-name(f1) = <z, 0>
22. A-face-name(f2) = <z, 1>
23. \mneg{}(x = z)
24. (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f) \mwedge{} A-face-compatible(X;A;I;alpha;f2;f))
25. j : \mBbbN{}(||bx|| + 1) + 1
26. \mneg{}(j = 0)
27. \mneg{}(j = 1)
28. k : \mBbbN{}
29. k < ||J|| + 1
30. (fst(bx[j - 2])) = [x / J][k]
31. \mneg{}(k = 0)
\mvdash{} k + 1 < ||[x; [z / J]]|| c\mwedge{} (J[k - 1] = [x; [z / J]][k + 1])
By
Latex:
D 0
Home
Index