Nuprl Lemma : list_accum_invariant2

  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ ℙ]
      ∀L:T List. ∀a:A.
         (∀a:A. ∀x:T.  ((x ∈ L)  P[a]  P[f[a;x]]))
         P[accumulate (with value and list item x):
             over list:
             with starting value:


Definitions occuring in Statement :  l_member: (x ∈ l) list_accum: list_accum list: List uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: so_apply: x[s] subtype_rel: A ⊆B so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] top: Top iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q or: P ∨ Q guard: {T}
Lemmas referenced :  list_induction all_wf l_member_wf list_accum_wf list_wf list_accum_nil_lemma nil_wf list_accum_cons_lemma cons_member equal_wf cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity functionEquality applyEquality hypothesis universeEquality because_Cache independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality rename productElimination inlFormation inrFormation

    \mforall{}f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
        \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}]
            \mforall{}L:T  List.  \mforall{}a:A.
                {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}x:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  P[a]  {}\mRightarrow{}  P[f[a;x]]))
                {}\mRightarrow{}  P[accumulate  (with  value  a  and  list  item  x):
                          over  list:
                          with  starting  value:

Date html generated: 2016_05_14-PM-01_40_44
Last ObjectModification: 2015_12_26-PM-05_29_54

Theory : list_1

Home Index