Nuprl Lemma : sublist_accum

∀[T:Type]
  ∀L,l1,l2:T List. ∀f:(T List) ⟶ T ⟶ (T List).
    (l1 ⊆ l2
    ⇒ (∀x:T. ∀l:T List.  l ⊆ f[l;x])
    ⇒ l1 ⊆ accumulate (with value l and list item x):
             f[l;x]
            over list:
              L
            with starting value:
             l2))


Proof



Definitions occuring in Statement :  sublist: L1 ⊆ L2,  list_accum: list_accum,  list: T List,  uall: ∀[x:A]. B[x],  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],  member: t ∈ T,  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  prop: ℙ,  so_apply: x[s1;s2],  so_apply: x[s],  so_lambda: λ2x y.t[x; y],  top: Top
Lemmas referenced :  list_induction,  all_wf,  list_wf,  sublist_wf,  list_accum_wf,  list_accum_nil_lemma,  list_accum_cons_lemma,  sublist_transitivity
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  lambdaFormation,  cut,  thin,  lemma_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  cumulativity,  hypothesis,  because_Cache,  functionEquality,  applyEquality,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  voidElimination,  voidEquality,  rename,  universeEquality
Latex:
\mforall{}[T:Type]
    \mforall{}L,l1,l2:T  List.  \mforall{}f:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List).
        (l1  \msubseteq{}  l2
        {}\mRightarrow{}  (\mforall{}x:T.  \mforall{}l:T  List.    l  \msubseteq{}  f[l;x])
        {}\mRightarrow{}  l1  \msubseteq{}  accumulate  (with  value  l  and  list  item  x):
                          f[l;x]
                        over  list:
                            L
                        with  starting  value:
                          l2))


Date html generated: 2016_05_15-PM-03_57_36
Last ObjectModification: 2015_12_27-PM-03_08_05

Theory : general


Home Index