---

Step * 1 1 1 1 2 1 1 1 of Lemma length-open_box-ge-3


1. X : CubicalSet
2. I : Cname List
3. u : nameset(I)
4. v : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(X;I;[u / v];x;i)
8. 3 < 1 + (||remove-repeats(CnameDeq;[u / v])|| * 2)
9. CnameDeq ∈ EqDecider(nameset(I))
10. 1 < ||remove-repeats(CnameDeq;[u / v])||
11. (u ∈ [u / v])
12. y : Cname
13. (y ∈ I)
14. (y ∈ [u / v])
15. ¬(y = u ∈ Cname)
⊢ (∃j1∈[u / v]. (∃j2∈[u / v]. ¬(j1 = j2 ∈ Cname)))
BY
{ ((With ⌜0⌝ (D 0)⋅ THENA Auto) THEN Reduce 0) }

1
1. X : CubicalSet
2. I : Cname List
3. u : nameset(I)
4. v : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(X;I;[u / v];x;i)
8. 3 < 1 + (||remove-repeats(CnameDeq;[u / v])|| * 2)
9. CnameDeq ∈ EqDecider(nameset(I))
10. 1 < ||remove-repeats(CnameDeq;[u / v])||
11. (u ∈ [u / v])
12. y : Cname
13. (y ∈ I)
14. (y ∈ [u / v])
15. ¬(y = u ∈ Cname)
⊢ (∃j2∈[u / v]. ¬(u = j2 ∈ Cname))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  u  :  nameset(I)
4.  v  :  nameset(I)  List
5.  x  :  nameset(I)
6.  i  :  \mBbbN{}2
7.  box  :  open\_box(X;I;[u  /  v];x;i)
8.  3  <  1  +  (||remove-repeats(CnameDeq;[u  /  v])||  *  2)
9.  CnameDeq  \mmember{}  EqDecider(nameset(I))
10.  1  <  ||remove-repeats(CnameDeq;[u  /  v])||
11.  (u  \mmember{}  [u  /  v])
12.  y  :  Cname
13.  (y  \mmember{}  I)
14.  (y  \mmember{}  [u  /  v])
15.  \mneg{}(y  =  u)
\mvdash{}  (\mexists{}j1\mmember{}[u  /  v].  (\mexists{}j2\mmember{}[u  /  v].  \mneg{}(j1  =  j2)))


By

---

Latex:
((With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)  THEN  Reduce  0)

---

Home Index