src/HOL/Boogie/Examples/VCC_Max.certs
author boehmes
Wed May 12 23:54:06 2010 +0200 (2010-05-12)
changeset 36900 631e961a9e95
parent 35981 bd4e0d68c56d
child 37156 42c53229800d
permissions -rw-r--r--
updated SMT certificates
boehmes@36900
     1
95b4b08061ee75475bbfdf75c59af3c86af542dc 7862 0
boehmes@34994
     2
#2 := false
boehmes@36900
     3
decl f111 :: (-> S4 S5 int)
boehmes@36900
     4
decl f67 :: (-> S5 int S3 S5)
boehmes@36900
     5
decl f9 :: S3
boehmes@36900
     6
#16 := f9
boehmes@36900
     7
decl ?v0!14 :: int
boehmes@36900
     8
#18498 := ?v0!14
boehmes@36900
     9
decl f44 :: (-> S3 int S5)
boehmes@36900
    10
decl f288 :: int
boehmes@36900
    11
#3006 := f288
boehmes@36900
    12
#3007 := (f44 f9 f288)
boehmes@36900
    13
#18503 := (f67 #3007 ?v0!14 f9)
boehmes@36900
    14
decl f287 :: S4
boehmes@36900
    15
#3004 := f287
boehmes@36900
    16
#18504 := (f111 f287 #18503)
boehmes@36900
    17
decl f299 :: int
boehmes@36900
    18
#3104 := f299
boehmes@36900
    19
#3222 := (f67 #3007 f299 f9)
boehmes@36900
    20
#3231 := (f111 f287 #3222)
boehmes@36900
    21
#30499 := (= #3231 #18504)
boehmes@36900
    22
#30505 := (not #30499)
boehmes@36900
    23
#127 := 0::int
boehmes@36900
    24
#4119 := -1::int
boehmes@36900
    25
#18825 := (* -1::int #18504)
boehmes@36900
    26
#30500 := (+ #3231 #18825)
boehmes@36900
    27
#30502 := (>= #30500 0::int)
boehmes@36900
    28
#30512 := (not #30502)
boehmes@36900
    29
decl f305 :: int
boehmes@36900
    30
#3240 := f305
boehmes@36900
    31
#13479 := (* -1::int f305)
boehmes@36900
    32
#30081 := (+ #3231 #13479)
boehmes@36900
    33
#30011 := (<= #30081 0::int)
boehmes@36900
    34
#30077 := (= #3231 f305)
boehmes@36900
    35
decl f304 :: int
boehmes@36900
    36
#3233 := f304
boehmes@36900
    37
#12510 := (= f304 f305)
boehmes@36900
    38
#18826 := (+ f305 #18825)
boehmes@36900
    39
#18827 := (>= #18826 0::int)
boehmes@36900
    40
#18812 := (* -1::int ?v0!14)
boehmes@36900
    41
decl f307 :: int
boehmes@36900
    42
#3250 := f307
boehmes@36900
    43
#18813 := (+ f307 #18812)
boehmes@36900
    44
#18814 := (<= #18813 0::int)
boehmes@36900
    45
#18500 := (>= ?v0!14 0::int)
boehmes@36900
    46
#22280 := (not #18500)
boehmes@36900
    47
#7548 := 4294967295::int
boehmes@36900
    48
#18499 := (<= ?v0!14 4294967295::int)
boehmes@36900
    49
#22279 := (not #18499)
boehmes@36900
    50
#22295 := (or #22279 #22280 #18814 #18827)
boehmes@36900
    51
#22300 := (not #22295)
boehmes@36900
    52
#168 := (:var 0 int)
boehmes@36900
    53
#3088 := (f67 #3007 #168 f9)
boehmes@36900
    54
#23202 := (pattern #3088)
boehmes@36900
    55
#15118 := (<= #168 4294967295::int)
boehmes@36900
    56
#19497 := (not #15118)
boehmes@36900
    57
#3089 := (f111 f287 #3088)
boehmes@36900
    58
#13480 := (+ #3089 #13479)
boehmes@36900
    59
#13481 := (<= #13480 0::int)
boehmes@36900
    60
#13460 := (* -1::int f307)
boehmes@36900
    61
#13468 := (+ #168 #13460)
boehmes@36900
    62
#13467 := (>= #13468 0::int)
boehmes@36900
    63
#4118 := (>= #168 0::int)
boehmes@36900
    64
#5040 := (not #4118)
boehmes@36900
    65
#22261 := (or #5040 #13467 #13481 #19497)
boehmes@36900
    66
#23219 := (forall (vars (?v0 int)) (:pat #23202) #22261)
boehmes@36900
    67
#23224 := (not #23219)
boehmes@36900
    68
decl f306 :: int
boehmes@36900
    69
#3242 := f306
boehmes@36900
    70
#13501 := (* -1::int f306)
boehmes@36900
    71
decl f286 :: int
boehmes@36900
    72
#3001 := f286
boehmes@36900
    73
#13502 := (+ f286 #13501)
boehmes@36900
    74
#13503 := (<= #13502 0::int)
boehmes@36900
    75
#3263 := (f67 #3007 f306 f9)
boehmes@36900
    76
#3264 := (f111 f287 #3263)
boehmes@36900
    77
#12552 := (= f305 #3264)
boehmes@36900
    78
#22246 := (not #12552)
boehmes@36900
    79
#22247 := (or #22246 #13503)
boehmes@36900
    80
#22248 := (not #22247)
boehmes@36900
    81
#23227 := (or #22248 #23224)
boehmes@34994
    82
#23230 := (not #23227)
boehmes@36900
    83
#23233 := (or #23230 #22300)
boehmes@34994
    84
#23236 := (not #23233)
boehmes@36900
    85
#13461 := (+ f286 #13460)
boehmes@36900
    86
#13459 := (>= #13461 0::int)
boehmes@36900
    87
#13464 := (not #13459)
boehmes@36900
    88
#23239 := (or #13464 #23236)
boehmes@36900
    89
#23242 := (not #23239)
boehmes@36900
    90
#23245 := (or #13464 #23242)
boehmes@36900
    91
#23248 := (not #23245)
boehmes@36900
    92
#15808 := 4294967294::int
boehmes@36900
    93
#15809 := (<= f299 4294967294::int)
boehmes@36900
    94
#18481 := (not #15809)
boehmes@36900
    95
#13528 := (+ f299 #13460)
boehmes@36900
    96
#13527 := (= #13528 -1::int)
boehmes@36900
    97
#13531 := (not #13527)
boehmes@36900
    98
#901 := 2::int
boehmes@36900
    99
#13451 := (>= f307 2::int)
boehmes@36900
   100
#22323 := (not #13451)
boehmes@36900
   101
#13443 := (>= f299 -1::int)
boehmes@36900
   102
#18478 := (not #13443)
boehmes@36900
   103
#13434 := (>= f306 0::int)
boehmes@36900
   104
#22322 := (not #13434)
boehmes@36900
   105
decl f291 :: (-> S4 S2 S2 int S3 S1)
boehmes@36900
   106
decl f6 :: S3
boehmes@36900
   107
#12 := f6
boehmes@36900
   108
decl f274 :: S2
boehmes@36900
   109
#2977 := f274
boehmes@36900
   110
decl f270 :: S2
boehmes@36900
   111
#2973 := f270
boehmes@36900
   112
#3252 := (f291 f287 f270 f274 f307 f6)
boehmes@36900
   113
decl f1 :: S1
boehmes@36900
   114
#4 := f1
boehmes@36900
   115
#12531 := (= f1 #3252)
boehmes@36900
   116
#12601 := (not #12531)
boehmes@36900
   117
#23251 := (or #12601 #22322 #18478 #22323 #13531 #18481 #23248)
boehmes@36900
   118
#23254 := (not #23251)
boehmes@36900
   119
#23257 := (or #18478 #18481 #23254)
boehmes@36900
   120
#23260 := (not #23257)
boehmes@36900
   121
#8 := 1::int
boehmes@36900
   122
#13425 := (>= f299 1::int)
boehmes@36900
   123
#13565 := (not #13425)
boehmes@36900
   124
#12513 := (= f299 f306)
boehmes@36900
   125
#12640 := (not #12513)
boehmes@36900
   126
#12649 := (not #12510)
boehmes@36900
   127
decl f276 :: S2
boehmes@36900
   128
#2979 := f276
boehmes@36900
   129
decl f271 :: S2
boehmes@36900
   130
#2974 := f271
boehmes@36900
   131
#3237 := (f291 f287 f271 f276 f299 f6)
boehmes@36900
   132
#12505 := (= f1 #3237)
boehmes@36900
   133
#12667 := (not #12505)
boehmes@36900
   134
decl f278 :: S2
boehmes@36900
   135
#2981 := f278
boehmes@36900
   136
decl f272 :: S2
boehmes@36900
   137
#2975 := f272
boehmes@36900
   138
#3235 := (f291 f287 f272 f278 f304 f9)
boehmes@36900
   139
#12502 := (= f1 #3235)
boehmes@36900
   140
#12676 := (not #12502)
boehmes@36900
   141
#12499 := (= #3231 f304)
boehmes@36900
   142
#12685 := (not #12499)
boehmes@36900
   143
decl f69 :: (-> S4 S5 S1)
boehmes@36900
   144
#3228 := (f69 f287 #3222)
boehmes@36900
   145
#12493 := (= f1 #3228)
boehmes@36900
   146
#18449 := (not #12493)
boehmes@36900
   147
decl f49 :: (-> S5 S3 S1)
boehmes@36900
   148
#3223 := (f49 #3222 f9)
boehmes@36900
   149
#12484 := (= f1 #3223)
boehmes@36900
   150
#18440 := (not #12484)
boehmes@36900
   151
#23263 := (or #18440 #18449 #12685 #12676 #12667 #12649 #12640 #13565 #22322 #23260)
boehmes@36900
   152
#23266 := (not #23263)
boehmes@36900
   153
decl f26 :: (-> S4 S5 S5)
boehmes@36900
   154
decl f136 :: (-> S14 S5)
boehmes@36900
   155
decl f59 :: (-> S13 S5 S14)
boehmes@36900
   156
decl f60 :: (-> S4 S13)
boehmes@36900
   157
#3185 := (f60 f287)
boehmes@36900
   158
#27673 := (f59 #3185 #3222)
boehmes@36900
   159
#29196 := (f136 #27673)
boehmes@36900
   160
#29199 := (f26 f287 #29196)
boehmes@36900
   161
decl f27 :: S5
boehmes@36900
   162
#82 := f27
boehmes@36900
   163
#29200 := (= f27 #29199)
boehmes@36900
   164
decl f211 :: (-> S4 S5 S1)
boehmes@36900
   165
#29197 := (f211 f287 #29196)
boehmes@36900
   166
#29198 := (= f1 #29197)
boehmes@36900
   167
#29256 := (or #29198 #29200)
boehmes@36900
   168
#29259 := (not #29256)
boehmes@36900
   169
decl f137 :: (-> S14 S1)
boehmes@36900
   170
#29209 := (f137 #27673)
boehmes@36900
   171
#29210 := (= f1 #29209)
boehmes@36900
   172
#29211 := (not #29210)
boehmes@36900
   173
decl f28 :: (-> S4 S5 S1)
boehmes@36900
   174
#29206 := (f28 f287 #29196)
boehmes@36900
   175
#29207 := (= f1 #29206)
boehmes@36900
   176
#29208 := (not #29207)
boehmes@36900
   177
#29250 := (or #29208 #29211)
boehmes@36900
   178
#29253 := (not #29250)
boehmes@36900
   179
decl f13 :: (-> S3 S8)
boehmes@36900
   180
decl f14 :: (-> S5 S3)
boehmes@36900
   181
#27769 := (f14 #3222)
boehmes@36900
   182
#29214 := (f13 #27769)
boehmes@36900
   183
decl f15 :: S8
boehmes@36900
   184
#33 := f15
boehmes@36900
   185
#29232 := (= f15 #29214)
boehmes@36900
   186
#29247 := (not #29232)
boehmes@36900
   187
#29203 := (f14 #29196)
boehmes@36900
   188
#29204 := (f13 #29203)
boehmes@36900
   189
#29205 := (= f15 #29204)
boehmes@36900
   190
#29265 := (or #29205 #29247 #29253 #29259)
boehmes@36900
   191
#29270 := (not #29265)
boehmes@36900
   192
#29221 := (f26 f287 #3222)
boehmes@36900
   193
#29222 := (= f27 #29221)
boehmes@36900
   194
#29219 := (f211 f287 #3222)
boehmes@36900
   195
#29220 := (= f1 #29219)
boehmes@36900
   196
#29235 := (or #29220 #29222)
boehmes@36900
   197
#29238 := (not #29235)
boehmes@36900
   198
#29241 := (or #29232 #29238)
boehmes@36900
   199
#29244 := (not #29241)
boehmes@36900
   200
#29273 := (or #29244 #29270)
boehmes@36900
   201
#29276 := (not #29273)
boehmes@36900
   202
decl f25 :: (-> S4 S5 S1)
boehmes@36900
   203
#3225 := (f25 f287 #3222)
boehmes@36900
   204
#12487 := (= f1 #3225)
boehmes@36900
   205
#18443 := (not #12487)
boehmes@36900
   206
#29279 := (or #18443 #29276)
boehmes@36900
   207
#29282 := (not #29279)
boehmes@36900
   208
#29285 := (iff #12493 #29282)
boehmes@36900
   209
#29865 := (not #29285)
boehmes@36900
   210
#29981 := [hypothesis]: #29865
boehmes@36900
   211
#28 := (:var 0 S5)
boehmes@36900
   212
#52 := (:var 1 S4)
boehmes@36900
   213
#2404 := (f69 #52 #28)
boehmes@36900
   214
#2405 := (pattern #2404)
boehmes@36900
   215
#290 := (f60 #52)
boehmes@36900
   216
#2407 := (f59 #290 #28)
boehmes@36900
   217
#2411 := (f136 #2407)
boehmes@36900
   218
#2422 := (f211 #52 #2411)
boehmes@36900
   219
#10612 := (= f1 #2422)
boehmes@36900
   220
#2420 := (f26 #52 #2411)
boehmes@36900
   221
#10609 := (= f27 #2420)
boehmes@36900
   222
#10615 := (or #10609 #10612)
boehmes@36900
   223
#21954 := (not #10615)
boehmes@36900
   224
#2416 := (f14 #2411)
boehmes@36900
   225
#2417 := (f13 #2416)
boehmes@36900
   226
#10603 := (= f15 #2417)
boehmes@36900
   227
#2412 := (f28 #52 #2411)
boehmes@36900
   228
#10594 := (= f1 #2412)
boehmes@36900
   229
#10597 := (not #10594)
boehmes@36900
   230
#2408 := (f137 #2407)
boehmes@36900
   231
#10588 := (= f1 #2408)
boehmes@36900
   232
#10591 := (not #10588)
boehmes@36900
   233
#10600 := (or #10591 #10597)
boehmes@36900
   234
#21953 := (not #10600)
boehmes@36900
   235
#31 := (f14 #28)
boehmes@36900
   236
#32 := (f13 #31)
boehmes@36900
   237
#34 := (= #32 f15)
boehmes@36900
   238
#57 := (not #34)
boehmes@36900
   239
#21955 := (or #57 #21953 #10603 #21954)
boehmes@36900
   240
#21956 := (not #21955)
boehmes@36900
   241
#2428 := (f211 #52 #28)
boehmes@36900
   242
#10627 := (= f1 #2428)
boehmes@36900
   243
#148 := (f26 #52 #28)
boehmes@36900
   244
#3677 := (= f27 #148)
boehmes@36900
   245
#10630 := (or #3677 #10627)
boehmes@36900
   246
#21948 := (not #10630)
boehmes@36900
   247
#21949 := (or #34 #21948)
boehmes@36900
   248
#21950 := (not #21949)
boehmes@36900
   249
#21959 := (or #21950 #21956)
boehmes@36900
   250
#21965 := (not #21959)
boehmes@36900
   251
#152 := (f25 #52 #28)
boehmes@36900
   252
#3683 := (= f1 #152)
boehmes@36900
   253
#11206 := (not #3683)
boehmes@36900
   254
#21966 := (or #11206 #21965)
boehmes@36900
   255
#21967 := (not #21966)
boehmes@36900
   256
#10584 := (= f1 #2404)
boehmes@36900
   257
#21972 := (iff #10584 #21967)
boehmes@36900
   258
#21975 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #2405) #21972)
boehmes@36900
   259
#10606 := (not #10603)
boehmes@36900
   260
#10648 := (and #34 #10600 #10606 #10615)
boehmes@36900
   261
#10633 := (and #57 #10630)
boehmes@36900
   262
#10654 := (or #10633 #10648)
boehmes@36900
   263
#10659 := (and #3683 #10654)
boehmes@36900
   264
#10662 := (iff #10584 #10659)
boehmes@36900
   265
#10665 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #2405) #10662)
boehmes@36900
   266
#21976 := (iff #10665 #21975)
boehmes@36900
   267
#21973 := (iff #10662 #21972)
boehmes@36900
   268
#21970 := (iff #10659 #21967)
boehmes@36900
   269
#21962 := (and #3683 #21959)
boehmes@36900
   270
#21968 := (iff #21962 #21967)
boehmes@36900
   271
#21969 := [rewrite]: #21968
boehmes@36900
   272
#21963 := (iff #10659 #21962)
boehmes@36900
   273
#21960 := (iff #10654 #21959)
boehmes@36900
   274
#21957 := (iff #10648 #21956)
boehmes@36900
   275
#21958 := [rewrite]: #21957
boehmes@36900
   276
#21951 := (iff #10633 #21950)
boehmes@36900
   277
#21952 := [rewrite]: #21951
boehmes@36900
   278
#21961 := [monotonicity #21952 #21958]: #21960
boehmes@36900
   279
#21964 := [monotonicity #21961]: #21963
boehmes@36900
   280
#21971 := [trans #21964 #21969]: #21970
boehmes@36900
   281
#21974 := [monotonicity #21971]: #21973
boehmes@36900
   282
#21977 := [quant-intro #21974]: #21976
boehmes@36900
   283
#17898 := (~ #10665 #10665)
boehmes@36900
   284
#17896 := (~ #10662 #10662)
boehmes@36900
   285
#17897 := [refl]: #17896
boehmes@36900
   286
#17899 := [nnf-pos #17897]: #17898
boehmes@36900
   287
#2429 := (= #2428 f1)
boehmes@36900
   288
#149 := (= #148 f27)
boehmes@36900
   289
#2430 := (or #149 #2429)
boehmes@36900
   290
#2431 := (and #57 #2430)
boehmes@36900
   291
#2423 := (= #2422 f1)
boehmes@36900
   292
#2421 := (= #2420 f27)
boehmes@36900
   293
#2424 := (or #2421 #2423)
boehmes@36900
   294
#2418 := (= #2417 f15)
boehmes@36900
   295
#2419 := (not #2418)
boehmes@36900
   296
#2425 := (and #2419 #2424)
boehmes@36900
   297
#2413 := (= #2412 f1)
boehmes@36900
   298
#2414 := (not #2413)
boehmes@36900
   299
#2409 := (= #2408 f1)
boehmes@36900
   300
#2410 := (not #2409)
boehmes@36900
   301
#2415 := (or #2410 #2414)
boehmes@36900
   302
#2426 := (and #2415 #2425)
boehmes@36900
   303
#2427 := (and #34 #2426)
boehmes@36900
   304
#2432 := (or #2427 #2431)
boehmes@36900
   305
#153 := (= #152 f1)
boehmes@36900
   306
#2433 := (and #153 #2432)
boehmes@36900
   307
#2406 := (= #2404 f1)
boehmes@36900
   308
#2434 := (iff #2406 #2433)
boehmes@36900
   309
#2435 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #2405) #2434)
boehmes@36900
   310
#10668 := (iff #2435 #10665)
boehmes@36900
   311
#10618 := (and #10606 #10615)
boehmes@36900
   312
#10621 := (and #10600 #10618)
boehmes@36900
   313
#10624 := (and #34 #10621)
boehmes@36900
   314
#10636 := (or #10624 #10633)
boehmes@36900
   315
#10639 := (and #3683 #10636)
boehmes@36900
   316
#10642 := (iff #10584 #10639)
boehmes@36900
   317
#10645 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #2405) #10642)
boehmes@36900
   318
#10666 := (iff #10645 #10665)
boehmes@36900
   319
#10663 := (iff #10642 #10662)
boehmes@36900
   320
#10660 := (iff #10639 #10659)
boehmes@36900
   321
#10657 := (iff #10636 #10654)
boehmes@36900
   322
#10651 := (or #10648 #10633)
boehmes@36900
   323
#10655 := (iff #10651 #10654)
boehmes@36900
   324
#10656 := [rewrite]: #10655
boehmes@36900
   325
#10652 := (iff #10636 #10651)
boehmes@36900
   326
#10649 := (iff #10624 #10648)
boehmes@36900
   327
#10650 := [rewrite]: #10649
boehmes@36900
   328
#10653 := [monotonicity #10650]: #10652
boehmes@36900
   329
#10658 := [trans #10653 #10656]: #10657
boehmes@36900
   330
#10661 := [monotonicity #10658]: #10660
boehmes@36900
   331
#10664 := [monotonicity #10661]: #10663
boehmes@36900
   332
#10667 := [quant-intro #10664]: #10666
boehmes@36900
   333
#10646 := (iff #2435 #10645)
boehmes@36900
   334
#10643 := (iff #2434 #10642)
boehmes@36900
   335
#10640 := (iff #2433 #10639)
boehmes@36900
   336
#10637 := (iff #2432 #10636)
boehmes@36900
   337
#10634 := (iff #2431 #10633)
boehmes@36900
   338
#10631 := (iff #2430 #10630)
boehmes@36900
   339
#10628 := (iff #2429 #10627)
boehmes@36900
   340
#10629 := [rewrite]: #10628
boehmes@36900
   341
#3678 := (iff #149 #3677)
boehmes@36900
   342
#3679 := [rewrite]: #3678
boehmes@36900
   343
#10632 := [monotonicity #3679 #10629]: #10631
boehmes@36900
   344
#10635 := [monotonicity #10632]: #10634
boehmes@36900
   345
#10625 := (iff #2427 #10624)
boehmes@36900
   346
#10622 := (iff #2426 #10621)
boehmes@36900
   347
#10619 := (iff #2425 #10618)
boehmes@36900
   348
#10616 := (iff #2424 #10615)
boehmes@36900
   349
#10613 := (iff #2423 #10612)
boehmes@36900
   350
#10614 := [rewrite]: #10613
boehmes@36900
   351
#10610 := (iff #2421 #10609)
boehmes@36900
   352
#10611 := [rewrite]: #10610
boehmes@36900
   353
#10617 := [monotonicity #10611 #10614]: #10616
boehmes@36900
   354
#10607 := (iff #2419 #10606)
boehmes@36900
   355
#10604 := (iff #2418 #10603)
boehmes@36900
   356
#10605 := [rewrite]: #10604
boehmes@36900
   357
#10608 := [monotonicity #10605]: #10607
boehmes@36900
   358
#10620 := [monotonicity #10608 #10617]: #10619
boehmes@36900
   359
#10601 := (iff #2415 #10600)
boehmes@36900
   360
#10598 := (iff #2414 #10597)
boehmes@36900
   361
#10595 := (iff #2413 #10594)
boehmes@36900
   362
#10596 := [rewrite]: #10595
boehmes@36900
   363
#10599 := [monotonicity #10596]: #10598
boehmes@36900
   364
#10592 := (iff #2410 #10591)
boehmes@36900
   365
#10589 := (iff #2409 #10588)
boehmes@36900
   366
#10590 := [rewrite]: #10589
boehmes@36900
   367
#10593 := [monotonicity #10590]: #10592
boehmes@36900
   368
#10602 := [monotonicity #10593 #10599]: #10601
boehmes@36900
   369
#10623 := [monotonicity #10602 #10620]: #10622
boehmes@36900
   370
#10626 := [monotonicity #10623]: #10625
boehmes@36900
   371
#10638 := [monotonicity #10626 #10635]: #10637
boehmes@36900
   372
#3684 := (iff #153 #3683)
boehmes@36900
   373
#3685 := [rewrite]: #3684
boehmes@36900
   374
#10641 := [monotonicity #3685 #10638]: #10640
boehmes@36900
   375
#10586 := (iff #2406 #10584)
boehmes@36900
   376
#10587 := [rewrite]: #10586
boehmes@36900
   377
#10644 := [monotonicity #10587 #10641]: #10643
boehmes@36900
   378
#10647 := [quant-intro #10644]: #10646
boehmes@36900
   379
#10669 := [trans #10647 #10667]: #10668
boehmes@36900
   380
#10583 := [asserted]: #2435
boehmes@36900
   381
#10670 := [mp #10583 #10669]: #10665
boehmes@36900
   382
#17900 := [mp~ #10670 #17899]: #10665
boehmes@36900
   383
#21978 := [mp #17900 #21977]: #21975
boehmes@36900
   384
#27322 := (not #21975)
boehmes@36900
   385
#29781 := (or #27322 #29285)
boehmes@36900
   386
#29201 := (or #29200 #29198)
boehmes@36900
   387
#29202 := (not #29201)
boehmes@36900
   388
#29212 := (or #29211 #29208)
boehmes@36900
   389
#29213 := (not #29212)
boehmes@36900
   390
#29215 := (= #29214 f15)
boehmes@36900
   391
#29216 := (not #29215)
boehmes@36900
   392
#29217 := (or #29216 #29213 #29205 #29202)
boehmes@36900
   393
#29218 := (not #29217)
boehmes@36900
   394
#29223 := (or #29222 #29220)
boehmes@36900
   395
#29224 := (not #29223)
boehmes@36900
   396
#29225 := (or #29215 #29224)
boehmes@36900
   397
#29226 := (not #29225)
boehmes@36900
   398
#29227 := (or #29226 #29218)
boehmes@36900
   399
#29228 := (not #29227)
boehmes@36900
   400
#29229 := (or #18443 #29228)
boehmes@36900
   401
#29230 := (not #29229)
boehmes@36900
   402
#29231 := (iff #12493 #29230)
boehmes@36900
   403
#29782 := (or #27322 #29231)
boehmes@36900
   404
#29902 := (iff #29782 #29781)
boehmes@36900
   405
#29917 := (iff #29781 #29781)
boehmes@36900
   406
#29933 := [rewrite]: #29917
boehmes@36900
   407
#29286 := (iff #29231 #29285)
boehmes@36900
   408
#29283 := (iff #29230 #29282)
boehmes@36900
   409
#29280 := (iff #29229 #29279)
boehmes@36900
   410
#29277 := (iff #29228 #29276)
boehmes@36900
   411
#29274 := (iff #29227 #29273)
boehmes@36900
   412
#29271 := (iff #29218 #29270)
boehmes@36900
   413
#29268 := (iff #29217 #29265)
boehmes@36900
   414
#29262 := (or #29247 #29253 #29205 #29259)
boehmes@36900
   415
#29266 := (iff #29262 #29265)
boehmes@36900
   416
#29267 := [rewrite]: #29266
boehmes@36900
   417
#29263 := (iff #29217 #29262)
boehmes@36900
   418
#29260 := (iff #29202 #29259)
boehmes@36900
   419
#29257 := (iff #29201 #29256)
boehmes@36900
   420
#29258 := [rewrite]: #29257
boehmes@36900
   421
#29261 := [monotonicity #29258]: #29260
boehmes@36900
   422
#29254 := (iff #29213 #29253)
boehmes@36900
   423
#29251 := (iff #29212 #29250)
boehmes@36900
   424
#29252 := [rewrite]: #29251
boehmes@36900
   425
#29255 := [monotonicity #29252]: #29254
boehmes@36900
   426
#29248 := (iff #29216 #29247)
boehmes@36900
   427
#29233 := (iff #29215 #29232)
boehmes@36900
   428
#29234 := [rewrite]: #29233
boehmes@36900
   429
#29249 := [monotonicity #29234]: #29248
boehmes@36900
   430
#29264 := [monotonicity #29249 #29255 #29261]: #29263
boehmes@36900
   431
#29269 := [trans #29264 #29267]: #29268
boehmes@36900
   432
#29272 := [monotonicity #29269]: #29271
boehmes@36900
   433
#29245 := (iff #29226 #29244)
boehmes@36900
   434
#29242 := (iff #29225 #29241)
boehmes@36900
   435
#29239 := (iff #29224 #29238)
boehmes@36900
   436
#29236 := (iff #29223 #29235)
boehmes@36900
   437
#29237 := [rewrite]: #29236
boehmes@36900
   438
#29240 := [monotonicity #29237]: #29239
boehmes@36900
   439
#29243 := [monotonicity #29234 #29240]: #29242
boehmes@36900
   440
#29246 := [monotonicity #29243]: #29245
boehmes@36900
   441
#29275 := [monotonicity #29246 #29272]: #29274
boehmes@36900
   442
#29278 := [monotonicity #29275]: #29277
boehmes@36900
   443
#29281 := [monotonicity #29278]: #29280
boehmes@36900
   444
#29284 := [monotonicity #29281]: #29283
boehmes@36900
   445
#29287 := [monotonicity #29284]: #29286
boehmes@36900
   446
#29906 := [monotonicity #29287]: #29902
boehmes@36900
   447
#29798 := [trans #29906 #29933]: #29902
boehmes@36900
   448
#29896 := [quant-inst]: #29782
boehmes@36900
   449
#29799 := [mp #29896 #29798]: #29781
boehmes@36900
   450
#29774 := [unit-resolution #29799 #21978 #29981]: false
boehmes@36900
   451
#29946 := [lemma #29774]: #29285
boehmes@36900
   452
#30008 := (or #29865 #12493)
boehmes@36900
   453
#29909 := [hypothesis]: #29265
boehmes@36900
   454
decl f117 :: (-> S5 int)
boehmes@36900
   455
#3008 := (f117 #3007)
boehmes@36900
   456
decl f125 :: (-> S3 int S3)
boehmes@36900
   457
#3005 := (f125 f9 f286)
boehmes@36900
   458
#3009 := (f44 #3005 #3008)
boehmes@36900
   459
#3012 := (f26 f287 #3009)
boehmes@36900
   460
#29965 := (= #3012 #29199)
boehmes@36900
   461
#29974 := (= #29199 #3012)
boehmes@36900
   462
#30151 := (= #29196 #3009)
boehmes@36900
   463
decl f144 :: (-> S3 int)
boehmes@36900
   464
#24837 := (f144 #3005)
boehmes@36900
   465
decl f145 :: (-> S3 S3)
boehmes@36900
   466
#24835 := (f145 #3005)
boehmes@36900
   467
#26983 := (f125 #24835 #24837)
boehmes@36900
   468
#26984 := (f44 #26983 #3008)
boehmes@36900
   469
#28336 := (= #26984 #3009)
boehmes@36900
   470
#28334 := (= #26983 #3005)
boehmes@36900
   471
#28332 := (= #24837 f286)
boehmes@36900
   472
#24838 := (= f286 #24837)
boehmes@36900
   473
#335 := (:var 1 S3)
boehmes@36900
   474
#1367 := (f125 #335 #168)
boehmes@36900
   475
#1604 := (pattern #1367)
boehmes@36900
   476
#1615 := (f144 #1367)
boehmes@36900
   477
#8360 := (= #168 #1615)
boehmes@36900
   478
#8363 := (forall (vars (?v0 S3) (?v1 int)) (:pat #1604) #8360)
boehmes@36900
   479
#17274 := (~ #8363 #8363)
boehmes@36900
   480
#17272 := (~ #8360 #8360)
boehmes@36900
   481
#17273 := [refl]: #17272
boehmes@36900
   482
#17275 := [nnf-pos #17273]: #17274
boehmes@36900
   483
#1616 := (= #1615 #168)
boehmes@36900
   484
#1617 := (forall (vars (?v0 S3) (?v1 int)) (:pat #1604) #1616)
boehmes@36900
   485
#8364 := (iff #1617 #8363)
boehmes@36900
   486
#8361 := (iff #1616 #8360)
boehmes@36900
   487
#8362 := [rewrite]: #8361
boehmes@36900
   488
#8365 := [quant-intro #8362]: #8364
boehmes@36900
   489
#8359 := [asserted]: #1617
boehmes@36900
   490
#8368 := [mp #8359 #8365]: #8363
boehmes@36900
   491
#17276 := [mp~ #8368 #17275]: #8363
boehmes@36900
   492
#24844 := (not #8363)
boehmes@36900
   493
#24845 := (or #24844 #24838)
boehmes@36900
   494
#24846 := [quant-inst]: #24845
boehmes@36900
   495
#28245 := [unit-resolution #24846 #17276]: #24838
boehmes@36900
   496
#28333 := [symm #28245]: #28332
boehmes@36900
   497
#28224 := (= #24835 f9)
boehmes@36900
   498
#24836 := (= f9 #24835)
boehmes@36900
   499
#1618 := (f145 #1367)
boehmes@36900
   500
#8367 := (= #335 #1618)
boehmes@36900
   501
#8371 := (forall (vars (?v0 S3) (?v1 int)) (:pat #1604) #8367)
boehmes@36900
   502
#17279 := (~ #8371 #8371)
boehmes@36900
   503
#17277 := (~ #8367 #8367)
boehmes@36900
   504
#17278 := [refl]: #17277
boehmes@36900
   505
#17280 := [nnf-pos #17278]: #17279
boehmes@36900
   506
#1619 := (= #1618 #335)
boehmes@36900
   507
#1620 := (forall (vars (?v0 S3) (?v1 int)) (:pat #1604) #1619)
boehmes@36900
   508
#8372 := (iff #1620 #8371)
boehmes@36900
   509
#8369 := (iff #1619 #8367)
boehmes@36900
   510
#8370 := [rewrite]: #8369
boehmes@36900
   511
#8373 := [quant-intro #8370]: #8372
boehmes@36900
   512
#8366 := [asserted]: #1620
boehmes@36900
   513
#8376 := [mp #8366 #8373]: #8371
boehmes@36900
   514
#17281 := [mp~ #8376 #17280]: #8371
boehmes@36900
   515
#24839 := (not #8371)
boehmes@36900
   516
#24840 := (or #24839 #24836)
boehmes@36900
   517
#24841 := [quant-inst]: #24840
boehmes@36900
   518
#28223 := [unit-resolution #24841 #17281]: #24836
boehmes@36900
   519
#28225 := [symm #28223]: #28224
boehmes@36900
   520
#28335 := [monotonicity #28225 #28333]: #28334
boehmes@36900
   521
#28337 := [monotonicity #28335]: #28336
boehmes@36900
   522
#30149 := (= #29196 #26984)
boehmes@36900
   523
decl f126 :: (-> S5 S5 int)
boehmes@36900
   524
decl f29 :: (-> int S5)
boehmes@36900
   525
decl f30 :: (-> S5 int)
boehmes@36900
   526
#3041 := (f30 #3007)
boehmes@36900
   527
#24672 := (f29 #3041)
boehmes@36900
   528
#26961 := (f14 #24672)
boehmes@36900
   529
#28957 := (f67 #24672 f299 #26961)
boehmes@36900
   530
#28958 := (f126 #28957 #24672)
boehmes@36900
   531
#28982 := (f67 #26984 #28958 #24835)
boehmes@36900
   532
#28986 := (f59 #3185 #28982)
boehmes@36900
   533
#28992 := (f136 #28986)
boehmes@36900
   534
#30147 := (= #28992 #26984)
boehmes@36900
   535
#28993 := (= #26984 #28992)
boehmes@36900
   536
#28994 := (not #28993)
boehmes@36900
   537
#28990 := (f137 #28986)
boehmes@36900
   538
#28991 := (= f1 #28990)
boehmes@36900
   539
decl f68 :: (-> S14 S1)
boehmes@36900
   540
#28987 := (f68 #28986)
boehmes@36900
   541
#28988 := (= f1 #28987)
boehmes@36900
   542
#28989 := (not #28988)
boehmes@36900
   543
#28983 := (f25 f287 #28982)
boehmes@36900
   544
#28984 := (= f1 #28983)
boehmes@36900
   545
#28985 := (not #28984)
boehmes@36900
   546
#29015 := (or #28985 #28989 #28991 #28994)
boehmes@36900
   547
#29018 := (not #29015)
boehmes@36900
   548
#29008 := (* -1::int #28958)
boehmes@36900
   549
#29009 := (+ #24837 #29008)
boehmes@36900
   550
#29010 := (<= #29009 0::int)
boehmes@36900
   551
#30108 := (not #29010)
boehmes@36900
   552
#29118 := (+ f299 #29008)
boehmes@36900
   553
#29120 := (>= #29118 0::int)
boehmes@36900
   554
#28959 := (= f299 #28958)
boehmes@36900
   555
#21 := (:var 1 S5)
boehmes@36900
   556
#1399 := (f14 #21)
boehmes@36900
   557
#1400 := (f67 #21 #168 #1399)
boehmes@36900
   558
#1401 := (pattern #1400)
boehmes@36900
   559
#1402 := (f126 #1400 #21)
boehmes@36900
   560
#7740 := (= #168 #1402)
boehmes@36900
   561
#7744 := (forall (vars (?v0 S5) (?v1 int)) (:pat #1401) #7740)
boehmes@36900
   562
#16989 := (~ #7744 #7744)
boehmes@36900
   563
#16987 := (~ #7740 #7740)
boehmes@36900
   564
#16988 := [refl]: #16987
boehmes@36900
   565
#16990 := [nnf-pos #16988]: #16989
boehmes@36900
   566
#1403 := (= #1402 #168)
boehmes@36900
   567
#1404 := (forall (vars (?v0 S5) (?v1 int)) (:pat #1401) #1403)
boehmes@36900
   568
#7745 := (iff #1404 #7744)
boehmes@36900
   569
#7742 := (iff #1403 #7740)
boehmes@36900
   570
#7743 := [rewrite]: #7742
boehmes@36900
   571
#7746 := [quant-intro #7743]: #7745
boehmes@36900
   572
#7739 := [asserted]: #1404
boehmes@36900
   573
#7749 := [mp #7739 #7746]: #7744
boehmes@36900
   574
#16991 := [mp~ #7749 #16990]: #7744
boehmes@36900
   575
#26968 := (not #7744)
boehmes@36900
   576
#28962 := (or #26968 #28959)
boehmes@36900
   577
#28963 := [quant-inst]: #28962
boehmes@36900
   578
#29598 := [unit-resolution #28963 #16991]: #28959
boehmes@36900
   579
#29599 := (not #28959)
boehmes@36900
   580
#30105 := (or #29599 #29120)
boehmes@36900
   581
#30106 := [th-lemma]: #30105
boehmes@36900
   582
#30107 := [unit-resolution #30106 #29598]: #29120
boehmes@36900
   583
#13446 := (* -1::int f299)
boehmes@36900
   584
#13709 := (+ f286 #13446)
boehmes@36900
   585
#13710 := (<= #13709 0::int)
boehmes@36900
   586
#13711 := (not #13710)
boehmes@36900
   587
#13618 := (* -1::int #3231)
boehmes@36900
   588
decl f297 :: int
boehmes@36900
   589
#3096 := f297
boehmes@36900
   590
#13619 := (+ f297 #13618)
boehmes@36900
   591
#13617 := (>= #13619 0::int)
boehmes@36900
   592
#13616 := (not #13617)
boehmes@36900
   593
decl f298 :: int
boehmes@36900
   594
#3100 := f298
boehmes@36900
   595
#13422 := (>= f298 0::int)
boehmes@36900
   596
#22363 := (not #13422)
boehmes@36900
   597
#12751 := (= f298 f306)
boehmes@36900
   598
#12757 := (not #12751)
boehmes@36900
   599
#12748 := (= f297 f305)
boehmes@36900
   600
#12766 := (not #12748)
boehmes@36900
   601
#23293 := (or #12766 #12757 #22363 #13565 #22322 #13616 #23260)
boehmes@36900
   602
#23296 := (not #23293)
boehmes@36900
   603
#23269 := (or #18440 #18449 #23266)
boehmes@36900
   604
#23272 := (not #23269)
boehmes@36900
   605
#23275 := (or #18440 #18443 #23272)
boehmes@36900
   606
#23278 := (not #23275)
boehmes@36900
   607
#23281 := (or #18440 #18443 #23278)
boehmes@36900
   608
#23284 := (not #23281)
boehmes@36900
   609
#23287 := (or #22363 #13565 #13617 #23284)
boehmes@36900
   610
#23290 := (not #23287)
boehmes@36900
   611
#23299 := (or #23290 #23296)
boehmes@36900
   612
#23302 := (not #23299)
boehmes@36900
   613
#23305 := (or #18440 #18449 #22363 #13565 #23302)
boehmes@36900
   614
#23308 := (not #23305)
boehmes@36900
   615
#23311 := (or #18440 #18449 #23308)
boehmes@36900
   616
#23314 := (not #23311)
boehmes@36900
   617
#23317 := (or #18440 #18443 #23314)
boehmes@36900
   618
#23320 := (not #23317)
boehmes@36900
   619
#23323 := (or #18440 #18443 #23320)
boehmes@36900
   620
#23326 := (not #23323)
boehmes@36900
   621
#23329 := (or #22363 #13565 #13710 #23326)
boehmes@36900
   622
#23332 := (not #23329)
boehmes@36900
   623
decl ?v0!15 :: int
boehmes@36900
   624
#18622 := ?v0!15
boehmes@36900
   625
#18627 := (f67 #3007 ?v0!15 f9)
boehmes@36900
   626
#18628 := (f111 f287 #18627)
boehmes@36900
   627
#18973 := (* -1::int #18628)
boehmes@36900
   628
decl f303 :: int
boehmes@36900
   629
#3131 := f303
boehmes@36900
   630
#18974 := (+ f303 #18973)
boehmes@36900
   631
#18975 := (>= #18974 0::int)
boehmes@36900
   632
#18960 := (* -1::int ?v0!15)
boehmes@36900
   633
#18961 := (+ f286 #18960)
boehmes@36900
   634
#18962 := (<= #18961 0::int)
boehmes@36900
   635
#18624 := (>= ?v0!15 0::int)
boehmes@36900
   636
#22457 := (not #18624)
boehmes@36900
   637
#18623 := (<= ?v0!15 4294967295::int)
boehmes@36900
   638
#22456 := (not #18623)
boehmes@36900
   639
#22472 := (or #22456 #22457 #18962 #18975)
boehmes@36900
   640
#22477 := (not #22472)
boehmes@36900
   641
#13351 := (* -1::int f286)
boehmes@36900
   642
#13739 := (+ #168 #13351)
boehmes@36900
   643
#13738 := (>= #13739 0::int)
boehmes@36900
   644
#3138 := (= #3089 f303)
boehmes@36900
   645
#22430 := (not #3138)
boehmes@36900
   646
#22431 := (or #22430 #5040 #13738 #19497)
boehmes@36900
   647
#23343 := (forall (vars (?v0 int)) (:pat #23202) #22431)
boehmes@36900
   648
#23348 := (not #23343)
boehmes@36900
   649
#13750 := (* -1::int f303)
boehmes@36900
   650
#13751 := (+ #3089 #13750)
boehmes@36900
   651
#13752 := (<= #13751 0::int)
boehmes@36900
   652
#22422 := (or #5040 #13738 #13752 #19497)
boehmes@36900
   653
#23335 := (forall (vars (?v0 int)) (:pat #23202) #22422)
boehmes@36900
   654
#23340 := (not #23335)
boehmes@36900
   655
#23351 := (or #23340 #23348)
boehmes@36900
   656
#23354 := (not #23351)
boehmes@36900
   657
#23357 := (or #23354 #22477)
boehmes@36900
   658
#23360 := (not #23357)
boehmes@36900
   659
#12187 := (= f297 f303)
boehmes@36900
   660
#12222 := (not #12187)
boehmes@36900
   661
decl f302 :: int
boehmes@36900
   662
#3129 := f302
boehmes@36900
   663
#12184 := (= f298 f302)
boehmes@36900
   664
#12231 := (not #12184)
boehmes@36900
   665
decl f301 :: int
boehmes@36900
   666
#3127 := f301
boehmes@36900
   667
#12181 := (= f299 f301)
boehmes@36900
   668
#12240 := (not #12181)
boehmes@36900
   669
decl f300 :: int
boehmes@36900
   670
#3125 := f300
boehmes@36900
   671
#12178 := (= f297 f300)
boehmes@36900
   672
#12249 := (not #12178)
boehmes@36900
   673
#23363 := (or #12249 #12240 #12231 #12222 #22363 #13565 #13711 #23360)
boehmes@36900
   674
#23366 := (not #23363)
boehmes@36900
   675
#23369 := (or #23332 #23366)
boehmes@36900
   676
#23372 := (not #23369)
boehmes@36900
   677
#13915 := (* -1::int f297)
boehmes@36900
   678
#13916 := (+ #3089 #13915)
boehmes@36900
   679
#13917 := (<= #13916 0::int)
boehmes@36900
   680
#13904 := (+ #168 #13446)
boehmes@36900
   681
#13903 := (>= #13904 0::int)
boehmes@36900
   682
#22238 := (or #5040 #13903 #13917 #19497)
boehmes@36900
   683
#23211 := (forall (vars (?v0 int)) (:pat #23202) #22238)
boehmes@36900
   684
#23216 := (not #23211)
boehmes@36900
   685
#1340 := 255::int
boehmes@36900
   686
#15794 := (<= f297 255::int)
boehmes@36900
   687
#22507 := (not #15794)
boehmes@36900
   688
#15777 := (<= f298 4294967295::int)
boehmes@36900
   689
#22506 := (not #15777)
boehmes@36900
   690
#15760 := (<= f299 4294967295::int)
boehmes@36900
   691
#22505 := (not #15760)
boehmes@36900
   692
#13965 := (>= f297 0::int)
boehmes@36900
   693
#22503 := (not #13965)
boehmes@36900
   694
#13943 := (>= f299 0::int)
boehmes@36900
   695
#22502 := (not #13943)
boehmes@36900
   696
#13937 := (>= #13709 0::int)
boehmes@34994
   697
#13940 := (not #13937)
boehmes@36900
   698
#13886 := (* -1::int f298)
boehmes@36900
   699
#13887 := (+ f286 #13886)
boehmes@36900
   700
#13888 := (<= #13887 0::int)
boehmes@36900
   701
#13417 := (<= f286 0::int)
boehmes@36900
   702
decl f292 :: (-> S4 S2 S2 S5 S3 S1)
boehmes@36900
   703
decl f8 :: (-> S3 S3)
boehmes@36900
   704
#17 := (f8 f9)
boehmes@36900
   705
decl f281 :: S2
boehmes@36900
   706
#2984 := f281
boehmes@36900
   707
decl f273 :: S2
boehmes@36900
   708
#2976 := f273
boehmes@36900
   709
#3215 := (f292 f287 f273 f281 #3007 #17)
boehmes@36900
   710
#12467 := (= f1 #3215)
boehmes@36900
   711
#22501 := (not #12467)
boehmes@36900
   712
#3213 := (f291 f287 f273 f281 #3041 #17)
boehmes@36900
   713
#12464 := (= f1 #3213)
boehmes@36900
   714
#22500 := (not #12464)
boehmes@36900
   715
decl f280 :: S2
boehmes@36900
   716
#2983 := f280
boehmes@36900
   717
#3211 := (f291 f287 f273 f280 f286 f6)
boehmes@36900
   718
#12461 := (= f1 #3211)
boehmes@36900
   719
#12942 := (not #12461)
boehmes@36900
   720
#3209 := (f291 f287 f273 f278 f297 f9)
boehmes@36900
   721
#12458 := (= f1 #3209)
boehmes@36900
   722
#12951 := (not #12458)
boehmes@36900
   723
#3207 := (f291 f287 f273 f276 f298 f6)
boehmes@36900
   724
#12455 := (= f1 #3207)
boehmes@36900
   725
#12960 := (not #12455)
boehmes@36900
   726
#3205 := (f291 f287 f273 f274 f299 f6)
boehmes@36900
   727
#12452 := (= f1 #3205)
boehmes@36900
   728
#12969 := (not #12452)
boehmes@36900
   729
decl f179 :: (-> S4 S4 S1)
boehmes@36900
   730
#3197 := (f179 f287 f287)
boehmes@36900
   731
#12424 := (= f1 #3197)
boehmes@36900
   732
#13883 := (not #12424)
boehmes@36900
   733
decl f203 :: (-> S2 S4 S1)
boehmes@36900
   734
#3122 := (f203 f273 f287)
boehmes@36900
   735
#12167 := (= f1 #3122)
boehmes@36900
   736
#15198 := (not #12167)
boehmes@36900
   737
#3117 := (f67 #3007 f298 f9)
boehmes@36900
   738
#3118 := (f111 f287 #3117)
boehmes@36900
   739
#12159 := (= f297 #3118)
boehmes@36900
   740
#22499 := (not #12159)
boehmes@36900
   741
#3063 := (f67 #3007 0::int f9)
boehmes@36900
   742
#3073 := (f111 f287 #3063)
boehmes@36900
   743
decl f296 :: int
boehmes@36900
   744
#3072 := f296
boehmes@36900
   745
#3074 := (= f296 #3073)
boehmes@36900
   746
#13176 := (not #3074)
boehmes@36900
   747
#23375 := (or #13176 #22499 #15198 #13883 #12969 #12960 #12951 #12942 #22500 #22501 #13417 #22363 #13565 #13888 #13940 #22502 #22503 #22505 #22506 #22507 #23216 #23372)
boehmes@36900
   748
#23378 := (not #23375)
boehmes@36900
   749
#23381 := (or #13176 #13417 #23378)
boehmes@36900
   750
#23384 := (not #23381)
boehmes@36900
   751
#13397 := (* -1::int #3089)
boehmes@36900
   752
#13398 := (+ f296 #13397)
boehmes@36900
   753
#13396 := (>= #13398 0::int)
boehmes@36900
   754
#13384 := (>= #168 1::int)
boehmes@36900
   755
#22227 := (or #5040 #13384 #13396 #19497)
boehmes@36900
   756
#23203 := (forall (vars (?v0 int)) (:pat #23202) #22227)
boehmes@36900
   757
#23208 := (not #23203)
boehmes@36900
   758
#23387 := (or #23208 #23384)
boehmes@36900
   759
#23390 := (not #23387)
boehmes@36900
   760
decl ?v0!13 :: int
boehmes@36900
   761
#18361 := ?v0!13
boehmes@36900
   762
#18371 := (>= ?v0!13 1::int)
boehmes@36900
   763
#18366 := (f67 #3007 ?v0!13 f9)
boehmes@36900
   764
#18367 := (f111 f287 #18366)
boehmes@36900
   765
#18368 := (* -1::int #18367)
boehmes@36900
   766
#18369 := (+ f296 #18368)
boehmes@36900
   767
#18370 := (>= #18369 0::int)
boehmes@36900
   768
#18363 := (>= ?v0!13 0::int)
boehmes@36900
   769
#22201 := (not #18363)
boehmes@36900
   770
#18362 := (<= ?v0!13 4294967295::int)
boehmes@36900
   771
#22200 := (not #18362)
boehmes@36900
   772
#22216 := (or #22200 #22201 #18370 #18371)
boehmes@36900
   773
#22221 := (not #22216)
boehmes@36900
   774
#23393 := (or #22221 #23390)
boehmes@36900
   775
#23396 := (not #23393)
boehmes@36900
   776
#13378 := (>= f286 1::int)
boehmes@36900
   777
#13381 := (not #13378)
boehmes@36900
   778
#23399 := (or #13381 #23396)
boehmes@36900
   779
#23402 := (not #23399)
boehmes@36900
   780
#23405 := (or #13381 #23402)
boehmes@36900
   781
#23408 := (not #23405)
boehmes@36900
   782
decl f275 :: S2
boehmes@36900
   783
#2978 := f275
boehmes@36900
   784
#3079 := (f291 f287 f275 f274 1::int f6)
boehmes@36900
   785
#12110 := (= f1 #3079)
boehmes@36900
   786
#13149 := (not #12110)
boehmes@36900
   787
decl f277 :: S2
boehmes@36900
   788
#2980 := f277
boehmes@36900
   789
#3077 := (f291 f287 f277 f276 0::int f6)
boehmes@36900
   790
#12107 := (= f1 #3077)
boehmes@36900
   791
#13158 := (not #12107)
boehmes@36900
   792
decl f279 :: S2
boehmes@36900
   793
#2982 := f279
boehmes@36900
   794
#3075 := (f291 f287 f279 f278 f296 f9)
boehmes@36900
   795
#12104 := (= f1 #3075)
boehmes@36900
   796
#13167 := (not #12104)
boehmes@36900
   797
#3069 := (f69 f287 #3063)
boehmes@36900
   798
#12098 := (= f1 #3069)
boehmes@36900
   799
#18338 := (not #12098)
boehmes@36900
   800
#3064 := (f49 #3063 f9)
boehmes@36900
   801
#12089 := (= f1 #3064)
boehmes@36900
   802
#18329 := (not #12089)
boehmes@36900
   803
#23411 := (or #13176 #18329 #18338 #13167 #13158 #13149 #23408)
boehmes@36900
   804
#23414 := (not #23411)
boehmes@36900
   805
#23417 := (or #18329 #18338 #23414)
boehmes@36900
   806
#23420 := (not #23417)
boehmes@36900
   807
#3066 := (f25 f287 #3063)
boehmes@36900
   808
#12092 := (= f1 #3066)
boehmes@36900
   809
#18332 := (not #12092)
boehmes@36900
   810
#23423 := (or #18329 #18332 #23420)
boehmes@36900
   811
#23426 := (not #23423)
boehmes@36900
   812
#23429 := (or #18329 #18332 #23426)
boehmes@36900
   813
#23432 := (not #23429)
boehmes@36900
   814
decl f201 :: (-> S4 S5 S5 S16 S1)
boehmes@36900
   815
decl f295 :: S16
boehmes@36900
   816
#3060 := f295
boehmes@36900
   817
#3061 := (f201 f287 #3009 #3009 f295)
boehmes@36900
   818
#12086 := (= f1 #3061)
boehmes@36900
   819
#13209 := (not #12086)
boehmes@36900
   820
#23435 := (or #13209 #23432)
boehmes@36900
   821
#23438 := (not #23435)
boehmes@36900
   822
#24719 := (f117 #3009)
boehmes@36900
   823
#26021 := (f44 #3005 #24719)
boehmes@36900
   824
#26555 := (f201 f287 #26021 #26021 f295)
boehmes@36900
   825
#26805 := (= #26555 #3061)
boehmes@36900
   826
#26808 := (= #3061 #26555)
boehmes@36900
   827
#26028 := (= #3009 #26021)
boehmes@36900
   828
#3014 := (f49 #3009 #3005)
boehmes@36900
   829
#12018 := (= f1 #3014)
boehmes@36900
   830
decl f24 :: (-> S3 S1)
boehmes@36900
   831
#3021 := (f24 #3005)
boehmes@36900
   832
#12030 := (= f1 #3021)
boehmes@36900
   833
#3018 := (f13 #3005)
boehmes@36900
   834
#12024 := (= f15 #3018)
boehmes@36900
   835
#12027 := (not #12024)
boehmes@36900
   836
#3016 := (f25 f287 #3009)
boehmes@36900
   837
#12021 := (= f1 #3016)
boehmes@36900
   838
#12015 := (= f27 #3012)
boehmes@36900
   839
#3010 := (f28 f287 #3009)
boehmes@36900
   840
#12011 := (= f1 #3010)
boehmes@36900
   841
#14137 := (and #12011 #12015 #12018 #12021 #12027 #12030)
boehmes@36900
   842
decl f283 :: int
boehmes@36900
   843
#2989 := f283
boehmes@36900
   844
#14193 := (* -1::int f283)
boehmes@36900
   845
decl f79 :: int
boehmes@36900
   846
#438 := f79
boehmes@36900
   847
#14194 := (+ f79 #14193)
boehmes@36900
   848
#14192 := (>= #14194 0::int)
boehmes@36900
   849
#14190 := (>= f283 0::int)
boehmes@36900
   850
#14197 := (and #14190 #14192)
boehmes@36900
   851
#14200 := (not #14197)
boehmes@36900
   852
decl f284 :: int
boehmes@36900
   853
#2993 := f284
boehmes@36900
   854
#14179 := (* -1::int f284)
boehmes@36900
   855
decl f77 :: int
boehmes@36900
   856
#418 := f77
boehmes@36900
   857
#14180 := (+ f77 #14179)
boehmes@36900
   858
#14178 := (>= #14180 0::int)
boehmes@36900
   859
#14176 := (>= f284 0::int)
boehmes@36900
   860
#14183 := (and #14176 #14178)
boehmes@36900
   861
#14186 := (not #14183)
boehmes@36900
   862
decl f285 :: int
boehmes@36900
   863
#2997 := f285
boehmes@36900
   864
#14165 := (* -1::int f285)
boehmes@36900
   865
#14166 := (+ f77 #14165)
boehmes@36900
   866
#14164 := (>= #14166 0::int)
boehmes@36900
   867
#14162 := (>= f285 0::int)
boehmes@36900
   868
#14169 := (and #14162 #14164)
boehmes@36900
   869
#14172 := (not #14169)
boehmes@36900
   870
#1051 := 1099511627776::int
boehmes@36900
   871
#14150 := (>= f286 1099511627776::int)
boehmes@36900
   872
#14140 := (not #14137)
boehmes@36900
   873
decl f289 :: (-> S19 int)
boehmes@36900
   874
#3035 := (:var 0 S19)
boehmes@36900
   875
#3036 := (f289 #3035)
boehmes@36900
   876
#3037 := (pattern #3036)
boehmes@36900
   877
decl f290 :: int
boehmes@36900
   878
#3038 := f290
boehmes@36900
   879
#14127 := (* -1::int f290)
boehmes@36900
   880
#14128 := (+ #3036 #14127)
boehmes@36900
   881
#14126 := (>= #14128 0::int)
boehmes@36900
   882
#14125 := (not #14126)
boehmes@36900
   883
#14131 := (forall (vars (?v0 S19)) (:pat #3037) #14125)
boehmes@36900
   884
#14134 := (not #14131)
boehmes@36900
   885
#13418 := (not #13417)
boehmes@36900
   886
#13981 := (and #3074 #13418)
boehmes@36900
   887
#13986 := (not #13981)
boehmes@36900
   888
#13969 := (+ f79 #13915)
boehmes@36900
   889
#13968 := (>= #13969 0::int)
boehmes@36900
   890
#13972 := (and #13965 #13968)
boehmes@36900
   891
#13975 := (not #13972)
boehmes@36900
   892
#13956 := (+ f77 #13886)
boehmes@36900
   893
#13955 := (>= #13956 0::int)
boehmes@36900
   894
#13959 := (and #13422 #13955)
boehmes@36900
   895
#13962 := (not #13959)
boehmes@36900
   896
#13447 := (+ f77 #13446)
boehmes@36900
   897
#13946 := (>= #13447 0::int)
boehmes@36900
   898
#13949 := (and #13943 #13946)
boehmes@36900
   899
#13952 := (not #13949)
boehmes@36900
   900
#4430 := (* -1::int f77)
boehmes@36900
   901
#4431 := (+ #168 #4430)
boehmes@36900
   902
#4432 := (<= #4431 0::int)
boehmes@36900
   903
#4439 := (and #4118 #4432)
boehmes@36900
   904
#5654 := (not #4439)
boehmes@36900
   905
#13926 := (or #5654 #13903 #13917)
boehmes@36900
   906
#13931 := (forall (vars (?v0 int)) #13926)
boehmes@34994
   907
#13934 := (not #13931)
boehmes@36900
   908
#13889 := (not #13888)
boehmes@36900
   909
#13895 := (and #12159 #13889)
boehmes@36900
   910
#13900 := (not #13895)
boehmes@36900
   911
#13740 := (not #13738)
boehmes@36900
   912
#13778 := (and #3138 #4118 #4432 #13740)
boehmes@36900
   913
#13783 := (exists (vars (?v0 int)) #13778)
boehmes@36900
   914
#13761 := (or #5654 #13738 #13752)
boehmes@36900
   915
#13766 := (forall (vars (?v0 int)) #13761)
boehmes@36900
   916
#13786 := (not #13766)
boehmes@36900
   917
#13792 := (or #13786 #13783)
boehmes@36900
   918
#13797 := (and #13766 #13792)
boehmes@36900
   919
#13427 := (and #13422 #13425)
boehmes@36900
   920
#13430 := (not #13427)
boehmes@36900
   921
decl f217 :: S1
boehmes@36900
   922
#2506 := f217
boehmes@36900
   923
#10869 := (= f1 f217)
boehmes@36900
   924
#12283 := (not #10869)
boehmes@36900
   925
#13824 := (or #12283 #12249 #12240 #12231 #12222 #13430 #13797)
boehmes@36900
   926
#13829 := (and #10869 #13824)
boehmes@36900
   927
#13854 := (or #13430 #13711 #13829)
boehmes@36900
   928
#13445 := (>= #13447 1::int)
boehmes@36900
   929
#13534 := (and #13443 #13445)
boehmes@36900
   930
#13537 := (not #13534)
boehmes@36900
   931
#13504 := (not #13503)
boehmes@36900
   932
#13510 := (and #12552 #13504)
boehmes@36900
   933
#13490 := (or #5654 #13467 #13481)
boehmes@36900
   934
#13495 := (forall (vars (?v0 int)) #13490)
boehmes@36900
   935
#13498 := (not #13495)
boehmes@36900
   936
#13515 := (or #13498 #13510)
boehmes@36900
   937
#13518 := (and #13495 #13515)
boehmes@36900
   938
#13521 := (or #13464 #13518)
boehmes@36900
   939
#13524 := (and #13459 #13521)
boehmes@36900
   940
#13453 := (and #13434 #13451)
boehmes@36900
   941
#13456 := (not #13453)
boehmes@36900
   942
#13552 := (or #12601 #13456 #13524 #13531 #13537)
boehmes@36900
   943
#13560 := (and #13443 #13445 #13552)
boehmes@36900
   944
#13436 := (and #13425 #13434)
boehmes@36900
   945
#13439 := (not #13436)
boehmes@36900
   946
#13671 := (or #12766 #12757 #13430 #13439 #13560 #13616)
boehmes@36900
   947
#12496 := (and #12484 #12493)
boehmes@36900
   948
#12694 := (not #12496)
boehmes@36900
   949
#13592 := (or #12694 #12685 #12676 #12667 #12649 #12640 #13565 #13439 #13560)
boehmes@36900
   950
#13600 := (and #12484 #12493 #13592)
boehmes@36900
   951
#12490 := (and #12484 #12487)
boehmes@36900
   952
#12706 := (not #12490)
boehmes@36900
   953
#13605 := (or #12706 #13600)
boehmes@36900
   954
#13611 := (and #12484 #12487 #13605)
boehmes@36900
   955
#13641 := (or #13430 #13611 #13617)
boehmes@36900
   956
#13676 := (and #13641 #13671)
boehmes@36900
   957
#13685 := (or #12694 #13430 #13676)
boehmes@36900
   958
#13693 := (and #12484 #12493 #13685)
boehmes@36900
   959
#13698 := (or #12706 #13693)
boehmes@36900
   960
#13704 := (and #12484 #12487 #13698)
boehmes@36900
   961
#13733 := (or #13430 #13704 #13710)
boehmes@36900
   962
#13859 := (and #13733 #13854)
boehmes@36900
   963
#12470 := (and #12464 #12467)
boehmes@36900
   964
#12933 := (not #12470)
boehmes@36900
   965
decl f56 :: (-> S4 S1)
boehmes@36900
   966
#3032 := (f56 f287)
boehmes@36900
   967
#12054 := (= f1 #3032)
boehmes@36900
   968
#12173 := (and #12054 #12167)
boehmes@36900
   969
#12311 := (not #12173)
boehmes@36900
   970
#14052 := (or #12311 #13883 #12969 #12960 #12951 #12942 #12933 #13430 #13859 #13900 #13934 #13940 #13952 #13962 #13975 #13986)
boehmes@36900
   971
#14060 := (and #3074 #13418 #14052)
boehmes@36900
   972
#13406 := (or #5654 #13384 #13396)
boehmes@36900
   973
#13411 := (forall (vars (?v0 int)) #13406)
boehmes@36900
   974
#13414 := (not #13411)
boehmes@36900
   975
#14065 := (or #13414 #14060)
boehmes@36900
   976
#14068 := (and #13411 #14065)
boehmes@36900
   977
#14071 := (or #13381 #14068)
boehmes@36900
   978
#14074 := (and #13378 #14071)
boehmes@36900
   979
#12101 := (and #12089 #12098)
boehmes@36900
   980
#13185 := (not #12101)
boehmes@36900
   981
#14095 := (or #13176 #13185 #13167 #13158 #13149 #14074)
boehmes@36900
   982
#14103 := (and #12089 #12098 #14095)
boehmes@36900
   983
#12095 := (and #12089 #12092)
boehmes@36900
   984
#13197 := (not #12095)
boehmes@36900
   985
#14108 := (or #13197 #14103)
boehmes@36900
   986
#14114 := (and #12089 #12092 #14108)
boehmes@36900
   987
#14119 := (or #13209 #14114)
boehmes@36900
   988
#14122 := (and #12086 #14119)
boehmes@36900
   989
#13352 := (+ f77 #13351)
boehmes@36900
   990
#13350 := (>= #13352 0::int)
boehmes@36900
   991
#13348 := (>= f286 0::int)
boehmes@36900
   992
#13355 := (and #13348 #13350)
boehmes@36900
   993
#13358 := (not #13355)
boehmes@36900
   994
decl f294 :: (-> int S5 S1)
boehmes@36900
   995
decl f293 :: int
boehmes@36900
   996
#3049 := f293
boehmes@36900
   997
#3052 := (f294 f293 #28)
boehmes@36900
   998
#3053 := (pattern #3052)
boehmes@36900
   999
#12072 := (= f1 #3052)
boehmes@36900
  1000
#12078 := (not #12072)
boehmes@36900
  1001
#12083 := (forall (vars (?v0 S5)) (:pat #3053) #12078)
boehmes@36900
  1002
#13230 := (not #12083)
boehmes@36900
  1003
decl f282 :: S2
boehmes@36900
  1004
#2985 := f282
boehmes@36900
  1005
#3047 := (f291 f287 f282 f280 f286 f6)
boehmes@36900
  1006
#12069 := (= f1 #3047)
boehmes@36900
  1007
#13248 := (not #12069)
boehmes@36900
  1008
#3044 := (f292 f287 f282 f281 #3007 #17)
boehmes@36900
  1009
#12063 := (= f1 #3044)
boehmes@36900
  1010
#3042 := (f291 f287 f282 f281 #3041 #17)
boehmes@36900
  1011
#12060 := (= f1 #3042)
boehmes@36900
  1012
#12066 := (and #12060 #12063)
boehmes@36900
  1013
#13257 := (not #12066)
boehmes@36900
  1014
#3030 := (f203 f282 f287)
boehmes@36900
  1015
#12051 := (= f1 #3030)
boehmes@36900
  1016
#12057 := (and #12051 #12054)
boehmes@36900
  1017
#13275 := (not #12057)
boehmes@36900
  1018
decl f204 :: (-> S4 S1)
boehmes@36900
  1019
#3028 := (f204 f287)
boehmes@36900
  1020
#12048 := (= f1 #3028)
boehmes@36900
  1021
#13284 := (not #12048)
boehmes@36900
  1022
decl f174 :: (-> S4 int)
boehmes@36900
  1023
#3050 := (f174 f287)
boehmes@36900
  1024
#3051 := (= f293 #3050)
boehmes@36900
  1025
#13239 := (not #3051)
boehmes@36900
  1026
#14245 := (or #13239 #13284 #13275 #13257 #13248 #13230 #13358 #13417 #14122 #14134 #14140 #14150 #14172 #14186 #14200)
boehmes@36900
  1027
#14250 := (not #14245)
boehmes@34994
  1028
#1 := true
boehmes@36900
  1029
#3133 := (< #168 f286)
boehmes@36900
  1030
#3139 := (and #3133 #3138)
boehmes@36900
  1031
#420 := (<= #168 f77)
boehmes@36900
  1032
#3140 := (and #420 #3139)
boehmes@36900
  1033
#293 := (<= 0::int #168)
boehmes@36900
  1034
#3141 := (and #293 #3140)
boehmes@36900
  1035
#3142 := (exists (vars (?v0 int)) #3141)
boehmes@36900
  1036
#3143 := (and #3142 true)
boehmes@36900
  1037
#3134 := (<= #3089 f303)
boehmes@36900
  1038
#3135 := (implies #3133 #3134)
boehmes@36900
  1039
#421 := (and #293 #420)
boehmes@36900
  1040
#3136 := (implies #421 #3135)
boehmes@36900
  1041
#3137 := (forall (vars (?v0 int)) #3136)
boehmes@36900
  1042
#3144 := (implies #3137 #3143)
boehmes@36900
  1043
#3145 := (and #3137 #3144)
boehmes@36900
  1044
#3132 := (= f303 f297)
boehmes@36900
  1045
#3146 := (implies #3132 #3145)
boehmes@36900
  1046
#3130 := (= f302 f298)
boehmes@36900
  1047
#3147 := (implies #3130 #3146)
boehmes@36900
  1048
#3128 := (= f301 f299)
boehmes@36900
  1049
#3148 := (implies #3128 #3147)
boehmes@36900
  1050
#3126 := (= f300 f297)
boehmes@36900
  1051
#3149 := (implies #3126 #3148)
boehmes@36900
  1052
#3101 := (<= 0::int f298)
boehmes@36900
  1053
#3108 := (<= 1::int f299)
boehmes@36900
  1054
#3109 := (and #3108 #3101)
boehmes@36900
  1055
#3150 := (implies #3109 #3149)
boehmes@36900
  1056
#3151 := (implies #3109 #3150)
boehmes@36900
  1057
#3152 := (implies #3109 #3151)
boehmes@36900
  1058
#2507 := (= f217 f1)
boehmes@36900
  1059
#3153 := (implies #2507 #3152)
boehmes@36900
  1060
#3154 := (and #2507 #3153)
boehmes@36900
  1061
#3155 := (implies #3109 #3154)
boehmes@36900
  1062
#3156 := (implies #3109 #3155)
boehmes@36900
  1063
#3313 := (implies #3109 #3156)
boehmes@36900
  1064
#3314 := (implies #3109 #3313)
boehmes@36900
  1065
#3312 := (<= f286 f299)
boehmes@36900
  1066
#3315 := (implies #3312 #3314)
boehmes@36900
  1067
#3316 := (implies #3109 #3315)
boehmes@36900
  1068
#3265 := (= #3264 f305)
boehmes@36900
  1069
#3262 := (< f306 f286)
boehmes@36900
  1070
#3266 := (and #3262 #3265)
boehmes@36900
  1071
#3267 := (and #3266 true)
boehmes@36900
  1072
#3258 := (<= #3089 f305)
boehmes@36900
  1073
#3257 := (< #168 f307)
boehmes@36900
  1074
#3259 := (implies #3257 #3258)
boehmes@36900
  1075
#3260 := (implies #421 #3259)
boehmes@36900
  1076
#3261 := (forall (vars (?v0 int)) #3260)
boehmes@36900
  1077
#3268 := (implies #3261 #3267)
boehmes@36900
  1078
#3269 := (and #3261 #3268)
boehmes@36900
  1079
#3256 := (<= f307 f286)
boehmes@36900
  1080
#3270 := (implies #3256 #3269)
boehmes@36900
  1081
#3271 := (and #3256 #3270)
boehmes@36900
  1082
#3244 := (<= 0::int f306)
boehmes@36900
  1083
#3254 := (<= 2::int f307)
boehmes@36900
  1084
#3255 := (and #3254 #3244)
boehmes@36900
  1085
#3272 := (implies #3255 #3271)
boehmes@36900
  1086
#3253 := (= #3252 f1)
boehmes@36900
  1087
#3273 := (implies #3253 #3272)
boehmes@36900
  1088
#3246 := (+ f299 1::int)
boehmes@36900
  1089
#3251 := (= f307 #3246)
boehmes@36900
  1090
#3274 := (implies #3251 #3273)
boehmes@36900
  1091
#3248 := (<= #3246 f77)
boehmes@36900
  1092
#3247 := (<= 0::int #3246)
boehmes@36900
  1093
#3249 := (and #3247 #3248)
boehmes@36900
  1094
#3275 := (implies #3249 #3274)
boehmes@36900
  1095
#3276 := (and #3249 #3275)
boehmes@36900
  1096
#3245 := (and #3108 #3244)
boehmes@36900
  1097
#3277 := (implies #3245 #3276)
boehmes@36900
  1098
#3294 := (= f306 f298)
boehmes@36900
  1099
#3295 := (implies #3294 #3277)
boehmes@36900
  1100
#3293 := (= f305 f297)
boehmes@36900
  1101
#3296 := (implies #3293 #3295)
boehmes@36900
  1102
#3297 := (implies #3109 #3296)
boehmes@36900
  1103
#3298 := (implies #3109 #3297)
boehmes@36900
  1104
#3299 := (implies #3109 #3298)
boehmes@36900
  1105
#3292 := (<= #3231 f297)
boehmes@36900
  1106
#3300 := (implies #3292 #3299)
boehmes@36900
  1107
#3301 := (implies #3109 #3300)
boehmes@36900
  1108
#3243 := (= f306 f299)
boehmes@36900
  1109
#3278 := (implies #3243 #3277)
boehmes@36900
  1110
#3241 := (= f305 f304)
boehmes@36900
  1111
#3279 := (implies #3241 #3278)
boehmes@36900
  1112
#3239 := (and #3108 #3108)
boehmes@36900
  1113
#3280 := (implies #3239 #3279)
boehmes@36900
  1114
#3238 := (= #3237 f1)
boehmes@36900
  1115
#3281 := (implies #3238 #3280)
boehmes@36900
  1116
#3236 := (= #3235 f1)
boehmes@36900
  1117
#3282 := (implies #3236 #3281)
boehmes@36900
  1118
#3234 := (= f304 #3231)
boehmes@36900
  1119
#3283 := (implies #3234 #3282)
boehmes@36900
  1120
#3229 := (= #3228 f1)
boehmes@36900
  1121
#3224 := (= #3223 f1)
boehmes@36900
  1122
#3230 := (and #3224 #3229)
boehmes@36900
  1123
#3284 := (implies #3230 #3283)
boehmes@36900
  1124
#3285 := (and #3230 #3284)
boehmes@36900
  1125
#3226 := (= #3225 f1)
boehmes@36900
  1126
#3227 := (and #3224 #3226)
boehmes@36900
  1127
#3286 := (implies #3227 #3285)
boehmes@36900
  1128
#3287 := (and #3227 #3286)
boehmes@36900
  1129
#3288 := (implies #3109 #3287)
boehmes@36900
  1130
#3289 := (implies #3109 #3288)
boehmes@36900
  1131
#3232 := (< f297 #3231)
boehmes@36900
  1132
#3290 := (implies #3232 #3289)
boehmes@36900
  1133
#3291 := (implies #3109 #3290)
boehmes@36900
  1134
#3302 := (and #3291 #3301)
boehmes@36900
  1135
#3303 := (implies #3109 #3302)
boehmes@36900
  1136
#3304 := (implies #3230 #3303)
boehmes@36900
  1137
#3305 := (and #3230 #3304)
boehmes@36900
  1138
#3306 := (implies #3227 #3305)
boehmes@36900
  1139
#3307 := (and #3227 #3306)
boehmes@36900
  1140
#3308 := (implies #3109 #3307)
boehmes@36900
  1141
#3309 := (implies #3109 #3308)
boehmes@36900
  1142
#3221 := (< f299 f286)
boehmes@36900
  1143
#3310 := (implies #3221 #3309)
boehmes@36900
  1144
#3311 := (implies #3109 #3310)
boehmes@36900
  1145
#3317 := (and #3311 #3316)
boehmes@36900
  1146
#3318 := (implies #3109 #3317)
boehmes@36900
  1147
decl f42 :: (-> S4 S12)
boehmes@36900
  1148
#3162 := (f42 f287)
boehmes@36900
  1149
#3219 := (= #3162 #3162)
boehmes@36900
  1150
#3218 := (= #3185 #3185)
boehmes@36900
  1151
#3220 := (and #3218 #3219)
boehmes@36900
  1152
#3319 := (implies #3220 #3318)
boehmes@36900
  1153
#3216 := (= #3215 f1)
boehmes@36900
  1154
#3214 := (= #3213 f1)
boehmes@36900
  1155
#3217 := (and #3214 #3216)
boehmes@36900
  1156
#3320 := (implies #3217 #3319)
boehmes@36900
  1157
#3212 := (= #3211 f1)
boehmes@36900
  1158
#3321 := (implies #3212 #3320)
boehmes@36900
  1159
#3210 := (= #3209 f1)
boehmes@36900
  1160
#3322 := (implies #3210 #3321)
boehmes@36900
  1161
#3208 := (= #3207 f1)
boehmes@36900
  1162
#3323 := (implies #3208 #3322)
boehmes@36900
  1163
#3206 := (= #3205 f1)
boehmes@36900
  1164
#3324 := (implies #3206 #3323)
boehmes@36900
  1165
#3033 := (= #3032 f1)
boehmes@36900
  1166
#3123 := (= #3122 f1)
boehmes@36900
  1167
#3124 := (and #3123 #3033)
boehmes@36900
  1168
#3325 := (implies #3124 #3324)
boehmes@36900
  1169
#3198 := (= #3197 f1)
boehmes@36900
  1170
decl f173 :: (-> S4 S5 int)
boehmes@36900
  1171
#3193 := (f173 f287 #28)
boehmes@36900
  1172
#3194 := (pattern #3193)
boehmes@36900
  1173
#3195 := (<= #3193 #3193)
boehmes@36900
  1174
#3196 := (forall (vars (?v0 S5)) (:pat #3194) #3195)
boehmes@36900
  1175
#3199 := (and #3196 #3198)
boehmes@36900
  1176
#3192 := (<= #3050 #3050)
boehmes@36900
  1177
#3200 := (and #3192 #3199)
boehmes@36900
  1178
#3326 := (implies #3200 #3325)
boehmes@36900
  1179
#3186 := (f59 #3185 #28)
boehmes@36900
  1180
#3187 := (pattern #3186)
boehmes@36900
  1181
#3175 := (f69 f287 #28)
boehmes@36900
  1182
#3176 := (= #3175 f1)
boehmes@36900
  1183
#3188 := (= #3186 #3186)
boehmes@36900
  1184
#3189 := (and #3188 #3176)
boehmes@36900
  1185
#3190 := (implies #3176 #3189)
boehmes@36900
  1186
#3191 := (forall (vars (?v0 S5)) (:pat #3187) #3190)
boehmes@36900
  1187
#3201 := (and #3191 #3200)
boehmes@36900
  1188
decl f41 :: (-> S12 S5 S11)
boehmes@36900
  1189
#3163 := (f41 #3162 #28)
boehmes@36900
  1190
#3164 := (pattern #3163)
boehmes@36900
  1191
#3181 := (= #3163 #3163)
boehmes@36900
  1192
#3182 := (and #3181 #3176)
boehmes@36900
  1193
#3183 := (implies #3176 #3182)
boehmes@36900
  1194
#3184 := (forall (vars (?v0 S5)) (:pat #3164) #3183)
boehmes@36900
  1195
#3202 := (and #3184 #3201)
boehmes@36900
  1196
decl f20 :: (-> S9 S5 int)
boehmes@36900
  1197
decl f21 :: (-> S4 S9)
boehmes@36900
  1198
#3172 := (f21 f287)
boehmes@36900
  1199
#3173 := (f20 #3172 #28)
boehmes@36900
  1200
#3174 := (pattern #3173)
boehmes@36900
  1201
#3177 := (= #3173 #3173)
boehmes@36900
  1202
#3178 := (and #3177 #3176)
boehmes@36900
  1203
#3179 := (implies #3176 #3178)
boehmes@36900
  1204
#3180 := (forall (vars (?v0 S5)) (:pat #3174) #3179)
boehmes@36900
  1205
#3203 := (and #3180 #3202)
boehmes@36900
  1206
decl f262 :: S8
boehmes@36900
  1207
#2868 := f262
boehmes@36900
  1208
#3165 := (f26 f287 #28)
boehmes@36900
  1209
#3166 := (f14 #3165)
boehmes@36900
  1210
#3167 := (f13 #3166)
boehmes@36900
  1211
#3168 := (= #3167 f262)
boehmes@36900
  1212
#3169 := (not #3168)
boehmes@36900
  1213
#3170 := (implies #3169 #3169)
boehmes@36900
  1214
#3171 := (forall (vars (?v0 S5)) (:pat #3164) #3170)
boehmes@36900
  1215
#3204 := (and #3171 #3203)
boehmes@36900
  1216
#3327 := (implies #3204 #3326)
boehmes@36900
  1217
#3328 := (implies #3109 #3327)
boehmes@36900
  1218
#3329 := (implies #3109 #3328)
boehmes@36900
  1219
#3330 := (implies #3109 #3329)
boehmes@36900
  1220
#3157 := (implies #3124 #3156)
boehmes@36900
  1221
#3158 := (implies #3109 #3157)
boehmes@36900
  1222
#3159 := (implies #3109 #3158)
boehmes@36900
  1223
#3121 := (not true)
boehmes@36900
  1224
#3160 := (implies #3121 #3159)
boehmes@36900
  1225
#3161 := (implies #3109 #3160)
boehmes@36900
  1226
#3331 := (and #3161 #3330)
boehmes@36900
  1227
#3332 := (implies #3109 #3331)
boehmes@36900
  1228
#3119 := (= #3118 f297)
boehmes@36900
  1229
#3116 := (< f298 f286)
boehmes@36900
  1230
#3120 := (and #3116 #3119)
boehmes@36900
  1231
#3333 := (implies #3120 #3332)
boehmes@36900
  1232
#3112 := (<= #3089 f297)
boehmes@36900
  1233
#3111 := (< #168 f299)
boehmes@36900
  1234
#3113 := (implies #3111 #3112)
boehmes@36900
  1235
#3114 := (implies #421 #3113)
boehmes@36900
  1236
#3115 := (forall (vars (?v0 int)) #3114)
boehmes@36900
  1237
#3334 := (implies #3115 #3333)
boehmes@36900
  1238
#3110 := (<= f299 f286)
boehmes@36900
  1239
#3335 := (implies #3110 #3334)
boehmes@36900
  1240
#3336 := (implies #3109 #3335)
boehmes@36900
  1241
#3106 := (<= f299 f77)
boehmes@36900
  1242
#3105 := (<= 0::int f299)
boehmes@36900
  1243
#3107 := (and #3105 #3106)
boehmes@36900
  1244
#3337 := (implies #3107 #3336)
boehmes@36900
  1245
#3102 := (<= f298 f77)
boehmes@36900
  1246
#3103 := (and #3101 #3102)
boehmes@36900
  1247
#3338 := (implies #3103 #3337)
boehmes@36900
  1248
#3098 := (<= f297 f79)
boehmes@36900
  1249
#3097 := (<= 0::int f297)
boehmes@36900
  1250
#3099 := (and #3097 #3098)
boehmes@36900
  1251
#3339 := (implies #3099 #3338)
boehmes@36900
  1252
#3094 := (= #3073 f296)
boehmes@36900
  1253
#3003 := (< 0::int f286)
boehmes@36900
  1254
#3095 := (and #3003 #3094)
boehmes@36900
  1255
#3340 := (implies #3095 #3339)
boehmes@36900
  1256
#3341 := (and #3095 #3340)
boehmes@36900
  1257
#3090 := (<= #3089 f296)
boehmes@36900
  1258
#3087 := (< #168 1::int)
boehmes@36900
  1259
#3091 := (implies #3087 #3090)
boehmes@36900
  1260
#3092 := (implies #421 #3091)
boehmes@36900
  1261
#3093 := (forall (vars (?v0 int)) #3092)
boehmes@36900
  1262
#3342 := (implies #3093 #3341)
boehmes@36900
  1263
#3343 := (and #3093 #3342)
boehmes@36900
  1264
#3086 := (<= 1::int f286)
boehmes@36900
  1265
#3344 := (implies #3086 #3343)
boehmes@36900
  1266
#3345 := (and #3086 #3344)
boehmes@36900
  1267
#3082 := (<= 0::int 0::int)
boehmes@36900
  1268
#3083 := (and #3082 #3082)
boehmes@36900
  1269
#3081 := (<= 1::int 1::int)
boehmes@36900
  1270
#3084 := (and #3081 #3083)
boehmes@34994
  1271
#3085 := (and #3081 #3084)
boehmes@36900
  1272
#3346 := (implies #3085 #3345)
boehmes@36900
  1273
#3080 := (= #3079 f1)
boehmes@36900
  1274
#3347 := (implies #3080 #3346)
boehmes@36900
  1275
#3078 := (= #3077 f1)
boehmes@36900
  1276
#3348 := (implies #3078 #3347)
boehmes@36900
  1277
#3076 := (= #3075 f1)
boehmes@36900
  1278
#3349 := (implies #3076 #3348)
boehmes@36900
  1279
#3350 := (implies #3074 #3349)
boehmes@36900
  1280
#3070 := (= #3069 f1)
boehmes@36900
  1281
#3065 := (= #3064 f1)
boehmes@36900
  1282
#3071 := (and #3065 #3070)
boehmes@36900
  1283
#3351 := (implies #3071 #3350)
boehmes@36900
  1284
#3352 := (and #3071 #3351)
boehmes@36900
  1285
#3067 := (= #3066 f1)
boehmes@36900
  1286
#3068 := (and #3065 #3067)
boehmes@36900
  1287
#3353 := (implies #3068 #3352)
boehmes@36900
  1288
#3354 := (and #3068 #3353)
boehmes@36900
  1289
#3062 := (= #3061 f1)
boehmes@36900
  1290
#3355 := (implies #3062 #3354)
boehmes@36900
  1291
#3356 := (and #3062 #3355)
boehmes@36900
  1292
#3058 := (<= f286 f77)
boehmes@36900
  1293
#3057 := (<= 0::int f286)
boehmes@36900
  1294
#3059 := (and #3057 #3058)
boehmes@36900
  1295
#3357 := (implies #3059 #3356)
boehmes@36900
  1296
#3054 := (= #3052 f1)
boehmes@36900
  1297
#3055 := (iff #3054 false)
boehmes@36900
  1298
#3056 := (forall (vars (?v0 S5)) (:pat #3053) #3055)
boehmes@36900
  1299
#3358 := (implies #3056 #3357)
boehmes@36900
  1300
#3359 := (implies #3051 #3358)
boehmes@36900
  1301
#3048 := (= #3047 f1)
boehmes@36900
  1302
#3360 := (implies #3048 #3359)
boehmes@36900
  1303
#3045 := (= #3044 f1)
boehmes@36900
  1304
#3043 := (= #3042 f1)
boehmes@36900
  1305
#3046 := (and #3043 #3045)
boehmes@36900
  1306
#3361 := (implies #3046 #3360)
boehmes@36900
  1307
#3039 := (< #3036 f290)
boehmes@36900
  1308
#3040 := (forall (vars (?v0 S19)) (:pat #3037) #3039)
boehmes@36900
  1309
#3362 := (implies #3040 #3361)
boehmes@36900
  1310
#3031 := (= #3030 f1)
boehmes@36900
  1311
#3034 := (and #3031 #3033)
boehmes@36900
  1312
#3363 := (implies #3034 #3362)
boehmes@36900
  1313
#3029 := (= #3028 f1)
boehmes@36900
  1314
#3364 := (implies #3029 #3363)
boehmes@36900
  1315
#3022 := (= #3021 f1)
boehmes@36900
  1316
#3019 := (= #3018 f15)
boehmes@36900
  1317
#3020 := (not #3019)
boehmes@36900
  1318
#3023 := (and #3020 #3022)
boehmes@36900
  1319
#3017 := (= #3016 f1)
boehmes@36900
  1320
#3024 := (and #3017 #3023)
boehmes@36900
  1321
#3015 := (= #3014 f1)
boehmes@36900
  1322
#3025 := (and #3015 #3024)
boehmes@36900
  1323
#3013 := (= #3012 f27)
boehmes@36900
  1324
#3026 := (and #3013 #3025)
boehmes@36900
  1325
#3011 := (= #3010 f1)
boehmes@36900
  1326
#3027 := (and #3011 #3026)
boehmes@36900
  1327
#3365 := (implies #3027 #3364)
boehmes@36900
  1328
#3366 := (implies #3003 #3365)
boehmes@36900
  1329
#3002 := (< f286 1099511627776::int)
boehmes@36900
  1330
#3367 := (implies #3002 #3366)
boehmes@36900
  1331
#2999 := (<= f285 f77)
boehmes@36900
  1332
#2998 := (<= 0::int f285)
boehmes@36900
  1333
#3000 := (and #2998 #2999)
boehmes@36900
  1334
#3368 := (implies #3000 #3367)
boehmes@36900
  1335
#2995 := (<= f284 f77)
boehmes@36900
  1336
#2994 := (<= 0::int f284)
boehmes@36900
  1337
#2996 := (and #2994 #2995)
boehmes@36900
  1338
#3369 := (implies #2996 #3368)
boehmes@36900
  1339
#2991 := (<= f283 f79)
boehmes@36900
  1340
#2990 := (<= 0::int f283)
boehmes@36900
  1341
#2992 := (and #2990 #2991)
boehmes@36900
  1342
#3370 := (implies #2992 #3369)
boehmes@36900
  1343
#3371 := (not #3370)
boehmes@36900
  1344
#14253 := (iff #3371 #14250)
boehmes@36900
  1345
#12190 := (not #3133)
boehmes@36900
  1346
#12191 := (or #12190 #3134)
boehmes@36900
  1347
#5645 := (not #421)
boehmes@36900
  1348
#12197 := (or #5645 #12191)
boehmes@36900
  1349
#12202 := (forall (vars (?v0 int)) #12197)
boehmes@36900
  1350
#12210 := (not #12202)
boehmes@36900
  1351
#12211 := (or #3142 #12210)
boehmes@36900
  1352
#12216 := (and #12202 #12211)
boehmes@36900
  1353
#12223 := (or #12222 #12216)
boehmes@36900
  1354
#12232 := (or #12231 #12223)
boehmes@36900
  1355
#12241 := (or #12240 #12232)
boehmes@36900
  1356
#12250 := (or #12249 #12241)
boehmes@36900
  1357
#12141 := (and #3101 #3108)
boehmes@36900
  1358
#12258 := (not #12141)
boehmes@36900
  1359
#12259 := (or #12258 #12250)
boehmes@36900
  1360
#12267 := (or #12258 #12259)
boehmes@36900
  1361
#12275 := (or #12258 #12267)
boehmes@36900
  1362
#12284 := (or #12283 #12275)
boehmes@36900
  1363
#12289 := (and #10869 #12284)
boehmes@36900
  1364
#12295 := (or #12258 #12289)
boehmes@36900
  1365
#12303 := (or #12258 #12295)
boehmes@36900
  1366
#12882 := (or #12258 #12303)
boehmes@36900
  1367
#12890 := (or #12258 #12882)
boehmes@36900
  1368
#12898 := (not #3312)
boehmes@36900
  1369
#12899 := (or #12898 #12890)
boehmes@36900
  1370
#12907 := (or #12258 #12899)
boehmes@36900
  1371
#12555 := (and #3262 #12552)
boehmes@36900
  1372
#12537 := (not #3257)
boehmes@36900
  1373
#12538 := (or #12537 #3258)
boehmes@36900
  1374
#12544 := (or #5645 #12538)
boehmes@36900
  1375
#12549 := (forall (vars (?v0 int)) #12544)
boehmes@36900
  1376
#12568 := (not #12549)
boehmes@36900
  1377
#12569 := (or #12568 #12555)
boehmes@36900
  1378
#12574 := (and #12549 #12569)
boehmes@36900
  1379
#12580 := (not #3256)
boehmes@36900
  1380
#12581 := (or #12580 #12574)
boehmes@36900
  1381
#12586 := (and #3256 #12581)
boehmes@36900
  1382
#12534 := (and #3244 #3254)
boehmes@36900
  1383
#12592 := (not #12534)
boehmes@36900
  1384
#12593 := (or #12592 #12586)
boehmes@36900
  1385
#12602 := (or #12601 #12593)
boehmes@36900
  1386
#12516 := (+ 1::int f299)
boehmes@36900
  1387
#12528 := (= f307 #12516)
boehmes@36900
  1388
#12610 := (not #12528)
boehmes@36900
  1389
#12611 := (or #12610 #12602)
boehmes@36900
  1390
#12522 := (<= #12516 f77)
boehmes@36900
  1391
#12519 := (<= 0::int #12516)
boehmes@36900
  1392
#12525 := (and #12519 #12522)
boehmes@36900
  1393
#12619 := (not #12525)
boehmes@36900
  1394
#12620 := (or #12619 #12611)
boehmes@36900
  1395
#12625 := (and #12525 #12620)
boehmes@36900
  1396
#12631 := (not #3245)
boehmes@36900
  1397
#12632 := (or #12631 #12625)
boehmes@36900
  1398
#12758 := (or #12632 #12757)
boehmes@36900
  1399
#12767 := (or #12766 #12758)
boehmes@36900
  1400
#12775 := (or #12258 #12767)
boehmes@36900
  1401
#12783 := (or #12258 #12775)
boehmes@36900
  1402
#12791 := (or #12258 #12783)
boehmes@36900
  1403
#12799 := (not #3292)
boehmes@36900
  1404
#12800 := (or #12799 #12791)
boehmes@36900
  1405
#12808 := (or #12258 #12800)
boehmes@36900
  1406
#12641 := (or #12640 #12632)
boehmes@36900
  1407
#12650 := (or #12649 #12641)
boehmes@36900
  1408
#12658 := (not #3108)
boehmes@36900
  1409
#12659 := (or #12658 #12650)
boehmes@36900
  1410
#12668 := (or #12667 #12659)
boehmes@36900
  1411
#12677 := (or #12676 #12668)
boehmes@36900
  1412
#12686 := (or #12685 #12677)
boehmes@36900
  1413
#12695 := (or #12694 #12686)
boehmes@36900
  1414
#12700 := (and #12496 #12695)
boehmes@36900
  1415
#12707 := (or #12706 #12700)
boehmes@36900
  1416
#12712 := (and #12490 #12707)
boehmes@36900
  1417
#12718 := (or #12258 #12712)
boehmes@36900
  1418
#12726 := (or #12258 #12718)
boehmes@36900
  1419
#12734 := (not #3232)
boehmes@36900
  1420
#12735 := (or #12734 #12726)
boehmes@36900
  1421
#12743 := (or #12258 #12735)
boehmes@36900
  1422
#12813 := (and #12743 #12808)
boehmes@36900
  1423
#12819 := (or #12258 #12813)
boehmes@36900
  1424
#12827 := (or #12694 #12819)
boehmes@36900
  1425
#12832 := (and #12496 #12827)
boehmes@36900
  1426
#12838 := (or #12706 #12832)
boehmes@36900
  1427
#12843 := (and #12490 #12838)
boehmes@36900
  1428
#12849 := (or #12258 #12843)
boehmes@36900
  1429
#12857 := (or #12258 #12849)
boehmes@36900
  1430
#12865 := (not #3221)
boehmes@36900
  1431
#12866 := (or #12865 #12857)
boehmes@36900
  1432
#12874 := (or #12258 #12866)
boehmes@36900
  1433
#12912 := (and #12874 #12907)
boehmes@36900
  1434
#12918 := (or #12258 #12912)
boehmes@36900
  1435
#12934 := (or #12933 #12918)
boehmes@36900
  1436
#12943 := (or #12942 #12934)
boehmes@36900
  1437
#12952 := (or #12951 #12943)
boehmes@36900
  1438
#12961 := (or #12960 #12952)
boehmes@36900
  1439
#12970 := (or #12969 #12961)
boehmes@36900
  1440
#12978 := (or #12311 #12970)
boehmes@36900
  1441
#12427 := (and #3196 #12424)
boehmes@36900
  1442
#12430 := (and #3192 #12427)
boehmes@36900
  1443
#12986 := (not #12430)
boehmes@36900
  1444
#12987 := (or #12986 #12978)
boehmes@36900
  1445
#12995 := (or #12986 #12987)
boehmes@36900
  1446
#13003 := (or #12258 #12995)
boehmes@36900
  1447
#13011 := (or #12258 #13003)
boehmes@36900
  1448
#13019 := (or #12258 #13011)
boehmes@36900
  1449
#13034 := (or #12258 #13019)
boehmes@36900
  1450
#12162 := (and #3116 #12159)
boehmes@36900
  1451
#13042 := (not #12162)
boehmes@36900
  1452
#13043 := (or #13042 #13034)
boehmes@36900
  1453
#12144 := (not #3111)
boehmes@36900
  1454
#12145 := (or #12144 #3112)
boehmes@36900
  1455
#12151 := (or #5645 #12145)
boehmes@36900
  1456
#12156 := (forall (vars (?v0 int)) #12151)
boehmes@36900
  1457
#13051 := (not #12156)
boehmes@36900
  1458
#13052 := (or #13051 #13043)
boehmes@36900
  1459
#13060 := (not #3110)
boehmes@36900
  1460
#13061 := (or #13060 #13052)
boehmes@36900
  1461
#13069 := (or #12258 #13061)
boehmes@36900
  1462
#13077 := (not #3107)
boehmes@36900
  1463
#13078 := (or #13077 #13069)
boehmes@36900
  1464
#13086 := (not #3103)
boehmes@36900
  1465
#13087 := (or #13086 #13078)
boehmes@36900
  1466
#13095 := (not #3099)
boehmes@36900
  1467
#13096 := (or #13095 #13087)
boehmes@36900
  1468
#12138 := (and #3003 #3074)
boehmes@36900
  1469
#13104 := (not #12138)
boehmes@36900
  1470
#13105 := (or #13104 #13096)
boehmes@36900
  1471
#13110 := (and #12138 #13105)
boehmes@36900
  1472
#12121 := (not #3087)
boehmes@36900
  1473
#12122 := (or #12121 #3090)
boehmes@36900
  1474
#12128 := (or #5645 #12122)
boehmes@36900
  1475
#12133 := (forall (vars (?v0 int)) #12128)
boehmes@36900
  1476
#13116 := (not #12133)
boehmes@36900
  1477
#13117 := (or #13116 #13110)
boehmes@36900
  1478
#13122 := (and #12133 #13117)
boehmes@36900
  1479
#13128 := (not #3086)
boehmes@36900
  1480
#13129 := (or #13128 #13122)
boehmes@36900
  1481
#13134 := (and #3086 #13129)
boehmes@36900
  1482
#12115 := (and #3081 #3082)
boehmes@36900
  1483
#12118 := (and #3081 #12115)
boehmes@36900
  1484
#13140 := (not #12118)
boehmes@36900
  1485
#13141 := (or #13140 #13134)
boehmes@36900
  1486
#13150 := (or #13149 #13141)
boehmes@36900
  1487
#13159 := (or #13158 #13150)
boehmes@36900
  1488
#13168 := (or #13167 #13159)
boehmes@36900
  1489
#13177 := (or #13176 #13168)
boehmes@36900
  1490
#13186 := (or #13185 #13177)
boehmes@36900
  1491
#13191 := (and #12101 #13186)
boehmes@36900
  1492
#13198 := (or #13197 #13191)
boehmes@36900
  1493
#13203 := (and #12095 #13198)
boehmes@36900
  1494
#13210 := (or #13209 #13203)
boehmes@36900
  1495
#13215 := (and #12086 #13210)
boehmes@36900
  1496
#13221 := (not #3059)
boehmes@36900
  1497
#13222 := (or #13221 #13215)
boehmes@36900
  1498
#13231 := (or #13230 #13222)
boehmes@36900
  1499
#13240 := (or #13239 #13231)
boehmes@36900
  1500
#13249 := (or #13248 #13240)
boehmes@36900
  1501
#13258 := (or #13257 #13249)
boehmes@36900
  1502
#13266 := (not #3040)
boehmes@36900
  1503
#13267 := (or #13266 #13258)
boehmes@36900
  1504
#13276 := (or #13275 #13267)
boehmes@36900
  1505
#13285 := (or #13284 #13276)
boehmes@36900
  1506
#12033 := (and #12027 #12030)
boehmes@36900
  1507
#12036 := (and #12021 #12033)
boehmes@36900
  1508
#12039 := (and #12018 #12036)
boehmes@36900
  1509
#12042 := (and #12015 #12039)
boehmes@36900
  1510
#12045 := (and #12011 #12042)
boehmes@36900
  1511
#13293 := (not #12045)
boehmes@36900
  1512
#13294 := (or #13293 #13285)
boehmes@36900
  1513
#13302 := (not #3003)
boehmes@36900
  1514
#13303 := (or #13302 #13294)
boehmes@36900
  1515
#13311 := (not #3002)
boehmes@36900
  1516
#13312 := (or #13311 #13303)
boehmes@36900
  1517
#13320 := (not #3000)
boehmes@36900
  1518
#13321 := (or #13320 #13312)
boehmes@36900
  1519
#13329 := (not #2996)
boehmes@36900
  1520
#13330 := (or #13329 #13321)
boehmes@36900
  1521
#13338 := (not #2992)
boehmes@36900
  1522
#13339 := (or #13338 #13330)
boehmes@36900
  1523
#13344 := (not #13339)
boehmes@36900
  1524
#14251 := (iff #13344 #14250)
boehmes@36900
  1525
#14248 := (iff #13339 #14245)
boehmes@36900
  1526
#14203 := (or #13358 #14122)
boehmes@36900
  1527
#14206 := (or #13230 #14203)
boehmes@36900
  1528
#14209 := (or #13239 #14206)
boehmes@36900
  1529
#14212 := (or #13248 #14209)
boehmes@36900
  1530
#14215 := (or #13257 #14212)
boehmes@36900
  1531
#14218 := (or #14134 #14215)
boehmes@36900
  1532
#14221 := (or #13275 #14218)
boehmes@36900
  1533
#14224 := (or #13284 #14221)
boehmes@36900
  1534
#14227 := (or #14140 #14224)
boehmes@36900
  1535
#14230 := (or #13417 #14227)
boehmes@36900
  1536
#14233 := (or #14150 #14230)
boehmes@36900
  1537
#14236 := (or #14172 #14233)
boehmes@36900
  1538
#14239 := (or #14186 #14236)
boehmes@36900
  1539
#14242 := (or #14200 #14239)
boehmes@36900
  1540
#14246 := (iff #14242 #14245)
boehmes@36900
  1541
#14247 := [rewrite]: #14246
boehmes@36900
  1542
#14243 := (iff #13339 #14242)
boehmes@36900
  1543
#14240 := (iff #13330 #14239)
boehmes@36900
  1544
#14237 := (iff #13321 #14236)
boehmes@36900
  1545
#14234 := (iff #13312 #14233)
boehmes@36900
  1546
#14231 := (iff #13303 #14230)
boehmes@36900
  1547
#14228 := (iff #13294 #14227)
boehmes@36900
  1548
#14225 := (iff #13285 #14224)
boehmes@36900
  1549
#14222 := (iff #13276 #14221)
boehmes@36900
  1550
#14219 := (iff #13267 #14218)
boehmes@36900
  1551
#14216 := (iff #13258 #14215)
boehmes@36900
  1552
#14213 := (iff #13249 #14212)
boehmes@36900
  1553
#14210 := (iff #13240 #14209)
boehmes@36900
  1554
#14207 := (iff #13231 #14206)
boehmes@36900
  1555
#14204 := (iff #13222 #14203)
boehmes@36900
  1556
#14123 := (iff #13215 #14122)
boehmes@36900
  1557
#14120 := (iff #13210 #14119)
boehmes@36900
  1558
#14117 := (iff #13203 #14114)
boehmes@36900
  1559
#14111 := (and #12095 #14108)
boehmes@36900
  1560
#14115 := (iff #14111 #14114)
boehmes@36900
  1561
#14116 := [rewrite]: #14115
boehmes@36900
  1562
#14112 := (iff #13203 #14111)
boehmes@36900
  1563
#14109 := (iff #13198 #14108)
boehmes@36900
  1564
#14106 := (iff #13191 #14103)
boehmes@36900
  1565
#14100 := (and #12101 #14095)
boehmes@36900
  1566
#14104 := (iff #14100 #14103)
boehmes@36900
  1567
#14105 := [rewrite]: #14104
boehmes@36900
  1568
#14101 := (iff #13191 #14100)
boehmes@36900
  1569
#14098 := (iff #13186 #14095)
boehmes@36900
  1570
#14077 := (or false #14074)
boehmes@36900
  1571
#14080 := (or #13149 #14077)
boehmes@36900
  1572
#14083 := (or #13158 #14080)
boehmes@36900
  1573
#14086 := (or #13167 #14083)
boehmes@36900
  1574
#14089 := (or #13176 #14086)
boehmes@36900
  1575
#14092 := (or #13185 #14089)
boehmes@36900
  1576
#14096 := (iff #14092 #14095)
boehmes@36900
  1577
#14097 := [rewrite]: #14096
boehmes@36900
  1578
#14093 := (iff #13186 #14092)
boehmes@36900
  1579
#14090 := (iff #13177 #14089)
boehmes@36900
  1580
#14087 := (iff #13168 #14086)
boehmes@36900
  1581
#14084 := (iff #13159 #14083)
boehmes@36900
  1582
#14081 := (iff #13150 #14080)
boehmes@36900
  1583
#14078 := (iff #13141 #14077)
boehmes@36900
  1584
#14075 := (iff #13134 #14074)
boehmes@36900
  1585
#14072 := (iff #13129 #14071)
boehmes@36900
  1586
#14069 := (iff #13122 #14068)
boehmes@36900
  1587
#14066 := (iff #13117 #14065)
boehmes@36900
  1588
#14063 := (iff #13110 #14060)
boehmes@36900
  1589
#13978 := (and #13418 #3074)
boehmes@36900
  1590
#14057 := (and #13978 #14052)
boehmes@36900
  1591
#14061 := (iff #14057 #14060)
boehmes@36900
  1592
#14062 := [rewrite]: #14061
boehmes@36900
  1593
#14058 := (iff #13110 #14057)
boehmes@36900
  1594
#14055 := (iff #13105 #14052)
boehmes@36900
  1595
#13989 := (or #13430 #13859)
boehmes@36900
  1596
#13992 := (or #12933 #13989)
boehmes@36900
  1597
#13995 := (or #12942 #13992)
boehmes@36900
  1598
#13998 := (or #12951 #13995)
boehmes@36900
  1599
#14001 := (or #12960 #13998)
boehmes@36900
  1600
#14004 := (or #12969 #14001)
boehmes@36900
  1601
#14007 := (or #12311 #14004)
boehmes@36900
  1602
#14010 := (or #13883 #14007)
boehmes@36900
  1603
#14013 := (or #13883 #14010)
boehmes@36900
  1604
#14016 := (or #13430 #14013)
boehmes@36900
  1605
#14019 := (or #13430 #14016)
boehmes@36900
  1606
#14022 := (or #13430 #14019)
boehmes@36900
  1607
#14025 := (or #13430 #14022)
boehmes@36900
  1608
#14028 := (or #13900 #14025)
boehmes@36900
  1609
#14031 := (or #13934 #14028)
boehmes@36900
  1610
#14034 := (or #13940 #14031)
boehmes@36900
  1611
#14037 := (or #13430 #14034)
boehmes@36900
  1612
#14040 := (or #13952 #14037)
boehmes@36900
  1613
#14043 := (or #13962 #14040)
boehmes@36900
  1614
#14046 := (or #13975 #14043)
boehmes@36900
  1615
#14049 := (or #13986 #14046)
boehmes@36900
  1616
#14053 := (iff #14049 #14052)
boehmes@36900
  1617
#14054 := [rewrite]: #14053
boehmes@36900
  1618
#14050 := (iff #13105 #14049)
boehmes@36900
  1619
#14047 := (iff #13096 #14046)
boehmes@36900
  1620
#14044 := (iff #13087 #14043)
boehmes@36900
  1621
#14041 := (iff #13078 #14040)
boehmes@36900
  1622
#14038 := (iff #13069 #14037)
boehmes@36900
  1623
#14035 := (iff #13061 #14034)
boehmes@36900
  1624
#14032 := (iff #13052 #14031)
boehmes@36900
  1625
#14029 := (iff #13043 #14028)
boehmes@36900
  1626
#14026 := (iff #13034 #14025)
boehmes@36900
  1627
#14023 := (iff #13019 #14022)
boehmes@36900
  1628
#14020 := (iff #13011 #14019)
boehmes@36900
  1629
#14017 := (iff #13003 #14016)
boehmes@36900
  1630
#14014 := (iff #12995 #14013)
boehmes@36900
  1631
#14011 := (iff #12987 #14010)
boehmes@36900
  1632
#14008 := (iff #12978 #14007)
boehmes@36900
  1633
#14005 := (iff #12970 #14004)
boehmes@36900
  1634
#14002 := (iff #12961 #14001)
boehmes@36900
  1635
#13999 := (iff #12952 #13998)
boehmes@36900
  1636
#13996 := (iff #12943 #13995)
boehmes@36900
  1637
#13993 := (iff #12934 #13992)
boehmes@36900
  1638
#13990 := (iff #12918 #13989)
boehmes@36900
  1639
#13860 := (iff #12912 #13859)
boehmes@36900
  1640
#13857 := (iff #12907 #13854)
boehmes@36900
  1641
#13836 := (or #13430 #13829)
boehmes@36900
  1642
#13839 := (or #13430 #13836)
boehmes@36900
  1643
#13842 := (or #13430 #13839)
boehmes@36900
  1644
#13845 := (or #13430 #13842)
boehmes@36900
  1645
#13848 := (or #13711 #13845)
boehmes@36900
  1646
#13851 := (or #13430 #13848)
boehmes@36900
  1647
#13855 := (iff #13851 #13854)
boehmes@36900
  1648
#13856 := [rewrite]: #13855
boehmes@36900
  1649
#13852 := (iff #12907 #13851)
boehmes@36900
  1650
#13849 := (iff #12899 #13848)
boehmes@36900
  1651
#13846 := (iff #12890 #13845)
boehmes@36900
  1652
#13843 := (iff #12882 #13842)
boehmes@36900
  1653
#13840 := (iff #12303 #13839)
boehmes@36900
  1654
#13837 := (iff #12295 #13836)
boehmes@36900
  1655
#13830 := (iff #12289 #13829)
boehmes@36900
  1656
#13827 := (iff #12284 #13824)
boehmes@36900
  1657
#13800 := (or #12222 #13797)
boehmes@36900
  1658
#13803 := (or #12231 #13800)
boehmes@36900
  1659
#13806 := (or #12240 #13803)
boehmes@36900
  1660
#13809 := (or #12249 #13806)
boehmes@36900
  1661
#13812 := (or #13430 #13809)
boehmes@36900
  1662
#13815 := (or #13430 #13812)
boehmes@36900
  1663
#13818 := (or #13430 #13815)
boehmes@36900
  1664
#13821 := (or #12283 #13818)
boehmes@36900
  1665
#13825 := (iff #13821 #13824)
boehmes@36900
  1666
#13826 := [rewrite]: #13825
boehmes@36900
  1667
#13822 := (iff #12284 #13821)
boehmes@36900
  1668
#13819 := (iff #12275 #13818)
boehmes@36900
  1669
#13816 := (iff #12267 #13815)
boehmes@36900
  1670
#13813 := (iff #12259 #13812)
boehmes@36900
  1671
#13810 := (iff #12250 #13809)
boehmes@36900
  1672
#13807 := (iff #12241 #13806)
boehmes@36900
  1673
#13804 := (iff #12232 #13803)
boehmes@36900
  1674
#13801 := (iff #12223 #13800)
boehmes@36900
  1675
#13798 := (iff #12216 #13797)
boehmes@36900
  1676
#13795 := (iff #12211 #13792)
boehmes@36900
  1677
#13789 := (or #13783 #13786)
boehmes@36900
  1678
#13793 := (iff #13789 #13792)
boehmes@36900
  1679
#13794 := [rewrite]: #13793
boehmes@36900
  1680
#13790 := (iff #12211 #13789)
boehmes@36900
  1681
#13787 := (iff #12210 #13786)
boehmes@36900
  1682
#13767 := (iff #12202 #13766)
boehmes@36900
  1683
#13764 := (iff #12197 #13761)
boehmes@36900
  1684
#13755 := (or #13738 #13752)
boehmes@36900
  1685
#13758 := (or #5654 #13755)
boehmes@36900
  1686
#13762 := (iff #13758 #13761)
boehmes@36900
  1687
#13763 := [rewrite]: #13762
boehmes@36900
  1688
#13759 := (iff #12197 #13758)
boehmes@36900
  1689
#13756 := (iff #12191 #13755)
boehmes@36900
  1690
#13753 := (iff #3134 #13752)
boehmes@36900
  1691
#13754 := [rewrite]: #13753
boehmes@36900
  1692
#13748 := (iff #12190 #13738)
boehmes@36900
  1693
#13743 := (not #13740)
boehmes@36900
  1694
#13746 := (iff #13743 #13738)
boehmes@36900
  1695
#13747 := [rewrite]: #13746
boehmes@36900
  1696
#13744 := (iff #12190 #13743)
boehmes@36900
  1697
#13741 := (iff #3133 #13740)
boehmes@36900
  1698
#13742 := [rewrite]: #13741
boehmes@36900
  1699
#13745 := [monotonicity #13742]: #13744
boehmes@36900
  1700
#13749 := [trans #13745 #13747]: #13748
boehmes@36900
  1701
#13757 := [monotonicity #13749 #13754]: #13756
boehmes@36900
  1702
#5655 := (iff #5645 #5654)
boehmes@36900
  1703
#4440 := (iff #421 #4439)
boehmes@36900
  1704
#4433 := (iff #420 #4432)
boehmes@36900
  1705
#4434 := [rewrite]: #4433
boehmes@36900
  1706
#4116 := (iff #293 #4118)
boehmes@36900
  1707
#4117 := [rewrite]: #4116
boehmes@36900
  1708
#4441 := [monotonicity #4117 #4434]: #4440
boehmes@36900
  1709
#5656 := [monotonicity #4441]: #5655
boehmes@36900
  1710
#13760 := [monotonicity #5656 #13757]: #13759
boehmes@36900
  1711
#13765 := [trans #13760 #13763]: #13764
boehmes@36900
  1712
#13768 := [quant-intro #13765]: #13767
boehmes@36900
  1713
#13788 := [monotonicity #13768]: #13787
boehmes@36900
  1714
#13784 := (iff #3142 #13783)
boehmes@36900
  1715
#13781 := (iff #3141 #13778)
boehmes@36900
  1716
#13769 := (and #13740 #3138)
boehmes@36900
  1717
#13772 := (and #4432 #13769)
boehmes@36900
  1718
#13775 := (and #4118 #13772)
boehmes@36900
  1719
#13779 := (iff #13775 #13778)
boehmes@36900
  1720
#13780 := [rewrite]: #13779
boehmes@36900
  1721
#13776 := (iff #3141 #13775)
boehmes@36900
  1722
#13773 := (iff #3140 #13772)
boehmes@36900
  1723
#13770 := (iff #3139 #13769)
boehmes@36900
  1724
#13771 := [monotonicity #13742]: #13770
boehmes@36900
  1725
#13774 := [monotonicity #4434 #13771]: #13773
boehmes@36900
  1726
#13777 := [monotonicity #4117 #13774]: #13776
boehmes@36900
  1727
#13782 := [trans #13777 #13780]: #13781
boehmes@36900
  1728
#13785 := [quant-intro #13782]: #13784
boehmes@36900
  1729
#13791 := [monotonicity #13785 #13788]: #13790
boehmes@36900
  1730
#13796 := [trans #13791 #13794]: #13795
boehmes@36900
  1731
#13799 := [monotonicity #13768 #13796]: #13798
boehmes@36900
  1732
#13802 := [monotonicity #13799]: #13801
boehmes@36900
  1733
#13805 := [monotonicity #13802]: #13804
boehmes@36900
  1734
#13808 := [monotonicity #13805]: #13807
boehmes@36900
  1735
#13811 := [monotonicity #13808]: #13810
boehmes@36900
  1736
#13431 := (iff #12258 #13430)
boehmes@36900
  1737
#13428 := (iff #12141 #13427)
boehmes@36900
  1738
#13424 := (iff #3108 #13425)
boehmes@36900
  1739
#13426 := [rewrite]: #13424
boehmes@36900
  1740
#13421 := (iff #3101 #13422)
boehmes@36900
  1741
#13423 := [rewrite]: #13421
boehmes@36900
  1742
#13429 := [monotonicity #13423 #13426]: #13428
boehmes@36900
  1743
#13432 := [monotonicity #13429]: #13431
boehmes@36900
  1744
#13814 := [monotonicity #13432 #13811]: #13813
boehmes@36900
  1745
#13817 := [monotonicity #13432 #13814]: #13816
boehmes@36900
  1746
#13820 := [monotonicity #13432 #13817]: #13819
boehmes@36900
  1747
#13823 := [monotonicity #13820]: #13822
boehmes@36900
  1748
#13828 := [trans #13823 #13826]: #13827
boehmes@36900
  1749
#13831 := [monotonicity #13828]: #13830
boehmes@36900
  1750
#13838 := [monotonicity #13432 #13831]: #13837
boehmes@36900
  1751
#13841 := [monotonicity #13432 #13838]: #13840
boehmes@36900
  1752
#13844 := [monotonicity #13432 #13841]: #13843
boehmes@36900
  1753
#13847 := [monotonicity #13432 #13844]: #13846
boehmes@36900
  1754
#13834 := (iff #12898 #13711)
boehmes@36900
  1755
#13832 := (iff #3312 #13710)
boehmes@36900
  1756
#13833 := [rewrite]: #13832
boehmes@36900
  1757
#13835 := [monotonicity #13833]: #13834
boehmes@36900
  1758
#13850 := [monotonicity #13835 #13847]: #13849
boehmes@36900
  1759
#13853 := [monotonicity #13432 #13850]: #13852
boehmes@36900
  1760
#13858 := [trans #13853 #13856]: #13857
boehmes@36900
  1761
#13736 := (iff #12874 #13733)
boehmes@36900
  1762
#13721 := (or #13430 #13704)
boehmes@36900
  1763
#13724 := (or #13430 #13721)
boehmes@36900
  1764
#13727 := (or #13710 #13724)
boehmes@36900
  1765
#13730 := (or #13430 #13727)
boehmes@36900
  1766
#13734 := (iff #13730 #13733)
boehmes@36900
  1767
#13735 := [rewrite]: #13734
boehmes@36900
  1768
#13731 := (iff #12874 #13730)
boehmes@36900
  1769
#13728 := (iff #12866 #13727)
boehmes@36900
  1770
#13725 := (iff #12857 #13724)
boehmes@36900
  1771
#13722 := (iff #12849 #13721)
boehmes@36900
  1772
#13707 := (iff #12843 #13704)
boehmes@36900
  1773
#13701 := (and #12490 #13698)
boehmes@36900
  1774
#13705 := (iff #13701 #13704)
boehmes@36900
  1775
#13706 := [rewrite]: #13705
boehmes@36900
  1776
#13702 := (iff #12843 #13701)
boehmes@36900
  1777
#13699 := (iff #12838 #13698)
boehmes@36900
  1778
#13696 := (iff #12832 #13693)
boehmes@36900
  1779
#13690 := (and #12496 #13685)
boehmes@36900
  1780
#13694 := (iff #13690 #13693)
boehmes@36900
  1781
#13695 := [rewrite]: #13694
boehmes@36900
  1782
#13691 := (iff #12832 #13690)
boehmes@36900
  1783
#13688 := (iff #12827 #13685)
boehmes@36900
  1784
#13679 := (or #13430 #13676)
boehmes@36900
  1785
#13682 := (or #12694 #13679)
boehmes@36900
  1786
#13686 := (iff #13682 #13685)
boehmes@36900
  1787
#13687 := [rewrite]: #13686
boehmes@36900
  1788
#13683 := (iff #12827 #13682)
boehmes@36900
  1789
#13680 := (iff #12819 #13679)
boehmes@36900
  1790
#13677 := (iff #12813 #13676)
boehmes@36900
  1791
#13674 := (iff #12808 #13671)
boehmes@36900
  1792
#13568 := (or #13439 #13560)
boehmes@36900
  1793
#13650 := (or #13568 #12757)
boehmes@36900
  1794
#13653 := (or #12766 #13650)
boehmes@36900
  1795
#13656 := (or #13430 #13653)
boehmes@36900
  1796
#13659 := (or #13430 #13656)
boehmes@36900
  1797
#13662 := (or #13430 #13659)
boehmes@36900
  1798
#13665 := (or #13616 #13662)
boehmes@36900
  1799
#13668 := (or #13430 #13665)
boehmes@36900
  1800
#13672 := (iff #13668 #13671)
boehmes@36900
  1801
#13673 := [rewrite]: #13672
boehmes@36900
  1802
#13669 := (iff #12808 #13668)
boehmes@36900
  1803
#13666 := (iff #12800 #13665)
boehmes@36900
  1804
#13663 := (iff #12791 #13662)
boehmes@36900
  1805
#13660 := (iff #12783 #13659)
boehmes@36900
  1806
#13657 := (iff #12775 #13656)
boehmes@36900
  1807
#13654 := (iff #12767 #13653)
boehmes@36900
  1808
#13651 := (iff #12758 #13650)
boehmes@36900
  1809
#13569 := (iff #12632 #13568)
boehmes@36900
  1810
#13563 := (iff #12625 #13560)
boehmes@36900
  1811
#13557 := (and #13534 #13552)
boehmes@36900
  1812
#13561 := (iff #13557 #13560)
boehmes@36900
  1813
#13562 := [rewrite]: #13561
boehmes@36900
  1814
#13558 := (iff #12625 #13557)
boehmes@36900
  1815
#13555 := (iff #12620 #13552)
boehmes@36900
  1816
#13540 := (or #13456 #13524)
boehmes@36900
  1817
#13543 := (or #12601 #13540)
boehmes@36900
  1818
#13546 := (or #13531 #13543)
boehmes@36900
  1819
#13549 := (or #13537 #13546)
boehmes@36900
  1820
#13553 := (iff #13549 #13552)
boehmes@36900
  1821
#13554 := [rewrite]: #13553
boehmes@36900
  1822
#13550 := (iff #12620 #13549)
boehmes@36900
  1823
#13547 := (iff #12611 #13546)
boehmes@36900
  1824
#13544 := (iff #12602 #13543)
boehmes@36900
  1825
#13541 := (iff #12593 #13540)
boehmes@36900
  1826
#13525 := (iff #12586 #13524)
boehmes@36900
  1827
#13522 := (iff #12581 #13521)
boehmes@36900
  1828
#13519 := (iff #12574 #13518)
boehmes@36900
  1829
#13516 := (iff #12569 #13515)
boehmes@36900
  1830
#13513 := (iff #12555 #13510)
boehmes@36900
  1831
#13507 := (and #13504 #12552)
boehmes@36900
  1832
#13511 := (iff #13507 #13510)
boehmes@36900
  1833
#13512 := [rewrite]: #13511
boehmes@36900
  1834
#13508 := (iff #12555 #13507)
boehmes@36900
  1835
#13505 := (iff #3262 #13504)
boehmes@36900
  1836
#13506 := [rewrite]: #13505
boehmes@36900
  1837
#13509 := [monotonicity #13506]: #13508
boehmes@36900
  1838
#13514 := [trans #13509 #13512]: #13513
boehmes@36900
  1839
#13499 := (iff #12568 #13498)
boehmes@36900
  1840
#13496 := (iff #12549 #13495)
boehmes@36900
  1841
#13493 := (iff #12544 #13490)
boehmes@36900
  1842
#13484 := (or #13467 #13481)
boehmes@36900
  1843
#13487 := (or #5654 #13484)
boehmes@36900
  1844
#13491 := (iff #13487 #13490)
boehmes@36900
  1845
#13492 := [rewrite]: #13491
boehmes@36900
  1846
#13488 := (iff #12544 #13487)
boehmes@36900
  1847
#13485 := (iff #12538 #13484)
boehmes@36900
  1848
#13482 := (iff #3258 #13481)
boehmes@36900
  1849
#13483 := [rewrite]: #13482
boehmes@36900
  1850
#13477 := (iff #12537 #13467)
boehmes@36900
  1851
#13469 := (not #13467)
boehmes@36900
  1852
#13472 := (not #13469)
boehmes@36900
  1853
#13475 := (iff #13472 #13467)
boehmes@36900
  1854
#13476 := [rewrite]: #13475
boehmes@36900
  1855
#13473 := (iff #12537 #13472)
boehmes@36900
  1856
#13470 := (iff #3257 #13469)
boehmes@36900
  1857
#13471 := [rewrite]: #13470
boehmes@36900
  1858
#13474 := [monotonicity #13471]: #13473
boehmes@36900
  1859
#13478 := [trans #13474 #13476]: #13477
boehmes@36900
  1860
#13486 := [monotonicity #13478 #13483]: #13485
boehmes@36900
  1861
#13489 := [monotonicity #5656 #13486]: #13488
boehmes@36900
  1862
#13494 := [trans #13489 #13492]: #13493
boehmes@36900
  1863
#13497 := [quant-intro #13494]: #13496
boehmes@36900
  1864
#13500 := [monotonicity #13497]: #13499
boehmes@36900
  1865
#13517 := [monotonicity #13500 #13514]: #13516
boehmes@36900
  1866
#13520 := [monotonicity #13497 #13517]: #13519
boehmes@36900
  1867
#13465 := (iff #12580 #13464)
boehmes@36900
  1868
#13462 := (iff #3256 #13459)
boehmes@36900
  1869
#13463 := [rewrite]: #13462
boehmes@36900
  1870
#13466 := [monotonicity #13463]: #13465
boehmes@36900
  1871
#13523 := [monotonicity #13466 #13520]: #13522
boehmes@36900
  1872
#13526 := [monotonicity #13463 #13523]: #13525
boehmes@36900
  1873
#13457 := (iff #12592 #13456)
boehmes@36900
  1874
#13454 := (iff #12534 #13453)
boehmes@36900
  1875
#13450 := (iff #3254 #13451)
boehmes@36900
  1876
#13452 := [rewrite]: #13450
boehmes@36900
  1877
#13433 := (iff #3244 #13434)
boehmes@36900
  1878
#13435 := [rewrite]: #13433
boehmes@36900
  1879
#13455 := [monotonicity #13435 #13452]: #13454
boehmes@36900
  1880
#13458 := [monotonicity #13455]: #13457
boehmes@36900
  1881
#13542 := [monotonicity #13458 #13526]: #13541
boehmes@36900
  1882
#13545 := [monotonicity #13542]: #13544
boehmes@36900
  1883
#13532 := (iff #12610 #13531)
boehmes@36900
  1884
#13529 := (iff #12528 #13527)
boehmes@36900
  1885
#13530 := [rewrite]: #13529
boehmes@36900
  1886
#13533 := [monotonicity #13530]: #13532
boehmes@36900
  1887
#13548 := [monotonicity #13533 #13545]: #13547
boehmes@36900
  1888
#13538 := (iff #12619 #13537)
boehmes@36900
  1889
#13535 := (iff #12525 #13534)
boehmes@36900
  1890
#13448 := (iff #12522 #13445)
boehmes@36900
  1891
#13449 := [rewrite]: #13448
boehmes@36900
  1892
#13442 := (iff #12519 #13443)
boehmes@36900
  1893
#13444 := [rewrite]: #13442
boehmes@36900
  1894
#13536 := [monotonicity #13444 #13449]: #13535
boehmes@36900
  1895
#13539 := [monotonicity #13536]: #13538
boehmes@36900
  1896
#13551 := [monotonicity #13539 #13548]: #13550
boehmes@36900
  1897
#13556 := [trans #13551 #13554]: #13555
boehmes@36900
  1898
#13559 := [monotonicity #13536 #13556]: #13558
boehmes@36900
  1899
#13564 := [trans #13559 #13562]: #13563
boehmes@36900
  1900
#13440 := (iff #12631 #13439)
boehmes@36900
  1901
#13437 := (iff #3245 #13436)
boehmes@36900
  1902
#13438 := [monotonicity #13426 #13435]: #13437
boehmes@36900
  1903
#13441 := [monotonicity #13438]: #13440
boehmes@36900
  1904
#13570 := [monotonicity #13441 #13564]: #13569
boehmes@36900
  1905
#13652 := [monotonicity #13570]: #13651
boehmes@36900
  1906
#13655 := [monotonicity #13652]: #13654
boehmes@36900
  1907
#13658 := [monotonicity #13432 #13655]: #13657
boehmes@36900
  1908
#13661 := [monotonicity #13432 #13658]: #13660
boehmes@36900
  1909
#13664 := [monotonicity #13432 #13661]: #13663
boehmes@36900
  1910
#13648 := (iff #12799 #13616)
boehmes@36900
  1911
#13646 := (iff #3292 #13617)
boehmes@36900
  1912
#13647 := [rewrite]: #13646
boehmes@36900
  1913
#13649 := [monotonicity #13647]: #13648
boehmes@36900
  1914
#13667 := [monotonicity #13649 #13664]: #13666
boehmes@36900
  1915
#13670 := [monotonicity #13432 #13667]: #13669
boehmes@36900
  1916
#13675 := [trans #13670 #13673]: #13674
boehmes@36900
  1917
#13644 := (iff #12743 #13641)
boehmes@36900
  1918
#13629 := (or #13430 #13611)
boehmes@36900
  1919
#13632 := (or #13430 #13629)
boehmes@36900
  1920
#13635 := (or #13617 #13632)
boehmes@36900
  1921
#13638 := (or #13430 #13635)
boehmes@36900
  1922
#13642 := (iff #13638 #13641)
boehmes@36900
  1923
#13643 := [rewrite]: #13642
boehmes@36900
  1924
#13639 := (iff #12743 #13638)
boehmes@36900
  1925
#13636 := (iff #12735 #13635)
boehmes@36900
  1926
#13633 := (iff #12726 #13632)
boehmes@36900
  1927
#13630 := (iff #12718 #13629)
boehmes@36900
  1928
#13614 := (iff #12712 #13611)
boehmes@36900
  1929
#13608 := (and #12490 #13605)
boehmes@36900
  1930
#13612 := (iff #13608 #13611)
boehmes@36900
  1931
#13613 := [rewrite]: #13612
boehmes@36900
  1932
#13609 := (iff #12712 #13608)
boehmes@36900
  1933
#13606 := (iff #12707 #13605)
boehmes@36900
  1934
#13603 := (iff #12700 #13600)
boehmes@36900
  1935
#13597 := (and #12496 #13592)
boehmes@36900
  1936
#13601 := (iff #13597 #13600)
boehmes@36900
  1937
#13602 := [rewrite]: #13601
boehmes@36900
  1938
#13598 := (iff #12700 #13597)
boehmes@36900
  1939
#13595 := (iff #12695 #13592)
boehmes@36900
  1940
#13571 := (or #12640 #13568)
boehmes@36900
  1941
#13574 := (or #12649 #13571)
boehmes@36900
  1942
#13577 := (or #13565 #13574)
boehmes@36900
  1943
#13580 := (or #12667 #13577)
boehmes@36900
  1944
#13583 := (or #12676 #13580)
boehmes@36900
  1945
#13586 := (or #12685 #13583)
boehmes@36900
  1946
#13589 := (or #12694 #13586)
boehmes@36900
  1947
#13593 := (iff #13589 #13592)
boehmes@36900
  1948
#13594 := [rewrite]: #13593
boehmes@36900
  1949
#13590 := (iff #12695 #13589)
boehmes@36900
  1950
#13587 := (iff #12686 #13586)
boehmes@36900
  1951
#13584 := (iff #12677 #13583)
boehmes@36900
  1952
#13581 := (iff #12668 #13580)
boehmes@36900
  1953
#13578 := (iff #12659 #13577)
boehmes@36900
  1954
#13575 := (iff #12650 #13574)
boehmes@36900
  1955
#13572 := (iff #12641 #13571)
boehmes@36900
  1956
#13573 := [monotonicity #13570]: #13572
boehmes@36900
  1957
#13576 := [monotonicity #13573]: #13575
boehmes@36900
  1958
#13566 := (iff #12658 #13565)
boehmes@36900
  1959
#13567 := [monotonicity #13426]: #13566
boehmes@36900
  1960
#13579 := [monotonicity #13567 #13576]: #13578
boehmes@36900
  1961
#13582 := [monotonicity #13579]: #13581
boehmes@36900
  1962
#13585 := [monotonicity #13582]: #13584
boehmes@36900
  1963
#13588 := [monotonicity #13585]: #13587
boehmes@36900
  1964
#13591 := [monotonicity #13588]: #13590
boehmes@36900
  1965
#13596 := [trans #13591 #13594]: #13595
boehmes@36900
  1966
#13599 := [monotonicity #13596]: #13598
boehmes@36900
  1967
#13604 := [trans #13599 #13602]: #13603
boehmes@36900
  1968
#13607 := [monotonicity #13604]: #13606
boehmes@36900
  1969
#13610 := [monotonicity #13607]: #13609
boehmes@36900
  1970
#13615 := [trans #13610 #13613]: #13614
boehmes@36900
  1971
#13631 := [monotonicity #13432 #13615]: #13630
boehmes@36900
  1972
#13634 := [monotonicity #13432 #13631]: #13633
boehmes@36900
  1973
#13627 := (iff #12734 #13617)
boehmes@36900
  1974
#13622 := (not #13616)
boehmes@36900
  1975
#13625 := (iff #13622 #13617)
boehmes@36900
  1976
#13626 := [rewrite]: #13625
boehmes@36900
  1977
#13623 := (iff #12734 #13622)
boehmes@36900
  1978
#13620 := (iff #3232 #13616)
boehmes@36900
  1979
#13621 := [rewrite]: #13620
boehmes@36900
  1980
#13624 := [monotonicity #13621]: #13623
boehmes@36900
  1981
#13628 := [trans #13624 #13626]: #13627
boehmes@36900
  1982
#13637 := [monotonicity #13628 #13634]: #13636
boehmes@36900
  1983
#13640 := [monotonicity #13432 #13637]: #13639
boehmes@36900
  1984
#13645 := [trans #13640 #13643]: #13644
boehmes@36900
  1985
#13678 := [monotonicity #13645 #13675]: #13677
boehmes@36900
  1986
#13681 := [monotonicity #13432 #13678]: #13680
boehmes@36900
  1987
#13684 := [monotonicity #13681]: #13683
boehmes@36900
  1988
#13689 := [trans #13684 #13687]: #13688
boehmes@36900
  1989
#13692 := [monotonicity #13689]: #13691
boehmes@36900
  1990
#13697 := [trans #13692 #13695]: #13696
boehmes@36900
  1991
#13700 := [monotonicity #13697]: #13699
boehmes@36900
  1992
#13703 := [monotonicity #13700]: #13702
boehmes@36900
  1993
#13708 := [trans #13703 #13706]: #13707
boehmes@36900
  1994
#13723 := [monotonicity #13432 #13708]: #13722
boehmes@36900
  1995
#13726 := [monotonicity #13432 #13723]: #13725
boehmes@36900
  1996
#13719 := (iff #12865 #13710)
boehmes@36900
  1997
#13714 := (not #13711)
boehmes@36900
  1998
#13717 := (iff #13714 #13710)
boehmes@36900
  1999
#13718 := [rewrite]: #13717
boehmes@36900
  2000
#13715 := (iff #12865 #13714)
boehmes@36900
  2001
#13712 := (iff #3221 #13711)
boehmes@36900
  2002
#13713 := [rewrite]: #13712
boehmes@36900
  2003
#13716 := [monotonicity #13713]: #13715
boehmes@36900
  2004
#13720 := [trans #13716 #13718]: #13719
boehmes@36900
  2005
#13729 := [monotonicity #13720 #13726]: #13728
boehmes@36900
  2006
#13732 := [monotonicity #13432 #13729]: #13731
boehmes@36900
  2007
#13737 := [trans #13732 #13735]: #13736
boehmes@36900
  2008
#13861 := [monotonicity #13737 #13858]: #13860
boehmes@36900
  2009
#13991 := [monotonicity #13432 #13861]: #13990
boehmes@36900
  2010
#13994 := [monotonicity #13991]: #13993
boehmes@36900
  2011
#13997 := [monotonicity #13994]: #13996
boehmes@36900
  2012
#14000 := [monotonicity #13997]: #13999
boehmes@36900
  2013
#14003 := [monotonicity #14000]: #14002
boehmes@36900
  2014
#14006 := [monotonicity #14003]: #14005
boehmes@36900
  2015
#14009 := [monotonicity #14006]: #14008
boehmes@36900
  2016
#13884 := (iff #12986 #13883)
boehmes@36900
  2017
#13881 := (iff #12430 #12424)
boehmes@36900
  2018
#13873 := (and true #12424)
boehmes@36900
  2019
#13876 := (and true #13873)
boehmes@36900
  2020
#13879 := (iff #13876 #12424)
boehmes@36900
  2021
#13880 := [rewrite]: #13879
boehmes@36900
  2022
#13877 := (iff #12430 #13876)
boehmes@36900
  2023
#13874 := (iff #12427 #13873)
boehmes@36900
  2024
#13869 := (iff #3196 true)
boehmes@36900
  2025
#13864 := (forall (vars (?v0 S5)) (:pat #3194) true)
boehmes@36900
  2026
#13867 := (iff #13864 true)
boehmes@36900
  2027
#13868 := [elim-unused]: #13867
boehmes@36900
  2028
#13865 := (iff #3196 #13864)
boehmes@36900
  2029
#13862 := (iff #3195 true)
boehmes@36900
  2030
#13863 := [rewrite]: #13862
boehmes@36900
  2031
#13866 := [quant-intro #13863]: #13865
boehmes@36900
  2032
#13870 := [trans #13866 #13868]: #13869
boehmes@36900
  2033
#13875 := [monotonicity #13870]: #13874
boehmes@36900
  2034
#13871 := (iff #3192 true)
boehmes@36900
  2035
#13872 := [rewrite]: #13871
boehmes@36900
  2036
#13878 := [monotonicity #13872 #13875]: #13877
boehmes@36900
  2037
#13882 := [trans #13878 #13880]: #13881
boehmes@36900
  2038
#13885 := [monotonicity #13882]: #13884
boehmes@36900
  2039
#14012 := [monotonicity #13885 #14009]: #14011
boehmes@36900
  2040
#14015 := [monotonicity #13885 #14012]: #14014
boehmes@36900
  2041
#14018 := [monotonicity #13432 #14015]: #14017
boehmes@36900
  2042
#14021 := [monotonicity #13432 #14018]: #14020
boehmes@36900
  2043
#14024 := [monotonicity #13432 #14021]: #14023
boehmes@36900
  2044
#14027 := [monotonicity #13432 #14024]: #14026
boehmes@36900
  2045
#13901 := (iff #13042 #13900)
boehmes@36900
  2046
#13898 := (iff #12162 #13895)
boehmes@36900
  2047
#13892 := (and #13889 #12159)
boehmes@34994
  2048
#13896 := (iff #13892 #13895)
boehmes@34994
  2049
#13897 := [rewrite]: #13896
boehmes@36900
  2050
#13893 := (iff #12162 #13892)
boehmes@36900
  2051
#13890 := (iff #3116 #13889)
boehmes@36900
  2052
#13891 := [rewrite]: #13890
boehmes@34994
  2053
#13894 := [monotonicity #13891]: #13893
boehmes@34994
  2054
#13899 := [trans #13894 #13897]: #13898
boehmes@34994
  2055
#13902 := [monotonicity #13899]: #13901
boehmes@36900
  2056
#14030 := [monotonicity #13902 #14027]: #14029
boehmes@36900
  2057
#13935 := (iff #13051 #13934)
boehmes@36900
  2058
#13932 := (iff #12156 #13931)
boehmes@36900
  2059
#13929 := (iff #12151 #13926)
boehmes@36900
  2060
#13920 := (or #13903 #13917)
boehmes@36900
  2061
#13923 := (or #5654 #13920)
boehmes@36900
  2062
#13927 := (iff #13923 #13926)
boehmes@36900
  2063
#13928 := [rewrite]: #13927
boehmes@36900
  2064
#13924 := (iff #12151 #13923)
boehmes@36900
  2065
#13921 := (iff #12145 #13920)
boehmes@36900
  2066
#13918 := (iff #3112 #13917)
boehmes@36900
  2067
#13919 := [rewrite]: #13918
boehmes@36900
  2068
#13913 := (iff #12144 #13903)
boehmes@36900
  2069
#13905 := (not #13903)
boehmes@36900
  2070
#13908 := (not #13905)
boehmes@36900
  2071
#13911 := (iff #13908 #13903)
boehmes@36900
  2072
#13912 := [rewrite]: #13911
boehmes@36900
  2073
#13909 := (iff #12144 #13908)
boehmes@36900
  2074
#13906 := (iff #3111 #13905)
boehmes@36900
  2075
#13907 := [rewrite]: #13906
boehmes@34994
  2076
#13910 := [monotonicity #13907]: #13909
boehmes@36900
  2077
#13914 := [trans #13910 #13912]: #13913
boehmes@36900
  2078
#13922 := [monotonicity #13914 #13919]: #13921
boehmes@36900
  2079
#13925 := [monotonicity #5656 #13922]: #13924
boehmes@36900
  2080
#13930 := [trans #13925 #13928]: #13929
boehmes@34994
  2081
#13933 := [quant-intro #13930]: #13932
boehmes@34994
  2082
#13936 := [monotonicity #13933]: #13935
boehmes@36900
  2083
#14033 := [monotonicity #13936 #14030]: #14032
boehmes@36900
  2084
#13941 := (iff #13060 #13940)
boehmes@36900
  2085
#13938 := (iff #3110 #13937)
boehmes@34994
  2086
#13939 := [rewrite]: #13938
boehmes@34994
  2087
#13942 := [monotonicity #13939]: #13941
boehmes@36900
  2088
#14036 := [monotonicity #13942 #14033]: #14035
boehmes@36900
  2089
#14039 := [monotonicity #13432 #14036]: #14038
boehmes@36900
  2090
#13953 := (iff #13077 #13952)
boehmes@36900
  2091
#13950 := (iff #3107 #13949)
boehmes@36900
  2092
#13947 := (iff #3106 #13946)
boehmes@36900
  2093
#13948 := [rewrite]: #13947
boehmes@36900
  2094
#13944 := (iff #3105 #13943)
boehmes@36900
  2095
#13945 := [rewrite]: #13944
boehmes@36900
  2096
#13951 := [monotonicity #13945 #13948]: #13950
boehmes@36900
  2097
#13954 := [monotonicity #13951]: #13953
boehmes@36900
  2098
#14042 := [monotonicity #13954 #14039]: #14041
boehmes@36900
  2099
#13963 := (iff #13086 #13962)
boehmes@36900
  2100
#13960 := (iff #3103 #13959)
boehmes@36900
  2101
#13957 := (iff #3102 #13955)
boehmes@34994
  2102
#13958 := [rewrite]: #13957
boehmes@36900
  2103
#13961 := [monotonicity #13423 #13958]: #13960
boehmes@36900
  2104
#13964 := [monotonicity #13961]: #13963
boehmes@36900
  2105
#14045 := [monotonicity #13964 #14042]: #14044
boehmes@36900
  2106
#13976 := (iff #13095 #13975)
boehmes@36900
  2107
#13973 := (iff #3099 #13972)
boehmes@36900
  2108
#13970 := (iff #3098 #13968)
boehmes@36900
  2109
#13971 := [rewrite]: #13970
boehmes@36900
  2110
#13966 := (iff #3097 #13965)
boehmes@36900
  2111
#13967 := [rewrite]: #13966
boehmes@36900
  2112
#13974 := [monotonicity #13967 #13971]: #13973
boehmes@36900
  2113
#13977 := [monotonicity #13974]: #13976
boehmes@36900
  2114
#14048 := [monotonicity #13977 #14045]: #14047
boehmes@36900
  2115
#13987 := (iff #13104 #13986)
boehmes@36900
  2116
#13984 := (iff #12138 #13981)
boehmes@36900
  2117
#13982 := (iff #13978 #13981)
boehmes@36900
  2118
#13983 := [rewrite]: #13982
boehmes@36900
  2119
#13979 := (iff #12138 #13978)
boehmes@36900
  2120
#13419 := (iff #3003 #13418)
boehmes@36900
  2121
#13420 := [rewrite]: #13419
boehmes@36900
  2122
#13980 := [monotonicity #13420]: #13979
boehmes@36900
  2123
#13985 := [trans #13980 #13983]: #13984
boehmes@34994
  2124
#13988 := [monotonicity #13985]: #13987
boehmes@36900
  2125
#14051 := [monotonicity #13988 #14048]: #14050
boehmes@36900
  2126
#14056 := [trans #14051 #14054]: #14055
boehmes@36900
  2127
#14059 := [monotonicity #13980 #14056]: #14058
boehmes@36900
  2128
#14064 := [trans #14059 #14062]: #14063
boehmes@36900
  2129
#13415 := (iff #13116 #13414)
boehmes@36900
  2130
#13412 := (iff #12133 #13411)
boehmes@36900
  2131
#13409 := (iff #12128 #13406)
boehmes@36900
  2132
#13400 := (or #13384 #13396)
boehmes@36900
  2133
#13403 := (or #5654 #13400)
boehmes@36900
  2134
#13407 := (iff #13403 #13406)
boehmes@36900
  2135
#13408 := [rewrite]: #13407
boehmes@36900
  2136
#13404 := (iff #12128 #13403)
boehmes@36900
  2137
#13401 := (iff #12122 #13400)
boehmes@36900
  2138
#13395 := (iff #3090 #13396)
boehmes@36900
  2139
#13399 := [rewrite]: #13395
boehmes@36900
  2140
#13393 := (iff #12121 #13384)
boehmes@36900
  2141
#13385 := (not #13384)
boehmes@36900
  2142
#13388 := (not #13385)
boehmes@36900
  2143
#13391 := (iff #13388 #13384)
boehmes@36900
  2144
#13392 := [rewrite]: #13391
boehmes@36900
  2145
#13389 := (iff #12121 #13388)
boehmes@36900
  2146
#13386 := (iff #3087 #13385)
boehmes@36900
  2147
#13387 := [rewrite]: #13386
boehmes@36900
  2148
#13390 := [monotonicity #13387]: #13389
boehmes@36900
  2149
#13394 := [trans #13390 #13392]: #13393
boehmes@36900
  2150
#13402 := [monotonicity #13394 #13399]: #13401
boehmes@36900
  2151
#13405 := [monotonicity #5656 #13402]: #13404
boehmes@36900
  2152
#13410 := [trans #13405 #13408]: #13409
boehmes@36900
  2153
#13413 := [quant-intro #13410]: #13412
boehmes@36900
  2154
#13416 := [monotonicity #13413]: #13415
boehmes@36900
  2155
#14067 := [monotonicity #13416 #14064]: #14066
boehmes@36900
  2156
#14070 := [monotonicity #13413 #14067]: #14069
boehmes@36900
  2157
#13382 := (iff #13128 #13381)
boehmes@36900
  2158
#13379 := (iff #3086 #13378)
boehmes@36900
  2159
#13380 := [rewrite]: #13379
boehmes@36900
  2160
#13383 := [monotonicity #13380]: #13382
boehmes@36900
  2161
#14073 := [monotonicity #13383 #14070]: #14072
boehmes@36900
  2162
#14076 := [monotonicity #13380 #14073]: #14075
boehmes@36900
  2163
#13376 := (iff #13140 false)
boehmes@36900
  2164
#12165 := (iff #3121 false)
boehmes@36900
  2165
#12166 := [rewrite]: #12165
boehmes@36900
  2166
#13374 := (iff #13140 #3121)
boehmes@36900
  2167
#13372 := (iff #12118 true)
boehmes@36900
  2168
#12477 := (and true true)
boehmes@36900
  2169
#13367 := (and true #12477)
boehmes@36900
  2170
#13370 := (iff #13367 true)
boehmes@36900
  2171
#13371 := [rewrite]: #13370
boehmes@36900
  2172
#13368 := (iff #12118 #13367)
boehmes@36900
  2173
#13365 := (iff #12115 #12477)
boehmes@36900
  2174
#13363 := (iff #3082 true)
boehmes@36900
  2175
#13364 := [rewrite]: #13363
boehmes@36900
  2176
#13361 := (iff #3081 true)
boehmes@36900
  2177
#13362 := [rewrite]: #13361
boehmes@36900
  2178
#13366 := [monotonicity #13362 #13364]: #13365
boehmes@36900
  2179
#13369 := [monotonicity #13362 #13366]: #13368
boehmes@36900
  2180
#13373 := [trans #13369 #13371]: #13372
boehmes@36900
  2181
#13375 := [monotonicity #13373]: #13374
boehmes@36900
  2182
#13377 := [trans #13375 #12166]: #13376
boehmes@36900
  2183
#14079 := [monotonicity #13377 #14076]: #14078
boehmes@36900
  2184
#14082 := [monotonicity #14079]: #14081
boehmes@36900
  2185
#14085 := [monotonicity #14082]: #14084
boehmes@36900
  2186
#14088 := [monotonicity #14085]: #14087
boehmes@36900
  2187
#14091 := [monotonicity #14088]: #14090
boehmes@36900
  2188
#14094 := [monotonicity #14091]: #14093
boehmes@36900
  2189
#14099 := [trans #14094 #14097]: #14098
boehmes@36900
  2190
#14102 := [monotonicity #14099]: #14101
boehmes@36900
  2191
#14107 := [trans #14102 #14105]: #14106
boehmes@36900
  2192
#14110 := [monotonicity #14107]: #14109
boehmes@36900
  2193
#14113 := [monotonicity #14110]: #14112
boehmes@36900
  2194
#14118 := [trans #14113 #14116]: #14117
boehmes@36900
  2195
#14121 := [monotonicity #14118]: #14120
boehmes@36900
  2196
#14124 := [monotonicity #14121]: #14123
boehmes@36900
  2197
#13359 := (iff #13221 #13358)
boehmes@36900
  2198
#13356 := (iff #3059 #13355)
boehmes@36900
  2199
#13353 := (iff #3058 #13350)
boehmes@36900
  2200
#13354 := [rewrite]: #13353
boehmes@36900
  2201
#13347 := (iff #3057 #13348)
boehmes@36900
  2202
#13349 := [rewrite]: #13347
boehmes@36900
  2203
#13357 := [monotonicity #13349 #13354]: #13356
boehmes@36900
  2204
#13360 := [monotonicity #13357]: #13359
boehmes@36900
  2205
#14205 := [monotonicity #13360 #14124]: #14204
boehmes@36900
  2206
#14208 := [monotonicity #14205]: #14207
boehmes@36900
  2207
#14211 := [monotonicity #14208]: #14210
boehmes@36900
  2208
#14214 := [monotonicity #14211]: #14213
boehmes@36900
  2209
#14217 := [monotonicity #14214]: #14216
boehmes@36900
  2210
#14135 := (iff #13266 #14134)
boehmes@36900
  2211
#14132 := (iff #3040 #14131)
boehmes@36900
  2212
#14129 := (iff #3039 #14125)
boehmes@36900
  2213
#14130 := [rewrite]: #14129
boehmes@36900
  2214
#14133 := [quant-intro #14130]: #14132
boehmes@36900
  2215
#14136 := [monotonicity #14133]: #14135
boehmes@36900
  2216
#14220 := [monotonicity #14136 #14217]: #14219
boehmes@36900
  2217
#14223 := [monotonicity #14220]: #14222
boehmes@36900
  2218
#14226 := [monotonicity #14223]: #14225
boehmes@36900
  2219
#14141 := (iff #13293 #14140)
boehmes@36900
  2220
#14138 := (iff #12045 #14137)
boehmes@36900
  2221
#14139 := [rewrite]: #14138
boehmes@36900
  2222
#14142 := [monotonicity #14139]: #14141
boehmes@36900
  2223
#14229 := [monotonicity #14142 #14226]: #14228
boehmes@36900
  2224
#14148 := (iff #13302 #13417)
boehmes@36900
  2225
#14143 := (not #13418)
boehmes@36900
  2226
#14146 := (iff #14143 #13417)
boehmes@36900
  2227
#14147 := [rewrite]: #14146
boehmes@36900
  2228
#14144 := (iff #13302 #14143)
boehmes@36900
  2229
#14145 := [monotonicity #13420]: #14144
boehmes@36900
  2230
#14149 := [trans #14145 #14147]: #14148
boehmes@36900
  2231
#14232 := [monotonicity #14149 #14229]: #14231
boehmes@36900
  2232
#14159 := (iff #13311 #14150)
boehmes@36900
  2233
#14151 := (not #14150)
boehmes@36900
  2234
#14154 := (not #14151)
boehmes@36900
  2235
#14157 := (iff #14154 #14150)
boehmes@36900
  2236
#14158 := [rewrite]: #14157
boehmes@36900
  2237
#14155 := (iff #13311 #14154)
boehmes@36900
  2238
#14152 := (iff #3002 #14151)
boehmes@36900
  2239
#14153 := [rewrite]: #14152
boehmes@36900
  2240
#14156 := [monotonicity #14153]: #14155
boehmes@36900
  2241
#14160 := [trans #14156 #14158]: #14159
boehmes@36900
  2242
#14235 := [monotonicity #14160 #14232]: #14234
boehmes@36900
  2243
#14173 := (iff #13320 #14172)
boehmes@36900
  2244
#14170 := (iff #3000 #14169)
boehmes@36900
  2245
#14167 := (iff #2999 #14164)
boehmes@36900
  2246
#14168 := [rewrite]: #14167
boehmes@36900
  2247
#14161 := (iff #2998 #14162)
boehmes@36900
  2248
#14163 := [rewrite]: #14161
boehmes@36900
  2249
#14171 := [monotonicity #14163 #14168]: #14170
boehmes@36900
  2250
#14174 := [monotonicity #14171]: #14173
boehmes@36900
  2251
#14238 := [monotonicity #14174 #14235]: #14237
boehmes@36900
  2252
#14187 := (iff #13329 #14186)
boehmes@36900
  2253
#14184 := (iff #2996 #14183)
boehmes@36900
  2254
#14181 := (iff #2995 #14178)
boehmes@36900
  2255
#14182 := [rewrite]: #14181
boehmes@36900
  2256
#14175 := (iff #2994 #14176)
boehmes@36900
  2257
#14177 := [rewrite]: #14175
boehmes@36900
  2258
#14185 := [monotonicity #14177 #14182]: #14184
boehmes@36900
  2259
#14188 := [monotonicity #14185]: #14187
boehmes@36900
  2260
#14241 := [monotonicity #14188 #14238]: #14240
boehmes@36900
  2261
#14201 := (iff #13338 #14200)
boehmes@36900
  2262
#14198 := (iff #2992 #14197)
boehmes@36900
  2263
#14195 := (iff #2991 #14192)
boehmes@36900
  2264
#14196 := [rewrite]: #14195
boehmes@36900
  2265
#14189 := (iff #2990 #14190)
boehmes@36900
  2266
#14191 := [rewrite]: #14189
boehmes@36900
  2267
#14199 := [monotonicity #14191 #14196]: #14198
boehmes@36900
  2268
#14202 := [monotonicity #14199]: #14201
boehmes@36900
  2269
#14244 := [monotonicity #14202 #14241]: #14243
boehmes@36900
  2270
#14249 := [trans #14244 #14247]: #14248
boehmes@36900
  2271
#14252 := [monotonicity #14249]: #14251
boehmes@36900
  2272
#13345 := (iff #3371 #13344)
boehmes@36900
  2273
#13342 := (iff #3370 #13339)
boehmes@36900
  2274
#13335 := (implies #2992 #13330)
boehmes@36900
  2275
#13340 := (iff #13335 #13339)
boehmes@36900
  2276
#13341 := [rewrite]: #13340
boehmes@36900
  2277
#13336 := (iff #3370 #13335)
boehmes@36900
  2278
#13333 := (iff #3369 #13330)
boehmes@36900
  2279
#13326 := (implies #2996 #13321)
boehmes@36900
  2280
#13331 := (iff #13326 #13330)
boehmes@36900
  2281
#13332 := [rewrite]: #13331
boehmes@36900
  2282
#13327 := (iff #3369 #13326)
boehmes@36900
  2283
#13324 := (iff #3368 #13321)
boehmes@36900
  2284
#13317 := (implies #3000 #13312)
boehmes@36900
  2285
#13322 := (iff #13317 #13321)
boehmes@36900
  2286
#13323 := [rewrite]: #13322
boehmes@36900
  2287
#13318 := (iff #3368 #13317)
boehmes@36900
  2288
#13315 := (iff #3367 #13312)
boehmes@36900
  2289
#13308 := (implies #3002 #13303)
boehmes@36900
  2290
#13313 := (iff #13308 #13312)
boehmes@36900
  2291
#13314 := [rewrite]: #13313
boehmes@36900
  2292
#13309 := (iff #3367 #13308)
boehmes@36900
  2293
#13306 := (iff #3366 #13303)
boehmes@36900
  2294
#13299 := (implies #3003 #13294)
boehmes@36900
  2295
#13304 := (iff #13299 #13303)
boehmes@36900
  2296
#13305 := [rewrite]: #13304
boehmes@36900
  2297
#13300 := (iff #3366 #13299)
boehmes@36900
  2298
#13297 := (iff #3365 #13294)
boehmes@36900
  2299
#13290 := (implies #12045 #13285)
boehmes@36900
  2300
#13295 := (iff #13290 #13294)
boehmes@36900
  2301
#13296 := [rewrite]: #13295
boehmes@36900
  2302
#13291 := (iff #3365 #13290)
boehmes@36900
  2303
#13288 := (iff #3364 #13285)
boehmes@36900
  2304
#13281 := (implies #12048 #13276)
boehmes@36900
  2305
#13286 := (iff #13281 #13285)
boehmes@36900
  2306
#13287 := [rewrite]: #13286
boehmes@36900
  2307
#13282 := (iff #3364 #13281)
boehmes@36900
  2308
#13279 := (iff #3363 #13276)
boehmes@36900
  2309
#13272 := (implies #12057 #13267)
boehmes@36900
  2310
#13277 := (iff #13272 #13276)
boehmes@36900
  2311
#13278 := [rewrite]: #13277
boehmes@36900
  2312
#13273 := (iff #3363 #13272)
boehmes@36900
  2313
#13270 := (iff #3362 #13267)
boehmes@36900
  2314
#13263 := (implies #3040 #13258)
boehmes@36900
  2315
#13268 := (iff #13263 #13267)
boehmes@36900
  2316
#13269 := [rewrite]: #13268
boehmes@36900
  2317
#13264 := (iff #3362 #13263)
boehmes@36900
  2318
#13261 := (iff #3361 #13258)
boehmes@36900
  2319
#13254 := (implies #12066 #13249)
boehmes@36900
  2320
#13259 := (iff #13254 #13258)
boehmes@36900
  2321
#13260 := [rewrite]: #13259
boehmes@36900
  2322
#13255 := (iff #3361 #13254)
boehmes@36900
  2323
#13252 := (iff #3360 #13249)
boehmes@36900
  2324
#13245 := (implies #12069 #13240)
boehmes@36900
  2325
#13250 := (iff #13245 #13249)
boehmes@36900
  2326
#13251 := [rewrite]: #13250
boehmes@36900
  2327
#13246 := (iff #3360 #13245)
boehmes@36900
  2328
#13243 := (iff #3359 #13240)
boehmes@36900
  2329
#13236 := (implies #3051 #13231)
boehmes@36900
  2330
#13241 := (iff #13236 #13240)
boehmes@36900
  2331
#13242 := [rewrite]: #13241
boehmes@36900
  2332
#13237 := (iff #3359 #13236)
boehmes@36900
  2333
#13234 := (iff #3358 #13231)
boehmes@36900
  2334
#13227 := (implies #12083 #13222)
boehmes@36900
  2335
#13232 := (iff #13227 #13231)
boehmes@36900
  2336
#13233 := [rewrite]: #13232
boehmes@36900
  2337
#13228 := (iff #3358 #13227)
boehmes@36900
  2338
#13225 := (iff #3357 #13222)
boehmes@36900
  2339
#13218 := (implies #3059 #13215)
boehmes@36900
  2340
#13223 := (iff #13218 #13222)
boehmes@36900
  2341
#13224 := [rewrite]: #13223
boehmes@36900
  2342
#13219 := (iff #3357 #13218)
boehmes@36900
  2343
#13216 := (iff #3356 #13215)
boehmes@36900
  2344
#13213 := (iff #3355 #13210)
boehmes@36900
  2345
#13206 := (implies #12086 #13203)
boehmes@36900
  2346
#13211 := (iff #13206 #13210)
boehmes@36900
  2347
#13212 := [rewrite]: #13211
boehmes@36900
  2348
#13207 := (iff #3355 #13206)
boehmes@36900
  2349
#13204 := (iff #3354 #13203)
boehmes@36900
  2350
#13201 := (iff #3353 #13198)
boehmes@36900
  2351
#13194 := (implies #12095 #13191)
boehmes@36900
  2352
#13199 := (iff #13194 #13198)
boehmes@36900
  2353
#13200 := [rewrite]: #13199
boehmes@36900
  2354
#13195 := (iff #3353 #13194)
boehmes@36900
  2355
#13192 := (iff #3352 #13191)
boehmes@36900
  2356
#13189 := (iff #3351 #13186)
boehmes@36900
  2357
#13182 := (implies #12101 #13177)
boehmes@36900
  2358
#13187 := (iff #13182 #13186)
boehmes@36900
  2359
#13188 := [rewrite]: #13187
boehmes@36900
  2360
#13183 := (iff #3351 #13182)
boehmes@36900
  2361
#13180 := (iff #3350 #13177)
boehmes@36900
  2362
#13173 := (implies #3074 #13168)
boehmes@36900
  2363
#13178 := (iff #13173 #13177)
boehmes@36900
  2364
#13179 := [rewrite]: #13178
boehmes@36900
  2365
#13174 := (iff #3350 #13173)
boehmes@36900
  2366
#13171 := (iff #3349 #13168)
boehmes@36900
  2367
#13164 := (implies #12104 #13159)
boehmes@36900
  2368
#13169 := (iff #13164 #13168)
boehmes@36900
  2369
#13170 := [rewrite]: #13169
boehmes@36900
  2370
#13165 := (iff #3349 #13164)
boehmes@36900
  2371
#13162 := (iff #3348 #13159)
boehmes@36900
  2372
#13155 := (implies #12107 #13150)
boehmes@36900
  2373
#13160 := (iff #13155 #13159)
boehmes@36900
  2374
#13161 := [rewrite]: #13160
boehmes@36900
  2375
#13156 := (iff #3348 #13155)
boehmes@36900
  2376
#13153 := (iff #3347 #13150)
boehmes@36900
  2377
#13146 := (implies #12110 #13141)
boehmes@36900
  2378
#13151 := (iff #13146 #13150)
boehmes@36900
  2379
#13152 := [rewrite]: #13151
boehmes@36900
  2380
#13147 := (iff #3347 #13146)
boehmes@36900
  2381
#13144 := (iff #3346 #13141)
boehmes@36900
  2382
#13137 := (implies #12118 #13134)
boehmes@36900
  2383
#13142 := (iff #13137 #13141)
boehmes@36900
  2384
#13143 := [rewrite]: #13142
boehmes@36900
  2385
#13138 := (iff #3346 #13137)
boehmes@36900
  2386
#13135 := (iff #3345 #13134)
boehmes@36900
  2387
#13132 := (iff #3344 #13129)
boehmes@36900
  2388
#13125 := (implies #3086 #13122)
boehmes@36900
  2389
#13130 := (iff #13125 #13129)
boehmes@36900
  2390
#13131 := [rewrite]: #13130
boehmes@36900
  2391
#13126 := (iff #3344 #13125)
boehmes@36900
  2392
#13123 := (iff #3343 #13122)
boehmes@36900
  2393
#13120 := (iff #3342 #13117)
boehmes@36900
  2394
#13113 := (implies #12133 #13110)
boehmes@36900
  2395
#13118 := (iff #13113 #13117)
boehmes@36900
  2396
#13119 := [rewrite]: #13118
boehmes@36900
  2397
#13114 := (iff #3342 #13113)
boehmes@36900
  2398
#13111 := (iff #3341 #13110)
boehmes@36900
  2399
#13108 := (iff #3340 #13105)
boehmes@36900
  2400
#13101 := (implies #12138 #13096)
boehmes@36900
  2401
#13106 := (iff #13101 #13105)
boehmes@36900
  2402
#13107 := [rewrite]: #13106
boehmes@36900
  2403
#13102 := (iff #3340 #13101)
boehmes@36900
  2404
#13099 := (iff #3339 #13096)
boehmes@36900
  2405
#13092 := (implies #3099 #13087)
boehmes@36900
  2406
#13097 := (iff #13092 #13096)
boehmes@36900
  2407
#13098 := [rewrite]: #13097
boehmes@36900
  2408
#13093 := (iff #3339 #13092)
boehmes@36900
  2409
#13090 := (iff #3338 #13087)
boehmes@36900
  2410
#13083 := (implies #3103 #13078)
boehmes@36900
  2411
#13088 := (iff #13083 #13087)
boehmes@36900
  2412
#13089 := [rewrite]: #13088
boehmes@36900
  2413
#13084 := (iff #3338 #13083)
boehmes@36900
  2414
#13081 := (iff #3337 #13078)
boehmes@36900
  2415
#13074 := (implies #3107 #13069)
boehmes@36900
  2416
#13079 := (iff #13074 #13078)
boehmes@36900
  2417
#13080 := [rewrite]: #13079
boehmes@36900
  2418
#13075 := (iff #3337 #13074)
boehmes@36900
  2419
#13072 := (iff #3336 #13069)
boehmes@36900
  2420
#13066 := (implies #12141 #13061)
boehmes@36900
  2421
#13070 := (iff #13066 #13069)
boehmes@36900
  2422
#13071 := [rewrite]: #13070
boehmes@36900
  2423
#13067 := (iff #3336 #13066)
boehmes@36900
  2424
#13064 := (iff #3335 #13061)
boehmes@36900
  2425
#13057 := (implies #3110 #13052)
boehmes@36900
  2426
#13062 := (iff #13057 #13061)
boehmes@36900
  2427
#13063 := [rewrite]: #13062
boehmes@36900
  2428
#13058 := (iff #3335 #13057)
boehmes@36900
  2429
#13055 := (iff #3334 #13052)
boehmes@36900
  2430
#13048 := (implies #12156 #13043)
boehmes@36900
  2431
#13053 := (iff #13048 #13052)
boehmes@36900
  2432
#13054 := [rewrite]: #13053
boehmes@36900
  2433
#13049 := (iff #3334 #13048)
boehmes@36900
  2434
#13046 := (iff #3333 #13043)
boehmes@36900
  2435
#13039 := (implies #12162 #13034)
boehmes@36900
  2436
#13044 := (iff #13039 #13043)
boehmes@36900
  2437
#13045 := [rewrite]: #13044
boehmes@36900
  2438
#13040 := (iff #3333 #13039)
boehmes@36900
  2439
#13037 := (iff #3332 #13034)
boehmes@36900
  2440
#13031 := (implies #12141 #13019)
boehmes@36900
  2441
#13035 := (iff #13031 #13034)
boehmes@36900
  2442
#13036 := [rewrite]: #13035
boehmes@36900
  2443
#13032 := (iff #3332 #13031)
boehmes@36900
  2444
#13029 := (iff #3331 #13019)
boehmes@36900
  2445
#13024 := (and true #13019)
boehmes@36900
  2446
#13027 := (iff #13024 #13019)
boehmes@36900
  2447
#13028 := [rewrite]: #13027
boehmes@36900
  2448
#13025 := (iff #3331 #13024)
boehmes@36900
  2449
#13022 := (iff #3330 #13019)
boehmes@36900
  2450
#13016 := (implies #12141 #13011)
boehmes@36900
  2451
#13020 := (iff #13016 #13019)
boehmes@36900
  2452
#13021 := [rewrite]: #13020
boehmes@36900
  2453
#13017 := (iff #3330 #13016)
boehmes@36900
  2454
#13014 := (iff #3329 #13011)
boehmes@36900
  2455
#13008 := (implies #12141 #13003)
boehmes@36900
  2456
#13012 := (iff #13008 #13011)
boehmes@36900
  2457
#13013 := [rewrite]: #13012
boehmes@36900
  2458
#13009 := (iff #3329 #13008)
boehmes@36900
  2459
#13006 := (iff #3328 #13003)
boehmes@36900
  2460
#13000 := (implies #12141 #12995)
boehmes@36900
  2461
#13004 := (iff #13000 #13003)
boehmes@36900
  2462
#13005 := [rewrite]: #13004
boehmes@36900
  2463
#13001 := (iff #3328 #13000)
boehmes@36900
  2464
#12998 := (iff #3327 #12995)
boehmes@36900
  2465
#12992 := (implies #12430 #12987)
boehmes@36900
  2466
#12996 := (iff #12992 #12995)
boehmes@36900
  2467
#12997 := [rewrite]: #12996
boehmes@36900
  2468
#12993 := (iff #3327 #12992)
boehmes@36900
  2469
#12990 := (iff #3326 #12987)
boehmes@36900
  2470
#12983 := (implies #12430 #12978)
boehmes@36900
  2471
#12988 := (iff #12983 #12987)
boehmes@36900
  2472
#12989 := [rewrite]: #12988
boehmes@36900
  2473
#12984 := (iff #3326 #12983)
boehmes@36900
  2474
#12981 := (iff #3325 #12978)
boehmes@36900
  2475
#12975 := (implies #12173 #12970)
boehmes@36900
  2476
#12979 := (iff #12975 #12978)
boehmes@36900
  2477
#12980 := [rewrite]: #12979
boehmes@36900
  2478
#12976 := (iff #3325 #12975)
boehmes@36900
  2479
#12973 := (iff #3324 #12970)
boehmes@36900
  2480
#12966 := (implies #12452 #12961)
boehmes@36900
  2481
#12971 := (iff #12966 #12970)
boehmes@36900
  2482
#12972 := [rewrite]: #12971
boehmes@36900
  2483
#12967 := (iff #3324 #12966)
boehmes@36900
  2484
#12964 := (iff #3323 #12961)
boehmes@36900
  2485
#12957 := (implies #12455 #12952)
boehmes@36900
  2486
#12962 := (iff #12957 #12961)
boehmes@36900
  2487
#12963 := [rewrite]: #12962
boehmes@36900
  2488
#12958 := (iff #3323 #12957)
boehmes@36900
  2489
#12955 := (iff #3322 #12952)
boehmes@36900
  2490
#12948 := (implies #12458 #12943)
boehmes@36900
  2491
#12953 := (iff #12948 #12952)
boehmes@36900
  2492
#12954 := [rewrite]: #12953
boehmes@36900
  2493
#12949 := (iff #3322 #12948)
boehmes@36900
  2494
#12946 := (iff #3321 #12943)
boehmes@36900
  2495
#12939 := (implies #12461 #12934)
boehmes@36900
  2496
#12944 := (iff #12939 #12943)
boehmes@36900
  2497
#12945 := [rewrite]: #12944
boehmes@36900
  2498
#12940 := (iff #3321 #12939)
boehmes@36900
  2499
#12937 := (iff #3320 #12934)
boehmes@36900
  2500
#12930 := (implies #12470 #12918)
boehmes@36900
  2501
#12935 := (iff #12930 #12934)
boehmes@36900
  2502
#12936 := [rewrite]: #12935
boehmes@36900
  2503
#12931 := (iff #3320 #12930)
boehmes@36900
  2504
#12928 := (iff #3319 #12918)
boehmes@36900
  2505
#12923 := (implies true #12918)
boehmes@36900
  2506
#12926 := (iff #12923 #12918)
boehmes@36900
  2507
#12927 := [rewrite]: #12926
boehmes@36900
  2508
#12924 := (iff #3319 #12923)
boehmes@36900
  2509
#12921 := (iff #3318 #12918)
boehmes@36900
  2510
#12915 := (implies #12141 #12912)
boehmes@36900
  2511
#12919 := (iff #12915 #12918)
boehmes@36900
  2512
#12920 := [rewrite]: #12919
boehmes@36900
  2513
#12916 := (iff #3318 #12915)
boehmes@36900
  2514
#12913 := (iff #3317 #12912)
boehmes@36900
  2515
#12910 := (iff #3316 #12907)
boehmes@36900
  2516
#12904 := (implies #12141 #12899)
boehmes@36900
  2517
#12908 := (iff #12904 #12907)
boehmes@36900
  2518
#12909 := [rewrite]: #12908
boehmes@36900
  2519
#12905 := (iff #3316 #12904)
boehmes@36900
  2520
#12902 := (iff #3315 #12899)
boehmes@36900
  2521
#12895 := (implies #3312 #12890)
boehmes@36900
  2522
#12900 := (iff #12895 #12899)
boehmes@36900
  2523
#12901 := [rewrite]: #12900
boehmes@36900
  2524
#12896 := (iff #3315 #12895)
boehmes@36900
  2525
#12893 := (iff #3314 #12890)
boehmes@36900
  2526
#12887 := (implies #12141 #12882)
boehmes@36900
  2527
#12891 := (iff #12887 #12890)
boehmes@36900
  2528
#12892 := [rewrite]: #12891
boehmes@36900
  2529
#12888 := (iff #3314 #12887)
boehmes@36900
  2530
#12885 := (iff #3313 #12882)
boehmes@36900
  2531
#12879 := (implies #12141 #12303)
boehmes@36900
  2532
#12883 := (iff #12879 #12882)
boehmes@36900
  2533
#12884 := [rewrite]: #12883
boehmes@36900
  2534
#12880 := (iff #3313 #12879)
boehmes@36900
  2535
#12306 := (iff #3156 #12303)
boehmes@36900
  2536
#12300 := (implies #12141 #12295)
boehmes@36900
  2537
#12304 := (iff #12300 #12303)
boehmes@36900
  2538
#12305 := [rewrite]: #12304
boehmes@36900
  2539
#12301 := (iff #3156 #12300)
boehmes@36900
  2540
#12298 := (iff #3155 #12295)
boehmes@36900
  2541
#12292 := (implies #12141 #12289)
boehmes@36900
  2542
#12296 := (iff #12292 #12295)
boehmes@36900
  2543
#12297 := [rewrite]: #12296
boehmes@36900
  2544
#12293 := (iff #3155 #12292)
boehmes@36900
  2545
#12290 := (iff #3154 #12289)
boehmes@36900
  2546
#12287 := (iff #3153 #12284)
boehmes@36900
  2547
#12280 := (implies #10869 #12275)
boehmes@36900
  2548
#12285 := (iff #12280 #12284)
boehmes@36900
  2549
#12286 := [rewrite]: #12285
boehmes@36900
  2550
#12281 := (iff #3153 #12280)
boehmes@36900
  2551
#12278 := (iff #3152 #12275)
boehmes@36900
  2552
#12272 := (implies #12141 #12267)
boehmes@36900
  2553
#12276 := (iff #12272 #12275)
boehmes@36900
  2554
#12277 := [rewrite]: #12276
boehmes@36900
  2555
#12273 := (iff #3152 #12272)
boehmes@36900
  2556
#12270 := (iff #3151 #12267)
boehmes@36900
  2557
#12264 := (implies #12141 #12259)
boehmes@36900
  2558
#12268 := (iff #12264 #12267)
boehmes@36900
  2559
#12269 := [rewrite]: #12268
boehmes@36900
  2560
#12265 := (iff #3151 #12264)
boehmes@36900
  2561
#12262 := (iff #3150 #12259)
boehmes@36900
  2562
#12255 := (implies #12141 #12250)
boehmes@36900
  2563
#12260 := (iff #12255 #12259)
boehmes@36900
  2564
#12261 := [rewrite]: #12260
boehmes@36900
  2565
#12256 := (iff #3150 #12255)
boehmes@36900
  2566
#12253 := (iff #3149 #12250)
boehmes@36900
  2567
#12246 := (implies #12178 #12241)
boehmes@36900
  2568
#12251 := (iff #12246 #12250)
boehmes@36900
  2569
#12252 := [rewrite]: #12251
boehmes@36900
  2570
#12247 := (iff #3149 #12246)
boehmes@36900
  2571
#12244 := (iff #3148 #12241)
boehmes@36900
  2572
#12237 := (implies #12181 #12232)
boehmes@36900
  2573
#12242 := (iff #12237 #12241)
boehmes@36900
  2574
#12243 := [rewrite]: #12242
boehmes@36900
  2575
#12238 := (iff #3148 #12237)
boehmes@36900
  2576
#12235 := (iff #3147 #12232)
boehmes@36900
  2577
#12228 := (implies #12184 #12223)
boehmes@36900
  2578
#12233 := (iff #12228 #12232)
boehmes@36900
  2579
#12234 := [rewrite]: #12233
boehmes@36900
  2580
#12229 := (iff #3147 #12228)
boehmes@36900
  2581
#12226 := (iff #3146 #12223)
boehmes@36900
  2582
#12219 := (implies #12187 #12216)
boehmes@36900
  2583
#12224 := (iff #12219 #12223)
boehmes@36900
  2584
#12225 := [rewrite]: #12224
boehmes@36900
  2585
#12220 := (iff #3146 #12219)
boehmes@36900
  2586
#12217 := (iff #3145 #12216)
boehmes@36900
  2587
#12214 := (iff #3144 #12211)
boehmes@36900
  2588
#12207 := (implies #12202 #3142)
boehmes@36900
  2589
#12212 := (iff #12207 #12211)
boehmes@36900
  2590
#12213 := [rewrite]: #12212
boehmes@36900
  2591
#12208 := (iff #3144 #12207)
boehmes@36900
  2592
#12205 := (iff #3143 #3142)
boehmes@36900
  2593
#12206 := [rewrite]: #12205
boehmes@36900
  2594
#12203 := (iff #3137 #12202)
boehmes@36900
  2595
#12200 := (iff #3136 #12197)
boehmes@36900
  2596
#12194 := (implies #421 #12191)
boehmes@36900
  2597
#12198 := (iff #12194 #12197)
boehmes@36900
  2598
#12199 := [rewrite]: #12198
boehmes@36900
  2599
#12195 := (iff #3136 #12194)
boehmes@36900
  2600
#12192 := (iff #3135 #12191)
boehmes@36900
  2601
#12193 := [rewrite]: #12192
boehmes@36900
  2602
#12196 := [monotonicity #12193]: #12195
boehmes@36900
  2603
#12201 := [trans #12196 #12199]: #12200
boehmes@36900
  2604
#12204 := [quant-intro #12201]: #12203
boehmes@36900
  2605
#12209 := [monotonicity #12204 #12206]: #12208
boehmes@36900
  2606
#12215 := [trans #12209 #12213]: #12214
boehmes@36900
  2607
#12218 := [monotonicity #12204 #12215]: #12217
boehmes@36900
  2608
#12188 := (iff #3132 #12187)
boehmes@36900
  2609
#12189 := [rewrite]: #12188
boehmes@36900
  2610
#12221 := [monotonicity #12189 #12218]: #12220
boehmes@36900
  2611
#12227 := [trans #12221 #12225]: #12226
boehmes@36900
  2612
#12185 := (iff #3130 #12184)
boehmes@36900
  2613
#12186 := [rewrite]: #12185
boehmes@36900
  2614
#12230 := [monotonicity #12186 #12227]: #12229
boehmes@36900
  2615
#12236 := [trans #12230 #12234]: #12235
boehmes@36900
  2616
#12182 := (iff #3128 #12181)
boehmes@36900
  2617
#12183 := [rewrite]: #12182
boehmes@36900
  2618
#12239 := [monotonicity #12183 #12236]: #12238
boehmes@36900
  2619
#12245 := [trans #12239 #12243]: #12244
boehmes@36900
  2620
#12179 := (iff #3126 #12178)
boehmes@36900
  2621
#12180 := [rewrite]: #12179
boehmes@36900
  2622
#12248 := [monotonicity #12180 #12245]: #12247
boehmes@36900
  2623
#12254 := [trans #12248 #12252]: #12253
boehmes@36900
  2624
#12142 := (iff #3109 #12141)
boehmes@36900
  2625
#12143 := [rewrite]: #12142
boehmes@36900
  2626
#12257 := [monotonicity #12143 #12254]: #12256
boehmes@36900
  2627
#12263 := [trans #12257 #12261]: #12262
boehmes@36900
  2628
#12266 := [monotonicity #12143 #12263]: #12265
boehmes@36900
  2629
#12271 := [trans #12266 #12269]: #12270
boehmes@36900
  2630
#12274 := [monotonicity #12143 #12271]: #12273
boehmes@36900
  2631
#12279 := [trans #12274 #12277]: #12278
boehmes@36900
  2632
#10871 := (iff #2507 #10869)
boehmes@36900
  2633
#10872 := [rewrite]: #10871
boehmes@36900
  2634
#12282 := [monotonicity #10872 #12279]: #12281
boehmes@36900
  2635
#12288 := [trans #12282 #12286]: #12287
boehmes@36900
  2636
#12291 := [monotonicity #10872 #12288]: #12290
boehmes@36900
  2637
#12294 := [monotonicity #12143 #12291]: #12293
boehmes@36900
  2638
#12299 := [trans #12294 #12297]: #12298
boehmes@36900
  2639
#12302 := [monotonicity #12143 #12299]: #12301
boehmes@36900
  2640
#12307 := [trans #12302 #12305]: #12306
boehmes@36900
  2641
#12881 := [monotonicity #12143 #12307]: #12880
boehmes@36900
  2642
#12886 := [trans #12881 #12884]: #12885
boehmes@36900
  2643
#12889 := [monotonicity #12143 #12886]: #12888
boehmes@36900
  2644
#12894 := [trans #12889 #12892]: #12893
boehmes@36900
  2645
#12897 := [monotonicity #12894]: #12896
boehmes@36900
  2646
#12903 := [trans #12897 #12901]: #12902
boehmes@36900
  2647
#12906 := [monotonicity #12143 #12903]: #12905
boehmes@36900
  2648
#12911 := [trans #12906 #12909]: #12910
boehmes@36900
  2649
#12877 := (iff #3311 #12874)
boehmes@36900
  2650
#12871 := (implies #12141 #12866)
boehmes@36900
  2651
#12875 := (iff #12871 #12874)
boehmes@36900
  2652
#12876 := [rewrite]: #12875
boehmes@36900
  2653
#12872 := (iff #3311 #12871)
boehmes@36900
  2654
#12869 := (iff #3310 #12866)
boehmes@36900
  2655
#12862 := (implies #3221 #12857)
boehmes@36900
  2656
#12867 := (iff #12862 #12866)
boehmes@36900
  2657
#12868 := [rewrite]: #12867
boehmes@36900
  2658
#12863 := (iff #3310 #12862)
boehmes@36900
  2659
#12860 := (iff #3309 #12857)
boehmes@36900
  2660
#12854 := (implies #12141 #12849)
boehmes@36900
  2661
#12858 := (iff #12854 #12857)
boehmes@36900
  2662
#12859 := [rewrite]: #12858
boehmes@36900
  2663
#12855 := (iff #3309 #12854)
boehmes@36900
  2664
#12852 := (iff #3308 #12849)
boehmes@36900
  2665
#12846 := (implies #12141 #12843)
boehmes@36900
  2666
#12850 := (iff #12846 #12849)
boehmes@36900
  2667
#12851 := [rewrite]: #12850
boehmes@36900
  2668
#12847 := (iff #3308 #12846)
boehmes@36900
  2669
#12844 := (iff #3307 #12843)
boehmes@36900
  2670
#12841 := (iff #3306 #12838)
boehmes@36900
  2671
#12835 := (implies #12490 #12832)
boehmes@36900
  2672
#12839 := (iff #12835 #12838)
boehmes@36900
  2673
#12840 := [rewrite]: #12839
boehmes@36900
  2674
#12836 := (iff #3306 #12835)
boehmes@36900
  2675
#12833 := (iff #3305 #12832)
boehmes@36900 <