;; DO NOT EDIT BELOW THIS LINE

;;(BG_PUSH
;; ;; Why axiom union_sym
;; (FORALL (z |z'|) (EQ (zunion z |z'|) (zunion |z'| z))))

;;(BG_PUSH
;; ;; Why axiom union_assoc
;; (FORALL (z r s) (EQ (zunion (zunion z r) s) (zunion z (zunion r s)))))

;;(BG_PUSH
;; ;; Why axiom inc_sub_zone
;; (FORALL (z |z'|)
;; (EQ (included
;; (zunion (zunion z |z'|) (zunion |z'| z)) (zunion |z'| z)) |@true|)))

(BG_PUSH (NEQ |@true| |@false|))

(DEFPRED (zwf_zero a b) (AND (<= 0 b) (< a b)))

(BG_PUSH
 ;; Why axiom bool_and_def
 (FORALL (a b)
 (IFF (EQ (bool_and a b) |@true|) (AND (EQ a |@true|) (EQ b |@true|)))))

(BG_PUSH
 ;; Why axiom bool_or_def
 (FORALL (a b)
 (IFF (EQ (bool_or a b) |@true|) (OR (EQ a |@true|) (EQ b |@true|)))))

(BG_PUSH
 ;; Why axiom bool_xor_def
 (FORALL (a b) (IFF (EQ (bool_xor a b) |@true|) (NEQ a b))))

(BG_PUSH
 ;; Why axiom bool_not_def
 (FORALL (a) (IFF (EQ (bool_not a) |@true|) (EQ a |@false|))))

(BG_PUSH
 ;; Why axiom ite_true
 (FORALL (x y) (EQ (ite |@true| x y) x)))

(BG_PUSH
 ;; Why axiom ite_false
 (FORALL (x y) (EQ (ite |@false| x y) y)))

(BG_PUSH
 ;; Why axiom lt_int_bool_axiom
 (FORALL (x y) (IFF (EQ (lt_int_bool x y) |@true|) (< x y))))

(BG_PUSH
 ;; Why axiom le_int_bool_axiom
 (FORALL (x y) (IFF (EQ (le_int_bool x y) |@true|) (<= x y))))

(BG_PUSH
 ;; Why axiom gt_int_bool_axiom
 (FORALL (x y) (IFF (EQ (gt_int_bool x y) |@true|) (> x y))))

(BG_PUSH
 ;; Why axiom ge_int_bool_axiom
 (FORALL (x y) (IFF (EQ (ge_int_bool x y) |@true|) (>= x y))))

(BG_PUSH
 ;; Why axiom eq_int_bool_axiom
 (FORALL (x y) (IFF (EQ (eq_int_bool x y) |@true|) (EQ x y))))

(BG_PUSH
 ;; Why axiom neq_int_bool_axiom
 (FORALL (x y) (IFF (EQ (neq_int_bool x y) |@true|) (NEQ x y))))

(BG_PUSH
 ;; Why axiom abs_int_pos
 (FORALL (x) (IMPLIES (>= x 0) (EQ (abs_int x) x))))

(BG_PUSH
 ;; Why axiom abs_int_neg
 (FORALL (x) (IMPLIES (<= x 0) (EQ (abs_int x) (- 0 x)))))

(BG_PUSH
 ;; Why axiom int_max_is_ge
 (FORALL (x y) (AND (>= (int_max x y) x) (>= (int_max x y) y))))

(BG_PUSH
 ;; Why axiom int_max_is_some
 (FORALL (x y) (OR (EQ (int_max x y) x) (EQ (int_max x y) y))))

(BG_PUSH
 ;; Why axiom int_min_is_le
 (FORALL (x y) (AND (<= (int_min x y) x) (<= (int_min x y) y))))

(BG_PUSH
 ;; Why axiom int_min_is_some
 (FORALL (x y) (OR (EQ (int_min x y) x) (EQ (int_min x y) y))))

(BG_PUSH
 ;; Why axiom real_of_int_zero
 (EQ (real_of_int 0) real_constant_0_0e))

(BG_PUSH
 ;; Why axiom real_of_int_one
 (EQ (real_of_int 1) real_constant_1_0e))

(BG_PUSH
 ;; Why axiom real_of_int_add
 (FORALL (x y)
 (EQ (real_of_int (+ x y)) (real_add (real_of_int x) (real_of_int y)))))

(BG_PUSH
 ;; Why axiom real_of_int_sub
 (FORALL (x y)
 (EQ (real_of_int (- x y)) (real_sub (real_of_int x) (real_of_int y)))))

(BG_PUSH
 ;; Why axiom truncate_down_pos
 (FORALL (x)
 (IMPLIES (EQ (ge_real x real_constant_0_0e) |@true|)
 (AND (EQ (le_real (real_of_int (truncate_real_to_int x)) x) |@true|)
 (EQ (lt_real x (real_of_int (+ (truncate_real_to_int x) 1))) |@true|)))))

(BG_PUSH
 ;; Why axiom truncate_up_neg
 (FORALL (x)
 (IMPLIES (EQ (le_real x real_constant_0_0e) |@true|)
 (AND (EQ (lt_real (real_of_int (- (truncate_real_to_int x) 1)) x) |@true|)
 (EQ (le_real x (real_of_int (truncate_real_to_int x))) |@true|)))))

(BG_PUSH
 ;; Why axiom lt_real_bool_axiom
 (FORALL (x y)
 (IFF (EQ (lt_real_bool x y) |@true|) (EQ (lt_real x y) |@true|))))

(BG_PUSH
 ;; Why axiom le_real_bool_axiom
 (FORALL (x y)
 (IFF (EQ (le_real_bool x y) |@true|) (EQ (le_real x y) |@true|))))

(BG_PUSH
 ;; Why axiom gt_real_bool_axiom
 (FORALL (x y)
 (IFF (EQ (gt_real_bool x y) |@true|) (EQ (gt_real x y) |@true|))))

(BG_PUSH
 ;; Why axiom ge_real_bool_axiom
 (FORALL (x y)
 (IFF (EQ (ge_real_bool x y) |@true|) (EQ (ge_real x y) |@true|))))

(BG_PUSH
 ;; Why axiom eq_real_bool_axiom
 (FORALL (x y) (IFF (EQ (eq_real_bool x y) |@true|) (EQ x y))))

(BG_PUSH
 ;; Why axiom neq_real_bool_axiom
 (FORALL (x y) (IFF (EQ (neq_real_bool x y) |@true|) (NEQ x y))))

(BG_PUSH
 ;; Why axiom real_max_is_ge
 (FORALL (x y)
 (AND (EQ (ge_real (real_max x y) x) |@true|)
 (EQ (ge_real (real_max x y) y) |@true|))))

(BG_PUSH
 ;; Why axiom real_max_is_some
 (FORALL (x y) (OR (EQ (real_max x y) x) (EQ (real_max x y) y))))

(BG_PUSH
 ;; Why axiom real_min_is_le
 (FORALL (x y)
 (AND (EQ (le_real (real_min x y) x) |@true|)
 (EQ (le_real (real_min x y) y) |@true|))))

(BG_PUSH
 ;; Why axiom real_min_is_some
 (FORALL (x y) (OR (EQ (real_min x y) x) (EQ (real_min x y) y))))

(BG_PUSH
 ;; Why axiom sqr_real_def
 (FORALL (x) (EQ (sqr_real x) (real_mul x x))))

(BG_PUSH
 ;; Why axiom sqrt_pos
 (FORALL (x)
 (IMPLIES (EQ (ge_real x real_constant_0_0e) |@true|)
 (EQ (ge_real (real_sqrt x) real_constant_0_0e) |@true|))))

(BG_PUSH
 ;; Why axiom sqrt_sqr
 (FORALL (x)
 (IMPLIES (EQ (ge_real x real_constant_0_0e) |@true|)
 (EQ (sqr_real (real_sqrt x)) x))))

(BG_PUSH
 ;; Why axiom sqr_sqrt
 (FORALL (x)
 (IMPLIES (EQ (ge_real x real_constant_0_0e) |@true|)
 (EQ (real_sqrt (real_mul x x)) x))))

(BG_PUSH
 ;; Why axiom abs_real_pos
 (FORALL (x)
 (IMPLIES (EQ (ge_real x real_constant_0_0e) |@true|) (EQ (real_abs x) x))))

(BG_PUSH
 ;; Why axiom abs_real_neg
 (FORALL (x)
 (IMPLIES (EQ (le_real x real_constant_0_0e) |@true|)
 (EQ (real_abs x) (real_neg x)))))

(BG_PUSH
 ;; Why axiom log_exp
 (FORALL (x) (EQ (log (exp x)) x)))

(BG_PUSH
 ;; Why axiom exp_log
 (FORALL (x)
 (IMPLIES (EQ (gt_real x real_constant_0_0e) |@true|) (EQ (exp (log x)) x))))

(BG_PUSH
 ;; Why axiom prod_pos
 (FORALL (x y)
 (AND
 (IMPLIES
 (AND (EQ (gt_real x real_constant_0_0e) |@true|)
 (EQ (gt_real y real_constant_0_0e) |@true|))
 (EQ (gt_real (real_mul x y) real_constant_0_0e) |@true|))
 (IMPLIES
 (AND (EQ (lt_real x real_constant_0_0e) |@true|)
 (EQ (lt_real y real_constant_0_0e) |@true|))
 (EQ (gt_real (real_mul x y) real_constant_0_0e) |@true|)))))

(BG_PUSH
 ;; Why axiom abs_minus
 (FORALL (x) (EQ (real_abs (real_neg x)) (real_abs x))))

(BG_PUSH
 ;; Why axiom access_update
 (FORALL (a i v) (EQ (access (update a i v) i) v)))

(BG_PUSH
 ;; Why axiom access_update_neq
 (FORALL (a i j v)
 (IMPLIES (NEQ i j) (EQ (access (update a i v) j) (access a j))))

 (FORALL (i j)
 (IMPLIES (NEQ i j)
 (FORALL (a v) (EQ (access (update a i v) j) (access a j))))))

(DEFPRED (sorted_array t i j)
  (FORALL (k1 k2)
  (IMPLIES (AND (AND (<= i k1) (<= k1 k2)) (<= k2 j))
  (<= (access t k1) (access t k2)))))

(DEFPRED (exchange a1 a2 i j)
  (AND (EQ (array_length a1) (array_length a2))
  (AND (EQ (access a1 i) (access a2 j))
  (AND (EQ (access a2 i) (access a1 j))
  (FORALL (k)
  (IMPLIES (AND (NEQ k i) (NEQ k j)) (EQ (access a1 k) (access a2 k))))))))

(BG_PUSH
 ;; Why axiom permut_refl
 (FORALL (t l u) (EQ (permut t t l u) |@true|)))

(BG_PUSH
 ;; Why axiom permut_sym
 (FORALL (t1 t2 l u)
 (IMPLIES (EQ (permut t1 t2 l u) |@true|) (EQ (permut t2 t1 l u) |@true|))))

(BG_PUSH
 ;; Why axiom permut_trans
 (FORALL (t1 t2 t3 l u)
 (IMPLIES (EQ (permut t1 t2 l u) |@true|)
 (IMPLIES (EQ (permut t2 t3 l u) |@true|) (EQ (permut t1 t3 l u) |@true|))))

 (FORALL (t1 t2 l u)
 (IMPLIES (EQ (permut t1 t2 l u) |@true|)
 (FORALL (t3)
 (IMPLIES (EQ (permut t2 t3 l u) |@true|) (EQ (permut t1 t3 l u) |@true|))))))

(BG_PUSH
 ;; Why axiom permut_exchange
 (FORALL (a1 a2 l u i j)
 (IMPLIES (AND (<= l i) (<= i u))
 (IMPLIES (AND (<= l j) (<= j u))
 (IMPLIES (exchange a1 a2 i j) (EQ (permut a1 a2 l u) |@true|)))))

 (FORALL (l u i)
 (IMPLIES (AND (<= l i) (<= i u))
 (FORALL (j)
 (IMPLIES (AND (<= l j) (<= j u))
 (FORALL (a1 a2)
 (IMPLIES (exchange a1 a2 i j) (EQ (permut a1 a2 l u) |@true|))))))))

(BG_PUSH
 ;; Why axiom exchange_upd
 (FORALL (a i j)
 (exchange a (update (update a i (access a j)) j (access a i)) i j)))

(BG_PUSH
 ;; Why axiom permut_weakening
 (FORALL (a1 a2 l1 r1 l2 r2)
 (IMPLIES (AND (AND (<= l1 l2) (<= l2 r2)) (<= r2 r1))
 (IMPLIES (EQ (permut a1 a2 l2 r2) |@true|)
 (EQ (permut a1 a2 l1 r1) |@true|))))

 (FORALL (l1 r1 l2 r2)
 (IMPLIES (AND (AND (<= l1 l2) (<= l2 r2)) (<= r2 r1))
 (FORALL (a2 a1)
 (IMPLIES (EQ (permut a1 a2 l2 r2) |@true|)
 (EQ (permut a1 a2 l1 r1) |@true|))))))

(BG_PUSH
 ;; Why axiom permut_eq
 (FORALL (a1 a2 l u)
 (IMPLIES (<= l u)
 (IMPLIES (EQ (permut a1 a2 l u) |@true|)
 (FORALL (i) (IMPLIES (OR (< i l) (< u i)) (EQ (access a2 i) (access a1 i)))))))

 (FORALL (l u)
 (IMPLIES (<= l u)
 (FORALL (a2 a1)
 (IMPLIES (EQ (permut a1 a2 l u) |@true|)
 (FORALL (i) (IMPLIES (OR (< i l) (< u i)) (EQ (access a2 i) (access a1 i)))))))))

(DEFPRED (permutation a1 a2)
  (EQ (permut a1 a2 0 (- (array_length a1) 1)) |@true|))

(BG_PUSH
 ;; Why axiom array_length_update
 (FORALL (a i v) (EQ (array_length (update a i v)) (array_length a))))

(BG_PUSH
 ;; Why axiom permut_array_length
 (FORALL (a1 a2 l u)
 (IMPLIES (EQ (permut a1 a2 l u) |@true|)
 (EQ (array_length a1) (array_length a2)))))

(BG_PUSH
 ;; Why axiom math_div_mod
 (FORALL (x y)
 (IMPLIES (NEQ y 0) (EQ x (+ (* y (math_div x y)) (math_mod x y)))))

 (FORALL (y)
 (IMPLIES (NEQ y 0)
 (FORALL (x) (EQ x (+ (* y (math_div x y)) (math_mod x y)))))))

(BG_PUSH
 ;; Why axiom math_mod_bound
 (FORALL (x y)
 (IMPLIES (NEQ y 0)
 (AND (<= 0 (math_mod x y)) (< (math_mod x y) (abs_int y)))))

 (FORALL (y)
 (IMPLIES (NEQ y 0)
 (FORALL (x) (AND (<= 0 (math_mod x y)) (< (math_mod x y) (abs_int y)))))))

(BG_PUSH
 ;; Why axiom computer_div_mod
 (FORALL (x y)
 (IMPLIES (NEQ y 0) (EQ x (+ (* y (computer_div x y)) (computer_mod x y)))))

 (FORALL (y)
 (IMPLIES (NEQ y 0)
 (FORALL (x) (EQ x (+ (* y (computer_div x y)) (computer_mod x y)))))))

(BG_PUSH
 ;; Why axiom computer_div_bound
 (FORALL (x y)
 (IMPLIES (AND (>= x 0) (> y 0))
 (AND (<= 0 (computer_div x y)) (<= (computer_div x y) x)))))

(BG_PUSH
 ;; Why axiom computer_mod_bound
 (FORALL (x y)
 (IMPLIES (NEQ y 0) (< (abs_int (computer_mod x y)) (abs_int y))))

 (FORALL (y)
 (IMPLIES (NEQ y 0)
 (FORALL (x) (< (abs_int (computer_mod x y)) (abs_int y))))))

(BG_PUSH
 ;; Why axiom computer_mod_sign_pos
 (FORALL (x y) (IMPLIES (AND (>= x 0) (NEQ y 0)) (>= (computer_mod x y) 0))))

(BG_PUSH
 ;; Why axiom computer_mod_sign_neg
 (FORALL (x y) (IMPLIES (AND (<= x 0) (NEQ y 0)) (<= (computer_mod x y) 0))))

(BG_PUSH
 ;; Why axiom computer_rounds_toward_zero
 (FORALL (x y)
 (IMPLIES (NEQ y 0) (<= (abs_int (* (computer_div x y) y)) (abs_int x))))

 (FORALL (y)
 (IMPLIES (NEQ y 0)
 (FORALL (x) (<= (abs_int (* (computer_div x y) y)) (abs_int x))))))

(BG_PUSH
 ;; Why axiom positive_computer_div_div
 (FORALL (x y)
 (IMPLIES (> x 0) (IMPLIES (> y 0) (EQ (computer_div x y) (math_div x y)))))

 (FORALL (x)
 (IMPLIES (> x 0)
 (FORALL (y) (IMPLIES (> y 0) (EQ (computer_div x y) (math_div x y)))))))

(BG_PUSH
 ;; Why axiom singleton_def
 (FORALL (x) (EQ (member x (singleton x)) |@true|)))

(BG_PUSH
 ;; Why axiom singleton_eq
 (FORALL (x y) (IFF (EQ (member x (singleton y)) |@true|) (EQ x y))))

(BG_PUSH
 ;; Why axiom union_member
 (FORALL (x s1 s2)
 (IFF (EQ (member x (union s1 s2)) |@true|)
 (OR (EQ (member x s1) |@true|) (EQ (member x s2) |@true|)))))

(BG_PUSH
 ;; Why axiom union_of_empty
 (FORALL (x) (EQ (union x empty) x)))

(BG_PUSH
 ;; Why axiom inter_of_empty
 (FORALL (x) (EQ (inter x empty) empty)))

(BG_PUSH
 ;; Why axiom union_comm
 (FORALL (x y) (EQ (union x y) (union y x))))

(BG_PUSH
 ;; Why axiom inter_comm
 (FORALL (x y) (EQ (inter x y) (inter y x))))

(BG_PUSH
 ;; Why axiom inter_member
 (FORALL (x s1 s2)
 (IFF (EQ (member x (inter s1 s2)) |@true|)
 (AND (EQ (member x s1) |@true|) (EQ (member x s2) |@true|)))))

(BG_PUSH
 ;; Why axiom plus_int_member_1
 (FORALL (sa sb a b)
 (IMPLIES (EQ (member a sa) |@true|)
 (IMPLIES (EQ (member b sb) |@true|)
 (EQ (member (+ a b) (plus_int sa sb)) |@true|))))

 (FORALL (sa a)
 (IMPLIES (EQ (member a sa) |@true|)
 (FORALL (b sb)
 (IMPLIES (EQ (member b sb) |@true|)
 (EQ (member (+ a b) (plus_int sa sb)) |@true|))))))

(BG_PUSH
 ;; Why axiom plus_int_member_2
 (FORALL (sa sb c)
 (IMPLIES (EQ (member c (plus_int sa sb)) |@true|)
 (EXISTS (a)
 (EXISTS (b)
 (AND (EQ (member a sa) |@true|)
 (AND (EQ (member b sb) |@true|) (EQ c (+ a b)))))))))

(BG_PUSH
 ;; Why axiom subset_empty
 (FORALL (sa) (EQ (subset empty sa) |@true|)))

(BG_PUSH
 ;; Why axiom subset_sym
 (FORALL (sa) (EQ (subset sa sa) |@true|)))

(BG_PUSH
 ;; Why axiom subset_trans
 (FORALL (sa sb sc)
 (IMPLIES (EQ (subset sa sb) |@true|)
 (IMPLIES (EQ (subset sb sc) |@true|) (EQ (subset sa sc) |@true|))))

 (FORALL (sa sb)
 (IMPLIES (EQ (subset sa sb) |@true|)
 (FORALL (sc)
 (IMPLIES (EQ (subset sb sc) |@true|) (EQ (subset sa sc) |@true|))))))

(BG_PUSH
 ;; Why axiom subset_def
 (FORALL (sa sb)
 (IFF
 (FORALL (a) (IMPLIES (EQ (member a sa) |@true|) (EQ (member a sb) |@true|)))
 (EQ (subset sa sb) |@true|))))

(BG_PUSH
 ;; Why axiom range_def
 (FORALL (i j k)
 (IFF (AND (<= i k) (<= k j)) (EQ (member k (range i j)) |@true|))))

(BG_PUSH
 ;; Why axiom range_def1
 (FORALL (i j k)
 (IMPLIES (AND (<= i k) (<= k j)) (EQ (member k (range i j)) |@true|))))

(BG_PUSH
 ;; Why axiom range_def2
 (FORALL (i j k)
 (IMPLIES (EQ (member k (range i j)) |@true|) (AND (<= i k) (<= k j)))))

(BG_PUSH
 ;; Why axiom range_inf_def
 (FORALL (i k) (IFF (<= i k) (EQ (member k (range_inf i)) |@true|))))

(BG_PUSH
 ;; Why axiom range_sup_def
 (FORALL (j k) (IFF (<= k j) (EQ (member k (range_sup j)) |@true|))))

(BG_PUSH
 ;; Why axiom integers_set_def
 (FORALL (k) (IFF (>= k 0) (EQ (member k integers_set) |@true|))))

(BG_PUSH
 ;; Why axiom equiv_def
 (FORALL (s1 s2)
 (IFF
 (AND
 (FORALL (a) (IMPLIES (EQ (member a s1) |@true|) (EQ (member a s2) |@true|)))
 (FORALL (b) (IMPLIES (EQ (member b s2) |@true|) (EQ (member b s1) |@true|))))
 (EQ (equiv s1 s2) |@true|))))

(BG_PUSH
 ;; Why axiom equiv_refl
 (FORALL (s) (EQ (equiv s s) |@true|)))

(BG_PUSH
 ;; Why axiom equiv_sym
 (FORALL (s1 s2)
 (IMPLIES (EQ (equiv s1 s2) |@true|) (EQ (equiv s2 s1) |@true|))))

(BG_PUSH
 ;; Why axiom equiv_trans
 (FORALL (s1 s2 s3)
 (IMPLIES (EQ (equiv s1 s2) |@true|)
 (IMPLIES (EQ (equiv s2 s3) |@true|) (EQ (equiv s1 s3) |@true|))))

 (FORALL (s1 s2)
 (IMPLIES (EQ (equiv s1 s2) |@true|)
 (FORALL (s3)
 (IMPLIES (EQ (equiv s2 s3) |@true|) (EQ (equiv s1 s3) |@true|))))))

(DEFPRED (is_uint8 x) (AND (<= 0 x) (< x 256)))

(BG_PUSH
 ;; Why axiom as_uint8_def
 (FORALL (x) (is_uint8 (as_uint8 x))))

(BG_PUSH
 ;; Why axiom as_uint8_involve
 (FORALL (x) (EQ (as_uint8 (as_uint8 x)) (as_uint8 x))))

(BG_PUSH
 ;; Why axiom is_as_uint8
 (FORALL (x) (IMPLIES (is_uint8 x) (EQ (as_uint8 x) x))))

(DEFPRED (is_sint8 x) (AND (<= (- 0 128) x) (< x 128)))

(BG_PUSH
 ;; Why axiom as_sint8_def
 (FORALL (x) (is_sint8 (as_sint8 x))))

(BG_PUSH
 ;; Why axiom as_sint8_involve
 (FORALL (x) (EQ (as_sint8 (as_sint8 x)) (as_sint8 x))))

(BG_PUSH
 ;; Why axiom is_as_sint8
 (FORALL (x) (IMPLIES (is_sint8 x) (EQ (as_sint8 x) x))))

(DEFPRED (is_uint16 x) (AND (<= 0 x) (< x 65536)))

(BG_PUSH
 ;; Why axiom as_uint16_def
 (FORALL (x) (is_uint16 (as_uint16 x))))

(BG_PUSH
 ;; Why axiom as_uint16_involve
 (FORALL (x) (EQ (as_uint16 (as_uint16 x)) (as_uint16 x))))

(BG_PUSH
 ;; Why axiom is_as_uint16
 (FORALL (x) (IMPLIES (is_uint16 x) (EQ (as_uint16 x) x))))

(DEFPRED (is_sint16 x) (AND (<= (- 0 32768) x) (< x 32768)))

(BG_PUSH
 ;; Why axiom as_sint16_def
 (FORALL (x) (is_sint16 (as_sint16 x))))

(BG_PUSH
 ;; Why axiom as_sint16_involve
 (FORALL (x) (EQ (as_sint16 (as_sint16 x)) (as_sint16 x))))

(BG_PUSH
 ;; Why axiom is_as_sint16
 (FORALL (x) (IMPLIES (is_sint16 x) (EQ (as_sint16 x) x))))

(DEFPRED (is_uint32 x) (AND (<= 0 x) (< x constant_too_large_4294967296)))

(BG_PUSH
 ;; Why axiom as_uint32_def
 (FORALL (x) (is_uint32 (as_uint32 x))))

(BG_PUSH
 ;; Why axiom as_uint32_involve
 (FORALL (x) (EQ (as_uint32 (as_uint32 x)) (as_uint32 x))))

(BG_PUSH
 ;; Why axiom is_as_uint32
 (FORALL (x) (IMPLIES (is_uint32 x) (EQ (as_uint32 x) x))))

(DEFPRED (is_sint32 x)
  (AND (<= (- 0 constant_too_large_2147483648) x)
  (< x constant_too_large_2147483648)))

(BG_PUSH
 ;; Why axiom as_sint32_def
 (FORALL (x) (is_sint32 (as_sint32 x))))

(BG_PUSH
 ;; Why axiom as_sint32_involve
 (FORALL (x) (EQ (as_sint32 (as_sint32 x)) (as_sint32 x))))

(BG_PUSH
 ;; Why axiom is_as_sint32
 (FORALL (x) (IMPLIES (is_sint32 x) (EQ (as_sint32 x) x))))

(DEFPRED (is_uint64 x)
  (AND (<= 0 x) (< x constant_too_large_18446744073709551616)))

(BG_PUSH
 ;; Why axiom as_uint64_def
 (FORALL (x) (is_uint64 (as_uint64 x))))

(BG_PUSH
 ;; Why axiom as_uint64_involve
 (FORALL (x) (EQ (as_uint64 (as_uint64 x)) (as_uint64 x))))

(BG_PUSH
 ;; Why axiom is_as_uint64
 (FORALL (x) (IMPLIES (is_uint64 x) (EQ (as_uint64 x) x))))

(DEFPRED (is_sint64 x)
  (AND (<= (- 0 constant_too_large_9223372036854775808) x)
  (< x constant_too_large_9223372036854775808)))

(BG_PUSH
 ;; Why axiom as_sint64_def
 (FORALL (x) (is_sint64 (as_sint64 x))))

(BG_PUSH
 ;; Why axiom as_sint64_involve
 (FORALL (x) (EQ (as_sint64 (as_sint64 x)) (as_sint64 x))))

(BG_PUSH
 ;; Why axiom is_as_sint64
 (FORALL (x) (IMPLIES (is_sint64 x) (EQ (as_sint64 x) x))))

(BG_PUSH
 ;; Why axiom as_float16_def
 (FORALL (x) (EQ (is_float16 (as_float16 x)) |@true|)))

(BG_PUSH
 ;; Why axiom as_float16_involve
 (FORALL (x) (EQ (as_float16 (as_float16 x)) (as_float16 x))))

(BG_PUSH
 ;; Why axiom is_as_float16
 (FORALL (x) (IMPLIES (EQ (is_float16 x) |@true|) (EQ (as_float16 x) x))))

(BG_PUSH
 ;; Why axiom as_float32_def
 (FORALL (x) (EQ (is_float32 (as_float32 x)) |@true|)))

(BG_PUSH
 ;; Why axiom as_float32_involve
 (FORALL (x) (EQ (as_float32 (as_float32 x)) (as_float32 x))))

(BG_PUSH
 ;; Why axiom is_as_float32
 (FORALL (x) (IMPLIES (EQ (is_float32 x) |@true|) (EQ (as_float32 x) x))))

(BG_PUSH
 ;; Why axiom as_float64_def
 (FORALL (x) (EQ (is_float64 (as_float64 x)) |@true|)))

(BG_PUSH
 ;; Why axiom as_float64_involve
 (FORALL (x) (EQ (as_float64 (as_float64 x)) (as_float64 x))))

(BG_PUSH
 ;; Why axiom is_as_float64
 (FORALL (x) (IMPLIES (EQ (is_float64 x) |@true|) (EQ (as_float64 x) x))))

(BG_PUSH
 ;; Why axiom as_float128_def
 (FORALL (x) (EQ (is_float128 (as_float128 x)) |@true|)))

(BG_PUSH
 ;; Why axiom as_float128_involve
 (FORALL (x) (EQ (as_float128 (as_float128 x)) (as_float128 x))))

(BG_PUSH
 ;; Why axiom is_as_float128
 (FORALL (x) (IMPLIES (EQ (is_float128 x) |@true|) (EQ (as_float128 x) x))))

(BG_PUSH
 ;; Why axiom is_uint8_of_data
 (FORALL (d) (is_uint8 (uint8_of_data d))))

(BG_PUSH
 ;; Why axiom uint8ofdata_dataofuint8
 (FORALL (x) (IMPLIES (is_uint8 x) (EQ (uint8_of_data (data_of_uint8 x)) x))))

(BG_PUSH
 ;; Why axiom is_sint8_of_data
 (FORALL (d) (is_sint8 (sint8_of_data d))))

(BG_PUSH
 ;; Why axiom sint8ofdata_dataofsint8
 (FORALL (x) (IMPLIES (is_sint8 x) (EQ (sint8_of_data (data_of_sint8 x)) x))))

(BG_PUSH
 ;; Why axiom is_uint16_of_data
 (FORALL (d) (is_uint16 (uint16_of_data d))))

(BG_PUSH
 ;; Why axiom uint16ofdata_dataofuint16
 (FORALL (x)
 (IMPLIES (is_uint16 x) (EQ (uint16_of_data (data_of_uint16 x)) x))))

(BG_PUSH
 ;; Why axiom is_sint16_of_data
 (FORALL (d) (is_sint16 (sint16_of_data d))))

(BG_PUSH
 ;; Why axiom sint16ofdata_dataofsint16
 (FORALL (x)
 (IMPLIES (is_sint16 x) (EQ (sint16_of_data (data_of_sint16 x)) x))))

(BG_PUSH
 ;; Why axiom is_uint32_of_data
 (FORALL (d) (is_uint32 (uint32_of_data d))))

(BG_PUSH
 ;; Why axiom uint32ofdata_dataofuint32
 (FORALL (x)
 (IMPLIES (is_uint32 x) (EQ (uint32_of_data (data_of_uint32 x)) x))))

(BG_PUSH
 ;; Why axiom is_sint32_of_data
 (FORALL (d) (is_sint32 (sint32_of_data d))))

(BG_PUSH
 ;; Why axiom sint32ofdata_dataofsint32
 (FORALL (x)
 (IMPLIES (is_sint32 x) (EQ (sint32_of_data (data_of_sint32 x)) x))))

(BG_PUSH
 ;; Why axiom is_uint64_of_data
 (FORALL (d) (is_uint64 (uint64_of_data d))))

(BG_PUSH
 ;; Why axiom uint64ofdata_dataofuint64
 (FORALL (x)
 (IMPLIES (is_uint64 x) (EQ (uint64_of_data (data_of_uint64 x)) x))))

(BG_PUSH
 ;; Why axiom is_sint64_of_data
 (FORALL (d) (is_sint64 (sint64_of_data d))))

(BG_PUSH
 ;; Why axiom sint64ofdata_dataofsint64
 (FORALL (x)
 (IMPLIES (is_sint64 x) (EQ (sint64_of_data (data_of_sint64 x)) x))))

(BG_PUSH
 ;; Why axiom is_float16_of_data
 (FORALL (d) (EQ (is_float16 (float16_of_data d)) |@true|)))

(BG_PUSH
 ;; Why axiom float16ofdata_dataoffloat16
 (FORALL (x)
 (IMPLIES (EQ (is_float16 x) |@true|)
 (EQ (float16_of_data (data_of_float16 x)) x))))

(BG_PUSH
 ;; Why axiom is_float32_of_data
 (FORALL (d) (EQ (is_float32 (float32_of_data d)) |@true|)))

(BG_PUSH
 ;; Why axiom float32ofdata_dataoffloat32
 (FORALL (x)
 (IMPLIES (EQ (is_float32 x) |@true|)
 (EQ (float32_of_data (data_of_float32 x)) x))))

(BG_PUSH
 ;; Why axiom is_float64_of_data
 (FORALL (d) (EQ (is_float64 (float64_of_data d)) |@true|)))

(BG_PUSH
 ;; Why axiom float64ofdata_dataoffloat64
 (FORALL (x)
 (IMPLIES (EQ (is_float64 x) |@true|)
 (EQ (float64_of_data (data_of_float64 x)) x))))

(BG_PUSH
 ;; Why axiom is_float128_of_data
 (FORALL (d) (EQ (is_float128 (float128_of_data d)) |@true|)))

(BG_PUSH
 ;; Why axiom float128ofdata_dataoffloat128
 (FORALL (x)
 (IMPLIES (EQ (is_float128 x) |@true|)
 (EQ (float128_of_data (data_of_float128 x)) x))))

(BG_PUSH
 ;; Why axiom set_range_def
 (FORALL (t rg k i)
 (IMPLIES (NOT (EQ (member i rg) |@true|))
 (EQ (access (set_range_index t rg k) i) (access t i))))

 (FORALL (rg i)
 (IMPLIES (NOT (EQ (member i rg) |@true|))
 (FORALL (t k) (EQ (access (set_range_index t rg k) i) (access t i))))))

(BG_PUSH
 ;; Why axiom addr_def
 (FORALL (a b d)
 (IMPLIES (EQ (addr b d) a) (AND (EQ (base a) b) (EQ (offset a) d)))))

(BG_PUSH
 ;; Why axiom addr_id
 (FORALL (p) (EQ (addr (base p) (offset p)) p)))

(BG_PUSH
 ;; Why axiom minus_addr_def
 (FORALL (a b)
 (IMPLIES (EQ (base a) (base b))
 (EQ (minus_addr a b) (- (offset a) (offset b))))))

(DEFPRED (addr_lt a b)
  (AND (EQ (base a) (base b)) (< (offset a) (offset b))))

(BG_PUSH
 ;; Why axiom addr_lt_bool_def
 (FORALL (a b)
 (EQ (addr_lt_bool a b)
 (bool_and (eq_int_bool (base a) (base b)) (lt_int_bool
                                           (offset a) (offset b))))))

(DEFPRED (addr_le a b)
  (AND (EQ (base a) (base b)) (<= (offset a) (offset b))))

(BG_PUSH
 ;; Why axiom addr_le_bool_def
 (FORALL (a b)
 (EQ (addr_le_bool a b)
 (bool_and (eq_int_bool (base a) (base b)) (le_int_bool
                                           (offset a) (offset b))))))

(DEFPRED (addr_eq a b)
  (AND (EQ (base a) (base b)) (EQ (offset a) (offset b))))

(BG_PUSH
 ;; Why axiom addr_eq_bool_def
 (FORALL (a b)
 (EQ (addr_eq_bool a b)
 (bool_and (eq_int_bool (base a) (base b)) (eq_int_bool
                                           (offset a) (offset b))))))

(BG_PUSH
 ;; Why axiom cmp_null
 (FORALL (p) (IFF (EQ p 0) (addr_eq p 0))))

(BG_PUSH
 ;; Why axiom cmp_null_bool
 (FORALL (p) (IFF (EQ p 0) (EQ (addr_eq_bool p 0) |@true|))))

(BG_PUSH
 ;; Why axiom cmp_null_not
 (FORALL (p) (IFF (NEQ p 0) (NOT (addr_eq p 0)))))

(BG_PUSH
 ;; Why axiom cmp_null_bool_not
 (FORALL (p) (IFF (NEQ p 0) (EQ (addr_eq_bool p 0) |@false|))))

(BG_PUSH
 ;; Why axiom addrofdata_dataofaddr
 (FORALL (p) (EQ (addr_of_data (data_of_addr p)) p)))

(DEFPRED (valid ta p n)
  (IMPLIES (> n 0)
  (AND (<= 0 (offset p)) (<= (+ (offset p) n) (access ta (base p))))))

(BG_PUSH
 ;; Why axiom fresh
 (FORALL (mem ta |ta'| x p n)
 (IMPLIES (EQ (is_fresh mem ta x) |@true|)
 (IMPLIES (EQ (access ta x) 0)
 (IMPLIES (EQ (access ta (base p)) (access |ta'| (base p)))
 (IMPLIES (valid |ta'| p n) (FORALL (d sz) (NEQ (addr x d) p)))))))

 (FORALL (mem ta x)
 (IMPLIES (EQ (is_fresh mem ta x) |@true|)
 (IMPLIES (EQ (access ta x) 0)
 (FORALL (|ta'| p)
 (IMPLIES (EQ (access ta (base p)) (access |ta'| (base p)))
 (FORALL (n) (IMPLIES (valid |ta'| p n) (FORALL (sz d) (NEQ (addr x d) p))))))))))

(BG_PUSH
 ;; Why axiom fresh_access
 (FORALL (mem |mem'| ta |ta'| b p n)
 (IMPLIES (EQ (is_fresh mem ta b) |@true|)
 (IMPLIES (EQ (access ta b) 0)
 (IMPLIES (valid |ta'| p n)
 (IMPLIES (EQ (access ta (base p)) (access |ta'| (base p)))
 (IMPLIES (EQ (access mem p) (access |mem'| p))
 (FORALL (d) (NEQ (addr b d) (addr_of_data (access |mem'| p))))))))))

 (FORALL (mem ta b)
 (IMPLIES (EQ (is_fresh mem ta b) |@true|)
 (IMPLIES (EQ (access ta b) 0)
 (FORALL (|ta'| p n)
 (IMPLIES (valid |ta'| p n)
 (IMPLIES (EQ (access ta (base p)) (access |ta'| (base p)))
 (FORALL (|mem'|)
 (IMPLIES (EQ (access mem p) (access |mem'| p))
 (FORALL (d) (NEQ (addr b d) (addr_of_data (access |mem'| p)))))))))))))

(BG_PUSH
 ;; Why axiom addr_shift_def
 (FORALL (p dofs)
 (EQ (addr_shift p dofs) (addr (base p) (+ (offset p) dofs)))))

(DEFPRED (separated_on_addr p |p'| n1 n2)
  (IMPLIES (EQ (base p) (base |p'|))
  (OR (<= (+ (offset p) n1) (offset |p'|))
  (>= (offset p) (+ (offset |p'|) n2)))))

(BG_PUSH
 ;; Why axiom is_block_zrange
 (FORALL (x ofs len)
 (IMPLIES (> len 0) (EQ (is_block (zrange x ofs len)) |@true|)))

 (FORALL (len)
 (IMPLIES (> len 0)
 (FORALL (x ofs) (EQ (is_block (zrange x ofs len)) |@true|)))))

(BG_PUSH
 ;; Why axiom is_not_block_zempty
 (NOT (EQ (is_block zempty) |@true|)))

(BG_PUSH
 ;; Why axiom zrange_of_addr_def
 (FORALL (p) (EQ (zrange_of_addr p) (zrange (base p) (offset p) 1))))

(BG_PUSH
 ;; Why axiom zrange_of_addr_range_def
 (FORALL (p dofs n)
 (EQ (zrange_of_addr_range p dofs n) (zrange (base p) (+ (offset p) dofs) n))))

(BG_PUSH
 ;; Why axiom sep_zrange
 (FORALL (b |b'| d |d'| sz |sz'|)
 (IFF (EQ (separated (zrange b d sz) (zrange |b'| |d'| |sz'|)) |@true|)
 (separated_on_addr (addr b d) (addr |b'| |d'|) sz |sz'|))))

(BG_PUSH
 ;; Why axiom separated_sym
 (FORALL (z |z'|)
 (IMPLIES (EQ (separated z |z'|) |@true|) (EQ (separated |z'| z) |@true|))))

(BG_PUSH
 ;; Why axiom sep_empty
 (FORALL (z) (EQ (separated zempty z) |@true|)))

(BG_PUSH
 ;; Why axiom sep_union
 (FORALL (z |z'| r)
 (IFF (EQ (separated z (zunion |z'| r)) |@true|)
 (AND (EQ (separated z |z'|) |@true|) (EQ (separated z r) |@true|)))))

(BG_PUSH
 ;; Why axiom left_empty
 (FORALL (z) (EQ (zunion z zempty) z)))

(BG_PUSH
 ;; Why axiom right_empty
 (FORALL (z) (EQ (zunion zempty z) z)))

(BG_PUSH
 ;; Why axiom union_same
 (FORALL (z) (EQ (zunion z z) z)))

(BG_PUSH
 ;; Why axiom inc_range_range
 (FORALL (b d sz |b'| |d'| |sz'|)
 (IFF (EQ (included (zrange b d sz) (zrange |b'| |d'| |sz'|)) |@true|)
 (IMPLIES (<= d (+ d sz))
 (AND (EQ b |b'|) (AND (<= |d'| d) (<= (+ d sz) (+ |d'| |sz'|))))))))

(BG_PUSH
 ;; Why axiom inc_empty
 (FORALL (z) (EQ (included zempty z) |@true|)))

(BG_PUSH
 ;; Why axiom inc_same
 (FORALL (z) (EQ (included z z) |@true|)))

(BG_PUSH
 ;; Why axiom inc_range_empty
 (FORALL (b d sz)
 (IFF (EQ (included (zrange b d sz) zempty) |@true|) (> b (+ b sz)))))

(BG_PUSH
 ;; Why axiom inc_union_right
 (FORALL (z r s)
 (IMPLIES (OR (EQ (included z r) |@true|) (EQ (included z s) |@true|))
 (EQ (included z (zunion r s)) |@true|))))

(BG_PUSH
 ;; Why axiom inc_union_left
 (FORALL (s z |z'|)
 (IMPLIES (EQ (included s z) |@true|)
 (IMPLIES (EQ (included |z'| z) |@true|)
 (EQ (included (zunion s |z'|) z) |@true|))))

 (FORALL (s z)
 (IMPLIES (EQ (included s z) |@true|)
 (FORALL (|z'|)
 (IMPLIES (EQ (included |z'| z) |@true|)
 (EQ (included (zunion s |z'|) z) |@true|))))))

(BG_PUSH
 ;; Why axiom access_update_range_same
 (FORALL (m z d)
 (IMPLIES (EQ (is_block z) |@true|)
 (EQ (access_range (update_range m z d) z) d)))

 (FORALL (z)
 (IMPLIES (EQ (is_block z) |@true|)
 (FORALL (m d) (EQ (access_range (update_range m z d) z) d)))))

(BG_PUSH
 ;; Why axiom access_update_range_sep
 (FORALL (m v z |z'|)
 (IMPLIES (EQ (is_block z) |@true|)
 (IMPLIES (EQ (is_block |z'|) |@true|)
 (IMPLIES (EQ (separated z |z'|) |@true|)
 (EQ (access_range (update_range m z v) |z'|) (access_range m |z'|))))))

 (FORALL (z)
 (IMPLIES (EQ (is_block z) |@true|)
 (FORALL (|z'|)
 (IMPLIES (EQ (is_block |z'|) |@true|)
 (IMPLIES (EQ (separated z |z'|) |@true|)
 (FORALL (m v)
 (EQ (access_range (update_range m z v) |z'|) (access_range m |z'|)))))))))

(BG_PUSH
 ;; Why axiom access_range_update_addr_sep
 (FORALL (m v z p)
 (IMPLIES (EQ (is_block z) |@true|)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (EQ (access_range (update m p v) z) (access_range m z)))))

 (FORALL (z)
 (IMPLIES (EQ (is_block z) |@true|)
 (FORALL (p)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (FORALL (v m) (EQ (access_range (update m p v) z) (access_range m z))))))))

(BG_PUSH
 ;; Why axiom access_update_range_addr_sep
 (FORALL (m v z p)
 (IMPLIES (EQ (is_block z) |@true|)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (EQ (access (update_range m z v) p) (access m p)))))

 (FORALL (z)
 (IMPLIES (EQ (is_block z) |@true|)
 (FORALL (p)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (FORALL (v m) (EQ (access (update_range m z v) p) (access m p))))))))

(BG_PUSH
 ;; Why axiom access_update_sep
 (FORALL (m v p q)
 (IMPLIES (EQ (separated (zrange_of_addr p) (zrange_of_addr q)) |@true|)
 (EQ (access (update m p v) q) (access m q))))

 (FORALL (p q)
 (IMPLIES (EQ (separated (zrange_of_addr p) (zrange_of_addr q)) |@true|)
 (FORALL (m v) (EQ (access (update m p v) q) (access m q))))))

(BG_PUSH
 ;; Why axiom load_havoc
 (FORALL (m v z p)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (EQ (access (update_havoc m z v) p) (access m p))))

 (FORALL (z p)
 (IMPLIES (EQ (separated z (zrange_of_addr p)) |@true|)
 (FORALL (m v) (EQ (access (update_havoc m z v) p) (access m p))))))

(BG_PUSH
 ;; Why axiom load_is_havoc
 (FORALL (alloc mem |mem'| p z)
 (IMPLIES (EQ (included (zrange_of_addr p) z) |@true|)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (EQ (access |mem'| p) (access mem p)))))

 (FORALL (p z)
 (IMPLIES (EQ (included (zrange_of_addr p) z) |@true|)
 (FORALL (|mem'| mem alloc)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (EQ (access |mem'| p) (access mem p)))))))

(BG_PUSH
 ;; Why axiom is_assignable_range_free
 (FORALL (alloc p z)
 (IMPLIES (EQ (access alloc (base p)) 0)
 (EQ (is_assignable alloc (zrange_of_addr p) z) |@true|)))

 (FORALL (alloc p)
 (IMPLIES (EQ (access alloc (base p)) 0)
 (FORALL (z) (EQ (is_assignable alloc (zrange_of_addr p) z) |@true|)))))

(BG_PUSH
 ;; Why axiom is_assignable_included
 (FORALL (alloc z |z'|)
 (IMPLIES (EQ (included z |z'|) |@true|)
 (EQ (is_assignable alloc z |z'|) |@true|)))

 (FORALL (z |z'|)
 (IMPLIES (EQ (included z |z'|) |@true|)
 (FORALL (alloc) (EQ (is_assignable alloc z |z'|) |@true|)))))

(BG_PUSH
 ;; Why axiom same_havoc
 (FORALL (alloc mem z) (EQ (is_havoc alloc mem z mem) |@true|)))

(BG_PUSH
 ;; Why axiom havoc_sym
 (FORALL (alloc m1 m2 z)
 (IMPLIES (EQ (is_havoc alloc m2 z m1) |@true|)
 (EQ (is_havoc alloc m1 z m2) |@true|))))

(BG_PUSH
 ;; Why axiom store_havoc
 (FORALL (alloc mem |mem'| p v z)
 (IMPLIES (EQ (is_assignable alloc (zrange_of_addr p) z) |@true|)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (EQ (is_havoc alloc mem z (update |mem'| p v)) |@true|))))

 (FORALL (alloc p z)
 (IMPLIES (EQ (is_assignable alloc (zrange_of_addr p) z) |@true|)
 (FORALL (|mem'| mem)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (FORALL (v) (EQ (is_havoc alloc mem z (update |mem'| p v)) |@true|)))))))

(BG_PUSH
 ;; Why axiom store_havoc_havoc
 (FORALL (alloc mem |mem'| v |z'| z)
 (IMPLIES (EQ (is_assignable alloc |z'| z) |@true|)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (EQ (is_havoc alloc mem z (update_havoc |mem'| |z'| v)) |@true|))))

 (FORALL (alloc |z'| z)
 (IMPLIES (EQ (is_assignable alloc |z'| z) |@true|)
 (FORALL (|mem'| mem)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc alloc mem z (update_havoc |mem'| |z'| v)) |@true|)))))))

(BG_PUSH
 ;; Why axiom store_range_havoc
 (FORALL (alloc mem |mem'| v |z'| z)
 (IMPLIES (EQ (is_block |z'|) |@true|)
 (IMPLIES (EQ (is_assignable alloc |z'| z) |@true|)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (EQ (is_havoc alloc mem z (update_range |mem'| |z'| v)) |@true|)))))

 (FORALL (|z'|)
 (IMPLIES (EQ (is_block |z'|) |@true|)
 (FORALL (z alloc)
 (IMPLIES (EQ (is_assignable alloc |z'| z) |@true|)
 (FORALL (mem |mem'|)
 (IMPLIES (EQ (is_havoc alloc mem z |mem'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc alloc mem z (update_range |mem'| |z'| v)) |@true|)))))))))

(BG_PUSH
 ;; Why axiom addr_base
 (FORALL (b d) (EQ (base (addr b d)) b)))

(BG_PUSH
 ;; Why axiom addr_offset
 (FORALL (b d) (EQ (offset (addr b d)) d)))

(BG_PUSH
 ;; Why axiom base_sep
 (FORALL (b |b'| d |d'|)
 (IMPLIES (NEQ b |b'|) (NEQ (addr b d) (addr |b'| |d'|))))

 (FORALL (b |b'|)
 (IMPLIES (NEQ b |b'|) (FORALL (d |d'|) (NEQ (addr b d) (addr |b'| |d'|))))))

(BG_PUSH
 ;; Why axiom addr_inj1
 (FORALL (b |b'| d) (IFF (EQ b |b'|) (EQ (addr b d) (addr |b'| d)))))

(BG_PUSH
 ;; Why axiom addr_inj2
 (FORALL (b d |d'|) (IFF (EQ d |d'|) (EQ (addr b d) (addr b |d'|)))))

(BG_PUSH
 ;; Why axiom addr_lt_eq
 (FORALL (a) (NOT (addr_lt a a))))

(BG_PUSH
 ;; Why axiom addr_le_eq
 (FORALL (a) (addr_le a a)))

(BG_PUSH
 ;; Why axiom minus_pos_lt
 (FORALL (a b)
 (IMPLIES (EQ (base a) (base b))
 (IMPLIES (> (- (offset b) (offset a)) 0) (addr_lt a b)))))

(BG_PUSH
 ;; Why axiom minus_pos_le
 (FORALL (a b)
 (IMPLIES (EQ (base a) (base b))
 (IMPLIES (>= (- (offset b) (offset a)) 0) (addr_le a b)))))

(BG_PUSH
 ;; Why axiom addr_lt_le
 (FORALL (a b) (IMPLIES (addr_lt a b) (addr_le a b))))

(BG_PUSH
 ;; Why axiom havoc_union_update_left
 (FORALL (alloc m |m'| p v asgns)
 (IMPLIES
 (EQ (is_havoc alloc m (zunion (zrange_of_addr p) asgns) |m'|) |@true|)
 (EQ (is_havoc
 alloc m (zunion (zrange_of_addr p) asgns) (update |m'| p v)) |@true|)))

 (FORALL (alloc m |m'| p asgns)
 (IMPLIES
 (EQ (is_havoc alloc m (zunion (zrange_of_addr p) asgns) |m'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc
 alloc m (zunion (zrange_of_addr p) asgns) (update |m'| p v)) |@true|)))))

(BG_PUSH
 ;; Why axiom havoc_union_update_right
 (FORALL (alloc m |m'| p v z asgns)
 (IMPLIES (EQ (included (zrange_of_addr p) asgns) |@true|)
 (IMPLIES (EQ (is_havoc alloc m (zunion z asgns) |m'|) |@true|)
 (EQ (is_havoc alloc m (zunion z asgns) (update |m'| p v)) |@true|))))

 (FORALL (p asgns)
 (IMPLIES (EQ (included (zrange_of_addr p) asgns) |@true|)
 (FORALL (z |m'| m alloc)
 (IMPLIES (EQ (is_havoc alloc m (zunion z asgns) |m'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc alloc m (zunion z asgns) (update |m'| p v)) |@true|)))))))

(BG_PUSH
 ;; Why axiom havoc_union_update_range_left
 (FORALL (alloc m |m'| v p asgns)
 (IMPLIES
 (EQ (is_havoc alloc m (zunion (zrange_of_addr p) asgns) |m'|) |@true|)
 (EQ (is_havoc
 alloc m (zunion (zrange_of_addr p) asgns) (update_range
                                           |m'| (zrange_of_addr p) v)) |@true|)))

 (FORALL (alloc m |m'| p asgns)
 (IMPLIES
 (EQ (is_havoc alloc m (zunion (zrange_of_addr p) asgns) |m'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc
 alloc m (zunion (zrange_of_addr p) asgns) (update_range
                                           |m'| (zrange_of_addr p) v)) |@true|)))))

(BG_PUSH
 ;; Why axiom havoc_union_update_range_right
 (FORALL (alloc m |m'| v p z asgns)
 (IMPLIES (EQ (included (zrange_of_addr p) asgns) |@true|)
 (IMPLIES (EQ (is_havoc alloc m (zunion z asgns) |m'|) |@true|)
 (EQ (is_havoc
 alloc m (zunion z asgns) (update_range |m'| (zrange_of_addr p) v)) |@true|))))

 (FORALL (p asgns)
 (IMPLIES (EQ (included (zrange_of_addr p) asgns) |@true|)
 (FORALL (z |m'| m alloc)
 (IMPLIES (EQ (is_havoc alloc m (zunion z asgns) |m'|) |@true|)
 (FORALL (v)
 (EQ (is_havoc
 alloc m (zunion z asgns) (update_range |m'| (zrange_of_addr p) v)) |@true|)))))))

(BG_PUSH
 ;; Why axiom inc_union_union
 (FORALL (z0 z1 z2 z3)
 (IMPLIES (EQ (included z0 z2) |@true|)
 (IMPLIES (EQ (included z1 z3) |@true|)
 (EQ (included (zunion z0 z1) (zunion z2 z3)) |@true|))))

 (FORALL (z0 z2)
 (IMPLIES (EQ (included z0 z2) |@true|)
 (FORALL (z3 z1)
 (IMPLIES (EQ (included z1 z3) |@true|)
 (EQ (included (zunion z0 z1) (zunion z2 z3)) |@true|))))))

(BG_PUSH
 ;; Why axiom inc_permut_union
 (FORALL (z |z'| r)
 (EQ (included
 (zunion (zunion z |z'|) r) (zunion (zunion z r) |z'|)) |@true|)))

(BG_PUSH
 ;; Why axiom inc_permut2
 (FORALL (z s r)
 (EQ (included
 (zunion (zunion (zunion (zunion z s) r) r) s) (zunion (zunion z r) s)) |@true|)))

(BG_PUSH
 ;; Why axiom union_assoc2
 (FORALL (z |z'|) (EQ (zunion z (zunion z |z'|)) (zunion z |z'|))))

(BG_PUSH
 ;; Why axiom addr_shift_0
 (FORALL (p) (EQ (addr_shift p 0) p)))

(BG_PUSH
 ;; Why axiom addr_shift_shift
 (FORALL (p d |d'|)
 (EQ (addr_shift (addr_shift p d) |d'|) (addr_shift p (+ d |d'|)))))

(BG_PUSH
 ;; Why axiom valid_elt
 (FORALL (ta p i n)
 (IMPLIES (> n 0)
 (IMPLIES (valid ta p n)
 (IMPLIES (<= 0 i) (IMPLIES (<= (+ i 1) n) (valid ta (addr_shift p i) 1))))))

 (FORALL (n)
 (IMPLIES (> n 0)
 (FORALL (p ta)
 (IMPLIES (valid ta p n)
 (FORALL (i)
 (IMPLIES (<= 0 i) (IMPLIES (<= (+ i 1) n) (valid ta (addr_shift p i) 1)))))))))

(BG_PUSH
 ;; Why axiom separated_on_addr_sym
 (FORALL (p q n m)
 (IMPLIES (separated_on_addr p q n m) (separated_on_addr q p m n))))

(BG_PUSH
 ;; Why axiom separated_on_addr_inc
 (FORALL (b d |d'| sz |sz'| b1 d1 sz1)
 (IMPLIES (separated_on_addr (addr b1 d1) (addr b d) sz1 sz)
 (IMPLIES (<= d |d'|)
 (IMPLIES (<= (+ |d'| |sz'|) (+ d sz))
 (separated_on_addr (addr b1 d1) (addr b |d'|) sz1 |sz'|)))))

 (FORALL (b d sz b1 d1 sz1)
 (IMPLIES (separated_on_addr (addr b1 d1) (addr b d) sz1 sz)
 (FORALL (|d'|)
 (IMPLIES (<= d |d'|)
 (FORALL (|sz'|)
 (IMPLIES (<= (+ |d'| |sz'|) (+ d sz))
 (separated_on_addr (addr b1 d1) (addr b |d'|) sz1 |sz'|))))))))

(BG_PUSH
 ;; Why axiom separated_inc
 (FORALL (b d |d'| sz |sz'| b1 d1 sz1)
 (IMPLIES (EQ (separated (zrange b1 d1 sz1) (zrange b d sz)) |@true|)
 (IMPLIES (<= d |d'|)
 (IMPLIES (<= (+ |d'| |sz'|) (+ d sz))
 (EQ (separated (zrange b1 d1 sz1) (zrange b |d'| |sz'|)) |@true|)))))

 (FORALL (b d sz b1 d1 sz1)
 (IMPLIES (EQ (separated (zrange b1 d1 sz1) (zrange b d sz)) |@true|)
 (FORALL (|d'|)
 (IMPLIES (<= d |d'|)
 (FORALL (|sz'|)
 (IMPLIES (<= (+ |d'| |sz'|) (+ d sz))
 (EQ (separated (zrange b1 d1 sz1) (zrange b |d'| |sz'|)) |@true|))))))))

(BG_PUSH
 ;; Why axiom separated_one_elt
 (FORALL (n m b d sz |b'| |d'| |sz'|)
 (IMPLIES (< 0 n)
 (IMPLIES (< 0 m)
 (IMPLIES
 (EQ (separated
 (zrange b d (* sz n)) (zrange |b'| |d'| (* |sz'| m))) |@true|)
 (FORALL (i j)
 (IMPLIES (<= 0 i)
 (IMPLIES (<= 0 j)
 (IMPLIES (<= (+ (+ d i) sz) (+ d (* sz n)))
 (IMPLIES (<= (+ (+ |d'| j) |sz'|) (+ |d'| (* |sz'| m)))
 (EQ (separated
 (zrange b (+ d i) sz) (zrange |b'| (+ |d'| j) |sz'|)) |@true|))))))))))

 (FORALL (n)
 (IMPLIES (< 0 n)
 (FORALL (m)
 (IMPLIES (< 0 m)
 (FORALL (b d sz |b'| |d'| |sz'|)
 (IMPLIES
 (EQ (separated
 (zrange b d (* sz n)) (zrange |b'| |d'| (* |sz'| m))) |@true|)
 (FORALL (i)
 (IMPLIES (<= 0 i)
 (FORALL (j)
 (IMPLIES (<= 0 j)
 (IMPLIES (<= (+ (+ d i) sz) (+ d (* sz n)))
 (IMPLIES (<= (+ (+ |d'| j) |sz'|) (+ |d'| (* |sz'| m)))
 (EQ (separated
 (zrange b (+ d i) sz) (zrange |b'| (+ |d'| j) |sz'|)) |@true|))))))))))))))

(BG_PUSH
 ;; Why axiom store_pointer
 (FORALL (x ofs y |ofs'|)
 (OR (separated_on_addr (addr x ofs) (addr y |ofs'|) 1 1)
 (EQ (addr x ofs) (addr y |ofs'|)))))

(BG_PUSH
 ;; Why axiom X_i_def
 (EQ X_i 1))

(BG_PUSH
 ;; Why axiom X_a_def
 (EQ X_a 2))

(BG_PUSH
 ;; Why axiom X_n_def
 (EQ X_n 3))

(BG_PUSH
 ;; Why axiom X_b_def
 (EQ X_b 4))

(BG_PUSH
 ;; Why axiom Def_IsEqual
 (FORALL (m m_0 a n b)
 (IFF (EQ (D_IsEqual m m_0 a n b) |@true|)
 (FORALL (i)
 (IMPLIES (<= 0 i)
 (IMPLIES (< i n)
 (EQ (sint32_of_data (access m (addr_shift a i)))
 (sint32_of_data (access m_0 (addr_shift b i))))))))))

(BG_PUSH
 ;; Why axiom Def_IsValidRange
 (FORALL (ta a n)
 (IFF (EQ (D_IsValidRange ta a n) |@true|)
 (AND (<= 0 n) (valid ta (addr_shift a 0) n)))))

;; store_swap_ranges_exit_assigns_part3, File "./out/store_swap_ranges_exit_assigns_part3_po.why", line 997, characters 0-1179
(FORALL (b_0 n_0 a_0)
(IMPLIES (is_sint32 n_0)
(FORALL (m_0 ta_0)
(IMPLIES (EQ (global ta_0) |@true|)
(IMPLIES (EQ (D_IsValidRange ta_0 a_0 n_0) |@true|)
(IMPLIES (EQ (D_IsValidRange ta_0 b_0 n_0) |@true|)
(IMPLIES (separated_on_addr a_0 b_0 n_0 n_0)
(FORALL (i_0 v_0 v_1 i_1 m_1)
(IMPLIES (is_sint32 i_1)
(IMPLIES (is_sint32 i_0)
(IMPLIES (EQ i_1 i_0)
(IMPLIES
(EQ m_1
(update_havoc
(update_havoc m_0 (zrange_of_addr_range a_0 0 i_1) v_0) (zrange_of_addr_range
                                                        b_0 0 i_1) v_1))
(IMPLIES
(EQ (D_IsEqual
(update_havoc
(update_havoc m_0 (zrange_of_addr_range a_0 0 i_1) v_0) (zrange_of_addr_range
                                                        b_0 0 i_1) v_1) m_0 a_0 i_0 b_0) |@true|)
(IMPLIES
(EQ (D_IsEqual
m_0 (update_havoc
    (update_havoc m_0 (zrange_of_addr_range a_0 0 i_1) v_0) (zrange_of_addr_range
                                                            b_0 0 i_1) v_1) a_0 i_0 b_0) |@true|)
(IMPLIES (<= 0 i_0)
(IMPLIES (<= i_0 n_0)
(IMPLIES (< i_0 n_0)
(IMPLIES (valid ta_0 (addr_shift a_0 i_0) 1)
(IMPLIES (valid ta_0 (addr_shift b_0 i_0) 1)
(EQ (included
(zrange_of_addr_range (addr_shift a_0 i_0) 0 1) (zunion
                                                (zrange_of_addr_range
                                                b_0 0 n_0) (zunion
                                                           (zrange_of_addr_range
                                                           a_0 0 n_0) 
                                                           (zunion
                                                           (zrange X_i 0 1) 
                                                           (zunion
                                                           (zrange X_b 0 1) 
                                                           (zunion
                                                           (zrange X_n 0 1) 
                                                           (zrange X_a 0 1))))))) |@true|))))))))))))))))))))