---

Step * 2 1 1 1 1 1 1 1 of Lemma KleeneSearch_wf


1. a2 : ℕ
2. a3 : ℕ
3. v1 : ℕ ⋃ (ℕ × ℕ)
4. v1 = <a2, a3> ∈ (ℕ ⋃ (ℕ × ℕ))
5. x : v1 is an integer
6. v1 is an integer = False ∈ ℙ
⊢ x ∈ False
BY
{ (SubsumeC  ⌜v1 is an integer⌝⋅ THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(SubsumeC    \mkleeneopen{}v1  is  an  integer\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index