mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
33 lines
429 B
Plaintext
33 lines
429 B
Plaintext
|
|
theory Th1
|
|
use set.FsetInt
|
|
(* proved with vampire 0.6 and eprover 1.4 *)
|
|
lemma l_false : false
|
|
end
|
|
|
|
|
|
theory Th2
|
|
use set.FsetInt
|
|
|
|
function integer : fset int
|
|
lemma mem_integer: forall x:int. mem x integer
|
|
|
|
goal foo : false
|
|
|
|
end
|
|
|
|
|
|
theory Th3
|
|
|
|
use int.Int
|
|
|
|
type set 'a
|
|
|
|
function f (set int) : int
|
|
function g (set int) : int
|
|
axiom axiom1: forall s: set int, x: int. f s <= x <= g s
|
|
|
|
goal foo : false
|
|
|
|
end
|