Nuprl Lemma : bl-exists-as-accum

[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
  ((∃x∈L.P[x])_b accumulate (with value and list item x):
                    p ∨bP[x]
                   over list:
                   with starting value:


Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b list_accum: list_accum list: List bor: p ∨bq bfalse: ff bool: 𝔹 uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a bl-exists: (∃x∈L.P[x])_b squash: T prop: so_apply: x[s] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q top: Top true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b false: False bor: p ∨bq so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  subtype_base_sq bool_wf bool_subtype_base equal_wf squash_wf true_wf reduce-as-accum bor_wf eqtt_to_assert testxxx_lemma bor_tt_simp btrue_wf iff_weakening_equal eqff_to_assert bool_cases_sqequal assert-bnot bfalse_wf list_accum_wf list_wf bor_ff_simp
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesis independent_isectElimination applyEquality lambdaEquality imageElimination hypothesisEquality equalityTransitivity equalitySymmetry because_Cache functionExtensionality sqequalRule lambdaFormation unionElimination equalityElimination productElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination dependent_pairFormation promote_hyp universeEquality sqequalAxiom functionEquality

\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    ((\mexists{}x\mmember{}L.P[x])\_b  \msim{}  accumulate  (with  value  p  and  list  item  x):
                                        p  \mvee{}\msubb{}P[x]
                                      over  list:
                                      with  starting  value:

Date html generated: 2017_04_17-AM-08_03_30
Last ObjectModification: 2017_02_27-PM-04_33_38

Theory : list_1

Home Index