src/HOL/Multivariate_Analysis/Integration.certs

 #425 := [unit-resolution #424 #319 #414 #321 #421]: #379
 #426 := [unit-resolution #383 #425]: #378
 #427 := [unit-resolution #411 #426]: #395
 [th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
 unsat
-76aef63700c44d6a49155f473f80703718124469 57 0
+02d40f3e43c6a17458cd5dc30adbe4da03d87a0c 57 0
 #2 := false
-#37 := 0::Real
+#41 := 0::Real
 decl f12 :: (-> S5 Real)
 decl f13 :: (-> S4 S4 S5)
 decl f14 :: (-> S3 S4)
 decl f4 :: S3
 #8 := f4
-#45 := (f14 f4)
+#38 := (f14 f4)
 decl f10 :: S3
 #25 := f10
-#44 := (f14 f10)
-#46 := (f13 #44 #45)
-#47 := (f12 #46)
-#258 := (>= #47 0::Real)
-#260 := (not #258)
-#49 := (= #47 0::Real)
+#37 := (f14 f10)
+#39 := (f13 #37 #38)
+#40 := (f12 #39)
+#248 := (>= #40 0::Real)
+#250 := (not #248)
+#49 := (= #40 0::Real)
 #50 := (not #49)
 #134 := [asserted]: #50
-#266 := (or #49 #260)
-#48 := (<= #47 0::Real)
+#256 := (or #49 #250)
+#42 := (<= #40 0::Real)
+#132 := [asserted]: #42
+#249 := (not #42)
+#254 := (or #49 #249 #250)
+#255 := [th-lemma arith triangle-eq]: #254
+#257 := [unit-resolution #255 #132]: #256
+#258 := [unit-resolution #257 #134]: #250
+#44 := (:var 0 S4)
+#43 := (:var 1 S4)
+#45 := (f13 #43 #44)
+#241 := (pattern #45)
+#46 := (f12 #45)
+#137 := (>= #46 0::Real)
+#242 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #241) #137)
+#139 := (forall (vars (?v0 S4) (?v1 S4)) #137)
+#245 := (iff #139 #242)
+#243 := (iff #137 #137)
+#244 := [refl]: #243
+#246 := [quant-intro #244]: #245
+#146 := (~ #139 #139)
+#148 := (~ #137 #137)
+#145 := [refl]: #148
+#143 := [nnf-pos #145]: #146
+#47 := (<= 0::Real #46)
+#48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
+#140 := (iff #48 #139)
+#136 := (iff #47 #137)
+#138 := [rewrite]: #136
+#141 := [quant-intro #138]: #140
 #133 := [asserted]: #48
-#259 := (not #48)
-#264 := (or #49 #259 #260)
-#265 := [th-lemma arith triangle-eq]: #264
-#267 := [unit-resolution #265 #133]: #266
-#268 := [unit-resolution #267 #134]: #260
-#39 := (:var 0 S4)
-#38 := (:var 1 S4)
-#40 := (f13 #38 #39)
-#251 := (pattern #40)
-#41 := (f12 #40)
-#136 := (>= #41 0::Real)
-#252 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #251) #136)
-#138 := (forall (vars (?v0 S4) (?v1 S4)) #136)
-#255 := (iff #138 #252)
-#253 := (iff #136 #136)
-#254 := [refl]: #253
-#256 := [quant-intro #254]: #255
-#165 := (~ #138 #138)
-#153 := (~ #136 #136)
-#154 := [refl]: #153
-#166 := [nnf-pos #154]: #165
-#42 := (<= 0::Real #41)
-#43 := (forall (vars (?v0 S4) (?v1 S4)) #42)
-#139 := (iff #43 #138)
-#135 := (iff #42 #136)
-#137 := [rewrite]: #135
-#140 := [quant-intro #137]: #139
-#132 := [asserted]: #43
-#141 := [mp #132 #140]: #138
-#167 := [mp~ #141 #166]: #138
-#257 := [mp #167 #256]: #252
-#261 := (not #252)
-#262 := (or #261 #258)
-#263 := [quant-inst #44 #45]: #262
-[unit-resolution #263 #257 #268]: false
+#142 := [mp #133 #141]: #139
+#144 := [mp~ #142 #143]: #139
+#247 := [mp #144 #246]: #242
+#251 := (not #242)
+#252 := (or #251 #248)
+#253 := [quant-inst #37 #38]: #252
+[unit-resolution #253 #247 #258]: false
+unsat
+d7759998d2972bb8616477c86659060b5a9117ad 218 0
+#2 := false
+#31 := 0::Real
+decl f3 :: (-> S2 S3 Real)
+decl f5 :: S3
+#9 := f5
+decl f10 :: S2
+#23 := f10
+#34 := (f3 f10 f5)
+#102 := -1::Real
+#348 := (* -1::Real #34)
+decl f6 :: S2
+#11 := f6
+#12 := (f3 f6 f5)
+#374 := (+ #12 #348)
+#375 := (>= #374 0::Real)
+#380 := (not #375)
+decl f4 :: S2
+#8 := f4
+#10 := (f3 f4 f5)
+#349 := (+ #10 #348)
+#350 := (<= #349 0::Real)
+#351 := (not #350)
+#383 := (or #351 #380)
+#386 := (not #383)
+#19 := (:var 0 S3)
+#26 := (f3 f6 #19)
+#318 := (pattern #26)
+#24 := (f3 f10 #19)
+#317 := (pattern #24)
+#22 := (f3 f4 #19)
+#316 := (pattern #22)
+decl f7 :: (-> S3 Int)
+#20 := (f7 #19)
+#315 := (pattern #20)
+#108 := (* -1::Real #26)
+#109 := (+ #24 #108)
+#110 := (<= #109 0::Real)
+#246 := (not #110)
+#103 := (* -1::Real #24)
+#104 := (+ #22 #103)
+#105 := (<= #104 0::Real)
+#245 := (not #105)
+#247 := (or #245 #246)
+#248 := (not #247)
+#40 := 0::Int
+#75 := -1::Int
+#89 := (* -1::Int #20)
+decl f8 :: (-> S4 S3)
+decl f9 :: S4
+#15 := f9
+#16 := (f8 f9)
+#17 := (f7 #16)
+#90 := (+ #17 #89)
+#91 := (<= #90 0::Int)
+#251 := (or #91 #248)
+#319 := (forall (vars (?v0 S3)) (:pat #315 #316 #317 #318) #251)
+#254 := (forall (vars (?v0 S3)) #251)
+#322 := (iff #254 #319)
+#320 := (iff #251 #251)
+#321 := [refl]: #320
+#323 := [quant-intro #321]: #322
+#113 := (and #105 #110)
+#116 := (or #91 #113)
+#119 := (forall (vars (?v0 S3)) #116)
+#255 := (iff #119 #254)
+#252 := (iff #116 #251)
+#249 := (iff #113 #248)
+#250 := [rewrite]: #249
+#253 := [monotonicity #250]: #252
+#256 := [quant-intro #253]: #255
+#239 := (~ #119 #119)
+#241 := (~ #116 #116)
+#242 := [refl]: #241
+#240 := [nnf-pos #242]: #239
+#27 := (<= #24 #26)
+#25 := (<= #22 #24)
+#28 := (and #25 #27)
+#21 := (< #20 #17)
+#29 := (implies #21 #28)
+#30 := (forall (vars (?v0 S3)) #29)
+#122 := (iff #30 #119)
+#74 := (not #21)
+#83 := (or #74 #28)
+#86 := (forall (vars (?v0 S3)) #83)
+#120 := (iff #86 #119)
+#117 := (iff #83 #116)
+#114 := (iff #28 #113)
+#111 := (iff #27 #110)
+#112 := [rewrite]: #111
+#106 := (iff #25 #105)
+#107 := [rewrite]: #106
+#115 := [monotonicity #107 #112]: #114
+#100 := (iff #74 #91)
+#92 := (not #91)
+#95 := (not #92)
+#98 := (iff #95 #91)
+#99 := [rewrite]: #98
+#96 := (iff #74 #95)
+#93 := (iff #21 #92)
+#94 := [rewrite]: #93
+#97 := [monotonicity #94]: #96
+#101 := [trans #97 #99]: #100
+#118 := [monotonicity #101 #115]: #117
+#121 := [quant-intro #118]: #120
+#87 := (iff #30 #86)
+#84 := (iff #29 #83)
+#85 := [rewrite]: #84
+#88 := [quant-intro #85]: #87
+#123 := [trans #88 #121]: #122
+#73 := [asserted]: #30
+#124 := [mp #73 #123]: #119
+#237 := [mp~ #124 #240]: #119
+#257 := [mp #237 #256]: #254
+#324 := [mp #257 #323]: #319
+#78 := (* -1::Int #17)
+#14 := (f7 f5)
+#79 := (+ #14 #78)
+#77 := (>= #79 0::Int)
+#76 := (not #77)
+#18 := (< #14 #17)
+#80 := (iff #18 #76)
+#81 := [rewrite]: #80
+#72 := [asserted]: #18
+#82 := [mp #72 #81]: #76
+#392 := (not #319)
+#393 := (or #392 #77 #386)
+#344 := (* -1::Real #12)
+#345 := (+ #34 #344)
+#346 := (<= #345 0::Real)
+#347 := (not #346)
+#352 := (or #351 #347)
+#353 := (not #352)
+#354 := (* -1::Int #14)
+#355 := (+ #17 #354)
+#356 := (<= #355 0::Int)
+#357 := (or #356 #353)
+#394 := (or #392 #357)
+#401 := (iff #394 #393)
+#389 := (or #77 #386)
+#396 := (or #392 #389)
+#399 := (iff #396 #393)
+#400 := [rewrite]: #399
+#397 := (iff #394 #396)
+#390 := (iff #357 #389)
+#387 := (iff #353 #386)
+#384 := (iff #352 #383)
+#381 := (iff #347 #380)
+#378 := (iff #346 #375)
+#368 := (+ #344 #34)
+#371 := (<= #368 0::Real)
+#376 := (iff #371 #375)
+#377 := [rewrite]: #376
+#372 := (iff #346 #371)
+#369 := (= #345 #368)
+#370 := [rewrite]: #369
+#373 := [monotonicity #370]: #372
+#379 := [trans #373 #377]: #378
+#382 := [monotonicity #379]: #381
+#385 := [monotonicity #382]: #384
+#388 := [monotonicity #385]: #387
+#366 := (iff #356 #77)
+#358 := (+ #354 #17)
+#361 := (<= #358 0::Int)
+#364 := (iff #361 #77)
+#365 := [rewrite]: #364
+#362 := (iff #356 #361)
+#359 := (= #355 #358)
+#360 := [rewrite]: #359
+#363 := [monotonicity #360]: #362
+#367 := [trans #363 #365]: #366
+#391 := [monotonicity #367 #388]: #390
+#398 := [monotonicity #391]: #397
+#402 := [trans #398 #400]: #401
+#395 := [quant-inst #9]: #394
+#403 := [mp #395 #402]: #393
+#530 := [unit-resolution #403 #82 #324]: #386
+#406 := (or #383 #375)
+#407 := [def-axiom]: #406
+#531 := [unit-resolution #407 #530]: #375
+#492 := (>= #349 0::Real)
+#541 := (not #492)
+#491 := (= #10 #34)
+#536 := (not #491)
+#127 := (= #12 #34)
+#135 := (not #127)
+#537 := (iff #135 #536)
+#534 := (iff #127 #491)
+#532 := (iff #491 #127)
+#13 := (= #10 #12)
+#71 := [asserted]: #13
+#533 := [monotonicity #71]: #532
+#535 := [symm #533]: #534
+#538 := [monotonicity #535]: #537
+#35 := (= #34 #12)
+#36 := (not #35)
+#136 := (iff #36 #135)
+#133 := (iff #35 #127)
+#134 := [rewrite]: #133
+#137 := [monotonicity #134]: #136
+#126 := [asserted]: #36
+#140 := [mp #126 #137]: #135
+#539 := [mp #140 #538]: #536
+#544 := (or #491 #541)
+#404 := (or #383 #350)
+#405 := [def-axiom]: #404
+#540 := [unit-resolution #405 #530]: #350
+#542 := (or #491 #351 #541)
+#543 := [th-lemma arith triangle-eq]: #542
+#545 := [unit-resolution #543 #540]: #544
+#546 := [unit-resolution #545 #539]: #541
+#486 := (+ #10 #344)
+#490 := (>= #486 0::Real)
+#547 := (not #13)
+#548 := (or #547 #490)
+#549 := [th-lemma arith triangle-eq]: #548
+#550 := [unit-resolution #549 #71]: #490
+[th-lemma arith farkas 1 -1 1 #550 #546 #531]: false
 unsat
 fe6d352e9186ccd9319b5d4bd3ff26ab342ba6c4 351 0
 #2 := false
 #8 := 0::Real
 decl f7 :: (-> S4 S2 Real)

 #732 := [unit-resolution #569 #731]: #565
 #733 := (not #565)
 #734 := (or #733 #709)
 #735 := [th-lemma arith triangle-eq]: #734
 [unit-resolution #735 #732 #718]: false
-unsat
-d7759998d2972bb8616477c86659060b5a9117ad 218 0
-#2 := false
-#31 := 0::Real
-decl f3 :: (-> S2 S3 Real)
-decl f5 :: S3
-#9 := f5
-decl f10 :: S2
-#23 := f10
-#34 := (f3 f10 f5)
-#102 := -1::Real
-#348 := (* -1::Real #34)
-decl f6 :: S2
-#11 := f6
-#12 := (f3 f6 f5)
-#374 := (+ #12 #348)
-#375 := (>= #374 0::Real)
-#380 := (not #375)
-decl f4 :: S2
-#8 := f4
-#10 := (f3 f4 f5)
-#349 := (+ #10 #348)
-#350 := (<= #349 0::Real)
-#351 := (not #350)
-#383 := (or #351 #380)
-#386 := (not #383)
-#19 := (:var 0 S3)
-#26 := (f3 f6 #19)
-#318 := (pattern #26)
-#24 := (f3 f10 #19)
-#317 := (pattern #24)
-#22 := (f3 f4 #19)
-#316 := (pattern #22)
-decl f7 :: (-> S3 Int)
-#20 := (f7 #19)
-#315 := (pattern #20)
-#108 := (* -1::Real #26)
-#109 := (+ #24 #108)
-#110 := (<= #109 0::Real)
-#246 := (not #110)
-#103 := (* -1::Real #24)
-#104 := (+ #22 #103)
-#105 := (<= #104 0::Real)
-#245 := (not #105)
-#247 := (or #245 #246)
-#248 := (not #247)
-#40 := 0::Int
-#75 := -1::Int
-#89 := (* -1::Int #20)
-decl f8 :: (-> S4 S3)
-decl f9 :: S4
-#15 := f9
-#16 := (f8 f9)
-#17 := (f7 #16)
-#90 := (+ #17 #89)
-#91 := (<= #90 0::Int)
-#251 := (or #91 #248)
-#319 := (forall (vars (?v0 S3)) (:pat #315 #316 #317 #318) #251)
-#254 := (forall (vars (?v0 S3)) #251)
-#322 := (iff #254 #319)
-#320 := (iff #251 #251)
-#321 := [refl]: #320
-#323 := [quant-intro #321]: #322
-#113 := (and #105 #110)
-#116 := (or #91 #113)
-#119 := (forall (vars (?v0 S3)) #116)
-#255 := (iff #119 #254)
-#252 := (iff #116 #251)
-#249 := (iff #113 #248)
-#250 := [rewrite]: #249
-#253 := [monotonicity #250]: #252
-#256 := [quant-intro #253]: #255
-#239 := (~ #119 #119)
-#241 := (~ #116 #116)
-#242 := [refl]: #241
-#240 := [nnf-pos #242]: #239
-#27 := (<= #24 #26)
-#25 := (<= #22 #24)
-#28 := (and #25 #27)
-#21 := (< #20 #17)
-#29 := (implies #21 #28)
-#30 := (forall (vars (?v0 S3)) #29)
-#122 := (iff #30 #119)
-#74 := (not #21)
-#83 := (or #74 #28)
-#86 := (forall (vars (?v0 S3)) #83)
-#120 := (iff #86 #119)
-#117 := (iff #83 #116)
-#114 := (iff #28 #113)
-#111 := (iff #27 #110)
-#112 := [rewrite]: #111
-#106 := (iff #25 #105)
-#107 := [rewrite]: #106
-#115 := [monotonicity #107 #112]: #114
-#100 := (iff #74 #91)
-#92 := (not #91)
-#95 := (not #92)
-#98 := (iff #95 #91)
-#99 := [rewrite]: #98
-#96 := (iff #74 #95)
-#93 := (iff #21 #92)
-#94 := [rewrite]: #93
-#97 := [monotonicity #94]: #96
-#101 := [trans #97 #99]: #100
-#118 := [monotonicity #101 #115]: #117
-#121 := [quant-intro #118]: #120
-#87 := (iff #30 #86)
-#84 := (iff #29 #83)
-#85 := [rewrite]: #84
-#88 := [quant-intro #85]: #87
-#123 := [trans #88 #121]: #122
-#73 := [asserted]: #30
-#124 := [mp #73 #123]: #119
-#237 := [mp~ #124 #240]: #119
-#257 := [mp #237 #256]: #254
-#324 := [mp #257 #323]: #319
-#78 := (* -1::Int #17)
-#14 := (f7 f5)
-#79 := (+ #14 #78)
-#77 := (>= #79 0::Int)
-#76 := (not #77)
-#18 := (< #14 #17)
-#80 := (iff #18 #76)
-#81 := [rewrite]: #80
-#72 := [asserted]: #18
-#82 := [mp #72 #81]: #76
-#392 := (not #319)
-#393 := (or #392 #77 #386)
-#344 := (* -1::Real #12)
-#345 := (+ #34 #344)
-#346 := (<= #345 0::Real)
-#347 := (not #346)
-#352 := (or #351 #347)
-#353 := (not #352)
-#354 := (* -1::Int #14)
-#355 := (+ #17 #354)
-#356 := (<= #355 0::Int)
-#357 := (or #356 #353)
-#394 := (or #392 #357)
-#401 := (iff #394 #393)
-#389 := (or #77 #386)
-#396 := (or #392 #389)
-#399 := (iff #396 #393)
-#400 := [rewrite]: #399
-#397 := (iff #394 #396)
-#390 := (iff #357 #389)
-#387 := (iff #353 #386)
-#384 := (iff #352 #383)
-#381 := (iff #347 #380)
-#378 := (iff #346 #375)
-#368 := (+ #344 #34)
-#371 := (<= #368 0::Real)
-#376 := (iff #371 #375)
-#377 := [rewrite]: #376
-#372 := (iff #346 #371)
-#369 := (= #345 #368)
-#370 := [rewrite]: #369
-#373 := [monotonicity #370]: #372
-#379 := [trans #373 #377]: #378
-#382 := [monotonicity #379]: #381
-#385 := [monotonicity #382]: #384
-#388 := [monotonicity #385]: #387
-#366 := (iff #356 #77)
-#358 := (+ #354 #17)
-#361 := (<= #358 0::Int)
-#364 := (iff #361 #77)
-#365 := [rewrite]: #364
-#362 := (iff #356 #361)
-#359 := (= #355 #358)
-#360 := [rewrite]: #359
-#363 := [monotonicity #360]: #362
-#367 := [trans #363 #365]: #366
-#391 := [monotonicity #367 #388]: #390
-#398 := [monotonicity #391]: #397
-#402 := [trans #398 #400]: #401
-#395 := [quant-inst #9]: #394
-#403 := [mp #395 #402]: #393
-#530 := [unit-resolution #403 #82 #324]: #386
-#406 := (or #383 #375)
-#407 := [def-axiom]: #406
-#531 := [unit-resolution #407 #530]: #375
-#492 := (>= #349 0::Real)
-#541 := (not #492)
-#491 := (= #10 #34)
-#536 := (not #491)
-#127 := (= #12 #34)
-#135 := (not #127)
-#537 := (iff #135 #536)
-#534 := (iff #127 #491)
-#532 := (iff #491 #127)
-#13 := (= #10 #12)
-#71 := [asserted]: #13
-#533 := [monotonicity #71]: #532
-#535 := [symm #533]: #534
-#538 := [monotonicity #535]: #537
-#35 := (= #34 #12)
-#36 := (not #35)
-#136 := (iff #36 #135)
-#133 := (iff #35 #127)
-#134 := [rewrite]: #133
-#137 := [monotonicity #134]: #136
-#126 := [asserted]: #36
-#140 := [mp #126 #137]: #135
-#539 := [mp #140 #538]: #536
-#544 := (or #491 #541)
-#404 := (or #383 #350)
-#405 := [def-axiom]: #404
-#540 := [unit-resolution #405 #530]: #350
-#542 := (or #491 #351 #541)
-#543 := [th-lemma arith triangle-eq]: #542
-#545 := [unit-resolution #543 #540]: #544
-#546 := [unit-resolution #545 #539]: #541
-#486 := (+ #10 #344)
-#490 := (>= #486 0::Real)
-#547 := (not #13)
-#548 := (or #547 #490)
-#549 := [th-lemma arith triangle-eq]: #548
-#550 := [unit-resolution #549 #71]: #490
-[th-lemma arith farkas 1 -1 1 #550 #546 #531]: false
 unsat
 2e6294cf4cca8c6e762613c9c359f9400d601092 898 0
 #2 := false
 #11 := 0::Real
 decl ?v3!2 :: Real