[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem Butmin
⊦ s ≠ ∅ → s.butmin = s -- s.min
Type: An axiom
Validity: The proof is valid.
Features: localsimp, kodkodaxstrong,
Comment:
Used by:
bm-shift
,
bmin-bin
,
bmin-bls
,
bmin-bneq
,
bmin-del
,
bmin-del-01
,
bmin-del-02
,
bmin-del-03
,
bmin-del-04
,
bmin-del-05
,
bmin-eq
,
bmin-eq-01
,
bmin-f
,
bmin-in-01
,
bmin-in-03
,
bmin-in-04
,
bmin-intempty
,
bmin-min
,
bmin-nin
,
bmin-nin-01
,
bmin-one-01
,
bmin-one-02
,
bmin-one-03
,
bmin-size
,
bmin-size-01
,
bmin-size-02
,
bmin-sub
,
bmin-sub-03
,
bmin-sub-04
,
bmin-sub-05
,
bminmin
,
butmin-in
,
butmin-ins
,
butmin-ins-01
,
butminempty-sizeone
,
max-bmin
,
minmax
,
minmax-01
,
Used by units in proved state:
Proof exists?: No