---

Step * 2 1 of Lemma sp-meet-is-top


1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
5. x ∈ ℕ ⟶ 𝔹
6. x1 ∈ ℕ ⟶ 𝔹
7. (x = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (x1 = ⊥ ∈ (ℕ ⟶ 𝔹))
8. (x = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
12. y ∈ ℕ ⟶ 𝔹
13. y1 ∈ ℕ ⟶ 𝔹
14. (y = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. (λn.let x@0,y@0 = coded-pair(n) 
        in (x x@0) ∧b (y y@0))
= ⊤
∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
16. λn.let x@0,y@0 = coded-pair(n) 
       in (x x@0) ∧b (y y@0) ∈ ℕ ⟶ 𝔹
17. ⊤ ∈ ℕ ⟶ 𝔹
18. ((λn.let x@0,y@0 = coded-pair(n) in (x x@0) ∧b (y y@0)) = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (⊤ = ⊥ ∈ (ℕ ⟶ 𝔹))
19. ((λn.let x@0,y@0 = coded-pair(n) in (x x@0) ∧b (y y@0)) = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ ⊤ = ⊥ ∈ (ℕ ⟶ 𝔹)
20. y = ⊥ ∈ (ℕ ⟶ 𝔹)
21. y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
22. x2 : ℕ
⊢ let x@0,y@0 = coded-pair(x2) in (x x@0) ∧b ff = ff
BY
{ TACTIC:((GenConclTerm ⌜coded-pair(x2)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  (\mbot{}  =  \mtop{})  {}\mRightarrow{}  False
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  x1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
7.  (x  =  \mbot{})  {}\mRightarrow{}  (x1  =  \mbot{})
8.  (x  =  \mbot{})  \mLeftarrow{}{}  x1  =  \mbot{}
9.  y  :  Base
10.  y1  :  Base
11.  y  =  y1
12.  y  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
13.  y1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
14.  (y  =  \mbot{})  \mLeftarrow{}{}  y1  =  \mbot{}
15.  (\mlambda{}n.let  x@0,y@0  =  coded-pair(n)  in  (x  x@0)  \mwedge{}\msubb{}  (y  y@0))  =  \mtop{}
16.  \mlambda{}n.let  x@0,y@0  =  coded-pair(n) 
              in  (x  x@0)  \mwedge{}\msubb{}  (y  y@0)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
17.  \mtop{}  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
18.  ((\mlambda{}n.let  x@0,y@0  =  coded-pair(n)  in  (x  x@0)  \mwedge{}\msubb{}  (y  y@0))  =  \mbot{})  {}\mRightarrow{}  (\mtop{}  =  \mbot{})
19.  ((\mlambda{}n.let  x@0,y@0  =  coded-pair(n)  in  (x  x@0)  \mwedge{}\msubb{}  (y  y@0))  =  \mbot{})  \mLeftarrow{}{}  \mtop{}  =  \mbot{}
20.  y  =  \mbot{}
21.  y1  =  \mbot{}
22.  x2  :  \mBbbN{}
\mvdash{}  let  x@0,y@0  =  coded-pair(x2)  in  (x  x@0)  \mwedge{}\msubb{}  ff  =  ff


By

---

Latex:
TACTIC:((GenConclTerm  \mkleeneopen{}coded-pair(x2)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index