Nuprl Lemma : sqequal-list_accum

[F:Base]
  ∀[G:Base]
    ∀[H,J:Base].
      ∀as,b1,b2:Base.
        F[accumulate (with value and list item a):
           H[v;a]
          over list:
            as
          with starting value:
           b1)] G[accumulate (with value 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: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q and: P ∧ Q lambda: λx.A[x] base: Base sqle: s ≤ t sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] and: P ∧ Q cand: c∧ B prop: so_lambda: λ2x.t[x] implies:  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