---

Step * 2 1 1 1 1 1 of Lemma KleeneSearch_wf


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
BY
{ Reduce -1 }

1
1. a2 : ℕ
2. a3 : ℕ
3. v1 : ℕ ⋃ (ℕ × ℕ)
4. v1 = <a2, a3> ∈ (ℕ ⋃ (ℕ × ℕ))
5. v1 is an integer
6. v1 is an integer = False ∈ ℙ
⊢ 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
6.  v1  is  an  integer  =  <a2,  a3>  is  an  integer
\mvdash{}  False


By

---

Latex:
Reduce  -1

---

Home Index