Nuprl Lemma : sqequal-list_accum

∀[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[accumulate (with value v and list item a):
                     J[v;a]
                    over list:
                      as
                    with starting value:
                     b2)] 
        supposing F[b1] ~ G[b2] 
      supposing (∀a,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]])))
      ∧ (∀a,r1,r2:Base.  ((G[r1] ≤ F[r2]) ⇒ (G[J[r1;a]] ≤ F[H[r2;a]]))) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])


Proof



Definitions occuring in Statement :  list_accum: list_accum,  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],  implies: P ⇒ Q,  and: P ∧ Q,  lambda: λx.A[x],  base: Base,  sqle: s ≤ t,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  all: ∀x:A. B[x],  and: P ∧ Q,  cand: A c∧ B,  prop: ℙ,  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  so_apply: x[s],  so_apply: x[s1;s2]
Lemmas referenced :  strict1_wf,  sqle_wf_base,  all_wf,  base_wf,  sqle-list_accum
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  lambdaFormation,  sqequalSqle,  sqequalHypSubstitution,  productElimination,  thin,  lemma_by_obid,  isectElimination,  hypothesisEquality,  independent_isectElimination,  hypothesis,  dependent_functionElimination,  sqequalRule,  sqleReflexivity,  sqequalAxiom,  sqequalIntensionalEquality,  baseApply,  closedConclusion,  baseClosed,  lambdaEquality,  isect_memberEquality,  because_Cache,  equalityTransitivity,  equalitySymmetry,  productEquality,  functionEquality
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[accumulate  (with  value  v  and  list  item  a):
                                          J[v;a]
                                        over  list:
                                            as
                                        with  starting  value:
                                          b2)] 
                supposing  F[b1]  \msim{}  G[b2] 
            supposing  (\mforall{}a,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[r1;a]]  \mleq{}  G[J[r2;a]])))
            \mwedge{}  (\mforall{}a,r1,r2:Base.    ((G[r1]  \mleq{}  F[r2])  {}\mRightarrow{}  (G[J[r1;a]]  \mleq{}  F[H[r2;a]]))) 
        supposing  strict1(\mlambda{}x.G[x]) 
    supposing  strict1(\mlambda{}x.F[x])


Date html generated: 2016_05_14-AM-06_27_53
Last ObjectModification: 2016_01_14-PM-08_26_18

Theory : list_0


Home Index