Nuprl Lemma : concat-lifting-0_wf

[B:Type]. ∀[f:bag(B)].  (concat-lifting-0(f) ∈ bag(B))


Proof




Definitions occuring in Statement :  concat-lifting-0: concat-lifting-0(f) bag: bag(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T concat-lifting-0: concat-lifting-0(f) select: L[n] uimplies: supposing a all: x:A. B[x] nil: [] it: so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: guard: {T} int_seg: {i..j-} lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] subtype_rel: A ⊆B funtype: funtype(n;A;T) concat-lifting: concat-lifting(n;f;bags) concat-lifting-list: concat-lifting-list(n;bags) bag-union: bag-union(bbs) concat: concat(ll) reduce: reduce(f;k;as) list_ind: list_ind lifting-gen-list-rev: lifting-gen-list-rev(n;bags) ifthenelse: if then else fi  eq_int: (i =z j) btrue: tt single-bag: {x} cons: [a b] append: as bs
Lemmas referenced :  bag_wf primrec0_lemma int_seg_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt int_seg_properties le_wf false_wf concat-lifting_wf base_wf stuck-spread
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin baseClosed independent_isectElimination lambdaFormation hypothesis isect_memberEquality voidElimination voidEquality hypothesisEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaEquality because_Cache setElimination rename productElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination computeAll applyEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[B:Type].  \mforall{}[f:bag(B)].    (concat-lifting-0(f)  \mmember{}  bag(B))



Date html generated: 2016_05_15-PM-03_07_39
Last ObjectModification: 2016_01_16-AM-08_34_30

Theory : bags


Home Index