Nuprl Lemma : bag-append-cancel

[T:Type]. ∀[as,bs,cs:bag(T)].  uiff((as bs) (as cs) ∈ bag(T);bs cs ∈ bag(T))


Proof




Definitions occuring in Statement :  bag-append: as bs bag: bag(T) uiff: uiff(P;Q) uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a squash: T exists: x:A. B[x] prop: subtype_rel: A ⊆B bag-append: as bs so_lambda: λ2x.t[x] implies:  Q so_apply: x[s] append: as bs all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] bag: bag(T) quotient: x,y:A//B[x; y] cand: c∧ B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  bag_to_squash_list equal_wf bag_wf bag-append_wf list-subtype-bag and_wf list_induction append_wf list_wf list_ind_nil_lemma nil_wf cons_wf list_ind_cons_lemma cons_cancel_wrt_permutation quotient-member-eq permutation_wf permutation-equiv member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement Error :applyLambdaEquality,  cumulativity sqequalRule rename applyEquality because_Cache independent_isectElimination lambdaEquality equalityTransitivity dependent_set_memberEquality setElimination setEquality independent_pairEquality isect_memberEquality axiomEquality functionEquality independent_functionElimination lambdaFormation dependent_functionElimination voidElimination voidEquality pertypeElimination productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs:bag(T)].    uiff((as  +  bs)  =  (as  +  cs);bs  =  cs)



Date html generated: 2016_10_25-AM-10_21_57
Last ObjectModification: 2016_07_12-AM-06_38_54

Theory : bags


Home Index