src/HOL/SMT_Examples/Boogie_Dijkstra.b2i
author wenzelm
Sun, 11 Feb 2018 12:51:23 +0100
changeset 67593 5efb88c90051
parent 52722 2c81f7baf8c4
permissions -rw-r--r--
clarified command-line defaults;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     1
type-decl Vertex 0 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     2
fun-decl G 1 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     3
    array 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     4
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     5
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     6
      int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     7
fun-decl Infinity 1 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     8
    int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     9
fun-decl Source 1 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    10
    type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    11
axiom 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    12
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    13
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    14
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    15
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    16
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    17
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    18
        string-attr BoogieDi.3:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    19
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    20
        string-attr 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    21
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    22
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    23
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    24
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    25
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    26
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    27
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    28
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    29
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    30
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    31
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    32
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    33
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    34
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    35
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    36
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    37
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    38
axiom 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    39
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    40
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    41
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    42
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    43
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    44
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    45
        string-attr BoogieDi.4:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    46
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    47
        string-attr 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    48
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    49
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    50
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    51
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    52
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    53
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    54
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    55
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    56
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    57
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    58
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    59
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    60
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    61
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    62
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    63
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    64
axiom 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    65
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    66
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    67
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    68
var-decl SP 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    69
    array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    70
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    71
      int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    72
vc Dijkstra 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    73
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    74
    label pos 26 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    75
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    76
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    77
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    78
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    79
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    80
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    81
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    82
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    83
        string-attr BoogieDi.27:18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    84
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    85
        string-attr 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    86
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    87
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    88
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    89
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    90
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    91
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    92
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    93
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    94
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    95
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    96
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    97
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    98
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    99
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   100
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   101
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   102
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   103
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   104
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   105
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   106
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   107
        string-attr BoogieDi.28:18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   108
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   109
        string-attr 6
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   110
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   111
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   112
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   113
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   114
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   115
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   116
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   117
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   118
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   119
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   120
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   121
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   122
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   123
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   124
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   125
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   126
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   127
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   128
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   129
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   130
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   131
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   132
        string-attr BoogieDi.31:18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   133
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   134
        string-attr 7
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   135
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   136
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   137
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   138
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   139
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   140
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   141
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   142
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   143
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   144
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   145
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   146
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   147
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   148
    label neg 34 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   149
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   150
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   151
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   152
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   153
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   154
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   155
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   156
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   157
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   158
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   159
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   160
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   161
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   162
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   163
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   164
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   165
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   166
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   167
    label neg 35 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   168
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   169
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   170
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   171
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   172
        string-attr BoogieDi.35:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   173
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   174
        string-attr 9
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   175
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   176
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   177
    >=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   178
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   179
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   180
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   181
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   182
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   183
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   184
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   185
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   186
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   187
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   188
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   189
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   190
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   191
        string-attr BoogieDi.35:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   192
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   193
        string-attr 9
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   194
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   195
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   196
    >=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   197
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   198
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   199
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   200
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   201
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   202
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   203
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   204
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   205
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   206
    label neg 36 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   207
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   208
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   209
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   210
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   211
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   212
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   213
        string-attr BoogieDi.36:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   214
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   215
        string-attr 10
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   216
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   217
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   218
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   219
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   220
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   221
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   222
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   223
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   224
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   225
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   226
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   227
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   228
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   229
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   230
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   231
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   232
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   233
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   234
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   235
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   236
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   237
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   238
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   239
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   240
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   241
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   242
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   243
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   244
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   245
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   246
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   247
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   248
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   249
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   250
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   251
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   252
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   253
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   254
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   255
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   256
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   257
        string-attr BoogieDi.36:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   258
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   259
        string-attr 10
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   260
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   261
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   262
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   263
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   264
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   265
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   266
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   267
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   268
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   269
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   270
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   271
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   272
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   273
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   274
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   275
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   276
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   277
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   278
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   279
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   280
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   281
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   282
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   283
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   284
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   285
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   286
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   287
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   288
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   289
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   290
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   291
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   292
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   293
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   294
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   295
    label neg 38 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   296
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   297
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   298
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   299
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   300
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   301
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   302
        string-attr BoogieDi.38:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   303
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   304
        string-attr 11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   305
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   306
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   307
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   308
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   309
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   310
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   311
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   312
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   313
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   314
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   315
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   316
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   317
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   318
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   319
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   320
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   321
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   322
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   323
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   324
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   325
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   326
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   327
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   328
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   329
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   330
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   331
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   332
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   333
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   334
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   335
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   336
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   337
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   338
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   339
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   340
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   341
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   342
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   343
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   344
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   345
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   346
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   347
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   348
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   349
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   350
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   351
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   352
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   353
        string-attr BoogieDi.38:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   354
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   355
        string-attr 11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   356
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   357
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   358
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   359
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   360
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   361
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   362
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   363
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   364
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   365
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   366
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   367
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   368
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   369
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   370
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   371
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   372
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   373
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   374
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   375
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   376
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   377
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   378
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   379
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   380
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   381
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   382
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   383
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   384
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   385
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   386
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   387
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   388
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   389
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   390
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   391
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   392
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   393
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   394
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   395
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   396
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   397
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   398
    label neg 40 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   399
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   400
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   401
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   402
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   403
        string-attr BoogieDi.40:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   404
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   405
        string-attr 13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   406
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   407
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   408
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   409
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   410
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   411
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   412
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   413
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   414
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   415
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   416
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   417
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   418
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   419
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   420
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   421
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   422
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   423
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   424
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   425
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   426
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   427
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   428
        string-attr BoogieDi.41:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   429
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   430
        string-attr 12
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   431
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   432
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   433
    and 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   434
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   435
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   436
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   437
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   438
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   439
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   440
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   441
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   442
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   443
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   444
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   445
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   446
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   447
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   448
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   449
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   450
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   451
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   452
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   453
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   454
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   455
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   456
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   457
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   458
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   459
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   460
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   461
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   462
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   463
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   464
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   465
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   466
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   467
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   468
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   469
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   470
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   471
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   472
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   473
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   474
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   475
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   476
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   477
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   478
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   479
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   480
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   481
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   482
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   483
        string-attr BoogieDi.40:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   484
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   485
        string-attr 13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   486
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   487
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   488
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   489
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   490
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   491
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   492
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   493
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   494
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   495
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   496
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   497
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   498
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   499
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   500
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   501
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   502
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   503
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   504
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   505
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   506
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   507
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   508
        string-attr BoogieDi.41:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   509
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   510
        string-attr 12
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   511
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   512
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   513
    and 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   514
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   515
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   516
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   517
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   518
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   519
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   520
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   521
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   522
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   523
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   524
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   525
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   526
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   527
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   528
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   529
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   530
    var Visited@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   531
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   532
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   533
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   534
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   535
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   536
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   537
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   538
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   539
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   540
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   541
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   542
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   543
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   544
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   545
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   546
    var SP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   547
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   548
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   549
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   550
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   551
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   552
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   553
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   554
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   555
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   556
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   557
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   558
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   559
    label pos 33 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   560
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   561
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   562
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   563
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   564
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   565
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   566
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   567
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   568
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   569
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   570
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   571
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   572
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   573
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   574
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   575
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   576
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   577
        string-attr BoogieDi.35:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   578
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   579
        string-attr 9
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   580
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   581
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   582
    >=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   583
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   584
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   585
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   586
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   587
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   588
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   589
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   590
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   591
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   592
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   593
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   594
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   595
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   596
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   597
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   598
        string-attr BoogieDi.36:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   599
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   600
        string-attr 10
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   601
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   602
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   603
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   604
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   605
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   606
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   607
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   608
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   609
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   610
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   611
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   612
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   613
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   614
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   615
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   616
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   617
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   618
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   619
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   620
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   621
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   622
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   623
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   624
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   625
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   626
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   627
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   628
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   629
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   630
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   631
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   632
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   633
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   634
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   635
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   636
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   637
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   638
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   639
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   640
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   641
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   642
        string-attr BoogieDi.38:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   643
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   644
        string-attr 11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   645
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   646
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   647
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   648
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   649
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   650
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   651
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   652
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   653
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   654
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   655
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   656
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   657
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   658
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   659
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   660
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   661
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   662
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   663
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   664
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   665
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   666
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   667
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   668
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   669
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   670
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   671
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   672
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   673
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   674
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   675
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   676
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   677
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   678
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   679
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   680
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   681
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   682
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   683
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   684
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   685
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   686
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   687
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   688
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   689
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   690
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   691
        string-attr BoogieDi.40:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   692
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   693
        string-attr 13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   694
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   695
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   696
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   697
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   698
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   699
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   700
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   701
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   702
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   703
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   704
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   705
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   706
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   707
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   708
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   709
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   710
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   711
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   712
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   713
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   714
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   715
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   716
        string-attr BoogieDi.41:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   717
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   718
        string-attr 12
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   719
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   720
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   721
    and 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   722
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   723
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   724
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   725
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   726
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   727
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   728
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   729
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   730
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   731
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   732
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   733
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   734
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   735
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   736
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   737
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   738
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   739
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   740
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   741
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   742
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   743
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   744
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   745
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   746
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   747
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   748
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   749
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   750
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   751
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   752
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   753
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   754
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   755
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   756
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   757
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   758
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   759
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   760
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   761
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   762
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   763
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   764
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   765
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   766
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   767
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   768
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   769
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   770
    label pos 33 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   771
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   772
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   773
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   774
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   775
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   776
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   777
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   778
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   779
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   780
        string-attr BoogieDi.33:18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   781
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   782
        string-attr 8
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   783
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   784
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   785
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   786
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   787
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   788
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   789
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   790
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   791
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   792
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   793
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   794
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   795
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   796
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   797
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   798
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   799
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   800
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   801
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   802
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   803
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   804
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   805
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   806
    label pos 0 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   807
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   808
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   809
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   810
    var Visited@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   811
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   812
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   813
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   814
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   815
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   816
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   817
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   818
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   819
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   820
    var v@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   821
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   822
    var v@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   823
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   824
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   825
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   826
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   827
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   828
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   829
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   830
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   831
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   832
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   833
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   834
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   835
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   836
    var oldSP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   837
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   838
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   839
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   840
    var oldSP@0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   841
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   842
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   843
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   844
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   845
    label pos 0 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   846
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   847
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   848
    label neg 17 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   849
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   850
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   851
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   852
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   853
        string-attr BoogieDi.17:19
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   854
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   855
        string-attr 4
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   856
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   857
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   858
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   859
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   860
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   861
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   862
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   863
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   864
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   865
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   866
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   867
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   868
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   869
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   870
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   871
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   872
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   873
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   874
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   875
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   876
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   877
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   878
        string-attr BoogieDi.18:13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   879
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   880
        string-attr 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   881
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   882
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   883
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   884
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   885
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   886
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   887
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   888
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   889
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   890
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   891
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   892
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   893
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   894
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   895
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   896
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   897
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   898
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   899
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   900
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   901
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   902
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   903
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   904
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   905
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   906
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   907
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   908
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   909
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   910
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   911
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   912
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   913
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   914
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   915
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   916
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   917
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   918
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   919
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   920
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   921
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   922
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   923
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   924
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   925
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   926
        string-attr BoogieDi.17:19
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   927
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   928
        string-attr 4
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   929
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   930
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   931
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   932
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   933
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   934
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   935
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   936
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   937
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   938
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   939
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   940
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   941
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   942
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   943
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   944
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   945
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   946
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   947
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   948
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   949
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   950
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   951
        string-attr BoogieDi.18:13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   952
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   953
        string-attr 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   954
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   955
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   956
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   957
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   958
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   959
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   960
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   961
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   962
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   963
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   964
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   965
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   966
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   967
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   968
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   969
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   970
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   971
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   972
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   973
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   974
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   975
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   976
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   977
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   978
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   979
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   980
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   981
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   982
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   983
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   984
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   985
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   986
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   987
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   988
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   989
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   990
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   991
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   992
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   993
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   994
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   995
    label neg 15 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   996
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   997
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   998
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
   999
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1000
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1001
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1002
        string-attr BoogieDi.15:19
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1003
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1004
        string-attr 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1005
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1006
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1007
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1008
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1009
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1010
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1011
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1012
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1013
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1014
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1015
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1016
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1017
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1018
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1019
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1020
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1021
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1022
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1023
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1024
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1025
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1026
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1027
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1028
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1029
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1030
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1031
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1032
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1033
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1034
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1035
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1036
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1037
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1038
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1039
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1040
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1041
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1042
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1043
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1044
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1045
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1046
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1047
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1048
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1049
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1050
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1051
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1052
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1053
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1054
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1055
        string-attr BoogieDi.15:19
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1056
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1057
        string-attr 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1058
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1059
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1060
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1061
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1062
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1063
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1064
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1065
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1066
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1067
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1068
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1069
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1070
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1071
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1072
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1073
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1074
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1075
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1076
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1077
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1078
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1079
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1080
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1081
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1082
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1083
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1084
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1085
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1086
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1087
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1088
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1089
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1090
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1091
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1092
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1093
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1094
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1095
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1096
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1097
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1098
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1099
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1100
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1101
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1102
    label neg 14 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1103
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1104
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1105
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1106
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1107
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1108
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1109
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1110
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1111
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1112
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1113
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1114
    var SP@3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1115
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1116
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1117
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1118
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1119
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1120
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1121
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1122
    label pos 44 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1123
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1124
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1125
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1126
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1127
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1128
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1129
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1130
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1131
        string-attr BoogieDi.33:18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1132
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1133
        string-attr 8
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1134
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1135
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1136
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1137
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1138
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1139
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1140
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1141
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1142
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1143
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1144
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1145
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1146
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1147
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1148
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1149
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1150
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1151
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1152
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1153
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1154
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1155
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1156
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1157
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1158
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1159
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1160
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1161
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1162
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1163
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1164
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1165
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1166
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1167
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1168
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1169
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1170
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1171
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1172
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1173
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1174
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1175
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1176
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1177
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1178
        string-attr BoogieDi.47:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1179
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1180
        string-attr 14
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1181
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1182
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1183
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1184
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1185
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1186
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1187
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1188
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1189
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1190
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1191
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1192
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1193
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1194
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1195
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1196
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1197
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1198
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1199
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1200
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1201
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1202
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1203
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1204
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1205
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1206
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1207
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1208
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1209
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1210
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1211
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1212
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1213
    store 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1214
    var Visited@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1215
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1216
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1217
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1218
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1219
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1220
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1221
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1222
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1223
      var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1224
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1225
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1226
        string-attr BoogieDi.53:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1227
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1228
        string-attr 15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1229
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1230
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1231
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1232
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1233
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1234
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1235
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1236
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1237
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1238
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1239
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1240
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1241
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1242
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1243
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1244
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1245
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1246
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1247
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1248
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1249
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1250
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1251
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1252
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1253
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1254
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1255
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1256
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1257
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1258
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1259
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1260
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1261
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1262
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1263
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1264
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1265
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1266
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1267
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1268
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1269
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1270
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1271
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1272
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1273
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1274
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1275
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1276
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1277
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1278
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1279
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1280
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1281
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1282
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1283
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1284
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1285
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1286
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1287
      var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1288
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1289
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1290
        string-attr BoogieDi.56:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1291
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1292
        string-attr 16
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1293
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1294
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1295
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1296
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1297
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1298
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1299
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1300
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1301
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1302
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1303
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1304
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1305
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1306
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1307
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1308
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1309
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1310
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1311
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1312
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1313
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1314
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1315
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1316
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1317
    var v@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1318
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1319
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1320
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1321
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1322
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1323
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1324
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1325
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1326
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1327
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1328
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1329
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1330
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1331
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1332
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1333
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1334
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1335
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1336
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1337
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1338
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1339
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1340
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1341
    var u
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1342
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1343
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1344
    label neg 59 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1345
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1346
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1347
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1348
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1349
        string-attr BoogieDi.59:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1350
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1351
        string-attr 17
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1352
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1353
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1354
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1355
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1356
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1357
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1358
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1359
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1360
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1361
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1362
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1363
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1364
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1365
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1366
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1367
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1368
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1369
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1370
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1371
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1372
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1373
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1374
        string-attr BoogieDi.59:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1375
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1376
        string-attr 17
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1377
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1378
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1379
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1380
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1381
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1382
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1383
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1384
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1385
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1386
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1387
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1388
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1389
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1390
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1391
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1392
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1393
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1394
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1395
    label neg 60 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1396
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1397
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1398
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1399
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1400
        string-attr BoogieDi.60:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1401
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1402
        string-attr 18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1403
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1404
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1405
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1406
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1407
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1408
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1409
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1410
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1411
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1412
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1413
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1414
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1415
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1416
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1417
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1418
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1419
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1420
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1421
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1422
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1423
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1424
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1425
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1426
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1427
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1428
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1429
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1430
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1431
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1432
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1433
        string-attr BoogieDi.60:20
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1434
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1435
        string-attr 18
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1436
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1437
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1438
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1439
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1440
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1441
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1442
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1443
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1444
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1445
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1446
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1447
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1448
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1449
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1450
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1451
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1452
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1453
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1454
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1455
    var SP@1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1456
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1457
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1458
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1459
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1460
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1461
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1462
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1463
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1464
    label pos 0 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1465
    true
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1466
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1467
    label neg 34 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1468
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1469
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1470
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1471
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1472
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1473
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1474
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1475
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1476
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1477
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1478
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1479
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1480
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1481
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1482
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1483
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1484
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1485
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1486
    label neg 35 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1487
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1488
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1489
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1490
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1491
        string-attr BoogieDi.35:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1492
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1493
        string-attr 9
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1494
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1495
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1496
    >=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1497
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1498
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1499
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1500
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1501
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1502
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1503
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1504
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1505
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1506
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1507
      var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1508
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1509
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1510
        string-attr BoogieDi.35:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1511
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1512
        string-attr 9
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1513
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1514
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1515
    >=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1516
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1517
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1518
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1519
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1520
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1521
    var x
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1522
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1523
    int-num 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1524
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1525
    label neg 36 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1526
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1527
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1528
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1529
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1530
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1531
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1532
        string-attr BoogieDi.36:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1533
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1534
        string-attr 10
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1535
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1536
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1537
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1538
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1539
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1540
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1541
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1542
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1543
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1544
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1545
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1546
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1547
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1548
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1549
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1550
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1551
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1552
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1553
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1554
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1555
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1556
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1557
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1558
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1559
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1560
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1561
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1562
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1563
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1564
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1565
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1566
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1567
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1568
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1569
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1570
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1571
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1572
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1573
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1574
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1575
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1576
        string-attr BoogieDi.36:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1577
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1578
        string-attr 10
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1579
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1580
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1581
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1582
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1583
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1584
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1585
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1586
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1587
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1588
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1589
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1590
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1591
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1592
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1593
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1594
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1595
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1596
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1597
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1598
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1599
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1600
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1601
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1602
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1603
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1604
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1605
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1606
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1607
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1608
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1609
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1610
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1611
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1612
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1613
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1614
    label neg 38 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1615
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1616
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1617
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1618
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1619
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1620
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1621
        string-attr BoogieDi.38:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1622
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1623
        string-attr 11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1624
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1625
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1626
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1627
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1628
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1629
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1630
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1631
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1632
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1633
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1634
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1635
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1636
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1637
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1638
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1639
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1640
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1641
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1642
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1643
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1644
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1645
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1646
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1647
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1648
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1649
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1650
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1651
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1652
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1653
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1654
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1655
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1656
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1657
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1658
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1659
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1660
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1661
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1662
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1663
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1664
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1665
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1666
    forall 2 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1667
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1668
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1669
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1670
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1671
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1672
        string-attr BoogieDi.38:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1673
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1674
        string-attr 11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1675
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1676
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1677
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1678
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1679
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1680
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1681
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1682
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1683
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1684
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1685
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1686
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1687
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1688
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1689
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1690
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1691
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1692
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1693
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1694
    <=
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1695
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1696
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1697
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1698
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1699
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1700
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1701
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1702
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1703
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1704
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1705
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1706
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1707
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1708
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1709
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1710
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1711
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1712
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1713
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1714
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1715
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1716
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1717
    label neg 40 5
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1718
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1719
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1720
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1721
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1722
        string-attr BoogieDi.40:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1723
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1724
        string-attr 13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1725
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1726
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1727
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1728
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1729
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1730
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1731
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1732
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1733
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1734
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1735
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1736
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1737
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1738
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1739
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1740
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1741
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1742
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1743
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1744
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1745
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1746
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1747
        string-attr BoogieDi.41:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1748
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1749
        string-attr 12
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1750
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1751
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1752
    and 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1753
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1754
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1755
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1756
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1757
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1758
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1759
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1760
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1761
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1762
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1763
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1764
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1765
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1766
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1767
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1768
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1769
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1770
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1771
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1772
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1773
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1774
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1775
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1776
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1777
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1778
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1779
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1780
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1781
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1782
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1783
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1784
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1785
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1786
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1787
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1788
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1789
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1790
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1791
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1792
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1793
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1794
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1795
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1796
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1797
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1798
    forall 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1799
      var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1800
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1801
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1802
        string-attr BoogieDi.40:23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1803
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1804
        string-attr 13
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1805
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1806
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1807
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1808
    and 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1809
    not
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1810
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1811
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1812
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1813
    fun Source 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1814
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1815
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1816
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1817
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1818
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1819
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1820
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1821
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1822
    fun Infinity 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1823
    exists 1 0 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1824
      var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1825
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1826
      attribute qid 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1827
        string-attr BoogieDi.41:15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1828
      attribute uniqueId 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1829
        string-attr 12
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1830
      attribute bvZ3Native 1
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1831
        string-attr False
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1832
    and 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1833
    <
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1834
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1835
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1836
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1837
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1838
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1839
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1840
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1841
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1842
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1843
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1844
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1845
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1846
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1847
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1848
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1849
    var Visited@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1850
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1851
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1852
        bool
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1853
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1854
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1855
    =
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1856
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1857
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1858
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1859
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1860
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1861
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1862
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1863
    +
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1864
    select 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1865
    var SP@2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1866
      array 2
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1867
        type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1868
        int
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1869
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1870
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1871
    select 3
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1872
    fun G 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1873
    var y
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1874
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1875
    var z
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1876
      type-con Vertex 0
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1877
    implies
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1878
    false
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
  1879
    true