mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
11 lines
125 B
Plaintext
11 lines
125 B
Plaintext
|
|
goal g41:
|
|
forall x,y,z:int.
|
|
x > 3 ->
|
|
y > 0 ->
|
|
z > 0 ->
|
|
y > z ->
|
|
z = ((x / y) + y) / 2 ->
|
|
z > 1 and y > 2
|
|
|