---

Step * of Lemma prec-sub-size

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].
∀[y:prec(lbl,p.a[lbl;p];i)].
  ||j;x|| < ||i;y|| supposing prec-sub(P;lbl,p.a[lbl;p];j;x;i;y)
BY
{ (Auto
   THEN (RW (AddrC [2] (LemmaC `prec-size-unfold`)) 0  THENA Auto)
   THEN pRecElim (-2)
   THEN Reduce 0
   THEN (Assert ⌜||j;x|| ≤ tuple-sum(λc,x. case c
                                           of inl(p) =>
                                           case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
                                           | inr(_) =>
                                           0;a[labl;i];y1)⌝⋅
   THENM (MoveToConcl (-1)
          THEN GenConcl ⌜tuple-sum(λc,x. case c
                                         of inl(p) =>
                                         case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
                                         | inr(_) =>
                                         0;a[labl;i];y1)
                         = X
                         ∈ ℕ⌝⋅
          THEN Auto)
   )) }

1
.....assertion..... 
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : {lbl:Atom| 0 < ||a[lbl;i]||} 
7. y1 : 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;a[labl;i]))
8. prec-sub(P;lbl,p.a[lbl;p];j;x;i;<labl, y1>)
⊢ ||j;x|| ≤ tuple-sum(λc,x. case c
                            of inl(p) =>
                            case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
                            | inr(_) =>
                            0;a[labl;i];y1)

2
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : {lbl:Atom| 0 < ||a[lbl;i]||} 
7. y1 : 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;a[labl;i]))
8. prec-sub(P;lbl,p.a[lbl;p];j;x;i;<labl, y1>)
9. y : P
10. x1 : (λ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) 
         (inl (inr y ))
⊢ l_sum(map(λz.||y;z||;x1)) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[j:P].  \mforall{}[x:prec(lbl,p.a[lbl;p];j)].  \mforall{}[i:P].
\mforall{}[y:prec(lbl,p.a[lbl;p];i)].
    ||j;x||  <  ||i;y||  supposing  prec-sub(P;lbl,p.a[lbl;p];j;x;i;y)


By

---

Latex:
(Auto
  THEN  (RW  (AddrC  [2]  (LemmaC  `prec-size-unfold`))  0    THENA  Auto)
  THEN  pRecElim  (-2)
  THEN  Reduce  0
  THEN  (Assert  \mkleeneopen{}||j;x||  \mleq{}  tuple-sum(\mlambda{}c,x.  case  c
                                                                                  of  inl(p)  =>
                                                                                  case  p
                                                                                    of  inl(j)  =>
                                                                                    ||j;x||
                                                                                    |  inr(j)  =>
                                                                                    l\_sum(map(\mlambda{}z.||j;z||;x))
                                                                                  |  inr($_{}$)  =>
                                                                                  0;a[labl;i];y1)\mkleeneclose{}\mcdot{}
  THENM  (MoveToConcl  (-1)
                THEN  GenConcl  \mkleeneopen{}tuple-sum(\mlambda{}c,x.  case  c
                                                                              of  inl(p)  =>
                                                                              case  p
                                                                                of  inl(j)  =>
                                                                                ||j;x||
                                                                                |  inr(j)  =>
                                                                                l\_sum(map(\mlambda{}z.||j;z||;x))
                                                                              |  inr($_{}$)  =>
                                                                              0;a[labl;i];y1)
                                              =  X\mkleeneclose{}\mcdot{}
                THEN  Auto)
  ))

---

Home Index