Step * of Lemma bag-remove-trivial

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bs bs ∈ bag(T) supposing ¬x ↓∈ bs
BY
(Auto
   THEN RepUR ``bag-remove`` 0
   THEN RWO "bag-filter-trivial2" 0
   THEN Auto
   THEN AllPushDown
   THEN ParallelOp -3
   THEN Assert ⌜y ∈ T⌝⋅
   THEN Auto
   THEN Unfold `deq` 2
   THEN DVarSets
   THEN Auto) }


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    bs  -  x  =  bs  supposing  \mneg{}x  \mdownarrow{}\mmember{}  bs


By


Latex:
(Auto
  THEN  RepUR  ``bag-remove``  0
  THEN  RWO  "bag-filter-trivial2"  0
  THEN  Auto
  THEN  AllPushDown
  THEN  ParallelOp  -3
  THEN  Assert  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Unfold  `deq`  2
  THEN  DVarSets
  THEN  Auto)




Home Index