---

Step * of Lemma mrec-induction

∀[L:MutualRectypeSpec]. ∀[P:mobj(L) ⟶ TYPE].
  ((∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])) ⇒ (∀x:mobj(L). P[x]))
BY
{ (InstLemma `mobj-ext` []
   THEN ParallelLast'
   THEN D -1
   THEN (RepeatFor 2 ((D 0 THENA Auto))
         THEN (Assert ∀i:Atom. ∀x:prec(lbl,p.mrec-spec(L;lbl;p);i).  (P[<i, x>] ∈ TYPE) BY
                     (Fold `mrec` 0
                      THEN RepeatFor 2 ((D 0 THENA Auto))
                      THEN MemCD
                      THEN Try (Trivial)
                      THEN SubsumeC  ⌜i:Atom × mrec(L;i)⌝⋅
                      THEN Auto))
         )
   THEN ((InstLemma `prec-induction-ext` [⌜Atom⌝;⌜λ2lbl p.mrec-spec(L;lbl;p)⌝;⌜λ2i x.P[<i, x>]⌝]⋅ THENW Auto)
         THENA (Intros
                THEN (BHyp 5 THENW (SubsumeC ⌜i:Atom × mrec(L;i)⌝⋅ THEN Auto))
                THEN (Assert <i, x> ∈ mobj(L) BY
                            (SubsumeC ⌜i:Atom × mrec(L;i)⌝⋅ THEN Auto))
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN D -2
                THEN BHyp 9
                THEN Try ((Fold `mrec-lt` 0 THEN Fold `mrec` 0))
                THEN Auto)
         )) }

1
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]

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[P:mobj(L)  {}\mrightarrow{}  TYPE].
    ((\mforall{}x:mobj(L).  ((\mforall{}z:\{z:mobj(L)|  z  <  x\}  .  P[z])  {}\mRightarrow{}  P[x]))  {}\mRightarrow{}  (\mforall{}x:mobj(L).  P[x]))


By

---

Latex:
(InstLemma  `mobj-ext`  []
  THEN  ParallelLast'
  THEN  D  -1
  THEN  (RepeatFor  2  ((D  0  THENA  Auto))
              THEN  (Assert  \mforall{}i:Atom.  \mforall{}x:prec(lbl,p.mrec-spec(L;lbl;p);i).    (P[<i,  x>]  \mmember{}  TYPE)  BY
                                      (Fold  `mrec`  0
                                        THEN  RepeatFor  2  ((D  0  THENA  Auto))
                                        THEN  MemCD
                                        THEN  Try  (Trivial)
                                        THEN  SubsumeC    \mkleeneopen{}i:Atom  \mtimes{}  mrec(L;i)\mkleeneclose{}\mcdot{}
                                        THEN  Auto))
              )
  THEN  ((InstLemma  `prec-induction-ext`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}lbl  p.mrec-spec(L;lbl;p)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i  x.P[<i,  x>]\mkleeneclose{}]\mcdot{}  THEN\000CW  Auto)
              THENA  (Intros
                            THEN  (BHyp  5  THENW  (SubsumeC  \mkleeneopen{}i:Atom  \mtimes{}  mrec(L;i)\mkleeneclose{}\mcdot{}  THEN  Auto))
                            THEN  (Assert  <i,  x>  \mmember{}  mobj(L)  BY
                                                    (SubsumeC  \mkleeneopen{}i:Atom  \mtimes{}  mrec(L;i)\mkleeneclose{}\mcdot{}  THEN  Auto))
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  D  -2
                            THEN  BHyp  9
                            THEN  Try  ((Fold  `mrec-lt`  0  THEN  Fold  `mrec`  0))
                            THEN  Auto)
              ))

---

Home Index