Nuprl Lemma : member_list_accum_l_subset2

[T:Type]
  ∀f:(T List) ⟶ T ⟶ (T List). ∀L,a:T List. ∀x:T.
    ((∀a:T List. ∀x:T.  l_subset(T;f[a;x];[x a]))
     (x ∈ accumulate (with value and list item x):
             f[a;x]
            over list:
              L
            with starting value:
             a))
     ((x ∈ a) ∨ (x ∈ L)))


Proof




Definitions occuring in Statement :  l_subset: l_subset(T;as;bs) l_member: (x ∈ l) list_accum: list_accum cons: [a b] list: List uall: [x:A]. B[x] so_apply: x[s1;s2] all: x:A. B[x] implies:  Q or: 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:  Q prop: so_apply: x[s1;s2] so_apply: x[s] so_lambda: λ2y.t[x; y] or: P ∨ Q top: Top l_subset: l_subset(T;as;bs) iff: ⇐⇒ Q and: P ∧ Q guard: {T} rev_implies:  Q
Lemmas referenced :  list_induction all_wf list_wf l_subset_wf cons_wf l_member_wf list_accum_wf or_wf list_accum_nil_lemma nil_wf list_accum_cons_lemma cons_member equal_wf
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 inlFormation rename unionElimination productElimination inrFormation universeEquality

Latex:
\mforall{}[T:Type]
    \mforall{}f:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List).  \mforall{}L,a:T  List.  \mforall{}x:T.
        ((\mforall{}a:T  List.  \mforall{}x:T.    l\_subset(T;f[a;x];[x  /  a]))
        {}\mRightarrow{}  (x  \mmember{}  accumulate  (with  value  a  and  list  item  x):
                          f[a;x]
                        over  list:
                            L
                        with  starting  value:
                          a))
        {}\mRightarrow{}  ((x  \mmember{}  a)  \mvee{}  (x  \mmember{}  L)))



Date html generated: 2016_05_15-PM-03_43_52
Last ObjectModification: 2015_12_27-PM-01_19_35

Theory : general


Home Index