---

Step * 1 1 of Lemma sp-lub_wf1


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

1
1. A1 : ℕ ⟶ ℕ ⟶ 𝔹@i
2. A2 : ℕ ⟶ ℕ ⟶ 𝔹@i
3. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A1[i] j)
4. ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n)))
5. ∀i,j:ℕ.  (¬↑(A1 i j))
6. ∀i,j:ℕ.  (¬↑(A2 i j))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[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  A1[i]  j)
4.  \mforall{}x:\mBbbN{}.  (\mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A1  x  n))  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A2  x  n)))
5.  \mforall{}i,j:\mBbbN{}.    (\mneg{}\muparrow{}(A1  i  j))
\mvdash{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  i,j  =  coded-pair(n)  in  A2[i]  j)


By

---

Latex:
TACTIC:(Assert  \mforall{}i,j:\mBbbN{}.    (\mneg{}\muparrow{}(A2  i  j))  BY
                            (ParallelOp  -2  THEN  Auto))

---

Home Index