Nuprl Lemma : sqequal-list_accum-list_ind

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


Proof



Definitions occuring in Statement :  list_accum: list_accum,  list_ind: list_ind,  strict1: strict1(F),  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  all: ∀x:A. B[x],  lambda: λx.A[x],  base: Base,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  all: ∀x:A. B[x],  prop: ℙ,  so_lambda: λ2x.t[x],  so_apply: x[s]
Lemmas referenced :  strict1_wf,  base_wf,  all_wf,  sqle-list_ind-list_accum,  is-exception_wf,  has-value_wf_base,  sqle-list_accum-list_ind
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  lambdaFormation,  sqequalSqle,  lemma_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  independent_isectElimination,  hypothesis,  sqequalRule,  dependent_functionElimination,  divergentSqle,  sqleReflexivity,  baseApply,  closedConclusion,  baseClosed,  because_Cache,  sqequalAxiom,  lambdaEquality,  sqequalIntensionalEquality,  isect_memberEquality,  equalityTransitivity,  equalitySymmetry
Latex:
\mforall{}[F:Base]
    \mforall{}[G:Base]
        \mforall{}[H,J:Base].
            \mforall{}as,b1,b2:Base.
                F[accumulate  (with  value  v  and  list  item  a):
                      H[v;a]
                    over  list:
                        as
                    with  starting  value:
                      b1)]  \msim{}  G[b1;rec-case(as)  of
                                              []  =>  b2
                                              h::t  =>
                                                r.J[h;r]] 
                supposing  \mforall{}x:Base.  (F[x]  \msim{}  G[x;b2]) 
            supposing  \mforall{}a,b,c:Base.    (G[H[b;a];c]  \msim{}  G[b;J[a;c]]) 
        supposing  \mforall{}z:Base.  strict1(\mlambda{}x.G[z;x]) 
    supposing  strict1(\mlambda{}x.F[x])


Date html generated: 2016_05_14-AM-06_29_11
Last ObjectModification: 2016_01_14-PM-08_25_46

Theory : list_0


Home Index