---

Step * 1 of Lemma mrec-induction


1. [L] : MutualRectypeSpec
2. mobj(L) ⊆r (i:Atom × mrec(L;i))
3. (i:Atom × mrec(L;i)) ⊆r mobj(L)
4. [P] : mobj(L) ⟶ TYPE
5. ∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])
6. ∀i:Atom. ∀x:prec(lbl,p.mrec-spec(L;lbl;p);i).  (P[<i, x>] ∈ TYPE)
7. ∀i:Atom. ∀x:prec(lbl,p.mrec-spec(L;lbl;p);i).  P[<i, x>]
⊢ ∀x:mobj(L). P[x]
BY
{ ((D 0 THENA Auto) THEN D -1 THEN All (Fold `mrec`) THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  [L]  :  MutualRectypeSpec
2.  mobj(L)  \msubseteq{}r  (i:Atom  \mtimes{}  mrec(L;i))
3.  (i:Atom  \mtimes{}  mrec(L;i))  \msubseteq{}r  mobj(L)
4.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
5.  \mforall{}x:mobj(L).  ((\mforall{}z:\{z:mobj(L)|  z  <  x\}  .  P[z])  {}\mRightarrow{}  P[x])
6.  \mforall{}i:Atom.  \mforall{}x:prec(lbl,p.mrec-spec(L;lbl;p);i).    (P[<i,  x>]  \mmember{}  TYPE)
7.  \mforall{}i:Atom.  \mforall{}x:prec(lbl,p.mrec-spec(L;lbl;p);i).    P[<i,  x>]
\mvdash{}  \mforall{}x:mobj(L).  P[x]


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  All  (Fold  `mrec`)  THEN  BackThruSomeHyp)

---

Home Index