---

Step * 1 1 1 1 of Lemma Escardo-Xu


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 ∈ (ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ)
15. ∀g:ℕ ⟶ ℕ. ((∀i:ℕM D. ((g i) = 0 ∈ ℕ)) ⇒ ((D (λi.0)) = (D g) ∈ ℕ))
⊢ False
BY
{ (HypSubst' 8 (-1) THEN (Subst' D (λi.0) ~ J -1 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 ∈ (ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ)
15. ∀g:ℕ ⟶ ℕ. ((∀i:ℕK. ((g i) = 0 ∈ ℕ)) ⇒ ((D (λi.0)) = (D g) ∈ ℕ))
⊢ (D (λi.0)) = J ∈ ℕ

2
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 ∈ (ℕ ⟶ ℕ ⟶ ℕ ⟶ ℕ)
15. ∀g:ℕ ⟶ ℕ. ((∀i:ℕK. ((g i) = 0 ∈ ℕ)) ⇒ (J = (D g) ∈ ℕ))
⊢ 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)))
3.  J  :  \mBbbN{}
4.  (M  (\mlambda{}f.0))  =  J
5.  D  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
6.  (\mlambda{}g.(M  (\mlambda{}f.(g  (f  J)))))  =  D
7.  K  :  \mBbbN{}
8.  (M  D)  =  K
9.  G  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
10.  (\mlambda{}f.if  f  J  <z  K  then  0  else  1  fi  )  =  G
11.  H  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
12.  (\mlambda{}f.(f  J))  =  H
13.  z  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
14.  (\mlambda{}t,n,i.  if  i  <z  t  then  0  else  n  fi  )  =  z
15.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}i:\mBbbN{}M  D.  ((g  i)  =  0))  {}\mRightarrow{}  ((D  (\mlambda{}i.0))  =  (D  g)))
\mvdash{}  False


By

---

Latex:
(HypSubst'  8  (-1)  THEN  (Subst'  D  (\mlambda{}i.0)  \msim{}  J  -1  THENA  Auto))

---

Home Index