---

Step * 1 1 2 of Lemma istype-mrecind


1. L : MutualRectypeSpec
2. P : mobj(L) ⟶ TYPE
3. k : Atom
4. (k ∈ eager-map(λp.(fst(p));L))
5. lbl : Atom
6. 0 < ||mrec-spec(L;lbl;k)||
7. v : (Atom + Atom + Type) List
8. mrec-spec(L;lbl;k) = v ∈ ((Atom + Atom + Type) List)
9. t : tuple-type(map(λx.case x
                          of inl(y) =>
                          case y
                           of inl(p) =>
                           prec(lbl,p.mrec-spec(L;lbl;p);p)
                           | inr(p) =>
                           prec(lbl,p.mrec-spec(L;lbl;p);p) List
                          | inr(E) =>
                          E;v))
10. j : ℕ||v||
11. y : Atom
12. v[j] = (inl (inr y )) ∈ (Atom + Atom + Type)
⊢ istype((∀u∈t.j.P[<y, u>]))
BY
{ ((GenConclTerm ⌜t.j⌝⋅ THENA (MemCD THEN Try (RWO "map-length" 0) THEN Auto))
   THEN Thin (-1)
   THEN (RWO "select-map" (-1) THENA Auto)
   THEN Reduce -1
   THEN Fold `mrec` (-1)
   THEN (GenConcl ⌜v1 = X ∈ (mrec(L;y) List)⌝⋅ THENW (InferEqualType THEN Auto THEN RWO "-2" 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 : Atom
6. 0 < ||mrec-spec(L;lbl;k)||
7. v : (Atom + Atom + Type) List
8. mrec-spec(L;lbl;k) = v ∈ ((Atom + Atom + Type) List)
9. t : tuple-type(map(λx.case x
                          of inl(y) =>
                          case y
                           of inl(p) =>
                           prec(lbl,p.mrec-spec(L;lbl;p);p)
                           | inr(p) =>
                           prec(lbl,p.mrec-spec(L;lbl;p);p) List
                          | inr(E) =>
                          E;v))
10. j : ℕ||v||
11. y : Atom
12. v[j] = (inl (inr y )) ∈ (Atom + Atom + Type)
13. v1 : case v[j] of inl(y) => case y of inl(p) => mrec(L;p) | inr(p) => mrec(L;p) List | inr(E) => E
14. X : mrec(L;y) List
15. v1 = X ∈ (mrec(L;y) List)
⊢ istype((∀u∈X.P[<y, u>]))

---

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  :  Atom
6.  0  <  ||mrec-spec(L;lbl;k)||
7.  v  :  (Atom  +  Atom  +  Type)  List
8.  mrec-spec(L;lbl;k)  =  v
9.  t  :  tuple-type(map(\mlambda{}x.case  x
                                                    of  inl(y)  =>
                                                    case  y
                                                      of  inl(p)  =>
                                                      prec(lbl,p.mrec-spec(L;lbl;p);p)
                                                      |  inr(p)  =>
                                                      prec(lbl,p.mrec-spec(L;lbl;p);p)  List
                                                    |  inr(E)  =>
                                                    E;v))
10.  j  :  \mBbbN{}||v||
11.  y  :  Atom
12.  v[j]  =  (inl  (inr  y  ))
\mvdash{}  istype((\mforall{}u\mmember{}t.j.P[<y,  u>]))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}t.j\mkleeneclose{}\mcdot{}  THENA  (MemCD  THEN  Try  (RWO  "map-length"  0)  THEN  Auto))
  THEN  Thin  (-1)
  THEN  (RWO  "select-map"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  Fold  `mrec`  (-1)
  THEN  (GenConcl  \mkleeneopen{}v1  =  X\mkleeneclose{}\mcdot{}  THENW  (InferEqualType  THEN  Auto  THEN  RWO  "-2"  0  THEN  Auto)))

---

Home Index