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

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

1
1. fset(ℕ)
2. {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
4. fset(ℕ)
5. I,phi(J)
6. f ∈ J ⟶ I
7. (phi f) 1
⊢ s ⋅ (i1) ⋅ f ∈ J ⟶ I


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{}  (i1)  \mcdot{}  f  =  f


By


Latex:
(RWO    "nh-comp-assoc"  0  THEN  Auto)




Home Index