---

Step * 1 of Lemma prec-size-unfold

.....subterm..... T:t
1:n
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. i : P
4. labl : {lbl:Atom| 0 < ||a[lbl;i]||} 
5. v : (P + P + Type) List
6. a[labl;i] = v ∈ ((P + P + Type) List)
7. t1 : tuple-type(map(λx.case x
                           of inl(y) =>
                           case y of inl(p) => prec(lbl,p.a[lbl;p];p) | inr(p) => prec(lbl,p.a[lbl;p];p) List
                           | inr(E) =>
                           E;v))
8. y : P
9. u : prec(lbl,p.a[lbl;p];y) List
10. 0 ≤ l_sum(map(λz.||y;z||;u))
⊢ map(λz.||y;z||;u) = map(pcorec-size(lbl,p.a[lbl;p]) y;u) ∈ (ℤ List)
BY
{ (EqCDA THEN FunExt THEN Reduce 0 THEN Try (Fold  `prec-size` 0) THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  P  :  Type
2.  a  :  Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)
3.  i  :  P
4.  labl  :  \{lbl:Atom|  0  <  ||a[lbl;i]||\} 
5.  v  :  (P  +  P  +  Type)  List
6.  a[labl;i]  =  v
7.  t1  :  tuple-type(map(\mlambda{}x.case  x
                                                      of  inl(y)  =>
                                                      case  y
                                                        of  inl(p)  =>
                                                        prec(lbl,p.a[lbl;p];p)
                                                        |  inr(p)  =>
                                                        prec(lbl,p.a[lbl;p];p)  List
                                                      |  inr(E)  =>
                                                      E;v))
8.  y  :  P
9.  u  :  prec(lbl,p.a[lbl;p];y)  List
10.  0  \mleq{}  l\_sum(map(\mlambda{}z.||y;z||;u))
\mvdash{}  map(\mlambda{}z.||y;z||;u)  =  map(pcorec-size(lbl,p.a[lbl;p])  y;u)


By

---

Latex:
(EqCDA  THEN  FunExt  THEN  Reduce  0  THEN  Try  (Fold    `prec-size`  0)  THEN  Auto)

---

Home Index