src/HOL/Boogie/Examples/Boogie_Max.b2i
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 33419 8ae45e87b992
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
boehmes@33419
     1
vc max 1
boehmes@33419
     2
    implies
boehmes@33419
     3
    label pos 10 7
boehmes@33419
     4
    true
boehmes@33419
     5
    implies
boehmes@33419
     6
    <
boehmes@33419
     7
    int-num 0
boehmes@33419
     8
    var length
boehmes@33419
     9
      int
boehmes@33419
    10
    implies
boehmes@33419
    11
    true
boehmes@33419
    12
    implies
boehmes@33419
    13
    =
boehmes@33419
    14
    var max@0
boehmes@33419
    15
      int
boehmes@33419
    16
    select 2
boehmes@33419
    17
    var array
boehmes@33419
    18
      array 2
boehmes@33419
    19
        int
boehmes@33419
    20
        int
boehmes@33419
    21
    int-num 0
boehmes@33419
    22
    implies
boehmes@33419
    23
    and 4
boehmes@33419
    24
    <=
boehmes@33419
    25
    int-num 0
boehmes@33419
    26
    int-num 0
boehmes@33419
    27
    <=
boehmes@33419
    28
    int-num 0
boehmes@33419
    29
    int-num 0
boehmes@33419
    30
    <=
boehmes@33419
    31
    int-num 1
boehmes@33419
    32
    int-num 1
boehmes@33419
    33
    <=
boehmes@33419
    34
    int-num 1
boehmes@33419
    35
    int-num 1
boehmes@33419
    36
    and 2
boehmes@33419
    37
    label neg 14 5
boehmes@33419
    38
    forall 1 0 3
boehmes@33419
    39
      var i
boehmes@33419
    40
        int
boehmes@33419
    41
      attribute qid 1
boehmes@33419
    42
        string-attr BoogieMa.14:23
boehmes@33419
    43
      attribute uniqueId 1
boehmes@33419
    44
        string-attr 2
boehmes@33419
    45
      attribute bvZ3Native 1
boehmes@33419
    46
        string-attr False
boehmes@33419
    47
    implies
boehmes@33419
    48
    and 2
boehmes@33419
    49
    <=
boehmes@33419
    50
    int-num 0
boehmes@33419
    51
    var i
boehmes@33419
    52
      int
boehmes@33419
    53
    <
boehmes@33419
    54
    var i
boehmes@33419
    55
      int
boehmes@33419
    56
    int-num 1
boehmes@33419
    57
    <=
boehmes@33419
    58
    select 2
boehmes@33419
    59
    var array
boehmes@33419
    60
      array 2
boehmes@33419
    61
        int
boehmes@33419
    62
        int
boehmes@33419
    63
    var i
boehmes@33419
    64
      int
boehmes@33419
    65
    var max@0
boehmes@33419
    66
      int
boehmes@33419
    67
    implies
boehmes@33419
    68
    forall 1 0 3
boehmes@33419
    69
      var i
boehmes@33419
    70
        int
boehmes@33419
    71
      attribute qid 1
boehmes@33419
    72
        string-attr BoogieMa.14:23
boehmes@33419
    73
      attribute uniqueId 1
boehmes@33419
    74
        string-attr 2
boehmes@33419
    75
      attribute bvZ3Native 1
boehmes@33419
    76
        string-attr False
boehmes@33419
    77
    implies
boehmes@33419
    78
    and 2
boehmes@33419
    79
    <=
boehmes@33419
    80
    int-num 0
boehmes@33419
    81
    var i
boehmes@33419
    82
      int
boehmes@33419
    83
    <
boehmes@33419
    84
    var i
boehmes@33419
    85
      int
boehmes@33419
    86
    int-num 1
boehmes@33419
    87
    <=
boehmes@33419
    88
    select 2
boehmes@33419
    89
    var array
boehmes@33419
    90
      array 2
boehmes@33419
    91
        int
boehmes@33419
    92
        int
boehmes@33419
    93
    var i
boehmes@33419
    94
      int
boehmes@33419
    95
    var max@0
boehmes@33419
    96
      int
boehmes@33419
    97
    and 2
boehmes@33419
    98
    label neg 15 5
boehmes@33419
    99
    =
boehmes@33419
   100
    select 2
boehmes@33419
   101
    var array
boehmes@33419
   102
      array 2
boehmes@33419
   103
        int
boehmes@33419
   104
        int
boehmes@33419
   105
    int-num 0
boehmes@33419
   106
    var max@0
boehmes@33419
   107
      int
boehmes@33419
   108
    implies
boehmes@33419
   109
    =
boehmes@33419
   110
    select 2
boehmes@33419
   111
    var array
boehmes@33419
   112
      array 2
boehmes@33419
   113
        int
boehmes@33419
   114
        int
boehmes@33419
   115
    int-num 0
boehmes@33419
   116
    var max@0
boehmes@33419
   117
      int
boehmes@33419
   118
    implies
boehmes@33419
   119
    label pos 13 3
boehmes@33419
   120
    true
boehmes@33419
   121
    implies
boehmes@33419
   122
    and 2
boehmes@33419
   123
    <=
boehmes@33419
   124
    int-num 0
boehmes@33419
   125
    var k@0
boehmes@33419
   126
      int
boehmes@33419
   127
    <=
boehmes@33419
   128
    int-num 1
boehmes@33419
   129
    var p@0
boehmes@33419
   130
      int
boehmes@33419
   131
    implies
boehmes@33419
   132
    forall 1 0 3
boehmes@33419
   133
      var i
boehmes@33419
   134
        int
boehmes@33419
   135
      attribute qid 1
boehmes@33419
   136
        string-attr BoogieMa.14:23
boehmes@33419
   137
      attribute uniqueId 1
boehmes@33419
   138
        string-attr 2
boehmes@33419
   139
      attribute bvZ3Native 1
boehmes@33419
   140
        string-attr False
boehmes@33419
   141
    implies
boehmes@33419
   142
    and 2
boehmes@33419
   143
    <=
boehmes@33419
   144
    int-num 0
boehmes@33419
   145
    var i
boehmes@33419
   146
      int
boehmes@33419
   147
    <
boehmes@33419
   148
    var i
boehmes@33419
   149
      int
boehmes@33419
   150
    var p@0
boehmes@33419
   151
      int
boehmes@33419
   152
    <=
boehmes@33419
   153
    select 2
boehmes@33419
   154
    var array
boehmes@33419
   155
      array 2
boehmes@33419
   156
        int
boehmes@33419
   157
        int
boehmes@33419
   158
    var i
boehmes@33419
   159
      int
boehmes@33419
   160
    var max@1
boehmes@33419
   161
      int
boehmes@33419
   162
    implies
boehmes@33419
   163
    =
boehmes@33419
   164
    select 2
boehmes@33419
   165
    var array
boehmes@33419
   166
      array 2
boehmes@33419
   167
        int
boehmes@33419
   168
        int
boehmes@33419
   169
    var k@0
boehmes@33419
   170
      int
boehmes@33419
   171
    var max@1
boehmes@33419
   172
      int
boehmes@33419
   173
    implies
boehmes@33419
   174
    and 2
boehmes@33419
   175
    <=
boehmes@33419
   176
    int-num 0
boehmes@33419
   177
    var k@0
boehmes@33419
   178
      int
boehmes@33419
   179
    <=
boehmes@33419
   180
    int-num 1
boehmes@33419
   181
    var p@0
boehmes@33419
   182
      int
boehmes@33419
   183
    and 2
boehmes@33419
   184
    implies
boehmes@33419
   185
    label pos 13 3
boehmes@33419
   186
    true
boehmes@33419
   187
    implies
boehmes@33419
   188
    and 2
boehmes@33419
   189
    <=
boehmes@33419
   190
    int-num 0
boehmes@33419
   191
    var k@0
boehmes@33419
   192
      int
boehmes@33419
   193
    <=
boehmes@33419
   194
    int-num 1
boehmes@33419
   195
    var p@0
boehmes@33419
   196
      int
boehmes@33419
   197
    implies
boehmes@33419
   198
    >=
boehmes@33419
   199
    var p@0
boehmes@33419
   200
      int
boehmes@33419
   201
    var length
boehmes@33419
   202
      int
boehmes@33419
   203
    implies
boehmes@33419
   204
    and 2
boehmes@33419
   205
    <=
boehmes@33419
   206
    int-num 0
boehmes@33419
   207
    var k@0
boehmes@33419
   208
      int
boehmes@33419
   209
    <=
boehmes@33419
   210
    int-num 1
boehmes@33419
   211
    var p@0
boehmes@33419
   212
      int
boehmes@33419
   213
    implies
boehmes@33419
   214
    label pos 0 0
boehmes@33419
   215
    true
boehmes@33419
   216
    implies
boehmes@33419
   217
    =
boehmes@33419
   218
    var k@2
boehmes@33419
   219
      int
boehmes@33419
   220
    var k@0
boehmes@33419
   221
      int
boehmes@33419
   222
    implies
boehmes@33419
   223
    =
boehmes@33419
   224
    var max@4
boehmes@33419
   225
      int
boehmes@33419
   226
    var max@1
boehmes@33419
   227
      int
boehmes@33419
   228
    implies
boehmes@33419
   229
    =
boehmes@33419
   230
    var p@2
boehmes@33419
   231
      int
boehmes@33419
   232
    var p@0
boehmes@33419
   233
      int
boehmes@33419
   234
    implies
boehmes@33419
   235
    label pos 0 0
boehmes@33419
   236
    true
boehmes@33419
   237
    and 2
boehmes@33419
   238
    label neg 5 3
boehmes@33419
   239
    exists 1 0 3
boehmes@33419
   240
      var i
boehmes@33419
   241
        int
boehmes@33419
   242
      attribute qid 1
boehmes@33419
   243
        string-attr BoogieMa.5:19
boehmes@33419
   244
      attribute uniqueId 1
boehmes@33419
   245
        string-attr 1
boehmes@33419
   246
      attribute bvZ3Native 1
boehmes@33419
   247
        string-attr False
boehmes@33419
   248
    implies
boehmes@33419
   249
    and 2
boehmes@33419
   250
    <=
boehmes@33419
   251
    int-num 0
boehmes@33419
   252
    var i
boehmes@33419
   253
      int
boehmes@33419
   254
    <
boehmes@33419
   255
    var i
boehmes@33419
   256
      int
boehmes@33419
   257
    var length
boehmes@33419
   258
      int
boehmes@33419
   259
    =
boehmes@33419
   260
    select 2
boehmes@33419
   261
    var array
boehmes@33419
   262
      array 2
boehmes@33419
   263
        int
boehmes@33419
   264
        int
boehmes@33419
   265
    var i
boehmes@33419
   266
      int
boehmes@33419
   267
    var max@4
boehmes@33419
   268
      int
boehmes@33419
   269
    implies
boehmes@33419
   270
    exists 1 0 3
boehmes@33419
   271
      var i
boehmes@33419
   272
        int
boehmes@33419
   273
      attribute qid 1
boehmes@33419
   274
        string-attr BoogieMa.5:19
boehmes@33419
   275
      attribute uniqueId 1
boehmes@33419
   276
        string-attr 1
boehmes@33419
   277
      attribute bvZ3Native 1
boehmes@33419
   278
        string-attr False
boehmes@33419
   279
    implies
boehmes@33419
   280
    and 2
boehmes@33419
   281
    <=
boehmes@33419
   282
    int-num 0
boehmes@33419
   283
    var i
boehmes@33419
   284
      int
boehmes@33419
   285
    <
boehmes@33419
   286
    var i
boehmes@33419
   287
      int
boehmes@33419
   288
    var length
boehmes@33419
   289
      int
boehmes@33419
   290
    =
boehmes@33419
   291
    select 2
boehmes@33419
   292
    var array
boehmes@33419
   293
      array 2
boehmes@33419
   294
        int
boehmes@33419
   295
        int
boehmes@33419
   296
    var i
boehmes@33419
   297
      int
boehmes@33419
   298
    var max@4
boehmes@33419
   299
      int
boehmes@33419
   300
    and 2
boehmes@33419
   301
    label neg 4 3
boehmes@33419
   302
    forall 1 0 3
boehmes@33419
   303
      var i
boehmes@33419
   304
        int
boehmes@33419
   305
      attribute qid 1
boehmes@33419
   306
        string-attr BoogieMa.4:19
boehmes@33419
   307
      attribute uniqueId 1
boehmes@33419
   308
        string-attr 0
boehmes@33419
   309
      attribute bvZ3Native 1
boehmes@33419
   310
        string-attr False
boehmes@33419
   311
    implies
boehmes@33419
   312
    and 2
boehmes@33419
   313
    <=
boehmes@33419
   314
    int-num 0
boehmes@33419
   315
    var i
boehmes@33419
   316
      int
boehmes@33419
   317
    <
boehmes@33419
   318
    var i
boehmes@33419
   319
      int
boehmes@33419
   320
    var length
boehmes@33419
   321
      int
boehmes@33419
   322
    <=
boehmes@33419
   323
    select 2
boehmes@33419
   324
    var array
boehmes@33419
   325
      array 2
boehmes@33419
   326
        int
boehmes@33419
   327
        int
boehmes@33419
   328
    var i
boehmes@33419
   329
      int
boehmes@33419
   330
    var max@4
boehmes@33419
   331
      int
boehmes@33419
   332
    implies
boehmes@33419
   333
    forall 1 0 3
boehmes@33419
   334
      var i
boehmes@33419
   335
        int
boehmes@33419
   336
      attribute qid 1
boehmes@33419
   337
        string-attr BoogieMa.4:19
boehmes@33419
   338
      attribute uniqueId 1
boehmes@33419
   339
        string-attr 0
boehmes@33419
   340
      attribute bvZ3Native 1
boehmes@33419
   341
        string-attr False
boehmes@33419
   342
    implies
boehmes@33419
   343
    and 2
boehmes@33419
   344
    <=
boehmes@33419
   345
    int-num 0
boehmes@33419
   346
    var i
boehmes@33419
   347
      int
boehmes@33419
   348
    <
boehmes@33419
   349
    var i
boehmes@33419
   350
      int
boehmes@33419
   351
    var length
boehmes@33419
   352
      int
boehmes@33419
   353
    <=
boehmes@33419
   354
    select 2
boehmes@33419
   355
    var array
boehmes@33419
   356
      array 2
boehmes@33419
   357
        int
boehmes@33419
   358
        int
boehmes@33419
   359
    var i
boehmes@33419
   360
      int
boehmes@33419
   361
    var max@4
boehmes@33419
   362
      int
boehmes@33419
   363
    true
boehmes@33419
   364
    implies
boehmes@33419
   365
    label pos 17 5
boehmes@33419
   366
    true
boehmes@33419
   367
    implies
boehmes@33419
   368
    and 2
boehmes@33419
   369
    <=
boehmes@33419
   370
    int-num 0
boehmes@33419
   371
    var k@0
boehmes@33419
   372
      int
boehmes@33419
   373
    <=
boehmes@33419
   374
    int-num 1
boehmes@33419
   375
    var p@0
boehmes@33419
   376
      int
boehmes@33419
   377
    implies
boehmes@33419
   378
    <
boehmes@33419
   379
    var p@0
boehmes@33419
   380
      int
boehmes@33419
   381
    var length
boehmes@33419
   382
      int
boehmes@33419
   383
    implies
boehmes@33419
   384
    and 2
boehmes@33419
   385
    <=
boehmes@33419
   386
    int-num 0
boehmes@33419
   387
    var k@0
boehmes@33419
   388
      int
boehmes@33419
   389
    <=
boehmes@33419
   390
    int-num 1
boehmes@33419
   391
    var p@0
boehmes@33419
   392
      int
boehmes@33419
   393
    and 2
boehmes@33419
   394
    implies
boehmes@33419
   395
    label pos 17 31
boehmes@33419
   396
    true
boehmes@33419
   397
    implies
boehmes@33419
   398
    and 2
boehmes@33419
   399
    <=
boehmes@33419
   400
    int-num 0
boehmes@33419
   401
    var k@0
boehmes@33419
   402
      int
boehmes@33419
   403
    <=
boehmes@33419
   404
    int-num 1
boehmes@33419
   405
    var p@0
boehmes@33419
   406
      int
boehmes@33419
   407
    implies
boehmes@33419
   408
    >
boehmes@33419
   409
    select 2
boehmes@33419
   410
    var array
boehmes@33419
   411
      array 2
boehmes@33419
   412
        int
boehmes@33419
   413
        int
boehmes@33419
   414
    var p@0
boehmes@33419
   415
      int
boehmes@33419
   416
    var max@1
boehmes@33419
   417
      int
boehmes@33419
   418
    implies
boehmes@33419
   419
    =
boehmes@33419
   420
    var max@2
boehmes@33419
   421
      int
boehmes@33419
   422
    select 2
boehmes@33419
   423
    var array
boehmes@33419
   424
      array 2
boehmes@33419
   425
        int
boehmes@33419
   426
        int
boehmes@33419
   427
    var p@0
boehmes@33419
   428
      int
boehmes@33419
   429
    implies
boehmes@33419
   430
    and 2
boehmes@33419
   431
    <=
boehmes@33419
   432
    int-num 1
boehmes@33419
   433
    var p@0
boehmes@33419
   434
      int
boehmes@33419
   435
    <=
boehmes@33419
   436
    int-num 1
boehmes@33419
   437
    var p@0
boehmes@33419
   438
      int
boehmes@33419
   439
    implies
boehmes@33419
   440
    label pos 0 0
boehmes@33419
   441
    true
boehmes@33419
   442
    implies
boehmes@33419
   443
    =
boehmes@33419
   444
    var k@1
boehmes@33419
   445
      int
boehmes@33419
   446
    var p@0
boehmes@33419
   447
      int
boehmes@33419
   448
    implies
boehmes@33419
   449
    =
boehmes@33419
   450
    var max@3
boehmes@33419
   451
      int
boehmes@33419
   452
    var max@2
boehmes@33419
   453
      int
boehmes@33419
   454
    implies
boehmes@33419
   455
    label pos 18 7
boehmes@33419
   456
    true
boehmes@33419
   457
    implies
boehmes@33419
   458
    and 2
boehmes@33419
   459
    <=
boehmes@33419
   460
    int-num 0
boehmes@33419
   461
    var k@1
boehmes@33419
   462
      int
boehmes@33419
   463
    <=
boehmes@33419
   464
    int-num 1
boehmes@33419
   465
    var p@0
boehmes@33419
   466
      int
boehmes@33419
   467
    implies
boehmes@33419
   468
    =
boehmes@33419
   469
    var p@1
boehmes@33419
   470
      int
boehmes@33419
   471
    +
boehmes@33419
   472
    var p@0
boehmes@33419
   473
      int
boehmes@33419
   474
    int-num 1
boehmes@33419
   475
    implies
boehmes@33419
   476
    and 2
boehmes@33419
   477
    <=
boehmes@33419
   478
    int-num 0
boehmes@33419
   479
    var k@1
boehmes@33419
   480
      int
boehmes@33419
   481
    <=
boehmes@33419
   482
    int-num 2
boehmes@33419
   483
    var p@1
boehmes@33419
   484
      int
boehmes@33419
   485
    implies
boehmes@33419
   486
    label pos 0 0
boehmes@33419
   487
    true
boehmes@33419
   488
    and 2
boehmes@33419
   489
    label neg 14 5
boehmes@33419
   490
    forall 1 0 3
boehmes@33419
   491
      var i
boehmes@33419
   492
        int
boehmes@33419
   493
      attribute qid 1
boehmes@33419
   494
        string-attr BoogieMa.14:23
boehmes@33419
   495
      attribute uniqueId 1
boehmes@33419
   496
        string-attr 2
boehmes@33419
   497
      attribute bvZ3Native 1
boehmes@33419
   498
        string-attr False
boehmes@33419
   499
    implies
boehmes@33419
   500
    and 2
boehmes@33419
   501
    <=
boehmes@33419
   502
    int-num 0
boehmes@33419
   503
    var i
boehmes@33419
   504
      int
boehmes@33419
   505
    <
boehmes@33419
   506
    var i
boehmes@33419
   507
      int
boehmes@33419
   508
    var p@1
boehmes@33419
   509
      int
boehmes@33419
   510
    <=
boehmes@33419
   511
    select 2
boehmes@33419
   512
    var array
boehmes@33419
   513
      array 2
boehmes@33419
   514
        int
boehmes@33419
   515
        int
boehmes@33419
   516
    var i
boehmes@33419
   517
      int
boehmes@33419
   518
    var max@3
boehmes@33419
   519
      int
boehmes@33419
   520
    implies
boehmes@33419
   521
    forall 1 0 3
boehmes@33419
   522
      var i
boehmes@33419
   523
        int
boehmes@33419
   524
      attribute qid 1
boehmes@33419
   525
        string-attr BoogieMa.14:23
boehmes@33419
   526
      attribute uniqueId 1
boehmes@33419
   527
        string-attr 2
boehmes@33419
   528
      attribute bvZ3Native 1
boehmes@33419
   529
        string-attr False
boehmes@33419
   530
    implies
boehmes@33419
   531
    and 2
boehmes@33419
   532
    <=
boehmes@33419
   533
    int-num 0
boehmes@33419
   534
    var i
boehmes@33419
   535
      int
boehmes@33419
   536
    <
boehmes@33419
   537
    var i
boehmes@33419
   538
      int
boehmes@33419
   539
    var p@1
boehmes@33419
   540
      int
boehmes@33419
   541
    <=
boehmes@33419
   542
    select 2
boehmes@33419
   543
    var array
boehmes@33419
   544
      array 2
boehmes@33419
   545
        int
boehmes@33419
   546
        int
boehmes@33419
   547
    var i
boehmes@33419
   548
      int
boehmes@33419
   549
    var max@3
boehmes@33419
   550
      int
boehmes@33419
   551
    and 2
boehmes@33419
   552
    label neg 15 5
boehmes@33419
   553
    =
boehmes@33419
   554
    select 2
boehmes@33419
   555
    var array
boehmes@33419
   556
      array 2
boehmes@33419
   557
        int
boehmes@33419
   558
        int
boehmes@33419
   559
    var k@1
boehmes@33419
   560
      int
boehmes@33419
   561
    var max@3
boehmes@33419
   562
      int
boehmes@33419
   563
    implies
boehmes@33419
   564
    =
boehmes@33419
   565
    select 2
boehmes@33419
   566
    var array
boehmes@33419
   567
      array 2
boehmes@33419
   568
        int
boehmes@33419
   569
        int
boehmes@33419
   570
    var k@1
boehmes@33419
   571
      int
boehmes@33419
   572
    var max@3
boehmes@33419
   573
      int
boehmes@33419
   574
    implies
boehmes@33419
   575
    false
boehmes@33419
   576
    true
boehmes@33419
   577
    implies
boehmes@33419
   578
    label pos 17 5
boehmes@33419
   579
    true
boehmes@33419
   580
    implies
boehmes@33419
   581
    and 2
boehmes@33419
   582
    <=
boehmes@33419
   583
    int-num 0
boehmes@33419
   584
    var k@0
boehmes@33419
   585
      int
boehmes@33419
   586
    <=
boehmes@33419
   587
    int-num 1
boehmes@33419
   588
    var p@0
boehmes@33419
   589
      int
boehmes@33419
   590
    implies
boehmes@33419
   591
    <=
boehmes@33419
   592
    select 2
boehmes@33419
   593
    var array
boehmes@33419
   594
      array 2
boehmes@33419
   595
        int
boehmes@33419
   596
        int
boehmes@33419
   597
    var p@0
boehmes@33419
   598
      int
boehmes@33419
   599
    var max@1
boehmes@33419
   600
      int
boehmes@33419
   601
    implies
boehmes@33419
   602
    and 2
boehmes@33419
   603
    <=
boehmes@33419
   604
    int-num 0
boehmes@33419
   605
    var k@0
boehmes@33419
   606
      int
boehmes@33419
   607
    <=
boehmes@33419
   608
    int-num 1
boehmes@33419
   609
    var p@0
boehmes@33419
   610
      int
boehmes@33419
   611
    implies
boehmes@33419
   612
    label pos 0 0
boehmes@33419
   613
    true
boehmes@33419
   614
    implies
boehmes@33419
   615
    =
boehmes@33419
   616
    var k@1
boehmes@33419
   617
      int
boehmes@33419
   618
    var k@0
boehmes@33419
   619
      int
boehmes@33419
   620
    implies
boehmes@33419
   621
    =
boehmes@33419
   622
    var max@3
boehmes@33419
   623
      int
boehmes@33419
   624
    var max@1
boehmes@33419
   625
      int
boehmes@33419
   626
    implies
boehmes@33419
   627
    label pos 18 7
boehmes@33419
   628
    true
boehmes@33419
   629
    implies
boehmes@33419
   630
    and 2
boehmes@33419
   631
    <=
boehmes@33419
   632
    int-num 0
boehmes@33419
   633
    var k@1
boehmes@33419
   634
      int
boehmes@33419
   635
    <=
boehmes@33419
   636
    int-num 1
boehmes@33419
   637
    var p@0
boehmes@33419
   638
      int
boehmes@33419
   639
    implies
boehmes@33419
   640
    =
boehmes@33419
   641
    var p@1
boehmes@33419
   642
      int
boehmes@33419
   643
    +
boehmes@33419
   644
    var p@0
boehmes@33419
   645
      int
boehmes@33419
   646
    int-num 1
boehmes@33419
   647
    implies
boehmes@33419
   648
    and 2
boehmes@33419
   649
    <=
boehmes@33419
   650
    int-num 0
boehmes@33419
   651
    var k@1
boehmes@33419
   652
      int
boehmes@33419
   653
    <=
boehmes@33419
   654
    int-num 2
boehmes@33419
   655
    var p@1
boehmes@33419
   656
      int
boehmes@33419
   657
    implies
boehmes@33419
   658
    label pos 0 0
boehmes@33419
   659
    true
boehmes@33419
   660
    and 2
boehmes@33419
   661
    label neg 14 5
boehmes@33419
   662
    forall 1 0 3
boehmes@33419
   663
      var i
boehmes@33419
   664
        int
boehmes@33419
   665
      attribute qid 1
boehmes@33419
   666
        string-attr BoogieMa.14:23
boehmes@33419
   667
      attribute uniqueId 1
boehmes@33419
   668
        string-attr 2
boehmes@33419
   669
      attribute bvZ3Native 1
boehmes@33419
   670
        string-attr False
boehmes@33419
   671
    implies
boehmes@33419
   672
    and 2
boehmes@33419
   673
    <=
boehmes@33419
   674
    int-num 0
boehmes@33419
   675
    var i
boehmes@33419
   676
      int
boehmes@33419
   677
    <
boehmes@33419
   678
    var i
boehmes@33419
   679
      int
boehmes@33419
   680
    var p@1
boehmes@33419
   681
      int
boehmes@33419
   682
    <=
boehmes@33419
   683
    select 2
boehmes@33419
   684
    var array
boehmes@33419
   685
      array 2
boehmes@33419
   686
        int
boehmes@33419
   687
        int
boehmes@33419
   688
    var i
boehmes@33419
   689
      int
boehmes@33419
   690
    var max@3
boehmes@33419
   691
      int
boehmes@33419
   692
    implies
boehmes@33419
   693
    forall 1 0 3
boehmes@33419
   694
      var i
boehmes@33419
   695
        int
boehmes@33419
   696
      attribute qid 1
boehmes@33419
   697
        string-attr BoogieMa.14:23
boehmes@33419
   698
      attribute uniqueId 1
boehmes@33419
   699
        string-attr 2
boehmes@33419
   700
      attribute bvZ3Native 1
boehmes@33419
   701
        string-attr False
boehmes@33419
   702
    implies
boehmes@33419
   703
    and 2
boehmes@33419
   704
    <=
boehmes@33419
   705
    int-num 0
boehmes@33419
   706
    var i
boehmes@33419
   707
      int
boehmes@33419
   708
    <
boehmes@33419
   709
    var i
boehmes@33419
   710
      int
boehmes@33419
   711
    var p@1
boehmes@33419
   712
      int
boehmes@33419
   713
    <=
boehmes@33419
   714
    select 2
boehmes@33419
   715
    var array
boehmes@33419
   716
      array 2
boehmes@33419
   717
        int
boehmes@33419
   718
        int
boehmes@33419
   719
    var i
boehmes@33419
   720
      int
boehmes@33419
   721
    var max@3
boehmes@33419
   722
      int
boehmes@33419
   723
    and 2
boehmes@33419
   724
    label neg 15 5
boehmes@33419
   725
    =
boehmes@33419
   726
    select 2
boehmes@33419
   727
    var array
boehmes@33419
   728
      array 2
boehmes@33419
   729
        int
boehmes@33419
   730
        int
boehmes@33419
   731
    var k@1
boehmes@33419
   732
      int
boehmes@33419
   733
    var max@3
boehmes@33419
   734
      int
boehmes@33419
   735
    implies
boehmes@33419
   736
    =
boehmes@33419
   737
    select 2
boehmes@33419
   738
    var array
boehmes@33419
   739
      array 2
boehmes@33419
   740
        int
boehmes@33419
   741
        int
boehmes@33419
   742
    var k@1
boehmes@33419
   743
      int
boehmes@33419
   744
    var max@3
boehmes@33419
   745
      int
boehmes@33419
   746
    implies
boehmes@33419
   747
    false
boehmes@33419
   748
    true