---

Step * 1 1 1 of Lemma mrec-induction2

.....assertion..... 
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} . ∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl))\000C.
    ((∀z:{z:mobj(L)| z < <k, mk-prec(lbl;t)>} . P[z]) ⇒ P[<k, mk-prec(lbl;t)>])
BY
{ (UnfoldTopAb (-1)
   THEN RepeatFor 2 (ParallelLast')
   THEN DVar `k'
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN (D -2 THENM Auto)
   THEN (D 0 THENA Auto)
   THEN (GenConclTerm ⌜mrec-spec(L;lbl;k)[j]⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Try (TrueCD)
   THEN D -2
   THEN Reduce 0) }

1
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. k : Atom
4. [%2] : (k ∈ eager-map(λp.(fst(p));L))
5. lbl : {lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} 
6. t : tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl))
7. ∀z:{z:mobj(L)| z < <k, mk-prec(lbl;t)>} . P[z]
8. j : ℕ||mrec-spec(L;lbl;k)||
9. x1 : Atom
10. mrec-spec(L;lbl;k)[j] = (inl inl x1) ∈ (Atom + Atom + Type)
⊢ P[<x1, t.j>]

2
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. k : Atom
4. [%2] : (k ∈ eager-map(λp.(fst(p));L))
5. lbl : {lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} 
6. t : tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl))
7. ∀z:{z:mobj(L)| z < <k, mk-prec(lbl;t)>} . P[z]
8. j : ℕ||mrec-spec(L;lbl;k)||
9. y : Atom
10. mrec-spec(L;lbl;k)[j] = (inl (inr y )) ∈ (Atom + Atom + Type)
⊢ (∀u∈t.j.P[<y, u>])

---

Latex:

---

Latex:
.....assertion..... 
1.  L  :  MutualRectypeSpec
2.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  mrecind(L;x.P[x])
\mvdash{}  \mforall{}k:mKinds.  \mforall{}lbl:\{lbl:Atom|  0  <  ||mrec-spec(L;lbl;k)||\}  .
    \mforall{}t:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl)).
        ((\mforall{}z:\{z:mobj(L)|  z  <  <k,  mk-prec(lbl;t)>\}  .  P[z])  {}\mRightarrow{}  P[<k,  mk-prec(lbl;t)>])


By

---

Latex:
(UnfoldTopAb  (-1)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  DVar  `k'
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENM  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}mrec-spec(L;lbl;k)[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  (TrueCD)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index