---

Step * 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)) x ∈ (i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i)) ⟶ ℙ
BY
{ MemCD }

1
.....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))
  ⟶ ℙ

2
.....subterm..... T:t
2:n
1. L : MutualRectypeSpec
2. x : mobj(L)
3. y : mobj(L)
⊢ x ∈ i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i)

---

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))  x  \mmember{}  (i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i))  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
MemCD

---

Home Index