Nuprl Lemma : list_accum_proper_iseg_inv

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[R:A ⟶ A ⟶ ℙ]
      (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 :  proper-iseg: L1 < L2,  list_accum: list_accum,  list: T List,  trans: Trans(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,  proper-iseg: L1 < L2,  and: 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],  or: P ∨ Q,  not: ¬A,  false: False,  cons: [a / b],  so_lambda: λ2x.t[x],  so_apply: x[s],  guard: {T},  trans: Trans(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,  list-cases,  append-nil,  product_subtype_list,  list_accum_cons_lemma,  proper-iseg_wf,  list_wf,  all_wf,  trans_wf,  list_induction,  list_accum_nil_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,  dependent_functionElimination,  unionElimination,  independent_functionElimination,  equalitySymmetry,  promote_hyp,  hypothesis_subsumption,  equalityTransitivity,  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{}]
            (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  <  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_24
Last ObjectModification: 2017_07_26-PM-04_54_24

Theory : general


Home Index