---

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

.....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
BY
{ (GenConclAtAddr [3;1] THEN D -2 THEN Reduce 0 THEN Auto) }

1
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
6. ≤loc(pred(e)) = [] ∈ ({a:E| loc(a) = loc(pred(e)) ∈ Id}  List)@i
⊢ e = hd([]) ∈ E

---

Latex:


.....subterm.....  T:t
2:n
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{}  hd(\mleq{}loc(pred(e))  @  [e])  =  hd(\mleq{}loc(pred(e)))


By

(GenConclAtAddr  [3;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index