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 bool_and : bool, bool -> bool logic bool_or : bool, bool -> bool logic bool_xor : bool, bool -> bool logic bool_not : bool -> bool axiom bool_and_def: (forall a:bool. (forall b:bool. ((bool_and(a, b) = true) <-> ((a = true) and (b = true))))) axiom bool_or_def: (forall a:bool. (forall b:bool. ((bool_or(a, b) = true) <-> ((a = true) or (b = true))))) axiom bool_xor_def: (forall a:bool. (forall b:bool. ((bool_xor(a, b) = true) <-> (a <> b)))) axiom bool_not_def: (forall a:bool. ((bool_not(a) = true) <-> (a = false))) logic ite : bool, 'a1, 'a1 -> 'a1 axiom ite_true: (forall x:'a1. (forall y:'a1. (ite(true, x, y) = x))) axiom ite_false: (forall x:'a1. (forall y:'a1. (ite(false, x, y) = y))) logic add_int : int, int -> int logic sub_int : int, int -> int logic mul_int : int, int -> int logic div_int : int, int -> int logic mod_int : int, int -> int logic neg_int : int -> int 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 lt_int_bool : int, int -> bool logic le_int_bool : int, int -> bool logic gt_int_bool : int, int -> bool logic ge_int_bool : int, int -> bool logic eq_int_bool : int, int -> bool logic neq_int_bool : int, int -> bool axiom lt_int_bool_axiom: (forall x:int. (forall y:int. ((lt_int_bool(x, y) = true) <-> (x < y)))) axiom le_int_bool_axiom: (forall x:int. (forall y:int. ((le_int_bool(x, y) = true) <-> (x <= y)))) axiom gt_int_bool_axiom: (forall x:int. (forall y:int. ((gt_int_bool(x, y) = true) <-> (x > y)))) axiom ge_int_bool_axiom: (forall x:int. (forall y:int. ((ge_int_bool(x, y) = true) <-> (x >= y)))) axiom eq_int_bool_axiom: (forall x:int. (forall y:int. ((eq_int_bool(x, y) = true) <-> (x = y)))) axiom neq_int_bool_axiom: (forall x:int. (forall y:int. ((neq_int_bool(x, y) = true) <-> (x <> y)))) logic add_real : real, real -> real logic sub_real : real, real -> real logic mul_real : real, real -> real logic div_real : real, real -> real logic pow_real : real, real -> real logic neg_real : real -> real logic abs_real : real -> real logic sqrt_real : real -> real logic real_of_int : int -> real logic int_of_real : real -> int logic lt_real : real, real -> prop logic le_real : real, real -> prop logic gt_real : real, real -> prop logic ge_real : real, real -> prop logic eq_real : real, real -> prop logic neq_real : real, real -> prop logic lt_real_bool : real, real -> bool logic le_real_bool : real, real -> bool logic gt_real_bool : real, real -> bool logic ge_real_bool : real, real -> bool logic eq_real_bool : real, real -> bool logic neq_real_bool : real, real -> bool axiom lt_real_bool_axiom: (forall x:real. (forall y:real. ((lt_real_bool(x, y) = true) <-> (x < y)))) axiom le_real_bool_axiom: (forall x:real. (forall y:real. ((le_real_bool(x, y) = true) <-> (x <= y)))) axiom gt_real_bool_axiom: (forall x:real. (forall y:real. ((gt_real_bool(x, y) = true) <-> (x > y)))) axiom ge_real_bool_axiom: (forall x:real. (forall y:real. ((ge_real_bool(x, y) = true) <-> (x >= y)))) axiom eq_real_bool_axiom: (forall x:real. (forall y:real. ((eq_real_bool(x, y) = true) <-> (x = y)))) axiom neq_real_bool_axiom: (forall x:real. (forall y:real. ((neq_real_bool(x, y) = true) <-> (x <> y)))) logic int_max : int, int -> int logic int_min : int, int -> int logic real_max : real, real -> real logic real_min : real, real -> real predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b)) logic access : 'a1 farray, int -> 'a1 logic update : 'a1 farray, int, 'a1 -> 'a1 farray axiom access_update: (forall a:'a1 farray. (forall i:int. (forall v:'a1. (access(update(a, i, v), i) = v)))) axiom access_update_neq: (forall a:'a1 farray. (forall i:int. (forall j:int. (forall v:'a1. ((i <> j) -> (access(update(a, i, v), j) = access(a, j))))))) logic array_length : 'a1 farray -> int predicate sorted_array(t: int farray, i: int, j: int) = (forall k1:int. (forall k2:int. ((((i <= k1) and (k1 <= k2)) and (k2 <= j)) -> (access(t, k1) <= access(t, k2))))) predicate exchange(a1: 'a1 farray, a2: 'a1 farray, i: int, j: int) = ((array_length(a1) = array_length(a2)) and ((access(a1, i) = access(a2, j)) and ((access(a2, i) = access(a1, j)) and (forall k:int. (((k <> i) and (k <> j)) -> (access(a1, k) = access(a2, k))))))) logic permut : 'a1 farray, 'a1 farray, int, int -> prop axiom permut_refl: (forall t:'a1 farray. (forall l:int. (forall u:int. permut(t, t, l, u)))) axiom permut_sym: (forall t1:'a1 farray. (forall t2:'a1 farray. (forall l:int. (forall u:int. (permut(t1, t2, l, u) -> permut(t2, t1, l, u)))))) axiom permut_trans: (forall t1:'a1 farray. (forall t2:'a1 farray. (forall t3:'a1 farray. (forall l:int. (forall u:int. (permut(t1, t2, l, u) -> (permut(t2, t3, l, u) -> permut(t1, t3, l, u)))))))) axiom permut_exchange: (forall a1:'a1 farray. (forall a2:'a1 farray. (forall l:int. (forall u:int. (forall i:int. (forall j:int. (((l <= i) and (i <= u)) -> (((l <= j) and (j <= u)) -> (exchange(a1, a2, i, j) -> permut(a1, a2, l, u)))))))))) axiom exchange_upd: (forall a:'a1 farray. (forall i:int. (forall j:int. exchange(a, update(update(a, i, access(a, j)), j, access(a, i)), i, j)))) axiom permut_weakening: (forall a1:'a1 farray. (forall a2:'a1 farray. (forall l1:int. (forall r1:int. (forall l2:int. (forall r2:int. ((((l1 <= l2) and (l2 <= r2)) and (r2 <= r1)) -> (permut(a1, a2, l2, r2) -> permut(a1, a2, l1, r1))))))))) axiom permut_eq: (forall a1:'a1 farray. (forall a2:'a1 farray. (forall l:int. (forall u:int. ((l <= u) -> (permut(a1, a2, l, u) -> (forall i:int. (((i < l) or (u < i)) -> (access(a2, i) = access(a1, i)))))))))) predicate permutation(a1: 'a1 farray, a2: 'a1 farray) = permut(a1, a2, 0, (array_length(a1) - 1)) axiom array_length_update: (forall a:'a1 farray. (forall i:int. (forall v:'a1. (array_length(update(a, i, v)) = array_length(a))))) axiom permut_array_length: (forall a1:'a1 farray. (forall a2:'a1 farray. (forall l:int. (forall u:int. (permut(a1, a2, l, u) -> (array_length(a1) = array_length(a2))))))) goal swap1_po_1: forall x0:int. forall y:int. forall x:int. (x = y) -> forall y0:int. (y0 = x0) -> ((x = y) and (y0 = x0)) goal swap2_po_1: forall x0:int. forall y:int. forall x:int. (x = y) -> forall y0:int. (y0 = x0) -> ((x = y) and (y0 = x0)) goal swap3_po_1: forall a0:int. forall b:int. forall a:int. (a = b) -> forall b0:int. (b0 = a0) -> ((a = b) and (b0 = a0)) goal call_swap3_y_x_po_1: forall x0:int. forall y0:int. forall x:int. forall y:int. ((y = x0) and (x = y0)) -> ((x = y0) and (y = x0)) goal swap4_po_1: forall a:int. forall b:int. forall tmp:int. (tmp = a) -> forall a0:int. (a0 = b) -> forall b0:int. (b0 = tmp) -> ((a0 = b) and (b0 = a)) goal call_swap4_x_y_po_1: forall x:int. forall y:int. (x = 3) -> forall x0:int. forall y0:int. ((x0 = y) and (y0 = x)) -> (y0 = 3) goal call_swap4_y_x_po_1: forall x:int. forall y:int. (x = 3) -> forall x0:int. forall y0:int. ((y0 = x) and (x0 = y)) -> (y0 = 3)