mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
11 lines
148 B
Plaintext
11 lines
148 B
Plaintext
|
|
|
|
theory T
|
|
|
|
use real.Real
|
|
use real.MinMax
|
|
|
|
goal g: forall e p: real.
|
|
(2.0 * e + p + max e p) / 4.0 = max ((e+p)/2.0) ((3.0*e+p)/4.0)
|
|
|
|
end |