mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
15 lines
256 B
Plaintext
15 lines
256 B
Plaintext
|
|
theory T
|
|
|
|
use bool.Bool
|
|
use int.Int
|
|
use list.List
|
|
use list.Length
|
|
use list.Nth
|
|
|
|
|
|
goal G : forall l: list 'a. length l >= 3 -> exists i j:int, x:'a. i <> j /\ nth i l = Some x /\ nth j l = Some x
|
|
|
|
goal g1: forall x:int. x >= 0 -> -x <= 0
|
|
|
|
end |