---

Step * 2 of Lemma sp-lub_wf1


1. A1 : ℕ ⟶ ℕ ⟶ 𝔹@i
2. A2 : ℕ ⟶ ℕ ⟶ 𝔹@i
3. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[i] j)
4. ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n)))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A1[i] j)
BY
{ TACTIC:(Assert ∀i,j:ℕ.  (¬↑(A2 i j)) BY
                (Auto
                 THEN (InstHyp [⌜code-pair(i;j)⌝] 3⋅ THENA Auto)
                 THEN (RWO "coded-code-pair" (-1) THENM Reduce (-1))
                 THEN Auto)) }

1
1. A1 : ℕ ⟶ ℕ ⟶ 𝔹@i
2. A2 : ℕ ⟶ ℕ ⟶ 𝔹@i
3. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[i] j)
4. ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n)))
5. ∀i,j:ℕ.  (¬↑(A2 i j))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A1[i] j)

---

Latex:

---

Latex:

1.  A1  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
2.  A2  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
3.  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  i,j  =  coded-pair(n)  in  A2[i]  j)
4.  \mforall{}x:\mBbbN{}.  (\mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A1  x  n))  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A2  x  n)))
\mvdash{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  i,j  =  coded-pair(n)  in  A1[i]  j)


By

---

Latex:
TACTIC:(Assert  \mforall{}i,j:\mBbbN{}.    (\mneg{}\muparrow{}(A2  i  j))  BY
                            (Auto
                              THEN  (InstHyp  [\mkleeneopen{}code-pair(i;j)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
                              THEN  (RWO  "coded-code-pair"  (-1)  THENM  Reduce  (-1))
                              THEN  Auto))

---

Home Index