---

Step * 1 of Lemma implies-mrec-lt


1. [L] : MutualRectypeSpec
2. mobj(L) ⊆r (i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i))
3. (i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i)) ⊆r mobj(L)
4. [x] : mobj(L)
5. y : mobj(L)
6. prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p)) x y
⊢ prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p))+ x y
BY
{ (BLemma  `implies-rel_plus` THEN Try (Complete (Auto)) THEN SubsumeC ⌜mobj(L)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [L]  :  MutualRectypeSpec
2.  mobj(L)  \msubseteq{}r  (i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i))
3.  (i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i))  \msubseteq{}r  mobj(L)
4.  [x]  :  mobj(L)
5.  y  :  mobj(L)
6.  prec\_sub(Atom;lbl,p.mrec-spec(L;lbl;p))  x  y
\mvdash{}  prec\_sub(Atom;lbl,p.mrec-spec(L;lbl;p))\msupplus{}  x  y


By

---

Latex:
(BLemma    `implies-rel\_plus`  THEN  Try  (Complete  (Auto))  THEN  SubsumeC  \mkleeneopen{}mobj(L)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index