---

Step * 1 1 1 1 of Lemma stdEO-le


1. v : ℙ@i'
2. v1 : ℙ@i'
3. v2 : Id@i
4. v3 : Id@i
5. v4 : ℕ@i
6. v5 : ℕ@i
7. v ⇒ ((v2 = v3 ∈ Id) ∧ v4 < v5)@i
8. v ⇐ (v2 = v3 ∈ Id) ∧ v4 < v5@i
9. v1 ⇒ ((v2 = v3 ∈ Id) ∧ (v4 = v5 ∈ ℤ))@i
10. v1 ⇐ (v2 = v3 ∈ Id) ∧ (v4 = v5 ∈ ℤ)@i
11. v2 = v3 ∈ Id@i
12. v4 ≤ v5@i
⊢ v ∨ v1
BY
{ (Decide ⌈v4 = v5 ∈ ℤ⌉⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbP{}@i'
2.  v1  :  \mBbbP{}@i'
3.  v2  :  Id@i
4.  v3  :  Id@i
5.  v4  :  \mBbbN{}@i
6.  v5  :  \mBbbN{}@i
7.  v  {}\mRightarrow{}  ((v2  =  v3)  \mwedge{}  v4  <  v5)@i
8.  v  \mLeftarrow{}{}  (v2  =  v3)  \mwedge{}  v4  <  v5@i
9.  v1  {}\mRightarrow{}  ((v2  =  v3)  \mwedge{}  (v4  =  v5))@i
10.  v1  \mLeftarrow{}{}  (v2  =  v3)  \mwedge{}  (v4  =  v5)@i
11.  v2  =  v3@i
12.  v4  \mleq{}  v5@i
\mvdash{}  v  \mvee{}  v1


By

---

Latex:
(Decide  \mkleeneopen{}v4  =  v5\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index