bench/encoding/why2/caduceus/pi_again_why.why

   1 logic eq_unit : unit, unit -> prop
   2
   3 logic neq_unit : unit, unit -> prop
   4
   5 logic eq_bool : bool, bool -> prop
   6
   7 logic neq_bool : bool, bool -> prop
   8
   9 logic lt_int : int, int -> prop
  10
  11 logic le_int : int, int -> prop
  12
  13 logic gt_int : int, int -> prop
  14
  15 logic ge_int : int, int -> prop
  16
  17 logic eq_int : int, int -> prop
  18
  19 logic neq_int : int, int -> prop
  20
  21 logic add_int : int, int -> int
  22
  23 logic sub_int : int, int -> int
  24
  25 logic mul_int : int, int -> int
  26
  27 logic div_int : int, int -> int
  28
  29 logic mod_int : int, int -> int
  30
  31 logic neg_int : int -> int
  32
  33 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
  34
  35 logic lt_real : real, real -> prop
  36
  37 logic le_real : real, real -> prop
  38
  39 logic gt_real : real, real -> prop
  40
  41 logic ge_real : real, real -> prop
  42
  43 logic eq_real : real, real -> prop
  44
  45 logic neq_real : real, real -> prop
  46
  47 logic add_real : real, real -> real
  48
  49 logic sub_real : real, real -> real
  50
  51 logic mul_real : real, real -> real
  52
  53 logic div_real : real, real -> real
  54
  55 logic neg_real : real -> real
  56
  57 logic real_of_int : int -> real
  58
  59 logic int_of_real : real -> int
  60
  61 logic lt_real_bool : real, real -> bool
  62
  63 logic le_real_bool : real, real -> bool
  64
  65 logic gt_real_bool : real, real -> bool
  66
  67 logic ge_real_bool : real, real -> bool
  68
  69 logic eq_real_bool : real, real -> bool
  70
  71 logic neq_real_bool : real, real -> bool
  72
  73 axiom lt_real_bool_axiom:
  74   (forall x:real. (forall y:real. ((lt_real_bool(x, y) = true) <-> (x < y))))
  75
  76 axiom le_real_bool_axiom:
  77   (forall x:real.
  78     (forall y:real. ((le_real_bool(x, y) = true) <-> (x <= y))))
  79
  80 axiom gt_real_bool_axiom:
  81   (forall x:real. (forall y:real. ((gt_real_bool(x, y) = true) <-> (x > y))))
  82
  83 axiom ge_real_bool_axiom:
  84   (forall x:real.
  85     (forall y:real. ((ge_real_bool(x, y) = true) <-> (x >= y))))
  86
  87 axiom eq_real_bool_axiom:
  88   (forall x:real. (forall y:real. ((eq_real_bool(x, y) = true) <-> (x = y))))
  89
  90 axiom neq_real_bool_axiom:
  91   (forall x:real.
  92     (forall y:real. ((neq_real_bool(x, y) = true) <-> (x <> y))))
  93
  94 logic real_max : real, real -> real
  95
  96 logic real_min : real, real -> real
  97
  98 axiom real_max_is_ge:
  99   (forall x:real.
 100     (forall y:real. ((real_max(x, y) >= x) and (real_max(x, y) >= y))))
 101
 102 axiom real_max_is_some:
 103   (forall x:real.
 104     (forall y:real. ((real_max(x, y) = x) or (real_max(x, y) = y))))
 105
 106 axiom real_min_is_le:
 107   (forall x:real.
 108     (forall y:real. ((real_min(x, y) <= x) and (real_min(x, y) <= y))))
 109
 110 axiom real_min_is_some:
 111   (forall x:real.
 112     (forall y:real. ((real_min(x, y) = x) or (real_min(x, y) = y))))
 113
 114 logic sqrt_real : real -> real
 115
 116 logic pow_real : real, real -> real
 117
 118 logic abs_real : real -> real
 119
 120 axiom abs_real_pos:
 121   (forall x:real [abs_real(x)]. ((x >= 0.0) -> (abs_real(x) = x)))
 122
 123 axiom abs_real_neg:
 124   (forall x:real [abs_real(x)]. ((x <= 0.0) -> (abs_real(x) = (-x))))
 125
 126 logic exp : real -> real
 127
 128 logic log : real -> real
 129
 130 logic log10 : real -> real
 131
 132 axiom log_exp: (forall x:real. (log(exp(x)) = x))
 133
 134 logic cos : real -> real
 135
 136 logic sin : real -> real
 137
 138 logic tan : real -> real
 139
 140 logic cosh : real -> real
 141
 142 logic sinh : real -> real
 143
 144 logic tanh : real -> real
 145
 146 logic acos : real -> real
 147
 148 logic asin : real -> real
 149
 150 logic atan : real -> real
 151
 152 logic atan2 : real, real -> real
 153
 154 logic hypot : real, real -> real
 155
 156 axiom prod_pos:
 157   (forall x:real.
 158     (forall y:real.
 159       ((((x > 0.0) and (y > 0.0)) -> ((x * y) > 0.0)) and
 160        (((x < 0.0) and (y < 0.0)) -> ((x * y) > 0.0)))))
 161
 162 axiom abs_minus: (forall x:real. (abs_real((-x)) = abs_real(x)))
 163
 164 type mode
 165
 166 logic nearest_even : mode
 167
 168 logic to_zero : mode
 169
 170 logic up : mode
 171
 172 logic down : mode
 173
 174 logic nearest_away : mode
 175
 176 type single
 177
 178 logic add_single : mode, single, single -> single
 179
 180 logic sub_single : mode, single, single -> single
 181
 182 logic mul_single : mode, single, single -> single
 183
 184 logic div_single : mode, single, single -> single
 185
 186 logic neg_single : mode, single -> single
 187
 188 logic abs_single : mode, single -> single
 189
 190 logic sqrt_single : mode, single -> single
 191
 192 logic s_to_r : single -> real
 193
 194 logic s_to_exact : single -> real
 195
 196 logic s_to_model : single -> real
 197
 198 logic r_to_s : mode, real -> single
 199
 200 logic single_round_error : single -> real
 201
 202 logic single_total_error : single -> real
 203
 204 logic single_set_model : single, real -> single
 205
 206 logic max_single : real
 207
 208 type double
 209
 210 logic add_double : mode, double, double -> double
 211
 212 logic sub_double : mode, double, double -> double
 213
 214 logic mul_double : mode, double, double -> double
 215
 216 logic div_double : mode, double, double -> double
 217
 218 logic neg_double : mode, double -> double
 219
 220 logic abs_double : mode, double -> double
 221
 222 logic sqrt_double : mode, double -> double
 223
 224 logic d_to_r : double -> real
 225
 226 logic d_to_exact : double -> real
 227
 228 logic d_to_model : double -> real
 229
 230 logic r_to_d : mode, real -> double
 231
 232 logic double_round_error : double -> real
 233
 234 logic double_total_error : double -> real
 235
 236 logic double_set_model : double, real -> double
 237
 238 predicate eq_double(x: double, y: double) = (d_to_r(x) = d_to_r(y))
 239
 240 predicate neq_double(x: double, y: double) = (d_to_r(x) <> d_to_r(y))
 241
 242 predicate lt_double(x: double, y: double) = (d_to_r(x) < d_to_r(y))
 243
 244 predicate gt_double(x: double, y: double) = (d_to_r(x) > d_to_r(y))
 245
 246 predicate le_double(x: double, y: double) = (d_to_r(x) <= d_to_r(y))
 247
 248 predicate ge_double(x: double, y: double) = (d_to_r(x) >= d_to_r(y))
 249
 250 logic max_double : real
 251
 252 logic lt_double_bool : double, double -> bool
 253
 254 logic le_double_bool : double, double -> bool
 255
 256 logic gt_double_bool : double, double -> bool
 257
 258 logic ge_double_bool : double, double -> bool
 259
 260 logic eq_double_bool : double, double -> bool
 261
 262 logic neq_double_bool : double, double -> bool
 263
 264 axiom lt_double_bool_axiom:
 265   (forall x:double.
 266     (forall y:double.
 267       ((lt_double_bool(x, y) = true) <-> (d_to_r(x) < d_to_r(y)))))
 268
 269 axiom le_double_bool_axiom:
 270   (forall x:double.
 271     (forall y:double.
 272       ((le_double_bool(x, y) = true) <-> (d_to_r(x) <= d_to_r(y)))))
 273
 274 axiom gt_double_bool_axiom:
 275   (forall x:double.
 276     (forall y:double.
 277       ((gt_double_bool(x, y) = true) <-> (d_to_r(x) > d_to_r(y)))))
 278
 279 axiom ge_double_bool_axiom:
 280   (forall x:double.
 281     (forall y:double.
 282       ((ge_double_bool(x, y) = true) <-> (d_to_r(x) >= d_to_r(y)))))
 283
 284 axiom eq_double_bool_axiom:
 285   (forall x:double.
 286     (forall y:double.
 287       ((eq_double_bool(x, y) = true) <-> (d_to_r(x) = d_to_r(y)))))
 288
 289 axiom neq_double_bool_axiom:
 290   (forall x:double.
 291     (forall y:double.
 292       ((neq_double_bool(x, y) = true) <-> (d_to_r(x) <> d_to_r(y)))))
 293
 294 type quad
 295
 296 logic add_quad : mode, quad, quad -> quad
 297
 298 logic sub_quad : mode, quad, quad -> quad
 299
 300 logic mul_quad : mode, quad, quad -> quad
 301
 302 logic div_quad : mode, quad, quad -> quad
 303
 304 logic neg_quad : mode, quad -> quad
 305
 306 logic abs_quad : mode, quad -> quad
 307
 308 logic sqrt_quad : mode, quad -> quad
 309
 310 logic q_to_r : quad -> real
 311
 312 logic q_to_exact : quad -> real
 313
 314 logic q_to_model : quad -> real
 315
 316 logic r_to_q : mode, real -> quad
 317
 318 logic quad_round_error : quad -> real
 319
 320 logic quad_total_error : quad -> real
 321
 322 logic quad_set_model : quad, real -> quad
 323
 324 logic max_quad : real
 325
 326 logic double_of_single : single -> double
 327
 328 logic single_of_double : mode, double -> single
 329
 330 logic quad_of_single : single -> quad
 331
 332 logic single_of_quad : mode, quad -> single
 333
 334 logic quad_of_double : double -> quad
 335
 336 logic double_of_quad : mode, quad -> double
 337
 338 logic bw_compl : int -> int
 339
 340 logic bw_and : int, int -> int
 341
 342 logic bw_xor : int, int -> int
 343
 344 logic bw_or : int, int -> int
 345
 346 logic lsl : int, int -> int
 347
 348 logic lsr : int, int -> int
 349
 350 type 'z pointer
 351
 352 type 'z addr
 353
 354 type alloc_table
 355
 356 logic block_length : alloc_table, 'a1 pointer -> int
 357
 358 logic base_addr : 'a1 pointer -> 'a1 addr
 359
 360 logic offset : 'a1 pointer -> int
 361
 362 logic shift : 'a1 pointer, int -> 'a1 pointer
 363
 364 logic sub_pointer : 'a1 pointer, 'a1 pointer -> int
 365
 366 predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
 367   ((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))
 368
 369 predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
 370   ((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))
 371
 372 predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
 373   ((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))
 374
 375 predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
 376   ((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))
 377
 378 predicate valid(a: alloc_table, p: 'a1 pointer) =
 379   ((0 <= offset(p)) and (offset(p) < block_length(a, p)))
 380
 381 predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
 382   ((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))
 383
 384 predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
 385   ((0 <= (offset(p) + i)) and ((offset(p) + j) < block_length(a, p)))
 386
 387 axiom offset_shift:
 388   (forall p:'a1 pointer.
 389     (forall i:int [offset(shift(p, i))]. (offset(shift(p,
 390       i)) = (offset(p) + i))))
 391
 392 axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))
 393
 394 axiom shift_shift:
 395   (forall p:'a1 pointer.
 396     (forall i:int.
 397       (forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
 398         j) = shift(p, (i + j))))))
 399
 400 axiom base_addr_shift:
 401   (forall p:'a1 pointer.
 402     (forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
 403       i)) = base_addr(p))))
 404
 405 axiom block_length_shift:
 406   (forall a:alloc_table.
 407     (forall p:'a1 pointer.
 408       (forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
 409         i)) = block_length(a, p)))))
 410
 411 axiom base_addr_block_length:
 412   (forall a:alloc_table.
 413     (forall p1:'a1 pointer.
 414       (forall p2:'a1 pointer.
 415         ((base_addr(p1) = base_addr(p2)) -> (block_length(a,
 416          p1) = block_length(a, p2))))))
 417
 418 axiom pointer_pair_1:
 419   (forall p1:'a1 pointer.
 420     (forall p2:'a1 pointer.
 421       (((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
 422        (p1 = p2))))
 423
 424 axiom pointer_pair_2:
 425   (forall p1:'a1 pointer.
 426     (forall p2:'a1 pointer.
 427       ((p1 = p2) ->
 428        ((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))
 429
 430 axiom neq_base_addr_neq_shift:
 431   (forall p1:'a1 pointer.
 432     (forall p2:'a1 pointer.
 433       (forall i:int.
 434         (forall j:int.
 435           ((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))
 436
 437 axiom neq_offset_neq_shift:
 438   (forall p1:'a1 pointer.
 439     (forall p2:'a1 pointer.
 440       (forall i:int.
 441         (forall j:int.
 442           (((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
 443            i) <> shift(p2, j)))))))
 444
 445 axiom eq_offset_eq_shift:
 446   (forall p1:'a1 pointer.
 447     (forall p2:'a1 pointer.
 448       (forall i:int.
 449         (forall j:int.
 450           ((base_addr(p1) = base_addr(p2)) ->
 451            (((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
 452             i) = shift(p2, j))))))))
 453
 454 axiom valid_index_valid_shift:
 455   (forall a:alloc_table.
 456     (forall p:'a1 pointer.
 457       (forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))
 458
 459 axiom valid_range_valid_shift:
 460   (forall a:alloc_table.
 461     (forall p:'a1 pointer.
 462       (forall i:int.
 463         (forall j:int.
 464           (forall k:int.
 465             (valid_range(a, p, i, j) ->
 466              (((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))
 467
 468 axiom valid_range_valid:
 469   (forall a:alloc_table.
 470     (forall p:'a1 pointer.
 471       (forall i:int.
 472         (forall j:int.
 473           (valid_range(a, p, i, j) ->
 474            (((i <= 0) and (0 <= j)) -> valid(a, p)))))))
 475
 476 axiom valid_range_valid_index:
 477   (forall a:alloc_table.
 478     (forall p:'a1 pointer.
 479       (forall i:int.
 480         (forall j:int.
 481           (forall k:int.
 482             (valid_range(a, p, i, j) ->
 483              (((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))
 484
 485 axiom sub_pointer_def:
 486   (forall p1:'a1 pointer.
 487     (forall p2:'a1 pointer.
 488       ((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
 489        p2) = (offset(p1) - offset(p2))))))
 490
 491 type ('a, 'z) memory
 492
 493 logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1
 494
 495 logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory
 496
 497 axiom acc_upd:
 498   (forall m:('a1, 'a2) memory.
 499     (forall p:'a2 pointer.
 500       (forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))
 501
 502 axiom acc_upd_neq:
 503   (forall m:('a1, 'a2) memory.
 504     (forall p1:'a2 pointer.
 505       (forall p2:'a2 pointer.
 506         (forall a:'a1 [acc(upd(m, p1, a), p2)].
 507           ((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))
 508
 509 axiom false_not_true: (false <> true)
 510
 511 type 'z pset
 512
 513 logic pset_empty : 'a1 pset
 514
 515 logic pset_singleton : 'a1 pointer -> 'a1 pset
 516
 517 logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 518
 519 logic pset_all : 'a1 pset -> 'a1 pset
 520
 521 logic pset_range : 'a1 pset, int, int -> 'a1 pset
 522
 523 logic pset_range_left : 'a1 pset, int -> 'a1 pset
 524
 525 logic pset_range_right : 'a1 pset, int -> 'a1 pset
 526
 527 logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 528
 529 logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
 530 int -> 'a1 pset
 531
 532 logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
 533 int -> 'a1 pset
 534
 535 logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
 536 int -> 'a1 pset
 537
 538 logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset
 539
 540 logic not_in_pset : 'a1 pointer, 'a1 pset -> prop
 541
 542 predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
 543   'a2) memory, l: 'a2 pset) =
 544   (forall p:'a2 pointer.
 545     (valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))
 546
 547 axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))
 548
 549 axiom pset_singleton_intro:
 550   (forall p1:'a1 pointer.
 551     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 552       ((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))
 553
 554 axiom pset_singleton_elim:
 555   (forall p1:'a1 pointer.
 556     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 557       (not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))
 558
 559 axiom not_not_in_singleton:
 560   (forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))
 561
 562 axiom pset_union_intro:
 563   (forall l1:'a1 pset.
 564     (forall l2:'a1 pset.
 565       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 566         ((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
 567          pset_union(l1, l2))))))
 568
 569 axiom pset_union_elim1:
 570   (forall l1:'a1 pset.
 571     (forall l2:'a1 pset.
 572       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 573         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))
 574
 575 axiom pset_union_elim2:
 576   (forall l1:'a1 pset.
 577     (forall l2:'a1 pset.
 578       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 579         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))
 580
 581 axiom pset_star_intro:
 582   (forall l:'a1 pset.
 583     (forall m:('a2 pointer, 'a1) memory.
 584       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 585         ((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
 586          not_in_pset(p, pset_star(l, m))))))
 587
 588 axiom pset_star_elim:
 589   (forall l:'a1 pset.
 590     (forall m:('a2 pointer, 'a1) memory.
 591       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 592         (not_in_pset(p, pset_star(l, m)) ->
 593          (forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))
 594
 595 axiom pset_all_intro:
 596   (forall p:'a1 pointer.
 597     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 598       ((forall p1:'a1 pointer.
 599          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
 600        not_in_pset(p, pset_all(l)))))
 601
 602 axiom pset_all_elim:
 603   (forall p:'a1 pointer.
 604     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 605       (not_in_pset(p, pset_all(l)) ->
 606        (forall p1:'a1 pointer.
 607          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))
 608
 609 axiom pset_range_intro:
 610   (forall p:'a1 pointer.
 611     (forall l:'a1 pset.
 612       (forall a:int.
 613         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 614           ((forall p1:'a1 pointer.
 615              (not_in_pset(p1, l) or
 616               (forall i:int.
 617                 (((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
 618            not_in_pset(p, pset_range(l, a, b)))))))
 619
 620 axiom pset_range_elim:
 621   (forall p:'a1 pointer.
 622     (forall l:'a1 pset.
 623       (forall a:int.
 624         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 625           (not_in_pset(p, pset_range(l, a, b)) ->
 626            (forall p1:'a1 pointer.
 627              ((not not_in_pset(p1, l)) ->
 628               (forall i:int.
 629                 (((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))
 630
 631 axiom pset_range_left_intro:
 632   (forall p:'a1 pointer.
 633     (forall l:'a1 pset.
 634       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 635         ((forall p1:'a1 pointer.
 636            (not_in_pset(p1, l) or
 637             (forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
 638          not_in_pset(p, pset_range_left(l, a))))))
 639
 640 axiom pset_range_left_elim:
 641   (forall p:'a1 pointer.
 642     (forall l:'a1 pset.
 643       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 644         (not_in_pset(p, pset_range_left(l, a)) ->
 645          (forall p1:'a1 pointer.
 646            ((not not_in_pset(p1, l)) ->
 647             (forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))
 648
 649 axiom pset_range_right_intro:
 650   (forall p:'a1 pointer.
 651     (forall l:'a1 pset.
 652       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 653         ((forall p1:'a1 pointer.
 654            (not_in_pset(p1, l) or
 655             (forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->
 656          not_in_pset(p, pset_range_right(l, a))))))
 657
 658 axiom pset_range_right_elim:
 659   (forall p:'a1 pointer.
 660     (forall l:'a1 pset.
 661       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 662         (not_in_pset(p, pset_range_right(l, a)) ->
 663          (forall p1:'a1 pointer.
 664            ((not not_in_pset(p1, l)) ->
 665             (forall i:int. ((a <= i) -> (shift(p1, i) <> p)))))))))
 666
 667 axiom pset_acc_all_intro:
 668   (forall p:'a1 pointer.
 669     (forall l:'a2 pset.
 670       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 671         m))].
 672         ((forall p1:'a2 pointer.
 673            ((not not_in_pset(p1, l)) ->
 674             (forall i:int. (p <> acc(m, shift(p1, i)))))) ->
 675          not_in_pset(p, pset_acc_all(l, m))))))
 676
 677 axiom pset_acc_all_elim:
 678   (forall p:'a1 pointer.
 679     (forall l:'a2 pset.
 680       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 681         m))].
 682         (not_in_pset(p, pset_acc_all(l, m)) ->
 683          (forall p1:'a2 pointer.
 684            ((not not_in_pset(p1, l)) ->
 685             (forall i:int. (acc(m, shift(p1, i)) <> p))))))))
 686
 687 axiom pset_acc_range_intro:
 688   (forall p:'a1 pointer.
 689     (forall l:'a2 pset.
 690       (forall m:('a1 pointer, 'a2) memory.
 691         (forall a:int.
 692           (forall b:int [not_in_pset(p, pset_acc_range(l, m, a, b))].
 693             ((forall p1:'a2 pointer.
 694                ((not not_in_pset(p1, l)) ->
 695                 (forall i:int.
 696                   (((a <= i) and (i <= b)) -> (p <> acc(m, shift(p1, i))))))) ->
 697              not_in_pset(p, pset_acc_range(l, m, a, b))))))))
 698
 699 axiom pset_acc_range_elim:
 700   (forall p:'a1 pointer.
 701     (forall l:'a2 pset.
 702       (forall m:('a1 pointer, 'a2) memory.
 703         (forall a:int.
 704           (forall b:int.
 705             (not_in_pset(p, pset_acc_range(l, m, a, b)) ->
 706              (forall p1:'a2 pointer.
 707                ((not not_in_pset(p1, l)) ->
 708                 (forall i:int.
 709                   (((a <= i) and (i <= b)) -> (acc(m, shift(p1, i)) <> p)))))))))))
 710
 711 axiom pset_acc_range_left_intro:
 712   (forall p:'a1 pointer.
 713     (forall l:'a2 pset.
 714       (forall m:('a1 pointer, 'a2) memory.
 715         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 716           ((forall p1:'a2 pointer.
 717              ((not not_in_pset(p1, l)) ->
 718               (forall i:int. ((i <= a) -> (p <> acc(m, shift(p1, i))))))) ->
 719            not_in_pset(p, pset_acc_range_left(l, m, a)))))))
 720
 721 axiom pset_acc_range_left_elim:
 722   (forall p:'a1 pointer.
 723     (forall l:'a2 pset.
 724       (forall m:('a1 pointer, 'a2) memory.
 725         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 726           (not_in_pset(p, pset_acc_range_left(l, m, a)) ->
 727            (forall p1:'a2 pointer.
 728              ((not not_in_pset(p1, l)) ->
 729               (forall i:int. ((i <= a) -> (acc(m, shift(p1, i)) <> p))))))))))
 730
 731 axiom pset_acc_range_right_intro:
 732   (forall p:'a1 pointer.
 733     (forall l:'a2 pset.
 734       (forall m:('a1 pointer, 'a2) memory.
 735         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 736           ((forall p1:'a2 pointer.
 737              ((not not_in_pset(p1, l)) ->
 738               (forall i:int. ((a <= i) -> (p <> acc(m, shift(p1, i))))))) ->
 739            not_in_pset(p, pset_acc_range_right(l, m, a)))))))
 740
 741 axiom pset_acc_range_right_elim:
 742   (forall p:'a1 pointer.
 743     (forall l:'a2 pset.
 744       (forall m:('a1 pointer, 'a2) memory.
 745         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 746           (not_in_pset(p, pset_acc_range_right(l, m, a)) ->
 747            (forall p1:'a2 pointer.
 748              ((not not_in_pset(p1, l)) ->
 749               (forall i:int. ((a <= i) -> (acc(m, shift(p1, i)) <> p))))))))))
 750
 751 axiom not_assigns_trans:
 752   (forall a:alloc_table.
 753     (forall l:'a1 pset.
 754       (forall m1:('a2, 'a1) memory.
 755         (forall m2:('a2, 'a1) memory.
 756           (forall m3:('a2, 'a1) memory.
 757             (not_assigns(a, m1, m2, l) ->
 758              (not_assigns(a, m2, m3, l) -> not_assigns(a, m1, m3, l))))))))
 759
 760 axiom not_assigns_refl:
 761   (forall a:alloc_table.
 762     (forall l:'a1 pset.
 763       (forall m:('a2, 'a1) memory. not_assigns(a, m, m, l))))
 764
 765 predicate valid_acc(m1: ('a1 pointer, 'a2) memory) =
 766   (forall p:'a2 pointer.
 767     (forall a:alloc_table. (valid(a, p) -> valid(a, acc(m1, p)))))
 768
 769 predicate valid_acc_range(m1: ('a1 pointer, 'a2) memory, size: int) =
 770   (forall p:'a2 pointer.
 771     (forall a:alloc_table.
 772       (valid(a, p) -> valid_range(a, acc(m1, p), 0, (size - 1)))))
 773
 774 axiom valid_acc_range_valid:
 775   (forall m1:('a1 pointer, 'a2) memory.
 776     (forall size:int.
 777       (forall p:'a2 pointer.
 778         (forall a:alloc_table.
 779           (valid_acc_range(m1, size) -> (valid(a, p) -> valid(a, acc(m1, p))))))))
 780
 781 predicate separation1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 782   'a2) memory) =
 783   (forall p:'a2 pointer.
 784     (forall a:alloc_table.
 785       (valid(a, p) -> (base_addr(acc(m1, p)) <> base_addr(acc(m2, p))))))
 786
 787 predicate separation1_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 788   'a2) memory, size: int) =
 789   (forall p:'a2 pointer.
 790     (forall a:alloc_table.
 791       (valid(a, p) ->
 792        (forall i1:int.
 793          (forall i2:int.
 794            (((0 <= i1) and (i1 < size)) ->
 795             (((0 <= i2) and (i2 < size)) -> (base_addr(acc(m1, shift(p,
 796              i1))) <> base_addr(acc(m2, shift(p, i2)))))))))))
 797
 798 predicate separation1_range(m: ('a1 pointer, 'a2) memory, size: int) =
 799   (forall p:'a2 pointer.
 800     (forall a:alloc_table.
 801       (valid(a, p) ->
 802        (forall i1:int.
 803          (((0 <= i1) and (i1 < size)) -> (base_addr(acc(m, shift(p,
 804           i1))) <> base_addr(acc(m, p))))))))
 805
 806 predicate separation2(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 807   'a2) memory) =
 808   (forall p1:'a2 pointer.
 809     (forall p2:'a2 pointer.
 810       ((p1 <> p2) -> (base_addr(acc(m1, p1)) <> base_addr(acc(m2, p2))))))
 811
 812 predicate separation2_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 813   'a2) memory, size: int) =
 814   (forall p:'a2 pointer.
 815     (forall q:'a2 pointer.
 816       (forall a:alloc_table.
 817         (forall i:int.
 818           (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
 819            i))) <> base_addr(acc(m2, q))))))))
 820
 821 logic on_heap : alloc_table, 'a1 pointer -> prop
 822
 823 logic on_stack : alloc_table, 'a1 pointer -> prop
 824
 825 logic fresh : alloc_table, 'a1 pointer -> prop
 826
 827 axiom fresh_not_valid:
 828   (forall a:alloc_table.
 829     (forall p:'a1 pointer. (fresh(a, p) -> (not valid(a, p)))))
 830
 831 axiom fresh_not_valid_shift:
 832   (forall a:alloc_table.
 833     (forall p:'a1 pointer.
 834       (fresh(a, p) -> (forall i:int. (not valid(a, shift(p, i)))))))
 835
 836 logic alloc_extends : alloc_table, alloc_table -> prop
 837
 838 axiom alloc_extends_valid:
 839   (forall a1:alloc_table.
 840     (forall a2:alloc_table.
 841       (alloc_extends(a1, a2) ->
 842        (forall q:'a1 pointer. (valid(a1, q) -> valid(a2, q))))))
 843
 844 axiom alloc_extends_valid_index:
 845   (forall a1:alloc_table.
 846     (forall a2:alloc_table.
 847       (alloc_extends(a1, a2) ->
 848        (forall q:'a1 pointer.
 849          (forall i:int. (valid_index(a1, q, i) -> valid_index(a2, q, i)))))))
 850
 851 axiom alloc_extends_valid_range:
 852   (forall a1:alloc_table.
 853     (forall a2:alloc_table.
 854       (alloc_extends(a1, a2) ->
 855        (forall q:'a1 pointer.
 856          (forall i:int.
 857            (forall j:int.
 858              (valid_range(a1, q, i, j) -> valid_range(a2, q, i, j))))))))
 859
 860 axiom alloc_extends_refl: (forall a:alloc_table. alloc_extends(a, a))
 861
 862 axiom alloc_extends_trans:
 863   (forall a1:alloc_table.
 864     (forall a2:alloc_table.
 865       (forall a3:alloc_table [alloc_extends(a1, a2), alloc_extends(a2, a3)].
 866         (alloc_extends(a1, a2) ->
 867          (alloc_extends(a2, a3) -> alloc_extends(a1, a3))))))
 868
 869 logic free_stack : alloc_table, alloc_table, alloc_table -> prop
 870
 871 axiom free_stack_heap:
 872   (forall a1:alloc_table.
 873     (forall a2:alloc_table.
 874       (forall a3:alloc_table.
 875         (free_stack(a1, a2, a3) ->
 876          (forall p:'a1 pointer.
 877            (valid(a2, p) -> (on_heap(a2, p) -> valid(a3, p))))))))
 878
 879 axiom free_stack_stack:
 880   (forall a1:alloc_table.
 881     (forall a2:alloc_table.
 882       (forall a3:alloc_table.
 883         (free_stack(a1, a2, a3) ->
 884          (forall p:'a1 pointer.
 885            (valid(a1, p) -> (on_stack(a1, p) -> valid(a3, p))))))))
 886
 887 logic null : 'a1 pointer
 888
 889 axiom null_not_valid: (forall a:alloc_table. (not valid(a, null)))
 890
 891 type a_0
 892
 893 type a_1
 894
 895 type a_2
 896
 897 goal main_impl_po_1:
 898   forall a:a_2 pointer.
 899   forall alloc:alloc_table.
 900   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
 901   forall mutable_x:int.
 902   forall p:int.
 903   (p <> 0) ->
 904   (mutable_x <> 0)
 905
 906 goal main_impl_po_2:
 907   forall a:a_2 pointer.
 908   forall alloc:alloc_table.
 909   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
 910   forall g:int.
 911   forall mutable_x:int.
 912   forall p:int.
 913   (p <> 0) ->
 914   (mutable_x <> 0) ->
 915   forall result:int.
 916   (result = (g / mutable_x)) ->
 917   forall result0:a_2 pointer.
 918   (result0 = shift(a, p)) ->
 919   valid(alloc, result0)
 920
 921 goal main_impl_po_3:
 922   forall a:a_2 pointer.
 923   forall alloc:alloc_table.
 924   forall i:int.
 925   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
 926   forall g:int.
 927   forall intM_a_2:(int,
 928   a_2) memory.
 929   forall mutable_x:int.
 930   forall o:int.
 931   forall p:int.
 932   (p <> 0) ->
 933   (mutable_x <> 0) ->
 934   forall result:int.
 935   (result = (g / mutable_x)) ->
 936   forall result0:a_2 pointer.
 937   (result0 = shift(a, p)) ->
 938   valid(alloc, result0) ->
 939   forall result1:int.
 940   (result1 = acc(intM_a_2, result0)) ->
 941   (o = 0) ->
 942   forall g0:int.
 943   (g0 = (((result * p) + (result1 * i)) + (2 * 1))) ->
 944   (g0 <> 0) ->
 945   forall mutable_x0:int.
 946   (mutable_x0 = ((p * 2) - 1)) ->
 947   forall p0:int.
 948   (p0 = (p - 1)) ->
 949   forall result2:a_2 pointer.
 950   (result2 = shift(a, p)) ->
 951   (mutable_x0 <> 0)
 952
 953 goal main_impl_po_4:
 954   forall a:a_2 pointer.
 955   forall alloc:alloc_table.
 956   forall i:int.
 957   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
 958   forall g:int.
 959   forall intM_a_2:(int,
 960   a_2) memory.
 961   forall mutable_x:int.
 962   forall o:int.
 963   forall p:int.
 964   (p <> 0) ->
 965   (mutable_x <> 0) ->
 966   forall result:int.
 967   (result = (g / mutable_x)) ->
 968   forall result0:a_2 pointer.
 969   (result0 = shift(a, p)) ->
 970   valid(alloc, result0) ->
 971   forall result1:int.
 972   (result1 = acc(intM_a_2, result0)) ->
 973   (o = 0) ->
 974   forall g0:int.
 975   (g0 = (((result * p) + (result1 * i)) + (2 * 1))) ->
 976   (g0 <> 0) ->
 977   forall mutable_x0:int.
 978   (mutable_x0 = ((p * 2) - 1)) ->
 979   forall p0:int.
 980   (p0 = (p - 1)) ->
 981   forall result2:a_2 pointer.
 982   (result2 = shift(a, p)) ->
 983   (mutable_x0 <> 0) ->
 984   forall result3:int.
 985   (result3 = (g0 % mutable_x0)) ->
 986   valid(alloc, result2)
 987
 988 goal main_impl_po_5:
 989   forall a:a_2 pointer.
 990   forall alloc:alloc_table.
 991   forall i:int.
 992   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
 993   forall g:int.
 994   forall intM_a_2:(int,
 995   a_2) memory.
 996   forall mutable_x:int.
 997   forall o:int.
 998   forall p:int.
 999   (p <> 0) ->
1000   (mutable_x <> 0) ->
1001   forall result:int.
1002   (result = (g / mutable_x)) ->
1003   forall result0:a_2 pointer.
1004   (result0 = shift(a, p)) ->
1005   valid(alloc, result0) ->
1006   forall result1:int.
1007   (result1 = acc(intM_a_2, result0)) ->
1008   (o <> 0) ->
1009   forall g0:int.
1010   (g0 = (((result * p) + (result1 * i)) + (2 * 0))) ->
1011   (g0 <> 0) ->
1012   forall mutable_x0:int.
1013   (mutable_x0 = ((p * 2) - 1)) ->
1014   forall p0:int.
1015   (p0 = (p - 1)) ->
1016   forall result2:a_2 pointer.
1017   (result2 = shift(a, p)) ->
1018   (mutable_x0 <> 0)
1019
1020 goal main_impl_po_6:
1021   forall a:a_2 pointer.
1022   forall alloc:alloc_table.
1023   forall i:int.
1024   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
1025   forall g:int.
1026   forall intM_a_2:(int,
1027   a_2) memory.
1028   forall mutable_x:int.
1029   forall o:int.
1030   forall p:int.
1031   (p <> 0) ->
1032   (mutable_x <> 0) ->
1033   forall result:int.
1034   (result = (g / mutable_x)) ->
1035   forall result0:a_2 pointer.
1036   (result0 = shift(a, p)) ->
1037   valid(alloc, result0) ->
1038   forall result1:int.
1039   (result1 = acc(intM_a_2, result0)) ->
1040   (o <> 0) ->
1041   forall g0:int.
1042   (g0 = (((result * p) + (result1 * i)) + (2 * 0))) ->
1043   (g0 <> 0) ->
1044   forall mutable_x0:int.
1045   (mutable_x0 = ((p * 2) - 1)) ->
1046   forall p0:int.
1047   (p0 = (p - 1)) ->
1048   forall result2:a_2 pointer.
1049   (result2 = shift(a, p)) ->
1050   (mutable_x0 <> 0) ->
1051   forall result3:int.
1052   (result3 = (g0 % mutable_x0)) ->
1053   valid(alloc, result2)
1054
1055 goal main_impl_po_7:
1056   forall a:a_2 pointer.
1057   forall alloc:alloc_table.
1058   forall i:int.
1059   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
1060   forall p:int.
1061   (p = 0) ->
1062   (i <> 0)
1063
1064 goal main_impl_po_8:
1065   forall a:a_2 pointer.
1066   forall alloc:alloc_table.
1067   forall i:int.
1068   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
1069   forall g:int.
1070   forall p:int.
1071   (p = 0) ->
1072   (i <> 0) ->
1073   forall result:int.
1074   (result = (g / i)) ->
1075   forall p0:int.
1076   (p0 = i) ->
1077   (i <> 0) ->
1078   forall result0:int.
1079   (result0 = (g % i)) ->
1080   forall o0:int.
1081   (o0 = result0) ->
1082   (bw_xor(53, o0) <> 0) ->
1083   forall mutable_x0:int.
1084   (mutable_x0 = ((p0 * 2) - 1)) ->
1085   forall p1:int.
1086   (p1 = (p0 - 1)) ->
1087   forall result1:a_2 pointer.
1088   (result1 = shift(a, p0)) ->
1089   (mutable_x0 <> 0)
1090
1091 goal main_impl_po_9:
1092   forall a:a_2 pointer.
1093   forall alloc:alloc_table.
1094   forall i:int.
1095   ("CADUCEUS_1": valid_range(alloc, a, 0, 10000)) ->
1096   forall g:int.
1097   forall p:int.
1098   (p = 0) ->
1099   (i <> 0) ->
1100   forall result:int.
1101   (result = (g / i)) ->
1102   forall p0:int.
1103   (p0 = i) ->
1104   (i <> 0) ->
1105   forall result0:int.
1106   (result0 = (g % i)) ->
1107   forall o0:int.
1108   (o0 = result0) ->
1109   (bw_xor(53, o0) <> 0) ->
1110   forall mutable_x0:int.
1111   (mutable_x0 = ((p0 * 2) - 1)) ->
1112   forall p1:int.
1113   (p1 = (p0 - 1)) ->
1114   forall result1:a_2 pointer.
1115   (result1 = shift(a, p0)) ->
1116   (mutable_x0 <> 0) ->
1117   forall result2:int.
1118   (result2 = (g % mutable_x0)) ->
1119   valid(alloc, result1)
1120