---

Step * of Lemma mrecind_wf

∀[L:MutualRectypeSpec]. ∀[P:mobj(L) ⟶ ℙ].  (mrecind(L;x.P[x]) ∈ ℙ)
BY
{ (Auto
   THEN Unfold `mrecind` 0
   THEN (MemCD THENL [Auto; D -1])
   THEN (MemCD THENL [Auto; Id])
   THEN (Assert 0 < ||mrec-spec(L;lbl;k)|| BY
               Auto)
   THEN MoveToConcl (-1)
   THEN RepUR ``prec-arg-types`` 0
   THEN (GenConclTerm ⌜mrec-spec(L;lbl;k)⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (MemCD THENL [Auto; MemCD])) }

1
.....subterm..... T:t
1:n
1. L : MutualRectypeSpec
2. P : mobj(L) ⟶ ℙ
3. k : Atom
4. (k ∈ eager-map(λp.(fst(p));L))
5. lbl : {lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} 
6. v : (Atom + Atom + Type) List
7. mrec-spec(L;lbl;k) = v ∈ ((Atom + Atom + Type) List)
8. 0 < ||v||
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))
⊢ ∀j:ℕ||v||. case v[j] of inl(y) => case y of inl(p) => P[<p, t.j>] | inr(p) => (∀u∈t.j.P[<p, u>]) | inr(_) => True ∈ ℙ

2
.....subterm..... T:t
2:n
1. L : MutualRectypeSpec
2. P : mobj(L) ⟶ ℙ
3. k : Atom
4. (k ∈ eager-map(λp.(fst(p));L))
5. lbl : {lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} 
6. v : (Atom + Atom + Type) List
7. mrec-spec(L;lbl;k) = v ∈ ((Atom + Atom + Type) List)
8. 0 < ||v||
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||. case v[j] of inl(y) => case y of inl(p) => P[<p, t.j>] | inr(p) => (∀u∈t.j.P[<p, u>]) | inr(_) => True
⊢ P[<k, mk-prec(lbl;t)>] ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[P:mobj(L)  {}\mrightarrow{}  \mBbbP{}].    (mrecind(L;x.P[x])  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  Unfold  `mrecind`  0
  THEN  (MemCD  THENL  [Auto;  D  -1])
  THEN  (MemCD  THENL  [Auto;  Id])
  THEN  (Assert  0  <  ||mrec-spec(L;lbl;k)||  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``prec-arg-types``  0
  THEN  (GenConclTerm  \mkleeneopen{}mrec-spec(L;lbl;k)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (MemCD  THENL  [Auto;  MemCD]))

---

Home Index