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)