Step
*
2
3
1
2
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. (∀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))
26. j : ℕ(||bx|| + 1) + 1
27. ¬(j = 0 ∈ ℤ)
28. ¬(j = 1 ∈ ℤ)
⊢ (fst([f1; [f2 / bx]][j]) ∈ [x; [z / J]])
BY
{ ((Subst' [f1; [f2 / bx]][j] ~ bx[j - 2] 0 THENA (RWW "select-cons-tl" 0 THEN Auto))
THEN OnMaybeHyp 16 (\h. ((With ⌜j - 2⌝ (D h)⋅ THENA Complete (Auto))
THEN RepeatFor 2 (D -1)
THEN Reduce (-2)
THEN RenameVar `k' (-3)
THEN (CaseNat 0 `k'
THENL [(HypSubst' (-1) (-2) THEN Reduce (-2) THEN HypSubst' (-2) 0 THEN Auto)
; TACTIC:(HypSubst' (-2) 0 THEN (RWO "select-cons-tl" 0 THENA 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. ∀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 ∈ ℤ)
⊢ 0 < k
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 ∈ ℤ)
⊢ (J[k - 1] ∈ [x; [z / J]])
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. (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z \mmember{} I)
21. \mneg{}(z \mmember{} J)
22. A-face-name(f1) = <z, 0>
23. A-face-name(f2) = <z, 1>
24. \mneg{}(x = z)
25. (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f) \mwedge{} A-face-compatible(X;A;I;alpha;f2;f))
26. j : \mBbbN{}(||bx|| + 1) + 1
27. \mneg{}(j = 0)
28. \mneg{}(j = 1)
\mvdash{} (fst([f1; [f2 / bx]][j]) \mmember{} [x; [z / J]])
By
Latex:
((Subst' [f1; [f2 / bx]][j] \msim{} bx[j - 2] 0 THENA (RWW "select-cons-tl" 0 THEN Auto))
THEN OnMaybeHyp 16 (\mbackslash{}h. ((With \mkleeneopen{}j - 2\mkleeneclose{} (D h)\mcdot{} THENA Complete (Auto))
THEN RepeatFor 2 (D -1)
THEN Reduce (-2)
THEN RenameVar `k' (-3)
THEN (CaseNat 0 `k'
THENL [(HypSubst' (-1) (-2)
THEN Reduce (-2)
THEN HypSubst' (-2) 0
THEN Auto)
; TACTIC:(HypSubst' (-2) 0
THEN (RWO "select-cons-tl" 0 THENA Auto)
)]
)))
)
Home
Index