---

Step * of Lemma es-pred-one-one

∀[es:EO]. ∀[a,b:E].  (a = b ∈ E) supposing ((pred(a) = pred(b) ∈ E) and (¬↑first(b)) and (¬↑first(a)))
BY
{ (((((Auto
       THEN AssertBY ⌜(a <loc b) ∨ (a = b ∈ E) ∨ (b <loc a)⌝
          (((InstESAxiom ⌜es⌝ [⌜a⌝; ⌜b⌝] 3)⋅ THENA Auto)
           THEN (BHyp (-1))
           THEN Auto
           THEN RWO "es-loc-pred<" 0
           THEN Auto
           THEN EqCD
           THEN Auto)⋅
       THEN SplitOrHyps
       THEN Auto
       THEN (RWO "es-le-pred<" (-1)))
      THENA Auto
      )
     THENL [(RevHypSubst (-2) (-1)); (HypSubst (-2) (-1))]
    )
    THENA Auto
    )
   THEN (RWO "es-le-pred" (-1))
   THEN Auto
   THEN (InstLemma `es-locl-antireflexive` [⌜es⌝; ⌜a⌝])⋅
   THEN Auto
   THEN (InstLemma `es-locl-antireflexive` [⌜es⌝; ⌜b⌝])⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[a,b:E].    (a  =  b)  supposing  ((pred(a)  =  pred(b))  and  (\mneg{}\muparrow{}first(b))  and  (\mneg{}\muparrow{}first(a)))


By

---

Latex:
(((((Auto
          THEN  AssertBY  \mkleeneopen{}(a  <loc  b)  \mvee{}  (a  =  b)  \mvee{}  (b  <loc  a)\mkleeneclose{}
                (((InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  [\mkleeneopen{}a\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}]  3)\mcdot{}  THENA  Auto)
                  THEN  (BHyp  (-1))
                  THEN  Auto
                  THEN  RWO  "es-loc-pred<"  0
                  THEN  Auto
                  THEN  EqCD
                  THEN  Auto)\mcdot{}
          THEN  SplitOrHyps
          THEN  Auto
          THEN  (RWO  "es-le-pred<"  (-1)))
        THENA  Auto
        )
      THENL  [(RevHypSubst  (-2)  (-1));  (HypSubst  (-2)  (-1))]
    )
    THENA  Auto
    )
  THEN  (RWO  "es-le-pred"  (-1))
  THEN  Auto
  THEN  (InstLemma  `es-locl-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `es-locl-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}
  THEN  Auto)

---

Home Index