---

Step * 1 1 2 2 1 1 1 1 of Lemma open_box-nil


1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. x1 : nameset(I)
6. u3 : ℕ2
7. u4 : X(I-[x1])
8. x2 : nameset(I)
9. u6 : ℕ2
10. u7 : X(I-[x2])
11. v : I-face(X;I) List
12. adjacent-compatible(X;I;[<x1, u3, u4>; [<x2, u6, u7> / v]])
13. ¬(x ∈ [])
14. l_subset(Cname;[];I)
15. ∀y:nameset([]). ∀c:ℕ2.  (∃f∈[<x1, u3, u4>; [<x2, u6, u7> / v]]. <fst(f), fst(snd(f))> = <y, c> ∈ (nameset(I) × ℕ2))
16. (∃f∈[<x1, u3, u4>; [<x2, u6, u7> / v]]. <fst(f), fst(snd(f))> = <x, i> ∈ (nameset(I) × ℕ2))
17. (∀f∈[<x1, u3, u4>; [<x2, u6, u7> / v]].¬(<fst(f), fst(snd(f))> = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
18. (∀f∈[<x1, u3, u4>; [<x2, u6, u7> / v]].(fst(f) ∈ [x]))
19. (fst(<x1, u3, u4>)) = x ∈ Cname
20. (fst(<x2, u6, u7>)) = x ∈ Cname
21. ¬(<x1, u3> = <x, 1 - i> ∈ (nameset(I) × ℕ2))
22. ¬(<x2, u6> = <x, 1 - i> ∈ (nameset(I) × ℕ2))
⊢ <x1, u3> = <x2, u6> ∈ (nameset(I) × ℕ2)
BY
{ TACTIC:(All Reduce THEN Eliminate ⌜x1⌝⋅ THEN Eliminate ⌜x2⌝⋅ THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. x1 : nameset(I)
6. u3 : ℕ2
7. u4 : X(I-[x])
8. x2 : nameset(I)
9. u6 : ℕ2
10. u7 : X(I-[x])
11. v : I-face(X;I) List
12. adjacent-compatible(X;I;[<x, u3, u4>; [<x, u6, u7> / v]])
13. ¬(x ∈ [])
14. l_subset(Cname;[];I)
15. ∀y:nameset([]). ∀c:ℕ2.  (∃f∈[<x, u3, u4>; [<x, u6, u7> / v]]. <fst(f), fst(snd(f))> = <y, c> ∈ (nameset(I) × ℕ2))
16. (∃f∈[<x, u3, u4>; [<x, u6, u7> / v]]. <fst(f), fst(snd(f))> = <x, i> ∈ (nameset(I) × ℕ2))
17. (∀f∈[<x, u3, u4>; [<x, u6, u7> / v]].¬(<fst(f), fst(snd(f))> = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
18. (∀f∈[<x, u3, u4>; [<x, u6, u7> / v]].(fst(f) ∈ [x]))
19. x1 = x ∈ Cname
20. x2 = x ∈ Cname
21. ¬(<x, u3> = <x, 1 - i> ∈ (nameset(I) × ℕ2))
22. ¬(<x, u6> = <x, 1 - i> ∈ (nameset(I) × ℕ2))
⊢ u3 = u6 ∈ ℕ2

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  x  :  nameset(I)
4.  i  :  \mBbbN{}2
5.  x1  :  nameset(I)
6.  u3  :  \mBbbN{}2
7.  u4  :  X(I-[x1])
8.  x2  :  nameset(I)
9.  u6  :  \mBbbN{}2
10.  u7  :  X(I-[x2])
11.  v  :  I-face(X;I)  List
12.  adjacent-compatible(X;I;[<x1,  u3,  u4>  [<x2,  u6,  u7>  /  v]])
13.  \mneg{}(x  \mmember{}  [])
14.  l\_subset(Cname;[];I)
15.  \mforall{}y:nameset([]).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}[<x1,  u3,  u4>  [<x2,  u6,  u7>  /  v]].  <fst(f),  fst(snd(f))>  =  <y,  c>)
16.  (\mexists{}f\mmember{}[<x1,  u3,  u4>  [<x2,  u6,  u7>  /  v]].  <fst(f),  fst(snd(f))>  =  <x,  i>)
17.  (\mforall{}f\mmember{}[<x1,  u3,  u4>  [<x2,  u6,  u7>  /  v]].\mneg{}(<fst(f),  fst(snd(f))>  =  <x,  1  -  i>))
18.  (\mforall{}f\mmember{}[<x1,  u3,  u4>  [<x2,  u6,  u7>  /  v]].(fst(f)  \mmember{}  [x]))
19.  (fst(<x1,  u3,  u4>))  =  x
20.  (fst(<x2,  u6,  u7>))  =  x
21.  \mneg{}(<x1,  u3>  =  <x,  1  -  i>)
22.  \mneg{}(<x2,  u6>  =  <x,  1  -  i>)
\mvdash{}  <x1,  u3>  =  <x2,  u6>


By

---

Latex:
TACTIC:(All  Reduce  THEN  Eliminate  \mkleeneopen{}x1\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}x2\mkleeneclose{}\mcdot{}  THEN  EqCD  THEN  Auto)

---

Home Index