---

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


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. if (F (λn.if (n =z F (λn.x)) then y else x fi ) =z F (λn.x)) then y else x fi 
= if (j1 =z F (λn.x)) then y else x fi 
∈ T
⊢ Dec(x = y ∈ T)
BY
{ xxx(SplitOnHypITE -1  THENA Auto)xxx }

1
.....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)

2
.....falsecase..... 
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. x = 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:

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.  if  (F  (\mlambda{}n.if  (n  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi  )  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi 
=  if  (j1  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi 
\mvdash{}  Dec(x  =  y)


By

---

Latex:
xxx(SplitOnHypITE  -1    THENA  Auto)xxx

---

Home Index