---

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. x : T
4. y : T
5. F : f:(ℕ ⟶ T) ⟶ ℕ
6. ∀f:ℕ ⟶ T. ∃j:ℕ. ((¬((F f) = j ∈ ℕ)) ∧ ((f (F f)) = (f j) ∈ T))
7. j : ℕ
8. ¬((F (λn.x)) = j ∈ ℕ)
9. x = x ∈ T
10. j1 : ℕ
11. ¬((F (λn.if (n =z F (λn.x)) then y else x fi )) = j1 ∈ ℕ)
12. y = if (j1 =z F (λn.x)) then y else x fi  ∈ T
13. (F (λn.if (n =z F (λn.x)) then y else x 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. x : T
4. y : T
5. F : f:(ℕ ⟶ T) ⟶ ℕ
6. ∀f:ℕ ⟶ T. ∃j:ℕ. ((¬((F f) = j ∈ ℕ)) ∧ ((f (F f)) = (f j) ∈ T))
7. j : ℕ
8. ¬((F (λn.x)) = j ∈ ℕ)
9. x = x ∈ T
10. j1 : ℕ
11. ¬((F (λn.x)) = j1 ∈ ℕ)
12. y = if (j1 =z F (λn.x)) then y else x fi  ∈ T
13. (F (λn.if (n =z F (λn.x)) then y else x 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