---

Step * 1 1 1 1 1 1 of Lemma length-open_box-le-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. ¬False
9. (1 + ((||filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))|| + 1) * 2)) ≤ 3
10. CnameDeq ∈ EqDecider(nameset(I))
11. (||filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))|| + 1) ≤ 1
12. j' : nameset(I)
13. (j' ∈ [u / v])
14. ∀x:Cname. ((x ∈ remove-repeats(CnameDeq;v)) ∈ Type)
15. x1 : Cname
16. (x1 ∈ remove-repeats(CnameDeq;v))
⊢ x1 ∈ nameset(I)
BY
{ GenListD (-1) }

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. ¬False
9. (1 + ((||filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))|| + 1) * 2)) ≤ 3
10. CnameDeq ∈ EqDecider(nameset(I))
11. (||filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))|| + 1) ≤ 1
12. j' : nameset(I)
13. (j' ∈ [u / v])
14. ∀x:Cname. ((x ∈ remove-repeats(CnameDeq;v)) ∈ Type)
15. x1 : Cname
16. (x1 ∈ v)
⊢ x1 ∈ nameset(I)

---

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.  \mneg{}False
9.  (1  +  ((||filter(\mlambda{}x.(\mneg{}\msubb{}(CnameDeq  x  u));remove-repeats(CnameDeq;v))||  +  1)  *  2))  \mleq{}  3
10.  CnameDeq  \mmember{}  EqDecider(nameset(I))
11.  (||filter(\mlambda{}x.(\mneg{}\msubb{}(CnameDeq  x  u));remove-repeats(CnameDeq;v))||  +  1)  \mleq{}  1
12.  j'  :  nameset(I)
13.  (j'  \mmember{}  [u  /  v])
14.  \mforall{}x:Cname.  ((x  \mmember{}  remove-repeats(CnameDeq;v))  \mmember{}  Type)
15.  x1  :  Cname
16.  (x1  \mmember{}  remove-repeats(CnameDeq;v))
\mvdash{}  x1  \mmember{}  nameset(I)


By

---

Latex:
GenListD  (-1)

---

Home Index