[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 52 from proof max-ordered (
previous step
)
max(x2 + x0) = max(x2), ordered≤(x0), x1 ⊑ x0, ∀ x, x3. max(x2 + x) = max(x2) ∧ ordered≤(x) ∧ x3 ⊑ x → max(x2 + x3) = max(x2) ⊦ max(x2 + x1) = max(x2), x2 + x1 = [], x2 = [], x2 + x0 = [], max(x2 + x1) < a, max(x2) < a
Heuristic quantifier closing applied rule all left
And closed the goal!
Rule argument
pos: left 4 terms: x0, x1
Additional information
Used terms: x0, x1