Step
*
2
of Lemma
sp-meet_wf
1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (f1 = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g : Base
9. g1 : Base
10. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
11. g ∈ ℕ ⟶ 𝔹
12. g1 ∈ ℕ ⟶ 𝔹
13. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f1 x) ∧b (g1 y))
16. i : ℕ
17. j : ℕ
18. ↑((f i) ∧b (g j))
⊢ False
BY
{ Assert ⌜(¬(g1 = ⊥ ∈ (ℕ ⟶ 𝔹))) ∧ (¬(f1 = ⊥ ∈ (ℕ ⟶ 𝔹)))⌝⋅ }
1
.....assertion..... 
1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (f1 = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g : Base
9. g1 : Base
10. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
11. g ∈ ℕ ⟶ 𝔹
12. g1 ∈ ℕ ⟶ 𝔹
13. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f1 x) ∧b (g1 y))
16. i : ℕ
17. j : ℕ
18. ↑((f i) ∧b (g j))
⊢ (¬(g1 = ⊥ ∈ (ℕ ⟶ 𝔹))) ∧ (¬(f1 = ⊥ ∈ (ℕ ⟶ 𝔹)))
2
1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (f1 = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g : Base
9. g1 : Base
10. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) 
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
11. g ∈ ℕ ⟶ 𝔹
12. g1 ∈ ℕ ⟶ 𝔹
13. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) 
⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f1 x) ∧b (g1 y))
16. i : ℕ
17. j : ℕ
18. ↑((f i) ∧b (g j))
19. (¬(g1 = ⊥ ∈ (ℕ ⟶ 𝔹))) ∧ (¬(f1 = ⊥ ∈ (ℕ ⟶ 𝔹)))
⊢ False
Latex:
Latex:
1.  f  :  Base
2.  f1  :  Base
3.  f  =  f1
4.  f  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
5.  f1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  (f  =  \mbot{})  {}\mRightarrow{}  (f1  =  \mbot{})
7.  (f  =  \mbot{})  \mLeftarrow{}{}  f1  =  \mbot{}
8.  g  :  Base
9.  g1  :  Base
10.  g  =  g1
11.  g  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
12.  g1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
13.  (g  =  \mbot{})  {}\mRightarrow{}  (g1  =  \mbot{})
14.  (g  =  \mbot{})  \mLeftarrow{}{}  g1  =  \mbot{}
15.  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  x,y  =  coded-pair(n)  in  (f1  x)  \mwedge{}\msubb{}  (g1  y))
16.  i  :  \mBbbN{}
17.  j  :  \mBbbN{}
18.  \muparrow{}((f  i)  \mwedge{}\msubb{}  (g  j))
\mvdash{}  False
By
Latex:
Assert  \mkleeneopen{}(\mneg{}(g1  =  \mbot{}))  \mwedge{}  (\mneg{}(f1  =  \mbot{}))\mkleeneclose{}\mcdot{}
Home
Index