---

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