---

Step * 2 1 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 = False ∈ ℙ
⊢ False
BY
{ (RenameVar `x' (-2) THEN UseWitness ⌜x⌝⋅) }

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


By

---

Latex:
(RenameVar  `x'  (-2)  THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index