---

Step * 1 of Lemma mrecind_wf

.....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 ∈ ℙ
BY
{ (MemCD THENL [Auto; RepeatFor 2 ((MemCD THENA Auto))]) }

1
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||
11. x : Atom + Atom
12. v[j] = (inl x) ∈ (Atom + Atom + Type)
13. x1 : Atom
14. x = (inl x1) ∈ (Atom + Atom)
⊢ P[<x1, t.j>] ∈ ℙ

2
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||
11. x : Atom + Atom
12. v[j] = (inl x) ∈ (Atom + Atom + Type)
13. y : Atom
14. x = (inr y ) ∈ (Atom + Atom)
⊢ (∀u∈t.j.P[<y, u>]) ∈ ℙ

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  L  :  MutualRectypeSpec
2.  P  :  mobj(L)  {}\mrightarrow{}  \mBbbP{}
3.  k  :  Atom
4.  (k  \mmember{}  eager-map(\mlambda{}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
8.  0  <  ||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))
\mvdash{}  \mforall{}j:\mBbbN{}||v||
        case  v[j]  of  inl(y)  =>  case  y  of  inl(p)  =>  P[<p,  t.j>]  |  inr(p)  =>  (\mforall{}u\mmember{}t.j.P[<p,  u>])  |  inr(\mbackslash{}ff2\000C4_{}$)  =>  True  \mmember{}  \mBbbP{}


By

---

Latex:
(MemCD  THENL  [Auto;  RepeatFor  2  ((MemCD  THENA  Auto))])

---

Home Index