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)