theory Why2 use array.Array as A use unit_inf.Unit use int.Int use int.ComputerDivision use real.Real use bool_inf.Bool predicate eq_unit Unit.unit Unit.unit predicate neq_unit Unit.unit Unit.unit predicate eq_bool Bool.bool Bool.bool predicate neq_bool Bool.bool Bool.bool predicate lt_int int int predicate le_int int int predicate gt_int int int predicate ge_int int int predicate eq_int int int predicate neq_int int int function add_int int int : int function sub_int int int : int function mul_int int int : int function div_int int int : int function mod_int int int : int function neg_int int : int predicate zwf_zero (a : int) (b : int) = ((Int.(<=) 0 b) /\ (Int.(<) a b)) function bw_compl int : int function bw_and int int : int function bw_xor int int : int function bw_or int int : int function lsl int int : int function lsr int int : int type pointer 'z type addr 'z type alloc_table function block_length alloc_table (pointer 'a1) : int function base_addr (pointer 'a1) : (addr 'a1) function offset (pointer 'a1) : int function shift (pointer 'a1) int : (pointer 'a1) function sub_pointer (pointer 'a1) (pointer 'a1) : int predicate lt_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) = (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ (Int.(<) (offset p1 : int) (offset p2 : int))) predicate le_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) = (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ (Int.(<=) (offset p1 : int) (offset p2 : int))) predicate gt_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) = (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ (Int.(>) (offset p1 : int) (offset p2 : int))) predicate ge_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) = (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ (Int.(>=) (offset p1 : int) (offset p2 : int))) predicate valid (a : alloc_table) (p : (pointer 'a1)) = ((Int.(<=) 0 (offset p : int)) /\ (Int.(<) (offset p : int) (block_length a p : int))) predicate valid_index (a : alloc_table) (p : (pointer 'a1)) (i : int) = ((Int.(<=) 0 (Int.(+) (offset p : int) i : int)) /\ (Int.(<) (Int.(+) (offset p : int) i : int) (block_length a p : int))) predicate valid_range (a : alloc_table) (p : (pointer 'a1)) (i : int) (j : int) = ((Int.(<=) 0 (Int.(+) (offset p : int) i : int)) /\ (Int.(<) (Int.(+) (offset p : int) j : int) (block_length a p : int))) axiom Offset_shift: (forall p:(pointer 'a1). (forall i:int [(offset (shift p i : (pointer 'a1)) : int)]. ((offset (shift p i : (pointer 'a1)) : int) = (Int.(+) (offset p : int) i : int)))) axiom Shift_zero: (forall p:(pointer 'a1) [(shift p 0 : (pointer 'a1))]. ((shift p 0 : (pointer 'a1)) = p)) axiom Shift_shift: (forall p:(pointer 'a1). (forall i:int. (forall j:int [(shift (shift p i : (pointer 'a1)) j : (pointer 'a1))]. ((shift (shift p i : (pointer 'a1)) j : (pointer 'a1)) = (shift p (Int.(+) i j : int) : (pointer 'a1)))))) axiom Base_addr_shift: (forall p:(pointer 'a1). (forall i:int [(base_addr (shift p i : (pointer 'a1)) : (addr 'a1))]. ((base_addr (shift p i : (pointer 'a1)) : (addr 'a1)) = (base_addr p : (addr 'a1))))) axiom Block_length_shift: (forall a:alloc_table. (forall p:(pointer 'a1). (forall i:int [(block_length a (shift p i : (pointer 'a1)) : int)]. ((block_length a (shift p i : (pointer 'a1)) : int) = (block_length a p : int))))) axiom Base_addr_block_length: (forall a:alloc_table. (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) -> ((block_length a p1 : int) = (block_length a p2 : int)))))) axiom Pointer_pair_1: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). ((((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ ((offset p1 : int) = (offset p2 : int))) -> (p1 = p2)))) axiom Pointer_pair_2: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). ((p1 = p2) -> (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\ ((offset p1 : int) = (offset p2 : int)))))) axiom Neq_base_addr_neq_shift: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (forall i:int. (forall j:int. (((base_addr p1 : (addr 'a1)) <> (base_addr p2 : (addr 'a1))) -> ((shift p1 i : (pointer 'a1)) <> (shift p2 j : (pointer 'a1)))))))) axiom Neq_offset_neq_shift: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (forall i:int. (forall j:int. (((Int.(+) (offset p1 : int) i : int) <> (Int.(+) (offset p2 : int) j : int)) -> ((shift p1 i : (pointer 'a1)) <> (shift p2 j : (pointer 'a1)))))))) axiom Eq_offset_eq_shift: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (forall i:int. (forall j:int. (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) -> (((Int.(+) (offset p1 : int) i : int) = (Int.(+) (offset p2 : int) j : int)) -> ((shift p1 i : (pointer 'a1)) = (shift p2 j : (pointer 'a1))))))))) axiom Valid_index_valid_shift: (forall a:alloc_table. (forall p:(pointer 'a1). (forall i:int. ((valid_index a p i) -> (valid a (shift p i : (pointer 'a1))))))) axiom Valid_range_valid_shift: (forall a:alloc_table. (forall p:(pointer 'a1). (forall i:int. (forall j:int. (forall k:int. ((valid_range a p i j) -> (((Int.(<=) i k) /\ (Int.(<=) k j)) -> (valid a (shift p k : (pointer 'a1)))))))))) axiom Valid_range_valid: (forall a:alloc_table. (forall p:(pointer 'a1). (forall i:int. (forall j:int. ((valid_range a p i j) -> (((Int.(<=) i 0) /\ (Int.(<=) 0 j)) -> (valid a p))))))) axiom Valid_range_valid_index: (forall a:alloc_table. (forall p:(pointer 'a1). (forall i:int. (forall j:int. (forall k:int. ((valid_range a p i j) -> (((Int.(<=) i k) /\ (Int.(<=) k j)) -> (valid_index a p k)))))))) axiom Sub_pointer_def: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) -> ((sub_pointer p1 p2 : int) = (Int.(-) (offset p1 : int) (offset p2 : int) : int))))) type memory 'a 'z = A.t (pointer 'z) 'a function acc (m:memory 'a1 'a2) (k:pointer 'a2) : 'a1 = A.get m k function upd (m:memory 'a1 'a2) (k:pointer 'a2) (v:'a1) : (memory 'a1 'a2) = A.set m k v type pset 'z function pset_empty : (pset 'a1) function pset_singleton (pointer 'a1) : (pset 'a1) function pset_star (pset 'a2) (memory (pointer 'a1) 'a2) : (pset 'a1) function pset_all (pset 'a1) : (pset 'a1) function pset_range (pset 'a1) int int : (pset 'a1) function pset_range_left (pset 'a1) int : (pset 'a1) function pset_range_right (pset 'a1) int : (pset 'a1) function pset_acc_all (pset 'a2) (memory (pointer 'a1) 'a2) : (pset 'a1) function pset_acc_range (pset 'a2) (memory (pointer 'a1) 'a2) int int : (pset 'a1) function pset_acc_range_left (pset 'a2) (memory (pointer 'a1) 'a2) int : (pset 'a1) function pset_acc_range_right (pset 'a2) (memory (pointer 'a1) 'a2) int : (pset 'a1) function pset_union (pset 'a1) (pset 'a1) : (pset 'a1) predicate not_in_pset (pointer 'a1) (pset 'a1) predicate not_assigns (a : alloc_table) (m1 : (memory 'a1 'a2)) (m2 : (memory 'a1 'a2)) (l : (pset 'a2)) = (forall p:(pointer 'a2). ((valid a p) -> ((not_in_pset p l) -> ((acc m2 p : 'a1) = (acc m1 p : 'a1))))) axiom Pset_empty_intro: (forall p:(pointer 'a1). (not_in_pset p (pset_empty : (pset 'a1)))) axiom Pset_singleton_intro: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1) [(not_in_pset p1 (pset_singleton p2 : (pset 'a1)))]. ((p1 <> p2) -> (not_in_pset p1 (pset_singleton p2 : (pset 'a1)))))) axiom Pset_singleton_elim: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1) [(not_in_pset p1 (pset_singleton p2 : (pset 'a1)))]. ((not_in_pset p1 (pset_singleton p2 : (pset 'a1))) -> (p1 <> p2)))) axiom Not_not_in_singleton: (forall p:(pointer 'a1). (not (not_in_pset p (pset_singleton p : (pset 'a1))))) axiom Pset_union_intro: (forall l1:(pset 'a1). (forall l2:(pset 'a1). (forall p:(pointer 'a1) [(not_in_pset p (pset_union l1 l2 : (pset 'a1)))]. (((not_in_pset p l1) /\ (not_in_pset p l2)) -> (not_in_pset p (pset_union l1 l2 : (pset 'a1))))))) axiom Pset_union_elim1: (forall l1:(pset 'a1). (forall l2:(pset 'a1). (forall p:(pointer 'a1) [(not_in_pset p (pset_union l1 l2 : (pset 'a1)))]. ((not_in_pset p (pset_union l1 l2 : (pset 'a1))) -> (not_in_pset p l1))))) axiom Pset_union_elim2: (forall l1:(pset 'a1). (forall l2:(pset 'a1). (forall p:(pointer 'a1) [(not_in_pset p (pset_union l1 l2 : (pset 'a1)))]. ((not_in_pset p (pset_union l1 l2 : (pset 'a1))) -> (not_in_pset p l2))))) axiom Pset_star_intro: (forall l:(pset 'a1). (forall m:(memory (pointer 'a2) 'a1). (forall p:(pointer 'a2) [(not_in_pset p (pset_star l m : (pset 'a2)))]. ((forall p1:(pointer 'a1). ((p = (acc m p1 : (pointer 'a2))) -> (not_in_pset p1 l))) -> (not_in_pset p (pset_star l m : (pset 'a2))))))) axiom Pset_star_elim: (forall l:(pset 'a1). (forall m:(memory (pointer 'a2) 'a1). (forall p:(pointer 'a2) [(not_in_pset p (pset_star l m : (pset 'a2)))]. ((not_in_pset p (pset_star l m : (pset 'a2))) -> (forall p1:(pointer 'a1). ((p = (acc m p1 : (pointer 'a2))) -> (not_in_pset p1 l))))))) axiom Pset_all_intro: (forall p:(pointer 'a1). (forall l:(pset 'a1) [(not_in_pset p (pset_all l : (pset 'a1)))]. ((forall p1:(pointer 'a1). ((not (not_in_pset p1 l)) -> ((base_addr p : (addr 'a1)) <> (base_addr p1 : (addr 'a1))))) -> (not_in_pset p (pset_all l : (pset 'a1)))))) axiom Pset_all_elim: (forall p:(pointer 'a1). (forall l:(pset 'a1) [(not_in_pset p (pset_all l : (pset 'a1)))]. ((not_in_pset p (pset_all l : (pset 'a1))) -> (forall p1:(pointer 'a1). ((not (not_in_pset p1 l)) -> ((base_addr p : (addr 'a1)) <> (base_addr p1 : (addr 'a1)))))))) axiom Pset_range_intro: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int. (forall b:int [(not_in_pset p (pset_range l a b : (pset 'a1)))]. ((forall p1:(pointer 'a1). ((not_in_pset p1 l) \/ (forall i:int. (((Int.(<=) a i) /\ (Int.(<=) i b)) -> (p <> (shift p1 i : (pointer 'a1))))))) -> (not_in_pset p (pset_range l a b : (pset 'a1)))))))) axiom Pset_range_elim: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int. (forall b:int [(not_in_pset p (pset_range l a b : (pset 'a1)))]. ((not_in_pset p (pset_range l a b : (pset 'a1))) -> (forall p1:(pointer 'a1). ((not (not_in_pset p1 l)) -> (forall i:int. (((Int.(<=) a i) /\ (Int.(<=) i b)) -> ((shift p1 i : (pointer 'a1)) <> p)))))))))) axiom Pset_range_left_intro: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int [(not_in_pset p (pset_range_left l a : (pset 'a1)))]. ((forall p1:(pointer 'a1). ((not_in_pset p1 l) \/ (forall i:int. ((Int.(<=) i a) -> (p <> (shift p1 i : (pointer 'a1))))))) -> (not_in_pset p (pset_range_left l a : (pset 'a1))))))) axiom Pset_range_left_elim: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int [(not_in_pset p (pset_range_left l a : (pset 'a1)))]. ((not_in_pset p (pset_range_left l a : (pset 'a1))) -> (forall p1:(pointer 'a1). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) i a) -> ((shift p1 i : (pointer 'a1)) <> p))))))))) axiom Pset_range_right_intro: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int [(not_in_pset p (pset_range_right l a : (pset 'a1)))]. ((forall p1:(pointer 'a1). ((not_in_pset p1 l) \/ (forall i:int. ((Int.(<=) a i) -> (p <> (shift p1 i : (pointer 'a1))))))) -> (not_in_pset p (pset_range_right l a : (pset 'a1))))))) axiom Pset_range_right_elim: (forall p:(pointer 'a1). (forall l:(pset 'a1). (forall a:int [(not_in_pset p (pset_range_right l a : (pset 'a1)))]. ((not_in_pset p (pset_range_right l a : (pset 'a1))) -> (forall p1:(pointer 'a1). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) a i) -> ((shift p1 i : (pointer 'a1)) <> p))))))))) axiom Pset_acc_all_intro: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2) [(not_in_pset p (pset_acc_all l m : (pset 'a1)))]. ((forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. (p <> (acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1)))))) -> (not_in_pset p (pset_acc_all l m : (pset 'a1))))))) axiom Pset_acc_all_elim: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2) [(not_in_pset p (pset_acc_all l m : (pset 'a1)))]. ((not_in_pset p (pset_acc_all l m : (pset 'a1))) -> (forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. ((acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1)) <> p)))))))) axiom Pset_acc_range_intro: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int. (forall b:int [(not_in_pset p (pset_acc_range l m a b : (pset 'a1)))]. ((forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. (((Int.(<=) a i) /\ (Int.(<=) i b)) -> (p <> (acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1))))))) -> (not_in_pset p (pset_acc_range l m a b : (pset 'a1))))))))) axiom Pset_acc_range_elim: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int. (forall b:int. ((not_in_pset p (pset_acc_range l m a b : (pset 'a1))) -> (forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. (((Int.(<=) a i) /\ (Int.(<=) i b)) -> ((acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1)) <> p))))))))))) axiom Pset_acc_range_left_intro: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int [(not_in_pset p (pset_acc_range_left l m a : (pset 'a1)))]. ((forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) i a) -> (p <> (acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1))))))) -> (not_in_pset p (pset_acc_range_left l m a : (pset 'a1)))))))) axiom Pset_acc_range_left_elim: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int [(not_in_pset p (pset_acc_range_left l m a : (pset 'a1)))]. ((not_in_pset p (pset_acc_range_left l m a : (pset 'a1))) -> (forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) i a) -> ((acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1)) <> p)))))))))) axiom Pset_acc_range_right_intro: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int [(not_in_pset p (pset_acc_range_right l m a : (pset 'a1)))]. ((forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) a i) -> (p <> (acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1))))))) -> (not_in_pset p (pset_acc_range_right l m a : (pset 'a1)))))))) axiom Pset_acc_range_right_elim: (forall p:(pointer 'a1). (forall l:(pset 'a2). (forall m:(memory (pointer 'a1) 'a2). (forall a:int [(not_in_pset p (pset_acc_range_right l m a : (pset 'a1)))]. ((not_in_pset p (pset_acc_range_right l m a : (pset 'a1))) -> (forall p1:(pointer 'a2). ((not (not_in_pset p1 l)) -> (forall i:int. ((Int.(<=) a i) -> ((acc m (shift p1 i : (pointer 'a2)) : (pointer 'a1)) <> p)))))))))) axiom Not_assigns_trans: (forall a:alloc_table. (forall l:(pset 'a1). (forall m1:(memory 'a2 'a1). (forall m2:(memory 'a2 'a1). (forall m3:(memory 'a2 'a1). ((not_assigns a m1 m2 l) -> ((not_assigns a m2 m3 l) -> (not_assigns a m1 m3 l)))))))) axiom Not_assigns_refl: (forall a:alloc_table. (forall l:(pset 'a1). (forall m:(memory 'a2 'a1). (not_assigns a m m l)))) predicate valid_acc (m1 : (memory (pointer 'a1) 'a2)) = (forall p:(pointer 'a2). (forall a:alloc_table. ((valid a p) -> (valid a (acc m1 p : (pointer 'a1)))))) predicate valid_acc_range (m1 : (memory (pointer 'a1) 'a2)) (size : int) = (forall p:(pointer 'a2). (forall a:alloc_table. ((valid a p) -> (valid_range a (acc m1 p : (pointer 'a1)) 0 (Int.(-) size 1 : int))))) axiom Valid_acc_range_valid: (forall m1:(memory (pointer 'a1) 'a2). (forall size:int. (forall p:(pointer 'a2). (forall a:alloc_table. ((valid_acc_range m1 size) -> ((valid a p) -> (valid a (acc m1 p : (pointer 'a1))))))))) predicate separation1 (m1 : (memory (pointer 'a1) 'a2)) (m2 : (memory (pointer 'a1) 'a2)) = (forall p:(pointer 'a2). (forall a:alloc_table. ((valid a p) -> ((base_addr (acc m1 p : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m2 p : (pointer 'a1)) : (addr 'a1)))))) predicate separation1_range1 (m1 : (memory (pointer 'a1) 'a2)) (m2 : (memory (pointer 'a1) 'a2)) (size : int) = (forall p:(pointer 'a2). (forall a:alloc_table. ((valid a p) -> (forall i1:int. (forall i2:int. (((Int.(<=) 0 i1) /\ (Int.(<) i1 size)) -> (((Int.(<=) 0 i2) /\ (Int.(<) i2 size)) -> ((base_addr (acc m1 (shift p i1 : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m2 (shift p i2 : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1)))))))))) predicate separation1_range (m : (memory (pointer 'a1) 'a2)) (size : int) = (forall p:(pointer 'a2). (forall a:alloc_table. ((valid a p) -> (forall i1:int. (((Int.(<=) 0 i1) /\ (Int.(<) i1 size)) -> ((base_addr (acc m (shift p i1 : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m p : (pointer 'a1)) : (addr 'a1)))))))) predicate separation2 (m1 : (memory (pointer 'a1) 'a2)) (m2 : (memory (pointer 'a1) 'a2)) = (forall p1:(pointer 'a2). (forall p2:(pointer 'a2). ((p1 <> p2) -> ((base_addr (acc m1 p1 : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m2 p2 : (pointer 'a1)) : (addr 'a1)))))) predicate separation2_range1 (m1 : (memory (pointer 'a1) 'a2)) (m2 : (memory (pointer 'a1) 'a2)) (size : int) = (forall p:(pointer 'a2). (forall q:(pointer 'a2). (forall a:alloc_table. (forall i:int. (((Int.(<=) 0 i) /\ (Int.(<) i size)) -> ((base_addr (acc m1 (shift p i : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m2 q : (pointer 'a1)) : (addr 'a1)))))))) predicate on_heap alloc_table (pointer 'a1) predicate on_stack alloc_table (pointer 'a1) predicate fresh alloc_table (pointer 'a1) axiom Fresh_not_valid: (forall a:alloc_table. (forall p:(pointer 'a1). ((fresh a p) -> (not (valid a p))))) axiom Fresh_not_valid_shift: (forall a:alloc_table. (forall p:(pointer 'a1). ((fresh a p) -> (forall i:int. (not (valid a (shift p i : (pointer 'a1)))))))) predicate alloc_extends alloc_table alloc_table axiom Alloc_extends_valid: (forall a1:alloc_table. (forall a2:alloc_table. ((alloc_extends a1 a2) -> (forall q:(pointer 'a1). ((valid a1 q) -> (valid a2 q)))))) axiom Alloc_extends_valid_index: (forall a1:alloc_table. (forall a2:alloc_table. ((alloc_extends a1 a2) -> (forall q:(pointer 'a1). (forall i:int. ((valid_index a1 q i) -> (valid_index a2 q i))))))) axiom Alloc_extends_valid_range: (forall a1:alloc_table. (forall a2:alloc_table. ((alloc_extends a1 a2) -> (forall q:(pointer 'a1). (forall i:int. (forall j:int. ((valid_range a1 q i j) -> (valid_range a2 q i j)))))))) axiom Alloc_extends_refl: (forall a:alloc_table. (alloc_extends a a)) axiom Alloc_extends_trans: (forall a1:alloc_table. (forall a2:alloc_table. (forall a3:alloc_table [(alloc_extends a1 a2), (alloc_extends a2 a3)]. ((alloc_extends a1 a2) -> ((alloc_extends a2 a3) -> (alloc_extends a1 a3)))))) predicate free_stack alloc_table alloc_table alloc_table axiom Free_stack_heap: (forall a1:alloc_table. (forall a2:alloc_table. (forall a3:alloc_table. ((free_stack a1 a2 a3) -> (forall p:(pointer 'a1). ((valid a2 p) -> ((on_heap a2 p) -> (valid a3 p)))))))) axiom Free_stack_stack: (forall a1:alloc_table. (forall a2:alloc_table. (forall a3:alloc_table. ((free_stack a1 a2 a3) -> (forall p:(pointer 'a1). ((valid a1 p) -> ((on_stack a1 p) -> (valid a3 p)))))))) function null : (pointer 'a1) axiom Null_not_valid: (forall a:alloc_table. (not (valid a (null : (pointer 'a1))))) type anonymous_0PM_134 type anonymous_0PM_136 type p2_1_111 type p1_0_54 type anonymous_0PM_137 type anonymous_0PM_139 type anonymous_1PM_132 type index_3_83 type w_8 type w_9 type index_7_91 type v2_14 type anonymous_1PM_135 type v2_15 type p2_1_84 type anonymous_1PM_138 type p_52 type u_26 type p1_0 type u_27 type p2_1_89 type p_56 type m_10 type anonymous_0PM_144 type m_11 type p2_1_120 type anonymous_0PM_146 type anonymous_0PM_147 type anonymous_1PM_140 type anonymous_0PM_149 type anonymous_1PM_141 type p1_0_104 type anonymous_1PM_143 type anonymous_1PM_145 type p2_1_92 type p2_1_93 type p2_1_41 type anonymous_1PM_148 type p2_1_95 type pp1_2_55 type v_6 type p2_1_44 type v_7 type index_2_82 type anonymous_0PM_150 type index_6_90 type p2_1_47 type anonymous_0PM_152 type anonymous_0PM_153 type anonymous_0PM_101 type p_16 type p_17 type anonymous_0PM_155 type anonymous_0PM_103 type p_18 type p1_0_110 type p_19 type anonymous_0PM_106 type anonymous_1PM_151 type anonymous_0PM_107 type anonymous_1PM_128_129 type anonymous_0PM_109 type anonymous_1PM_154 type anonymous_0PM_97_102 type p2_1_50 type v2_36 type p1_0_119 type index_1_79 type v2_37 type p2_1_53 type index_5_87 type anonymous_0PM_97_108 type anonymous_0PM_97 type u2_12 type u2_13 type p1_0_80 type p1_0_81 type u_4 type anonymous_0PM_112 type null_20 type u_5 type anonymous_0PM_113 type m_32 type null_21 type anonymous_0PM_114 type m_33 type null_22 type anonymous_0PM_115 type p1_0_85 type null_23 type pp2_3 type anonymous_0PM_116 type null_24 type null_25 type anonymous_0PM_118 type p1_0_88 type w_30 type w_31 type anonymous_0PM_97_117 type anonymous_1PM_128_142 type anonymous_0PM_121 type anonymous_0PM_122 type index_0_78 type anonymous_0PM_123 type anonymous_0PM_124 type index_4_86 type p1_0_42 type anonymous_0PM_125 type p2_1_100 type anonymous_0PM_126 type p1_0_96 type index_8_94 type anonymous_0PM_127 type p1_0_45 type pp2_3_57 type p1_0_99 type p2_1_105 type p1_0_48 type v_28 type p2_1 type v_29 type pp1_2 type anonymous_0PM_97_98 type anonymous_1PM_128 type anonymous_0PM_130 type u2_34 type anonymous_0PM_131 type u2_35 type anonymous_0PM_133 type p1_0_51 goal F_impl_po_1: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid alloc u))))))))))))))))))) goal F_impl_po_2: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid alloc (acc p1_u_27 u : (pointer p1_0_51))))))))))))))))))))) goal F_impl_po_3: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid alloc (acc p2_u_27 u : (pointer p2_1_50))))))))))))))))))))) goal F_impl_po_4: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid alloc (acc pp1_u_27 u : (pointer null_20)))))))))))))))))))))) goal F_impl_po_5: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4))))))))))))))))))) goal F_impl_po_6: (forall alloc:alloc_table. (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v2_0:(pointer v2_37). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ (("CADUCEUS_2" (valid_acc p1_u_27)) /\ (("CADUCEUS_3" (valid_acc p1_v_29)) /\ (("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> ("CADUCEUS_25" (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))))))))))))))))))) goal F_impl_po_7: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid alloc v)))))))))))))))))))))))))))))))) goal F_impl_po_8: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))))))))))))))))))))))))))))))))) goal F_impl_po_9: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))))))))))))))))))))))))))))))))) goal F_impl_po_10: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid alloc (acc pp1_v_29 v : (pointer null_21))))))))))))))))))))))))))))))))))) goal F_impl_po_11: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)))))))))))))))))))))))))))))))) goal F_impl_po_12: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ (("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ (("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ (("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ (("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ (("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ (("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ (("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ (("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ (("CADUCEUS_6" (valid_acc p2_u_27)) /\ (("CADUCEUS_7" (valid_acc p2_v_29)) /\ (("CADUCEUS_8" (valid_acc p2_w_31)) /\ (("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). ((("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" (((((not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4)))))))))))))))))))))))))))))))) goal F_impl_po_13: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid alloc w))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_14: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid alloc (acc p1_w_31 w : (pointer p1_0_45))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_15: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid alloc (acc p2_w_31 w : (pointer p2_1_44))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_16: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid alloc (acc pp1_w_31 w : (pointer null_22)))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_17: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_18: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall w:(pointer w_31). ((("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (("CADUCEUS_23" (valid alloc u)) /\ (("CADUCEUS_22" (valid alloc m)) /\ (("CADUCEUS_21" (valid alloc v2_0)) /\ (("CADUCEUS_20" (valid alloc u2)) /\ (("CADUCEUS_19" (valid alloc w)) /\ (("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" ((((((valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_19: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> ("CADUCEUS_25" (valid alloc m)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_20: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> ("CADUCEUS_25" (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_21: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> ("CADUCEUS_25" (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_22: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_23: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> ("CADUCEUS_25" (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_24: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> ("CADUCEUS_32" (valid alloc u2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_25: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> ("CADUCEUS_32" (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_26: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_null_24:(memory int null_24). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> (("CADUCEUS_32" ((valid alloc u2) /\ (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))) -> (forall intM_null_24_0:(memory int null_24). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_24_0 (acc pp2_u2_35 u2 : (pointer null_24)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_24 intM_null_24_0 (pset_singleton (acc pp2_u2_35 u2 : (pointer null_24)) : (pset null_24))))) -> ("CADUCEUS_32" (valid alloc v2_0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_27: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_null_24:(memory int null_24). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall pp2_v2_37:(memory (pointer null_25) v2_37). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> (("CADUCEUS_32" ((valid alloc u2) /\ (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))) -> (forall intM_null_24_0:(memory int null_24). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_24_0 (acc pp2_u2_35 u2 : (pointer null_24)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_24 intM_null_24_0 (pset_singleton (acc pp2_u2_35 u2 : (pointer null_24)) : (pset null_24))))) -> ("CADUCEUS_32" (valid alloc (acc pp2_v2_37 v2_0 : (pointer null_25)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_28: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_null_24:(memory int null_24). (forall intM_null_25:(memory int null_25). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall pp2_v2_37:(memory (pointer null_25) v2_37). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> (("CADUCEUS_32" ((valid alloc u2) /\ (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))) -> (forall intM_null_24_0:(memory int null_24). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_24_0 (acc pp2_u2_35 u2 : (pointer null_24)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_24 intM_null_24_0 (pset_singleton (acc pp2_u2_35 u2 : (pointer null_24)) : (pset null_24))))) -> (("CADUCEUS_32" ((valid alloc v2_0) /\ (valid alloc (acc pp2_v2_37 v2_0 : (pointer null_25))))) -> (forall intM_null_25_0:(memory int null_25). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_25_0 (acc pp2_v2_37 v2_0 : (pointer null_25)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_25 intM_null_25_0 (pset_singleton (acc pp2_v2_37 v2_0 : (pointer null_25)) : (pset null_25))))) -> ("CADUCEUS_24" (exists i:int. (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) i : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_29: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_null_24:(memory int null_24). (forall intM_null_25:(memory int null_25). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall pp2_v2_37:(memory (pointer null_25) v2_37). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> (("CADUCEUS_32" ((valid alloc u2) /\ (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))) -> (forall intM_null_24_0:(memory int null_24). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_24_0 (acc pp2_u2_35 u2 : (pointer null_24)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_24 intM_null_24_0 (pset_singleton (acc pp2_u2_35 u2 : (pointer null_24)) : (pset null_24))))) -> (("CADUCEUS_32" ((valid alloc v2_0) /\ (valid alloc (acc pp2_v2_37 v2_0 : (pointer null_25))))) -> (forall intM_null_25_0:(memory int null_25). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_25_0 (acc pp2_v2_37 v2_0 : (pointer null_25)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_25 intM_null_25_0 (pset_singleton (acc pp2_v2_37 v2_0 : (pointer null_25)) : (pset null_25))))) -> ("CADUCEUS_24" (exists i:int. (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) i : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) goal F_impl_po_30: (forall alloc:alloc_table. (forall intM_null_20:(memory int null_20). (forall intM_null_21:(memory int null_21). (forall intM_null_22:(memory int null_22). (forall intM_null_23:(memory int null_23). (forall intM_null_24:(memory int null_24). (forall intM_null_25:(memory int null_25). (forall intM_p1_0_42:(memory int p1_0_42). (forall intM_p1_0_45:(memory int p1_0_45). (forall intM_p1_0_48:(memory int p1_0_48). (forall intM_p1_0_51:(memory int p1_0_51). (forall intM_p2_1_41:(memory int p2_1_41). (forall intM_p2_1_44:(memory int p2_1_44). (forall intM_p2_1_47:(memory int p2_1_47). (forall intM_p2_1_50:(memory int p2_1_50). (forall m:(pointer m_33). (forall p1_m_33:(memory (pointer p1_0_42) m_33). (forall p1_u_27:(memory (pointer p1_0_51) u_27). (forall p1_v_29:(memory (pointer p1_0_48) v_29). (forall p1_w_31:(memory (pointer p1_0_45) w_31). (forall p2_m_33:(memory (pointer p2_1_41) m_33). (forall p2_u_27:(memory (pointer p2_1_50) u_27). (forall p2_v_29:(memory (pointer p2_1_47) v_29). (forall p2_w_31:(memory (pointer p2_1_44) w_31). (forall pp1_m_33:(memory (pointer null_23) m_33). (forall pp1_u_27:(memory (pointer null_20) u_27). (forall pp1_v_29:(memory (pointer null_21) v_29). (forall pp1_w_31:(memory (pointer null_22) w_31). (forall pp2_u2_35:(memory (pointer null_24) u2_35). (forall pp2_v2_37:(memory (pointer null_25) v2_37). (forall u:(pointer u_27). (forall u2:(pointer u2_35). (forall v:(pointer v_29). (forall v1_m_33:(memory int m_33). (forall v1_u_27:(memory int u_27). (forall v1_v_29:(memory int v_29). (forall v1_w_31:(memory int w_31). (forall v2_0:(pointer v2_37). (forall v2_m_33:(memory int m_33). (forall v2_u_27:(memory int u_27). (forall v2_v_29:(memory int v_29). (forall v2_w_31:(memory int w_31). (forall w:(pointer w_31). (( ("CADUCEUS_1" (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ ( ("CADUCEUS_23" (valid alloc u)) /\ ( ("CADUCEUS_22" (valid alloc m)) /\ ( ("CADUCEUS_21" (valid alloc v2_0)) /\ ( ("CADUCEUS_20" (valid alloc u2)) /\ ( ("CADUCEUS_19" (valid alloc w)) /\ ( ("CADUCEUS_18" (valid alloc v)) /\ ( ("CADUCEUS_14" (valid_acc_range p2_u_27 5)) /\ ( ("CADUCEUS_15" (valid_acc_range p2_v_29 5)) /\ ( ("CADUCEUS_16" (valid_acc_range p2_w_31 5)) /\ ( ("CADUCEUS_17" (valid_acc_range p2_m_33 5)) /\ ( ("CADUCEUS_10" (valid_acc_range p1_u_27 5)) /\ ( ("CADUCEUS_11" (valid_acc_range p1_v_29 5)) /\ ( ("CADUCEUS_12" (valid_acc_range p1_w_31 5)) /\ ( ("CADUCEUS_13" (valid_acc_range p1_m_33 5)) /\ ( ("CADUCEUS_6" (valid_acc p2_u_27)) /\ ( ("CADUCEUS_7" (valid_acc p2_v_29)) /\ ( ("CADUCEUS_8" (valid_acc p2_w_31)) /\ ( ("CADUCEUS_9" (valid_acc p2_m_33)) /\ ( ("CADUCEUS_2" (valid_acc p1_u_27)) /\ ( ("CADUCEUS_3" (valid_acc p1_v_29)) /\ ( ("CADUCEUS_4" (valid_acc p1_w_31)) /\ ("CADUCEUS_5" (valid_acc p1_m_33)))))))))))))))))))))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc u) /\ (valid alloc (acc p1_u_27 u : (pointer p1_0_51)))) /\ (valid alloc (acc p2_u_27 u : (pointer p2_1_50)))) /\ (valid alloc (acc pp1_u_27 u : (pointer null_20)))) /\ (valid_range alloc (acc p1_u_27 u : (pointer p1_0_51)) 0 4)) /\ (valid_range alloc (acc p2_u_27 u : (pointer p2_1_50)) 0 4))) -> (forall intM_null_20_0:(memory int null_20). (forall intM_p1_0_51_0:(memory int p1_0_51). (forall intM_p2_1_50_0:(memory int p2_1_50). (forall v1_u_27_0:(memory int u_27). (forall v2_u_27_0:(memory int u_27). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_51_0 (shift (acc p1_u_27 u : (pointer p1_0_51)) 1 : (pointer p1_0_51)) : int) (acc v1_u_27_0 u : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_51 intM_p1_0_51_0 (pset_range (pset_singleton (acc p1_u_27 u : (pointer p1_0_51)) : (pset p1_0_51)) 0 5 : (pset p1_0_51))) /\ (not_assigns alloc intM_p2_1_50 intM_p2_1_50_0 (pset_range (pset_singleton (acc p2_u_27 u : (pointer p2_1_50)) : (pset p2_1_50)) 0 5 : (pset p2_1_50)))) /\ (not_assigns alloc intM_null_20 intM_null_20_0 (pset_singleton (acc pp1_u_27 u : (pointer null_20)) : (pset null_20)))) /\ (not_assigns alloc v1_u_27 v1_u_27_0 (pset_singleton u : (pset u_27)))) /\ (not_assigns alloc v2_u_27 v2_u_27_0 (pset_singleton u : (pset u_27)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc v) /\ (valid alloc (acc p1_v_29 v : (pointer p1_0_48)))) /\ (valid alloc (acc p2_v_29 v : (pointer p2_1_47)))) /\ (valid alloc (acc pp1_v_29 v : (pointer null_21)))) /\ (valid_range alloc (acc p1_v_29 v : (pointer p1_0_48)) 0 4)) /\ (valid_range alloc (acc p2_v_29 v : (pointer p2_1_47)) 0 4))) -> (forall intM_null_21_0:(memory int null_21). (forall intM_p1_0_48_0:(memory int p1_0_48). (forall intM_p2_1_47_0:(memory int p2_1_47). (forall v1_v_29_0:(memory int v_29). (forall v2_v_29_0:(memory int v_29). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_48_0 (shift (acc p1_v_29 v : (pointer p1_0_48)) 1 : (pointer p1_0_48)) : int) (acc v1_v_29_0 v : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_48 intM_p1_0_48_0 (pset_range (pset_singleton (acc p1_v_29 v : (pointer p1_0_48)) : (pset p1_0_48)) 0 5 : (pset p1_0_48))) /\ (not_assigns alloc intM_p2_1_47 intM_p2_1_47_0 (pset_range (pset_singleton (acc p2_v_29 v : (pointer p2_1_47)) : (pset p2_1_47)) 0 5 : (pset p2_1_47)))) /\ (not_assigns alloc intM_null_21 intM_null_21_0 (pset_singleton (acc pp1_v_29 v : (pointer null_21)) : (pset null_21)))) /\ (not_assigns alloc v1_v_29 v1_v_29_0 (pset_singleton v : (pset v_29)))) /\ (not_assigns alloc v2_v_29 v2_v_29_0 (pset_singleton v : (pset v_29)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc w) /\ (valid alloc (acc p1_w_31 w : (pointer p1_0_45)))) /\ (valid alloc (acc p2_w_31 w : (pointer p2_1_44)))) /\ (valid alloc (acc pp1_w_31 w : (pointer null_22)))) /\ (valid_range alloc (acc p1_w_31 w : (pointer p1_0_45)) 0 4)) /\ (valid_range alloc (acc p2_w_31 w : (pointer p2_1_44)) 0 4))) -> (forall intM_null_22_0:(memory int null_22). (forall intM_p1_0_45_0:(memory int p1_0_45). (forall intM_p2_1_44_0:(memory int p2_1_44). (forall v1_w_31_0:(memory int w_31). (forall v2_w_31_0:(memory int w_31). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) 1 : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_45 intM_p1_0_45_0 (pset_range (pset_singleton (acc p1_w_31 w : (pointer p1_0_45)) : (pset p1_0_45)) 0 5 : (pset p1_0_45))) /\ (not_assigns alloc intM_p2_1_44 intM_p2_1_44_0 (pset_range (pset_singleton (acc p2_w_31 w : (pointer p2_1_44)) : (pset p2_1_44)) 0 5 : (pset p2_1_44)))) /\ (not_assigns alloc intM_null_22 intM_null_22_0 (pset_singleton (acc pp1_w_31 w : (pointer null_22)) : (pset null_22)))) /\ (not_assigns alloc v1_w_31 v1_w_31_0 (pset_singleton w : (pset w_31)))) /\ (not_assigns alloc v2_w_31 v2_w_31_0 (pset_singleton w : (pset w_31)))))) -> (("CADUCEUS_25" (( ( ( ( (valid alloc m) /\ (valid alloc (acc p1_m_33 m : (pointer p1_0_42)))) /\ (valid alloc (acc p2_m_33 m : (pointer p2_1_41)))) /\ (valid alloc (acc pp1_m_33 m : (pointer null_23)))) /\ (valid_range alloc (acc p1_m_33 m : (pointer p1_0_42)) 0 4)) /\ (valid_range alloc (acc p2_m_33 m : (pointer p2_1_41)) 0 4))) -> (forall intM_null_23_0:(memory int null_23). (forall intM_p1_0_42_0:(memory int p1_0_42). (forall intM_p2_1_41_0:(memory int p2_1_41). (forall v1_m_33_0:(memory int m_33). (forall v2_m_33_0:(memory int m_33). (( ("CADUCEUS_31" (Int.(<=) (acc intM_p1_0_42_0 (shift (acc p1_m_33 m : (pointer p1_0_42)) 1 : (pointer p1_0_42)) : int) (acc v1_m_33_0 m : int))) /\ ("CADUCEUS_30" ( ( ( ( (not_assigns alloc intM_p1_0_42 intM_p1_0_42_0 (pset_range (pset_singleton (acc p1_m_33 m : (pointer p1_0_42)) : (pset p1_0_42)) 0 5 : (pset p1_0_42))) /\ (not_assigns alloc intM_p2_1_41 intM_p2_1_41_0 (pset_range (pset_singleton (acc p2_m_33 m : (pointer p2_1_41)) : (pset p2_1_41)) 0 5 : (pset p2_1_41)))) /\ (not_assigns alloc intM_null_23 intM_null_23_0 (pset_singleton (acc pp1_m_33 m : (pointer null_23)) : (pset null_23)))) /\ (not_assigns alloc v1_m_33 v1_m_33_0 (pset_singleton m : (pset m_33)))) /\ (not_assigns alloc v2_m_33 v2_m_33_0 (pset_singleton m : (pset m_33)))))) -> (("CADUCEUS_32" ((valid alloc u2) /\ (valid alloc (acc pp2_u2_35 u2 : (pointer null_24))))) -> (forall intM_null_24_0:(memory int null_24). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_24_0 (acc pp2_u2_35 u2 : (pointer null_24)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_24 intM_null_24_0 (pset_singleton (acc pp2_u2_35 u2 : (pointer null_24)) : (pset null_24))))) -> (("CADUCEUS_32" ((valid alloc v2_0) /\ (valid alloc (acc pp2_v2_37 v2_0 : (pointer null_25))))) -> (forall intM_null_25_0:(memory int null_25). (( ("CADUCEUS_34" (Int.(>=) (acc intM_null_25_0 (acc pp2_v2_37 v2_0 : (pointer null_25)) : int) 5)) /\ ("CADUCEUS_33" (not_assigns alloc intM_null_25 intM_null_25_0 (pset_singleton (acc pp2_v2_37 v2_0 : (pointer null_25)) : (pset null_25))))) -> ("CADUCEUS_24" (exists i:int. (Int.(<=) (acc intM_p1_0_45_0 (shift (acc p1_w_31 w : (pointer p1_0_45)) i : (pointer p1_0_45)) : int) (acc v1_w_31_0 w : int)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) end