Step
*
of Lemma
es-le-antisymmetric
∀[es:EO]. ∀[e,e':E]. (e = e' ∈ E) supposing (e' ≤loc e and e ≤loc e' )
BY
{ (Auto
THEN AssertBY ⌈(e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e)⌉
(((InstESAxiom ⌈es⌉ [⌈e⌉; ⌈e'⌉] 3)⋅ THENA Auto) THEN (BHyp (-1)) THEN Auto)⋅
THEN SplitOrHyps
THEN Auto
THEN (InstLemma `es-le-not-locl` [⌈es⌉; ⌈e⌉; ⌈e'⌉])⋅
THEN Auto
THEN (InstLemma `es-le-not-locl` [⌈es⌉; ⌈e'⌉; ⌈e⌉])⋅
THEN Auto
THEN ThinTrivial
THEN Auto) }
Latex:
\mforall{}[es:EO]. \mforall{}[e,e':E]. (e = e') supposing (e' \mleq{}loc e and e \mleq{}loc e' )
By
(Auto
THEN AssertBY \mkleeneopen{}(e <loc e') \mvee{} (e = e') \mvee{} (e' <loc e)\mkleeneclose{}
(((InstESAxiom \mkleeneopen{}es\mkleeneclose{} [\mkleeneopen{}e\mkleeneclose{}; \mkleeneopen{}e'\mkleeneclose{}] 3)\mcdot{} THENA Auto) THEN (BHyp (-1)) THEN Auto)\mcdot{}
THEN SplitOrHyps
THEN Auto
THEN (InstLemma `es-le-not-locl` [\mkleeneopen{}es\mkleeneclose{}; \mkleeneopen{}e\mkleeneclose{}; \mkleeneopen{}e'\mkleeneclose{}])\mcdot{}
THEN Auto
THEN (InstLemma `es-le-not-locl` [\mkleeneopen{}es\mkleeneclose{}; \mkleeneopen{}e'\mkleeneclose{}; \mkleeneopen{}e\mkleeneclose{}])\mcdot{}
THEN Auto
THEN ThinTrivial
THEN Auto)
Home
Index