Nuprl Lemma : lifting-0_wf

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


Proof




Definitions occuring in Statement :  lifting-0: lifting-0(b) 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 lifting-0: lifting-0(b) 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) primrec: primrec(n;b;c) lifting-gen-rev: lifting-gen-rev(n;f;bags) 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]
Lemmas referenced :  subtype_rel_self 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 lifting-gen-rev_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 because_Cache dependent_set_memberEquality natural_numberEquality independent_pairFormation hypothesisEquality lambdaEquality setElimination rename productElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination computeAll applyEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

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



Date html generated: 2016_05_15-PM-03_01_15
Last ObjectModification: 2016_01_16-AM-08_36_27

Theory : bags


Home Index