---

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

.....set predicate..... 
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. 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 )
12. t.j ∈ mrec(L;y) List
13. u : mrec(L;y)
14. (u ∈ t.j)
⊢ <y, u> < <k, mk-prec(lbl;t)>
BY
{ (RepUR ``mrec-lt prec_sub+`` 0 THEN (BLemma `implies-rel_plus` THENW Auto) THEN RepUR ``prec_sub prec-sub let`` 0) }

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. 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 )
12. t.j ∈ mrec(L;y) List
13. u : mrec(L;y)
14. (u ∈ t.j)
⊢ ∃k@0:ℕ||mrec-spec(L;lbl;k)||
   ((↑isl(mrec-spec(L;lbl;k)[k@0]))
   ∧ (((outl(mrec-spec(L;lbl;k)[k@0]) = (inl y) ∈ (Atom + Atom)) ∧ (u = t.k@0 ∈ prec(lbl,i.mrec-spec(L;lbl;i);y)))
     ∨ ((outl(mrec-spec(L;lbl;k)[k@0]) = (inr y ) ∈ (Atom + Atom)) ∧ (u ∈ t.k@0))))

---

Latex:

---

Latex:
.....set  predicate..... 
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.  y  :  Atom
10.  mrec-spec(L;lbl;k)[j]  =  (inl  (inr  y  ))
11.  mrec-spec(L;lbl;k)[j]  \msim{}  inl  (inr  y  )
12.  t.j  \mmember{}  mrec(L;y)  List
13.  u  :  mrec(L;y)
14.  (u  \mmember{}  t.j)
\mvdash{}  <y,  u>  <  <k,  mk-prec(lbl;t)>


By

---

Latex:
(RepUR  ``mrec-lt  prec\_sub+``  0
  THEN  (BLemma  `implies-rel\_plus`  THENW  Auto)
  THEN  RepUR  ``prec\_sub  prec-sub  let``  0)

---

Home Index