---

Step * 1 of Lemma mrec-lt_transitivity


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
BY
{ (((InstLemma `mobj-ext` [⌜L⌝]⋅ THENA Auto) THEN D -1)
   THEN FLemma `rel_plus_transitivity` [-3;-4]
   THEN Fold `mrec` 0
   THEN Auto) }

---

Latex:

---

Latex:

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))\msupplus{}  x  y
6.  prec\_sub(Atom;lbl,p.mrec-spec(L;lbl;p))\msupplus{}  y  z
\mvdash{}  prec\_sub(Atom;lbl,p.mrec-spec(L;lbl;p))\msupplus{}  x  z


By

---

Latex:
(((InstLemma  `mobj-ext`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
  THEN  FLemma  `rel\_plus\_transitivity`  [-3;-4]
  THEN  Fold  `mrec`  0
  THEN  Auto)

---

Home Index