Nuprl Lemma : list_accum_equality

∀[T,A,B,C:Type]. ∀[f:A ⟶ T ⟶ A]. ∀[g:B ⟶ T ⟶ B]. ∀[F:A ⟶ C]. ∀[G:B ⟶ C].
  ∀[L:T List]. ∀[a0:A]. ∀[b0:B].
    F[accumulate (with value a and list item x):
       f[a;x]
      over list:
        L
      with starting value:
       a0)]
    = G[accumulate (with value b and list item x):
         g[b;x]
        over list:
          L
        with starting value:
         b0)]
    ∈ C 
    supposing F[a0] = G[b0] ∈ C 
  supposing ∀a:A. ∀b:B. ∀x:T.  (((F a) = (G b) ∈ C) ⇒ (F[f[a;x]] = G[g[b;x]] ∈ C))


Proof



Definitions occuring in Statement :  list_accum: list_accum,  list: T List,  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,  apply: f a,  function: x:A ⟶ B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  so_lambda: λ2x.t[x],  so_apply: x[s],  prop: ℙ,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  implies: P ⇒ Q,  all: ∀x:A. B[x],  top: Top
Lemmas referenced :  list_induction,  uall_wf,  isect_wf,  equal_wf,  list_accum_wf,  list_wf,  list_accum_nil_lemma,  list_accum_cons_lemma,  all_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  because_Cache,  cumulativity,  applyEquality,  functionExtensionality,  hypothesis,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  voidElimination,  voidEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  lambdaFormation,  rename,  independent_isectElimination,  functionEquality,  universeEquality
Latex:
\mforall{}[T,A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].  \mforall{}[g:B  {}\mrightarrow{}  T  {}\mrightarrow{}  B].  \mforall{}[F:A  {}\mrightarrow{}  C].  \mforall{}[G:B  {}\mrightarrow{}  C].
    \mforall{}[L:T  List].  \mforall{}[a0:A].  \mforall{}[b0:B].
        F[accumulate  (with  value  a  and  list  item  x):
              f[a;x]
            over  list:
                L
            with  starting  value:
              a0)]
        =  G[accumulate  (with  value  b  and  list  item  x):
                  g[b;x]
                over  list:
                    L
                with  starting  value:
                  b0)] 
        supposing  F[a0]  =  G[b0] 
    supposing  \mforall{}a:A.  \mforall{}b:B.  \mforall{}x:T.    (((F  a)  =  (G  b))  {}\mRightarrow{}  (F[f[a;x]]  =  G[g[b;x]]))


Date html generated: 2017_04_17-AM-07_38_32
Last ObjectModification: 2017_02_27-PM-04_12_54

Theory : list_1


Home Index