---

Step * 1 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))
6. ∀i,j:ℕ.  (¬↑(A2 i j))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[i] j)
BY
{ TACTIC:(Auto THEN (GenConclTerm ⌜coded-pair(n)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

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))
6.  \mforall{}i,j:\mBbbN{}.    (\mneg{}\muparrow{}(A2  i  j))
\mvdash{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  i,j  =  coded-pair(n)  in  A2[i]  j)


By

---

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

---

Home Index