---

Step * 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
⊢ Dec(x = y ∈ T)
BY
{ xxx((InstHyp [⌜λn.if (n =z F (λn.x)) then y else x fi ⌝] (-4)⋅ THENA Auto) THEN Reduce (-1) THEN ExRepD)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.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)

---

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
\mvdash{}  Dec(x  =  y)


By

---

Latex:
xxx((InstHyp  [\mkleeneopen{}\mlambda{}n.if  (n  =\msubz{}  F  (\mlambda{}n.x))  then  y  else  x  fi  \mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  ExRepD)xxx

---

Home Index