---

Step * of Lemma es-loc-pred-plus

∀[es:EO]. ∀[x,y:E].  loc(x) = loc(y) ∈ Id supposing x λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))+ y
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``infix_ap rel_plus`` 0
   THEN (Assert ⌈∀n:ℕ. ∀x,y:E.  ((λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))^n x y) ⇒ (loc(x) = loc(y) ∈ Id))⌉ BY
               (CompleteInductionOnNat
                THEN RepeatFor 2 ((D 0 THENA Auto))
                THEN RecUnfold `rel_exp` 0
                THEN Reduce 0
                THEN AutoSplit
                THEN Auto
                THEN ExRepD
                THEN FHyp 3 [-1]
                THEN Auto
                THEN RWO "-3 -1<" 0
                THEN Auto))) }

1
1. es : EO
2. ∀n:ℕ. ∀x,y:E.  ((λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))^n x y) ⇒ (loc(x) = loc(y) ∈ Id))
⊢ ∀[x,y:E].  loc(x) = loc(y) ∈ Id supposing ∃n:ℕ+. (λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))^n x y)

---

Latex:


\mforall{}[es:EO].  \mforall{}[x,y:E].    loc(x)  =  loc(y)  supposing  x  \mlambda{}x,y.  ((\mneg{}\muparrow{}first(y))  c\mwedge{}  (x  =  pred(y)))\msupplus{}  y


By

((D  0  THENA  Auto)
  THEN  RepUR  ``infix\_ap  rel\_plus``  0
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x,y:E.    ((\mlambda{}x,y.  ((\mneg{}\muparrow{}first(y))  c\mwedge{}  (x  =  pred(y)))\^{}n  x  y)  {}\mRightarrow{}  (loc(x)  =  loc(y)))\mkleeneclose{}  \000CBY
                          (CompleteInductionOnNat
                            THEN  RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  RecUnfold  `rel\_exp`  0
                            THEN  Reduce  0
                            THEN  AutoSplit
                            THEN  Auto
                            THEN  ExRepD
                            THEN  FHyp  3  [-1]
                            THEN  Auto
                            THEN  RWO  "-3  -1<"  0
                            THEN  Auto)))

---

Home Index