[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
,
Proof step 3 from proof min-empty (
previous step
)
mon<([]) → ([] = [] ⊃ min([], n) = 0 ;(# [] ≠ ∞ ∧ ([])[(# []).n - 1] < n ⊃ min([], n) = (# []).n ;⌜min([], n)⌝ < # [] ∧ n ≤ ([])[min([], n)] ∧ (∀ m. ⌜m⌝ < # [] ∧ n ≤ ([])[m] → min([], n) ≤ m) ) ) ⊦ min([], n) = 0
Heuristic simplifier applied rule simplifier
And obtained the following new goals
Proof step 4
:
⊦ min([], n) = 0, mon<([])
Rule argument
Additional information