test-smoke-detector.why 304 Bytes
Newer Older
1
theory T
2
  use int.Int
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

function f (x : int) : int = x + 1

goal G1_true : forall x : int. f x - 1 = x

goal G2_false : forall x : int. f x = x

axiom A_false : forall x : int. f x = x

goal G1W : forall x : int. f x - 1 = x

goal G2W : forall x : int. f x = x

goal G3W : forall x : int. f x = 2*x

end