---

Step * 1 of Lemma hd-es-le-before-is-first


1. es : EO
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ first(hd(≤loc(e1))) = tt)
4. ¬↑first(e)
5. first(hd(≤loc(pred(e)))) = tt
⊢ first(hd(≤loc(pred(e)) @ [e])) = tt
BY
{ (NthHypEq (-1) THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
2:n
1. es : EO
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ first(hd(≤loc(e1))) = tt)
4. ¬↑first(e)
5. first(hd(≤loc(pred(e)))) = tt
⊢ hd(≤loc(pred(e)) @ [e]) = hd(≤loc(pred(e))) ∈ E

---

Latex:



1.  es  :  EO
2.  e  :  E@i
3.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  first(hd(\mleq{}loc(e1)))  =  tt)
4.  \mneg{}\muparrow{}first(e)
5.  first(hd(\mleq{}loc(pred(e))))  =  tt
\mvdash{}  first(hd(\mleq{}loc(pred(e))  @  [e]))  =  tt


By

(NthHypEq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index