Nuprl Lemma : bag-remove1-append1

[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[bs:bag(T)].
  (bag-remove1(eq;{y} bs;x)
  if eq then inl bs else case bag-remove1(eq;bs;x) of inl(as) => inl ({y} as) inr(x) => inr ⋅  fi 
  ∈ (bag(T)?))


Definitions occuring in Statement :  bag-remove1: bag-remove1(eq;bs;a) bag-append: as bs single-bag: {x} bag: bag(T) deq: EqDecider(T) ifthenelse: if then else fi  it: uall: [x:A]. B[x] unit: Unit apply: a decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T deq: EqDecider(T) all: x:A. B[x] implies:  Q exposed-bfalse: exposed-bfalse bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a eqof: eqof(d) ifthenelse: if then else fi  squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A prop: isl: isl(x) sq_or: a ↓∨ b
Lemmas referenced :  eqtt_to_assert safe-assert-deq equal_wf bag_wf unit_wf2 bag-remove1_wf bag-append_wf single-bag_wf iff_weakening_equal bag-remove1-member eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_weakening_uiff assert_wf bag-remove1-property squash_wf true_wf istype-universe inl-one-one not-0-eq-1 inr-one-one it_wf subtype_rel_self btrue_wf bfalse_wf btrue_neq_bfalse bag-append-assoc-comm bag-append-cancel bag-member-single bag-member_wf bag-member-append
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut applyEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality hypothesis inhabitedIsType lambdaFormation_alt unionElimination equalityElimination extract_by_obid isectElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule lambdaEquality_alt imageElimination because_Cache universeIsType universeEquality unionEquality dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed inlEquality_alt independent_functionElimination dependent_pairFormation_alt equalityIsType3 promote_hyp instantiate voidElimination equalityIsType1 isect_memberEquality_alt axiomEquality isectIsTypeImplies applyLambdaEquality inrEquality_alt dependent_set_memberEquality_alt independent_pairFormation productIsType inrFormation_alt inlFormation_alt

\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].  \mforall{}[bs:bag(T)].
    (bag-remove1(eq;\{y\}  +  bs;x)
    =  if  eq  x  y
        then  inl  bs
        else  case  bag-remove1(eq;bs;x)  of  inl(as)  =>  inl  (\{y\}  +  as)  |  inr(x)  =>  inr  \mcdot{} 
        fi  )

Date html generated: 2019_10_16-AM-11_31_08
Last ObjectModification: 2018_10_16-AM-09_34_29

Theory : bags_2

Home Index