---

Step * 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])
⊢ 1 ≤ (||filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))|| + 1)
BY
{ (GenConclTerm ⌜filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v))⌝⋅ THENA Auto) }

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 ∈ remove-repeats(CnameDeq;v))
⊢ x1 ∈ nameset(I)

2
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. v1 : Cname List
15. filter(λx.(¬b(CnameDeq x u));remove-repeats(CnameDeq;v)) = v1 ∈ (Cname List)
⊢ 1 ≤ (||v1|| + 1)

---

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])
\mvdash{}  1  \mleq{}  (||filter(\mlambda{}x.(\mneg{}\msubb{}(CnameDeq  x  u));remove-repeats(CnameDeq;v))||  +  1)


By

---

Latex:
(GenConclTerm  \mkleeneopen{}filter(\mlambda{}x.(\mneg{}\msubb{}(CnameDeq  x  u));remove-repeats(CnameDeq;v))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index