### Nuprl Lemma : bag_all-cons

`∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. ∀[f:T ⟶ 𝔹].  (bag_all(x.b;f) ~ (f x) ∧b bag_all(b;f))`

Proof

Definitions occuring in Statement :  bag_all: `bag_all(b;f)` cons-bag: `x.b` bag: `bag(T)` band: `p ∧b q` bool: `𝔹` uall: `∀[x:A]. B[x]` apply: `f a` 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` squash: `↓T` exists: `∃x:A. B[x]` bag_all: `bag_all(b;f)` cons-bag: `x.b` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` all: `∀x:A. B[x]` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` band: `p ∧b q` ifthenelse: `if b then t else f fi ` btrue: `tt` implies: `P `` Q` sq_type: `SQType(T)` guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` bool: `𝔹` unit: `Unit` it: `⋅` bfalse: `ff` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q`
Lemmas referenced :  subtype_base_sq bool_wf bool_subtype_base bag_to_squash_list list_accum_cons_lemma btrue_wf band-btrue list_induction all_wf equal_wf list_accum_wf eqtt_to_assert list_wf list_accum_nil_lemma band_assoc band_wf bag_all_wf cons-bag_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesis independent_isectElimination because_Cache hypothesisEquality imageElimination productElimination promote_hyp rename sqequalRule dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation equalitySymmetry equalityTransitivity independent_functionElimination applyEquality functionExtensionality lambdaEquality unionElimination equalityElimination hyp_replacement applyLambdaEquality sqequalAxiom functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbB{}].    (bag\_all(x.b;f)  \msim{}  (f  x)  \mwedge{}\msubb{}  bag\_all(b;f))

Date html generated: 2017_10_01-AM-08_52_23
Last ObjectModification: 2017_07_26-PM-04_33_58

Theory : bags

Home Index