Step * of Lemma sqle-list_ind-list_accum

`∀[F:Base]`
`  ∀[G:Base]`
`    ∀[H,J:Base].`
`      ∀as,b1,b2:Base.`
`        G[b1;rec-case(as) of`
`             [] => b2`
`             h::t =>`
`              r.J[h;r]] ≤ F[accumulate (with value v and list item a):`
`                             H[v;a]`
`                            over list:`
`                              as`
`                            with starting value:`
`                             b1)] `
`        supposing ∀x:Base. (G[x;b2] ≤ F[x]) `
`      supposing ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c]) `
`    supposing ∀z:Base. strict1(λx.G[z;x]) `
`  supposing strict1(λx.F[x])`
BY
`{ ((UnivCD THENA Auto)`
`   THEN Assert ⌜∀j:ℕ. ∀as,x:Base.`
`                  (G[x;λlist_ind,L. eval v = L in`
`                                    if v is a pair then let h,t = v `
`                                                        in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j `
`                       ⊥ `
`                       as] ≤ F[λlist_accum,y,L. eval v = L in`
`                                                if v is a pair then let h,t = v `
`                                                                    in list_accum H[y;h] t`
`                                                otherwise if v = Ax then y otherwise ⊥^j `
`                               ⊥ `
`                               x `
`                               as])⌝⋅`
`   ) }`

1
`.....assertion..... `
`1. F : Base`
`2. strict1(λx.F[x])`
`3. G : Base`
`4. ∀z:Base. strict1(λx.G[z;x])`
`5. H : Base`
`6. J : Base`
`7. ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c])`
`8. as : Base@i`
`9. b1 : Base@i`
`10. b2 : Base@i`
`11. ∀x:Base. (G[x;b2] ≤ F[x])`
`⊢ ∀j:ℕ. ∀as,x:Base.`
`    (G[x;λlist_ind,L. eval v = L in`
`                      if v is a pair then let h,t = v `
`                                          in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j `
`         ⊥ `
`         as] ≤ F[λlist_accum,y,L. eval v = L in`
`                                  if v is a pair then let h,t = v `
`                                                      in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j `
`                 ⊥ `
`                 x `
`                 as])`

2
`1. F : Base`
`2. strict1(λx.F[x])`
`3. G : Base`
`4. ∀z:Base. strict1(λx.G[z;x])`
`5. H : Base`
`6. J : Base`
`7. ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c])`
`8. as : Base@i`
`9. b1 : Base@i`
`10. b2 : Base@i`
`11. ∀x:Base. (G[x;b2] ≤ F[x])`
`12. ∀j:ℕ. ∀as,x:Base.`
`      (G[x;λlist_ind,L. eval v = L in`
`                        if v is a pair then let h,t = v `
`                                            in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j `
`           ⊥ `
`           as] ≤ F[λlist_accum,y,L. eval v = L in`
`                                    if v is a pair then let h,t = v `
`                                                        in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j `
`                   ⊥ `
`                   x `
`                   as])`
`⊢ G[b1;rec-case(as) of`
`       [] => b2`
`       h::t =>`
`        r.J[h;r]] ≤ F[accumulate (with value v and list item a):`
`                       H[v;a]`
`                      over list:`
`                        as`
`                      with starting value:`
`                       b1)]`

Latex:

Latex:
\mforall{}[F:Base]
\mforall{}[G:Base]
\mforall{}[H,J:Base].
\mforall{}as,b1,b2:Base.
G[b1;rec-case(as)  of
[]  =>  b2
h::t  =>
r.J[h;r]]  \mleq{}  F[accumulate  (with  value  v  and  list  item  a):
H[v;a]
over  list:
as
with  starting  value:
b1)]
supposing  \mforall{}x:Base.  (G[x;b2]  \mleq{}  F[x])
supposing  \mforall{}a,b,c:Base.    (G[b;J[a;c]]  \mleq{}  G[H[b;a];c])
supposing  \mforall{}z:Base.  strict1(\mlambda{}x.G[z;x])
supposing  strict1(\mlambda{}x.F[x])

By

Latex:
((UnivCD  THENA  Auto)
THEN  Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}.  \mforall{}as,x:Base.
(G[x;\mlambda{}list\$_{ind}\$,L.  eval  v  =  L  in
if  v  is  a  pair  then  let  h,t  =  v
in  J[h;list\$_{ind}\$  t]
otherwise  if  v  =  Ax  then  b2  otherwise  \mbot{}\^{}j
\mbot{}
as]  \mleq{}  F[\mlambda{}list\$_{accum}\$,y,L.  eval  v  =  L  in
if  v  is  a  pair  then  let  h,t  =  v
in  list\$_{accum}\mbackslash{}ff\000C24  H[y;h]  t
otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j
\mbot{}
x
as])\mkleeneclose{}\mcdot{}
)

Home Index