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