Nuprl Lemma : lifting-2-strict

[f:Top]. ∀[b:bag(Top)].  ((lifting-2(f) {} {}) ∧ (lifting-2(f) {} {}))


Proof




Definitions occuring in Statement :  lifting-2: lifting-2(f) empty-bag: {} bag: bag(T) uall: [x:A]. B[x] top: Top and: P ∧ Q apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: lifting-2: lifting-2(f) lifting2: lifting2(f;abag;bbag) lifting-gen: lifting-gen(n;f) int_seg: {i..j-} uimplies: supposing a guard: {T} lelt: i ≤ j < k all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top less_than: a < b squash: T true: True empty-bag: {} bag-null: bag-null(bs) select: L[n] cons: [a b] assert: b ifthenelse: if then else fi  btrue: tt subtype_rel: A ⊆B subtract: m
Lemmas referenced :  list_wf bag-subtype-list list-subtype-bag null_wf assert_wf null_nil_lemma lelt_wf int_seg_wf int_term_value_add_lemma int_formula_prop_less_lemma itermAdd_wf intformless_wf decidable__lt length_of_nil_lemma length_of_cons_lemma int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le int_seg_properties nil_wf empty-bag_wf cons_wf top_wf bag_wf select_wf le_wf false_wf lifting-gen-strict
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation lambdaFormation hypothesis hypothesisEquality lambdaEquality because_Cache setElimination rename independent_isectElimination productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll addEquality independent_pairEquality sqequalAxiom imageMemberEquality baseClosed applyEquality

Latex:
\mforall{}[f:Top].  \mforall{}[b:bag(Top)].    ((lifting-2(f)  \{\}  b  \msim{}  \{\})  \mwedge{}  (lifting-2(f)  b  \{\}  \msim{}  \{\}))



Date html generated: 2016_05_15-PM-03_02_07
Last ObjectModification: 2016_01_16-AM-08_36_35

Theory : bags


Home Index