---

Step * 1 of Lemma firstn-before


∀the_es:EO. ∀e:E. ∀n:ℕ.  (n < ||before(e)|| ⇒ (firstn(n;before(e)) ~ before(before(e)[n])))
BY
{ ((D 0 THENA Auto)
   THEN CausalInd'
   THEN (UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN (Subst' before(e) ~ if first(e) then [] else before(pred(e)) @ [pred(e)] fi  0
         THENL [(RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Auto); OldAutoSplit]
   )
   THEN (D 0 THENA Auto)
   THEN (RWO "length-append" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (InstHyp [⌈pred(e)⌉] 3 ⋅ THENA Auto)
   THEN (RWO "firstn_append" 0 THENA Auto)) }

1
1. the_es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀n:ℕ. (n < ||before(e1)|| ⇒ (firstn(n;before(e1)) ~ before(before(e1)[n])))))
4. n : ℕ@i
5. ¬↑first(e)
6. n < ||before(pred(e))|| + 1@i
7. ∀n:ℕ. (n < ||before(pred(e))|| ⇒ (firstn(n;before(pred(e))) ~ before(before(pred(e))[n])))
⊢ firstn(n;before(pred(e))) ~ before(before(pred(e)) @ [pred(e)][n])

---

Latex:



\mforall{}the$_{es}$:EO.  \mforall{}e:E.  \mforall{}n:\mBbbN{}.    (n  <  ||before(e)||  {}\mRightarrow{}  (firstn(n;before(e))  \msim{}  before\000C(before(e)[n])))


By

((D  0  THENA  Auto)
  THEN  CausalInd'
  THEN  (UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (Subst'  before(e)  \msim{}  if  first(e)  then  []  else  before(pred(e))  @  [pred(e)]  fi    0
              THENL  [(RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Auto);  OldAutoSplit]
  )
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "length-append"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  3  \mcdot{}  THENA  Auto)
  THEN  (RWO  "firstn\_append"  0  THENA  Auto))

---

Home Index