---

Step * of Lemma length-open_box

No Annotations
∀[X:CubicalSet]. ∀[I:Cname List].
  ∀J:nameset(I) List
    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  (||box|| = (1 + (||remove-repeats(CnameDeq;J)|| * 2)) ∈ ℤ)
BY
{ (Auto
   THEN (Assert CnameDeq ∈ EqDecider(nameset(I)) BY
               (Unfold `nameset` 0 THEN Auto))
   THEN (DVar `box' THEN SplitAndHyps)
   THEN (BLemma `equipollent-nsub` THENA Auto)
   THEN (RWW "equipollent-add< equipollent-multiply< nameset-equipollent<" 0 THENA Auto)) }

1
1. X : CubicalSet
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(X;I) List
7. adjacent-compatible(X;I;box)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. CnameDeq ∈ EqDecider(nameset(I))
⊢ ℕ||box|| ~ ℕ1 + (nameset(J) × ℕ2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].
    \mforall{}J:nameset(I)  List
        \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[box:open\_box(X;I;J;x;i)].
            (||box||  =  (1  +  (||remove-repeats(CnameDeq;J)||  *  2)))


By

---

Latex:
(Auto
  THEN  (Assert  CnameDeq  \mmember{}  EqDecider(nameset(I))  BY
                          (Unfold  `nameset`  0  THEN  Auto))
  THEN  (DVar  `box'  THEN  SplitAndHyps)
  THEN  (BLemma  `equipollent-nsub`  THENA  Auto)
  THEN  (RWW  "equipollent-add<  equipollent-multiply<  nameset-equipollent<"  0  THENA  Auto))

---

Home Index