Nuprl Lemma : concat-lifting-3-strict

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


Proof




Definitions occuring in Statement :  concat-lifting-3: concat-lifting-3(f) empty-bag: {} bag: bag(T) uall: [x:A]. B[x] top: Top all: x:A. B[x] and: P ∧ Q apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] and: P ∧ Q cand: c∧ B concat-lifting-3: concat-lifting-3(f) concat-lifting: concat-lifting(n;f;bags) concat-lifting-list: concat-lifting-list(n;bags) nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: lifting-gen: lifting-gen(n;f) lifting-gen-rev: lifting-gen-rev(n;f;bags) int_seg: {i..j-} uimplies: supposing a guard: {T} lelt: i ≤ j < k 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 bag_union_empty_lemma 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 lambdaFormation sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality natural_numberEquality independent_pairFormation 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)].
    \mforall{}b':bag(Top)
        ((concat-lifting-3(f)  \{\}  b  b'  \msim{}  \{\})
        \mwedge{}  (concat-lifting-3(f)  b  \{\}  b'  \msim{}  \{\})
        \mwedge{}  (concat-lifting-3(f)  b  b'  \{\}  \msim{}  \{\}))



Date html generated: 2016_05_15-PM-03_08_37
Last ObjectModification: 2016_01_16-AM-08_35_53

Theory : bags


Home Index