---

Step * 1 1 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. s < t
⊢ s << t
BY
{ (BLemma `immediate-is-subterm` 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.  s  <  t
\mvdash{}  s  <<  t


By

---

Latex:
(BLemma  `immediate-is-subterm`  THEN  Auto)

---

Home Index