---

Step * 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 ∨ (∃r:term(opr). (s < r ∧ r << t))
⊢ s << t
BY
{ (D -1 THEN ExRepD) }

1
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

2
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

---

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  \mvee{}  (\mexists{}r:term(opr).  (s  <  r  \mwedge{}  r  <<  t))
\mvdash{}  s  <<  t


By

---

Latex:
(D  -1  THEN  ExRepD)

---

Home Index