--- a/etc/components Wed Mar 24 17:40:44 2010 +0100
+++ b/etc/components Wed Mar 24 17:41:25 2010 +0100
@@ -13,7 +13,6 @@
#misc components
src/Tools/Code
src/Tools/WWW_Find
-src/Tools/Cache_IO
src/HOL/Tools/ATP_Manager
src/HOL/Mirabelle
src/HOL/Library/Sum_Of_Squares
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 17:41:25 2010 +0100
@@ -1,4 +1,4 @@
-JinTdmjIiorL0/vvOyf3+w 6542 0
+6164a2366a9e57e212b8ac4aa01e3c8bcc1ea8e0 6542 0
#2 := false
decl up_6 :: (-> T4 T2 bool)
decl ?x47!7 :: (-> T2 T2)
--- a/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 17:41:25 2010 +0100
@@ -1,4 +1,4 @@
-iks4GfP7O/NgNFyGZ4ynjQ 2224 0
+cdfef9f27f2a4ba9648f86890c8563d0a1cfe888 2224 0
#2 := false
#4 := 0::int
decl uf_3 :: (-> int int)
--- a/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 17:41:25 2010 +0100
@@ -1,4 +1,4 @@
-6Q8QWdFv463DpfVfkr0XnA 7790 0
+b95bf7adc1e2b959cf13db317b64554768249b2e 7790 0
#2 := false
decl uf_110 :: (-> T4 T5 int)
decl uf_66 :: (-> T5 int T3 T5)
--- a/src/HOL/IsaMakefile Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Mar 24 17:41:25 2010 +0100
@@ -1078,7 +1078,10 @@
Multivariate_Analysis/Topology_Euclidean_Space.thy \
Multivariate_Analysis/Convex_Euclidean_Space.thy \
Multivariate_Analysis/Brouwer_Fixpoint.thy \
- Multivariate_Analysis/Derivative.thy
+ Multivariate_Analysis/Derivative.thy \
+ Multivariate_Analysis/Integration.thy \
+ Multivariate_Analysis/Integration.cert \
+ Multivariate_Analysis/Real_Integration.thy
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
@@ -1228,7 +1231,7 @@
SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
- SMT/Tools/z3_solver.ML $(SRC)/Tools/Cache_IO/cache_io.ML
+ SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
--- a/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 17:41:25 2010 +0100
@@ -1,4 +1,853 @@
-tB2Atlor9W4pSnrAz5nHpw 907 0
+534d3afbd3505abffa6b03e3986bfa7aa3cff358 428 0
+#2 := false
+decl uf_10 :: T1
+#38 := uf_10
+decl uf_3 :: T1
+#21 := uf_3
+#45 := (= uf_3 uf_10)
+decl uf_1 :: (-> int T1)
+decl uf_2 :: (-> T1 int)
+#39 := (uf_2 uf_10)
+#588 := (uf_1 #39)
+#686 := (= #588 uf_10)
+#589 := (= uf_10 #588)
+#4 := (:var 0 T1)
+#5 := (uf_2 #4)
+#541 := (pattern #5)
+#6 := (uf_1 #5)
+#93 := (= #4 #6)
+#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
+#96 := (forall (vars (?x1 T1)) #93)
+#545 := (iff #96 #542)
+#543 := (iff #93 #93)
+#544 := [refl]: #543
+#546 := [quant-intro #544]: #545
+#454 := (~ #96 #96)
+#456 := (~ #93 #93)
+#457 := [refl]: #456
+#455 := [nnf-pos #457]: #454
+#7 := (= #6 #4)
+#8 := (forall (vars (?x1 T1)) #7)
+#97 := (iff #8 #96)
+#94 := (iff #7 #93)
+#95 := [rewrite]: #94
+#98 := [quant-intro #95]: #97
+#92 := [asserted]: #8
+#101 := [mp #92 #98]: #96
+#452 := [mp~ #101 #455]: #96
+#547 := [mp #452 #546]: #542
+#590 := (not #542)
+#595 := (or #590 #589)
+#596 := [quant-inst]: #595
+#680 := [unit-resolution #596 #547]: #589
+#687 := [symm #680]: #686
+#688 := (= uf_3 #588)
+#22 := (uf_2 uf_3)
+#586 := (uf_1 #22)
+#684 := (= #586 #588)
+#682 := (= #588 #586)
+#678 := (= #39 #22)
+#676 := (= #22 #39)
+#9 := 0::int
+#227 := -1::int
+#230 := (* -1::int #39)
+#231 := (+ #22 #230)
+#296 := (<= #231 0::int)
+#70 := (<= #22 #39)
+#393 := (iff #70 #296)
+#394 := [rewrite]: #393
+#347 := [asserted]: #70
+#395 := [mp #347 #394]: #296
+#229 := (>= #231 0::int)
+decl uf_4 :: (-> T2 T3 real)
+decl uf_6 :: (-> T1 T3)
+#25 := (uf_6 uf_3)
+decl uf_7 :: T2
+#27 := uf_7
+#28 := (uf_4 uf_7 #25)
+decl uf_9 :: T2
+#33 := uf_9
+#34 := (uf_4 uf_9 #25)
+#46 := (uf_6 uf_10)
+decl uf_5 :: T2
+#24 := uf_5
+#47 := (uf_4 uf_5 #46)
+#48 := (ite #45 #47 #34)
+#256 := (ite #229 #48 #28)
+#568 := (= #28 #256)
+#648 := (not #568)
+#194 := 0::real
+#192 := -1::real
+#265 := (* -1::real #256)
+#640 := (+ #28 #265)
+#642 := (>= #640 0::real)
+#645 := (not #642)
+#643 := [hypothesis]: #642
+decl uf_8 :: T2
+#30 := uf_8
+#31 := (uf_4 uf_8 #25)
+#266 := (+ #31 #265)
+#264 := (>= #266 0::real)
+#267 := (not #264)
+#26 := (uf_4 uf_5 #25)
+decl uf_11 :: T2
+#41 := uf_11
+#42 := (uf_4 uf_11 #25)
+#237 := (ite #229 #42 #26)
+#245 := (* -1::real #237)
+#246 := (+ #31 #245)
+#247 := (<= #246 0::real)
+#248 := (not #247)
+#272 := (and #248 #267)
+#40 := (< #22 #39)
+#49 := (ite #40 #28 #48)
+#50 := (< #31 #49)
+#43 := (ite #40 #26 #42)
+#44 := (< #43 #31)
+#51 := (and #44 #50)
+#273 := (iff #51 #272)
+#270 := (iff #50 #267)
+#261 := (< #31 #256)
+#268 := (iff #261 #267)
+#269 := [rewrite]: #268
+#262 := (iff #50 #261)
+#259 := (= #49 #256)
+#228 := (not #229)
+#253 := (ite #228 #28 #48)
+#257 := (= #253 #256)
+#258 := [rewrite]: #257
+#254 := (= #49 #253)
+#232 := (iff #40 #228)
+#233 := [rewrite]: #232
+#255 := [monotonicity #233]: #254
+#260 := [trans #255 #258]: #259
+#263 := [monotonicity #260]: #262
+#271 := [trans #263 #269]: #270
+#251 := (iff #44 #248)
+#242 := (< #237 #31)
+#249 := (iff #242 #248)
+#250 := [rewrite]: #249
+#243 := (iff #44 #242)
+#240 := (= #43 #237)
+#234 := (ite #228 #26 #42)
+#238 := (= #234 #237)
+#239 := [rewrite]: #238
+#235 := (= #43 #234)
+#236 := [monotonicity #233]: #235
+#241 := [trans #236 #239]: #240
+#244 := [monotonicity #241]: #243
+#252 := [trans #244 #250]: #251
+#274 := [monotonicity #252 #271]: #273
+#178 := [asserted]: #51
+#275 := [mp #178 #274]: #272
+#277 := [and-elim #275]: #267
+#196 := (* -1::real #31)
+#197 := (+ #28 #196)
+#195 := (>= #197 0::real)
+#193 := (not #195)
+#213 := (* -1::real #34)
+#214 := (+ #31 #213)
+#212 := (>= #214 0::real)
+#215 := (not #212)
+#220 := (and #193 #215)
+#23 := (< #22 #22)
+#35 := (ite #23 #28 #34)
+#36 := (< #31 #35)
+#29 := (ite #23 #26 #28)
+#32 := (< #29 #31)
+#37 := (and #32 #36)
+#221 := (iff #37 #220)
+#218 := (iff #36 #215)
+#209 := (< #31 #34)
+#216 := (iff #209 #215)
+#217 := [rewrite]: #216
+#210 := (iff #36 #209)
+#207 := (= #35 #34)
+#202 := (ite false #28 #34)
+#205 := (= #202 #34)
+#206 := [rewrite]: #205
+#203 := (= #35 #202)
+#180 := (iff #23 false)
+#181 := [rewrite]: #180
+#204 := [monotonicity #181]: #203
+#208 := [trans #204 #206]: #207
+#211 := [monotonicity #208]: #210
+#219 := [trans #211 #217]: #218
+#200 := (iff #32 #193)
+#189 := (< #28 #31)
+#198 := (iff #189 #193)
+#199 := [rewrite]: #198
+#190 := (iff #32 #189)
+#187 := (= #29 #28)
+#182 := (ite false #26 #28)
+#185 := (= #182 #28)
+#186 := [rewrite]: #185
+#183 := (= #29 #182)
+#184 := [monotonicity #181]: #183
+#188 := [trans #184 #186]: #187
+#191 := [monotonicity #188]: #190
+#201 := [trans #191 #199]: #200
+#222 := [monotonicity #201 #219]: #221
+#177 := [asserted]: #37
+#223 := [mp #177 #222]: #220
+#224 := [and-elim #223]: #193
+#644 := [th-lemma #224 #277 #643]: false
+#646 := [lemma #644]: #645
+#647 := [hypothesis]: #568
+#649 := (or #648 #642)
+#650 := [th-lemma]: #649
+#651 := [unit-resolution #650 #647 #646]: false
+#652 := [lemma #651]: #648
+#578 := (or #229 #568)
+#579 := [def-axiom]: #578
+#675 := [unit-resolution #579 #652]: #229
+#677 := [th-lemma #675 #395]: #676
+#679 := [symm #677]: #678
+#683 := [monotonicity #679]: #682
+#685 := [symm #683]: #684
+#587 := (= uf_3 #586)
+#591 := (or #590 #587)
+#592 := [quant-inst]: #591
+#681 := [unit-resolution #592 #547]: #587
+#689 := [trans #681 #685]: #688
+#690 := [trans #689 #687]: #45
+#571 := (not #45)
+#54 := (uf_4 uf_11 #46)
+#279 := (ite #45 #28 #54)
+#465 := (* -1::real #279)
+#632 := (+ #28 #465)
+#633 := (<= #632 0::real)
+#580 := (= #28 #279)
+#656 := [hypothesis]: #45
+#582 := (or #571 #580)
+#583 := [def-axiom]: #582
+#657 := [unit-resolution #583 #656]: #580
+#658 := (not #580)
+#659 := (or #658 #633)
+#660 := [th-lemma]: #659
+#661 := [unit-resolution #660 #657]: #633
+#57 := (uf_4 uf_8 #46)
+#363 := (* -1::real #57)
+#379 := (+ #47 #363)
+#380 := (<= #379 0::real)
+#381 := (not #380)
+#364 := (+ #54 #363)
+#362 := (>= #364 0::real)
+#361 := (not #362)
+#386 := (and #361 #381)
+#59 := (uf_4 uf_7 #46)
+#64 := (< #39 #39)
+#67 := (ite #64 #59 #47)
+#68 := (< #57 #67)
+#65 := (ite #64 #47 #54)
+#66 := (< #65 #57)
+#69 := (and #66 #68)
+#387 := (iff #69 #386)
+#384 := (iff #68 #381)
+#376 := (< #57 #47)
+#382 := (iff #376 #381)
+#383 := [rewrite]: #382
+#377 := (iff #68 #376)
+#374 := (= #67 #47)
+#369 := (ite false #59 #47)
+#372 := (= #369 #47)
+#373 := [rewrite]: #372
+#370 := (= #67 #369)
+#349 := (iff #64 false)
+#350 := [rewrite]: #349
+#371 := [monotonicity #350]: #370
+#375 := [trans #371 #373]: #374
+#378 := [monotonicity #375]: #377
+#385 := [trans #378 #383]: #384
+#367 := (iff #66 #361)
+#358 := (< #54 #57)
+#365 := (iff #358 #361)
+#366 := [rewrite]: #365
+#359 := (iff #66 #358)
+#356 := (= #65 #54)
+#351 := (ite false #47 #54)
+#354 := (= #351 #54)
+#355 := [rewrite]: #354
+#352 := (= #65 #351)
+#353 := [monotonicity #350]: #352
+#357 := [trans #353 #355]: #356
+#360 := [monotonicity #357]: #359
+#368 := [trans #360 #366]: #367
+#388 := [monotonicity #368 #385]: #387
+#346 := [asserted]: #69
+#389 := [mp #346 #388]: #386
+#391 := [and-elim #389]: #381
+#397 := (* -1::real #59)
+#398 := (+ #47 #397)
+#399 := (<= #398 0::real)
+#409 := (* -1::real #54)
+#410 := (+ #47 #409)
+#408 := (>= #410 0::real)
+#60 := (uf_4 uf_9 #46)
+#402 := (* -1::real #60)
+#403 := (+ #59 #402)
+#404 := (<= #403 0::real)
+#418 := (and #399 #404 #408)
+#73 := (<= #59 #60)
+#72 := (<= #47 #59)
+#74 := (and #72 #73)
+#71 := (<= #54 #47)
+#75 := (and #71 #74)
+#421 := (iff #75 #418)
+#412 := (and #399 #404)
+#415 := (and #408 #412)
+#419 := (iff #415 #418)
+#420 := [rewrite]: #419
+#416 := (iff #75 #415)
+#413 := (iff #74 #412)
+#405 := (iff #73 #404)
+#406 := [rewrite]: #405
+#400 := (iff #72 #399)
+#401 := [rewrite]: #400
+#414 := [monotonicity #401 #406]: #413
+#407 := (iff #71 #408)
+#411 := [rewrite]: #407
+#417 := [monotonicity #411 #414]: #416
+#422 := [trans #417 #420]: #421
+#348 := [asserted]: #75
+#423 := [mp #348 #422]: #418
+#424 := [and-elim #423]: #399
+#637 := (+ #28 #397)
+#639 := (>= #637 0::real)
+#636 := (= #28 #59)
+#666 := (= #59 #28)
+#664 := (= #46 #25)
+#662 := (= #25 #46)
+#663 := [monotonicity #656]: #662
+#665 := [symm #663]: #664
+#667 := [monotonicity #665]: #666
+#668 := [symm #667]: #636
+#669 := (not #636)
+#670 := (or #669 #639)
+#671 := [th-lemma]: #670
+#672 := [unit-resolution #671 #668]: #639
+#468 := (+ #57 #465)
+#471 := (<= #468 0::real)
+#444 := (not #471)
+#322 := (ite #296 #279 #47)
+#330 := (* -1::real #322)
+#331 := (+ #57 #330)
+#332 := (<= #331 0::real)
+#333 := (not #332)
+#445 := (iff #333 #444)
+#472 := (iff #332 #471)
+#469 := (= #331 #468)
+#466 := (= #330 #465)
+#463 := (= #322 #279)
+#1 := true
+#458 := (ite true #279 #47)
+#461 := (= #458 #279)
+#462 := [rewrite]: #461
+#459 := (= #322 #458)
+#450 := (iff #296 true)
+#451 := [iff-true #395]: #450
+#460 := [monotonicity #451]: #459
+#464 := [trans #460 #462]: #463
+#467 := [monotonicity #464]: #466
+#470 := [monotonicity #467]: #469
+#473 := [monotonicity #470]: #472
+#474 := [monotonicity #473]: #445
+#303 := (ite #296 #60 #59)
+#313 := (* -1::real #303)
+#314 := (+ #57 #313)
+#312 := (>= #314 0::real)
+#311 := (not #312)
+#338 := (and #311 #333)
+#52 := (< #39 #22)
+#61 := (ite #52 #59 #60)
+#62 := (< #57 #61)
+#53 := (= uf_10 uf_3)
+#55 := (ite #53 #28 #54)
+#56 := (ite #52 #47 #55)
+#58 := (< #56 #57)
+#63 := (and #58 #62)
+#341 := (iff #63 #338)
+#282 := (ite #52 #47 #279)
+#285 := (< #282 #57)
+#291 := (and #62 #285)
+#339 := (iff #291 #338)
+#336 := (iff #285 #333)
+#327 := (< #322 #57)
+#334 := (iff #327 #333)
+#335 := [rewrite]: #334
+#328 := (iff #285 #327)
+#325 := (= #282 #322)
+#297 := (not #296)
+#319 := (ite #297 #47 #279)
+#323 := (= #319 #322)
+#324 := [rewrite]: #323
+#320 := (= #282 #319)
+#298 := (iff #52 #297)
+#299 := [rewrite]: #298
+#321 := [monotonicity #299]: #320
+#326 := [trans #321 #324]: #325
+#329 := [monotonicity #326]: #328
+#337 := [trans #329 #335]: #336
+#317 := (iff #62 #311)
+#308 := (< #57 #303)
+#315 := (iff #308 #311)
+#316 := [rewrite]: #315
+#309 := (iff #62 #308)
+#306 := (= #61 #303)
+#300 := (ite #297 #59 #60)
+#304 := (= #300 #303)
+#305 := [rewrite]: #304
+#301 := (= #61 #300)
+#302 := [monotonicity #299]: #301
+#307 := [trans #302 #305]: #306
+#310 := [monotonicity #307]: #309
+#318 := [trans #310 #316]: #317
+#340 := [monotonicity #318 #337]: #339
+#294 := (iff #63 #291)
+#288 := (and #285 #62)
+#292 := (iff #288 #291)
+#293 := [rewrite]: #292
+#289 := (iff #63 #288)
+#286 := (iff #58 #285)
+#283 := (= #56 #282)
+#280 := (= #55 #279)
+#226 := (iff #53 #45)
+#278 := [rewrite]: #226
+#281 := [monotonicity #278]: #280
+#284 := [monotonicity #281]: #283
+#287 := [monotonicity #284]: #286
+#290 := [monotonicity #287]: #289
+#295 := [trans #290 #293]: #294
+#342 := [trans #295 #340]: #341
+#179 := [asserted]: #63
+#343 := [mp #179 #342]: #338
+#345 := [and-elim #343]: #333
+#475 := [mp #345 #474]: #444
+#673 := [th-lemma #475 #672 #424 #391 #661]: false
+#674 := [lemma #673]: #571
+[unit-resolution #674 #690]: false
+unsat
+985f86fd1ea01264c02b8076ffd658677bd4d29a 419 0
+#2 := false
+#194 := 0::real
+decl uf_4 :: (-> T2 T3 real)
+decl uf_6 :: (-> T1 T3)
+decl uf_3 :: T1
+#21 := uf_3
+#25 := (uf_6 uf_3)
+decl uf_5 :: T2
+#24 := uf_5
+#26 := (uf_4 uf_5 #25)
+decl uf_7 :: T2
+#27 := uf_7
+#28 := (uf_4 uf_7 #25)
+decl uf_10 :: T1
+#38 := uf_10
+#42 := (uf_6 uf_10)
+decl uf_9 :: T2
+#33 := uf_9
+#43 := (uf_4 uf_9 #42)
+#41 := (= uf_3 uf_10)
+#44 := (ite #41 #43 #28)
+#9 := 0::int
+decl uf_2 :: (-> T1 int)
+#39 := (uf_2 uf_10)
+#226 := -1::int
+#229 := (* -1::int #39)
+#22 := (uf_2 uf_3)
+#230 := (+ #22 #229)
+#228 := (>= #230 0::int)
+#236 := (ite #228 #44 #26)
+#192 := -1::real
+#244 := (* -1::real #236)
+#642 := (+ #26 #244)
+#643 := (<= #642 0::real)
+#567 := (= #26 #236)
+#227 := (not #228)
+decl uf_1 :: (-> int T1)
+#593 := (uf_1 #39)
+#660 := (= #593 uf_10)
+#594 := (= uf_10 #593)
+#4 := (:var 0 T1)
+#5 := (uf_2 #4)
+#546 := (pattern #5)
+#6 := (uf_1 #5)
+#93 := (= #4 #6)
+#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
+#96 := (forall (vars (?x1 T1)) #93)
+#550 := (iff #96 #547)
+#548 := (iff #93 #93)
+#549 := [refl]: #548
+#551 := [quant-intro #549]: #550
+#448 := (~ #96 #96)
+#450 := (~ #93 #93)
+#451 := [refl]: #450
+#449 := [nnf-pos #451]: #448
+#7 := (= #6 #4)
+#8 := (forall (vars (?x1 T1)) #7)
+#97 := (iff #8 #96)
+#94 := (iff #7 #93)
+#95 := [rewrite]: #94
+#98 := [quant-intro #95]: #97
+#92 := [asserted]: #8
+#101 := [mp #92 #98]: #96
+#446 := [mp~ #101 #449]: #96
+#552 := [mp #446 #551]: #547
+#595 := (not #547)
+#600 := (or #595 #594)
+#601 := [quant-inst]: #600
+#654 := [unit-resolution #601 #552]: #594
+#680 := [symm #654]: #660
+#681 := (= uf_3 #593)
+#591 := (uf_1 #22)
+#658 := (= #591 #593)
+#656 := (= #593 #591)
+#652 := (= #39 #22)
+#647 := (= #22 #39)
+#290 := (<= #230 0::int)
+#70 := (<= #22 #39)
+#388 := (iff #70 #290)
+#389 := [rewrite]: #388
+#341 := [asserted]: #70
+#390 := [mp #341 #389]: #290
+#646 := [hypothesis]: #228
+#648 := [th-lemma #646 #390]: #647
+#653 := [symm #648]: #652
+#657 := [monotonicity #653]: #656
+#659 := [symm #657]: #658
+#592 := (= uf_3 #591)
+#596 := (or #595 #592)
+#597 := [quant-inst]: #596
+#655 := [unit-resolution #597 #552]: #592
+#682 := [trans #655 #659]: #681
+#683 := [trans #682 #680]: #41
+#570 := (not #41)
+decl uf_11 :: T2
+#47 := uf_11
+#59 := (uf_4 uf_11 #42)
+#278 := (ite #41 #26 #59)
+#459 := (* -1::real #278)
+#637 := (+ #26 #459)
+#639 := (>= #637 0::real)
+#585 := (= #26 #278)
+#661 := [hypothesis]: #41
+#587 := (or #570 #585)
+#588 := [def-axiom]: #587
+#662 := [unit-resolution #588 #661]: #585
+#663 := (not #585)
+#664 := (or #663 #639)
+#665 := [th-lemma]: #664
+#666 := [unit-resolution #665 #662]: #639
+decl uf_8 :: T2
+#30 := uf_8
+#56 := (uf_4 uf_8 #42)
+#357 := (* -1::real #56)
+#358 := (+ #43 #357)
+#356 := (>= #358 0::real)
+#355 := (not #356)
+#374 := (* -1::real #59)
+#375 := (+ #56 #374)
+#373 := (>= #375 0::real)
+#376 := (not #373)
+#381 := (and #355 #376)
+#64 := (< #39 #39)
+#67 := (ite #64 #43 #59)
+#68 := (< #56 #67)
+#53 := (uf_4 uf_5 #42)
+#65 := (ite #64 #53 #43)
+#66 := (< #65 #56)
+#69 := (and #66 #68)
+#382 := (iff #69 #381)
+#379 := (iff #68 #376)
+#370 := (< #56 #59)
+#377 := (iff #370 #376)
+#378 := [rewrite]: #377
+#371 := (iff #68 #370)
+#368 := (= #67 #59)
+#363 := (ite false #43 #59)
+#366 := (= #363 #59)
+#367 := [rewrite]: #366
+#364 := (= #67 #363)
+#343 := (iff #64 false)
+#344 := [rewrite]: #343
+#365 := [monotonicity #344]: #364
+#369 := [trans #365 #367]: #368
+#372 := [monotonicity #369]: #371
+#380 := [trans #372 #378]: #379
+#361 := (iff #66 #355)
+#352 := (< #43 #56)
+#359 := (iff #352 #355)
+#360 := [rewrite]: #359
+#353 := (iff #66 #352)
+#350 := (= #65 #43)
+#345 := (ite false #53 #43)
+#348 := (= #345 #43)
+#349 := [rewrite]: #348
+#346 := (= #65 #345)
+#347 := [monotonicity #344]: #346
+#351 := [trans #347 #349]: #350
+#354 := [monotonicity #351]: #353
+#362 := [trans #354 #360]: #361
+#383 := [monotonicity #362 #380]: #382
+#340 := [asserted]: #69
+#384 := [mp #340 #383]: #381
+#385 := [and-elim #384]: #355
+#394 := (* -1::real #53)
+#395 := (+ #43 #394)
+#393 := (>= #395 0::real)
+#54 := (uf_4 uf_7 #42)
+#402 := (* -1::real #54)
+#403 := (+ #53 #402)
+#401 := (>= #403 0::real)
+#397 := (+ #43 #374)
+#398 := (<= #397 0::real)
+#412 := (and #393 #398 #401)
+#73 := (<= #43 #59)
+#72 := (<= #53 #43)
+#74 := (and #72 #73)
+#71 := (<= #54 #53)
+#75 := (and #71 #74)
+#415 := (iff #75 #412)
+#406 := (and #393 #398)
+#409 := (and #401 #406)
+#413 := (iff #409 #412)
+#414 := [rewrite]: #413
+#410 := (iff #75 #409)
+#407 := (iff #74 #406)
+#399 := (iff #73 #398)
+#400 := [rewrite]: #399
+#392 := (iff #72 #393)
+#396 := [rewrite]: #392
+#408 := [monotonicity #396 #400]: #407
+#404 := (iff #71 #401)
+#405 := [rewrite]: #404
+#411 := [monotonicity #405 #408]: #410
+#416 := [trans #411 #414]: #415
+#342 := [asserted]: #75
+#417 := [mp #342 #416]: #412
+#418 := [and-elim #417]: #393
+#650 := (+ #26 #394)
+#651 := (<= #650 0::real)
+#649 := (= #26 #53)
+#671 := (= #53 #26)
+#669 := (= #42 #25)
+#667 := (= #25 #42)
+#668 := [monotonicity #661]: #667
+#670 := [symm #668]: #669
+#672 := [monotonicity #670]: #671
+#673 := [symm #672]: #649
+#674 := (not #649)
+#675 := (or #674 #651)
+#676 := [th-lemma]: #675
+#677 := [unit-resolution #676 #673]: #651
+#462 := (+ #56 #459)
+#465 := (>= #462 0::real)
+#438 := (not #465)
+#316 := (ite #290 #278 #43)
+#326 := (* -1::real #316)
+#327 := (+ #56 #326)
+#325 := (>= #327 0::real)
+#324 := (not #325)
+#439 := (iff #324 #438)
+#466 := (iff #325 #465)
+#463 := (= #327 #462)
+#460 := (= #326 #459)
+#457 := (= #316 #278)
+#1 := true
+#452 := (ite true #278 #43)
+#455 := (= #452 #278)
+#456 := [rewrite]: #455
+#453 := (= #316 #452)
+#444 := (iff #290 true)
+#445 := [iff-true #390]: #444
+#454 := [monotonicity #445]: #453
+#458 := [trans #454 #456]: #457
+#461 := [monotonicity #458]: #460
+#464 := [monotonicity #461]: #463
+#467 := [monotonicity #464]: #466
+#468 := [monotonicity #467]: #439
+#297 := (ite #290 #54 #53)
+#305 := (* -1::real #297)
+#306 := (+ #56 #305)
+#307 := (<= #306 0::real)
+#308 := (not #307)
+#332 := (and #308 #324)
+#58 := (= uf_10 uf_3)
+#60 := (ite #58 #26 #59)
+#52 := (< #39 #22)
+#61 := (ite #52 #43 #60)
+#62 := (< #56 #61)
+#55 := (ite #52 #53 #54)
+#57 := (< #55 #56)
+#63 := (and #57 #62)
+#335 := (iff #63 #332)
+#281 := (ite #52 #43 #278)
+#284 := (< #56 #281)
+#287 := (and #57 #284)
+#333 := (iff #287 #332)
+#330 := (iff #284 #324)
+#321 := (< #56 #316)
+#328 := (iff #321 #324)
+#329 := [rewrite]: #328
+#322 := (iff #284 #321)
+#319 := (= #281 #316)
+#291 := (not #290)
+#313 := (ite #291 #43 #278)
+#317 := (= #313 #316)
+#318 := [rewrite]: #317
+#314 := (= #281 #313)
+#292 := (iff #52 #291)
+#293 := [rewrite]: #292
+#315 := [monotonicity #293]: #314
+#320 := [trans #315 #318]: #319
+#323 := [monotonicity #320]: #322
+#331 := [trans #323 #329]: #330
+#311 := (iff #57 #308)
+#302 := (< #297 #56)
+#309 := (iff #302 #308)
+#310 := [rewrite]: #309
+#303 := (iff #57 #302)
+#300 := (= #55 #297)
+#294 := (ite #291 #53 #54)
+#298 := (= #294 #297)
+#299 := [rewrite]: #298
+#295 := (= #55 #294)
+#296 := [monotonicity #293]: #295
+#301 := [trans #296 #299]: #300
+#304 := [monotonicity #301]: #303
+#312 := [trans #304 #310]: #311
+#334 := [monotonicity #312 #331]: #333
+#288 := (iff #63 #287)
+#285 := (iff #62 #284)
+#282 := (= #61 #281)
+#279 := (= #60 #278)
+#225 := (iff #58 #41)
+#277 := [rewrite]: #225
+#280 := [monotonicity #277]: #279
+#283 := [monotonicity #280]: #282
+#286 := [monotonicity #283]: #285
+#289 := [monotonicity #286]: #288
+#336 := [trans #289 #334]: #335
+#179 := [asserted]: #63
+#337 := [mp #179 #336]: #332
+#339 := [and-elim #337]: #324
+#469 := [mp #339 #468]: #438
+#678 := [th-lemma #469 #677 #418 #385 #666]: false
+#679 := [lemma #678]: #570
+#684 := [unit-resolution #679 #683]: false
+#685 := [lemma #684]: #227
+#577 := (or #228 #567)
+#578 := [def-axiom]: #577
+#645 := [unit-resolution #578 #685]: #567
+#686 := (not #567)
+#687 := (or #686 #643)
+#688 := [th-lemma]: #687
+#689 := [unit-resolution #688 #645]: #643
+#31 := (uf_4 uf_8 #25)
+#245 := (+ #31 #244)
+#246 := (<= #245 0::real)
+#247 := (not #246)
+#34 := (uf_4 uf_9 #25)
+#48 := (uf_4 uf_11 #25)
+#255 := (ite #228 #48 #34)
+#264 := (* -1::real #255)
+#265 := (+ #31 #264)
+#263 := (>= #265 0::real)
+#266 := (not #263)
+#271 := (and #247 #266)
+#40 := (< #22 #39)
+#49 := (ite #40 #34 #48)
+#50 := (< #31 #49)
+#45 := (ite #40 #26 #44)
+#46 := (< #45 #31)
+#51 := (and #46 #50)
+#272 := (iff #51 #271)
+#269 := (iff #50 #266)
+#260 := (< #31 #255)
+#267 := (iff #260 #266)
+#268 := [rewrite]: #267
+#261 := (iff #50 #260)
+#258 := (= #49 #255)
+#252 := (ite #227 #34 #48)
+#256 := (= #252 #255)
+#257 := [rewrite]: #256
+#253 := (= #49 #252)
+#231 := (iff #40 #227)
+#232 := [rewrite]: #231
+#254 := [monotonicity #232]: #253
+#259 := [trans #254 #257]: #258
+#262 := [monotonicity #259]: #261
+#270 := [trans #262 #268]: #269
+#250 := (iff #46 #247)
+#241 := (< #236 #31)
+#248 := (iff #241 #247)
+#249 := [rewrite]: #248
+#242 := (iff #46 #241)
+#239 := (= #45 #236)
+#233 := (ite #227 #26 #44)
+#237 := (= #233 #236)
+#238 := [rewrite]: #237
+#234 := (= #45 #233)
+#235 := [monotonicity #232]: #234
+#240 := [trans #235 #238]: #239
+#243 := [monotonicity #240]: #242
+#251 := [trans #243 #249]: #250
+#273 := [monotonicity #251 #270]: #272
+#178 := [asserted]: #51
+#274 := [mp #178 #273]: #271
+#275 := [and-elim #274]: #247
+#196 := (* -1::real #31)
+#212 := (+ #26 #196)
+#213 := (<= #212 0::real)
+#214 := (not #213)
+#197 := (+ #28 #196)
+#195 := (>= #197 0::real)
+#193 := (not #195)
+#219 := (and #193 #214)
+#23 := (< #22 #22)
+#35 := (ite #23 #34 #26)
+#36 := (< #31 #35)
+#29 := (ite #23 #26 #28)
+#32 := (< #29 #31)
+#37 := (and #32 #36)
+#220 := (iff #37 #219)
+#217 := (iff #36 #214)
+#209 := (< #31 #26)
+#215 := (iff #209 #214)
+#216 := [rewrite]: #215
+#210 := (iff #36 #209)
+#207 := (= #35 #26)
+#202 := (ite false #34 #26)
+#205 := (= #202 #26)
+#206 := [rewrite]: #205
+#203 := (= #35 #202)
+#180 := (iff #23 false)
+#181 := [rewrite]: #180
+#204 := [monotonicity #181]: #203
+#208 := [trans #204 #206]: #207
+#211 := [monotonicity #208]: #210
+#218 := [trans #211 #216]: #217
+#200 := (iff #32 #193)
+#189 := (< #28 #31)
+#198 := (iff #189 #193)
+#199 := [rewrite]: #198
+#190 := (iff #32 #189)
+#187 := (= #29 #28)
+#182 := (ite false #26 #28)
+#185 := (= #182 #28)
+#186 := [rewrite]: #185
+#183 := (= #29 #182)
+#184 := [monotonicity #181]: #183
+#188 := [trans #184 #186]: #187
+#191 := [monotonicity #188]: #190
+#201 := [trans #191 #199]: #200
+#221 := [monotonicity #201 #218]: #220
+#177 := [asserted]: #37
+#222 := [mp #177 #221]: #219
+#224 := [and-elim #222]: #214
+[th-lemma #224 #275 #689]: false
+unsat
+00b949278548f13329cf92f11a0ad2161fa40793 907 0
#2 := false
#299 := 0::real
decl uf_1 :: (-> T3 T2 real)
@@ -906,856 +1755,7 @@
#1366 := [unit-resolution #1233 #1365]: #1231
[th-lemma #1366 #1364 #1362]: false
unsat
-NQHwTeL311Tq3wf2s5BReA 419 0
-#2 := false
-#194 := 0::real
-decl uf_4 :: (-> T2 T3 real)
-decl uf_6 :: (-> T1 T3)
-decl uf_3 :: T1
-#21 := uf_3
-#25 := (uf_6 uf_3)
-decl uf_5 :: T2
-#24 := uf_5
-#26 := (uf_4 uf_5 #25)
-decl uf_7 :: T2
-#27 := uf_7
-#28 := (uf_4 uf_7 #25)
-decl uf_10 :: T1
-#38 := uf_10
-#42 := (uf_6 uf_10)
-decl uf_9 :: T2
-#33 := uf_9
-#43 := (uf_4 uf_9 #42)
-#41 := (= uf_3 uf_10)
-#44 := (ite #41 #43 #28)
-#9 := 0::int
-decl uf_2 :: (-> T1 int)
-#39 := (uf_2 uf_10)
-#226 := -1::int
-#229 := (* -1::int #39)
-#22 := (uf_2 uf_3)
-#230 := (+ #22 #229)
-#228 := (>= #230 0::int)
-#236 := (ite #228 #44 #26)
-#192 := -1::real
-#244 := (* -1::real #236)
-#642 := (+ #26 #244)
-#643 := (<= #642 0::real)
-#567 := (= #26 #236)
-#227 := (not #228)
-decl uf_1 :: (-> int T1)
-#593 := (uf_1 #39)
-#660 := (= #593 uf_10)
-#594 := (= uf_10 #593)
-#4 := (:var 0 T1)
-#5 := (uf_2 #4)
-#546 := (pattern #5)
-#6 := (uf_1 #5)
-#93 := (= #4 #6)
-#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
-#96 := (forall (vars (?x1 T1)) #93)
-#550 := (iff #96 #547)
-#548 := (iff #93 #93)
-#549 := [refl]: #548
-#551 := [quant-intro #549]: #550
-#448 := (~ #96 #96)
-#450 := (~ #93 #93)
-#451 := [refl]: #450
-#449 := [nnf-pos #451]: #448
-#7 := (= #6 #4)
-#8 := (forall (vars (?x1 T1)) #7)
-#97 := (iff #8 #96)
-#94 := (iff #7 #93)
-#95 := [rewrite]: #94
-#98 := [quant-intro #95]: #97
-#92 := [asserted]: #8
-#101 := [mp #92 #98]: #96
-#446 := [mp~ #101 #449]: #96
-#552 := [mp #446 #551]: #547
-#595 := (not #547)
-#600 := (or #595 #594)
-#601 := [quant-inst]: #600
-#654 := [unit-resolution #601 #552]: #594
-#680 := [symm #654]: #660
-#681 := (= uf_3 #593)
-#591 := (uf_1 #22)
-#658 := (= #591 #593)
-#656 := (= #593 #591)
-#652 := (= #39 #22)
-#647 := (= #22 #39)
-#290 := (<= #230 0::int)
-#70 := (<= #22 #39)
-#388 := (iff #70 #290)
-#389 := [rewrite]: #388
-#341 := [asserted]: #70
-#390 := [mp #341 #389]: #290
-#646 := [hypothesis]: #228
-#648 := [th-lemma #646 #390]: #647
-#653 := [symm #648]: #652
-#657 := [monotonicity #653]: #656
-#659 := [symm #657]: #658
-#592 := (= uf_3 #591)
-#596 := (or #595 #592)
-#597 := [quant-inst]: #596
-#655 := [unit-resolution #597 #552]: #592
-#682 := [trans #655 #659]: #681
-#683 := [trans #682 #680]: #41
-#570 := (not #41)
-decl uf_11 :: T2
-#47 := uf_11
-#59 := (uf_4 uf_11 #42)
-#278 := (ite #41 #26 #59)
-#459 := (* -1::real #278)
-#637 := (+ #26 #459)
-#639 := (>= #637 0::real)
-#585 := (= #26 #278)
-#661 := [hypothesis]: #41
-#587 := (or #570 #585)
-#588 := [def-axiom]: #587
-#662 := [unit-resolution #588 #661]: #585
-#663 := (not #585)
-#664 := (or #663 #639)
-#665 := [th-lemma]: #664
-#666 := [unit-resolution #665 #662]: #639
-decl uf_8 :: T2
-#30 := uf_8
-#56 := (uf_4 uf_8 #42)
-#357 := (* -1::real #56)
-#358 := (+ #43 #357)
-#356 := (>= #358 0::real)
-#355 := (not #356)
-#374 := (* -1::real #59)
-#375 := (+ #56 #374)
-#373 := (>= #375 0::real)
-#376 := (not #373)
-#381 := (and #355 #376)
-#64 := (< #39 #39)
-#67 := (ite #64 #43 #59)
-#68 := (< #56 #67)
-#53 := (uf_4 uf_5 #42)
-#65 := (ite #64 #53 #43)
-#66 := (< #65 #56)
-#69 := (and #66 #68)
-#382 := (iff #69 #381)
-#379 := (iff #68 #376)
-#370 := (< #56 #59)
-#377 := (iff #370 #376)
-#378 := [rewrite]: #377
-#371 := (iff #68 #370)
-#368 := (= #67 #59)
-#363 := (ite false #43 #59)
-#366 := (= #363 #59)
-#367 := [rewrite]: #366
-#364 := (= #67 #363)
-#343 := (iff #64 false)
-#344 := [rewrite]: #343
-#365 := [monotonicity #344]: #364
-#369 := [trans #365 #367]: #368
-#372 := [monotonicity #369]: #371
-#380 := [trans #372 #378]: #379
-#361 := (iff #66 #355)
-#352 := (< #43 #56)
-#359 := (iff #352 #355)
-#360 := [rewrite]: #359
-#353 := (iff #66 #352)
-#350 := (= #65 #43)
-#345 := (ite false #53 #43)
-#348 := (= #345 #43)
-#349 := [rewrite]: #348
-#346 := (= #65 #345)
-#347 := [monotonicity #344]: #346
-#351 := [trans #347 #349]: #350
-#354 := [monotonicity #351]: #353
-#362 := [trans #354 #360]: #361
-#383 := [monotonicity #362 #380]: #382
-#340 := [asserted]: #69
-#384 := [mp #340 #383]: #381
-#385 := [and-elim #384]: #355
-#394 := (* -1::real #53)
-#395 := (+ #43 #394)
-#393 := (>= #395 0::real)
-#54 := (uf_4 uf_7 #42)
-#402 := (* -1::real #54)
-#403 := (+ #53 #402)
-#401 := (>= #403 0::real)
-#397 := (+ #43 #374)
-#398 := (<= #397 0::real)
-#412 := (and #393 #398 #401)
-#73 := (<= #43 #59)
-#72 := (<= #53 #43)
-#74 := (and #72 #73)
-#71 := (<= #54 #53)
-#75 := (and #71 #74)
-#415 := (iff #75 #412)
-#406 := (and #393 #398)
-#409 := (and #401 #406)
-#413 := (iff #409 #412)
-#414 := [rewrite]: #413
-#410 := (iff #75 #409)
-#407 := (iff #74 #406)
-#399 := (iff #73 #398)
-#400 := [rewrite]: #399
-#392 := (iff #72 #393)
-#396 := [rewrite]: #392
-#408 := [monotonicity #396 #400]: #407
-#404 := (iff #71 #401)
-#405 := [rewrite]: #404
-#411 := [monotonicity #405 #408]: #410
-#416 := [trans #411 #414]: #415
-#342 := [asserted]: #75
-#417 := [mp #342 #416]: #412
-#418 := [and-elim #417]: #393
-#650 := (+ #26 #394)
-#651 := (<= #650 0::real)
-#649 := (= #26 #53)
-#671 := (= #53 #26)
-#669 := (= #42 #25)
-#667 := (= #25 #42)
-#668 := [monotonicity #661]: #667
-#670 := [symm #668]: #669
-#672 := [monotonicity #670]: #671
-#673 := [symm #672]: #649
-#674 := (not #649)
-#675 := (or #674 #651)
-#676 := [th-lemma]: #675
-#677 := [unit-resolution #676 #673]: #651
-#462 := (+ #56 #459)
-#465 := (>= #462 0::real)
-#438 := (not #465)
-#316 := (ite #290 #278 #43)
-#326 := (* -1::real #316)
-#327 := (+ #56 #326)
-#325 := (>= #327 0::real)
-#324 := (not #325)
-#439 := (iff #324 #438)
-#466 := (iff #325 #465)
-#463 := (= #327 #462)
-#460 := (= #326 #459)
-#457 := (= #316 #278)
-#1 := true
-#452 := (ite true #278 #43)
-#455 := (= #452 #278)
-#456 := [rewrite]: #455
-#453 := (= #316 #452)
-#444 := (iff #290 true)
-#445 := [iff-true #390]: #444
-#454 := [monotonicity #445]: #453
-#458 := [trans #454 #456]: #457
-#461 := [monotonicity #458]: #460
-#464 := [monotonicity #461]: #463
-#467 := [monotonicity #464]: #466
-#468 := [monotonicity #467]: #439
-#297 := (ite #290 #54 #53)
-#305 := (* -1::real #297)
-#306 := (+ #56 #305)
-#307 := (<= #306 0::real)
-#308 := (not #307)
-#332 := (and #308 #324)
-#58 := (= uf_10 uf_3)
-#60 := (ite #58 #26 #59)
-#52 := (< #39 #22)
-#61 := (ite #52 #43 #60)
-#62 := (< #56 #61)
-#55 := (ite #52 #53 #54)
-#57 := (< #55 #56)
-#63 := (and #57 #62)
-#335 := (iff #63 #332)
-#281 := (ite #52 #43 #278)
-#284 := (< #56 #281)
-#287 := (and #57 #284)
-#333 := (iff #287 #332)
-#330 := (iff #284 #324)
-#321 := (< #56 #316)
-#328 := (iff #321 #324)
-#329 := [rewrite]: #328
-#322 := (iff #284 #321)
-#319 := (= #281 #316)
-#291 := (not #290)
-#313 := (ite #291 #43 #278)
-#317 := (= #313 #316)
-#318 := [rewrite]: #317
-#314 := (= #281 #313)
-#292 := (iff #52 #291)
-#293 := [rewrite]: #292
-#315 := [monotonicity #293]: #314
-#320 := [trans #315 #318]: #319
-#323 := [monotonicity #320]: #322
-#331 := [trans #323 #329]: #330
-#311 := (iff #57 #308)
-#302 := (< #297 #56)
-#309 := (iff #302 #308)
-#310 := [rewrite]: #309
-#303 := (iff #57 #302)
-#300 := (= #55 #297)
-#294 := (ite #291 #53 #54)
-#298 := (= #294 #297)
-#299 := [rewrite]: #298
-#295 := (= #55 #294)
-#296 := [monotonicity #293]: #295
-#301 := [trans #296 #299]: #300
-#304 := [monotonicity #301]: #303
-#312 := [trans #304 #310]: #311
-#334 := [monotonicity #312 #331]: #333
-#288 := (iff #63 #287)
-#285 := (iff #62 #284)
-#282 := (= #61 #281)
-#279 := (= #60 #278)
-#225 := (iff #58 #41)
-#277 := [rewrite]: #225
-#280 := [monotonicity #277]: #279
-#283 := [monotonicity #280]: #282
-#286 := [monotonicity #283]: #285
-#289 := [monotonicity #286]: #288
-#336 := [trans #289 #334]: #335
-#179 := [asserted]: #63
-#337 := [mp #179 #336]: #332
-#339 := [and-elim #337]: #324
-#469 := [mp #339 #468]: #438
-#678 := [th-lemma #469 #677 #418 #385 #666]: false
-#679 := [lemma #678]: #570
-#684 := [unit-resolution #679 #683]: false
-#685 := [lemma #684]: #227
-#577 := (or #228 #567)
-#578 := [def-axiom]: #577
-#645 := [unit-resolution #578 #685]: #567
-#686 := (not #567)
-#687 := (or #686 #643)
-#688 := [th-lemma]: #687
-#689 := [unit-resolution #688 #645]: #643
-#31 := (uf_4 uf_8 #25)
-#245 := (+ #31 #244)
-#246 := (<= #245 0::real)
-#247 := (not #246)
-#34 := (uf_4 uf_9 #25)
-#48 := (uf_4 uf_11 #25)
-#255 := (ite #228 #48 #34)
-#264 := (* -1::real #255)
-#265 := (+ #31 #264)
-#263 := (>= #265 0::real)
-#266 := (not #263)
-#271 := (and #247 #266)
-#40 := (< #22 #39)
-#49 := (ite #40 #34 #48)
-#50 := (< #31 #49)
-#45 := (ite #40 #26 #44)
-#46 := (< #45 #31)
-#51 := (and #46 #50)
-#272 := (iff #51 #271)
-#269 := (iff #50 #266)
-#260 := (< #31 #255)
-#267 := (iff #260 #266)
-#268 := [rewrite]: #267
-#261 := (iff #50 #260)
-#258 := (= #49 #255)
-#252 := (ite #227 #34 #48)
-#256 := (= #252 #255)
-#257 := [rewrite]: #256
-#253 := (= #49 #252)
-#231 := (iff #40 #227)
-#232 := [rewrite]: #231
-#254 := [monotonicity #232]: #253
-#259 := [trans #254 #257]: #258
-#262 := [monotonicity #259]: #261
-#270 := [trans #262 #268]: #269
-#250 := (iff #46 #247)
-#241 := (< #236 #31)
-#248 := (iff #241 #247)
-#249 := [rewrite]: #248
-#242 := (iff #46 #241)
-#239 := (= #45 #236)
-#233 := (ite #227 #26 #44)
-#237 := (= #233 #236)
-#238 := [rewrite]: #237
-#234 := (= #45 #233)
-#235 := [monotonicity #232]: #234
-#240 := [trans #235 #238]: #239
-#243 := [monotonicity #240]: #242
-#251 := [trans #243 #249]: #250
-#273 := [monotonicity #251 #270]: #272
-#178 := [asserted]: #51
-#274 := [mp #178 #273]: #271
-#275 := [and-elim #274]: #247
-#196 := (* -1::real #31)
-#212 := (+ #26 #196)
-#213 := (<= #212 0::real)
-#214 := (not #213)
-#197 := (+ #28 #196)
-#195 := (>= #197 0::real)
-#193 := (not #195)
-#219 := (and #193 #214)
-#23 := (< #22 #22)
-#35 := (ite #23 #34 #26)
-#36 := (< #31 #35)
-#29 := (ite #23 #26 #28)
-#32 := (< #29 #31)
-#37 := (and #32 #36)
-#220 := (iff #37 #219)
-#217 := (iff #36 #214)
-#209 := (< #31 #26)
-#215 := (iff #209 #214)
-#216 := [rewrite]: #215
-#210 := (iff #36 #209)
-#207 := (= #35 #26)
-#202 := (ite false #34 #26)
-#205 := (= #202 #26)
-#206 := [rewrite]: #205
-#203 := (= #35 #202)
-#180 := (iff #23 false)
-#181 := [rewrite]: #180
-#204 := [monotonicity #181]: #203
-#208 := [trans #204 #206]: #207
-#211 := [monotonicity #208]: #210
-#218 := [trans #211 #216]: #217
-#200 := (iff #32 #193)
-#189 := (< #28 #31)
-#198 := (iff #189 #193)
-#199 := [rewrite]: #198
-#190 := (iff #32 #189)
-#187 := (= #29 #28)
-#182 := (ite false #26 #28)
-#185 := (= #182 #28)
-#186 := [rewrite]: #185
-#183 := (= #29 #182)
-#184 := [monotonicity #181]: #183
-#188 := [trans #184 #186]: #187
-#191 := [monotonicity #188]: #190
-#201 := [trans #191 #199]: #200
-#221 := [monotonicity #201 #218]: #220
-#177 := [asserted]: #37
-#222 := [mp #177 #221]: #219
-#224 := [and-elim #222]: #214
-[th-lemma #224 #275 #689]: false
-unsat
-NX/HT1QOfbspC2LtZNKpBA 428 0
-#2 := false
-decl uf_10 :: T1
-#38 := uf_10
-decl uf_3 :: T1
-#21 := uf_3
-#45 := (= uf_3 uf_10)
-decl uf_1 :: (-> int T1)
-decl uf_2 :: (-> T1 int)
-#39 := (uf_2 uf_10)
-#588 := (uf_1 #39)
-#686 := (= #588 uf_10)
-#589 := (= uf_10 #588)
-#4 := (:var 0 T1)
-#5 := (uf_2 #4)
-#541 := (pattern #5)
-#6 := (uf_1 #5)
-#93 := (= #4 #6)
-#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
-#96 := (forall (vars (?x1 T1)) #93)
-#545 := (iff #96 #542)
-#543 := (iff #93 #93)
-#544 := [refl]: #543
-#546 := [quant-intro #544]: #545
-#454 := (~ #96 #96)
-#456 := (~ #93 #93)
-#457 := [refl]: #456
-#455 := [nnf-pos #457]: #454
-#7 := (= #6 #4)
-#8 := (forall (vars (?x1 T1)) #7)
-#97 := (iff #8 #96)
-#94 := (iff #7 #93)
-#95 := [rewrite]: #94
-#98 := [quant-intro #95]: #97
-#92 := [asserted]: #8
-#101 := [mp #92 #98]: #96
-#452 := [mp~ #101 #455]: #96
-#547 := [mp #452 #546]: #542
-#590 := (not #542)
-#595 := (or #590 #589)
-#596 := [quant-inst]: #595
-#680 := [unit-resolution #596 #547]: #589
-#687 := [symm #680]: #686
-#688 := (= uf_3 #588)
-#22 := (uf_2 uf_3)
-#586 := (uf_1 #22)
-#684 := (= #586 #588)
-#682 := (= #588 #586)
-#678 := (= #39 #22)
-#676 := (= #22 #39)
-#9 := 0::int
-#227 := -1::int
-#230 := (* -1::int #39)
-#231 := (+ #22 #230)
-#296 := (<= #231 0::int)
-#70 := (<= #22 #39)
-#393 := (iff #70 #296)
-#394 := [rewrite]: #393
-#347 := [asserted]: #70
-#395 := [mp #347 #394]: #296
-#229 := (>= #231 0::int)
-decl uf_4 :: (-> T2 T3 real)
-decl uf_6 :: (-> T1 T3)
-#25 := (uf_6 uf_3)
-decl uf_7 :: T2
-#27 := uf_7
-#28 := (uf_4 uf_7 #25)
-decl uf_9 :: T2
-#33 := uf_9
-#34 := (uf_4 uf_9 #25)
-#46 := (uf_6 uf_10)
-decl uf_5 :: T2
-#24 := uf_5
-#47 := (uf_4 uf_5 #46)
-#48 := (ite #45 #47 #34)
-#256 := (ite #229 #48 #28)
-#568 := (= #28 #256)
-#648 := (not #568)
-#194 := 0::real
-#192 := -1::real
-#265 := (* -1::real #256)
-#640 := (+ #28 #265)
-#642 := (>= #640 0::real)
-#645 := (not #642)
-#643 := [hypothesis]: #642
-decl uf_8 :: T2
-#30 := uf_8
-#31 := (uf_4 uf_8 #25)
-#266 := (+ #31 #265)
-#264 := (>= #266 0::real)
-#267 := (not #264)
-#26 := (uf_4 uf_5 #25)
-decl uf_11 :: T2
-#41 := uf_11
-#42 := (uf_4 uf_11 #25)
-#237 := (ite #229 #42 #26)
-#245 := (* -1::real #237)
-#246 := (+ #31 #245)
-#247 := (<= #246 0::real)
-#248 := (not #247)
-#272 := (and #248 #267)
-#40 := (< #22 #39)
-#49 := (ite #40 #28 #48)
-#50 := (< #31 #49)
-#43 := (ite #40 #26 #42)
-#44 := (< #43 #31)
-#51 := (and #44 #50)
-#273 := (iff #51 #272)
-#270 := (iff #50 #267)
-#261 := (< #31 #256)
-#268 := (iff #261 #267)
-#269 := [rewrite]: #268
-#262 := (iff #50 #261)
-#259 := (= #49 #256)
-#228 := (not #229)
-#253 := (ite #228 #28 #48)
-#257 := (= #253 #256)
-#258 := [rewrite]: #257
-#254 := (= #49 #253)
-#232 := (iff #40 #228)
-#233 := [rewrite]: #232
-#255 := [monotonicity #233]: #254
-#260 := [trans #255 #258]: #259
-#263 := [monotonicity #260]: #262
-#271 := [trans #263 #269]: #270
-#251 := (iff #44 #248)
-#242 := (< #237 #31)
-#249 := (iff #242 #248)
-#250 := [rewrite]: #249
-#243 := (iff #44 #242)
-#240 := (= #43 #237)
-#234 := (ite #228 #26 #42)
-#238 := (= #234 #237)
-#239 := [rewrite]: #238
-#235 := (= #43 #234)
-#236 := [monotonicity #233]: #235
-#241 := [trans #236 #239]: #240
-#244 := [monotonicity #241]: #243
-#252 := [trans #244 #250]: #251
-#274 := [monotonicity #252 #271]: #273
-#178 := [asserted]: #51
-#275 := [mp #178 #274]: #272
-#277 := [and-elim #275]: #267
-#196 := (* -1::real #31)
-#197 := (+ #28 #196)
-#195 := (>= #197 0::real)
-#193 := (not #195)
-#213 := (* -1::real #34)
-#214 := (+ #31 #213)
-#212 := (>= #214 0::real)
-#215 := (not #212)
-#220 := (and #193 #215)
-#23 := (< #22 #22)
-#35 := (ite #23 #28 #34)
-#36 := (< #31 #35)
-#29 := (ite #23 #26 #28)
-#32 := (< #29 #31)
-#37 := (and #32 #36)
-#221 := (iff #37 #220)
-#218 := (iff #36 #215)
-#209 := (< #31 #34)
-#216 := (iff #209 #215)
-#217 := [rewrite]: #216
-#210 := (iff #36 #209)
-#207 := (= #35 #34)
-#202 := (ite false #28 #34)
-#205 := (= #202 #34)
-#206 := [rewrite]: #205
-#203 := (= #35 #202)
-#180 := (iff #23 false)
-#181 := [rewrite]: #180
-#204 := [monotonicity #181]: #203
-#208 := [trans #204 #206]: #207
-#211 := [monotonicity #208]: #210
-#219 := [trans #211 #217]: #218
-#200 := (iff #32 #193)
-#189 := (< #28 #31)
-#198 := (iff #189 #193)
-#199 := [rewrite]: #198
-#190 := (iff #32 #189)
-#187 := (= #29 #28)
-#182 := (ite false #26 #28)
-#185 := (= #182 #28)
-#186 := [rewrite]: #185
-#183 := (= #29 #182)
-#184 := [monotonicity #181]: #183
-#188 := [trans #184 #186]: #187
-#191 := [monotonicity #188]: #190
-#201 := [trans #191 #199]: #200
-#222 := [monotonicity #201 #219]: #221
-#177 := [asserted]: #37
-#223 := [mp #177 #222]: #220
-#224 := [and-elim #223]: #193
-#644 := [th-lemma #224 #277 #643]: false
-#646 := [lemma #644]: #645
-#647 := [hypothesis]: #568
-#649 := (or #648 #642)
-#650 := [th-lemma]: #649
-#651 := [unit-resolution #650 #647 #646]: false
-#652 := [lemma #651]: #648
-#578 := (or #229 #568)
-#579 := [def-axiom]: #578
-#675 := [unit-resolution #579 #652]: #229
-#677 := [th-lemma #675 #395]: #676
-#679 := [symm #677]: #678
-#683 := [monotonicity #679]: #682
-#685 := [symm #683]: #684
-#587 := (= uf_3 #586)
-#591 := (or #590 #587)
-#592 := [quant-inst]: #591
-#681 := [unit-resolution #592 #547]: #587
-#689 := [trans #681 #685]: #688
-#690 := [trans #689 #687]: #45
-#571 := (not #45)
-#54 := (uf_4 uf_11 #46)
-#279 := (ite #45 #28 #54)
-#465 := (* -1::real #279)
-#632 := (+ #28 #465)
-#633 := (<= #632 0::real)
-#580 := (= #28 #279)
-#656 := [hypothesis]: #45
-#582 := (or #571 #580)
-#583 := [def-axiom]: #582
-#657 := [unit-resolution #583 #656]: #580
-#658 := (not #580)
-#659 := (or #658 #633)
-#660 := [th-lemma]: #659
-#661 := [unit-resolution #660 #657]: #633
-#57 := (uf_4 uf_8 #46)
-#363 := (* -1::real #57)
-#379 := (+ #47 #363)
-#380 := (<= #379 0::real)
-#381 := (not #380)
-#364 := (+ #54 #363)
-#362 := (>= #364 0::real)
-#361 := (not #362)
-#386 := (and #361 #381)
-#59 := (uf_4 uf_7 #46)
-#64 := (< #39 #39)
-#67 := (ite #64 #59 #47)
-#68 := (< #57 #67)
-#65 := (ite #64 #47 #54)
-#66 := (< #65 #57)
-#69 := (and #66 #68)
-#387 := (iff #69 #386)
-#384 := (iff #68 #381)
-#376 := (< #57 #47)
-#382 := (iff #376 #381)
-#383 := [rewrite]: #382
-#377 := (iff #68 #376)
-#374 := (= #67 #47)
-#369 := (ite false #59 #47)
-#372 := (= #369 #47)
-#373 := [rewrite]: #372
-#370 := (= #67 #369)
-#349 := (iff #64 false)
-#350 := [rewrite]: #349
-#371 := [monotonicity #350]: #370
-#375 := [trans #371 #373]: #374
-#378 := [monotonicity #375]: #377
-#385 := [trans #378 #383]: #384
-#367 := (iff #66 #361)
-#358 := (< #54 #57)
-#365 := (iff #358 #361)
-#366 := [rewrite]: #365
-#359 := (iff #66 #358)
-#356 := (= #65 #54)
-#351 := (ite false #47 #54)
-#354 := (= #351 #54)
-#355 := [rewrite]: #354
-#352 := (= #65 #351)
-#353 := [monotonicity #350]: #352
-#357 := [trans #353 #355]: #356
-#360 := [monotonicity #357]: #359
-#368 := [trans #360 #366]: #367
-#388 := [monotonicity #368 #385]: #387
-#346 := [asserted]: #69
-#389 := [mp #346 #388]: #386
-#391 := [and-elim #389]: #381
-#397 := (* -1::real #59)
-#398 := (+ #47 #397)
-#399 := (<= #398 0::real)
-#409 := (* -1::real #54)
-#410 := (+ #47 #409)
-#408 := (>= #410 0::real)
-#60 := (uf_4 uf_9 #46)
-#402 := (* -1::real #60)
-#403 := (+ #59 #402)
-#404 := (<= #403 0::real)
-#418 := (and #399 #404 #408)
-#73 := (<= #59 #60)
-#72 := (<= #47 #59)
-#74 := (and #72 #73)
-#71 := (<= #54 #47)
-#75 := (and #71 #74)
-#421 := (iff #75 #418)
-#412 := (and #399 #404)
-#415 := (and #408 #412)
-#419 := (iff #415 #418)
-#420 := [rewrite]: #419
-#416 := (iff #75 #415)
-#413 := (iff #74 #412)
-#405 := (iff #73 #404)
-#406 := [rewrite]: #405
-#400 := (iff #72 #399)
-#401 := [rewrite]: #400
-#414 := [monotonicity #401 #406]: #413
-#407 := (iff #71 #408)
-#411 := [rewrite]: #407
-#417 := [monotonicity #411 #414]: #416
-#422 := [trans #417 #420]: #421
-#348 := [asserted]: #75
-#423 := [mp #348 #422]: #418
-#424 := [and-elim #423]: #399
-#637 := (+ #28 #397)
-#639 := (>= #637 0::real)
-#636 := (= #28 #59)
-#666 := (= #59 #28)
-#664 := (= #46 #25)
-#662 := (= #25 #46)
-#663 := [monotonicity #656]: #662
-#665 := [symm #663]: #664
-#667 := [monotonicity #665]: #666
-#668 := [symm #667]: #636
-#669 := (not #636)
-#670 := (or #669 #639)
-#671 := [th-lemma]: #670
-#672 := [unit-resolution #671 #668]: #639
-#468 := (+ #57 #465)
-#471 := (<= #468 0::real)
-#444 := (not #471)
-#322 := (ite #296 #279 #47)
-#330 := (* -1::real #322)
-#331 := (+ #57 #330)
-#332 := (<= #331 0::real)
-#333 := (not #332)
-#445 := (iff #333 #444)
-#472 := (iff #332 #471)
-#469 := (= #331 #468)
-#466 := (= #330 #465)
-#463 := (= #322 #279)
-#1 := true
-#458 := (ite true #279 #47)
-#461 := (= #458 #279)
-#462 := [rewrite]: #461
-#459 := (= #322 #458)
-#450 := (iff #296 true)
-#451 := [iff-true #395]: #450
-#460 := [monotonicity #451]: #459
-#464 := [trans #460 #462]: #463
-#467 := [monotonicity #464]: #466
-#470 := [monotonicity #467]: #469
-#473 := [monotonicity #470]: #472
-#474 := [monotonicity #473]: #445
-#303 := (ite #296 #60 #59)
-#313 := (* -1::real #303)
-#314 := (+ #57 #313)
-#312 := (>= #314 0::real)
-#311 := (not #312)
-#338 := (and #311 #333)
-#52 := (< #39 #22)
-#61 := (ite #52 #59 #60)
-#62 := (< #57 #61)
-#53 := (= uf_10 uf_3)
-#55 := (ite #53 #28 #54)
-#56 := (ite #52 #47 #55)
-#58 := (< #56 #57)
-#63 := (and #58 #62)
-#341 := (iff #63 #338)
-#282 := (ite #52 #47 #279)
-#285 := (< #282 #57)
-#291 := (and #62 #285)
-#339 := (iff #291 #338)
-#336 := (iff #285 #333)
-#327 := (< #322 #57)
-#334 := (iff #327 #333)
-#335 := [rewrite]: #334
-#328 := (iff #285 #327)
-#325 := (= #282 #322)
-#297 := (not #296)
-#319 := (ite #297 #47 #279)
-#323 := (= #319 #322)
-#324 := [rewrite]: #323
-#320 := (= #282 #319)
-#298 := (iff #52 #297)
-#299 := [rewrite]: #298
-#321 := [monotonicity #299]: #320
-#326 := [trans #321 #324]: #325
-#329 := [monotonicity #326]: #328
-#337 := [trans #329 #335]: #336
-#317 := (iff #62 #311)
-#308 := (< #57 #303)
-#315 := (iff #308 #311)
-#316 := [rewrite]: #315
-#309 := (iff #62 #308)
-#306 := (= #61 #303)
-#300 := (ite #297 #59 #60)
-#304 := (= #300 #303)
-#305 := [rewrite]: #304
-#301 := (= #61 #300)
-#302 := [monotonicity #299]: #301
-#307 := [trans #302 #305]: #306
-#310 := [monotonicity #307]: #309
-#318 := [trans #310 #316]: #317
-#340 := [monotonicity #318 #337]: #339
-#294 := (iff #63 #291)
-#288 := (and #285 #62)
-#292 := (iff #288 #291)
-#293 := [rewrite]: #292
-#289 := (iff #63 #288)
-#286 := (iff #58 #285)
-#283 := (= #56 #282)
-#280 := (= #55 #279)
-#226 := (iff #53 #45)
-#278 := [rewrite]: #226
-#281 := [monotonicity #278]: #280
-#284 := [monotonicity #281]: #283
-#287 := [monotonicity #284]: #286
-#290 := [monotonicity #287]: #289
-#295 := [trans #290 #293]: #294
-#342 := [trans #295 #340]: #341
-#179 := [asserted]: #63
-#343 := [mp #179 #342]: #338
-#345 := [and-elim #343]: #333
-#475 := [mp #345 #474]: #444
-#673 := [th-lemma #475 #672 #424 #391 #661]: false
-#674 := [lemma #673]: #571
-[unit-resolution #674 #690]: false
-unsat
-IL2powemHjRpCJYwmXFxyw 211 0
+f5cf3017773c1cf700f533cb220ba6c9eb22de56 211 0
#2 := false
#33 := 0::real
decl uf_11 :: (-> T5 T6 real)
@@ -1967,7 +1967,7 @@
#328 := [unit-resolution #319 #327]: #300
[th-lemma #326 #334 #195 #328 #187 #138]: false
unsat
-GX51o3DUO/UBS3eNP2P9kA 285 0
+ad41c2d9b185dd9b4fd0abefcdc55357d2105ed8 285 0
#2 := false
#7 := 0::real
decl uf_4 :: real
@@ -2253,7 +2253,7 @@
#286 := [lemma #284]: #285
[unit-resolution #286 #308 #305]: false
unsat
-cebG074uorSr8ODzgTmcKg 97 0
+076d8565ad4c4370b16a3b0c139e8c8e8fb58224 97 0
#2 := false
#18 := 0::real
decl uf_1 :: (-> T2 T1 real)
@@ -2351,7 +2351,7 @@
#173 := [mp #167 #172]: #165
[unit-resolution #173 #147 #76]: false
unsat
-DKRtrJ2XceCkITuNwNViRw 57 0
+8e6ea05b53a9ffb5a6dec689eb004bdb0c2a755b 57 0
#2 := false
#4 := 0::real
decl uf_1 :: (-> T2 real)
@@ -2409,7 +2409,7 @@
#269 := [quant-inst]: #268
[unit-resolution #269 #247 #274]: false
unsat
-97KJAJfUio+nGchEHWvgAw 91 0
+d278c38176edc1fb6492d54817f0a9092db653e6 91 0
#2 := false
#38 := 0::real
decl uf_1 :: (-> T1 T2 real)
@@ -2501,157 +2501,7 @@
#153 := [mp #147 #152]: #145
[unit-resolution #153 #129 #160]: false
unsat
-flJYbeWfe+t2l/zsRqdujA 149 0
-#2 := false
-#19 := 0::real
-decl uf_1 :: (-> T1 T2 real)
-decl uf_3 :: T2
-#5 := uf_3
-decl uf_4 :: T1
-#7 := uf_4
-#8 := (uf_1 uf_4 uf_3)
-#44 := -1::real
-#156 := (* -1::real #8)
-decl uf_2 :: T1
-#4 := uf_2
-#6 := (uf_1 uf_2 uf_3)
-#203 := (+ #6 #156)
-#205 := (>= #203 0::real)
-#9 := (= #6 #8)
-#40 := [asserted]: #9
-#208 := (not #9)
-#209 := (or #208 #205)
-#210 := [th-lemma]: #209
-#211 := [unit-resolution #210 #40]: #205
-decl uf_5 :: T1
-#12 := uf_5
-#22 := (uf_1 uf_5 uf_3)
-#160 := (* -1::real #22)
-#161 := (+ #6 #160)
-#207 := (>= #161 0::real)
-#222 := (not #207)
-#206 := (= #6 #22)
-#216 := (not #206)
-#62 := (= #8 #22)
-#70 := (not #62)
-#217 := (iff #70 #216)
-#214 := (iff #62 #206)
-#212 := (iff #206 #62)
-#213 := [monotonicity #40]: #212
-#215 := [symm #213]: #214
-#218 := [monotonicity #215]: #217
-#23 := (= #22 #8)
-#24 := (not #23)
-#71 := (iff #24 #70)
-#68 := (iff #23 #62)
-#69 := [rewrite]: #68
-#72 := [monotonicity #69]: #71
-#43 := [asserted]: #24
-#75 := [mp #43 #72]: #70
-#219 := [mp #75 #218]: #216
-#225 := (or #206 #222)
-#162 := (<= #161 0::real)
-#172 := (+ #8 #160)
-#173 := (>= #172 0::real)
-#178 := (not #173)
-#163 := (not #162)
-#181 := (or #163 #178)
-#184 := (not #181)
-#10 := (:var 0 T2)
-#15 := (uf_1 uf_4 #10)
-#149 := (pattern #15)
-#13 := (uf_1 uf_5 #10)
-#148 := (pattern #13)
-#11 := (uf_1 uf_2 #10)
-#147 := (pattern #11)
-#50 := (* -1::real #15)
-#51 := (+ #13 #50)
-#52 := (<= #51 0::real)
-#76 := (not #52)
-#45 := (* -1::real #13)
-#46 := (+ #11 #45)
-#47 := (<= #46 0::real)
-#78 := (not #47)
-#73 := (or #78 #76)
-#83 := (not #73)
-#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83)
-#86 := (forall (vars (?x1 T2)) #83)
-#153 := (iff #86 #150)
-#151 := (iff #83 #83)
-#152 := [refl]: #151
-#154 := [quant-intro #152]: #153
-#55 := (and #47 #52)
-#58 := (forall (vars (?x1 T2)) #55)
-#87 := (iff #58 #86)
-#84 := (iff #55 #83)
-#85 := [rewrite]: #84
-#88 := [quant-intro #85]: #87
-#79 := (~ #58 #58)
-#81 := (~ #55 #55)
-#82 := [refl]: #81
-#80 := [nnf-pos #82]: #79
-#16 := (<= #13 #15)
-#14 := (<= #11 #13)
-#17 := (and #14 #16)
-#18 := (forall (vars (?x1 T2)) #17)
-#59 := (iff #18 #58)
-#56 := (iff #17 #55)
-#53 := (iff #16 #52)
-#54 := [rewrite]: #53
-#48 := (iff #14 #47)
-#49 := [rewrite]: #48
-#57 := [monotonicity #49 #54]: #56
-#60 := [quant-intro #57]: #59
-#41 := [asserted]: #18
-#61 := [mp #41 #60]: #58
-#77 := [mp~ #61 #80]: #58
-#89 := [mp #77 #88]: #86
-#155 := [mp #89 #154]: #150
-#187 := (not #150)
-#188 := (or #187 #184)
-#157 := (+ #22 #156)
-#158 := (<= #157 0::real)
-#159 := (not #158)
-#164 := (or #163 #159)
-#165 := (not #164)
-#189 := (or #187 #165)
-#191 := (iff #189 #188)
-#193 := (iff #188 #188)
-#194 := [rewrite]: #193
-#185 := (iff #165 #184)
-#182 := (iff #164 #181)
-#179 := (iff #159 #178)
-#176 := (iff #158 #173)
-#166 := (+ #156 #22)
-#169 := (<= #166 0::real)
-#174 := (iff #169 #173)
-#175 := [rewrite]: #174
-#170 := (iff #158 #169)
-#167 := (= #157 #166)
-#168 := [rewrite]: #167
-#171 := [monotonicity #168]: #170
-#177 := [trans #171 #175]: #176
-#180 := [monotonicity #177]: #179
-#183 := [monotonicity #180]: #182
-#186 := [monotonicity #183]: #185
-#192 := [monotonicity #186]: #191
-#195 := [trans #192 #194]: #191
-#190 := [quant-inst]: #189
-#196 := [mp #190 #195]: #188
-#220 := [unit-resolution #196 #155]: #184
-#197 := (or #181 #162)
-#198 := [def-axiom]: #197
-#221 := [unit-resolution #198 #220]: #162
-#223 := (or #206 #163 #222)
-#224 := [th-lemma]: #223
-#226 := [unit-resolution #224 #221]: #225
-#227 := [unit-resolution #226 #219]: #222
-#199 := (or #181 #173)
-#200 := [def-axiom]: #199
-#228 := [unit-resolution #200 #220]: #173
-[th-lemma #228 #227 #211]: false
-unsat
-rbrrQuQfaijtLkQizgEXnQ 222 0
+38b5e95092f91070fab780891ebf7b83d5f95757 222 0
#2 := false
#4 := 0::real
decl uf_2 :: (-> T2 T1 real)
@@ -2874,7 +2724,7 @@
#308 := [th-lemma]: #307
[unit-resolution #308 #305 #290]: false
unsat
-hwh3oeLAWt56hnKIa8Wuow 248 0
+4968b0a0840255d92fbecd59ed4dac302603b2bd 248 0
#2 := false
#4 := 0::real
decl uf_2 :: (-> T2 T1 real)
@@ -3123,7 +2973,157 @@
#380 := [th-lemma]: #379
[unit-resolution #380 #377 #363]: false
unsat
-WdMJH3tkMv/rps8y9Ukq5Q 86 0
+a3b02dd75d8b2261f1b7ef7215268d84fd25e972 149 0
+#2 := false
+#19 := 0::real
+decl uf_1 :: (-> T1 T2 real)
+decl uf_3 :: T2
+#5 := uf_3
+decl uf_4 :: T1
+#7 := uf_4
+#8 := (uf_1 uf_4 uf_3)
+#44 := -1::real
+#156 := (* -1::real #8)
+decl uf_2 :: T1
+#4 := uf_2
+#6 := (uf_1 uf_2 uf_3)
+#203 := (+ #6 #156)
+#205 := (>= #203 0::real)
+#9 := (= #6 #8)
+#40 := [asserted]: #9
+#208 := (not #9)
+#209 := (or #208 #205)
+#210 := [th-lemma]: #209
+#211 := [unit-resolution #210 #40]: #205
+decl uf_5 :: T1
+#12 := uf_5
+#22 := (uf_1 uf_5 uf_3)
+#160 := (* -1::real #22)
+#161 := (+ #6 #160)
+#207 := (>= #161 0::real)
+#222 := (not #207)
+#206 := (= #6 #22)
+#216 := (not #206)
+#62 := (= #8 #22)
+#70 := (not #62)
+#217 := (iff #70 #216)
+#214 := (iff #62 #206)
+#212 := (iff #206 #62)
+#213 := [monotonicity #40]: #212
+#215 := [symm #213]: #214
+#218 := [monotonicity #215]: #217
+#23 := (= #22 #8)
+#24 := (not #23)
+#71 := (iff #24 #70)
+#68 := (iff #23 #62)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#43 := [asserted]: #24
+#75 := [mp #43 #72]: #70
+#219 := [mp #75 #218]: #216
+#225 := (or #206 #222)
+#162 := (<= #161 0::real)
+#172 := (+ #8 #160)
+#173 := (>= #172 0::real)
+#178 := (not #173)
+#163 := (not #162)
+#181 := (or #163 #178)
+#184 := (not #181)
+#10 := (:var 0 T2)
+#15 := (uf_1 uf_4 #10)
+#149 := (pattern #15)
+#13 := (uf_1 uf_5 #10)
+#148 := (pattern #13)
+#11 := (uf_1 uf_2 #10)
+#147 := (pattern #11)
+#50 := (* -1::real #15)
+#51 := (+ #13 #50)
+#52 := (<= #51 0::real)
+#76 := (not #52)
+#45 := (* -1::real #13)
+#46 := (+ #11 #45)
+#47 := (<= #46 0::real)
+#78 := (not #47)
+#73 := (or #78 #76)
+#83 := (not #73)
+#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83)
+#86 := (forall (vars (?x1 T2)) #83)
+#153 := (iff #86 #150)
+#151 := (iff #83 #83)
+#152 := [refl]: #151
+#154 := [quant-intro #152]: #153
+#55 := (and #47 #52)
+#58 := (forall (vars (?x1 T2)) #55)
+#87 := (iff #58 #86)
+#84 := (iff #55 #83)
+#85 := [rewrite]: #84
+#88 := [quant-intro #85]: #87
+#79 := (~ #58 #58)
+#81 := (~ #55 #55)
+#82 := [refl]: #81
+#80 := [nnf-pos #82]: #79
+#16 := (<= #13 #15)
+#14 := (<= #11 #13)
+#17 := (and #14 #16)
+#18 := (forall (vars (?x1 T2)) #17)
+#59 := (iff #18 #58)
+#56 := (iff #17 #55)
+#53 := (iff #16 #52)
+#54 := [rewrite]: #53
+#48 := (iff #14 #47)
+#49 := [rewrite]: #48
+#57 := [monotonicity #49 #54]: #56
+#60 := [quant-intro #57]: #59
+#41 := [asserted]: #18
+#61 := [mp #41 #60]: #58
+#77 := [mp~ #61 #80]: #58
+#89 := [mp #77 #88]: #86
+#155 := [mp #89 #154]: #150
+#187 := (not #150)
+#188 := (or #187 #184)
+#157 := (+ #22 #156)
+#158 := (<= #157 0::real)
+#159 := (not #158)
+#164 := (or #163 #159)
+#165 := (not #164)
+#189 := (or #187 #165)
+#191 := (iff #189 #188)
+#193 := (iff #188 #188)
+#194 := [rewrite]: #193
+#185 := (iff #165 #184)
+#182 := (iff #164 #181)
+#179 := (iff #159 #178)
+#176 := (iff #158 #173)
+#166 := (+ #156 #22)
+#169 := (<= #166 0::real)
+#174 := (iff #169 #173)
+#175 := [rewrite]: #174
+#170 := (iff #158 #169)
+#167 := (= #157 #166)
+#168 := [rewrite]: #167
+#171 := [monotonicity #168]: #170
+#177 := [trans #171 #175]: #176
+#180 := [monotonicity #177]: #179
+#183 := [monotonicity #180]: #182
+#186 := [monotonicity #183]: #185
+#192 := [monotonicity #186]: #191
+#195 := [trans #192 #194]: #191
+#190 := [quant-inst]: #189
+#196 := [mp #190 #195]: #188
+#220 := [unit-resolution #196 #155]: #184
+#197 := (or #181 #162)
+#198 := [def-axiom]: #197
+#221 := [unit-resolution #198 #220]: #162
+#223 := (or #206 #163 #222)
+#224 := [th-lemma]: #223
+#226 := [unit-resolution #224 #221]: #225
+#227 := [unit-resolution #226 #219]: #222
+#199 := (or #181 #173)
+#200 := [def-axiom]: #199
+#228 := [unit-resolution #200 #220]: #173
+[th-lemma #228 #227 #211]: false
+unsat
+06d4133eb0950a5f12d22480aa2707e31af2b064 86 0
#2 := false
#37 := 0::real
decl uf_2 :: (-> T2 T1 real)
@@ -3210,511 +3210,3 @@
#155 := [th-lemma]: #154
[unit-resolution #155 #60 #148 #144]: false
unsat
-V+IAyBZU/6QjYs6JkXx8LQ 57 0
-#2 := false
-#4 := 0::real
-decl uf_1 :: (-> T2 real)
-decl uf_2 :: (-> T1 T1 T2)
-decl uf_12 :: (-> T4 T1)
-decl uf_4 :: T4
-#11 := uf_4
-#39 := (uf_12 uf_4)
-decl uf_10 :: T4
-#27 := uf_10
-#38 := (uf_12 uf_10)
-#40 := (uf_2 #38 #39)
-#41 := (uf_1 #40)
-#264 := (>= #41 0::real)
-#266 := (not #264)
-#43 := (= #41 0::real)
-#44 := (not #43)
-#131 := [asserted]: #44
-#272 := (or #43 #266)
-#42 := (<= #41 0::real)
-#130 := [asserted]: #42
-#265 := (not #42)
-#270 := (or #43 #265 #266)
-#271 := [th-lemma]: #270
-#273 := [unit-resolution #271 #130]: #272
-#274 := [unit-resolution #273 #131]: #266
-#6 := (:var 0 T1)
-#5 := (:var 1 T1)
-#7 := (uf_2 #5 #6)
-#241 := (pattern #7)
-#8 := (uf_1 #7)
-#65 := (>= #8 0::real)
-#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65)
-#66 := (forall (vars (?x1 T1) (?x2 T1)) #65)
-#245 := (iff #66 #242)
-#243 := (iff #65 #65)
-#244 := [refl]: #243
-#246 := [quant-intro #244]: #245
-#149 := (~ #66 #66)
-#151 := (~ #65 #65)
-#152 := [refl]: #151
-#150 := [nnf-pos #152]: #149
-#9 := (<= 0::real #8)
-#10 := (forall (vars (?x1 T1) (?x2 T1)) #9)
-#67 := (iff #10 #66)
-#63 := (iff #9 #65)
-#64 := [rewrite]: #63
-#68 := [quant-intro #64]: #67
-#60 := [asserted]: #10
-#69 := [mp #60 #68]: #66
-#147 := [mp~ #69 #150]: #66
-#247 := [mp #147 #246]: #242
-#267 := (not #242)
-#268 := (or #267 #264)
-#269 := [quant-inst]: #268
-[unit-resolution #269 #247 #274]: false
-unsat
-vqiyJ/qjGXZ3iOg6xftiug 15 0
-uf_1 -> val!0
-uf_2 -> val!1
-uf_3 -> val!2
-uf_5 -> val!15
-uf_6 -> val!26
-uf_4 -> {
- val!0 -> val!12
- val!1 -> val!13
- else -> val!13
-}
-uf_7 -> {
- val!6 -> val!31
- else -> val!31
-}
-sat
-mrZPJZyTokErrN6SYupisw 9 0
-uf_4 -> val!1
-uf_2 -> val!3
-uf_3 -> val!4
-uf_1 -> {
- val!5 -> val!6
- val!4 -> val!7
- else -> val!7
-}
-sat
-qkVrmXMcHAG5MLuJ9d8jXQ 211 0
-#2 := false
-#33 := 0::real
-decl uf_11 :: (-> T5 T6 real)
-decl uf_15 :: T6
-#28 := uf_15
-decl uf_16 :: T5
-#30 := uf_16
-#31 := (uf_11 uf_16 uf_15)
-decl uf_12 :: (-> T7 T8 T5)
-decl uf_14 :: T8
-#26 := uf_14
-decl uf_13 :: (-> T1 T7)
-decl uf_8 :: T1
-#16 := uf_8
-#25 := (uf_13 uf_8)
-#27 := (uf_12 #25 uf_14)
-#29 := (uf_11 #27 uf_15)
-#73 := -1::real
-#84 := (* -1::real #29)
-#85 := (+ #84 #31)
-#74 := (* -1::real #31)
-#75 := (+ #29 #74)
-#112 := (>= #75 0::real)
-#119 := (ite #112 #75 #85)
-#127 := (* -1::real #119)
-decl uf_17 :: T5
-#37 := uf_17
-#38 := (uf_11 uf_17 uf_15)
-#102 := -1/3::real
-#103 := (* -1/3::real #38)
-#128 := (+ #103 #127)
-#100 := 1/3::real
-#101 := (* 1/3::real #31)
-#129 := (+ #101 #128)
-#130 := (<= #129 0::real)
-#131 := (not #130)
-#40 := 3::real
-#39 := (- #31 #38)
-#41 := (/ #39 3::real)
-#32 := (- #29 #31)
-#35 := (- #32)
-#34 := (< #32 0::real)
-#36 := (ite #34 #35 #32)
-#42 := (< #36 #41)
-#136 := (iff #42 #131)
-#104 := (+ #101 #103)
-#78 := (< #75 0::real)
-#90 := (ite #78 #85 #75)
-#109 := (< #90 #104)
-#134 := (iff #109 #131)
-#124 := (< #119 #104)
-#132 := (iff #124 #131)
-#133 := [rewrite]: #132
-#125 := (iff #109 #124)
-#122 := (= #90 #119)
-#113 := (not #112)
-#116 := (ite #113 #85 #75)
-#120 := (= #116 #119)
-#121 := [rewrite]: #120
-#117 := (= #90 #116)
-#114 := (iff #78 #113)
-#115 := [rewrite]: #114
-#118 := [monotonicity #115]: #117
-#123 := [trans #118 #121]: #122
-#126 := [monotonicity #123]: #125
-#135 := [trans #126 #133]: #134
-#110 := (iff #42 #109)
-#107 := (= #41 #104)
-#93 := (* -1::real #38)
-#94 := (+ #31 #93)
-#97 := (/ #94 3::real)
-#105 := (= #97 #104)
-#106 := [rewrite]: #105
-#98 := (= #41 #97)
-#95 := (= #39 #94)
-#96 := [rewrite]: #95
-#99 := [monotonicity #96]: #98
-#108 := [trans #99 #106]: #107
-#91 := (= #36 #90)
-#76 := (= #32 #75)
-#77 := [rewrite]: #76
-#88 := (= #35 #85)
-#81 := (- #75)
-#86 := (= #81 #85)
-#87 := [rewrite]: #86
-#82 := (= #35 #81)
-#83 := [monotonicity #77]: #82
-#89 := [trans #83 #87]: #88
-#79 := (iff #34 #78)
-#80 := [monotonicity #77]: #79
-#92 := [monotonicity #80 #89 #77]: #91
-#111 := [monotonicity #92 #108]: #110
-#137 := [trans #111 #135]: #136
-#72 := [asserted]: #42
-#138 := [mp #72 #137]: #131
-decl uf_1 :: T1
-#4 := uf_1
-#43 := (uf_13 uf_1)
-#44 := (uf_12 #43 uf_14)
-#45 := (uf_11 #44 uf_15)
-#149 := (* -1::real #45)
-#150 := (+ #38 #149)
-#140 := (+ #93 #45)
-#161 := (<= #150 0::real)
-#168 := (ite #161 #140 #150)
-#176 := (* -1::real #168)
-#177 := (+ #103 #176)
-#178 := (+ #101 #177)
-#179 := (<= #178 0::real)
-#180 := (not #179)
-#46 := (- #45 #38)
-#48 := (- #46)
-#47 := (< #46 0::real)
-#49 := (ite #47 #48 #46)
-#50 := (< #49 #41)
-#185 := (iff #50 #180)
-#143 := (< #140 0::real)
-#155 := (ite #143 #150 #140)
-#158 := (< #155 #104)
-#183 := (iff #158 #180)
-#173 := (< #168 #104)
-#181 := (iff #173 #180)
-#182 := [rewrite]: #181
-#174 := (iff #158 #173)
-#171 := (= #155 #168)
-#162 := (not #161)
-#165 := (ite #162 #150 #140)
-#169 := (= #165 #168)
-#170 := [rewrite]: #169
-#166 := (= #155 #165)
-#163 := (iff #143 #162)
-#164 := [rewrite]: #163
-#167 := [monotonicity #164]: #166
-#172 := [trans #167 #170]: #171
-#175 := [monotonicity #172]: #174
-#184 := [trans #175 #182]: #183
-#159 := (iff #50 #158)
-#156 := (= #49 #155)
-#141 := (= #46 #140)
-#142 := [rewrite]: #141
-#153 := (= #48 #150)
-#146 := (- #140)
-#151 := (= #146 #150)
-#152 := [rewrite]: #151
-#147 := (= #48 #146)
-#148 := [monotonicity #142]: #147
-#154 := [trans #148 #152]: #153
-#144 := (iff #47 #143)
-#145 := [monotonicity #142]: #144
-#157 := [monotonicity #145 #154 #142]: #156
-#160 := [monotonicity #157 #108]: #159
-#186 := [trans #160 #184]: #185
-#139 := [asserted]: #50
-#187 := [mp #139 #186]: #180
-#299 := (+ #140 #176)
-#300 := (<= #299 0::real)
-#290 := (= #140 #168)
-#329 := [hypothesis]: #162
-#191 := (+ #29 #149)
-#192 := (<= #191 0::real)
-#51 := (<= #29 #45)
-#193 := (iff #51 #192)
-#194 := [rewrite]: #193
-#188 := [asserted]: #51
-#195 := [mp #188 #194]: #192
-#298 := (+ #75 #127)
-#301 := (<= #298 0::real)
-#284 := (= #75 #119)
-#302 := [hypothesis]: #113
-#296 := (+ #85 #127)
-#297 := (<= #296 0::real)
-#285 := (= #85 #119)
-#288 := (or #112 #285)
-#289 := [def-axiom]: #288
-#303 := [unit-resolution #289 #302]: #285
-#304 := (not #285)
-#305 := (or #304 #297)
-#306 := [th-lemma]: #305
-#307 := [unit-resolution #306 #303]: #297
-#315 := (not #290)
-#310 := (not #300)
-#311 := (or #310 #112)
-#308 := [hypothesis]: #300
-#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
-#312 := [lemma #309]: #311
-#322 := [unit-resolution #312 #302]: #310
-#316 := (or #315 #300)
-#313 := [hypothesis]: #310
-#314 := [hypothesis]: #290
-#317 := [th-lemma]: #316
-#318 := [unit-resolution #317 #314 #313]: false
-#319 := [lemma #318]: #316
-#323 := [unit-resolution #319 #322]: #315
-#292 := (or #162 #290)
-#293 := [def-axiom]: #292
-#324 := [unit-resolution #293 #323]: #162
-#325 := [th-lemma #324 #307 #138 #302 #195]: false
-#326 := [lemma #325]: #112
-#286 := (or #113 #284)
-#287 := [def-axiom]: #286
-#330 := [unit-resolution #287 #326]: #284
-#331 := (not #284)
-#332 := (or #331 #301)
-#333 := [th-lemma]: #332
-#334 := [unit-resolution #333 #330]: #301
-#335 := [th-lemma #326 #334 #195 #329 #138]: false
-#336 := [lemma #335]: #161
-#327 := [unit-resolution #293 #336]: #290
-#328 := [unit-resolution #319 #327]: #300
-[th-lemma #326 #334 #195 #328 #187 #138]: false
-unsat
-WrIjxhfF5EcRCmS6xKG3XQ 211 0
-#2 := false
-#33 := 0::real
-decl uf_11 :: (-> T5 T6 real)
-decl uf_15 :: T6
-#28 := uf_15
-decl uf_16 :: T5
-#30 := uf_16
-#31 := (uf_11 uf_16 uf_15)
-decl uf_12 :: (-> T7 T8 T5)
-decl uf_14 :: T8
-#26 := uf_14
-decl uf_13 :: (-> T1 T7)
-decl uf_8 :: T1
-#16 := uf_8
-#25 := (uf_13 uf_8)
-#27 := (uf_12 #25 uf_14)
-#29 := (uf_11 #27 uf_15)
-#73 := -1::real
-#84 := (* -1::real #29)
-#85 := (+ #84 #31)
-#74 := (* -1::real #31)
-#75 := (+ #29 #74)
-#112 := (>= #75 0::real)
-#119 := (ite #112 #75 #85)
-#127 := (* -1::real #119)
-decl uf_17 :: T5
-#37 := uf_17
-#38 := (uf_11 uf_17 uf_15)
-#102 := -1/3::real
-#103 := (* -1/3::real #38)
-#128 := (+ #103 #127)
-#100 := 1/3::real
-#101 := (* 1/3::real #31)
-#129 := (+ #101 #128)
-#130 := (<= #129 0::real)
-#131 := (not #130)
-#40 := 3::real
-#39 := (- #31 #38)
-#41 := (/ #39 3::real)
-#32 := (- #29 #31)
-#35 := (- #32)
-#34 := (< #32 0::real)
-#36 := (ite #34 #35 #32)
-#42 := (< #36 #41)
-#136 := (iff #42 #131)
-#104 := (+ #101 #103)
-#78 := (< #75 0::real)
-#90 := (ite #78 #85 #75)
-#109 := (< #90 #104)
-#134 := (iff #109 #131)
-#124 := (< #119 #104)
-#132 := (iff #124 #131)
-#133 := [rewrite]: #132
-#125 := (iff #109 #124)
-#122 := (= #90 #119)
-#113 := (not #112)
-#116 := (ite #113 #85 #75)
-#120 := (= #116 #119)
-#121 := [rewrite]: #120
-#117 := (= #90 #116)
-#114 := (iff #78 #113)
-#115 := [rewrite]: #114
-#118 := [monotonicity #115]: #117
-#123 := [trans #118 #121]: #122
-#126 := [monotonicity #123]: #125
-#135 := [trans #126 #133]: #134
-#110 := (iff #42 #109)
-#107 := (= #41 #104)
-#93 := (* -1::real #38)
-#94 := (+ #31 #93)
-#97 := (/ #94 3::real)
-#105 := (= #97 #104)
-#106 := [rewrite]: #105
-#98 := (= #41 #97)
-#95 := (= #39 #94)
-#96 := [rewrite]: #95
-#99 := [monotonicity #96]: #98
-#108 := [trans #99 #106]: #107
-#91 := (= #36 #90)
-#76 := (= #32 #75)
-#77 := [rewrite]: #76
-#88 := (= #35 #85)
-#81 := (- #75)
-#86 := (= #81 #85)
-#87 := [rewrite]: #86
-#82 := (= #35 #81)
-#83 := [monotonicity #77]: #82
-#89 := [trans #83 #87]: #88
-#79 := (iff #34 #78)
-#80 := [monotonicity #77]: #79
-#92 := [monotonicity #80 #89 #77]: #91
-#111 := [monotonicity #92 #108]: #110
-#137 := [trans #111 #135]: #136
-#72 := [asserted]: #42
-#138 := [mp #72 #137]: #131
-decl uf_1 :: T1
-#4 := uf_1
-#43 := (uf_13 uf_1)
-#44 := (uf_12 #43 uf_14)
-#45 := (uf_11 #44 uf_15)
-#149 := (* -1::real #45)
-#150 := (+ #38 #149)
-#140 := (+ #93 #45)
-#161 := (<= #150 0::real)
-#168 := (ite #161 #140 #150)
-#176 := (* -1::real #168)
-#177 := (+ #103 #176)
-#178 := (+ #101 #177)
-#179 := (<= #178 0::real)
-#180 := (not #179)
-#46 := (- #45 #38)
-#48 := (- #46)
-#47 := (< #46 0::real)
-#49 := (ite #47 #48 #46)
-#50 := (< #49 #41)
-#185 := (iff #50 #180)
-#143 := (< #140 0::real)
-#155 := (ite #143 #150 #140)
-#158 := (< #155 #104)
-#183 := (iff #158 #180)
-#173 := (< #168 #104)
-#181 := (iff #173 #180)
-#182 := [rewrite]: #181
-#174 := (iff #158 #173)
-#171 := (= #155 #168)
-#162 := (not #161)
-#165 := (ite #162 #150 #140)
-#169 := (= #165 #168)
-#170 := [rewrite]: #169
-#166 := (= #155 #165)
-#163 := (iff #143 #162)
-#164 := [rewrite]: #163
-#167 := [monotonicity #164]: #166
-#172 := [trans #167 #170]: #171
-#175 := [monotonicity #172]: #174
-#184 := [trans #175 #182]: #183
-#159 := (iff #50 #158)
-#156 := (= #49 #155)
-#141 := (= #46 #140)
-#142 := [rewrite]: #141
-#153 := (= #48 #150)
-#146 := (- #140)
-#151 := (= #146 #150)
-#152 := [rewrite]: #151
-#147 := (= #48 #146)
-#148 := [monotonicity #142]: #147
-#154 := [trans #148 #152]: #153
-#144 := (iff #47 #143)
-#145 := [monotonicity #142]: #144
-#157 := [monotonicity #145 #154 #142]: #156
-#160 := [monotonicity #157 #108]: #159
-#186 := [trans #160 #184]: #185
-#139 := [asserted]: #50
-#187 := [mp #139 #186]: #180
-#299 := (+ #140 #176)
-#300 := (<= #299 0::real)
-#290 := (= #140 #168)
-#329 := [hypothesis]: #162
-#191 := (+ #29 #149)
-#192 := (<= #191 0::real)
-#51 := (<= #29 #45)
-#193 := (iff #51 #192)
-#194 := [rewrite]: #193
-#188 := [asserted]: #51
-#195 := [mp #188 #194]: #192
-#298 := (+ #75 #127)
-#301 := (<= #298 0::real)
-#284 := (= #75 #119)
-#302 := [hypothesis]: #113
-#296 := (+ #85 #127)
-#297 := (<= #296 0::real)
-#285 := (= #85 #119)
-#288 := (or #112 #285)
-#289 := [def-axiom]: #288
-#303 := [unit-resolution #289 #302]: #285
-#304 := (not #285)
-#305 := (or #304 #297)
-#306 := [th-lemma]: #305
-#307 := [unit-resolution #306 #303]: #297
-#315 := (not #290)
-#310 := (not #300)
-#311 := (or #310 #112)
-#308 := [hypothesis]: #300
-#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
-#312 := [lemma #309]: #311
-#322 := [unit-resolution #312 #302]: #310
-#316 := (or #315 #300)
-#313 := [hypothesis]: #310
-#314 := [hypothesis]: #290
-#317 := [th-lemma]: #316
-#318 := [unit-resolution #317 #314 #313]: false
-#319 := [lemma #318]: #316
-#323 := [unit-resolution #319 #322]: #315
-#292 := (or #162 #290)
-#293 := [def-axiom]: #292
-#324 := [unit-resolution #293 #323]: #162
-#325 := [th-lemma #324 #307 #138 #302 #195]: false
-#326 := [lemma #325]: #112
-#286 := (or #113 #284)
-#287 := [def-axiom]: #286
-#330 := [unit-resolution #287 #326]: #284
-#331 := (not #284)
-#332 := (or #331 #301)
-#333 := [th-lemma]: #332
-#334 := [unit-resolution #333 #330]: #301
-#335 := [th-lemma #326 #334 #195 #329 #138]: false
-#336 := [lemma #335]: #161
-#327 := [unit-resolution #293 #336]: #290
-#328 := [unit-resolution #319 #327]: #300
-[th-lemma #326 #334 #195 #328 #187 #138]: false
-unsat
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 24 17:41:25 2010 +0100
@@ -8,7 +8,7 @@
begin
declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=true]]
+declare [[smt_record=false]]
declare [[z3_proofs=true]]
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
--- a/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 17:41:25 2010 +0100
@@ -1,4 +1,4 @@
-Fg1W6egjwo9zhhAmUXOW+w 8 0
+bb06851c317eb8b672e27364b0ae34a4e39eb880 8 0
#2 := false
#1 := true
#4 := (not true)
@@ -7,7 +7,7 @@
#20 := [asserted]: #4
[mp #20 #22]: false
unsat
-2+cndY9nzS72l7VvBCGRAw 19 0
+70d1f77bec207467bc0306af0d98a71fa8328274 19 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -27,7 +27,7 @@
#23 := [asserted]: #7
[mp #23 #32]: false
unsat
-0vJQrobUDcQ9PkGJO8aM8g 25 0
+148012a9e9d44fe30a0c79e3344bdb805124f661 25 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -53,7 +53,7 @@
#23 := [asserted]: #7
[mp #23 #38]: false
unsat
-AGGnpwEv208Vqxly7wTWHA 38 0
+bc9a25b7f6dc3ac2431ee71b6e71c5a7b25e89d1 38 0
#2 := false
decl up_2 :: bool
#5 := up_2
@@ -92,9 +92,9 @@
#30 := [and-elim #31]: #6
[mp #30 #52]: false
unsat
-wakXeIy1uoPgglzOQGFhJQ 1 0
-unsat
-cpSlDe0l7plVktRNxGU5dA 71 0
+9b3db6ce34c8a1806160f1349b898b6c5ca40ba0 1 0
+unsat
+912e9b7fb52f4a71d232354b3bb53c11e5a41ccd 71 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -166,7 +166,7 @@
#31 := [asserted]: #15
[mp #31 #82]: false
unsat
-pg19mjJfV75T2QDrgWd4JA 57 0
+4d063d3cdf6657ddb4258379f900ef18e9042978 57 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -224,7 +224,7 @@
#30 := [asserted]: #14
[mp #30 #70]: false
unsat
-Mj1B8X1MaN7xU/W4Kz3FoQ 194 0
+c6eb111aa830c9669a030c2e58b4e827706981da 194 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -419,7 +419,7 @@
#237 := [mp #83 #236]: #75
[mp #237 #247]: false
unsat
-JkhYJB8FDavTZkizO1/9IA 52 0
+42890f9fa7c18237798ca55d0cf9dfff6f2f868a 52 0
#2 := false
decl uf_1 :: (-> T1 T1 T1)
decl uf_2 :: T1
@@ -472,7 +472,7 @@
#113 := [quant-inst]: #199
[unit-resolution #113 #536 #49]: false
unsat
-0ZdSZH2DbtjHNTyrDkZmXg 1667 0
+94169ba151f7a720e818287ce490015dde764bad 1667 0
#2 := false
decl up_54 :: bool
#126 := up_54
@@ -2140,7 +2140,7 @@
#2371 := [unit-resolution #891 #2369]: #166
[unit-resolution #2159 #2371 #2370 #2358 #2357]: false
unsat
-R3pmBDBlU9XdUrxJXhj7nA 78 0
+d8841d120b7cf772be783d793f759fb6353b9fcd 78 0
#2 := false
decl up_1 :: (-> int bool)
decl ?x1!0 :: int
@@ -2219,7 +2219,7 @@
#82 := [and-elim #81]: #55
[unit-resolution #82 #95]: false
unsat
-IBRj/loev6P6r0J+HOit6A 135 0
+18bde40beb0dd1fc2613a67805e24d767dd9a3bf 135 0
#2 := false
decl up_1 :: (-> T1 T2 bool)
#5 := (:var 0 T2)
@@ -2355,7 +2355,7 @@
#176 := [quant-inst]: #538
[unit-resolution #176 #252 #535]: false
unsat
-72504KVBixGB/87pOYiU/A 135 2
+013861f683c286a3ef38681266913846a3a39b9a 135 2
#2 := false
decl up_1 :: (-> T1 T2 bool)
#5 := (:var 0 T2)
@@ -2493,7 +2493,7 @@
unsat
WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
-RaQLz4GxtUICnOD5WoYnzQ 56 0
+0e958e27514643bb596851e6dbb61a23f6b348b0 56 0
#2 := false
decl up_1 :: (-> T1 bool)
decl uf_2 :: T1
@@ -2550,7 +2550,7 @@
#120 := [quant-inst]: #206
[unit-resolution #120 #542 #41]: false
unsat
-NPQIgVPhSpgSLeS+u/EatQ 17 0
+6ecefa4023d224e6c51226d5bee17e2a19cc4333 17 0
#2 := false
#4 := 3::int
#5 := (= 3::int 3::int)
@@ -2568,7 +2568,7 @@
#22 := [asserted]: #6
[mp #22 #31]: false
unsat
-Lc9NwVtwY2Wo0G7UbFD1oA 17 0
+5e0256133fc82f0e2fea6597b863483e4e61d3c6 17 0
#2 := false
#4 := 3::real
#5 := (= 3::real 3::real)
@@ -2586,7 +2586,7 @@
#22 := [asserted]: #6
[mp #22 #31]: false
unsat
-pYVrUflpYrrZEWALJDnvPw 26 0
+55cf32b061b843ac5bcaefb74005a7dd3a24386f 26 0
#2 := false
#7 := 4::int
#5 := 1::int
@@ -2613,7 +2613,7 @@
#25 := [asserted]: #9
[mp #25 #40]: false
unsat
-FIqzVlbN8RT0iWarmBEpjw 41 0
+e81d17ec85af9db5ec6ba5bf4ced62daaa719ef3 41 0
#2 := false
decl uf_1 :: int
#4 := uf_1
@@ -2655,7 +2655,7 @@
#28 := [asserted]: #12
[mp #28 #52]: false
unsat
-HWVNtxMa8xktQsg8pHG+1w 35 0
+448f188ebf9d7fbd2920c0a51a8f105192e6af1a 35 0
#2 := false
#5 := 3::int
#6 := 8::int
@@ -2691,7 +2691,7 @@
#26 := [asserted]: #10
[mp #26 #51]: false
unsat
-M71YYpEc8u/aEIH3MOQrcg 250 0
+c3751ecae7701923f4ba6a90c6c6eee35ee1b13d 250 0
#2 := false
#7 := 0::real
decl uf_2 :: real
@@ -2942,7 +2942,7 @@
#294 := [unit-resolution #190 #293]: #188
[th-lemma #280 #294]: false
unsat
-G00bTqBjtW66EmwIZbXbOg 124 0
+8e6af261ea9f94b967813d4e2f2abcb94463d612 124 0
#2 := false
decl uf_1 :: (-> T1 T2)
decl uf_3 :: T1
@@ -3067,7 +3067,7 @@
#34 := [asserted]: #11
[unit-resolution #34 #536]: false
unsat
-6QdzkSy/RtEjUu+wUKIKqA 54 0
+243524c591f6dcfe16a79ddd249c64a337ff3612 54 0
#2 := false
#9 := 1::int
decl uf_1 :: int
@@ -3122,7 +3122,7 @@
#28 := [asserted]: #12
[mp #28 #67]: false
unsat
-xoSwaSeELbR0PHe0zb/BSg 63 0
+adfe7d6c2da6653191952bd9673c1274f94c2ab2 63 0
#2 := false
#11 := 0::int
decl uf_2 :: int
@@ -3186,7 +3186,7 @@
#76 := [mp #52 #75]: #63
[mp #76 #84]: false
unsat
-ciHqmDSmPpA15rO932dhvA 35 0
+3440e29713ba625633b10a2c4fdc186cb6e0cf3e 35 0
#2 := false
#6 := 5::int
#4 := 2::int
@@ -3222,7 +3222,7 @@
#25 := [asserted]: #9
[mp #25 #49]: false
unsat
-HzwFy7SRHqpspkYnzyeF4w 45 0
+5f3503ae4a43341932052006638f286bea551e87 45 0
#2 := false
#11 := 4::real
decl uf_2 :: real
@@ -3268,7 +3268,7 @@
#60 := [mp #36 #59]: #51
[th-lemma #60 #47 #38]: false
unsat
-XW7QIWmzYjfQXaHHPc98eA 59 0
+347776ce17d7d3f6d1252ead05795e4eee6f4b20 59 0
#2 := false
#16 := (not false)
decl uf_2 :: int
@@ -3328,94 +3328,7 @@
#34 := [asserted]: #18
[mp #34 #71]: false
unsat
-ZGL00TLLioiLlWFiXUnbxg 86 0
-#2 := false
-decl uf_1 :: int
-#5 := uf_1
-#7 := 2::int
-#29 := (* 2::int uf_1)
-#4 := 0::int
-#54 := (= 0::int #29)
-#55 := (not #54)
-#61 := (= #29 0::int)
-#104 := (not #61)
-#110 := (iff #104 #55)
-#108 := (iff #61 #54)
-#109 := [commutativity]: #108
-#111 := [monotonicity #109]: #110
-#62 := (<= #29 0::int)
-#100 := (not #62)
-#30 := (<= uf_1 0::int)
-#31 := (not #30)
-#6 := (< 0::int uf_1)
-#32 := (iff #6 #31)
-#33 := [rewrite]: #32
-#27 := [asserted]: #6
-#34 := [mp #27 #33]: #31
-#101 := (or #100 #30)
-#102 := [th-lemma]: #101
-#103 := [unit-resolution #102 #34]: #100
-#105 := (or #104 #62)
-#106 := [th-lemma]: #105
-#107 := [unit-resolution #106 #103]: #104
-#112 := [mp #107 #111]: #55
-#56 := (= uf_1 #29)
-#57 := (not #56)
-#53 := (= 0::int uf_1)
-#50 := (not #53)
-#58 := (and #50 #55 #57)
-#69 := (not #58)
-#42 := (distinct 0::int uf_1 #29)
-#47 := (not #42)
-#9 := (- uf_1 uf_1)
-#8 := (* uf_1 2::int)
-#10 := (distinct uf_1 #8 #9)
-#11 := (not #10)
-#48 := (iff #11 #47)
-#45 := (iff #10 #42)
-#39 := (distinct uf_1 #29 0::int)
-#43 := (iff #39 #42)
-#44 := [rewrite]: #43
-#40 := (iff #10 #39)
-#37 := (= #9 0::int)
-#38 := [rewrite]: #37
-#35 := (= #8 #29)
-#36 := [rewrite]: #35
-#41 := [monotonicity #36 #38]: #40
-#46 := [trans #41 #44]: #45
-#49 := [monotonicity #46]: #48
-#28 := [asserted]: #11
-#52 := [mp #28 #49]: #47
-#80 := (or #42 #69)
-#81 := [def-axiom]: #80
-#82 := [unit-resolution #81 #52]: #69
-#59 := (= uf_1 0::int)
-#83 := (not #59)
-#89 := (iff #83 #50)
-#87 := (iff #59 #53)
-#88 := [commutativity]: #87
-#90 := [monotonicity #88]: #89
-#84 := (or #83 #30)
-#85 := [th-lemma]: #84
-#86 := [unit-resolution #85 #34]: #83
-#91 := [mp #86 #90]: #50
-#64 := -1::int
-#65 := (* -1::int #29)
-#66 := (+ uf_1 #65)
-#68 := (>= #66 0::int)
-#92 := (not #68)
-#93 := (or #92 #30)
-#94 := [th-lemma]: #93
-#95 := [unit-resolution #94 #34]: #92
-#96 := (or #57 #68)
-#97 := [th-lemma]: #96
-#98 := [unit-resolution #97 #95]: #57
-#76 := (or #58 #53 #54 #56)
-#77 := [def-axiom]: #76
-#99 := [unit-resolution #77 #98 #91 #82]: #54
-[unit-resolution #99 #112]: false
-unsat
-DWt5rIK6NWlI4vrw+691Zg 212 0
+f7b1b99e3470f713e48aaae1336ace10223be6f0 212 0
#2 := false
decl uf_4 :: T1
#13 := uf_4
@@ -3628,7 +3541,94 @@
#519 := [unit-resolution #521 #518]: #547
[unit-resolution #519 #522]: false
unsat
-PaSeDRf7Set5ywlblDOoTg 673 0
+bf36938883aa38907d4d00c1860a1d18e7b620d0 86 0
+#2 := false
+decl uf_1 :: int
+#5 := uf_1
+#7 := 2::int
+#29 := (* 2::int uf_1)
+#4 := 0::int
+#54 := (= 0::int #29)
+#55 := (not #54)
+#61 := (= #29 0::int)
+#104 := (not #61)
+#110 := (iff #104 #55)
+#108 := (iff #61 #54)
+#109 := [commutativity]: #108
+#111 := [monotonicity #109]: #110
+#62 := (<= #29 0::int)
+#100 := (not #62)
+#30 := (<= uf_1 0::int)
+#31 := (not #30)
+#6 := (< 0::int uf_1)
+#32 := (iff #6 #31)
+#33 := [rewrite]: #32
+#27 := [asserted]: #6
+#34 := [mp #27 #33]: #31
+#101 := (or #100 #30)
+#102 := [th-lemma]: #101
+#103 := [unit-resolution #102 #34]: #100
+#105 := (or #104 #62)
+#106 := [th-lemma]: #105
+#107 := [unit-resolution #106 #103]: #104
+#112 := [mp #107 #111]: #55
+#56 := (= uf_1 #29)
+#57 := (not #56)
+#53 := (= 0::int uf_1)
+#50 := (not #53)
+#58 := (and #50 #55 #57)
+#69 := (not #58)
+#42 := (distinct 0::int uf_1 #29)
+#47 := (not #42)
+#9 := (- uf_1 uf_1)
+#8 := (* uf_1 2::int)
+#10 := (distinct uf_1 #8 #9)
+#11 := (not #10)
+#48 := (iff #11 #47)
+#45 := (iff #10 #42)
+#39 := (distinct uf_1 #29 0::int)
+#43 := (iff #39 #42)
+#44 := [rewrite]: #43
+#40 := (iff #10 #39)
+#37 := (= #9 0::int)
+#38 := [rewrite]: #37
+#35 := (= #8 #29)
+#36 := [rewrite]: #35
+#41 := [monotonicity #36 #38]: #40
+#46 := [trans #41 #44]: #45
+#49 := [monotonicity #46]: #48
+#28 := [asserted]: #11
+#52 := [mp #28 #49]: #47
+#80 := (or #42 #69)
+#81 := [def-axiom]: #80
+#82 := [unit-resolution #81 #52]: #69
+#59 := (= uf_1 0::int)
+#83 := (not #59)
+#89 := (iff #83 #50)
+#87 := (iff #59 #53)
+#88 := [commutativity]: #87
+#90 := [monotonicity #88]: #89
+#84 := (or #83 #30)
+#85 := [th-lemma]: #84
+#86 := [unit-resolution #85 #34]: #83
+#91 := [mp #86 #90]: #50
+#64 := -1::int
+#65 := (* -1::int #29)
+#66 := (+ uf_1 #65)
+#68 := (>= #66 0::int)
+#92 := (not #68)
+#93 := (or #92 #30)
+#94 := [th-lemma]: #93
+#95 := [unit-resolution #94 #34]: #92
+#96 := (or #57 #68)
+#97 := [th-lemma]: #96
+#98 := [unit-resolution #97 #95]: #57
+#76 := (or #58 #53 #54 #56)
+#77 := [def-axiom]: #76
+#99 := [unit-resolution #77 #98 #91 #82]: #54
+[unit-resolution #99 #112]: false
+unsat
+9791139ea2cfda88ae799477fc61e411aab42b18 673 0
#2 := false
#169 := 0::int
decl uf_2 :: int
@@ -4302,7 +4302,7 @@
#410 := [mp #349 #409]: #405
[unit-resolution #410 #710 #709 #697 #706]: false
unsat
-U7jSPEM53XYq3qs03aUczw 2291 0
+0d07e457c5602ba4a5dc70af32b6dc53a80a858c 2291 0
#2 := false
#6 := 0::int
decl z3name!0 :: int
@@ -6594,7 +6594,7 @@
#2323 := [unit-resolution #918 #2322]: #100
[unit-resolution #917 #2323 #2318]: false
unsat
-eqE7IAqFr0UIBuUsVDgHvw 52 0
+258b6cd4609a61b7800235c7f356739cfb8996c5 52 0
#2 := false
#8 := 1::real
decl uf_1 :: real
@@ -6647,7 +6647,7 @@
#29 := [asserted]: #13
[mp #29 #65]: false
unsat
-ADs4ZPiuUr7Xu7tk71NnEw 59 0
+3d1d0473f97c11d6c4d10f6e0313b2e2f4aac879 59 0
#2 := false
#55 := 0::int
#7 := 2::int
@@ -6707,7 +6707,7 @@
#144 := [unit-resolution #143 #28]: #58
[unit-resolution #144 #68]: false
unsat
-x2NmsblNl28xPXP2EG22rA 54 0
+f768cbe713eb8031e45b1a78d0f49a07f5398eb8 54 0
#2 := false
#5 := 2::int
decl uf_1 :: int
@@ -6762,7 +6762,7 @@
#139 := [unit-resolution #138 #27]: #127
[unit-resolution #139 #62]: false
unsat
-kfLiOGBz3RZx9wt+FS+hfg 118 0
+2c2bcacfbe018175dd39ce04dd5cbe02c800a0dd 118 0
#2 := false
#5 := 0::real
decl uf_1 :: real
@@ -6881,7 +6881,7 @@
#126 := [mp #101 #125]: #115
[unit-resolution #126 #132 #129]: false
unsat
-FPTJq9aN3ES4iIrHgaTv+A 208 0
+c8ed8eae868ac61c8f3a616f1b0b1df4032f4eac 208 0
#2 := false
#9 := 0::int
#11 := 4::int
@@ -7090,7 +7090,7 @@
#418 := [unit-resolution #417 #36]: #298
[th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
unsat
-yN0aj3KferzvOSp2KlyNwg 24 0
+7beaddc803d2c23197634dc63d56d564292d85fe 24 0
#2 := false
#4 := (exists (vars (?x1 int)) false)
#5 := (not #4)
@@ -7115,7 +7115,7 @@
#22 := [asserted]: #6
[mp #22 #38]: false
unsat
-7iMPasu6AIeHm45slLCByA 24 0
+723fcd1ecb9fa59a7e0fede642f23063fb499818 24 0
#2 := false
#4 := (exists (vars (?x1 real)) false)
#5 := (not #4)
@@ -7140,13 +7140,13 @@
#22 := [asserted]: #6
[mp #22 #38]: false
unsat
-cv2pC2I0gIUYtVwtXngvXg 1 0
-unsat
-4r8/IxBBDH1ZqF0YfzLLTg 1 0
-unsat
-uj7n+C4nG462DNJy9Divrg 1 0
-unsat
-dn/LVwy1BXEOmtqdUBNhLw 73 0
+a72d0e977596e1fac0cccee600f0bf9d29ed71aa 1 0
+unsat
+70141a690f46561f859d3deed80b9611816f9f81 1 0
+unsat
+41b6ddffa2c7efc9285d0e0a65d74c4325ef6ddb 1 0
+unsat
+a08fcdd29520930b0a940df57c3d8266dbefd10f 73 0
#2 := false
#5 := 0::int
#8 := 1::int
@@ -7220,7 +7220,7 @@
#144 := [trans #142 #82]: #143
[mp #144 #146]: false
unsat
-VzZ1W5SEEis1AJp1qZz86g 82 0
+470993954e986ab72716000fd7da9fa600b05225 82 0
#2 := false
#5 := (:var 0 int)
#7 := 0::int
@@ -7303,7 +7303,7 @@
#30 := [asserted]: #14
[mp #30 #96]: false
unsat
-UoXgZh5LkmyNCmQEfEtnig 78 0
+40c93af1a084932780f95bda03b3df7712e01201 78 0
#2 := false
#5 := (:var 0 int)
#7 := 2::int
@@ -7382,7 +7382,7 @@
#31 := [asserted]: #15
[mp #31 #92]: false
unsat
-Qv4gVhCmOzC39uufV9ZpDA 61 0
+26b175ea54cef59293a917c6fb083751b00d312a 61 0
#2 := false
#9 := (:var 0 int)
#4 := 2::int
@@ -7444,7 +7444,7 @@
#30 := [asserted]: #14
[mp #30 #75]: false
unsat
-+j+tSj7aUImWej2XcTL9dw 111 0
+74037c10b4f126275ba21e7140b7f1e159b39ed9 111 0
#2 := false
#4 := 2::int
decl ?x1!1 :: int
@@ -7556,7 +7556,7 @@
#184 := [th-lemma]: #183
[unit-resolution #184 #127 #125 #126]: false
unsat
-kQRsBd9oowc7exsvsEgTUg 89 0
+628c1b88ca8fb09c896ae05059a52dc2f8e25db2 89 0
#2 := false
#4 := 0::int
decl ?x1!0 :: int
@@ -7646,7 +7646,7 @@
#167 := [unit-resolution #154 #90]: #166
[unit-resolution #167 #165 #162]: false
unsat
-VPjD8BtzPcTZKIRT4SA3Nw 83 2
+b7c4f9440c4594c46eee14ce57f17610bb7e2536 83 2
#2 := false
#5 := 0::int
#4 := (:var 0 int)
@@ -7732,7 +7732,7 @@
unsat
WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
-DCV5zpDW3cC2A61VghqFkA 180 2
+7a9cc3ee85422788d981af84d181bd61d65f774c 180 2
#2 := false
#4 := 0::int
#5 := (:var 0 int)
@@ -7915,7 +7915,7 @@
unsat
WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
-lYXJpXHB9nLXJbOsr9VH1w 68 0
+5201b12abd6b3d0f247a34c1fd9f443fc951c55f 68 0
#2 := false
#12 := 1::int
#9 := (:var 1 int)
@@ -7984,7 +7984,7 @@
#32 := [asserted]: #16
[mp #32 #83]: false
unsat
-jNvpOd8qnh73F8B6mQDrRw 107 0
+0f9091dc6853772b5280c29fc11ae1382022f24d 107 0
#2 := false
#4 := 0::int
decl ?x2!1 :: int
@@ -8092,7 +8092,7 @@
#123 := [and-elim #101]: #88
[th-lemma #123 #124 #125]: false
unsat
-QWWPBUGjgvTCpxqJ9oPGdQ 117 0
+a19e2cec45cb985989328595a0e06836a1e0fbc3 117 0
#2 := false
#4 := 0::int
decl ?x2!1 :: int
@@ -8210,7 +8210,7 @@
#188 := [unit-resolution #187 #110]: #98
[unit-resolution #188 #130]: false
unsat
-3r4MsKEvDJc1RWnNRxu/3Q 148 0
+34bf666106f50c4ee2e8834de4912d59c6e7d9d9 148 0
#2 := false
#144 := (not false)
#7 := 0::int
@@ -8359,7 +8359,7 @@
#158 := [mp #126 #157]: #153
[mp #158 #181]: false
unsat
-Q+cnHyqIFLGWsSlQkp3fEg 67 0
+1d6946d9384f22b76e98f04aff657c54e4fe51ad 67 0
#2 := false
#4 := (:var 0 int)
#5 := (pattern #4)
@@ -8427,9 +8427,9 @@
#30 := [asserted]: #14
[mp #30 #80]: false
unsat
-Q7HDzu4ER2dw+lHHM6YgFg 1 0
-unsat
-saejIG5KeeVxOolEIo3gtw 75 0
+d938f8b556e86b20a82e4661e3a61bad7d95357d 1 0
+unsat
+dfca84a72c9a54145743ea34eaa7c75e8665fd45 75 0
#2 := false
#6 := 1::int
decl uf_3 :: int
@@ -8505,7 +8505,7 @@
#32 := [asserted]: #16
[mp #32 #86]: false
unsat
-PPaoU5CzQFYr3LRpOsGPhQ 62 0
+2662a556257bfe403cd3fda75e9fe55964bc9dcd 62 0
#2 := false
decl uf_2 :: real
#6 := uf_2
@@ -8568,7 +8568,7 @@
#32 := [asserted]: #16
[mp #32 #74]: false
unsat
-hXKzem5+KYZMOj+GKxjszQ 141 0
+99d65e323e3d85dbdc2d8c52c169db4d46ead198 141 0
#2 := false
decl uf_4 :: int
#9 := uf_4
@@ -8710,7 +8710,7 @@
#45 := [asserted]: #29
[mp #45 #150]: false
unsat
-3D8WhjZTO7T824d7mwXcCA 252 0
+2e721ab2035f9845f1e87e78db6dfc67c28f6d40 252 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -8963,7 +8963,7 @@
#539 := [unit-resolution #532 #451]: #557
[th-lemma #455 #539 #537 #546]: false
unsat
-kyphS4o71h68g2YhvYbQQQ 223 0
+5d4787d5f6bf7b62bda1a48bdd01dc6863801852 223 0
#2 := false
#23 := 3::int
decl uf_2 :: (-> T1 int)
@@ -9187,7 +9187,7 @@
#598 := [unit-resolution #593 #596]: #623
[th-lemma #152 #598 #139]: false
unsat
-M8P5WxpiY5AWxaJDBtXoLQ 367 0
+60689c41168db239dbf5f3a98d5f2bce0fef9e02 367 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -9555,7 +9555,7 @@
#456 := [th-lemma]: #455
[unit-resolution #456 #464 #452]: false
unsat
-Xs4JZCKb5egkcPabsrodXg 302 0
+94b7ba760bb9dd467688fc28632e0ae8f6f51951 302 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -9858,7 +9858,7 @@
#601 := [unit-resolution #615 #613]: #683
[th-lemma #623 #188 #601 #628]: false
unsat
-clMAi2WqMi360EjFURRGLg 458 0
+8d2fca14b1477934a0c7f4f6528bd3be029bba7b 458 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -10317,7 +10317,7 @@
#350 := [unit-resolution #369 #367]: #368
[unit-resolution #350 #323]: false
unsat
-mu7O1os0t3tPqWZhwizjxw 161 0
+720080123967f7b12d5ac9ba2a5e5203400a16cd 161 0
#2 := false
#9 := 0::int
decl uf_3 :: int
@@ -10479,7 +10479,7 @@
#361 := [unit-resolution #639 #655]: #647
[th-lemma #656 #361 #261]: false
unsat
-08cmOtIT4NYs2PG/F3zeZw 557 0
+980ba021fe0853c3aa46377383e3f0f6fa9e2888 557 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -11037,57 +11037,57 @@
#990 := [unit-resolution #501 #807]: #511
[unit-resolution #990 #989 #979]: false
unsat
-8HdmSMHHP2B8XMFzjNuw5Q 1 0
-unsat
-O4aM0+/isn2q5CrIefZjzg 1 0
-unsat
-t/ni9djl2DqxH0iKupZSwg 1 0
-unsat
-RumBGekdxZQaBF1HNa3x9w 1 0
-unsat
-Q9d+IbQ8chjKld71X6/zqw 1 0
-unsat
-PhC8zQV8hnJ6E2YYjZPGjQ 1 0
-unsat
-mieI2RhSp3bYaojlWH1A4A 1 0
-unsat
-pRSV6nBLconzrQz2zUrJ6g 1 0
-unsat
-Js0JfdwDoKq3YuilPPgeZw 1 0
-unsat
-GRIqjLUJiqXbo+pXhAeKIw 1 0
-unsat
-Bg5scsmPFp82+7Y2ScL6Wg 1 0
-unsat
-XD6zX6850dLxyfZSfNv30A 1 0
-unsat
-BG/HwJYnumvDICXxtBu/tA 1 0
-unsat
-YMc4t19sUMWbUkx3woxCmQ 1 0
-unsat
-YyD9IF72pKXGGKZTO7FY5Q 1 0
-unsat
-zRPsIUi+TEoz5fPWP0H9bQ 1 0
-unsat
-8ipTE8BOXpvSo/U6D4p3lA 1 0
-unsat
-MSzQywedZPsOE0CDxrrO0g 1 0
-unsat
-SryZuXv48ItET8NPIv07pA 1 0
-unsat
-qOMUQN18hYFl/wWt54lvbA 1 0
-unsat
-+njWXdn6fETK3/AjtiHjcA 1 0
-unsat
-5cQ7gJ33gzYTIIPA3hbBmQ 1 0
-unsat
-ZznT34cvumrP00mXZ3gcjw 1 0
-unsat
-//LQca1Et5RfhQJZA+CGCA 1 0
-unsat
-3ntxKz+kaQNfTrLzY9sVXw 1 0
-unsat
-4lL2Qo8ngE1EH1UdeN1Qng 43 0
+22877b17eafaba69b1f8a961a616fea28ae70d56 1 0
+unsat
+b5839159097bbd4e601a5681d1ca3493ec994a7c 1 0
+unsat
+90e1074350b5dcaae149781bcaa5d643b2ca9f48 1 0
+unsat
+08c7117fe974f5767051ed5aa61a27ce3084eb1d 1 0
+unsat
+858012417c9d327d8997f2a5dcb3da095ec65d34 1 0
+unsat
+84b2eee4890eaadb3638c7e522fb3237b3d476b0 1 0
+unsat
+8867717d9736308a2c27df0665a6e391b0562076 1 0
+unsat
+cd79c9a0488ab597d08dd9a0d6ac0f3647003bd6 1 0
+unsat
+395dd6c10b2a432137f9e3401cba8ec4dd64911b 1 0
+unsat
+17e3cc9534e04d86f095ec1a92c77d46d7dbb8e5 1 0
+unsat
+e046ea79beacf4bc3567b3b7f755232369d0c185 1 0
+unsat
+8ce4235464829d4be72e682f0c72bc5e3c6902d0 1 0
+unsat
+656a40b977d7716264443900d6bdb4d3d117d52f 1 0
+unsat
+ec27a57e58719625ff71dd4d68ed53a3851efb5c 1 0
+unsat
+2c3c366b8488ca0991cc767c94cdb78b18db9d5f 1 0
+unsat
+5894f6f19250b12885e38f54eae81f143b58fa01 1 0
+unsat
+e150815d9eb1ec168805b5501d7f4b2e378dd883 1 0
+unsat
+396d6254e993f414335de9378150e486d3cfcd4e 1 0
+unsat
+96014c61f582a811aff25ad7fa62b575b830fa8b 1 0
+unsat
+10580b87c0d062c9854e79d16047a53d045ccfac 1 0
+unsat
+87b5f388df1f43cc02ac0fa0d6944eb8cd8f8f50 1 0
+unsat
+92a5e2bb68f74b9e7dd3a9ef79ea641e9700d563 1 0
+unsat
+152e0f0f0a04b399b057beae92ae0455408b224f 1 0
+unsat
+41925af4711748a6e411453f2465920a1c6ffb8e 1 0
+unsat
+757462716f4a2619a1410bdca3faa2d058042c10 1 0
+unsat
+abdeeb4668a63f19473d6da94232379344d99fea 43 0
#2 := false
#6 := 0::int
decl uf_1 :: (-> bv[2] int)
@@ -11131,9 +11131,9 @@
#287 := [th-lemma]: #627
[unit-resolution #287 #47 #635]: false
unsat
-+xe3O927LrflFUE6NDqRlA 1 0
-unsat
-JPoL7fPYhqhAkjUiVF+THQ 50 0
+2e4bd6e1ab7bfedbefd3ada8caf5332ba5651065 1 0
+unsat
+96d2e1aad559535e781a07ee5e55bb19caef769c 50 0
#2 := false
decl uf_6 :: T2
#23 := uf_6
@@ -11184,7 +11184,7 @@
#66 := [asserted]: #26
[unit-resolution #66 #235]: false
unsat
-l23ZDmd0VbO/Q+uO5EtabA 105 0
+008ad82b0a62ff600e66e8f2cc72b5795c7c5032 105 0
#2 := false
decl uf_6 :: (-> T4 T2)
decl uf_10 :: T4
@@ -11290,7 +11290,7 @@
#110 := [asserted]: #46
[unit-resolution #110 #238]: false
unsat
-GZjffeZPQnL3OyLCvxdCpg 181 0
+0a15a60660bc0c3f06688ad5de50ed50a24d0df0 181 0
#2 := false
decl uf_1 :: (-> T1 T2 T3)
decl uf_3 :: T2
@@ -11472,7 +11472,7 @@
#76 := [asserted]: #38
[unit-resolution #76 #489]: false
unsat
-i6jCzzRosHYE0w7sF1Nraw 62 0
+dde2364f13fc9ce8af00c7a02bfea9a6c979a805 62 0
#2 := false
decl up_4 :: (-> T1 T2 bool)
decl uf_3 :: T2
@@ -11535,7 +11535,7 @@
#73 := [unit-resolution #71 #68]: #72
[unit-resolution #73 #59 #61]: false
unsat
-YZHSyhN2TGlpe+vpkzWrgQ 115 0
+3cb6787c7063b0a04bff9e2bfa4203b73903dabe 115 0
#2 := false
decl up_2 :: (-> T2 bool)
decl uf_3 :: T2
@@ -11651,7 +11651,7 @@
#560 := [mp #344 #559]: #557
[unit-resolution #560 #576 #561]: false
unsat
-TibRlXkU+X+1+zGPYTiT0g 464 0
+dcb635ada6f2482ea11de30713fe962bcb57c9ad 464 0
#2 := false
decl uf_2 :: (-> T2 T3 T3)
decl uf_4 :: T3
@@ -12116,7 +12116,7 @@
#177 := [asserted]: #53
[unit-resolution #177 #793]: false
unsat
-DJPKxi9AO25zGBcs5kxUrw 21 0
+ca467a37d809de06757809cab1cd30e08586674f 21 0
#2 := false
decl up_1 :: (-> T1 bool)
#4 := (:var 0 T1)
@@ -12138,7 +12138,7 @@
#25 := [asserted]: #9
[mp #25 #34]: false
unsat
-i5PnMbuM9mWv5LnVszz9+g 366 0
+f6e9645ebbb8739d12b8e96bc83ddef33c7d53bc 366 0
#2 := false
decl uf_1 :: (-> int T1)
#37 := 6::int
@@ -12505,7 +12505,7 @@
#182 := [asserted]: #40
[unit-resolution #182 #399]: false
unsat
-K2SXMHU6QCZJ8TRs6zjKRg 408 0
+b15b527236338a437e355afcde07dd3c6dfc451f 408 0
#2 := false
#22 := 0::int
#8 := 2::int
@@ -12914,7 +12914,7 @@
#375 := [unit-resolution #374 #407]: #708
[th-lemma #375 #370 #465]: false
unsat
-1DhSL9G2fGRGmuI8IaMNOA 50 0
+71b79533f46a8514b2fc189fc382867d50f52a9a 50 0
#2 := false
decl up_35 :: (-> int bool)
#112 := 1::int
@@ -12965,7 +12965,7 @@
#504 := [quant-inst]: #503
[unit-resolution #504 #916 #297]: false
unsat
-dyXROdcPFSd36N3K7dpmDw 506 0
+e40ba7aed8ae5409337a331038da0587c03354d6 506 0
#2 := false
decl uf_17 :: (-> T8 T3)
decl uf_18 :: (-> T1 T8)
--- a/src/HOL/SMT/SMT_Base.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy Wed Mar 24 17:41:25 2010 +0100
@@ -8,7 +8,7 @@
imports Real "~~/src/HOL/Word/Word"
"~~/src/HOL/Decision_Procs/Dense_Linear_Order"
uses
- "~~/src/Tools/Cache_IO/cache_io.ML"
+ "~~/src/Tools/cache_io.ML"
("Tools/smt_normalize.ML")
("Tools/smt_monomorph.ML")
("Tools/smt_translate.ML")
--- a/src/HOLCF/Lift.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOLCF/Lift.thy Wed Mar 24 17:41:25 2010 +0100
@@ -170,28 +170,6 @@
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
-text {*
- \medskip Extension of @{text cont_tac} and installation of simplifier.
-*}
-
-lemmas cont_lemmas_ext =
- cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
- cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
-
-ML {*
-local
- val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext";
- val flift1_def = thm "flift1_def";
-in
-
-fun cont_tac i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = REPEAT (cont_tac i);
-
-fun cont_tacRs ss i =
- simp_tac ss i THEN
- REPEAT (cont_tac i)
-end;
-*}
subsection {* Lifted countable types are bifinite *}
--- a/src/HOLCF/ex/Dagstuhl.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy Wed Mar 24 17:41:25 2010 +0100
@@ -72,7 +72,7 @@
apply (unfold YYS_def)
apply (rule fix_least)
apply (subst beta_cfun)
- apply (tactic "cont_tacR 1")
+ apply simp
apply (simp add: YS_def2 [symmetric])
done
--- a/src/HOLCF/ex/Hoare.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Mar 24 17:41:25 2010 +0100
@@ -232,12 +232,8 @@
lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (simp (no_asm))
apply (rule allI)
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
@@ -256,12 +252,8 @@
lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
@@ -285,12 +277,8 @@
lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
--- a/src/HOLCF/ex/Loop.thy Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy Wed Mar 24 17:41:25 2010 +0100
@@ -137,10 +137,8 @@
ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
apply (simplesubst while_def2)
apply (rule fix_ind)
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
--- a/src/Tools/Cache_IO/cache_io.ML Wed Mar 24 17:40:44 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-(* Title: Tools/Cache_IO/cache_io.ML
- Author: Sascha Boehme, TU Muenchen
-
-Cache for output of external processes.
-*)
-
-signature CACHE_IO =
-sig
- val with_tmp_file: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> string) -> Path.T -> string list
- val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
-
- type cache
- val make: Path.T -> cache
- val cache_path_of: cache -> Path.T
- val cached: cache -> (Path.T -> string) -> Path.T -> string list
- val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
- string list * string list
-end
-
-structure Cache_IO : CACHE_IO =
-struct
-
-fun with_tmp_file name f =
- let
- val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val x = Exn.capture f path
- val _ = try File.rm path
- in Exn.release x end
-
-fun run' make_cmd in_path =
- with_tmp_file "cache-io-" (fn out_path =>
- let
- val (out2, _) = bash_output (make_cmd in_path out_path)
- val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in (out1, split_lines out2) end)
-
-fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
-
-
-
-abstype cache = Cache of {
- path: Path.T,
- table: (int * (int * int * int) Symtab.table) Synchronized.var }
-with
-
-
-fun cache_path_of (Cache {path, ...}) = path
-
-
-fun load cache_path =
- let
- fun err () = error ("Cache IO: corrupted cache file: " ^
- File.shell_path cache_path)
-
- fun int_of_string s =
- (case read_int (explode s) of
- (i, []) => i
- | _ => err ())
-
- fun split line =
- (case space_explode " " line of
- [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
- | _ => err ())
-
- fun parse line ((i, l), tab) =
- if i = l
- then
- let val (key, l1, l2) = split line
- in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
- else ((i+1, l), tab)
- in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
-
-fun make path =
- let val table = if File.exists path then load path else (1, Symtab.empty)
- in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
-
-
-fun get_hash_key path =
- let
- val arg = File.shell_path path
- val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg)
- in
- if res = 0 then hd (split_lines out)
- else error ("Cache IO: failed to generate hash key for file " ^ arg)
- end
-
-fun load_cached_result cache_path (p, len1, len2) =
- let
- fun load line (i, xsp) =
- if i < p then (i+1, xsp)
- else if i < p + len1 then (i+1, apfst (cons line) xsp)
- else if i < p + len2 then (i+1, apsnd (cons line) xsp)
- else (i, xsp)
- in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
-
-fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
- let val key = get_hash_key in_path
- in
- (case Symtab.lookup (snd (Synchronized.value table)) key of
- SOME pos => load_cached_result cache_path pos
- | NONE =>
- let
- val res as (out, err) = run' make_cmd in_path
- val (l1, l2) = pairself length res
- val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
- val lines = map (suffix "\n") (header :: out @ err)
-
- val _ = Synchronized.change table (fn (p, tab) =>
- if Symtab.defined tab key then (p, tab)
- else
- let val _ = File.append_list cache_path lines
- in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in res end)
- end
-
-fun cached cache make_cmd =
- snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
-
-end
-end
--- a/src/Tools/Cache_IO/etc/settings Wed Mar 24 17:40:44 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-ISABELLE_CACHE_IO="$COMPONENT"
-
-COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
-
--- a/src/Tools/Cache_IO/lib/scripts/compute_hash_key Wed Mar 24 17:40:44 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Compute MD5 hash key.
-
-use strict;
-use warnings;
-use Digest::MD5;
-
-
-# argument
-
-my $file = $ARGV[0];
-
-
-# compute MD5 hash key
-
-my $md5 = Digest::MD5->new;
-open FILE, "<$file" or die "ERROR: Failed to open '$file' ($!)";
-$md5->addfile(*FILE);
-close FILE;
-print $md5->b64digest . "\n";
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/cache_io.ML Wed Mar 24 17:41:25 2010 +0100
@@ -0,0 +1,112 @@
+(* Title: Tools/cache_io.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Cache for output of external processes.
+*)
+
+signature CACHE_IO =
+sig
+ val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+ val run: (Path.T -> string) -> Path.T -> string list
+ val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+
+ type cache
+ val make: Path.T -> cache
+ val cache_path_of: cache -> Path.T
+ val cached: cache -> (Path.T -> string) -> Path.T -> string list
+ val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+ string list * string list
+end
+
+structure Cache_IO : CACHE_IO =
+struct
+
+fun with_tmp_file name f =
+ let
+ val path = File.tmp_path (Path.explode (name ^ serial_string ()))
+ val x = Exn.capture f path
+ val _ = try File.rm path
+ in Exn.release x end
+
+fun run' make_cmd in_path =
+ with_tmp_file "cache-io-" (fn out_path =>
+ let
+ val (out2, _) = bash_output (make_cmd in_path out_path)
+ val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+ in (out1, split_lines out2) end)
+
+fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+
+
+
+abstype cache = Cache of {
+ path: Path.T,
+ table: (int * (int * int * int) Symtab.table) Synchronized.var }
+with
+
+
+fun cache_path_of (Cache {path, ...}) = path
+
+
+fun load cache_path =
+ let
+ fun err () = error ("Cache IO: corrupted cache file: " ^
+ File.shell_path cache_path)
+
+ fun int_of_string s =
+ (case read_int (explode s) of
+ (i, []) => i
+ | _ => err ())
+
+ fun split line =
+ (case space_explode " " line of
+ [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
+ | _ => err ())
+
+ fun parse line ((i, l), tab) =
+ if i = l
+ then
+ let val (key, l1, l2) = split line
+ in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
+ else ((i+1, l), tab)
+ in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
+
+fun make path =
+ let val table = if File.exists path then load path else (1, Symtab.empty)
+ in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
+
+
+fun load_cached_result cache_path (p, len1, len2) =
+ let
+ fun load line (i, xsp) =
+ if i < p then (i+1, xsp)
+ else if i < p + len1 then (i+1, apfst (cons line) xsp)
+ else if i < p + len2 then (i+1, apsnd (cons line) xsp)
+ else (i, xsp)
+ in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
+
+fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
+ let val key = SHA1.digest (File.read in_path)
+ in
+ (case Symtab.lookup (snd (Synchronized.value table)) key of
+ SOME pos => load_cached_result cache_path pos
+ | NONE =>
+ let
+ val res as (out, err) = run' make_cmd in_path
+ val (l1, l2) = pairself length res
+ val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+ val lines = map (suffix "\n") (header :: out @ err)
+
+ val _ = Synchronized.change table (fn (p, tab) =>
+ if Symtab.defined tab key then (p, tab)
+ else
+ let val _ = File.append_list cache_path lines
+ in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
+ in res end)
+ end
+
+fun cached cache make_cmd =
+ snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+end
+end