---

Step * 1 of Lemma comp-nc-0-subset-I_cube

.....subterm..... T:t
4:n
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
4. J : fset(ℕ)
5. f : I,phi(J)
6. f ∈ J ⟶ I
7. (phi f) = 1
⊢ s ⋅ (i0) ⋅ f = f ∈ J ⟶ I
BY
{ (DVar `i' THEN RWW "nh-comp-assoc s-comp-nc-0" 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
4:n
1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  phi  :  \mBbbF{}(I)
4.  J  :  fset(\mBbbN{})
5.  f  :  I,phi(J)
6.  f  \mmember{}  J  {}\mrightarrow{}  I
7.  (phi  f)  =  1
\mvdash{}  s  \mcdot{}  (i0)  \mcdot{}  f  =  f


By

---

Latex:
(DVar  `i'  THEN  RWW  "nh-comp-assoc  s-comp-nc-0"  0  THEN  Auto)

---

Home Index