src/HOL/Multivariate_Analysis/Integration.cert
author hoelzl
Mon Feb 22 20:41:49 2010 +0100 (2010-02-22)
changeset 35292 e4a431b6d9b7
parent 35291 src/HOL/Multivariate_Analysis/Integration_MV.cert@ead7bfc30b26
child 35730 3167079f4cd1
permissions -rw-r--r--
Replaced Integration by Multivariate-Analysis/Real_Integration
himmelma@35172
     1
tB2Atlor9W4pSnrAz5nHpw 907 0
himmelma@35172
     2
#2 := false
himmelma@35172
     3
#299 := 0::real
himmelma@35172
     4
decl uf_1 :: (-> T3 T2 real)
himmelma@35172
     5
decl uf_10 :: (-> T4 T2)
himmelma@35172
     6
decl uf_7 :: T4
himmelma@35172
     7
#15 := uf_7
himmelma@35172
     8
#22 := (uf_10 uf_7)
himmelma@35172
     9
decl uf_2 :: (-> T1 T3)
himmelma@35172
    10
decl uf_4 :: T1
himmelma@35172
    11
#11 := uf_4
himmelma@35172
    12
#91 := (uf_2 uf_4)
himmelma@35172
    13
#902 := (uf_1 #91 #22)
himmelma@35172
    14
#297 := -1::real
himmelma@35172
    15
#1084 := (* -1::real #902)
himmelma@35172
    16
decl uf_16 :: T1
himmelma@35172
    17
#50 := uf_16
himmelma@35172
    18
#78 := (uf_2 uf_16)
himmelma@35172
    19
#799 := (uf_1 #78 #22)
himmelma@35172
    20
#1267 := (+ #799 #1084)
himmelma@35172
    21
#1272 := (>= #1267 0::real)
himmelma@35172
    22
#1266 := (= #799 #902)
himmelma@35172
    23
decl uf_9 :: T3
himmelma@35172
    24
#21 := uf_9
himmelma@35172
    25
#23 := (uf_1 uf_9 #22)
himmelma@35172
    26
#905 := (= #23 #902)
himmelma@35172
    27
decl uf_11 :: T3
himmelma@35172
    28
#24 := uf_11
himmelma@35172
    29
#850 := (uf_1 uf_11 #22)
himmelma@35172
    30
#904 := (= #850 #902)
himmelma@35172
    31
decl uf_6 :: (-> T2 T4)
himmelma@35172
    32
#74 := (uf_6 #22)
himmelma@35172
    33
#281 := (= uf_7 #74)
himmelma@35172
    34
#922 := (ite #281 #905 #904)
himmelma@35172
    35
decl uf_8 :: T3
himmelma@35172
    36
#18 := uf_8
himmelma@35172
    37
#848 := (uf_1 uf_8 #22)
himmelma@35172
    38
#903 := (= #848 #902)
himmelma@35172
    39
#60 := 0::int
himmelma@35172
    40
decl uf_5 :: (-> T4 int)
himmelma@35172
    41
#803 := (uf_5 #74)
himmelma@35172
    42
#117 := -1::int
himmelma@35172
    43
#813 := (* -1::int #803)
himmelma@35172
    44
#16 := (uf_5 uf_7)
himmelma@35172
    45
#916 := (+ #16 #813)
himmelma@35172
    46
#917 := (<= #916 0::int)
himmelma@35172
    47
#925 := (ite #917 #922 #903)
himmelma@35172
    48
#6 := (:var 0 T2)
himmelma@35172
    49
#19 := (uf_1 uf_8 #6)
himmelma@35172
    50
#544 := (pattern #19)
himmelma@35172
    51
#25 := (uf_1 uf_11 #6)
himmelma@35172
    52
#543 := (pattern #25)
himmelma@35172
    53
#92 := (uf_1 #91 #6)
himmelma@35172
    54
#542 := (pattern #92)
himmelma@35172
    55
#13 := (uf_6 #6)
himmelma@35172
    56
#541 := (pattern #13)
himmelma@35172
    57
#447 := (= #19 #92)
himmelma@35172
    58
#445 := (= #25 #92)
himmelma@35172
    59
#444 := (= #23 #92)
himmelma@35172
    60
#20 := (= #13 uf_7)
himmelma@35172
    61
#446 := (ite #20 #444 #445)
himmelma@35172
    62
#120 := (* -1::int #16)
himmelma@35172
    63
#14 := (uf_5 #13)
himmelma@35172
    64
#121 := (+ #14 #120)
himmelma@35172
    65
#119 := (>= #121 0::int)
himmelma@35172
    66
#448 := (ite #119 #446 #447)
himmelma@35172
    67
#545 := (forall (vars (?x3 T2)) (:pat #541 #542 #543 #544) #448)
himmelma@35172
    68
#451 := (forall (vars (?x3 T2)) #448)
himmelma@35172
    69
#548 := (iff #451 #545)
himmelma@35172
    70
#546 := (iff #448 #448)
himmelma@35172
    71
#547 := [refl]: #546
himmelma@35172
    72
#549 := [quant-intro #547]: #548
himmelma@35172
    73
#26 := (ite #20 #23 #25)
himmelma@35172
    74
#127 := (ite #119 #26 #19)
himmelma@35172
    75
#368 := (= #92 #127)
himmelma@35172
    76
#369 := (forall (vars (?x3 T2)) #368)
himmelma@35172
    77
#452 := (iff #369 #451)
himmelma@35172
    78
#449 := (iff #368 #448)
himmelma@35172
    79
#450 := [rewrite]: #449
himmelma@35172
    80
#453 := [quant-intro #450]: #452
himmelma@35172
    81
#392 := (~ #369 #369)
himmelma@35172
    82
#390 := (~ #368 #368)
himmelma@35172
    83
#391 := [refl]: #390
himmelma@35172
    84
#366 := [nnf-pos #391]: #392
himmelma@35172
    85
decl uf_3 :: (-> T1 T2 real)
himmelma@35172
    86
#12 := (uf_3 uf_4 #6)
himmelma@35172
    87
#132 := (= #12 #127)
himmelma@35172
    88
#135 := (forall (vars (?x3 T2)) #132)
himmelma@35172
    89
#370 := (iff #135 #369)
himmelma@35172
    90
#4 := (:var 1 T1)
himmelma@35172
    91
#8 := (uf_3 #4 #6)
himmelma@35172
    92
#5 := (uf_2 #4)
himmelma@35172
    93
#7 := (uf_1 #5 #6)
himmelma@35172
    94
#9 := (= #7 #8)
himmelma@35172
    95
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
himmelma@35172
    96
#113 := [asserted]: #10
himmelma@35172
    97
#371 := [rewrite* #113]: #370
himmelma@35172
    98
#17 := (< #14 #16)
himmelma@35172
    99
#27 := (ite #17 #19 #26)
himmelma@35172
   100
#28 := (= #12 #27)
himmelma@35172
   101
#29 := (forall (vars (?x3 T2)) #28)
himmelma@35172
   102
#136 := (iff #29 #135)
himmelma@35172
   103
#133 := (iff #28 #132)
himmelma@35172
   104
#130 := (= #27 #127)
himmelma@35172
   105
#118 := (not #119)
himmelma@35172
   106
#124 := (ite #118 #19 #26)
himmelma@35172
   107
#128 := (= #124 #127)
himmelma@35172
   108
#129 := [rewrite]: #128
himmelma@35172
   109
#125 := (= #27 #124)
himmelma@35172
   110
#122 := (iff #17 #118)
himmelma@35172
   111
#123 := [rewrite]: #122
himmelma@35172
   112
#126 := [monotonicity #123]: #125
himmelma@35172
   113
#131 := [trans #126 #129]: #130
himmelma@35172
   114
#134 := [monotonicity #131]: #133
himmelma@35172
   115
#137 := [quant-intro #134]: #136
himmelma@35172
   116
#114 := [asserted]: #29
himmelma@35172
   117
#138 := [mp #114 #137]: #135
himmelma@35172
   118
#372 := [mp #138 #371]: #369
himmelma@35172
   119
#367 := [mp~ #372 #366]: #369
himmelma@35172
   120
#454 := [mp #367 #453]: #451
himmelma@35172
   121
#550 := [mp #454 #549]: #545
himmelma@35172
   122
#738 := (not #545)
himmelma@35172
   123
#928 := (or #738 #925)
himmelma@35172
   124
#75 := (= #74 uf_7)
himmelma@35172
   125
#906 := (ite #75 #905 #904)
himmelma@35172
   126
#907 := (+ #803 #120)
himmelma@35172
   127
#908 := (>= #907 0::int)
himmelma@35172
   128
#909 := (ite #908 #906 #903)
himmelma@35172
   129
#929 := (or #738 #909)
himmelma@35172
   130
#931 := (iff #929 #928)
himmelma@35172
   131
#933 := (iff #928 #928)
himmelma@35172
   132
#934 := [rewrite]: #933
himmelma@35172
   133
#926 := (iff #909 #925)
himmelma@35172
   134
#923 := (iff #906 #922)
himmelma@35172
   135
#283 := (iff #75 #281)
himmelma@35172
   136
#284 := [rewrite]: #283
himmelma@35172
   137
#924 := [monotonicity #284]: #923
himmelma@35172
   138
#920 := (iff #908 #917)
himmelma@35172
   139
#910 := (+ #120 #803)
himmelma@35172
   140
#913 := (>= #910 0::int)
himmelma@35172
   141
#918 := (iff #913 #917)
himmelma@35172
   142
#919 := [rewrite]: #918
himmelma@35172
   143
#914 := (iff #908 #913)
himmelma@35172
   144
#911 := (= #907 #910)
himmelma@35172
   145
#912 := [rewrite]: #911
himmelma@35172
   146
#915 := [monotonicity #912]: #914
himmelma@35172
   147
#921 := [trans #915 #919]: #920
himmelma@35172
   148
#927 := [monotonicity #921 #924]: #926
himmelma@35172
   149
#932 := [monotonicity #927]: #931
himmelma@35172
   150
#935 := [trans #932 #934]: #931
himmelma@35172
   151
#930 := [quant-inst]: #929
himmelma@35172
   152
#936 := [mp #930 #935]: #928
himmelma@35172
   153
#1300 := [unit-resolution #936 #550]: #925
himmelma@35172
   154
#989 := (= #16 #803)
himmelma@35172
   155
#1277 := (= #803 #16)
himmelma@35172
   156
#280 := [asserted]: #75
himmelma@35172
   157
#287 := [mp #280 #284]: #281
himmelma@35172
   158
#1276 := [symm #287]: #75
himmelma@35172
   159
#1278 := [monotonicity #1276]: #1277
himmelma@35172
   160
#1301 := [symm #1278]: #989
himmelma@35172
   161
#1302 := (not #989)
himmelma@35172
   162
#1303 := (or #1302 #917)
himmelma@35172
   163
#1304 := [th-lemma]: #1303
himmelma@35172
   164
#1305 := [unit-resolution #1304 #1301]: #917
himmelma@35172
   165
#950 := (not #917)
himmelma@35172
   166
#949 := (not #925)
himmelma@35172
   167
#951 := (or #949 #950 #922)
himmelma@35172
   168
#952 := [def-axiom]: #951
himmelma@35172
   169
#1306 := [unit-resolution #952 #1305 #1300]: #922
himmelma@35172
   170
#937 := (not #922)
himmelma@35172
   171
#1307 := (or #937 #905)
himmelma@35172
   172
#938 := (not #281)
himmelma@35172
   173
#939 := (or #937 #938 #905)
himmelma@35172
   174
#940 := [def-axiom]: #939
himmelma@35172
   175
#1308 := [unit-resolution #940 #287]: #1307
himmelma@35172
   176
#1309 := [unit-resolution #1308 #1306]: #905
himmelma@35172
   177
#1356 := (= #799 #23)
himmelma@35172
   178
#800 := (= #23 #799)
himmelma@35172
   179
decl uf_15 :: T4
himmelma@35172
   180
#40 := uf_15
himmelma@35172
   181
#41 := (uf_5 uf_15)
himmelma@35172
   182
#814 := (+ #41 #813)
himmelma@35172
   183
#815 := (<= #814 0::int)
himmelma@35172
   184
#836 := (not #815)
himmelma@35172
   185
#158 := (* -1::int #41)
himmelma@35172
   186
#1270 := (+ #16 #158)
himmelma@35172
   187
#1265 := (>= #1270 0::int)
himmelma@35172
   188
#1339 := (not #1265)
himmelma@35172
   189
#1269 := (= #16 #41)
himmelma@35172
   190
#1298 := (not #1269)
himmelma@35172
   191
#286 := (= uf_7 uf_15)
himmelma@35172
   192
#44 := (uf_10 uf_15)
himmelma@35172
   193
#72 := (uf_6 #44)
himmelma@35172
   194
#73 := (= #72 uf_15)
himmelma@35172
   195
#277 := (= uf_15 #72)
himmelma@35172
   196
#278 := (iff #73 #277)
himmelma@35172
   197
#279 := [rewrite]: #278
himmelma@35172
   198
#276 := [asserted]: #73
himmelma@35172
   199
#282 := [mp #276 #279]: #277
himmelma@35172
   200
#1274 := [symm #282]: #73
himmelma@35172
   201
#729 := (= uf_7 #72)
himmelma@35172
   202
decl uf_17 :: (-> int T4)
himmelma@35172
   203
#611 := (uf_5 #72)
himmelma@35172
   204
#991 := (uf_17 #611)
himmelma@35172
   205
#1289 := (= #991 #72)
himmelma@35172
   206
#992 := (= #72 #991)
himmelma@35172
   207
#55 := (:var 0 T4)
himmelma@35172
   208
#56 := (uf_5 #55)
himmelma@35172
   209
#574 := (pattern #56)
himmelma@35172
   210
#57 := (uf_17 #56)
himmelma@35172
   211
#177 := (= #55 #57)
himmelma@35172
   212
#575 := (forall (vars (?x7 T4)) (:pat #574) #177)
himmelma@35172
   213
#195 := (forall (vars (?x7 T4)) #177)
himmelma@35172
   214
#578 := (iff #195 #575)
himmelma@35172
   215
#576 := (iff #177 #177)
himmelma@35172
   216
#577 := [refl]: #576
himmelma@35172
   217
#579 := [quant-intro #577]: #578
himmelma@35172
   218
#405 := (~ #195 #195)
himmelma@35172
   219
#403 := (~ #177 #177)
himmelma@35172
   220
#404 := [refl]: #403
himmelma@35172
   221
#406 := [nnf-pos #404]: #405
himmelma@35172
   222
#58 := (= #57 #55)
himmelma@35172
   223
#59 := (forall (vars (?x7 T4)) #58)
himmelma@35172
   224
#196 := (iff #59 #195)
himmelma@35172
   225
#193 := (iff #58 #177)
himmelma@35172
   226
#194 := [rewrite]: #193
himmelma@35172
   227
#197 := [quant-intro #194]: #196
himmelma@35172
   228
#155 := [asserted]: #59
himmelma@35172
   229
#200 := [mp #155 #197]: #195
himmelma@35172
   230
#407 := [mp~ #200 #406]: #195
himmelma@35172
   231
#580 := [mp #407 #579]: #575
himmelma@35172
   232
#995 := (not #575)
himmelma@35172
   233
#996 := (or #995 #992)
himmelma@35172
   234
#997 := [quant-inst]: #996
himmelma@35172
   235
#1273 := [unit-resolution #997 #580]: #992
himmelma@35172
   236
#1290 := [symm #1273]: #1289
himmelma@35172
   237
#1293 := (= uf_7 #991)
himmelma@35172
   238
#993 := (uf_17 #803)
himmelma@35172
   239
#1287 := (= #993 #991)
himmelma@35172
   240
#1284 := (= #803 #611)
himmelma@35172
   241
#987 := (= #41 #611)
himmelma@35172
   242
#1279 := (= #611 #41)
himmelma@35172
   243
#1280 := [monotonicity #1274]: #1279
himmelma@35172
   244
#1281 := [symm #1280]: #987
himmelma@35172
   245
#1282 := (= #803 #41)
himmelma@35172
   246
#1275 := [hypothesis]: #1269
himmelma@35172
   247
#1283 := [trans #1278 #1275]: #1282
himmelma@35172
   248
#1285 := [trans #1283 #1281]: #1284
himmelma@35172
   249
#1288 := [monotonicity #1285]: #1287
himmelma@35172
   250
#1291 := (= uf_7 #993)
himmelma@35172
   251
#994 := (= #74 #993)
himmelma@35172
   252
#1000 := (or #995 #994)
himmelma@35172
   253
#1001 := [quant-inst]: #1000
himmelma@35172
   254
#1286 := [unit-resolution #1001 #580]: #994
himmelma@35172
   255
#1292 := [trans #287 #1286]: #1291
himmelma@35172
   256
#1294 := [trans #1292 #1288]: #1293
himmelma@35172
   257
#1295 := [trans #1294 #1290]: #729
himmelma@35172
   258
#1296 := [trans #1295 #1274]: #286
himmelma@35172
   259
#290 := (not #286)
himmelma@35172
   260
#76 := (= uf_15 uf_7)
himmelma@35172
   261
#77 := (not #76)
himmelma@35172
   262
#291 := (iff #77 #290)
himmelma@35172
   263
#288 := (iff #76 #286)
himmelma@35172
   264
#289 := [rewrite]: #288
himmelma@35172
   265
#292 := [monotonicity #289]: #291
himmelma@35172
   266
#285 := [asserted]: #77
himmelma@35172
   267
#295 := [mp #285 #292]: #290
himmelma@35172
   268
#1297 := [unit-resolution #295 #1296]: false
himmelma@35172
   269
#1299 := [lemma #1297]: #1298
himmelma@35172
   270
#1342 := (or #1269 #1339)
himmelma@35172
   271
#1271 := (<= #1270 0::int)
himmelma@35172
   272
#621 := (* -1::int #611)
himmelma@35172
   273
#723 := (+ #16 #621)
himmelma@35172
   274
#724 := (<= #723 0::int)
himmelma@35172
   275
decl uf_12 :: T1
himmelma@35172
   276
#30 := uf_12
himmelma@35172
   277
#88 := (uf_2 uf_12)
himmelma@35172
   278
#771 := (uf_1 #88 #44)
himmelma@35172
   279
#45 := (uf_1 uf_9 #44)
himmelma@35172
   280
#772 := (= #45 #771)
himmelma@35172
   281
#796 := (not #772)
himmelma@35172
   282
decl uf_14 :: T1
himmelma@35172
   283
#38 := uf_14
himmelma@35172
   284
#83 := (uf_2 uf_14)
himmelma@35172
   285
#656 := (uf_1 #83 #44)
himmelma@35172
   286
#1239 := (= #656 #771)
himmelma@35172
   287
#1252 := (not #1239)
himmelma@35172
   288
#1324 := (iff #1252 #796)
himmelma@35172
   289
#1322 := (iff #1239 #772)
himmelma@35172
   290
#1320 := (= #656 #45)
himmelma@35172
   291
#661 := (= #45 #656)
himmelma@35172
   292
#659 := (uf_1 uf_11 #44)
himmelma@35172
   293
#664 := (= #656 #659)
himmelma@35172
   294
#667 := (ite #277 #661 #664)
himmelma@35172
   295
#657 := (uf_1 uf_8 #44)
himmelma@35172
   296
#670 := (= #656 #657)
himmelma@35172
   297
#622 := (+ #41 #621)
himmelma@35172
   298
#623 := (<= #622 0::int)
himmelma@35172
   299
#673 := (ite #623 #667 #670)
himmelma@35172
   300
#84 := (uf_1 #83 #6)
himmelma@35172
   301
#560 := (pattern #84)
himmelma@35172
   302
#467 := (= #19 #84)
himmelma@35172
   303
#465 := (= #25 #84)
himmelma@35172
   304
#464 := (= #45 #84)
himmelma@35172
   305
#43 := (= #13 uf_15)
himmelma@35172
   306
#466 := (ite #43 #464 #465)
himmelma@35172
   307
#159 := (+ #14 #158)
himmelma@35172
   308
#157 := (>= #159 0::int)
himmelma@35172
   309
#468 := (ite #157 #466 #467)
himmelma@35172
   310
#561 := (forall (vars (?x5 T2)) (:pat #541 #560 #543 #544) #468)
himmelma@35172
   311
#471 := (forall (vars (?x5 T2)) #468)
himmelma@35172
   312
#564 := (iff #471 #561)
himmelma@35172
   313
#562 := (iff #468 #468)
himmelma@35172
   314
#563 := [refl]: #562
himmelma@35172
   315
#565 := [quant-intro #563]: #564
himmelma@35172
   316
#46 := (ite #43 #45 #25)
himmelma@35172
   317
#165 := (ite #157 #46 #19)
himmelma@35172
   318
#378 := (= #84 #165)
himmelma@35172
   319
#379 := (forall (vars (?x5 T2)) #378)
himmelma@35172
   320
#472 := (iff #379 #471)
himmelma@35172
   321
#469 := (iff #378 #468)
himmelma@35172
   322
#470 := [rewrite]: #469
himmelma@35172
   323
#473 := [quant-intro #470]: #472
himmelma@35172
   324
#359 := (~ #379 #379)
himmelma@35172
   325
#361 := (~ #378 #378)
himmelma@35172
   326
#358 := [refl]: #361
himmelma@35172
   327
#356 := [nnf-pos #358]: #359
himmelma@35172
   328
#39 := (uf_3 uf_14 #6)
himmelma@35172
   329
#170 := (= #39 #165)
himmelma@35172
   330
#173 := (forall (vars (?x5 T2)) #170)
himmelma@35172
   331
#380 := (iff #173 #379)
himmelma@35172
   332
#381 := [rewrite* #113]: #380
himmelma@35172
   333
#42 := (< #14 #41)
himmelma@35172
   334
#47 := (ite #42 #19 #46)
himmelma@35172
   335
#48 := (= #39 #47)
himmelma@35172
   336
#49 := (forall (vars (?x5 T2)) #48)
himmelma@35172
   337
#174 := (iff #49 #173)
himmelma@35172
   338
#171 := (iff #48 #170)
himmelma@35172
   339
#168 := (= #47 #165)
himmelma@35172
   340
#156 := (not #157)
himmelma@35172
   341
#162 := (ite #156 #19 #46)
himmelma@35172
   342
#166 := (= #162 #165)
himmelma@35172
   343
#167 := [rewrite]: #166
himmelma@35172
   344
#163 := (= #47 #162)
himmelma@35172
   345
#160 := (iff #42 #156)
himmelma@35172
   346
#161 := [rewrite]: #160
himmelma@35172
   347
#164 := [monotonicity #161]: #163
himmelma@35172
   348
#169 := [trans #164 #167]: #168
himmelma@35172
   349
#172 := [monotonicity #169]: #171
himmelma@35172
   350
#175 := [quant-intro #172]: #174
himmelma@35172
   351
#116 := [asserted]: #49
himmelma@35172
   352
#176 := [mp #116 #175]: #173
himmelma@35172
   353
#382 := [mp #176 #381]: #379
himmelma@35172
   354
#357 := [mp~ #382 #356]: #379
himmelma@35172
   355
#474 := [mp #357 #473]: #471
himmelma@35172
   356
#566 := [mp #474 #565]: #561
himmelma@35172
   357
#676 := (not #561)
himmelma@35172
   358
#677 := (or #676 #673)
himmelma@35172
   359
#658 := (= #657 #656)
himmelma@35172
   360
#660 := (= #659 #656)
himmelma@35172
   361
#662 := (ite #73 #661 #660)
himmelma@35172
   362
#612 := (+ #611 #158)
himmelma@35172
   363
#613 := (>= #612 0::int)
himmelma@35172
   364
#663 := (ite #613 #662 #658)
himmelma@35172
   365
#678 := (or #676 #663)
himmelma@35172
   366
#680 := (iff #678 #677)
himmelma@35172
   367
#682 := (iff #677 #677)
himmelma@35172
   368
#683 := [rewrite]: #682
himmelma@35172
   369
#674 := (iff #663 #673)
himmelma@35172
   370
#671 := (iff #658 #670)
himmelma@35172
   371
#672 := [rewrite]: #671
himmelma@35172
   372
#668 := (iff #662 #667)
himmelma@35172
   373
#665 := (iff #660 #664)
himmelma@35172
   374
#666 := [rewrite]: #665
himmelma@35172
   375
#669 := [monotonicity #279 #666]: #668
himmelma@35172
   376
#626 := (iff #613 #623)
himmelma@35172
   377
#615 := (+ #158 #611)
himmelma@35172
   378
#618 := (>= #615 0::int)
himmelma@35172
   379
#624 := (iff #618 #623)
himmelma@35172
   380
#625 := [rewrite]: #624
himmelma@35172
   381
#619 := (iff #613 #618)
himmelma@35172
   382
#616 := (= #612 #615)
himmelma@35172
   383
#617 := [rewrite]: #616
himmelma@35172
   384
#620 := [monotonicity #617]: #619
himmelma@35172
   385
#627 := [trans #620 #625]: #626
himmelma@35172
   386
#675 := [monotonicity #627 #669 #672]: #674
himmelma@35172
   387
#681 := [monotonicity #675]: #680
himmelma@35172
   388
#684 := [trans #681 #683]: #680
himmelma@35172
   389
#679 := [quant-inst]: #678
himmelma@35172
   390
#685 := [mp #679 #684]: #677
himmelma@35172
   391
#1311 := [unit-resolution #685 #566]: #673
himmelma@35172
   392
#1312 := (not #987)
himmelma@35172
   393
#1313 := (or #1312 #623)
himmelma@35172
   394
#1314 := [th-lemma]: #1313
himmelma@35172
   395
#1315 := [unit-resolution #1314 #1281]: #623
himmelma@35172
   396
#645 := (not #623)
himmelma@35172
   397
#698 := (not #673)
himmelma@35172
   398
#699 := (or #698 #645 #667)
himmelma@35172
   399
#700 := [def-axiom]: #699
himmelma@35172
   400
#1316 := [unit-resolution #700 #1315 #1311]: #667
himmelma@35172
   401
#686 := (not #667)
himmelma@35172
   402
#1317 := (or #686 #661)
himmelma@35172
   403
#687 := (not #277)
himmelma@35172
   404
#688 := (or #686 #687 #661)
himmelma@35172
   405
#689 := [def-axiom]: #688
himmelma@35172
   406
#1318 := [unit-resolution #689 #282]: #1317
himmelma@35172
   407
#1319 := [unit-resolution #1318 #1316]: #661
himmelma@35172
   408
#1321 := [symm #1319]: #1320
himmelma@35172
   409
#1323 := [monotonicity #1321]: #1322
himmelma@35172
   410
#1325 := [monotonicity #1323]: #1324
himmelma@35172
   411
#1145 := (* -1::real #771)
himmelma@35172
   412
#1240 := (+ #656 #1145)
himmelma@35172
   413
#1241 := (<= #1240 0::real)
himmelma@35172
   414
#1249 := (not #1241)
himmelma@35172
   415
#1243 := [hypothesis]: #1241
himmelma@35172
   416
decl uf_18 :: T3
himmelma@35172
   417
#80 := uf_18
himmelma@35172
   418
#1040 := (uf_1 uf_18 #44)
himmelma@35172
   419
#1043 := (* -1::real #1040)
himmelma@35172
   420
#1156 := (+ #771 #1043)
himmelma@35172
   421
#1157 := (>= #1156 0::real)
himmelma@35172
   422
#1189 := (not #1157)
himmelma@35172
   423
#708 := (uf_1 #91 #44)
himmelma@35172
   424
#1168 := (+ #708 #1043)
himmelma@35172
   425
#1169 := (<= #1168 0::real)
himmelma@35172
   426
#1174 := (or #1157 #1169)
himmelma@35172
   427
#1177 := (not #1174)
himmelma@35172
   428
#89 := (uf_1 #88 #6)
himmelma@35172
   429
#552 := (pattern #89)
himmelma@35172
   430
#81 := (uf_1 uf_18 #6)
himmelma@35172
   431
#594 := (pattern #81)
himmelma@35172
   432
#324 := (* -1::real #92)
himmelma@35172
   433
#325 := (+ #81 #324)
himmelma@35172
   434
#323 := (>= #325 0::real)
himmelma@35172
   435
#317 := (* -1::real #89)
himmelma@35172
   436
#318 := (+ #81 #317)
himmelma@35172
   437
#319 := (<= #318 0::real)
himmelma@35172
   438
#436 := (or #319 #323)
himmelma@35172
   439
#437 := (not #436)
himmelma@35172
   440
#601 := (forall (vars (?x11 T2)) (:pat #594 #552 #542) #437)
himmelma@35172
   441
#440 := (forall (vars (?x11 T2)) #437)
himmelma@35172
   442
#604 := (iff #440 #601)
himmelma@35172
   443
#602 := (iff #437 #437)
himmelma@35172
   444
#603 := [refl]: #602
himmelma@35172
   445
#605 := [quant-intro #603]: #604
himmelma@35172
   446
#326 := (not #323)
himmelma@35172
   447
#320 := (not #319)
himmelma@35172
   448
#329 := (and #320 #326)
himmelma@35172
   449
#332 := (forall (vars (?x11 T2)) #329)
himmelma@35172
   450
#441 := (iff #332 #440)
himmelma@35172
   451
#438 := (iff #329 #437)
himmelma@35172
   452
#439 := [rewrite]: #438
himmelma@35172
   453
#442 := [quant-intro #439]: #441
himmelma@35172
   454
#425 := (~ #332 #332)
himmelma@35172
   455
#423 := (~ #329 #329)
himmelma@35172
   456
#424 := [refl]: #423
himmelma@35172
   457
#426 := [nnf-pos #424]: #425
himmelma@35172
   458
#306 := (* -1::real #84)
himmelma@35172
   459
#307 := (+ #81 #306)
himmelma@35172
   460
#305 := (>= #307 0::real)
himmelma@35172
   461
#308 := (not #305)
himmelma@35172
   462
#301 := (* -1::real #81)
himmelma@35172
   463
#79 := (uf_1 #78 #6)
himmelma@35172
   464
#302 := (+ #79 #301)
himmelma@35172
   465
#300 := (>= #302 0::real)
himmelma@35172
   466
#298 := (not #300)
himmelma@35172
   467
#311 := (and #298 #308)
himmelma@35172
   468
#314 := (forall (vars (?x10 T2)) #311)
himmelma@35172
   469
#335 := (and #314 #332)
himmelma@35172
   470
#93 := (< #81 #92)
himmelma@35172
   471
#90 := (< #89 #81)
himmelma@35172
   472
#94 := (and #90 #93)
himmelma@35172
   473
#95 := (forall (vars (?x11 T2)) #94)
himmelma@35172
   474
#85 := (< #81 #84)
himmelma@35172
   475
#82 := (< #79 #81)
himmelma@35172
   476
#86 := (and #82 #85)
himmelma@35172
   477
#87 := (forall (vars (?x10 T2)) #86)
himmelma@35172
   478
#96 := (and #87 #95)
himmelma@35172
   479
#336 := (iff #96 #335)
himmelma@35172
   480
#333 := (iff #95 #332)
himmelma@35172
   481
#330 := (iff #94 #329)
himmelma@35172
   482
#327 := (iff #93 #326)
himmelma@35172
   483
#328 := [rewrite]: #327
himmelma@35172
   484
#321 := (iff #90 #320)
himmelma@35172
   485
#322 := [rewrite]: #321
himmelma@35172
   486
#331 := [monotonicity #322 #328]: #330
himmelma@35172
   487
#334 := [quant-intro #331]: #333
himmelma@35172
   488
#315 := (iff #87 #314)
himmelma@35172
   489
#312 := (iff #86 #311)
himmelma@35172
   490
#309 := (iff #85 #308)
himmelma@35172
   491
#310 := [rewrite]: #309
himmelma@35172
   492
#303 := (iff #82 #298)
himmelma@35172
   493
#304 := [rewrite]: #303
himmelma@35172
   494
#313 := [monotonicity #304 #310]: #312
himmelma@35172
   495
#316 := [quant-intro #313]: #315
himmelma@35172
   496
#337 := [monotonicity #316 #334]: #336
himmelma@35172
   497
#293 := [asserted]: #96
himmelma@35172
   498
#338 := [mp #293 #337]: #335
himmelma@35172
   499
#340 := [and-elim #338]: #332
himmelma@35172
   500
#427 := [mp~ #340 #426]: #332
himmelma@35172
   501
#443 := [mp #427 #442]: #440
himmelma@35172
   502
#606 := [mp #443 #605]: #601
himmelma@35172
   503
#1124 := (not #601)
himmelma@35172
   504
#1180 := (or #1124 #1177)
himmelma@35172
   505
#1142 := (* -1::real #708)
himmelma@35172
   506
#1143 := (+ #1040 #1142)
himmelma@35172
   507
#1144 := (>= #1143 0::real)
himmelma@35172
   508
#1146 := (+ #1040 #1145)
himmelma@35172
   509
#1147 := (<= #1146 0::real)
himmelma@35172
   510
#1148 := (or #1147 #1144)
himmelma@35172
   511
#1149 := (not #1148)
himmelma@35172
   512
#1181 := (or #1124 #1149)
himmelma@35172
   513
#1183 := (iff #1181 #1180)
himmelma@35172
   514
#1185 := (iff #1180 #1180)
himmelma@35172
   515
#1186 := [rewrite]: #1185
himmelma@35172
   516
#1178 := (iff #1149 #1177)
himmelma@35172
   517
#1175 := (iff #1148 #1174)
himmelma@35172
   518
#1172 := (iff #1144 #1169)
himmelma@35172
   519
#1162 := (+ #1142 #1040)
himmelma@35172
   520
#1165 := (>= #1162 0::real)
himmelma@35172
   521
#1170 := (iff #1165 #1169)
himmelma@35172
   522
#1171 := [rewrite]: #1170
himmelma@35172
   523
#1166 := (iff #1144 #1165)
himmelma@35172
   524
#1163 := (= #1143 #1162)
himmelma@35172
   525
#1164 := [rewrite]: #1163
himmelma@35172
   526
#1167 := [monotonicity #1164]: #1166
himmelma@35172
   527
#1173 := [trans #1167 #1171]: #1172
himmelma@35172
   528
#1160 := (iff #1147 #1157)
himmelma@35172
   529
#1150 := (+ #1145 #1040)
himmelma@35172
   530
#1153 := (<= #1150 0::real)
himmelma@35172
   531
#1158 := (iff #1153 #1157)
himmelma@35172
   532
#1159 := [rewrite]: #1158
himmelma@35172
   533
#1154 := (iff #1147 #1153)
himmelma@35172
   534
#1151 := (= #1146 #1150)
himmelma@35172
   535
#1152 := [rewrite]: #1151
himmelma@35172
   536
#1155 := [monotonicity #1152]: #1154
himmelma@35172
   537
#1161 := [trans #1155 #1159]: #1160
himmelma@35172
   538
#1176 := [monotonicity #1161 #1173]: #1175
himmelma@35172
   539
#1179 := [monotonicity #1176]: #1178
himmelma@35172
   540
#1184 := [monotonicity #1179]: #1183
himmelma@35172
   541
#1187 := [trans #1184 #1186]: #1183
himmelma@35172
   542
#1182 := [quant-inst]: #1181
himmelma@35172
   543
#1188 := [mp #1182 #1187]: #1180
himmelma@35172
   544
#1244 := [unit-resolution #1188 #606]: #1177
himmelma@35172
   545
#1190 := (or #1174 #1189)
himmelma@35172
   546
#1191 := [def-axiom]: #1190
himmelma@35172
   547
#1245 := [unit-resolution #1191 #1244]: #1189
himmelma@35172
   548
#1054 := (+ #656 #1043)
himmelma@35172
   549
#1055 := (<= #1054 0::real)
himmelma@35172
   550
#1079 := (not #1055)
himmelma@35172
   551
#607 := (uf_1 #78 #44)
himmelma@35172
   552
#1044 := (+ #607 #1043)
himmelma@35172
   553
#1045 := (>= #1044 0::real)
himmelma@35172
   554
#1060 := (or #1045 #1055)
himmelma@35172
   555
#1063 := (not #1060)
himmelma@35172
   556
#567 := (pattern #79)
himmelma@35172
   557
#428 := (or #300 #305)
himmelma@35172
   558
#429 := (not #428)
himmelma@35172
   559
#595 := (forall (vars (?x10 T2)) (:pat #567 #594 #560) #429)
himmelma@35172
   560
#432 := (forall (vars (?x10 T2)) #429)
himmelma@35172
   561
#598 := (iff #432 #595)
himmelma@35172
   562
#596 := (iff #429 #429)
himmelma@35172
   563
#597 := [refl]: #596
himmelma@35172
   564
#599 := [quant-intro #597]: #598
himmelma@35172
   565
#433 := (iff #314 #432)
himmelma@35172
   566
#430 := (iff #311 #429)
himmelma@35172
   567
#431 := [rewrite]: #430
himmelma@35172
   568
#434 := [quant-intro #431]: #433
himmelma@35172
   569
#420 := (~ #314 #314)
himmelma@35172
   570
#418 := (~ #311 #311)
himmelma@35172
   571
#419 := [refl]: #418
himmelma@35172
   572
#421 := [nnf-pos #419]: #420
himmelma@35172
   573
#339 := [and-elim #338]: #314
himmelma@35172
   574
#422 := [mp~ #339 #421]: #314
himmelma@35172
   575
#435 := [mp #422 #434]: #432
himmelma@35172
   576
#600 := [mp #435 #599]: #595
himmelma@35172
   577
#1066 := (not #595)
himmelma@35172
   578
#1067 := (or #1066 #1063)
himmelma@35172
   579
#1039 := (* -1::real #656)
himmelma@35172
   580
#1041 := (+ #1040 #1039)
himmelma@35172
   581
#1042 := (>= #1041 0::real)
himmelma@35172
   582
#1046 := (or #1045 #1042)
himmelma@35172
   583
#1047 := (not #1046)
himmelma@35172
   584
#1068 := (or #1066 #1047)
himmelma@35172
   585
#1070 := (iff #1068 #1067)
himmelma@35172
   586
#1072 := (iff #1067 #1067)
himmelma@35172
   587
#1073 := [rewrite]: #1072
himmelma@35172
   588
#1064 := (iff #1047 #1063)
himmelma@35172
   589
#1061 := (iff #1046 #1060)
himmelma@35172
   590
#1058 := (iff #1042 #1055)
himmelma@35172
   591
#1048 := (+ #1039 #1040)
himmelma@35172
   592
#1051 := (>= #1048 0::real)
himmelma@35172
   593
#1056 := (iff #1051 #1055)
himmelma@35172
   594
#1057 := [rewrite]: #1056
himmelma@35172
   595
#1052 := (iff #1042 #1051)
himmelma@35172
   596
#1049 := (= #1041 #1048)
himmelma@35172
   597
#1050 := [rewrite]: #1049
himmelma@35172
   598
#1053 := [monotonicity #1050]: #1052
himmelma@35172
   599
#1059 := [trans #1053 #1057]: #1058
himmelma@35172
   600
#1062 := [monotonicity #1059]: #1061
himmelma@35172
   601
#1065 := [monotonicity #1062]: #1064
himmelma@35172
   602
#1071 := [monotonicity #1065]: #1070
himmelma@35172
   603
#1074 := [trans #1071 #1073]: #1070
himmelma@35172
   604
#1069 := [quant-inst]: #1068
himmelma@35172
   605
#1075 := [mp #1069 #1074]: #1067
himmelma@35172
   606
#1246 := [unit-resolution #1075 #600]: #1063
himmelma@35172
   607
#1080 := (or #1060 #1079)
himmelma@35172
   608
#1081 := [def-axiom]: #1080
himmelma@35172
   609
#1247 := [unit-resolution #1081 #1246]: #1079
himmelma@35172
   610
#1248 := [th-lemma #1247 #1245 #1243]: false
himmelma@35172
   611
#1250 := [lemma #1248]: #1249
himmelma@35172
   612
#1253 := (or #1252 #1241)
himmelma@35172
   613
#1254 := [th-lemma]: #1253
himmelma@35172
   614
#1310 := [unit-resolution #1254 #1250]: #1252
himmelma@35172
   615
#1326 := [mp #1310 #1325]: #796
himmelma@35172
   616
#1328 := (or #724 #772)
himmelma@35172
   617
decl uf_13 :: T3
himmelma@35172
   618
#33 := uf_13
himmelma@35172
   619
#609 := (uf_1 uf_13 #44)
himmelma@35172
   620
#773 := (= #609 #771)
himmelma@35172
   621
#775 := (ite #724 #773 #772)
himmelma@35172
   622
#32 := (uf_1 uf_9 #6)
himmelma@35172
   623
#553 := (pattern #32)
himmelma@35172
   624
#34 := (uf_1 uf_13 #6)
himmelma@35172
   625
#551 := (pattern #34)
himmelma@35172
   626
#456 := (= #32 #89)
himmelma@35172
   627
#455 := (= #34 #89)
himmelma@35172
   628
#457 := (ite #119 #455 #456)
himmelma@35172
   629
#554 := (forall (vars (?x4 T2)) (:pat #541 #551 #552 #553) #457)
himmelma@35172
   630
#460 := (forall (vars (?x4 T2)) #457)
himmelma@35172
   631
#557 := (iff #460 #554)
himmelma@35172
   632
#555 := (iff #457 #457)
himmelma@35172
   633
#556 := [refl]: #555
himmelma@35172
   634
#558 := [quant-intro #556]: #557
himmelma@35172
   635
#143 := (ite #119 #34 #32)
himmelma@35172
   636
#373 := (= #89 #143)
himmelma@35172
   637
#374 := (forall (vars (?x4 T2)) #373)
himmelma@35172
   638
#461 := (iff #374 #460)
himmelma@35172
   639
#458 := (iff #373 #457)
himmelma@35172
   640
#459 := [rewrite]: #458
himmelma@35172
   641
#462 := [quant-intro #459]: #461
himmelma@35172
   642
#362 := (~ #374 #374)
himmelma@35172
   643
#364 := (~ #373 #373)
himmelma@35172
   644
#365 := [refl]: #364
himmelma@35172
   645
#363 := [nnf-pos #365]: #362
himmelma@35172
   646
#31 := (uf_3 uf_12 #6)
himmelma@35172
   647
#148 := (= #31 #143)
himmelma@35172
   648
#151 := (forall (vars (?x4 T2)) #148)
himmelma@35172
   649
#375 := (iff #151 #374)
himmelma@35172
   650
#376 := [rewrite* #113]: #375
himmelma@35172
   651
#35 := (ite #17 #32 #34)
himmelma@35172
   652
#36 := (= #31 #35)
himmelma@35172
   653
#37 := (forall (vars (?x4 T2)) #36)
himmelma@35172
   654
#152 := (iff #37 #151)
himmelma@35172
   655
#149 := (iff #36 #148)
himmelma@35172
   656
#146 := (= #35 #143)
himmelma@35172
   657
#140 := (ite #118 #32 #34)
himmelma@35172
   658
#144 := (= #140 #143)
himmelma@35172
   659
#145 := [rewrite]: #144
himmelma@35172
   660
#141 := (= #35 #140)
himmelma@35172
   661
#142 := [monotonicity #123]: #141
himmelma@35172
   662
#147 := [trans #142 #145]: #146
himmelma@35172
   663
#150 := [monotonicity #147]: #149
himmelma@35172
   664
#153 := [quant-intro #150]: #152
himmelma@35172
   665
#115 := [asserted]: #37
himmelma@35172
   666
#154 := [mp #115 #153]: #151
himmelma@35172
   667
#377 := [mp #154 #376]: #374
himmelma@35172
   668
#360 := [mp~ #377 #363]: #374
himmelma@35172
   669
#463 := [mp #360 #462]: #460
himmelma@35172
   670
#559 := [mp #463 #558]: #554
himmelma@35172
   671
#778 := (not #554)
himmelma@35172
   672
#779 := (or #778 #775)
himmelma@35172
   673
#714 := (+ #611 #120)
himmelma@35172
   674
#715 := (>= #714 0::int)
himmelma@35172
   675
#774 := (ite #715 #773 #772)
himmelma@35172
   676
#780 := (or #778 #774)
himmelma@35172
   677
#782 := (iff #780 #779)
himmelma@35172
   678
#784 := (iff #779 #779)
himmelma@35172
   679
#785 := [rewrite]: #784
himmelma@35172
   680
#776 := (iff #774 #775)
himmelma@35172
   681
#727 := (iff #715 #724)
himmelma@35172
   682
#717 := (+ #120 #611)
himmelma@35172
   683
#720 := (>= #717 0::int)
himmelma@35172
   684
#725 := (iff #720 #724)
himmelma@35172
   685
#726 := [rewrite]: #725
himmelma@35172
   686
#721 := (iff #715 #720)
himmelma@35172
   687
#718 := (= #714 #717)
himmelma@35172
   688
#719 := [rewrite]: #718
himmelma@35172
   689
#722 := [monotonicity #719]: #721
himmelma@35172
   690
#728 := [trans #722 #726]: #727
himmelma@35172
   691
#777 := [monotonicity #728]: #776
himmelma@35172
   692
#783 := [monotonicity #777]: #782
himmelma@35172
   693
#786 := [trans #783 #785]: #782
himmelma@35172
   694
#781 := [quant-inst]: #780
himmelma@35172
   695
#787 := [mp #781 #786]: #779
himmelma@35172
   696
#1327 := [unit-resolution #787 #559]: #775
himmelma@35172
   697
#788 := (not #775)
himmelma@35172
   698
#791 := (or #788 #724 #772)
himmelma@35172
   699
#792 := [def-axiom]: #791
himmelma@35172
   700
#1329 := [unit-resolution #792 #1327]: #1328
himmelma@35172
   701
#1330 := [unit-resolution #1329 #1326]: #724
himmelma@35172
   702
#988 := (>= #622 0::int)
himmelma@35172
   703
#1331 := (or #1312 #988)
himmelma@35172
   704
#1332 := [th-lemma]: #1331
himmelma@35172
   705
#1333 := [unit-resolution #1332 #1281]: #988
himmelma@35172
   706
#761 := (not #724)
himmelma@35172
   707
#1334 := (not #988)
himmelma@35172
   708
#1335 := (or #1271 #1334 #761)
himmelma@35172
   709
#1336 := [th-lemma]: #1335
himmelma@35172
   710
#1337 := [unit-resolution #1336 #1333 #1330]: #1271
himmelma@35172
   711
#1338 := (not #1271)
himmelma@35172
   712
#1340 := (or #1269 #1338 #1339)
himmelma@35172
   713
#1341 := [th-lemma]: #1340
himmelma@35172
   714
#1343 := [unit-resolution #1341 #1337]: #1342
himmelma@35172
   715
#1344 := [unit-resolution #1343 #1299]: #1339
himmelma@35172
   716
#990 := (>= #916 0::int)
himmelma@35172
   717
#1345 := (or #1302 #990)
himmelma@35172
   718
#1346 := [th-lemma]: #1345
himmelma@35172
   719
#1347 := [unit-resolution #1346 #1301]: #990
himmelma@35172
   720
#1348 := (not #990)
himmelma@35172
   721
#1349 := (or #836 #1348 #1265)
himmelma@35172
   722
#1350 := [th-lemma]: #1349
himmelma@35172
   723
#1351 := [unit-resolution #1350 #1347 #1344]: #836
himmelma@35172
   724
#1353 := (or #815 #800)
himmelma@35172
   725
#801 := (uf_1 uf_13 #22)
himmelma@35172
   726
#820 := (= #799 #801)
himmelma@35172
   727
#823 := (ite #815 #820 #800)
himmelma@35172
   728
#476 := (= #32 #79)
himmelma@35172
   729
#475 := (= #34 #79)
himmelma@35172
   730
#477 := (ite #157 #475 #476)
himmelma@35172
   731
#568 := (forall (vars (?x6 T2)) (:pat #541 #551 #567 #553) #477)
himmelma@35172
   732
#480 := (forall (vars (?x6 T2)) #477)
himmelma@35172
   733
#571 := (iff #480 #568)
himmelma@35172
   734
#569 := (iff #477 #477)
himmelma@35172
   735
#570 := [refl]: #569
himmelma@35172
   736
#572 := [quant-intro #570]: #571
himmelma@35172
   737
#181 := (ite #157 #34 #32)
himmelma@35172
   738
#383 := (= #79 #181)
himmelma@35172
   739
#384 := (forall (vars (?x6 T2)) #383)
himmelma@35172
   740
#481 := (iff #384 #480)
himmelma@35172
   741
#478 := (iff #383 #477)
himmelma@35172
   742
#479 := [rewrite]: #478
himmelma@35172
   743
#482 := [quant-intro #479]: #481
himmelma@35172
   744
#352 := (~ #384 #384)
himmelma@35172
   745
#354 := (~ #383 #383)
himmelma@35172
   746
#355 := [refl]: #354
himmelma@35172
   747
#353 := [nnf-pos #355]: #352
himmelma@35172
   748
#51 := (uf_3 uf_16 #6)
himmelma@35172
   749
#186 := (= #51 #181)
himmelma@35172
   750
#189 := (forall (vars (?x6 T2)) #186)
himmelma@35172
   751
#385 := (iff #189 #384)
himmelma@35172
   752
#386 := [rewrite* #113]: #385
himmelma@35172
   753
#52 := (ite #42 #32 #34)
himmelma@35172
   754
#53 := (= #51 #52)
himmelma@35172
   755
#54 := (forall (vars (?x6 T2)) #53)
himmelma@35172
   756
#190 := (iff #54 #189)
himmelma@35172
   757
#187 := (iff #53 #186)
himmelma@35172
   758
#184 := (= #52 #181)
himmelma@35172
   759
#178 := (ite #156 #32 #34)
himmelma@35172
   760
#182 := (= #178 #181)
himmelma@35172
   761
#183 := [rewrite]: #182
himmelma@35172
   762
#179 := (= #52 #178)
himmelma@35172
   763
#180 := [monotonicity #161]: #179
himmelma@35172
   764
#185 := [trans #180 #183]: #184
himmelma@35172
   765
#188 := [monotonicity #185]: #187
himmelma@35172
   766
#191 := [quant-intro #188]: #190
himmelma@35172
   767
#139 := [asserted]: #54
himmelma@35172
   768
#192 := [mp #139 #191]: #189
himmelma@35172
   769
#387 := [mp #192 #386]: #384
himmelma@35172
   770
#402 := [mp~ #387 #353]: #384
himmelma@35172
   771
#483 := [mp #402 #482]: #480
himmelma@35172
   772
#573 := [mp #483 #572]: #568
himmelma@35172
   773
#634 := (not #568)
himmelma@35172
   774
#826 := (or #634 #823)
himmelma@35172
   775
#802 := (= #801 #799)
himmelma@35172
   776
#804 := (+ #803 #158)
himmelma@35172
   777
#805 := (>= #804 0::int)
himmelma@35172
   778
#806 := (ite #805 #802 #800)
himmelma@35172
   779
#827 := (or #634 #806)
himmelma@35172
   780
#829 := (iff #827 #826)
himmelma@35172
   781
#831 := (iff #826 #826)
himmelma@35172
   782
#832 := [rewrite]: #831
himmelma@35172
   783
#824 := (iff #806 #823)
himmelma@35172
   784
#821 := (iff #802 #820)
himmelma@35172
   785
#822 := [rewrite]: #821
himmelma@35172
   786
#818 := (iff #805 #815)
himmelma@35172
   787
#807 := (+ #158 #803)
himmelma@35172
   788
#810 := (>= #807 0::int)
himmelma@35172
   789
#816 := (iff #810 #815)
himmelma@35172
   790
#817 := [rewrite]: #816
himmelma@35172
   791
#811 := (iff #805 #810)
himmelma@35172
   792
#808 := (= #804 #807)
himmelma@35172
   793
#809 := [rewrite]: #808
himmelma@35172
   794
#812 := [monotonicity #809]: #811
himmelma@35172
   795
#819 := [trans #812 #817]: #818
himmelma@35172
   796
#825 := [monotonicity #819 #822]: #824
himmelma@35172
   797
#830 := [monotonicity #825]: #829
himmelma@35172
   798
#833 := [trans #830 #832]: #829
himmelma@35172
   799
#828 := [quant-inst]: #827
himmelma@35172
   800
#834 := [mp #828 #833]: #826
himmelma@35172
   801
#1352 := [unit-resolution #834 #573]: #823
himmelma@35172
   802
#835 := (not #823)
himmelma@35172
   803
#839 := (or #835 #815 #800)
himmelma@35172
   804
#840 := [def-axiom]: #839
himmelma@35172
   805
#1354 := [unit-resolution #840 #1352]: #1353
himmelma@35172
   806
#1355 := [unit-resolution #1354 #1351]: #800
himmelma@35172
   807
#1357 := [symm #1355]: #1356
himmelma@35172
   808
#1358 := [trans #1357 #1309]: #1266
himmelma@35172
   809
#1359 := (not #1266)
himmelma@35172
   810
#1360 := (or #1359 #1272)
himmelma@35172
   811
#1361 := [th-lemma]: #1360
himmelma@35172
   812
#1362 := [unit-resolution #1361 #1358]: #1272
himmelma@35172
   813
#1085 := (uf_1 uf_18 #22)
himmelma@35172
   814
#1099 := (* -1::real #1085)
himmelma@35172
   815
#1112 := (+ #902 #1099)
himmelma@35172
   816
#1113 := (<= #1112 0::real)
himmelma@35172
   817
#1137 := (not #1113)
himmelma@35172
   818
#960 := (uf_1 #88 #22)
himmelma@35172
   819
#1100 := (+ #960 #1099)
himmelma@35172
   820
#1101 := (>= #1100 0::real)
himmelma@35172
   821
#1118 := (or #1101 #1113)
himmelma@35172
   822
#1121 := (not #1118)
himmelma@35172
   823
#1125 := (or #1124 #1121)
himmelma@35172
   824
#1086 := (+ #1085 #1084)
himmelma@35172
   825
#1087 := (>= #1086 0::real)
himmelma@35172
   826
#1088 := (* -1::real #960)
himmelma@35172
   827
#1089 := (+ #1085 #1088)
himmelma@35172
   828
#1090 := (<= #1089 0::real)
himmelma@35172
   829
#1091 := (or #1090 #1087)
himmelma@35172
   830
#1092 := (not #1091)
himmelma@35172
   831
#1126 := (or #1124 #1092)
himmelma@35172
   832
#1128 := (iff #1126 #1125)
himmelma@35172
   833
#1130 := (iff #1125 #1125)
himmelma@35172
   834
#1131 := [rewrite]: #1130
himmelma@35172
   835
#1122 := (iff #1092 #1121)
himmelma@35172
   836
#1119 := (iff #1091 #1118)
himmelma@35172
   837
#1116 := (iff #1087 #1113)
himmelma@35172
   838
#1106 := (+ #1084 #1085)
himmelma@35172
   839
#1109 := (>= #1106 0::real)
himmelma@35172
   840
#1114 := (iff #1109 #1113)
himmelma@35172
   841
#1115 := [rewrite]: #1114
himmelma@35172
   842
#1110 := (iff #1087 #1109)
himmelma@35172
   843
#1107 := (= #1086 #1106)
himmelma@35172
   844
#1108 := [rewrite]: #1107
himmelma@35172
   845
#1111 := [monotonicity #1108]: #1110
himmelma@35172
   846
#1117 := [trans #1111 #1115]: #1116
himmelma@35172
   847
#1104 := (iff #1090 #1101)
himmelma@35172
   848
#1093 := (+ #1088 #1085)
himmelma@35172
   849
#1096 := (<= #1093 0::real)
himmelma@35172
   850
#1102 := (iff #1096 #1101)
himmelma@35172
   851
#1103 := [rewrite]: #1102
himmelma@35172
   852
#1097 := (iff #1090 #1096)
himmelma@35172
   853
#1094 := (= #1089 #1093)
himmelma@35172
   854
#1095 := [rewrite]: #1094
himmelma@35172
   855
#1098 := [monotonicity #1095]: #1097
himmelma@35172
   856
#1105 := [trans #1098 #1103]: #1104
himmelma@35172
   857
#1120 := [monotonicity #1105 #1117]: #1119
himmelma@35172
   858
#1123 := [monotonicity #1120]: #1122
himmelma@35172
   859
#1129 := [monotonicity #1123]: #1128
himmelma@35172
   860
#1132 := [trans #1129 #1131]: #1128
himmelma@35172
   861
#1127 := [quant-inst]: #1126
himmelma@35172
   862
#1133 := [mp #1127 #1132]: #1125
himmelma@35172
   863
#1363 := [unit-resolution #1133 #606]: #1121
himmelma@35172
   864
#1138 := (or #1118 #1137)
himmelma@35172
   865
#1139 := [def-axiom]: #1138
himmelma@35172
   866
#1364 := [unit-resolution #1139 #1363]: #1137
himmelma@35172
   867
#1200 := (+ #799 #1099)
himmelma@35172
   868
#1201 := (>= #1200 0::real)
himmelma@35172
   869
#1231 := (not #1201)
himmelma@35172
   870
#847 := (uf_1 #83 #22)
himmelma@35172
   871
#1210 := (+ #847 #1099)
himmelma@35172
   872
#1211 := (<= #1210 0::real)
himmelma@35172
   873
#1216 := (or #1201 #1211)
himmelma@35172
   874
#1219 := (not #1216)
himmelma@35172
   875
#1222 := (or #1066 #1219)
himmelma@35172
   876
#1197 := (* -1::real #847)
himmelma@35172
   877
#1198 := (+ #1085 #1197)
himmelma@35172
   878
#1199 := (>= #1198 0::real)
himmelma@35172
   879
#1202 := (or #1201 #1199)
himmelma@35172
   880
#1203 := (not #1202)
himmelma@35172
   881
#1223 := (or #1066 #1203)
himmelma@35172
   882
#1225 := (iff #1223 #1222)
himmelma@35172
   883
#1227 := (iff #1222 #1222)
himmelma@35172
   884
#1228 := [rewrite]: #1227
himmelma@35172
   885
#1220 := (iff #1203 #1219)
himmelma@35172
   886
#1217 := (iff #1202 #1216)
himmelma@35172
   887
#1214 := (iff #1199 #1211)
himmelma@35172
   888
#1204 := (+ #1197 #1085)
himmelma@35172
   889
#1207 := (>= #1204 0::real)
himmelma@35172
   890
#1212 := (iff #1207 #1211)
himmelma@35172
   891
#1213 := [rewrite]: #1212
himmelma@35172
   892
#1208 := (iff #1199 #1207)
himmelma@35172
   893
#1205 := (= #1198 #1204)
himmelma@35172
   894
#1206 := [rewrite]: #1205
himmelma@35172
   895
#1209 := [monotonicity #1206]: #1208
himmelma@35172
   896
#1215 := [trans #1209 #1213]: #1214
himmelma@35172
   897
#1218 := [monotonicity #1215]: #1217
himmelma@35172
   898
#1221 := [monotonicity #1218]: #1220
himmelma@35172
   899
#1226 := [monotonicity #1221]: #1225
himmelma@35172
   900
#1229 := [trans #1226 #1228]: #1225
himmelma@35172
   901
#1224 := [quant-inst]: #1223
himmelma@35172
   902
#1230 := [mp #1224 #1229]: #1222
himmelma@35172
   903
#1365 := [unit-resolution #1230 #600]: #1219
himmelma@35172
   904
#1232 := (or #1216 #1231)
himmelma@35172
   905
#1233 := [def-axiom]: #1232
himmelma@35172
   906
#1366 := [unit-resolution #1233 #1365]: #1231
himmelma@35172
   907
[th-lemma #1366 #1364 #1362]: false
himmelma@35172
   908
unsat
himmelma@35172
   909
NQHwTeL311Tq3wf2s5BReA 419 0
himmelma@35172
   910
#2 := false
himmelma@35172
   911
#194 := 0::real
himmelma@35172
   912
decl uf_4 :: (-> T2 T3 real)
himmelma@35172
   913
decl uf_6 :: (-> T1 T3)
himmelma@35172
   914
decl uf_3 :: T1
himmelma@35172
   915
#21 := uf_3
himmelma@35172
   916
#25 := (uf_6 uf_3)
himmelma@35172
   917
decl uf_5 :: T2
himmelma@35172
   918
#24 := uf_5
himmelma@35172
   919
#26 := (uf_4 uf_5 #25)
himmelma@35172
   920
decl uf_7 :: T2
himmelma@35172
   921
#27 := uf_7
himmelma@35172
   922
#28 := (uf_4 uf_7 #25)
himmelma@35172
   923
decl uf_10 :: T1
himmelma@35172
   924
#38 := uf_10
himmelma@35172
   925
#42 := (uf_6 uf_10)
himmelma@35172
   926
decl uf_9 :: T2
himmelma@35172
   927
#33 := uf_9
himmelma@35172
   928
#43 := (uf_4 uf_9 #42)
himmelma@35172
   929
#41 := (= uf_3 uf_10)
himmelma@35172
   930
#44 := (ite #41 #43 #28)
himmelma@35172
   931
#9 := 0::int
himmelma@35172
   932
decl uf_2 :: (-> T1 int)
himmelma@35172
   933
#39 := (uf_2 uf_10)
himmelma@35172
   934
#226 := -1::int
himmelma@35172
   935
#229 := (* -1::int #39)
himmelma@35172
   936
#22 := (uf_2 uf_3)
himmelma@35172
   937
#230 := (+ #22 #229)
himmelma@35172
   938
#228 := (>= #230 0::int)
himmelma@35172
   939
#236 := (ite #228 #44 #26)
himmelma@35172
   940
#192 := -1::real
himmelma@35172
   941
#244 := (* -1::real #236)
himmelma@35172
   942
#642 := (+ #26 #244)
himmelma@35172
   943
#643 := (<= #642 0::real)
himmelma@35172
   944
#567 := (= #26 #236)
himmelma@35172
   945
#227 := (not #228)
himmelma@35172
   946
decl uf_1 :: (-> int T1)
himmelma@35172
   947
#593 := (uf_1 #39)
himmelma@35172
   948
#660 := (= #593 uf_10)
himmelma@35172
   949
#594 := (= uf_10 #593)
himmelma@35172
   950
#4 := (:var 0 T1)
himmelma@35172
   951
#5 := (uf_2 #4)
himmelma@35172
   952
#546 := (pattern #5)
himmelma@35172
   953
#6 := (uf_1 #5)
himmelma@35172
   954
#93 := (= #4 #6)
himmelma@35172
   955
#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
himmelma@35172
   956
#96 := (forall (vars (?x1 T1)) #93)
himmelma@35172
   957
#550 := (iff #96 #547)
himmelma@35172
   958
#548 := (iff #93 #93)
himmelma@35172
   959
#549 := [refl]: #548
himmelma@35172
   960
#551 := [quant-intro #549]: #550
himmelma@35172
   961
#448 := (~ #96 #96)
himmelma@35172
   962
#450 := (~ #93 #93)
himmelma@35172
   963
#451 := [refl]: #450
himmelma@35172
   964
#449 := [nnf-pos #451]: #448
himmelma@35172
   965
#7 := (= #6 #4)
himmelma@35172
   966
#8 := (forall (vars (?x1 T1)) #7)
himmelma@35172
   967
#97 := (iff #8 #96)
himmelma@35172
   968
#94 := (iff #7 #93)
himmelma@35172
   969
#95 := [rewrite]: #94
himmelma@35172
   970
#98 := [quant-intro #95]: #97
himmelma@35172
   971
#92 := [asserted]: #8
himmelma@35172
   972
#101 := [mp #92 #98]: #96
himmelma@35172
   973
#446 := [mp~ #101 #449]: #96
himmelma@35172
   974
#552 := [mp #446 #551]: #547
himmelma@35172
   975
#595 := (not #547)
himmelma@35172
   976
#600 := (or #595 #594)
himmelma@35172
   977
#601 := [quant-inst]: #600
himmelma@35172
   978
#654 := [unit-resolution #601 #552]: #594
himmelma@35172
   979
#680 := [symm #654]: #660
himmelma@35172
   980
#681 := (= uf_3 #593)
himmelma@35172
   981
#591 := (uf_1 #22)
himmelma@35172
   982
#658 := (= #591 #593)
himmelma@35172
   983
#656 := (= #593 #591)
himmelma@35172
   984
#652 := (= #39 #22)
himmelma@35172
   985
#647 := (= #22 #39)
himmelma@35172
   986
#290 := (<= #230 0::int)
himmelma@35172
   987
#70 := (<= #22 #39)
himmelma@35172
   988
#388 := (iff #70 #290)
himmelma@35172
   989
#389 := [rewrite]: #388
himmelma@35172
   990
#341 := [asserted]: #70
himmelma@35172
   991
#390 := [mp #341 #389]: #290
himmelma@35172
   992
#646 := [hypothesis]: #228
himmelma@35172
   993
#648 := [th-lemma #646 #390]: #647
himmelma@35172
   994
#653 := [symm #648]: #652
himmelma@35172
   995
#657 := [monotonicity #653]: #656
himmelma@35172
   996
#659 := [symm #657]: #658
himmelma@35172
   997
#592 := (= uf_3 #591)
himmelma@35172
   998
#596 := (or #595 #592)
himmelma@35172
   999
#597 := [quant-inst]: #596
himmelma@35172
  1000
#655 := [unit-resolution #597 #552]: #592
himmelma@35172
  1001
#682 := [trans #655 #659]: #681
himmelma@35172
  1002
#683 := [trans #682 #680]: #41
himmelma@35172
  1003
#570 := (not #41)
himmelma@35172
  1004
decl uf_11 :: T2
himmelma@35172
  1005
#47 := uf_11
himmelma@35172
  1006
#59 := (uf_4 uf_11 #42)
himmelma@35172
  1007
#278 := (ite #41 #26 #59)
himmelma@35172
  1008
#459 := (* -1::real #278)
himmelma@35172
  1009
#637 := (+ #26 #459)
himmelma@35172
  1010
#639 := (>= #637 0::real)
himmelma@35172
  1011
#585 := (= #26 #278)
himmelma@35172
  1012
#661 := [hypothesis]: #41
himmelma@35172
  1013
#587 := (or #570 #585)
himmelma@35172
  1014
#588 := [def-axiom]: #587
himmelma@35172
  1015
#662 := [unit-resolution #588 #661]: #585
himmelma@35172
  1016
#663 := (not #585)
himmelma@35172
  1017
#664 := (or #663 #639)
himmelma@35172
  1018
#665 := [th-lemma]: #664
himmelma@35172
  1019
#666 := [unit-resolution #665 #662]: #639
himmelma@35172
  1020
decl uf_8 :: T2
himmelma@35172
  1021
#30 := uf_8
himmelma@35172
  1022
#56 := (uf_4 uf_8 #42)
himmelma@35172
  1023
#357 := (* -1::real #56)
himmelma@35172
  1024
#358 := (+ #43 #357)
himmelma@35172
  1025
#356 := (>= #358 0::real)
himmelma@35172
  1026
#355 := (not #356)
himmelma@35172
  1027
#374 := (* -1::real #59)
himmelma@35172
  1028
#375 := (+ #56 #374)
himmelma@35172
  1029
#373 := (>= #375 0::real)
himmelma@35172
  1030
#376 := (not #373)
himmelma@35172
  1031
#381 := (and #355 #376)
himmelma@35172
  1032
#64 := (< #39 #39)
himmelma@35172
  1033
#67 := (ite #64 #43 #59)
himmelma@35172
  1034
#68 := (< #56 #67)
himmelma@35172
  1035
#53 := (uf_4 uf_5 #42)
himmelma@35172
  1036
#65 := (ite #64 #53 #43)
himmelma@35172
  1037
#66 := (< #65 #56)
himmelma@35172
  1038
#69 := (and #66 #68)
himmelma@35172
  1039
#382 := (iff #69 #381)
himmelma@35172
  1040
#379 := (iff #68 #376)
himmelma@35172
  1041
#370 := (< #56 #59)
himmelma@35172
  1042
#377 := (iff #370 #376)
himmelma@35172
  1043
#378 := [rewrite]: #377
himmelma@35172
  1044
#371 := (iff #68 #370)
himmelma@35172
  1045
#368 := (= #67 #59)
himmelma@35172
  1046
#363 := (ite false #43 #59)
himmelma@35172
  1047
#366 := (= #363 #59)
himmelma@35172
  1048
#367 := [rewrite]: #366
himmelma@35172
  1049
#364 := (= #67 #363)
himmelma@35172
  1050
#343 := (iff #64 false)
himmelma@35172
  1051
#344 := [rewrite]: #343
himmelma@35172
  1052
#365 := [monotonicity #344]: #364
himmelma@35172
  1053
#369 := [trans #365 #367]: #368
himmelma@35172
  1054
#372 := [monotonicity #369]: #371
himmelma@35172
  1055
#380 := [trans #372 #378]: #379
himmelma@35172
  1056
#361 := (iff #66 #355)
himmelma@35172
  1057
#352 := (< #43 #56)
himmelma@35172
  1058
#359 := (iff #352 #355)
himmelma@35172
  1059
#360 := [rewrite]: #359
himmelma@35172
  1060
#353 := (iff #66 #352)
himmelma@35172
  1061
#350 := (= #65 #43)
himmelma@35172
  1062
#345 := (ite false #53 #43)
himmelma@35172
  1063
#348 := (= #345 #43)
himmelma@35172
  1064
#349 := [rewrite]: #348
himmelma@35172
  1065
#346 := (= #65 #345)
himmelma@35172
  1066
#347 := [monotonicity #344]: #346
himmelma@35172
  1067
#351 := [trans #347 #349]: #350
himmelma@35172
  1068
#354 := [monotonicity #351]: #353
himmelma@35172
  1069
#362 := [trans #354 #360]: #361
himmelma@35172
  1070
#383 := [monotonicity #362 #380]: #382
himmelma@35172
  1071
#340 := [asserted]: #69
himmelma@35172
  1072
#384 := [mp #340 #383]: #381
himmelma@35172
  1073
#385 := [and-elim #384]: #355
himmelma@35172
  1074
#394 := (* -1::real #53)
himmelma@35172
  1075
#395 := (+ #43 #394)
himmelma@35172
  1076
#393 := (>= #395 0::real)
himmelma@35172
  1077
#54 := (uf_4 uf_7 #42)
himmelma@35172
  1078
#402 := (* -1::real #54)
himmelma@35172
  1079
#403 := (+ #53 #402)
himmelma@35172
  1080
#401 := (>= #403 0::real)
himmelma@35172
  1081
#397 := (+ #43 #374)
himmelma@35172
  1082
#398 := (<= #397 0::real)
himmelma@35172
  1083
#412 := (and #393 #398 #401)
himmelma@35172
  1084
#73 := (<= #43 #59)
himmelma@35172
  1085
#72 := (<= #53 #43)
himmelma@35172
  1086
#74 := (and #72 #73)
himmelma@35172
  1087
#71 := (<= #54 #53)
himmelma@35172
  1088
#75 := (and #71 #74)
himmelma@35172
  1089
#415 := (iff #75 #412)
himmelma@35172
  1090
#406 := (and #393 #398)
himmelma@35172
  1091
#409 := (and #401 #406)
himmelma@35172
  1092
#413 := (iff #409 #412)
himmelma@35172
  1093
#414 := [rewrite]: #413
himmelma@35172
  1094
#410 := (iff #75 #409)
himmelma@35172
  1095
#407 := (iff #74 #406)
himmelma@35172
  1096
#399 := (iff #73 #398)
himmelma@35172
  1097
#400 := [rewrite]: #399
himmelma@35172
  1098
#392 := (iff #72 #393)
himmelma@35172
  1099
#396 := [rewrite]: #392
himmelma@35172
  1100
#408 := [monotonicity #396 #400]: #407
himmelma@35172
  1101
#404 := (iff #71 #401)
himmelma@35172
  1102
#405 := [rewrite]: #404
himmelma@35172
  1103
#411 := [monotonicity #405 #408]: #410
himmelma@35172
  1104
#416 := [trans #411 #414]: #415
himmelma@35172
  1105
#342 := [asserted]: #75
himmelma@35172
  1106
#417 := [mp #342 #416]: #412
himmelma@35172
  1107
#418 := [and-elim #417]: #393
himmelma@35172
  1108
#650 := (+ #26 #394)
himmelma@35172
  1109
#651 := (<= #650 0::real)
himmelma@35172
  1110
#649 := (= #26 #53)
himmelma@35172
  1111
#671 := (= #53 #26)
himmelma@35172
  1112
#669 := (= #42 #25)
himmelma@35172
  1113
#667 := (= #25 #42)
himmelma@35172
  1114
#668 := [monotonicity #661]: #667
himmelma@35172
  1115
#670 := [symm #668]: #669
himmelma@35172
  1116
#672 := [monotonicity #670]: #671
himmelma@35172
  1117
#673 := [symm #672]: #649
himmelma@35172
  1118
#674 := (not #649)
himmelma@35172
  1119
#675 := (or #674 #651)
himmelma@35172
  1120
#676 := [th-lemma]: #675
himmelma@35172
  1121
#677 := [unit-resolution #676 #673]: #651
himmelma@35172
  1122
#462 := (+ #56 #459)
himmelma@35172
  1123
#465 := (>= #462 0::real)
himmelma@35172
  1124
#438 := (not #465)
himmelma@35172
  1125
#316 := (ite #290 #278 #43)
himmelma@35172
  1126
#326 := (* -1::real #316)
himmelma@35172
  1127
#327 := (+ #56 #326)
himmelma@35172
  1128
#325 := (>= #327 0::real)
himmelma@35172
  1129
#324 := (not #325)
himmelma@35172
  1130
#439 := (iff #324 #438)
himmelma@35172
  1131
#466 := (iff #325 #465)
himmelma@35172
  1132
#463 := (= #327 #462)
himmelma@35172
  1133
#460 := (= #326 #459)
himmelma@35172
  1134
#457 := (= #316 #278)
himmelma@35172
  1135
#1 := true
himmelma@35172
  1136
#452 := (ite true #278 #43)
himmelma@35172
  1137
#455 := (= #452 #278)
himmelma@35172
  1138
#456 := [rewrite]: #455
himmelma@35172
  1139
#453 := (= #316 #452)
himmelma@35172
  1140
#444 := (iff #290 true)
himmelma@35172
  1141
#445 := [iff-true #390]: #444
himmelma@35172
  1142
#454 := [monotonicity #445]: #453
himmelma@35172
  1143
#458 := [trans #454 #456]: #457
himmelma@35172
  1144
#461 := [monotonicity #458]: #460
himmelma@35172
  1145
#464 := [monotonicity #461]: #463
himmelma@35172
  1146
#467 := [monotonicity #464]: #466
himmelma@35172
  1147
#468 := [monotonicity #467]: #439
himmelma@35172
  1148
#297 := (ite #290 #54 #53)
himmelma@35172
  1149
#305 := (* -1::real #297)
himmelma@35172
  1150
#306 := (+ #56 #305)
himmelma@35172
  1151
#307 := (<= #306 0::real)
himmelma@35172
  1152
#308 := (not #307)
himmelma@35172
  1153
#332 := (and #308 #324)
himmelma@35172
  1154
#58 := (= uf_10 uf_3)
himmelma@35172
  1155
#60 := (ite #58 #26 #59)
himmelma@35172
  1156
#52 := (< #39 #22)
himmelma@35172
  1157
#61 := (ite #52 #43 #60)
himmelma@35172
  1158
#62 := (< #56 #61)
himmelma@35172
  1159
#55 := (ite #52 #53 #54)
himmelma@35172
  1160
#57 := (< #55 #56)
himmelma@35172
  1161
#63 := (and #57 #62)
himmelma@35172
  1162
#335 := (iff #63 #332)
himmelma@35172
  1163
#281 := (ite #52 #43 #278)
himmelma@35172
  1164
#284 := (< #56 #281)
himmelma@35172
  1165
#287 := (and #57 #284)
himmelma@35172
  1166
#333 := (iff #287 #332)
himmelma@35172
  1167
#330 := (iff #284 #324)
himmelma@35172
  1168
#321 := (< #56 #316)
himmelma@35172
  1169
#328 := (iff #321 #324)
himmelma@35172
  1170
#329 := [rewrite]: #328
himmelma@35172
  1171
#322 := (iff #284 #321)
himmelma@35172
  1172
#319 := (= #281 #316)
himmelma@35172
  1173
#291 := (not #290)
himmelma@35172
  1174
#313 := (ite #291 #43 #278)
himmelma@35172
  1175
#317 := (= #313 #316)
himmelma@35172
  1176
#318 := [rewrite]: #317
himmelma@35172
  1177
#314 := (= #281 #313)
himmelma@35172
  1178
#292 := (iff #52 #291)
himmelma@35172
  1179
#293 := [rewrite]: #292
himmelma@35172
  1180
#315 := [monotonicity #293]: #314
himmelma@35172
  1181
#320 := [trans #315 #318]: #319
himmelma@35172
  1182
#323 := [monotonicity #320]: #322
himmelma@35172
  1183
#331 := [trans #323 #329]: #330
himmelma@35172
  1184
#311 := (iff #57 #308)
himmelma@35172
  1185
#302 := (< #297 #56)
himmelma@35172
  1186
#309 := (iff #302 #308)
himmelma@35172
  1187
#310 := [rewrite]: #309
himmelma@35172
  1188
#303 := (iff #57 #302)
himmelma@35172
  1189
#300 := (= #55 #297)
himmelma@35172
  1190
#294 := (ite #291 #53 #54)
himmelma@35172
  1191
#298 := (= #294 #297)
himmelma@35172
  1192
#299 := [rewrite]: #298
himmelma@35172
  1193
#295 := (= #55 #294)
himmelma@35172
  1194
#296 := [monotonicity #293]: #295
himmelma@35172
  1195
#301 := [trans #296 #299]: #300
himmelma@35172
  1196
#304 := [monotonicity #301]: #303
himmelma@35172
  1197
#312 := [trans #304 #310]: #311
himmelma@35172
  1198
#334 := [monotonicity #312 #331]: #333
himmelma@35172
  1199
#288 := (iff #63 #287)
himmelma@35172
  1200
#285 := (iff #62 #284)
himmelma@35172
  1201
#282 := (= #61 #281)
himmelma@35172
  1202
#279 := (= #60 #278)
himmelma@35172
  1203
#225 := (iff #58 #41)
himmelma@35172
  1204
#277 := [rewrite]: #225
himmelma@35172
  1205
#280 := [monotonicity #277]: #279
himmelma@35172
  1206
#283 := [monotonicity #280]: #282
himmelma@35172
  1207
#286 := [monotonicity #283]: #285
himmelma@35172
  1208
#289 := [monotonicity #286]: #288
himmelma@35172
  1209
#336 := [trans #289 #334]: #335
himmelma@35172
  1210
#179 := [asserted]: #63
himmelma@35172
  1211
#337 := [mp #179 #336]: #332
himmelma@35172
  1212
#339 := [and-elim #337]: #324
himmelma@35172
  1213
#469 := [mp #339 #468]: #438
himmelma@35172
  1214
#678 := [th-lemma #469 #677 #418 #385 #666]: false
himmelma@35172
  1215
#679 := [lemma #678]: #570
himmelma@35172
  1216
#684 := [unit-resolution #679 #683]: false
himmelma@35172
  1217
#685 := [lemma #684]: #227
himmelma@35172
  1218
#577 := (or #228 #567)
himmelma@35172
  1219
#578 := [def-axiom]: #577
himmelma@35172
  1220
#645 := [unit-resolution #578 #685]: #567
himmelma@35172
  1221
#686 := (not #567)
himmelma@35172
  1222
#687 := (or #686 #643)
himmelma@35172
  1223
#688 := [th-lemma]: #687
himmelma@35172
  1224
#689 := [unit-resolution #688 #645]: #643
himmelma@35172
  1225
#31 := (uf_4 uf_8 #25)
himmelma@35172
  1226
#245 := (+ #31 #244)
himmelma@35172
  1227
#246 := (<= #245 0::real)
himmelma@35172
  1228
#247 := (not #246)
himmelma@35172
  1229
#34 := (uf_4 uf_9 #25)
himmelma@35172
  1230
#48 := (uf_4 uf_11 #25)
himmelma@35172
  1231
#255 := (ite #228 #48 #34)
himmelma@35172
  1232
#264 := (* -1::real #255)
himmelma@35172
  1233
#265 := (+ #31 #264)
himmelma@35172
  1234
#263 := (>= #265 0::real)
himmelma@35172
  1235
#266 := (not #263)
himmelma@35172
  1236
#271 := (and #247 #266)
himmelma@35172
  1237
#40 := (< #22 #39)
himmelma@35172
  1238
#49 := (ite #40 #34 #48)
himmelma@35172
  1239
#50 := (< #31 #49)
himmelma@35172
  1240
#45 := (ite #40 #26 #44)
himmelma@35172
  1241
#46 := (< #45 #31)
himmelma@35172
  1242
#51 := (and #46 #50)
himmelma@35172
  1243
#272 := (iff #51 #271)
himmelma@35172
  1244
#269 := (iff #50 #266)
himmelma@35172
  1245
#260 := (< #31 #255)
himmelma@35172
  1246
#267 := (iff #260 #266)
himmelma@35172
  1247
#268 := [rewrite]: #267
himmelma@35172
  1248
#261 := (iff #50 #260)
himmelma@35172
  1249
#258 := (= #49 #255)
himmelma@35172
  1250
#252 := (ite #227 #34 #48)
himmelma@35172
  1251
#256 := (= #252 #255)
himmelma@35172
  1252
#257 := [rewrite]: #256
himmelma@35172
  1253
#253 := (= #49 #252)
himmelma@35172
  1254
#231 := (iff #40 #227)
himmelma@35172
  1255
#232 := [rewrite]: #231
himmelma@35172
  1256
#254 := [monotonicity #232]: #253
himmelma@35172
  1257
#259 := [trans #254 #257]: #258
himmelma@35172
  1258
#262 := [monotonicity #259]: #261
himmelma@35172
  1259
#270 := [trans #262 #268]: #269
himmelma@35172
  1260
#250 := (iff #46 #247)
himmelma@35172
  1261
#241 := (< #236 #31)
himmelma@35172
  1262
#248 := (iff #241 #247)
himmelma@35172
  1263
#249 := [rewrite]: #248
himmelma@35172
  1264
#242 := (iff #46 #241)
himmelma@35172
  1265
#239 := (= #45 #236)
himmelma@35172
  1266
#233 := (ite #227 #26 #44)
himmelma@35172
  1267
#237 := (= #233 #236)
himmelma@35172
  1268
#238 := [rewrite]: #237
himmelma@35172
  1269
#234 := (= #45 #233)
himmelma@35172
  1270
#235 := [monotonicity #232]: #234
himmelma@35172
  1271
#240 := [trans #235 #238]: #239
himmelma@35172
  1272
#243 := [monotonicity #240]: #242
himmelma@35172
  1273
#251 := [trans #243 #249]: #250
himmelma@35172
  1274
#273 := [monotonicity #251 #270]: #272
himmelma@35172
  1275
#178 := [asserted]: #51
himmelma@35172
  1276
#274 := [mp #178 #273]: #271
himmelma@35172
  1277
#275 := [and-elim #274]: #247
himmelma@35172
  1278
#196 := (* -1::real #31)
himmelma@35172
  1279
#212 := (+ #26 #196)
himmelma@35172
  1280
#213 := (<= #212 0::real)
himmelma@35172
  1281
#214 := (not #213)
himmelma@35172
  1282
#197 := (+ #28 #196)
himmelma@35172
  1283
#195 := (>= #197 0::real)
himmelma@35172
  1284
#193 := (not #195)
himmelma@35172
  1285
#219 := (and #193 #214)
himmelma@35172
  1286
#23 := (< #22 #22)
himmelma@35172
  1287
#35 := (ite #23 #34 #26)
himmelma@35172
  1288
#36 := (< #31 #35)
himmelma@35172
  1289
#29 := (ite #23 #26 #28)
himmelma@35172
  1290
#32 := (< #29 #31)
himmelma@35172
  1291
#37 := (and #32 #36)
himmelma@35172
  1292
#220 := (iff #37 #219)
himmelma@35172
  1293
#217 := (iff #36 #214)
himmelma@35172
  1294
#209 := (< #31 #26)
himmelma@35172
  1295
#215 := (iff #209 #214)
himmelma@35172
  1296
#216 := [rewrite]: #215
himmelma@35172
  1297
#210 := (iff #36 #209)
himmelma@35172
  1298
#207 := (= #35 #26)
himmelma@35172
  1299
#202 := (ite false #34 #26)
himmelma@35172
  1300
#205 := (= #202 #26)
himmelma@35172
  1301
#206 := [rewrite]: #205
himmelma@35172
  1302
#203 := (= #35 #202)
himmelma@35172
  1303
#180 := (iff #23 false)
himmelma@35172
  1304
#181 := [rewrite]: #180
himmelma@35172
  1305
#204 := [monotonicity #181]: #203
himmelma@35172
  1306
#208 := [trans #204 #206]: #207
himmelma@35172
  1307
#211 := [monotonicity #208]: #210
himmelma@35172
  1308
#218 := [trans #211 #216]: #217
himmelma@35172
  1309
#200 := (iff #32 #193)
himmelma@35172
  1310
#189 := (< #28 #31)
himmelma@35172
  1311
#198 := (iff #189 #193)
himmelma@35172
  1312
#199 := [rewrite]: #198
himmelma@35172
  1313
#190 := (iff #32 #189)
himmelma@35172
  1314
#187 := (= #29 #28)
himmelma@35172
  1315
#182 := (ite false #26 #28)
himmelma@35172
  1316
#185 := (= #182 #28)
himmelma@35172
  1317
#186 := [rewrite]: #185
himmelma@35172
  1318
#183 := (= #29 #182)
himmelma@35172
  1319
#184 := [monotonicity #181]: #183
himmelma@35172
  1320
#188 := [trans #184 #186]: #187
himmelma@35172
  1321
#191 := [monotonicity #188]: #190
himmelma@35172
  1322
#201 := [trans #191 #199]: #200
himmelma@35172
  1323
#221 := [monotonicity #201 #218]: #220
himmelma@35172
  1324
#177 := [asserted]: #37
himmelma@35172
  1325
#222 := [mp #177 #221]: #219
himmelma@35172
  1326
#224 := [and-elim #222]: #214
himmelma@35172
  1327
[th-lemma #224 #275 #689]: false
himmelma@35172
  1328
unsat
himmelma@35172
  1329
NX/HT1QOfbspC2LtZNKpBA 428 0
himmelma@35172
  1330
#2 := false
himmelma@35172
  1331
decl uf_10 :: T1
himmelma@35172
  1332
#38 := uf_10
himmelma@35172
  1333
decl uf_3 :: T1
himmelma@35172
  1334
#21 := uf_3
himmelma@35172
  1335
#45 := (= uf_3 uf_10)
himmelma@35172
  1336
decl uf_1 :: (-> int T1)
himmelma@35172
  1337
decl uf_2 :: (-> T1 int)
himmelma@35172
  1338
#39 := (uf_2 uf_10)
himmelma@35172
  1339
#588 := (uf_1 #39)
himmelma@35172
  1340
#686 := (= #588 uf_10)
himmelma@35172
  1341
#589 := (= uf_10 #588)
himmelma@35172
  1342
#4 := (:var 0 T1)
himmelma@35172
  1343
#5 := (uf_2 #4)
himmelma@35172
  1344
#541 := (pattern #5)
himmelma@35172
  1345
#6 := (uf_1 #5)
himmelma@35172
  1346
#93 := (= #4 #6)
himmelma@35172
  1347
#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
himmelma@35172
  1348
#96 := (forall (vars (?x1 T1)) #93)
himmelma@35172
  1349
#545 := (iff #96 #542)
himmelma@35172
  1350
#543 := (iff #93 #93)
himmelma@35172
  1351
#544 := [refl]: #543
himmelma@35172
  1352
#546 := [quant-intro #544]: #545
himmelma@35172
  1353
#454 := (~ #96 #96)
himmelma@35172
  1354
#456 := (~ #93 #93)
himmelma@35172
  1355
#457 := [refl]: #456
himmelma@35172
  1356
#455 := [nnf-pos #457]: #454
himmelma@35172
  1357
#7 := (= #6 #4)
himmelma@35172
  1358
#8 := (forall (vars (?x1 T1)) #7)
himmelma@35172
  1359
#97 := (iff #8 #96)
himmelma@35172
  1360
#94 := (iff #7 #93)
himmelma@35172
  1361
#95 := [rewrite]: #94
himmelma@35172
  1362
#98 := [quant-intro #95]: #97
himmelma@35172
  1363
#92 := [asserted]: #8
himmelma@35172
  1364
#101 := [mp #92 #98]: #96
himmelma@35172
  1365
#452 := [mp~ #101 #455]: #96
himmelma@35172
  1366
#547 := [mp #452 #546]: #542
himmelma@35172
  1367
#590 := (not #542)
himmelma@35172
  1368
#595 := (or #590 #589)
himmelma@35172
  1369
#596 := [quant-inst]: #595
himmelma@35172
  1370
#680 := [unit-resolution #596 #547]: #589
himmelma@35172
  1371
#687 := [symm #680]: #686
himmelma@35172
  1372
#688 := (= uf_3 #588)
himmelma@35172
  1373
#22 := (uf_2 uf_3)
himmelma@35172
  1374
#586 := (uf_1 #22)
himmelma@35172
  1375
#684 := (= #586 #588)
himmelma@35172
  1376
#682 := (= #588 #586)
himmelma@35172
  1377
#678 := (= #39 #22)
himmelma@35172
  1378
#676 := (= #22 #39)
himmelma@35172
  1379
#9 := 0::int
himmelma@35172
  1380
#227 := -1::int
himmelma@35172
  1381
#230 := (* -1::int #39)
himmelma@35172
  1382
#231 := (+ #22 #230)
himmelma@35172
  1383
#296 := (<= #231 0::int)
himmelma@35172
  1384
#70 := (<= #22 #39)
himmelma@35172
  1385
#393 := (iff #70 #296)
himmelma@35172
  1386
#394 := [rewrite]: #393
himmelma@35172
  1387
#347 := [asserted]: #70
himmelma@35172
  1388
#395 := [mp #347 #394]: #296
himmelma@35172
  1389
#229 := (>= #231 0::int)
himmelma@35172
  1390
decl uf_4 :: (-> T2 T3 real)
himmelma@35172
  1391
decl uf_6 :: (-> T1 T3)
himmelma@35172
  1392
#25 := (uf_6 uf_3)
himmelma@35172
  1393
decl uf_7 :: T2
himmelma@35172
  1394
#27 := uf_7
himmelma@35172
  1395
#28 := (uf_4 uf_7 #25)
himmelma@35172
  1396
decl uf_9 :: T2
himmelma@35172
  1397
#33 := uf_9
himmelma@35172
  1398
#34 := (uf_4 uf_9 #25)
himmelma@35172
  1399
#46 := (uf_6 uf_10)
himmelma@35172
  1400
decl uf_5 :: T2
himmelma@35172
  1401
#24 := uf_5
himmelma@35172
  1402
#47 := (uf_4 uf_5 #46)
himmelma@35172
  1403
#48 := (ite #45 #47 #34)
himmelma@35172
  1404
#256 := (ite #229 #48 #28)
himmelma@35172
  1405
#568 := (= #28 #256)
himmelma@35172
  1406
#648 := (not #568)
himmelma@35172
  1407
#194 := 0::real
himmelma@35172
  1408
#192 := -1::real
himmelma@35172
  1409
#265 := (* -1::real #256)
himmelma@35172
  1410
#640 := (+ #28 #265)
himmelma@35172
  1411
#642 := (>= #640 0::real)
himmelma@35172
  1412
#645 := (not #642)
himmelma@35172
  1413
#643 := [hypothesis]: #642
himmelma@35172
  1414
decl uf_8 :: T2
himmelma@35172
  1415
#30 := uf_8
himmelma@35172
  1416
#31 := (uf_4 uf_8 #25)
himmelma@35172
  1417
#266 := (+ #31 #265)
himmelma@35172
  1418
#264 := (>= #266 0::real)
himmelma@35172
  1419
#267 := (not #264)
himmelma@35172
  1420
#26 := (uf_4 uf_5 #25)
himmelma@35172
  1421
decl uf_11 :: T2
himmelma@35172
  1422
#41 := uf_11
himmelma@35172
  1423
#42 := (uf_4 uf_11 #25)
himmelma@35172
  1424
#237 := (ite #229 #42 #26)
himmelma@35172
  1425
#245 := (* -1::real #237)
himmelma@35172
  1426
#246 := (+ #31 #245)
himmelma@35172
  1427
#247 := (<= #246 0::real)
himmelma@35172
  1428
#248 := (not #247)
himmelma@35172
  1429
#272 := (and #248 #267)
himmelma@35172
  1430
#40 := (< #22 #39)
himmelma@35172
  1431
#49 := (ite #40 #28 #48)
himmelma@35172
  1432
#50 := (< #31 #49)
himmelma@35172
  1433
#43 := (ite #40 #26 #42)
himmelma@35172
  1434
#44 := (< #43 #31)
himmelma@35172
  1435
#51 := (and #44 #50)
himmelma@35172
  1436
#273 := (iff #51 #272)
himmelma@35172
  1437
#270 := (iff #50 #267)
himmelma@35172
  1438
#261 := (< #31 #256)
himmelma@35172
  1439
#268 := (iff #261 #267)
himmelma@35172
  1440
#269 := [rewrite]: #268
himmelma@35172
  1441
#262 := (iff #50 #261)
himmelma@35172
  1442
#259 := (= #49 #256)
himmelma@35172
  1443
#228 := (not #229)
himmelma@35172
  1444
#253 := (ite #228 #28 #48)
himmelma@35172
  1445
#257 := (= #253 #256)
himmelma@35172
  1446
#258 := [rewrite]: #257
himmelma@35172
  1447
#254 := (= #49 #253)
himmelma@35172
  1448
#232 := (iff #40 #228)
himmelma@35172
  1449
#233 := [rewrite]: #232
himmelma@35172
  1450
#255 := [monotonicity #233]: #254
himmelma@35172
  1451
#260 := [trans #255 #258]: #259
himmelma@35172
  1452
#263 := [monotonicity #260]: #262
himmelma@35172
  1453
#271 := [trans #263 #269]: #270
himmelma@35172
  1454
#251 := (iff #44 #248)
himmelma@35172
  1455
#242 := (< #237 #31)
himmelma@35172
  1456
#249 := (iff #242 #248)
himmelma@35172
  1457
#250 := [rewrite]: #249
himmelma@35172
  1458
#243 := (iff #44 #242)
himmelma@35172
  1459
#240 := (= #43 #237)
himmelma@35172
  1460
#234 := (ite #228 #26 #42)
himmelma@35172
  1461
#238 := (= #234 #237)
himmelma@35172
  1462
#239 := [rewrite]: #238
himmelma@35172
  1463
#235 := (= #43 #234)
himmelma@35172
  1464
#236 := [monotonicity #233]: #235
himmelma@35172
  1465
#241 := [trans #236 #239]: #240
himmelma@35172
  1466
#244 := [monotonicity #241]: #243
himmelma@35172
  1467
#252 := [trans #244 #250]: #251
himmelma@35172
  1468
#274 := [monotonicity #252 #271]: #273
himmelma@35172
  1469
#178 := [asserted]: #51
himmelma@35172
  1470
#275 := [mp #178 #274]: #272
himmelma@35172
  1471
#277 := [and-elim #275]: #267
himmelma@35172
  1472
#196 := (* -1::real #31)
himmelma@35172
  1473
#197 := (+ #28 #196)
himmelma@35172
  1474
#195 := (>= #197 0::real)
himmelma@35172
  1475
#193 := (not #195)
himmelma@35172
  1476
#213 := (* -1::real #34)
himmelma@35172
  1477
#214 := (+ #31 #213)
himmelma@35172
  1478
#212 := (>= #214 0::real)
himmelma@35172
  1479
#215 := (not #212)
himmelma@35172
  1480
#220 := (and #193 #215)
himmelma@35172
  1481
#23 := (< #22 #22)
himmelma@35172
  1482
#35 := (ite #23 #28 #34)
himmelma@35172
  1483
#36 := (< #31 #35)
himmelma@35172
  1484
#29 := (ite #23 #26 #28)
himmelma@35172
  1485
#32 := (< #29 #31)
himmelma@35172
  1486
#37 := (and #32 #36)
himmelma@35172
  1487
#221 := (iff #37 #220)
himmelma@35172
  1488
#218 := (iff #36 #215)
himmelma@35172
  1489
#209 := (< #31 #34)
himmelma@35172
  1490
#216 := (iff #209 #215)
himmelma@35172
  1491
#217 := [rewrite]: #216
himmelma@35172
  1492
#210 := (iff #36 #209)
himmelma@35172
  1493
#207 := (= #35 #34)
himmelma@35172
  1494
#202 := (ite false #28 #34)
himmelma@35172
  1495
#205 := (= #202 #34)
himmelma@35172
  1496
#206 := [rewrite]: #205
himmelma@35172
  1497
#203 := (= #35 #202)
himmelma@35172
  1498
#180 := (iff #23 false)
himmelma@35172
  1499
#181 := [rewrite]: #180
himmelma@35172
  1500
#204 := [monotonicity #181]: #203
himmelma@35172
  1501
#208 := [trans #204 #206]: #207
himmelma@35172
  1502
#211 := [monotonicity #208]: #210
himmelma@35172
  1503
#219 := [trans #211 #217]: #218
himmelma@35172
  1504
#200 := (iff #32 #193)
himmelma@35172
  1505
#189 := (< #28 #31)
himmelma@35172
  1506
#198 := (iff #189 #193)
himmelma@35172
  1507
#199 := [rewrite]: #198
himmelma@35172
  1508
#190 := (iff #32 #189)
himmelma@35172
  1509
#187 := (= #29 #28)
himmelma@35172
  1510
#182 := (ite false #26 #28)
himmelma@35172
  1511
#185 := (= #182 #28)
himmelma@35172
  1512
#186 := [rewrite]: #185
himmelma@35172
  1513
#183 := (= #29 #182)
himmelma@35172
  1514
#184 := [monotonicity #181]: #183
himmelma@35172
  1515
#188 := [trans #184 #186]: #187
himmelma@35172
  1516
#191 := [monotonicity #188]: #190
himmelma@35172
  1517
#201 := [trans #191 #199]: #200
himmelma@35172
  1518
#222 := [monotonicity #201 #219]: #221
himmelma@35172
  1519
#177 := [asserted]: #37
himmelma@35172
  1520
#223 := [mp #177 #222]: #220
himmelma@35172
  1521
#224 := [and-elim #223]: #193
himmelma@35172
  1522
#644 := [th-lemma #224 #277 #643]: false
himmelma@35172
  1523
#646 := [lemma #644]: #645
himmelma@35172
  1524
#647 := [hypothesis]: #568
himmelma@35172
  1525
#649 := (or #648 #642)
himmelma@35172
  1526
#650 := [th-lemma]: #649
himmelma@35172
  1527
#651 := [unit-resolution #650 #647 #646]: false
himmelma@35172
  1528
#652 := [lemma #651]: #648
himmelma@35172
  1529
#578 := (or #229 #568)
himmelma@35172
  1530
#579 := [def-axiom]: #578
himmelma@35172
  1531
#675 := [unit-resolution #579 #652]: #229
himmelma@35172
  1532
#677 := [th-lemma #675 #395]: #676
himmelma@35172
  1533
#679 := [symm #677]: #678
himmelma@35172
  1534
#683 := [monotonicity #679]: #682
himmelma@35172
  1535
#685 := [symm #683]: #684
himmelma@35172
  1536
#587 := (= uf_3 #586)
himmelma@35172
  1537
#591 := (or #590 #587)
himmelma@35172
  1538
#592 := [quant-inst]: #591
himmelma@35172
  1539
#681 := [unit-resolution #592 #547]: #587
himmelma@35172
  1540
#689 := [trans #681 #685]: #688
himmelma@35172
  1541
#690 := [trans #689 #687]: #45
himmelma@35172
  1542
#571 := (not #45)
himmelma@35172
  1543
#54 := (uf_4 uf_11 #46)
himmelma@35172
  1544
#279 := (ite #45 #28 #54)
himmelma@35172
  1545
#465 := (* -1::real #279)
himmelma@35172
  1546
#632 := (+ #28 #465)
himmelma@35172
  1547
#633 := (<= #632 0::real)
himmelma@35172
  1548
#580 := (= #28 #279)
himmelma@35172
  1549
#656 := [hypothesis]: #45
himmelma@35172
  1550
#582 := (or #571 #580)
himmelma@35172
  1551
#583 := [def-axiom]: #582
himmelma@35172
  1552
#657 := [unit-resolution #583 #656]: #580
himmelma@35172
  1553
#658 := (not #580)
himmelma@35172
  1554
#659 := (or #658 #633)
himmelma@35172
  1555
#660 := [th-lemma]: #659
himmelma@35172
  1556
#661 := [unit-resolution #660 #657]: #633
himmelma@35172
  1557
#57 := (uf_4 uf_8 #46)
himmelma@35172
  1558
#363 := (* -1::real #57)
himmelma@35172
  1559
#379 := (+ #47 #363)
himmelma@35172
  1560
#380 := (<= #379 0::real)
himmelma@35172
  1561
#381 := (not #380)
himmelma@35172
  1562
#364 := (+ #54 #363)
himmelma@35172
  1563
#362 := (>= #364 0::real)
himmelma@35172
  1564
#361 := (not #362)
himmelma@35172
  1565
#386 := (and #361 #381)
himmelma@35172
  1566
#59 := (uf_4 uf_7 #46)
himmelma@35172
  1567
#64 := (< #39 #39)
himmelma@35172
  1568
#67 := (ite #64 #59 #47)
himmelma@35172
  1569
#68 := (< #57 #67)
himmelma@35172
  1570
#65 := (ite #64 #47 #54)
himmelma@35172
  1571
#66 := (< #65 #57)
himmelma@35172
  1572
#69 := (and #66 #68)
himmelma@35172
  1573
#387 := (iff #69 #386)
himmelma@35172
  1574
#384 := (iff #68 #381)
himmelma@35172
  1575
#376 := (< #57 #47)
himmelma@35172
  1576
#382 := (iff #376 #381)
himmelma@35172
  1577
#383 := [rewrite]: #382
himmelma@35172
  1578
#377 := (iff #68 #376)
himmelma@35172
  1579
#374 := (= #67 #47)
himmelma@35172
  1580
#369 := (ite false #59 #47)
himmelma@35172
  1581
#372 := (= #369 #47)
himmelma@35172
  1582
#373 := [rewrite]: #372
himmelma@35172
  1583
#370 := (= #67 #369)
himmelma@35172
  1584
#349 := (iff #64 false)
himmelma@35172
  1585
#350 := [rewrite]: #349
himmelma@35172
  1586
#371 := [monotonicity #350]: #370
himmelma@35172
  1587
#375 := [trans #371 #373]: #374
himmelma@35172
  1588
#378 := [monotonicity #375]: #377
himmelma@35172
  1589
#385 := [trans #378 #383]: #384
himmelma@35172
  1590
#367 := (iff #66 #361)
himmelma@35172
  1591
#358 := (< #54 #57)
himmelma@35172
  1592
#365 := (iff #358 #361)
himmelma@35172
  1593
#366 := [rewrite]: #365
himmelma@35172
  1594
#359 := (iff #66 #358)
himmelma@35172
  1595
#356 := (= #65 #54)
himmelma@35172
  1596
#351 := (ite false #47 #54)
himmelma@35172
  1597
#354 := (= #351 #54)
himmelma@35172
  1598
#355 := [rewrite]: #354
himmelma@35172
  1599
#352 := (= #65 #351)
himmelma@35172
  1600
#353 := [monotonicity #350]: #352
himmelma@35172
  1601
#357 := [trans #353 #355]: #356
himmelma@35172
  1602
#360 := [monotonicity #357]: #359
himmelma@35172
  1603
#368 := [trans #360 #366]: #367
himmelma@35172
  1604
#388 := [monotonicity #368 #385]: #387
himmelma@35172
  1605
#346 := [asserted]: #69
himmelma@35172
  1606
#389 := [mp #346 #388]: #386
himmelma@35172
  1607
#391 := [and-elim #389]: #381
himmelma@35172
  1608
#397 := (* -1::real #59)
himmelma@35172
  1609
#398 := (+ #47 #397)
himmelma@35172
  1610
#399 := (<= #398 0::real)
himmelma@35172
  1611
#409 := (* -1::real #54)
himmelma@35172
  1612
#410 := (+ #47 #409)
himmelma@35172
  1613
#408 := (>= #410 0::real)
himmelma@35172
  1614
#60 := (uf_4 uf_9 #46)
himmelma@35172
  1615
#402 := (* -1::real #60)
himmelma@35172
  1616
#403 := (+ #59 #402)
himmelma@35172
  1617
#404 := (<= #403 0::real)
himmelma@35172
  1618
#418 := (and #399 #404 #408)
himmelma@35172
  1619
#73 := (<= #59 #60)
himmelma@35172
  1620
#72 := (<= #47 #59)
himmelma@35172
  1621
#74 := (and #72 #73)
himmelma@35172
  1622
#71 := (<= #54 #47)
himmelma@35172
  1623
#75 := (and #71 #74)
himmelma@35172
  1624
#421 := (iff #75 #418)
himmelma@35172
  1625
#412 := (and #399 #404)
himmelma@35172
  1626
#415 := (and #408 #412)
himmelma@35172
  1627
#419 := (iff #415 #418)
himmelma@35172
  1628
#420 := [rewrite]: #419
himmelma@35172
  1629
#416 := (iff #75 #415)
himmelma@35172
  1630
#413 := (iff #74 #412)
himmelma@35172
  1631
#405 := (iff #73 #404)
himmelma@35172
  1632
#406 := [rewrite]: #405
himmelma@35172
  1633
#400 := (iff #72 #399)
himmelma@35172
  1634
#401 := [rewrite]: #400
himmelma@35172
  1635
#414 := [monotonicity #401 #406]: #413
himmelma@35172
  1636
#407 := (iff #71 #408)
himmelma@35172
  1637
#411 := [rewrite]: #407
himmelma@35172
  1638
#417 := [monotonicity #411 #414]: #416
himmelma@35172
  1639
#422 := [trans #417 #420]: #421
himmelma@35172
  1640
#348 := [asserted]: #75
himmelma@35172
  1641
#423 := [mp #348 #422]: #418
himmelma@35172
  1642
#424 := [and-elim #423]: #399
himmelma@35172
  1643
#637 := (+ #28 #397)
himmelma@35172
  1644
#639 := (>= #637 0::real)
himmelma@35172
  1645
#636 := (= #28 #59)
himmelma@35172
  1646
#666 := (= #59 #28)
himmelma@35172
  1647
#664 := (= #46 #25)
himmelma@35172
  1648
#662 := (= #25 #46)
himmelma@35172
  1649
#663 := [monotonicity #656]: #662
himmelma@35172
  1650
#665 := [symm #663]: #664
himmelma@35172
  1651
#667 := [monotonicity #665]: #666
himmelma@35172
  1652
#668 := [symm #667]: #636
himmelma@35172
  1653
#669 := (not #636)
himmelma@35172
  1654
#670 := (or #669 #639)
himmelma@35172
  1655
#671 := [th-lemma]: #670
himmelma@35172
  1656
#672 := [unit-resolution #671 #668]: #639
himmelma@35172
  1657
#468 := (+ #57 #465)
himmelma@35172
  1658
#471 := (<= #468 0::real)
himmelma@35172
  1659
#444 := (not #471)
himmelma@35172
  1660
#322 := (ite #296 #279 #47)
himmelma@35172
  1661
#330 := (* -1::real #322)
himmelma@35172
  1662
#331 := (+ #57 #330)
himmelma@35172
  1663
#332 := (<= #331 0::real)
himmelma@35172
  1664
#333 := (not #332)
himmelma@35172
  1665
#445 := (iff #333 #444)
himmelma@35172
  1666
#472 := (iff #332 #471)
himmelma@35172
  1667
#469 := (= #331 #468)
himmelma@35172
  1668
#466 := (= #330 #465)
himmelma@35172
  1669
#463 := (= #322 #279)
himmelma@35172
  1670
#1 := true
himmelma@35172
  1671
#458 := (ite true #279 #47)
himmelma@35172
  1672
#461 := (= #458 #279)
himmelma@35172
  1673
#462 := [rewrite]: #461
himmelma@35172
  1674
#459 := (= #322 #458)
himmelma@35172
  1675
#450 := (iff #296 true)
himmelma@35172
  1676
#451 := [iff-true #395]: #450
himmelma@35172
  1677
#460 := [monotonicity #451]: #459
himmelma@35172
  1678
#464 := [trans #460 #462]: #463
himmelma@35172
  1679
#467 := [monotonicity #464]: #466
himmelma@35172
  1680
#470 := [monotonicity #467]: #469
himmelma@35172
  1681
#473 := [monotonicity #470]: #472
himmelma@35172
  1682
#474 := [monotonicity #473]: #445
himmelma@35172
  1683
#303 := (ite #296 #60 #59)
himmelma@35172
  1684
#313 := (* -1::real #303)
himmelma@35172
  1685
#314 := (+ #57 #313)
himmelma@35172
  1686
#312 := (>= #314 0::real)
himmelma@35172
  1687
#311 := (not #312)
himmelma@35172
  1688
#338 := (and #311 #333)
himmelma@35172
  1689
#52 := (< #39 #22)
himmelma@35172
  1690
#61 := (ite #52 #59 #60)
himmelma@35172
  1691
#62 := (< #57 #61)
himmelma@35172
  1692
#53 := (= uf_10 uf_3)
himmelma@35172
  1693
#55 := (ite #53 #28 #54)
himmelma@35172
  1694
#56 := (ite #52 #47 #55)
himmelma@35172
  1695
#58 := (< #56 #57)
himmelma@35172
  1696
#63 := (and #58 #62)
himmelma@35172
  1697
#341 := (iff #63 #338)
himmelma@35172
  1698
#282 := (ite #52 #47 #279)
himmelma@35172
  1699
#285 := (< #282 #57)
himmelma@35172
  1700
#291 := (and #62 #285)
himmelma@35172
  1701
#339 := (iff #291 #338)
himmelma@35172
  1702
#336 := (iff #285 #333)
himmelma@35172
  1703
#327 := (< #322 #57)
himmelma@35172
  1704
#334 := (iff #327 #333)
himmelma@35172
  1705
#335 := [rewrite]: #334
himmelma@35172
  1706
#328 := (iff #285 #327)
himmelma@35172
  1707
#325 := (= #282 #322)
himmelma@35172
  1708
#297 := (not #296)
himmelma@35172
  1709
#319 := (ite #297 #47 #279)
himmelma@35172
  1710
#323 := (= #319 #322)
himmelma@35172
  1711
#324 := [rewrite]: #323
himmelma@35172
  1712
#320 := (= #282 #319)
himmelma@35172
  1713
#298 := (iff #52 #297)
himmelma@35172
  1714
#299 := [rewrite]: #298
himmelma@35172
  1715
#321 := [monotonicity #299]: #320
himmelma@35172
  1716
#326 := [trans #321 #324]: #325
himmelma@35172
  1717
#329 := [monotonicity #326]: #328
himmelma@35172
  1718
#337 := [trans #329 #335]: #336
himmelma@35172
  1719
#317 := (iff #62 #311)
himmelma@35172
  1720
#308 := (< #57 #303)
himmelma@35172
  1721
#315 := (iff #308 #311)
himmelma@35172
  1722
#316 := [rewrite]: #315
himmelma@35172
  1723
#309 := (iff #62 #308)
himmelma@35172
  1724
#306 := (= #61 #303)
himmelma@35172
  1725
#300 := (ite #297 #59 #60)
himmelma@35172
  1726
#304 := (= #300 #303)
himmelma@35172
  1727
#305 := [rewrite]: #304
himmelma@35172
  1728
#301 := (= #61 #300)
himmelma@35172
  1729
#302 := [monotonicity #299]: #301
himmelma@35172
  1730
#307 := [trans #302 #305]: #306
himmelma@35172
  1731
#310 := [monotonicity #307]: #309
himmelma@35172
  1732
#318 := [trans #310 #316]: #317
himmelma@35172
  1733
#340 := [monotonicity #318 #337]: #339
himmelma@35172
  1734
#294 := (iff #63 #291)
himmelma@35172
  1735
#288 := (and #285 #62)
himmelma@35172
  1736
#292 := (iff #288 #291)
himmelma@35172
  1737
#293 := [rewrite]: #292
himmelma@35172
  1738
#289 := (iff #63 #288)
himmelma@35172
  1739
#286 := (iff #58 #285)
himmelma@35172
  1740
#283 := (= #56 #282)
himmelma@35172
  1741
#280 := (= #55 #279)
himmelma@35172
  1742
#226 := (iff #53 #45)
himmelma@35172
  1743
#278 := [rewrite]: #226
himmelma@35172
  1744
#281 := [monotonicity #278]: #280
himmelma@35172
  1745
#284 := [monotonicity #281]: #283
himmelma@35172
  1746
#287 := [monotonicity #284]: #286
himmelma@35172
  1747
#290 := [monotonicity #287]: #289
himmelma@35172
  1748
#295 := [trans #290 #293]: #294
himmelma@35172
  1749
#342 := [trans #295 #340]: #341
himmelma@35172
  1750
#179 := [asserted]: #63
himmelma@35172
  1751
#343 := [mp #179 #342]: #338
himmelma@35172
  1752
#345 := [and-elim #343]: #333
himmelma@35172
  1753
#475 := [mp #345 #474]: #444
himmelma@35172
  1754
#673 := [th-lemma #475 #672 #424 #391 #661]: false
himmelma@35172
  1755
#674 := [lemma #673]: #571
himmelma@35172
  1756
[unit-resolution #674 #690]: false
himmelma@35172
  1757
unsat
himmelma@35172
  1758
IL2powemHjRpCJYwmXFxyw 211 0
himmelma@35172
  1759
#2 := false
himmelma@35172
  1760
#33 := 0::real
himmelma@35172
  1761
decl uf_11 :: (-> T5 T6 real)
himmelma@35172
  1762
decl uf_15 :: T6
himmelma@35172
  1763
#28 := uf_15
himmelma@35172
  1764
decl uf_16 :: T5
himmelma@35172
  1765
#30 := uf_16
himmelma@35172
  1766
#31 := (uf_11 uf_16 uf_15)
himmelma@35172
  1767
decl uf_12 :: (-> T7 T8 T5)
himmelma@35172
  1768
decl uf_14 :: T8
himmelma@35172
  1769
#26 := uf_14
himmelma@35172
  1770
decl uf_13 :: (-> T1 T7)
himmelma@35172
  1771
decl uf_8 :: T1
himmelma@35172
  1772
#16 := uf_8
himmelma@35172
  1773
#25 := (uf_13 uf_8)
himmelma@35172
  1774
#27 := (uf_12 #25 uf_14)
himmelma@35172
  1775
#29 := (uf_11 #27 uf_15)
himmelma@35172
  1776
#73 := -1::real
himmelma@35172
  1777
#84 := (* -1::real #29)
himmelma@35172
  1778
#85 := (+ #84 #31)
himmelma@35172
  1779
#74 := (* -1::real #31)
himmelma@35172
  1780
#75 := (+ #29 #74)
himmelma@35172
  1781
#112 := (>= #75 0::real)
himmelma@35172
  1782
#119 := (ite #112 #75 #85)
himmelma@35172
  1783
#127 := (* -1::real #119)
himmelma@35172
  1784
decl uf_17 :: T5
himmelma@35172
  1785
#37 := uf_17
himmelma@35172
  1786
#38 := (uf_11 uf_17 uf_15)
himmelma@35172
  1787
#102 := -1/3::real
himmelma@35172
  1788
#103 := (* -1/3::real #38)
himmelma@35172
  1789
#128 := (+ #103 #127)
himmelma@35172
  1790
#100 := 1/3::real
himmelma@35172
  1791
#101 := (* 1/3::real #31)
himmelma@35172
  1792
#129 := (+ #101 #128)
himmelma@35172
  1793
#130 := (<= #129 0::real)
himmelma@35172
  1794
#131 := (not #130)
himmelma@35172
  1795
#40 := 3::real
himmelma@35172
  1796
#39 := (- #31 #38)
himmelma@35172
  1797
#41 := (/ #39 3::real)
himmelma@35172
  1798
#32 := (- #29 #31)
himmelma@35172
  1799
#35 := (- #32)
himmelma@35172
  1800
#34 := (< #32 0::real)
himmelma@35172
  1801
#36 := (ite #34 #35 #32)
himmelma@35172
  1802
#42 := (< #36 #41)
himmelma@35172
  1803
#136 := (iff #42 #131)
himmelma@35172
  1804
#104 := (+ #101 #103)
himmelma@35172
  1805
#78 := (< #75 0::real)
himmelma@35172
  1806
#90 := (ite #78 #85 #75)
himmelma@35172
  1807
#109 := (< #90 #104)
himmelma@35172
  1808
#134 := (iff #109 #131)
himmelma@35172
  1809
#124 := (< #119 #104)
himmelma@35172
  1810
#132 := (iff #124 #131)
himmelma@35172
  1811
#133 := [rewrite]: #132
himmelma@35172
  1812
#125 := (iff #109 #124)
himmelma@35172
  1813
#122 := (= #90 #119)
himmelma@35172
  1814
#113 := (not #112)
himmelma@35172
  1815
#116 := (ite #113 #85 #75)
himmelma@35172
  1816
#120 := (= #116 #119)
himmelma@35172
  1817
#121 := [rewrite]: #120
himmelma@35172
  1818
#117 := (= #90 #116)
himmelma@35172
  1819
#114 := (iff #78 #113)
himmelma@35172
  1820
#115 := [rewrite]: #114
himmelma@35172
  1821
#118 := [monotonicity #115]: #117
himmelma@35172
  1822
#123 := [trans #118 #121]: #122
himmelma@35172
  1823
#126 := [monotonicity #123]: #125
himmelma@35172
  1824
#135 := [trans #126 #133]: #134
himmelma@35172
  1825
#110 := (iff #42 #109)
himmelma@35172
  1826
#107 := (= #41 #104)
himmelma@35172
  1827
#93 := (* -1::real #38)
himmelma@35172
  1828
#94 := (+ #31 #93)
himmelma@35172
  1829
#97 := (/ #94 3::real)
himmelma@35172
  1830
#105 := (= #97 #104)
himmelma@35172
  1831
#106 := [rewrite]: #105
himmelma@35172
  1832
#98 := (= #41 #97)
himmelma@35172
  1833
#95 := (= #39 #94)
himmelma@35172
  1834
#96 := [rewrite]: #95
himmelma@35172
  1835
#99 := [monotonicity #96]: #98
himmelma@35172
  1836
#108 := [trans #99 #106]: #107
himmelma@35172
  1837
#91 := (= #36 #90)
himmelma@35172
  1838
#76 := (= #32 #75)
himmelma@35172
  1839
#77 := [rewrite]: #76
himmelma@35172
  1840
#88 := (= #35 #85)
himmelma@35172
  1841
#81 := (- #75)
himmelma@35172
  1842
#86 := (= #81 #85)
himmelma@35172
  1843
#87 := [rewrite]: #86
himmelma@35172
  1844
#82 := (= #35 #81)
himmelma@35172
  1845
#83 := [monotonicity #77]: #82
himmelma@35172
  1846
#89 := [trans #83 #87]: #88
himmelma@35172
  1847
#79 := (iff #34 #78)
himmelma@35172
  1848
#80 := [monotonicity #77]: #79
himmelma@35172
  1849
#92 := [monotonicity #80 #89 #77]: #91
himmelma@35172
  1850
#111 := [monotonicity #92 #108]: #110
himmelma@35172
  1851
#137 := [trans #111 #135]: #136
himmelma@35172
  1852
#72 := [asserted]: #42
himmelma@35172
  1853
#138 := [mp #72 #137]: #131
himmelma@35172
  1854
decl uf_1 :: T1
himmelma@35172
  1855
#4 := uf_1
himmelma@35172
  1856
#43 := (uf_13 uf_1)
himmelma@35172
  1857
#44 := (uf_12 #43 uf_14)
himmelma@35172
  1858
#45 := (uf_11 #44 uf_15)
himmelma@35172
  1859
#149 := (* -1::real #45)
himmelma@35172
  1860
#150 := (+ #38 #149)
himmelma@35172
  1861
#140 := (+ #93 #45)
himmelma@35172
  1862
#161 := (<= #150 0::real)
himmelma@35172
  1863
#168 := (ite #161 #140 #150)
himmelma@35172
  1864
#176 := (* -1::real #168)
himmelma@35172
  1865
#177 := (+ #103 #176)
himmelma@35172
  1866
#178 := (+ #101 #177)
himmelma@35172
  1867
#179 := (<= #178 0::real)
himmelma@35172
  1868
#180 := (not #179)
himmelma@35172
  1869
#46 := (- #45 #38)
himmelma@35172
  1870
#48 := (- #46)
himmelma@35172
  1871
#47 := (< #46 0::real)
himmelma@35172
  1872
#49 := (ite #47 #48 #46)
himmelma@35172
  1873
#50 := (< #49 #41)
himmelma@35172
  1874
#185 := (iff #50 #180)
himmelma@35172
  1875
#143 := (< #140 0::real)
himmelma@35172
  1876
#155 := (ite #143 #150 #140)
himmelma@35172
  1877
#158 := (< #155 #104)
himmelma@35172
  1878
#183 := (iff #158 #180)
himmelma@35172
  1879
#173 := (< #168 #104)
himmelma@35172
  1880
#181 := (iff #173 #180)
himmelma@35172
  1881
#182 := [rewrite]: #181
himmelma@35172
  1882
#174 := (iff #158 #173)
himmelma@35172
  1883
#171 := (= #155 #168)
himmelma@35172
  1884
#162 := (not #161)
himmelma@35172
  1885
#165 := (ite #162 #150 #140)
himmelma@35172
  1886
#169 := (= #165 #168)
himmelma@35172
  1887
#170 := [rewrite]: #169
himmelma@35172
  1888
#166 := (= #155 #165)
himmelma@35172
  1889
#163 := (iff #143 #162)
himmelma@35172
  1890
#164 := [rewrite]: #163
himmelma@35172
  1891
#167 := [monotonicity #164]: #166
himmelma@35172
  1892
#172 := [trans #167 #170]: #171
himmelma@35172
  1893
#175 := [monotonicity #172]: #174
himmelma@35172
  1894
#184 := [trans #175 #182]: #183
himmelma@35172
  1895
#159 := (iff #50 #158)
himmelma@35172
  1896
#156 := (= #49 #155)
himmelma@35172
  1897
#141 := (= #46 #140)
himmelma@35172
  1898
#142 := [rewrite]: #141
himmelma@35172
  1899
#153 := (= #48 #150)
himmelma@35172
  1900
#146 := (- #140)
himmelma@35172
  1901
#151 := (= #146 #150)
himmelma@35172
  1902
#152 := [rewrite]: #151
himmelma@35172
  1903
#147 := (= #48 #146)
himmelma@35172
  1904
#148 := [monotonicity #142]: #147
himmelma@35172
  1905
#154 := [trans #148 #152]: #153
himmelma@35172
  1906
#144 := (iff #47 #143)
himmelma@35172
  1907
#145 := [monotonicity #142]: #144
himmelma@35172
  1908
#157 := [monotonicity #145 #154 #142]: #156
himmelma@35172
  1909
#160 := [monotonicity #157 #108]: #159
himmelma@35172
  1910
#186 := [trans #160 #184]: #185
himmelma@35172
  1911
#139 := [asserted]: #50
himmelma@35172
  1912
#187 := [mp #139 #186]: #180
himmelma@35172
  1913
#299 := (+ #140 #176)
himmelma@35172
  1914
#300 := (<= #299 0::real)
himmelma@35172
  1915
#290 := (= #140 #168)
himmelma@35172
  1916
#329 := [hypothesis]: #162
himmelma@35172
  1917
#191 := (+ #29 #149)
himmelma@35172
  1918
#192 := (<= #191 0::real)
himmelma@35172
  1919
#51 := (<= #29 #45)
himmelma@35172
  1920
#193 := (iff #51 #192)
himmelma@35172
  1921
#194 := [rewrite]: #193
himmelma@35172
  1922
#188 := [asserted]: #51
himmelma@35172
  1923
#195 := [mp #188 #194]: #192
himmelma@35172
  1924
#298 := (+ #75 #127)
himmelma@35172
  1925
#301 := (<= #298 0::real)
himmelma@35172
  1926
#284 := (= #75 #119)
himmelma@35172
  1927
#302 := [hypothesis]: #113
himmelma@35172
  1928
#296 := (+ #85 #127)
himmelma@35172
  1929
#297 := (<= #296 0::real)
himmelma@35172
  1930
#285 := (= #85 #119)
himmelma@35172
  1931
#288 := (or #112 #285)
himmelma@35172
  1932
#289 := [def-axiom]: #288
himmelma@35172
  1933
#303 := [unit-resolution #289 #302]: #285
himmelma@35172
  1934
#304 := (not #285)
himmelma@35172
  1935
#305 := (or #304 #297)
himmelma@35172
  1936
#306 := [th-lemma]: #305
himmelma@35172
  1937
#307 := [unit-resolution #306 #303]: #297
himmelma@35172
  1938
#315 := (not #290)
himmelma@35172
  1939
#310 := (not #300)
himmelma@35172
  1940
#311 := (or #310 #112)
himmelma@35172
  1941
#308 := [hypothesis]: #300
himmelma@35172
  1942
#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
himmelma@35172
  1943
#312 := [lemma #309]: #311
himmelma@35172
  1944
#322 := [unit-resolution #312 #302]: #310
himmelma@35172
  1945
#316 := (or #315 #300)
himmelma@35172
  1946
#313 := [hypothesis]: #310
himmelma@35172
  1947
#314 := [hypothesis]: #290
himmelma@35172
  1948
#317 := [th-lemma]: #316
himmelma@35172
  1949
#318 := [unit-resolution #317 #314 #313]: false
himmelma@35172
  1950
#319 := [lemma #318]: #316
himmelma@35172
  1951
#323 := [unit-resolution #319 #322]: #315
himmelma@35172
  1952
#292 := (or #162 #290)
himmelma@35172
  1953
#293 := [def-axiom]: #292
himmelma@35172
  1954
#324 := [unit-resolution #293 #323]: #162
himmelma@35172
  1955
#325 := [th-lemma #324 #307 #138 #302 #195]: false
himmelma@35172
  1956
#326 := [lemma #325]: #112
himmelma@35172
  1957
#286 := (or #113 #284)
himmelma@35172
  1958
#287 := [def-axiom]: #286
himmelma@35172
  1959
#330 := [unit-resolution #287 #326]: #284
himmelma@35172
  1960
#331 := (not #284)
himmelma@35172
  1961
#332 := (or #331 #301)
himmelma@35172
  1962
#333 := [th-lemma]: #332
himmelma@35172
  1963
#334 := [unit-resolution #333 #330]: #301
himmelma@35172
  1964
#335 := [th-lemma #326 #334 #195 #329 #138]: false
himmelma@35172
  1965
#336 := [lemma #335]: #161
himmelma@35172
  1966
#327 := [unit-resolution #293 #336]: #290
himmelma@35172
  1967
#328 := [unit-resolution #319 #327]: #300
himmelma@35172
  1968
[th-lemma #326 #334 #195 #328 #187 #138]: false
himmelma@35172
  1969
unsat
himmelma@35172
  1970
GX51o3DUO/UBS3eNP2P9kA 285 0
himmelma@35172
  1971
#2 := false
himmelma@35172
  1972
#7 := 0::real
himmelma@35172
  1973
decl uf_4 :: real
himmelma@35172
  1974
#16 := uf_4
himmelma@35172
  1975
#40 := -1::real
himmelma@35172
  1976
#116 := (* -1::real uf_4)
himmelma@35172
  1977
decl uf_3 :: real
himmelma@35172
  1978
#11 := uf_3
himmelma@35172
  1979
#117 := (+ uf_3 #116)
himmelma@35172
  1980
#128 := (<= #117 0::real)
himmelma@35172
  1981
#129 := (not #128)
himmelma@35172
  1982
#220 := 2/3::real
himmelma@35172
  1983
#221 := (* 2/3::real uf_3)
himmelma@35172
  1984
#222 := (+ #221 #116)
himmelma@35172
  1985
decl uf_2 :: real
himmelma@35172
  1986
#5 := uf_2
himmelma@35172
  1987
#67 := 1/3::real
himmelma@35172
  1988
#68 := (* 1/3::real uf_2)
himmelma@35172
  1989
#233 := (+ #68 #222)
himmelma@35172
  1990
#243 := (<= #233 0::real)
himmelma@35172
  1991
#268 := (not #243)
himmelma@35172
  1992
#287 := [hypothesis]: #268
himmelma@35172
  1993
#41 := (* -1::real uf_2)
himmelma@35172
  1994
decl uf_1 :: real
himmelma@35172
  1995
#4 := uf_1
himmelma@35172
  1996
#42 := (+ uf_1 #41)
himmelma@35172
  1997
#79 := (>= #42 0::real)
himmelma@35172
  1998
#80 := (not #79)
himmelma@35172
  1999
#297 := (or #80 #243)
himmelma@35172
  2000
#158 := (+ uf_1 #116)
himmelma@35172
  2001
#159 := (<= #158 0::real)
himmelma@35172
  2002
#22 := (<= uf_1 uf_4)
himmelma@35172
  2003
#160 := (iff #22 #159)
himmelma@35172
  2004
#161 := [rewrite]: #160
himmelma@35172
  2005
#155 := [asserted]: #22
himmelma@35172
  2006
#162 := [mp #155 #161]: #159
himmelma@35172
  2007
#200 := (* 1/3::real uf_3)
himmelma@35172
  2008
#198 := -4/3::real
himmelma@35172
  2009
#199 := (* -4/3::real uf_2)
himmelma@35172
  2010
#201 := (+ #199 #200)
himmelma@35172
  2011
#202 := (+ uf_1 #201)
himmelma@35172
  2012
#203 := (>= #202 0::real)
himmelma@35172
  2013
#258 := (not #203)
himmelma@35172
  2014
#292 := [hypothesis]: #79
himmelma@35172
  2015
#293 := (or #80 #258)
himmelma@35172
  2016
#69 := -1/3::real
himmelma@35172
  2017
#70 := (* -1/3::real uf_3)
himmelma@35172
  2018
#186 := -2/3::real
himmelma@35172
  2019
#187 := (* -2/3::real uf_2)
himmelma@35172
  2020
#188 := (+ #187 #70)
himmelma@35172
  2021
#189 := (+ uf_1 #188)
himmelma@35172
  2022
#204 := (<= #189 0::real)
himmelma@35172
  2023
#205 := (ite #79 #203 #204)
himmelma@35172
  2024
#210 := (not #205)
himmelma@35172
  2025
#51 := (* -1::real uf_1)
himmelma@35172
  2026
#52 := (+ #51 uf_2)
himmelma@35172
  2027
#86 := (ite #79 #42 #52)
himmelma@35172
  2028
#94 := (* -1::real #86)
himmelma@35172
  2029
#95 := (+ #70 #94)
himmelma@35172
  2030
#96 := (+ #68 #95)
himmelma@35172
  2031
#97 := (<= #96 0::real)
himmelma@35172
  2032
#98 := (not #97)
himmelma@35172
  2033
#211 := (iff #98 #210)
himmelma@35172
  2034
#208 := (iff #97 #205)
himmelma@35172
  2035
#182 := 4/3::real
himmelma@35172
  2036
#183 := (* 4/3::real uf_2)
himmelma@35172
  2037
#184 := (+ #183 #70)
himmelma@35172
  2038
#185 := (+ #51 #184)
himmelma@35172
  2039
#190 := (ite #79 #185 #189)
himmelma@35172
  2040
#195 := (<= #190 0::real)
himmelma@35172
  2041
#206 := (iff #195 #205)
himmelma@35172
  2042
#207 := [rewrite]: #206
himmelma@35172
  2043
#196 := (iff #97 #195)
himmelma@35172
  2044
#193 := (= #96 #190)
himmelma@35172
  2045
#172 := (+ #41 #70)
himmelma@35172
  2046
#173 := (+ uf_1 #172)
himmelma@35172
  2047
#170 := (+ uf_2 #70)
himmelma@35172
  2048
#171 := (+ #51 #170)
himmelma@35172
  2049
#174 := (ite #79 #171 #173)
himmelma@35172
  2050
#179 := (+ #68 #174)
himmelma@35172
  2051
#191 := (= #179 #190)
himmelma@35172
  2052
#192 := [rewrite]: #191
himmelma@35172
  2053
#180 := (= #96 #179)
himmelma@35172
  2054
#177 := (= #95 #174)
himmelma@35172
  2055
#164 := (ite #79 #52 #42)
himmelma@35172
  2056
#167 := (+ #70 #164)
himmelma@35172
  2057
#175 := (= #167 #174)
himmelma@35172
  2058
#176 := [rewrite]: #175
himmelma@35172
  2059
#168 := (= #95 #167)
himmelma@35172
  2060
#156 := (= #94 #164)
himmelma@35172
  2061
#165 := [rewrite]: #156
himmelma@35172
  2062
#169 := [monotonicity #165]: #168
himmelma@35172
  2063
#178 := [trans #169 #176]: #177
himmelma@35172
  2064
#181 := [monotonicity #178]: #180
himmelma@35172
  2065
#194 := [trans #181 #192]: #193
himmelma@35172
  2066
#197 := [monotonicity #194]: #196
himmelma@35172
  2067
#209 := [trans #197 #207]: #208
himmelma@35172
  2068
#212 := [monotonicity #209]: #211
himmelma@35172
  2069
#13 := 3::real
himmelma@35172
  2070
#12 := (- uf_2 uf_3)
himmelma@35172
  2071
#14 := (/ #12 3::real)
himmelma@35172
  2072
#6 := (- uf_1 uf_2)
himmelma@35172
  2073
#9 := (- #6)
himmelma@35172
  2074
#8 := (< #6 0::real)
himmelma@35172
  2075
#10 := (ite #8 #9 #6)
himmelma@35172
  2076
#15 := (< #10 #14)
himmelma@35172
  2077
#103 := (iff #15 #98)
himmelma@35172
  2078
#71 := (+ #68 #70)
himmelma@35172
  2079
#45 := (< #42 0::real)
himmelma@35172
  2080
#57 := (ite #45 #52 #42)
himmelma@35172
  2081
#76 := (< #57 #71)
himmelma@35172
  2082
#101 := (iff #76 #98)
himmelma@35172
  2083
#91 := (< #86 #71)
himmelma@35172
  2084
#99 := (iff #91 #98)
himmelma@35172
  2085
#100 := [rewrite]: #99
himmelma@35172
  2086
#92 := (iff #76 #91)
himmelma@35172
  2087
#89 := (= #57 #86)
himmelma@35172
  2088
#83 := (ite #80 #52 #42)
himmelma@35172
  2089
#87 := (= #83 #86)
himmelma@35172
  2090
#88 := [rewrite]: #87
himmelma@35172
  2091
#84 := (= #57 #83)
himmelma@35172
  2092
#81 := (iff #45 #80)
himmelma@35172
  2093
#82 := [rewrite]: #81
himmelma@35172
  2094
#85 := [monotonicity #82]: #84
himmelma@35172
  2095
#90 := [trans #85 #88]: #89
himmelma@35172
  2096
#93 := [monotonicity #90]: #92
himmelma@35172
  2097
#102 := [trans #93 #100]: #101
himmelma@35172
  2098
#77 := (iff #15 #76)
himmelma@35172
  2099
#74 := (= #14 #71)
himmelma@35172
  2100
#60 := (* -1::real uf_3)
himmelma@35172
  2101
#61 := (+ uf_2 #60)
himmelma@35172
  2102
#64 := (/ #61 3::real)
himmelma@35172
  2103
#72 := (= #64 #71)
himmelma@35172
  2104
#73 := [rewrite]: #72
himmelma@35172
  2105
#65 := (= #14 #64)
himmelma@35172
  2106
#62 := (= #12 #61)
himmelma@35172
  2107
#63 := [rewrite]: #62
himmelma@35172
  2108
#66 := [monotonicity #63]: #65
himmelma@35172
  2109
#75 := [trans #66 #73]: #74
himmelma@35172
  2110
#58 := (= #10 #57)
himmelma@35172
  2111
#43 := (= #6 #42)
himmelma@35172
  2112
#44 := [rewrite]: #43
himmelma@35172
  2113
#55 := (= #9 #52)
himmelma@35172
  2114
#48 := (- #42)
himmelma@35172
  2115
#53 := (= #48 #52)
himmelma@35172
  2116
#54 := [rewrite]: #53
himmelma@35172
  2117
#49 := (= #9 #48)
himmelma@35172
  2118
#50 := [monotonicity #44]: #49
himmelma@35172
  2119
#56 := [trans #50 #54]: #55
himmelma@35172
  2120
#46 := (iff #8 #45)
himmelma@35172
  2121
#47 := [monotonicity #44]: #46
himmelma@35172
  2122
#59 := [monotonicity #47 #56 #44]: #58
himmelma@35172
  2123
#78 := [monotonicity #59 #75]: #77
himmelma@35172
  2124
#104 := [trans #78 #102]: #103
himmelma@35172
  2125
#39 := [asserted]: #15
himmelma@35172
  2126
#105 := [mp #39 #104]: #98
himmelma@35172
  2127
#213 := [mp #105 #212]: #210
himmelma@35172
  2128
#259 := (or #205 #80 #258)
himmelma@35172
  2129
#260 := [def-axiom]: #259
himmelma@35172
  2130
#294 := [unit-resolution #260 #213]: #293
himmelma@35172
  2131
#295 := [unit-resolution #294 #292]: #258
himmelma@35172
  2132
#296 := [th-lemma #287 #292 #295 #162]: false
himmelma@35172
  2133
#298 := [lemma #296]: #297
himmelma@35172
  2134
#299 := [unit-resolution #298 #287]: #80
himmelma@35172
  2135
#261 := (not #204)
himmelma@35172
  2136
#281 := (or #79 #261)
himmelma@35172
  2137
#262 := (or #205 #79 #261)
himmelma@35172
  2138
#263 := [def-axiom]: #262
himmelma@35172
  2139
#282 := [unit-resolution #263 #213]: #281
himmelma@35172
  2140
#300 := [unit-resolution #282 #299]: #261
himmelma@35172
  2141
#290 := (or #79 #204 #243)
himmelma@35172
  2142
#276 := [hypothesis]: #261
himmelma@35172
  2143
#288 := [hypothesis]: #80
himmelma@35172
  2144
#289 := [th-lemma #288 #276 #162 #287]: false
himmelma@35172
  2145
#291 := [lemma #289]: #290
himmelma@35172
  2146
#301 := [unit-resolution #291 #300 #299 #287]: false
himmelma@35172
  2147
#302 := [lemma #301]: #243
himmelma@35172
  2148
#303 := (or #129 #268)
himmelma@35172
  2149
#223 := (* -4/3::real uf_3)
himmelma@35172
  2150
#224 := (+ #223 uf_4)
himmelma@35172
  2151
#234 := (+ #68 #224)
himmelma@35172
  2152
#244 := (<= #234 0::real)
himmelma@35172
  2153
#245 := (ite #128 #243 #244)
himmelma@35172
  2154
#250 := (not #245)
himmelma@35172
  2155
#107 := (+ #60 uf_4)
himmelma@35172
  2156
#135 := (ite #128 #107 #117)
himmelma@35172
  2157
#143 := (* -1::real #135)
himmelma@35172
  2158
#144 := (+ #70 #143)
himmelma@35172
  2159
#145 := (+ #68 #144)
himmelma@35172
  2160
#146 := (<= #145 0::real)
himmelma@35172
  2161
#147 := (not #146)
himmelma@35172
  2162
#251 := (iff #147 #250)
himmelma@35172
  2163
#248 := (iff #146 #245)
himmelma@35172
  2164
#235 := (ite #128 #233 #234)
himmelma@35172
  2165
#240 := (<= #235 0::real)
himmelma@35172
  2166
#246 := (iff #240 #245)
himmelma@35172
  2167
#247 := [rewrite]: #246
himmelma@35172
  2168
#241 := (iff #146 #240)
himmelma@35172
  2169
#238 := (= #145 #235)
himmelma@35172
  2170
#225 := (ite #128 #222 #224)
himmelma@35172
  2171
#230 := (+ #68 #225)
himmelma@35172
  2172
#236 := (= #230 #235)
himmelma@35172
  2173
#237 := [rewrite]: #236
himmelma@35172
  2174
#231 := (= #145 #230)
himmelma@35172
  2175
#228 := (= #144 #225)
himmelma@35172
  2176
#214 := (ite #128 #117 #107)
himmelma@35172
  2177
#217 := (+ #70 #214)
himmelma@35172
  2178
#226 := (= #217 #225)
himmelma@35172
  2179
#227 := [rewrite]: #226
himmelma@35172
  2180
#218 := (= #144 #217)
himmelma@35172
  2181
#215 := (= #143 #214)
himmelma@35172
  2182
#216 := [rewrite]: #215
himmelma@35172
  2183
#219 := [monotonicity #216]: #218
himmelma@35172
  2184
#229 := [trans #219 #227]: #228
himmelma@35172
  2185
#232 := [monotonicity #229]: #231
himmelma@35172
  2186
#239 := [trans #232 #237]: #238
himmelma@35172
  2187
#242 := [monotonicity #239]: #241
himmelma@35172
  2188
#249 := [trans #242 #247]: #248
himmelma@35172
  2189
#252 := [monotonicity #249]: #251
himmelma@35172
  2190
#17 := (- uf_4 uf_3)
himmelma@35172
  2191
#19 := (- #17)
himmelma@35172
  2192
#18 := (< #17 0::real)
himmelma@35172
  2193
#20 := (ite #18 #19 #17)
himmelma@35172
  2194
#21 := (< #20 #14)
himmelma@35172
  2195
#152 := (iff #21 #147)
himmelma@35172
  2196
#110 := (< #107 0::real)
himmelma@35172
  2197
#122 := (ite #110 #117 #107)
himmelma@35172
  2198
#125 := (< #122 #71)
himmelma@35172
  2199
#150 := (iff #125 #147)
himmelma@35172
  2200
#140 := (< #135 #71)
himmelma@35172
  2201
#148 := (iff #140 #147)
himmelma@35172
  2202
#149 := [rewrite]: #148
himmelma@35172
  2203
#141 := (iff #125 #140)
himmelma@35172
  2204
#138 := (= #122 #135)
himmelma@35172
  2205
#132 := (ite #129 #117 #107)
himmelma@35172
  2206
#136 := (= #132 #135)
himmelma@35172
  2207
#137 := [rewrite]: #136
himmelma@35172
  2208
#133 := (= #122 #132)
himmelma@35172
  2209
#130 := (iff #110 #129)
himmelma@35172
  2210
#131 := [rewrite]: #130
himmelma@35172
  2211
#134 := [monotonicity #131]: #133
himmelma@35172
  2212
#139 := [trans #134 #137]: #138
himmelma@35172
  2213
#142 := [monotonicity #139]: #141
himmelma@35172
  2214
#151 := [trans #142 #149]: #150
himmelma@35172
  2215
#126 := (iff #21 #125)
himmelma@35172
  2216
#123 := (= #20 #122)
himmelma@35172
  2217
#108 := (= #17 #107)
himmelma@35172
  2218
#109 := [rewrite]: #108
himmelma@35172
  2219
#120 := (= #19 #117)
himmelma@35172
  2220
#113 := (- #107)
himmelma@35172
  2221
#118 := (= #113 #117)
himmelma@35172
  2222
#119 := [rewrite]: #118
himmelma@35172
  2223
#114 := (= #19 #113)
himmelma@35172
  2224
#115 := [monotonicity #109]: #114
himmelma@35172
  2225
#121 := [trans #115 #119]: #120
himmelma@35172
  2226
#111 := (iff #18 #110)
himmelma@35172
  2227
#112 := [monotonicity #109]: #111
himmelma@35172
  2228
#124 := [monotonicity #112 #121 #109]: #123
himmelma@35172
  2229
#127 := [monotonicity #124 #75]: #126
himmelma@35172
  2230
#153 := [trans #127 #151]: #152
himmelma@35172
  2231
#106 := [asserted]: #21
himmelma@35172
  2232
#154 := [mp #106 #153]: #147
himmelma@35172
  2233
#253 := [mp #154 #252]: #250
himmelma@35172
  2234
#269 := (or #245 #129 #268)
himmelma@35172
  2235
#270 := [def-axiom]: #269
himmelma@35172
  2236
#304 := [unit-resolution #270 #253]: #303
himmelma@35172
  2237
#305 := [unit-resolution #304 #302]: #129
himmelma@35172
  2238
#271 := (not #244)
himmelma@35172
  2239
#306 := (or #128 #271)
himmelma@35172
  2240
#272 := (or #245 #128 #271)
himmelma@35172
  2241
#273 := [def-axiom]: #272
himmelma@35172
  2242
#307 := [unit-resolution #273 #253]: #306
himmelma@35172
  2243
#308 := [unit-resolution #307 #305]: #271
himmelma@35172
  2244
#285 := (or #128 #244)
himmelma@35172
  2245
#274 := [hypothesis]: #271
himmelma@35172
  2246
#275 := [hypothesis]: #129
himmelma@35172
  2247
#278 := (or #204 #128 #244)
himmelma@35172
  2248
#277 := [th-lemma #276 #275 #274 #162]: false
himmelma@35172
  2249
#279 := [lemma #277]: #278
himmelma@35172
  2250
#280 := [unit-resolution #279 #275 #274]: #204
himmelma@35172
  2251
#283 := [unit-resolution #282 #280]: #79
himmelma@35172
  2252
#284 := [th-lemma #275 #274 #283 #162]: false
himmelma@35172
  2253
#286 := [lemma #284]: #285
himmelma@35172
  2254
[unit-resolution #286 #308 #305]: false
himmelma@35172
  2255
unsat
himmelma@35172
  2256
cebG074uorSr8ODzgTmcKg 97 0
himmelma@35172
  2257
#2 := false
himmelma@35172
  2258
#18 := 0::real
himmelma@35172
  2259
decl uf_1 :: (-> T2 T1 real)
himmelma@35172
  2260
decl uf_5 :: T1
himmelma@35172
  2261
#11 := uf_5
himmelma@35172
  2262
decl uf_2 :: T2
himmelma@35172
  2263
#4 := uf_2
himmelma@35172
  2264
#20 := (uf_1 uf_2 uf_5)
himmelma@35172
  2265
#42 := -1::real
himmelma@35172
  2266
#53 := (* -1::real #20)
himmelma@35172
  2267
decl uf_3 :: T2
himmelma@35172
  2268
#7 := uf_3
himmelma@35172
  2269
#19 := (uf_1 uf_3 uf_5)
himmelma@35172
  2270
#54 := (+ #19 #53)
himmelma@35172
  2271
#63 := (<= #54 0::real)
himmelma@35172
  2272
#21 := (- #19 #20)
himmelma@35172
  2273
#22 := (< 0::real #21)
himmelma@35172
  2274
#23 := (not #22)
himmelma@35172
  2275
#74 := (iff #23 #63)
himmelma@35172
  2276
#57 := (< 0::real #54)
himmelma@35172
  2277
#60 := (not #57)
himmelma@35172
  2278
#72 := (iff #60 #63)
himmelma@35172
  2279
#64 := (not #63)
himmelma@35172
  2280
#67 := (not #64)
himmelma@35172
  2281
#70 := (iff #67 #63)
himmelma@35172
  2282
#71 := [rewrite]: #70
himmelma@35172
  2283
#68 := (iff #60 #67)
himmelma@35172
  2284
#65 := (iff #57 #64)
himmelma@35172
  2285
#66 := [rewrite]: #65
himmelma@35172
  2286
#69 := [monotonicity #66]: #68
himmelma@35172
  2287
#73 := [trans #69 #71]: #72
himmelma@35172
  2288
#61 := (iff #23 #60)
himmelma@35172
  2289
#58 := (iff #22 #57)
himmelma@35172
  2290
#55 := (= #21 #54)
himmelma@35172
  2291
#56 := [rewrite]: #55
himmelma@35172
  2292
#59 := [monotonicity #56]: #58
himmelma@35172
  2293
#62 := [monotonicity #59]: #61
himmelma@35172
  2294
#75 := [trans #62 #73]: #74
himmelma@35172
  2295
#41 := [asserted]: #23
himmelma@35172
  2296
#76 := [mp #41 #75]: #63
himmelma@35172
  2297
#5 := (:var 0 T1)
himmelma@35172
  2298
#8 := (uf_1 uf_3 #5)
himmelma@35172
  2299
#141 := (pattern #8)
himmelma@35172
  2300
#6 := (uf_1 uf_2 #5)
himmelma@35172
  2301
#140 := (pattern #6)
himmelma@35172
  2302
#45 := (* -1::real #8)
himmelma@35172
  2303
#46 := (+ #6 #45)
himmelma@35172
  2304
#44 := (>= #46 0::real)
himmelma@35172
  2305
#43 := (not #44)
himmelma@35172
  2306
#142 := (forall (vars (?x1 T1)) (:pat #140 #141) #43)
himmelma@35172
  2307
#49 := (forall (vars (?x1 T1)) #43)
himmelma@35172
  2308
#145 := (iff #49 #142)
himmelma@35172
  2309
#143 := (iff #43 #43)
himmelma@35172
  2310
#144 := [refl]: #143
himmelma@35172
  2311
#146 := [quant-intro #144]: #145
himmelma@35172
  2312
#80 := (~ #49 #49)
himmelma@35172
  2313
#82 := (~ #43 #43)
himmelma@35172
  2314
#83 := [refl]: #82
himmelma@35172
  2315
#81 := [nnf-pos #83]: #80
himmelma@35172
  2316
#9 := (< #6 #8)
himmelma@35172
  2317
#10 := (forall (vars (?x1 T1)) #9)
himmelma@35172
  2318
#50 := (iff #10 #49)
himmelma@35172
  2319
#47 := (iff #9 #43)
himmelma@35172
  2320
#48 := [rewrite]: #47
himmelma@35172
  2321
#51 := [quant-intro #48]: #50
himmelma@35172
  2322
#39 := [asserted]: #10
himmelma@35172
  2323
#52 := [mp #39 #51]: #49
himmelma@35172
  2324
#79 := [mp~ #52 #81]: #49
himmelma@35172
  2325
#147 := [mp #79 #146]: #142
himmelma@35172
  2326
#164 := (not #142)
himmelma@35172
  2327
#165 := (or #164 #64)
himmelma@35172
  2328
#148 := (* -1::real #19)
himmelma@35172
  2329
#149 := (+ #20 #148)
himmelma@35172
  2330
#150 := (>= #149 0::real)
himmelma@35172
  2331
#151 := (not #150)
himmelma@35172
  2332
#166 := (or #164 #151)
himmelma@35172
  2333
#168 := (iff #166 #165)
himmelma@35172
  2334
#170 := (iff #165 #165)
himmelma@35172
  2335
#171 := [rewrite]: #170
himmelma@35172
  2336
#162 := (iff #151 #64)
himmelma@35172
  2337
#160 := (iff #150 #63)
himmelma@35172
  2338
#152 := (+ #148 #20)
himmelma@35172
  2339
#155 := (>= #152 0::real)
himmelma@35172
  2340
#158 := (iff #155 #63)
himmelma@35172
  2341
#159 := [rewrite]: #158
himmelma@35172
  2342
#156 := (iff #150 #155)
himmelma@35172
  2343
#153 := (= #149 #152)
himmelma@35172
  2344
#154 := [rewrite]: #153
himmelma@35172
  2345
#157 := [monotonicity #154]: #156
himmelma@35172
  2346
#161 := [trans #157 #159]: #160
himmelma@35172
  2347
#163 := [monotonicity #161]: #162
himmelma@35172
  2348
#169 := [monotonicity #163]: #168
himmelma@35172
  2349
#172 := [trans #169 #171]: #168
himmelma@35172
  2350
#167 := [quant-inst]: #166
himmelma@35172
  2351
#173 := [mp #167 #172]: #165
himmelma@35172
  2352
[unit-resolution #173 #147 #76]: false
himmelma@35172
  2353
unsat
himmelma@35172
  2354
DKRtrJ2XceCkITuNwNViRw 57 0
himmelma@35172
  2355
#2 := false
himmelma@35172
  2356
#4 := 0::real
himmelma@35172
  2357
decl uf_1 :: (-> T2 real)
himmelma@35172
  2358
decl uf_2 :: (-> T1 T1 T2)
himmelma@35172
  2359
decl uf_12 :: (-> T4 T1)
himmelma@35172
  2360
decl uf_4 :: T4
himmelma@35172
  2361
#11 := uf_4
himmelma@35172
  2362
#39 := (uf_12 uf_4)
himmelma@35172
  2363
decl uf_10 :: T4
himmelma@35172
  2364
#27 := uf_10
himmelma@35172
  2365
#38 := (uf_12 uf_10)
himmelma@35172
  2366
#40 := (uf_2 #38 #39)
himmelma@35172
  2367
#41 := (uf_1 #40)
himmelma@35172
  2368
#264 := (>= #41 0::real)
himmelma@35172
  2369
#266 := (not #264)
himmelma@35172
  2370
#43 := (= #41 0::real)
himmelma@35172
  2371
#44 := (not #43)
himmelma@35172
  2372
#131 := [asserted]: #44
himmelma@35172
  2373
#272 := (or #43 #266)
himmelma@35172
  2374
#42 := (<= #41 0::real)
himmelma@35172
  2375
#130 := [asserted]: #42
himmelma@35172
  2376
#265 := (not #42)
himmelma@35172
  2377
#270 := (or #43 #265 #266)
himmelma@35172
  2378
#271 := [th-lemma]: #270
himmelma@35172
  2379
#273 := [unit-resolution #271 #130]: #272
himmelma@35172
  2380
#274 := [unit-resolution #273 #131]: #266
himmelma@35172
  2381
#6 := (:var 0 T1)
himmelma@35172
  2382
#5 := (:var 1 T1)
himmelma@35172
  2383
#7 := (uf_2 #5 #6)
himmelma@35172
  2384
#241 := (pattern #7)
himmelma@35172
  2385
#8 := (uf_1 #7)
himmelma@35172
  2386
#65 := (>= #8 0::real)
himmelma@35172
  2387
#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65)
himmelma@35172
  2388
#66 := (forall (vars (?x1 T1) (?x2 T1)) #65)
himmelma@35172
  2389
#245 := (iff #66 #242)
himmelma@35172
  2390
#243 := (iff #65 #65)
himmelma@35172
  2391
#244 := [refl]: #243
himmelma@35172
  2392
#246 := [quant-intro #244]: #245
himmelma@35172
  2393
#149 := (~ #66 #66)
himmelma@35172
  2394
#151 := (~ #65 #65)
himmelma@35172
  2395
#152 := [refl]: #151
himmelma@35172
  2396
#150 := [nnf-pos #152]: #149
himmelma@35172
  2397
#9 := (<= 0::real #8)
himmelma@35172
  2398
#10 := (forall (vars (?x1 T1) (?x2 T1)) #9)
himmelma@35172
  2399
#67 := (iff #10 #66)
himmelma@35172
  2400
#63 := (iff #9 #65)
himmelma@35172
  2401
#64 := [rewrite]: #63
himmelma@35172
  2402
#68 := [quant-intro #64]: #67
himmelma@35172
  2403
#60 := [asserted]: #10
himmelma@35172
  2404
#69 := [mp #60 #68]: #66
himmelma@35172
  2405
#147 := [mp~ #69 #150]: #66
himmelma@35172
  2406
#247 := [mp #147 #246]: #242
himmelma@35172
  2407
#267 := (not #242)
himmelma@35172
  2408
#268 := (or #267 #264)
himmelma@35172
  2409
#269 := [quant-inst]: #268
himmelma@35172
  2410
[unit-resolution #269 #247 #274]: false
himmelma@35172
  2411
unsat
himmelma@35172
  2412
97KJAJfUio+nGchEHWvgAw 91 0
himmelma@35172
  2413
#2 := false
himmelma@35172
  2414
#38 := 0::real
himmelma@35172
  2415
decl uf_1 :: (-> T1 T2 real)
himmelma@35172
  2416
decl uf_3 :: T2
himmelma@35172
  2417
#5 := uf_3
himmelma@35172
  2418
decl uf_4 :: T1
himmelma@35172
  2419
#7 := uf_4
himmelma@35172
  2420
#8 := (uf_1 uf_4 uf_3)
himmelma@35172
  2421
#35 := -1::real
himmelma@35172
  2422
#36 := (* -1::real #8)
himmelma@35172
  2423
decl uf_2 :: T1
himmelma@35172
  2424
#4 := uf_2
himmelma@35172
  2425
#6 := (uf_1 uf_2 uf_3)
himmelma@35172
  2426
#37 := (+ #6 #36)
himmelma@35172
  2427
#130 := (>= #37 0::real)
himmelma@35172
  2428
#155 := (not #130)
himmelma@35172
  2429
#43 := (= #6 #8)
himmelma@35172
  2430
#55 := (not #43)
himmelma@35172
  2431
#15 := (= #8 #6)
himmelma@35172
  2432
#16 := (not #15)
himmelma@35172
  2433
#56 := (iff #16 #55)
himmelma@35172
  2434
#53 := (iff #15 #43)
himmelma@35172
  2435
#54 := [rewrite]: #53
himmelma@35172
  2436
#57 := [monotonicity #54]: #56
himmelma@35172
  2437
#34 := [asserted]: #16
himmelma@35172
  2438
#60 := [mp #34 #57]: #55
himmelma@35172
  2439
#158 := (or #43 #155)
himmelma@35172
  2440
#39 := (<= #37 0::real)
himmelma@35172
  2441
#9 := (<= #6 #8)
himmelma@35172
  2442
#40 := (iff #9 #39)
himmelma@35172
  2443
#41 := [rewrite]: #40
himmelma@35172
  2444
#32 := [asserted]: #9
himmelma@35172
  2445
#42 := [mp #32 #41]: #39
himmelma@35172
  2446
#154 := (not #39)
himmelma@35172
  2447
#156 := (or #43 #154 #155)
himmelma@35172
  2448
#157 := [th-lemma]: #156
himmelma@35172
  2449
#159 := [unit-resolution #157 #42]: #158
himmelma@35172
  2450
#160 := [unit-resolution #159 #60]: #155
himmelma@35172
  2451
#10 := (:var 0 T2)
himmelma@35172
  2452
#12 := (uf_1 uf_2 #10)
himmelma@35172
  2453
#123 := (pattern #12)
himmelma@35172
  2454
#11 := (uf_1 uf_4 #10)
himmelma@35172
  2455
#122 := (pattern #11)
himmelma@35172
  2456
#44 := (* -1::real #12)
himmelma@35172
  2457
#45 := (+ #11 #44)
himmelma@35172
  2458
#46 := (<= #45 0::real)
himmelma@35172
  2459