---

Step * 2 1 1 1 1 of Lemma KleeneSearch_wf


1. a2 : ℕ
2. a3 : ℕ
3. v1 : ℕ ⋃ (ℕ × ℕ)
4. v1 = <a2, a3> ∈ (ℕ ⋃ (ℕ × ℕ))
5. v1 is an integer
⊢ False
BY
{ (ApFunToHypEquands `Z' ⌜Z is an integer⌝ ⌜ℙ⌝ (-2)⋅ THENA Auto) }

1
1. a2 : ℕ
2. a3 : ℕ
3. v1 : ℕ ⋃ (ℕ × ℕ)
4. v1 = <a2, a3> ∈ (ℕ ⋃ (ℕ × ℕ))
5. v1 is an integer
6. v1 is an integer = <a2, a3> is an integer ∈ ℙ
⊢ False

---

Latex:

---

Latex:

1.  a2  :  \mBbbN{}
2.  a3  :  \mBbbN{}
3.  v1  :  \mBbbN{}  \mcup{}  (\mBbbN{}  \mtimes{}  \mBbbN{})
4.  v1  =  <a2,  a3>
5.  v1  is  an  integer
\mvdash{}  False


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}Z  is  an  integer\mkleeneclose{}  \mkleeneopen{}\mBbbP{}\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)

---

Home Index