---

Step * 1 1 1 1 1 1 of Lemma mrec-induction2


1. L : MutualRectypeSpec
2. P : mobj(L) ⟶ TYPE
3. k : Atom
4. (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)
11. mrec-spec(L;lbl;k)[j] ~ inl inl x1
⊢ <x1, t.j> ∈ {z:mobj(L)| z < <k, mk-prec(lbl;t)>} 
BY
{ (Assert t.j ∈ mrec(L;x1) BY
         (InferEqualType
          THENL [(RepUR ``prec-arg-types`` 0
                  THEN (RWO "select-map" 0 THENA Auto)
                  THEN Reduce 0
                  THEN HypSubst' (-1) 0
                  THEN Reduce 0
                  THEN Fold `mrec` 0
                  THEN Auto)
                ; (Auto THEN RepUR ``prec-arg-types`` 0 THEN RWO "length-map" 0 THEN Auto)]
         )) }

1
1. L : MutualRectypeSpec
2. P : mobj(L) ⟶ TYPE
3. k : Atom
4. (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)
11. mrec-spec(L;lbl;k)[j] ~ inl inl x1
12. t.j ∈ mrec(L;x1)
⊢ <x1, t.j> ∈ {z:mobj(L)| z < <k, mk-prec(lbl;t)>} 

---

Latex:

---

Latex:

1.  L  :  MutualRectypeSpec
2.  P  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  k  :  Atom
4.  (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.  x1  :  Atom
10.  mrec-spec(L;lbl;k)[j]  =  (inl  inl  x1)
11.  mrec-spec(L;lbl;k)[j]  \msim{}  inl  inl  x1
\mvdash{}  <x1,  t.j>  \mmember{}  \{z:mobj(L)|  z  <  <k,  mk-prec(lbl;t)>\} 


By

---

Latex:
(Assert  t.j  \mmember{}  mrec(L;x1)  BY
              (InferEqualType
                THENL  [(RepUR  ``prec-arg-types``  0
                                THEN  (RWO  "select-map"  0  THENA  Auto)
                                THEN  Reduce  0
                                THEN  HypSubst'  (-1)  0
                                THEN  Reduce  0
                                THEN  Fold  `mrec`  0
                                THEN  Auto)
                            ;  (Auto  THEN  RepUR  ``prec-arg-types``  0  THEN  RWO  "length-map"  0  THEN  Auto)]
              ))

---

Home Index