---

Step * of Lemma mrec-lt_transitivity

∀[L:MutualRectypeSpec]. ∀[x,y,z:mobj(L)].  (x < y ⇒ y < z ⇒ x < z)
BY
{ (Auto THEN All (RepUR ``mrec-lt prec-sub+ prec_sub+``)) }

1
1. [L] : MutualRectypeSpec
2. [x] : mobj(L)
3. [y] : mobj(L)
4. [z] : mobj(L)
5. prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p))+ x y
6. prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p))+ y z
⊢ prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p))+ x z

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[x,y,z:mobj(L)].    (x  <  y  {}\mRightarrow{}  y  <  z  {}\mRightarrow{}  x  <  z)


By

---

Latex:
(Auto  THEN  All  (RepUR  ``mrec-lt  prec-sub+  prec\_sub+``))

---

Home Index