Step * of Lemma sqle-list_ind

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

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

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

Latex:

Latex:
\mforall{}[F:Base]
\mforall{}[G:Base]
\mforall{}[H,J:Base].
\mforall{}as,b1,b2:Base.
F[rec-case(as)  of
[]  =>  b1
h::t  =>
r.H[h;t;r]]  \mleq{}  G[rec-case(as)  of
[]  =>  b2
h::t  =>
r.J[h;t;r]]
supposing  F[b1]  \mleq{}  G[b2]
supposing  \mforall{}x,y,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[x;y;r1]]  \mleq{}  G[J[x;y;r2]]))
supposing  strict1(\mlambda{}x.G[x])
supposing  strict1(\mlambda{}x.F[x])

By

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

Home Index