Nuprl Lemma : list_accum_iseg_inv

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[R:A ⟶ A ⟶ ℙ]
      (Refl(A;a,b.R[a;b])
      ⇒ Trans(A;a,b.R[a;b])
      ⇒ (∀a:A. ∀x:T.  R[a;f[a;x]])
      ⇒ (∀a:A. ∀L1,L2:T List.
            (L1 ≤ L2
            ⇒ R[accumulate (with value a and list item x):
                  f[a;x]
                 over list:
                   L1
                 with starting value:
                  a);accumulate (with value a and list item x):
                      f[a;x]
                     over list:
                       L2
                     with starting value:
                      a)])))


Proof



Definitions occuring in Statement :  iseg: l1 ≤ l2,  list_accum: list_accum,  list: T List,  trans: Trans(T;x,y.E[x; y]),  refl: Refl(T;x,y.E[x; y]),  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s1;s2],  all: ∀x:A. B[x],  implies: P ⇒ Q,  function: x:A ⟶ B[x],  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  iseg: l1 ≤ l2,  exists: ∃x:A. B[x],  member: t ∈ T,  prop: ℙ,  subtype_rel: A ⊆r B,  uimplies: b supposing a,  top: Top,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  so_lambda: λ2x.t[x],  so_apply: x[s],  trans: Trans(T;x,y.E[x; y]),  guard: {T},  refl: Refl(T;x,y.E[x; y])
Lemmas referenced :  length_wf_nat,  equal_wf,  nat_wf,  list_accum_append,  subtype_rel_list,  top_wf,  list_accum_wf,  iseg_wf,  list_wf,  all_wf,  trans_wf,  refl_wf,  list_induction,  list_accum_nil_lemma,  list_accum_cons_lemma
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  lambdaFormation,  sqequalHypSubstitution,  productElimination,  thin,  cut,  dependent_set_memberEquality,  hypothesis,  introduction,  extract_by_obid,  isectElimination,  cumulativity,  hypothesisEquality,  sqequalRule,  applyEquality,  independent_isectElimination,  lambdaEquality,  isect_memberEquality,  voidElimination,  voidEquality,  because_Cache,  functionExtensionality,  rename,  equalityTransitivity,  equalitySymmetry,  dependent_functionElimination,  independent_functionElimination,  hyp_replacement,  applyLambdaEquality,  setElimination,  functionEquality,  universeEquality
Latex:
\mforall{}[T,A:Type].
    \mforall{}f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
        \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
            (Refl(A;a,b.R[a;b])
            {}\mRightarrow{}  Trans(A;a,b.R[a;b])
            {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}x:T.    R[a;f[a;x]])
            {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}L1,L2:T  List.
                        (L1  \mleq{}  L2
                        {}\mRightarrow{}  R[accumulate  (with  value  a  and  list  item  x):
                                    f[a;x]
                                  over  list:
                                      L1
                                  with  starting  value:
                                    a);accumulate  (with  value  a  and  list  item  x):
                                            f[a;x]
                                          over  list:
                                              L2
                                          with  starting  value:
                                            a)])))


Date html generated: 2018_05_21-PM-06_42_16
Last ObjectModification: 2017_07_26-PM-04_54_20

Theory : general


Home Index