[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 max-del1-01
⊦ ints ≠ [] → (max(ints) < max(ints -1l i) ↔ ints = i ' ∧ i < 0)
Type: A user defined theorem
Validity: The proof is valid.
Features: simp, localsimp,
Comment:
Used by:
max-del1
,
max-perm
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 5
Proof steps: 12
Used lemmas:
max-rec
,
max-app
,
max-app-ls
,
max-empty
,
max-one
,
Used spec theorems:
list-del
/intlista/
del1-n
int-min
/
Max-left
Used simplifier rules:
list
/intlista/
e-01
list
/intlista/
c
list-del
/intlista/
del1-y
int-abs
/
zero-gels-01
list
/intlista/
c-03
list-del
/intlista/
del1-e
int-min
/
max-01
list
/intlista/
one-01
list
/intlista/
e
list
/intlista/
a
list-del
/intlista/
one-01
list
/intlista/
app
list-del
/intlista/
del1-empty
oelem
/intlista/
irreflexivity
int-min
/
max-c
int-min
/
max-a
int-min
/
Max-right