---

Step * 1 1 of Lemma Escardo-Xu


1. M : F:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ
2. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀g:ℕ ⟶ ℕ.  ((∀i:ℕM F. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))
⊢ False
BY
{ ((GenConcl ⌜(M (λf.0)) = J ∈ ℕ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λg.(M (λf.(g (f J))))) = D ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(M D) = K ∈ ℕ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λf.if f J <z K then 0 else 1 fi ) = G ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λf.(f J)) = H ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λt,n,i. if i <z t then 0 else n fi ) = z ∈ (ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ)⌝⋅ THENA Auto)) }

1
1. M : F:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ
2. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀g:ℕ ⟶ ℕ.  ((∀i:ℕM F. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))
3. J : ℕ
4. (M (λf.0)) = J ∈ ℕ
5. D : (ℕ ⟶ ℕ) ⟶ ℕ
6. (λg.(M (λf.(g (f J))))) = D ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)
7. K : ℕ
8. (M D) = K ∈ ℕ
9. G : (ℕ ⟶ ℕ) ⟶ ℕ
10. (λf.if f J <z K then 0 else 1 fi ) = G ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)
11. H : (ℕ ⟶ ℕ) ⟶ ℕ
12. (λf.(f J)) = H ∈ ((ℕ ⟶ ℕ) ⟶ ℕ)
13. z : ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ
14. (λt,n,i. if i <z t then 0 else n fi ) = z ∈ (ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ)
⊢ False

---

Latex:

---

Latex:

1.  M  :  F:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
2.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((\mforall{}i:\mBbbN{}M  F.  ((g  i)  =  0))  {}\mRightarrow{}  ((F  (\mlambda{}i.0))  =  (F  g)))
\mvdash{}  False


By

---

Latex:
((GenConcl  \mkleeneopen{}(M  (\mlambda{}f.0))  =  J\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}g.(M  (\mlambda{}f.(g  (f  J)))))  =  D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(M  D)  =  K\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}f.if  f  J  <z  K  then  0  else  1  fi  )  =  G\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}f.(f  J))  =  H\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}t,n,i.  if  i  <z  t  then  0  else  n  fi  )  =  z\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index