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