some (\xs -> issorted xs && equals (elementsof xs) emptybag)
===[unfold + simplification (step 1)
some
(\xs ->
issorted xs &&
equals
(case xs of
[] -> emptybag
x : b -> nonemptybag x (elementsof b)
)
emptybag
)
===[tactic simplify (step 2)
some
(\xs ->
case xs of
[] -> issorted [] && equals emptybag emptybag
x : b ->
issorted (x : b) &&
equals (nonemptybag x (elementsof b)) emptybag
)
===[apply rule general.thy/reflexivity (step 3)
some
(\xs ->
case xs of
[] -> issorted [] && True
x : b ->
issorted (x : b) &&
equals (nonemptybag x (elementsof b)) emptybag
)
===[apply catalog bag.thy + simplification (step 4)
some
(\xs ->
case xs of
[] -> issorted [] && True
x : b -> issorted (x : b) && False
)
===[tactic solve (step 5)
[]