---

Step * of Lemma es-before-pred-length

∀[es:EO]. ∀[e:E].  ||before(e)|| = (||before(pred(e))|| + 1) ∈ ℤ supposing ¬↑first(e)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN MoveToConcl (-1)
   THEN VrCausalInd'
   THEN Auto
   THEN RecUnfold `es-before` 0
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (RWO "length-append" 0 THENA Auto)
   THEN Reduce 0
   THEN Thin (-2)
   THEN Try (Complete ((RecUnfold `es-before` 0 THEN SplitOnConclITE THEN Reduce 0 THEN Auto)))
   THEN (InstHyp [⌈pred(e)⌉] (-3)⋅ THENA Auto)
   THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    ||before(e)||  =  (||before(pred(e))||  +  1)  supposing  \mneg{}\muparrow{}first(e)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  VrCausalInd'
  THEN  Auto
  THEN  RecUnfold  `es-before`  0
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "length-append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Thin  (-2)
  THEN  Try  (Complete  ((RecUnfold  `es-before`  0  THEN  SplitOnConclITE  THEN  Reduce  0  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Auto)

---

Home Index