---

Step * 1 2 of Lemma subterm-cases


1. [opr] : Type
2. ∀x,y:term(opr).  (x << y ⇒ (x < y ∨ (∃z:term(opr). (x < z ∧ z << y))))
3. s : term(opr)
4. t : term(opr)
5. r : term(opr)
6. s < r
7. r << t
⊢ s << t
BY
{ ((Assert s << r BY EAuto 1) THEN FLemma `subterm_transitivity` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  \mforall{}x,y:term(opr).    (x  <<  y  {}\mRightarrow{}  (x  <  y  \mvee{}  (\mexists{}z:term(opr).  (x  <  z  \mwedge{}  z  <<  y))))
3.  s  :  term(opr)
4.  t  :  term(opr)
5.  r  :  term(opr)
6.  s  <  r
7.  r  <<  t
\mvdash{}  s  <<  t


By

---

Latex:
((Assert  s  <<  r  BY  EAuto  1)  THEN  FLemma  `subterm\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index