---

Step * of Lemma mrec-ind_wf

∀[L:MutualRectypeSpec]. ∀[A:mobj(L) ⟶ TYPE]. ∀[h:x:mobj(L) ⟶ (z:{z:mobj(L)| z < x}  ⟶ A[z]) ⟶ A[x]]. ∀[o:mobj(L)].
  (mrec-ind(h;o) ∈ A[o])
BY
{ (Auto
   THEN (Subst' mrec-ind(h;o) ~ TERMOF{mrec-induction:o, \\v:l, i:l} h o 0
         THENA (Computation
                THEN EqCD
                THEN Try (Trivial)
                THEN (Reduce 0 THEN RW (AddrC [2] (TagC (mk_tag_term 1))) 0 THEN Reduce 0)
                THEN Auto)
         )
   THEN Fold `implies` (-2)
   THEN Fold `all` (-2)
   THEN GenConclAtAddrType  (∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . A[z]) ⇒ A[x])) ⇒ (∀x:mobj(L). A[x]) [2;1;1]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[A:mobj(L)  {}\mrightarrow{}  TYPE].  \mforall{}[h:x:mobj(L)  {}\mrightarrow{}  (z:\{z:mobj(L)|  z  <  x\}    {}\mrightarrow{}  A[z])  {}\mrightarrow{}  A[\000Cx]].
\mforall{}[o:mobj(L)].
    (mrec-ind(h;o)  \mmember{}  A[o])


By

---

Latex:
(Auto
  THEN  (Subst'  mrec-ind(h;o)  \msim{}  TERMOF\{mrec-induction:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  h  o  0
              THENA  (Computation
                            THEN  EqCD
                            THEN  Try  (Trivial)
                            THEN  (Reduce  0  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  0  THEN  Reduce  0)
                            THEN  Auto)
              )
  THEN  Fold  `implies`  (-2)
  THEN  Fold  `all`  (-2)
  THEN  GenConclAtAddrType    (\mforall{}x:mobj(L).  ((\mforall{}z:\{z:mobj(L)|  z  <  x\}  .  A[z])  {}\mRightarrow{}  A[x]))
  {}\mRightarrow{}  (\mforall{}x:mobj(L).  A[x])  [2;1;1]\mcdot{}
  THEN  Auto)

---

Home Index