8df1e20e7d
- Rebase Makefile.in patch. - Fix(?) test result. - No libdir/frama-c directory is created any more.
41 lines
723 B
Text
41 lines
723 B
Text
logic eq_unit : unit, unit -> prop
|
|
|
|
logic neq_unit : unit, unit -> prop
|
|
|
|
logic eq_bool : bool, bool -> prop
|
|
|
|
logic neq_bool : bool, bool -> prop
|
|
|
|
logic lt_int : int, int -> prop
|
|
|
|
logic le_int : int, int -> prop
|
|
|
|
logic gt_int : int, int -> prop
|
|
|
|
logic ge_int : int, int -> prop
|
|
|
|
logic eq_int : int, int -> prop
|
|
|
|
logic neq_int : int, int -> prop
|
|
|
|
logic add_int : int, int -> int
|
|
|
|
logic sub_int : int, int -> int
|
|
|
|
logic mul_int : int, int -> int
|
|
|
|
logic neg_int : int -> int
|
|
|
|
predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
|
|
|
|
logic min : int, int -> int
|
|
|
|
axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
|
|
|
|
goal f_po_1:
|
|
forall n:int.
|
|
forall r0:int.
|
|
forall r:int.
|
|
(r = min(r0, n)) ->
|
|
(r <= r0)
|
|
|