---

Step * 1 1 1 1 1 of Lemma cubical-interval-filler-fills


1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. u : I-face(cubical-interval();I)
5. (||[u]|| = 1 ∈ ℤ) ∧ (face-name(hd([u])) = <x, i> ∈ (nameset(I) × ℕ2))
6. j : ℤ
7. j = 0 ∈ ℤ
⊢ (dimension(u):=direction(u))(cube(u)) = cube(u) ∈ cubical-interval()(I-[dimension(u)])
BY
{ ((GenConclTerm ⌜cube(u)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜dimension(u)⌝;⌜direction(u)⌝]⋅
   THEN All Thin
   THEN Auto) }

1
1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : cubical-interval()(I-[v])
⊢ (v:=v1)(v@0) = v@0 ∈ cubical-interval()(I-[v])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  nameset(I)
3.  i  :  \mBbbN{}2
4.  u  :  I-face(cubical-interval();I)
5.  (||[u]||  =  1)  \mwedge{}  (face-name(hd([u]))  =  <x,  i>)
6.  j  :  \mBbbZ{}
7.  j  =  0
\mvdash{}  (dimension(u):=direction(u))(cube(u))  =  cube(u)


By

---

Latex:
((GenConclTerm  \mkleeneopen{}cube(u)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}dimension(u)\mkleeneclose{};\mkleeneopen{}direction(u)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto)

---

Home Index