---

Step * 1 1 of Lemma mrec-lt_wf

.....subterm..... T:t
1:n
1. L : MutualRectypeSpec
2. x : mobj(L)
3. y : mobj(L)
⊢ prec_sub+(Atom;lbl,p.mrec-spec(L;lbl;p)) ∈ (i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i))
  ⟶ (i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i))
  ⟶ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  L  :  MutualRectypeSpec
2.  x  :  mobj(L)
3.  y  :  mobj(L)
\mvdash{}  prec\_sub+(Atom;lbl,p.mrec-spec(L;lbl;p))  \mmember{}  (i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i))
    {}\mrightarrow{}  (i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i))
    {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index