Nuprl Lemma : lifting2_wf

[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].  (lifting2(f;abag;bbag) ∈ bag(C))


Proof




Definitions occuring in Statement :  lifting2: lifting2(f;abag;bbag) bag: bag(T) uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lifting2: lifting2(f;abag;bbag) nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: 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 sq_type: SQType(T) select: L[n] cons: [a b] subtract: m subtype_rel: A ⊆B funtype: funtype(n;A;T) primrec: primrec(n;b;c)
Lemmas referenced :  lifting-gen-rev_wf false_wf le_wf select_wf cons_wf nil_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_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_wf length_of_cons_lemma length_of_nil_lemma decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma int_seg_wf decidable__equal_int subtype_base_sq int_subtype_base int_seg_subtype int_seg_cases subtype_rel_self funtype_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation hypothesis lambdaEquality instantiate universeEquality because_Cache cumulativity setElimination rename independent_isectElimination productElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality addEquality equalityTransitivity equalitySymmetry hypothesis_subsumption applyEquality axiomEquality functionEquality

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[abag:bag(A)].  \mforall{}[bbag:bag(B)].    (lifting2(f;abag;bbag)  \mmember{}  bag(C))



Date html generated: 2018_05_21-PM-06_26_19
Last ObjectModification: 2018_05_19-PM-05_15_57

Theory : bags


Home Index