---

Step * 1 1 1 2 of Lemma mrec-induction2


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>])
BY
{ (Assert mrec-spec(L;lbl;k)[j] ~ inl (inr y ) BY
         (DupHyp (-1)
          THEN MoveToConcl  (-1)
          THEN (GenConclTerm ⌜mrec-spec(L;lbl;k)[j]⌝⋅ THENA Auto)
          THEN D -2
          THEN Reduce 0
          THEN Auto)) }

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. y : Atom
10. mrec-spec(L;lbl;k)[j] = (inl (inr y )) ∈ (Atom + Atom + Type)
11. mrec-spec(L;lbl;k)[j] ~ inl (inr y )
⊢ (∀u∈t.j.P[<y, u>])

---

Latex:

---

Latex:

1.  L  :  MutualRectypeSpec
2.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  k  :  Atom
4.  [\%2]  :  (k  \mmember{}  eager-map(\mlambda{}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.  \mforall{}z:\{z:mobj(L)|  z  <  <k,  mk-prec(lbl;t)>\}  .  P[z]
8.  j  :  \mBbbN{}||mrec-spec(L;lbl;k)||
9.  y  :  Atom
10.  mrec-spec(L;lbl;k)[j]  =  (inl  (inr  y  ))
\mvdash{}  (\mforall{}u\mmember{}t.j.P[<y,  u>])


By

---

Latex:
(Assert  mrec-spec(L;lbl;k)[j]  \msim{}  inl  (inr  y  )  BY
              (DupHyp  (-1)
                THEN  MoveToConcl    (-1)
                THEN  (GenConclTerm  \mkleeneopen{}mrec-spec(L;lbl;k)[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  D  -2
                THEN  Reduce  0
                THEN  Auto))

---

Home Index