---

Step * 1 of Lemma es-pred_property_base


1. es : EO@i'
2. e : es-base-E(es)@i
⊢ (pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es))
BY
{ ((InstLemma `es-pred-wf-base` [⌈es⌉]⋅ THENA Auto) THEN (Decide ⌈pred(e) = e ∈ es-base-E(es)⌉⋅ THENA Auto)) }

1
1. es : EO@i'
2. e : es-base-E(es)@i
3. ∀[e:es-base-E(es)]. (pred(e) ∈ es-base-E(es))
4. pred(e) = e ∈ es-base-E(es)
⊢ (pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es))

2
1. es : EO@i'
2. e : es-base-E(es)@i
3. ∀[e:es-base-E(es)]. (pred(e) ∈ es-base-E(es))
4. ¬(pred(e) = e ∈ es-base-E(es))
⊢ (pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es))

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
\mvdash{}  (pred(e)  <  e)  \mvee{}  (pred(e)  =  e)


By

((InstLemma  `es-pred-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (Decide  \mkleeneopen{}pred(e)  =  e\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index