Nuprl Lemma : bl-exists-as-accum

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


Proof



Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b,  list_accum: list_accum,  list: T List,  bor: p ∨bq,  bfalse: ff,  bool: 𝔹,  uall: ∀[x:A]. B[x],  so_apply: x[s],  function: x:A ⟶ B[x],  universe: Type,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  bl-exists: (∃x∈L.P[x])_b,  squash: ↓T,  prop: ℙ,  so_apply: x[s],  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  and: P ∧ Q,  top: Top,  true: True,  subtype_rel: A ⊆r B,  guard: {T},  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  bfalse: ff,  exists: ∃x:A. B[x],  or: P ∨ Q,  sq_type: SQType(T),  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  assert: ↑b,  false: False,  bor: p ∨bq,  so_lambda: λ2x y.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
Latex:
\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:
                                          L
                                      with  starting  value:
                                        ff))


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

Theory : list_1


Home Index