---

Step * of Lemma es-locl-total2

∀es:EO. ∀e,e':E.  (e <loc e') ∨ (e' = e ∈ E) ∨ (e' <loc e) supposing loc(e) = loc(e') ∈ Id
BY
{ (Auto THEN (Inst_ES_Axiom [⌈e⌉; ⌈e'⌉] 3)⋅ THEN Auto THEN RepeatFor 2 (ParallelLast)) }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  <loc  e')  \mvee{}  (e'  =  e)  \mvee{}  (e'  <loc  e)  supposing  loc(e)  =  loc(e')


By

(Auto  THEN  (Inst\_ES\_Axiom  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  3)\mcdot{}  THEN  Auto  THEN  RepeatFor  2  (ParallelLast))

---

Home Index