---

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


1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. i : ℕ2
5. bx : open_box(cubical-interval();I;J;x;i)
6. i@0 : ℕ||bx||
⊢ is-face(cubical-interval();I;cubical-interval-filler() I J x i bx;bx[i@0])
BY
{ (RenameVar `j' (-1)
   THEN RepUR ``cubical-interval-filler`` 0
   THEN ((BoolCase ⌜null(J)⌝⋅ THENA Auto)
         THENL [(DVar `J' THEN Try ((ImpossibleEq Auto (-1) THEN Auto)) THEN Thin (-1))
               ; TACTIC:((Assert ⌜nameset(J) ⊆r nameset(I)⌝⋅ THENA (DVar `bx' THEN Auto))
                         THEN (GenConcl ⌜hd(J) = y ∈ nameset(J)⌝⋅ THENA (Unfold `nameset` 0 THEN Auto))
                         )]
   )) }

1
1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. bx : open_box(cubical-interval();I;[];x;i)
5. j : ℕ||bx||
⊢ is-face(cubical-interval();I;cube(hd(bx));bx[j])

2
1. I : Cname List
2. J : nameset(I) List
3. ¬(J = [] ∈ (nameset(I) List))
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-interval();I;J;x;i)
7. j : ℕ||bx||
8. nameset(J) ⊆r nameset(I)
9. y : nameset(J)
10. hd(J) = y ∈ nameset(J)
⊢ is-face(cubical-interval();I;λL.cube(get_face(y;L y;bx))(L);bx[j])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  nameset(I)  List
3.  x  :  nameset(I)
4.  i  :  \mBbbN{}2
5.  bx  :  open\_box(cubical-interval();I;J;x;i)
6.  i@0  :  \mBbbN{}||bx||
\mvdash{}  is-face(cubical-interval();I;cubical-interval-filler()  I  J  x  i  bx;bx[i@0])


By

---

Latex:
(RenameVar  `j'  (-1)
  THEN  RepUR  ``cubical-interval-filler``  0
  THEN  ((BoolCase  \mkleeneopen{}null(J)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(DVar  `J'  THEN  Try  ((ImpossibleEq  Auto  (-1)  THEN  Auto))  THEN  Thin  (-1))
                          ;  TACTIC:((Assert  \mkleeneopen{}nameset(J)  \msubseteq{}r  nameset(I)\mkleeneclose{}\mcdot{}  THENA  (DVar  `bx'  THEN  Auto))
                                              THEN  (GenConcl  \mkleeneopen{}hd(J)  =  y\mkleeneclose{}\mcdot{}  THENA  (Unfold  `nameset`  0  THEN  Auto))
                                              )]
  ))

---

Home Index