---

Step * 1 1 1 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
12. t.j ∈ mrec(L;x1)
⊢ ∃k@0:ℕ||mrec-spec(L;lbl;k)||
   ((↑isl(mrec-spec(L;lbl;k)[k@0]))
   ∧ (((outl(mrec-spec(L;lbl;k)[k@0]) = (inl x1) ∈ (Atom + Atom)) ∧ (t.j = t.k@0 ∈ prec(lbl,i.mrec-spec(L;lbl;i);x1)))
     ∨ ((outl(mrec-spec(L;lbl;k)[k@0]) = (inr x1 ) ∈ (Atom + Atom)) ∧ (t.j ∈ t.k@0))))
BY
{ (D 0 With ⌜j⌝ 
   THENL [Auto
         ; (HypSubst' (-2) 0 THEN Reduce 0 THEN Fold `mrec` 0 THEN Auto)
         ; (RenameVar `i' (-1)
            THEN (GenConclTerm ⌜mrec-spec(L;lbl;k)[i]⌝⋅ THENA Auto)
            THEN Fold `mrec` 0
            THEN D -2
            THEN Reduce 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. 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)
13. i : ℕ||mrec-spec(L;lbl;k)||
14. x : Atom + Atom
15. mrec-spec(L;lbl;k)[i] = (inl x) ∈ (Atom + Atom + Type)
⊢ istype(True
∧ (((x = (inl x1) ∈ (Atom + Atom)) ∧ (t.j = t.i ∈ mrec(L;x1))) ∨ ((x = (inr x1 ) ∈ (Atom + Atom)) ∧ (t.j ∈ t.i))))

2
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)
13. i : ℕ||mrec-spec(L;lbl;k)||
14. y : Type
15. mrec-spec(L;lbl;k)[i] = (inr y ) ∈ (Atom + Atom + Type)
⊢ istype(False
∧ (((⊥ = (inl x1) ∈ (Atom + Atom)) ∧ (t.j = t.i ∈ mrec(L;x1))) ∨ ((⊥ = (inr x1 ) ∈ (Atom + Atom)) ∧ (t.j ∈ t.i))))

---

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
12.  t.j  \mmember{}  mrec(L;x1)
\mvdash{}  \mexists{}k@0:\mBbbN{}||mrec-spec(L;lbl;k)||
      ((\muparrow{}isl(mrec-spec(L;lbl;k)[k@0]))
      \mwedge{}  (((outl(mrec-spec(L;lbl;k)[k@0])  =  (inl  x1))  \mwedge{}  (t.j  =  t.k@0))
          \mvee{}  ((outl(mrec-spec(L;lbl;k)[k@0])  =  (inr  x1  ))  \mwedge{}  (t.j  \mmember{}  t.k@0))))


By

---

Latex:
(D  0  With  \mkleeneopen{}j\mkleeneclose{} 
  THENL  [Auto
              ;  (HypSubst'  (-2)  0  THEN  Reduce  0  THEN  Fold  `mrec`  0  THEN  Auto)
              ;  (RenameVar  `i'  (-1)
                    THEN  (GenConclTerm  \mkleeneopen{}mrec-spec(L;lbl;k)[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
                    THEN  Fold  `mrec`  0
                    THEN  D  -2
                    THEN  Reduce  0)]
)

---

Home Index