---

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


1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : name-morph(I-[v];[]) ⟶ ℕ2
5. x : name-morph(I-[v];[])
⊢ ∀x1:nameset(I-[v]). ((((v:=v1) o x) x1) = (x x1) ∈ extd-nameset([]))
BY
{ ((D 0 THENA Auto) THEN RepUR ``face-map name-comp uext`` 0 THEN (BoolCase ⌜(x1 =z v)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : name-morph(I-[v];[]) ⟶ ℕ2
5. x : name-morph(I-[v];[])
6. x1 : nameset(I-[v])
7. x1 = v ∈ ℤ
⊢ if isname(v1) then x v1 else v1 fi  = (x x1) ∈ extd-nameset([])

2
1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : name-morph(I-[v];[]) ⟶ ℕ2
5. x : name-morph(I-[v];[])
6. x1 : nameset(I-[v])
7. x1 ≠ v
⊢ if isname(x1) then x x1 else x1 fi  = (x x1) ∈ extd-nameset([])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  v  :  nameset(I)
3.  v1  :  \mBbbN{}2
4.  v@0  :  name-morph(I-[v];[])  {}\mrightarrow{}  \mBbbN{}2
5.  x  :  name-morph(I-[v];[])
\mvdash{}  \mforall{}x1:nameset(I-[v]).  ((((v:=v1)  o  x)  x1)  =  (x  x1))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepUR  ``face-map  name-comp  uext``  0  THEN  (BoolCase  \mkleeneopen{}(x1  =\msubz{}  v)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index