Nuprl Lemma : bag-lub_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  (bag-lub(eq;bs;as) ∈ bag(T))


Proof




Definitions occuring in Statement :  bag-lub: bag-lub(eq;b1;b2) bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-lub: bag-lub(eq;b1;b2) so_lambda: λ2x.t[x] nat: subtype_rel: A ⊆B all: x:A. B[x] implies:  Q guard: {T} ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top and: P ∧ Q prop: so_apply: x[s]
Lemmas referenced :  bag-combine_wf bag-to-set_wf bag-append_wf bag-rep_wf imax_wf bag-count_wf imax_nat nat_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf equal_wf le_wf list-subtype-bag bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality because_Cache hypothesis lambdaEquality dependent_set_memberEquality applyEquality setElimination rename lambdaFormation equalityTransitivity equalitySymmetry applyLambdaEquality dependent_functionElimination natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll independent_functionElimination axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs,as:bag(T)].    (bag-lub(eq;bs;as)  \mmember{}  bag(T))



Date html generated: 2018_05_21-PM-09_52_16
Last ObjectModification: 2017_07_26-PM-06_31_46

Theory : bags_2


Home Index