Step * 1 1 1 1 of Lemma streamless-dec-equal

.....truecase..... 
1. [T] Type
2. ∀f:ℕ ⟶ T. ∃i,j:ℕ((¬(i j ∈ ℕ)) ∧ ((f i) (f j) ∈ T))
3. T
4. T
5. f:(ℕ ⟶ T) ⟶ ℕ
6. ∀f:ℕ ⟶ T. ∃j:ℕ((¬((F f) j ∈ ℕ)) ∧ ((f (F f)) (f j) ∈ T))
7. : ℕ
8. ¬((F n.x)) j ∈ ℕ)
9. x ∈ T
10. j1 : ℕ
11. ¬((F n.if (n =z n.x)) then else fi )) j1 ∈ ℕ)
12. if (j1 =z n.x)) then else fi  ∈ T
13. (F n.if (n =z n.x)) then else fi )) (F n.x)) ∈ ℤ
⊢ Dec(x y ∈ T)
BY
xxxHypSubst' (-1) (-3)xxx }

1
1. [T] Type
2. ∀f:ℕ ⟶ T. ∃i,j:ℕ((¬(i j ∈ ℕ)) ∧ ((f i) (f j) ∈ T))
3. T
4. T
5. f:(ℕ ⟶ T) ⟶ ℕ
6. ∀f:ℕ ⟶ T. ∃j:ℕ((¬((F f) j ∈ ℕ)) ∧ ((f (F f)) (f j) ∈ T))
7. : ℕ
8. ¬((F n.x)) j ∈ ℕ)
9. x ∈ T
10. j1 : ℕ
11. ¬((F n.x)) j1 ∈ ℕ)
12. if (j1 =z n.x)) then else fi  ∈ T
13. (F n.if (n =z n.x)) then else fi )) (F n.x)) ∈ ℤ
⊢ Dec(x y ∈ T)


Latex:


Latex:
.....truecase..... 
1.  [T]  :  Type
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}i,j:\mBbbN{}.  ((\mneg{}(i  =  j))  \mwedge{}  ((f  i)  =  (f  j)))
3.  x  :  T
4.  y  :  T
5.  F  :  f:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}j:\mBbbN{}.  ((\mneg{}((F  f)  =  j))  \mwedge{}  ((f  (F  f))  =  (f  j)))
7.  j  :  \mBbbN{}
8.  \mneg{}((F  (\mlambda{}n.x))  =  j)
9.  x  =  x
10.  j1  :  \mBbbN{}
11.  \mneg{}((F  (\mlambda{}n.if  (n  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi  ))  =  j1)
12.  y  =  if  (j1  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi 
13.  (F  (\mlambda{}n.if  (n  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi  ))  =  (F  (\mlambda{}n.x))
\mvdash{}  Dec(x  =  y)


By


Latex:
xxxHypSubst'  (-1)  (-3)xxx




Home Index