--- a/src/HOL/Multivariate_Analysis/Integration.certs Tue Dec 04 18:00:37 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2413 +0,0 @@
-823dd49076db7ff6c930933717564ae1a0583125 272 0
-#2 := false
-#47 := 0::Real
-decl f5 :: (-> S4 S5 Real)
-decl f8 :: S5
-#13 := f8
-decl f19 :: S4
-#44 := f19
-#45 := (f5 f19 f8)
-decl f17 :: (-> S3 S10 Real)
-decl f18 :: S10
-#42 := f18
-decl f9 :: S3
-#17 := f9
-#43 := (f17 f9 f18)
-#93 := -1::Real
-#104 := (* -1::Real #43)
-#105 := (+ #104 #45)
-#94 := (* -1::Real #45)
-#95 := (+ #43 #94)
-#223 := (>= #95 0::Real)
-#230 := (if #223 #95 #105)
-#384 := (* -1::Real #230)
-#385 := (+ #105 #384)
-#386 := (<= #385 0::Real)
-#361 := (= #105 #230)
-#224 := (not #223)
-decl f4 :: S3
-#7 := f4
-#57 := (f17 f4 f18)
-#137 := (* -1::Real #57)
-decl f20 :: S4
-#53 := f20
-#54 := (f5 f20 f8)
-#138 := (+ #54 #137)
-#121 := (* -1::Real #54)
-#128 := (+ #121 #57)
-#181 := (<= #138 0::Real)
-#188 := (if #181 #128 #138)
-#380 := (* -1::Real #188)
-#383 := (+ #138 #380)
-#387 := (<= #383 0::Real)
-#375 := (= #138 #188)
-#182 := (not #181)
-#388 := [hypothesis]: #181
-#396 := (or #224 #182)
-#199 := -3::Real
-#200 := (* -3::Real #188)
-#201 := (+ #121 #200)
-#202 := (+ #45 #201)
-#203 := (<= #202 0::Real)
-#204 := (not #203)
-#216 := (+ #43 #137)
-#217 := (<= #216 0::Real)
-#220 := (not #217)
-#241 := (* -3::Real #230)
-#242 := (+ #121 #241)
-#243 := (+ #45 #242)
-#244 := (<= #243 0::Real)
-#263 := (or #244 #203 #220)
-#268 := (not #263)
-#64 := (<= #43 #57)
-#65 := (implies #64 false)
-#55 := (- #45 #54)
-#51 := 3::Real
-#58 := (- #57 #54)
-#60 := (- #58)
-#59 := (< #58 0::Real)
-#61 := (if #59 #60 #58)
-#62 := (* #61 3::Real)
-#63 := (< #62 #55)
-#66 := (implies #63 #65)
-#46 := (- #43 #45)
-#49 := (- #46)
-#48 := (< #46 0::Real)
-#50 := (if #48 #49 #46)
-#52 := (* #50 3::Real)
-#56 := (< #52 #55)
-#67 := (implies #56 #66)
-#68 := (not #67)
-#271 := (iff #68 #268)
-#157 := (not #64)
-#122 := (+ #45 #121)
-#131 := (< #128 0::Real)
-#143 := (if #131 #138 #128)
-#149 := (* 3::Real #143)
-#154 := (< #149 #122)
-#163 := (not #154)
-#164 := (or #163 #157)
-#98 := (< #95 0::Real)
-#110 := (if #98 #105 #95)
-#116 := (* 3::Real #110)
-#125 := (< #116 #122)
-#172 := (not #125)
-#173 := (or #172 #164)
-#178 := (not #173)
-#269 := (iff #178 #268)
-#266 := (iff #173 #263)
-#257 := (or #203 #220)
-#260 := (or #244 #257)
-#264 := (iff #260 #263)
-#265 := [rewrite]: #264
-#261 := (iff #173 #260)
-#258 := (iff #164 #257)
-#221 := (iff #157 #220)
-#218 := (iff #64 #217)
-#219 := [rewrite]: #218
-#222 := [monotonicity #219]: #221
-#214 := (iff #163 #203)
-#209 := (not #204)
-#212 := (iff #209 #203)
-#213 := [rewrite]: #212
-#210 := (iff #163 #209)
-#207 := (iff #154 #204)
-#193 := (* 3::Real #188)
-#196 := (< #193 #122)
-#205 := (iff #196 #204)
-#206 := [rewrite]: #205
-#197 := (iff #154 #196)
-#194 := (= #149 #193)
-#191 := (= #143 #188)
-#185 := (if #182 #138 #128)
-#189 := (= #185 #188)
-#190 := [rewrite]: #189
-#186 := (= #143 #185)
-#183 := (iff #131 #182)
-#184 := [rewrite]: #183
-#187 := [monotonicity #184]: #186
-#192 := [trans #187 #190]: #191
-#195 := [monotonicity #192]: #194
-#198 := [monotonicity #195]: #197
-#208 := [trans #198 #206]: #207
-#211 := [monotonicity #208]: #210
-#215 := [trans #211 #213]: #214
-#259 := [monotonicity #215 #222]: #258
-#255 := (iff #172 #244)
-#245 := (not #244)
-#250 := (not #245)
-#253 := (iff #250 #244)
-#254 := [rewrite]: #253
-#251 := (iff #172 #250)
-#248 := (iff #125 #245)
-#235 := (* 3::Real #230)
-#238 := (< #235 #122)
-#246 := (iff #238 #245)
-#247 := [rewrite]: #246
-#239 := (iff #125 #238)
-#236 := (= #116 #235)
-#233 := (= #110 #230)
-#227 := (if #224 #105 #95)
-#231 := (= #227 #230)
-#232 := [rewrite]: #231
-#228 := (= #110 #227)
-#225 := (iff #98 #224)
-#226 := [rewrite]: #225
-#229 := [monotonicity #226]: #228
-#234 := [trans #229 #232]: #233
-#237 := [monotonicity #234]: #236
-#240 := [monotonicity #237]: #239
-#249 := [trans #240 #247]: #248
-#252 := [monotonicity #249]: #251
-#256 := [trans #252 #254]: #255
-#262 := [monotonicity #256 #259]: #261
-#267 := [trans #262 #265]: #266
-#270 := [monotonicity #267]: #269
-#179 := (iff #68 #178)
-#176 := (iff #67 #173)
-#169 := (implies #125 #164)
-#174 := (iff #169 #173)
-#175 := [rewrite]: #174
-#170 := (iff #67 #169)
-#167 := (iff #66 #164)
-#160 := (implies #154 #157)
-#165 := (iff #160 #164)
-#166 := [rewrite]: #165
-#161 := (iff #66 #160)
-#158 := (iff #65 #157)
-#159 := [rewrite]: #158
-#155 := (iff #63 #154)
-#123 := (= #55 #122)
-#124 := [rewrite]: #123
-#152 := (= #62 #149)
-#146 := (* #143 3::Real)
-#150 := (= #146 #149)
-#151 := [rewrite]: #150
-#147 := (= #62 #146)
-#144 := (= #61 #143)
-#129 := (= #58 #128)
-#130 := [rewrite]: #129
-#141 := (= #60 #138)
-#134 := (- #128)
-#139 := (= #134 #138)
-#140 := [rewrite]: #139
-#135 := (= #60 #134)
-#136 := [monotonicity #130]: #135
-#142 := [trans #136 #140]: #141
-#132 := (iff #59 #131)
-#133 := [monotonicity #130]: #132
-#145 := [monotonicity #133 #142 #130]: #144
-#148 := [monotonicity #145]: #147
-#153 := [trans #148 #151]: #152
-#156 := [monotonicity #153 #124]: #155
-#162 := [monotonicity #156 #159]: #161
-#168 := [trans #162 #166]: #167
-#126 := (iff #56 #125)
-#119 := (= #52 #116)
-#113 := (* #110 3::Real)
-#117 := (= #113 #116)
-#118 := [rewrite]: #117
-#114 := (= #52 #113)
-#111 := (= #50 #110)
-#96 := (= #46 #95)
-#97 := [rewrite]: #96
-#108 := (= #49 #105)
-#101 := (- #95)
-#106 := (= #101 #105)
-#107 := [rewrite]: #106
-#102 := (= #49 #101)
-#103 := [monotonicity #97]: #102
-#109 := [trans #103 #107]: #108
-#99 := (iff #48 #98)
-#100 := [monotonicity #97]: #99
-#112 := [monotonicity #100 #109 #97]: #111
-#115 := [monotonicity #112]: #114
-#120 := [trans #115 #118]: #119
-#127 := [monotonicity #120 #124]: #126
-#171 := [monotonicity #127 #168]: #170
-#177 := [trans #171 #175]: #176
-#180 := [monotonicity #177]: #179
-#272 := [trans #180 #270]: #271
-#92 := [asserted]: #68
-#273 := [mp #92 #272]: #268
-#275 := [not-or-elim #273]: #204
-#381 := (+ #128 #380)
-#382 := (<= #381 0::Real)
-#374 := (= #128 #188)
-#376 := (or #182 #374)
-#377 := [def-axiom]: #376
-#389 := [unit-resolution #377 #388]: #374
-#390 := (not #374)
-#391 := (or #390 #382)
-#392 := [th-lemma arith triangle-eq]: #391
-#393 := [unit-resolution #392 #389]: #382
-#394 := [hypothesis]: #223
-#276 := [not-or-elim #273]: #217
-#395 := [th-lemma arith farkas 1/2 -1/2 3/2 -1/2 1 #276 #394 #393 #275 #388]: false
-#397 := [lemma #395]: #396
-#398 := [unit-resolution #397 #388]: #224
-#372 := (or #223 #361)
-#373 := [def-axiom]: #372
-#399 := [unit-resolution #373 #398]: #361
-#400 := (not #361)
-#401 := (or #400 #386)
-#402 := [th-lemma arith triangle-eq]: #401
-#403 := [unit-resolution #402 #399]: #386
-#274 := [not-or-elim #273]: #245
-#404 := [th-lemma arith farkas 1/2 -1/3 1/2 -1/6 1/2 1 #398 #274 #393 #275 #276 #403]: false
-#405 := [lemma #404]: #182
-#378 := (or #181 #375)
-#379 := [def-axiom]: #378
-#408 := [unit-resolution #379 #405]: #375
-#409 := (not #375)
-#410 := (or #409 #387)
-#411 := [th-lemma arith triangle-eq]: #410
-#412 := [unit-resolution #411 #408]: #387
-#413 := (not #387)
-#414 := (or #224 #413 #220 #203 #181)
-#415 := [th-lemma arith assign-bounds 3 1 1 4]: #414
-#416 := [unit-resolution #415 #405 #275 #276 #412]: #224
-#417 := [unit-resolution #373 #416]: #361
-#418 := [unit-resolution #402 #417]: #386
-[th-lemma arith farkas 2 1 2/3 3 1/3 1 #412 #276 #275 #405 #274 #418]: false
-unsat
-de944ddeb0dd396c6967b17dba5c16a293e6c02d 344 0
-#2 := false
-#10 := 0::Real
-decl ?v3!0 :: Real
-#226 := ?v3!0
-decl ?v0!3 :: Real
-#225 := ?v0!3
-#47 := -1::Real
-#233 := (* -1::Real ?v0!3)
-#234 := (+ #233 ?v3!0)
-#230 := (* -1::Real ?v3!0)
-#231 := (+ ?v0!3 #230)
-#232 := (>= #231 0::Real)
-#235 := (if #232 #231 #234)
-#236 := (* -1::Real #235)
-#393 := (+ #234 #236)
-#394 := (<= #393 0::Real)
-#377 := (= #234 #235)
-#378 := (not #232)
-decl ?v2!1 :: Real
-#227 := ?v2!1
-decl ?v1!2 :: Real
-#224 := ?v1!2
-#240 := (* -1::Real ?v1!2)
-#262 := (+ #240 ?v2!1)
-#243 := (* -1::Real ?v2!1)
-#268 := (+ ?v1!2 #243)
-#269 := (>= #268 0::Real)
-#276 := (if #269 #268 #262)
-#279 := (* -1::Real #276)
-#392 := (+ #262 #279)
-#395 := (<= #392 0::Real)
-#384 := (= #262 #276)
-#385 := (not #269)
-#396 := [hypothesis]: #269
-#404 := (or #378 #385)
-#76 := -1/3::Real
-#229 := (* -1/3::Real ?v2!1)
-#282 := (+ #229 #279)
-#74 := 1/3::Real
-#228 := (* 1/3::Real ?v3!0)
-#285 := (+ #228 #282)
-#288 := (<= #285 0::Real)
-#313 := (not #288)
-#297 := (+ ?v1!2 #233)
-#298 := (>= #297 0::Real)
-#303 := (not #298)
-#237 := (+ #229 #236)
-#238 := (+ #228 #237)
-#239 := (<= #238 0::Real)
-#306 := (or #239 #288 #303)
-#309 := (not #306)
-#250 := (+ ?v0!3 #240)
-#251 := (<= #250 0::Real)
-#252 := (not #251)
-#241 := (+ ?v2!1 #240)
-#244 := (+ #243 ?v1!2)
-#242 := (<= #241 0::Real)
-#245 := (if #242 #244 #241)
-#246 := (* -1::Real #245)
-#247 := (+ #229 #246)
-#248 := (+ #228 #247)
-#249 := (<= #248 0::Real)
-#253 := (or #239 #249 #252)
-#254 := (not #253)
-#310 := (iff #254 #309)
-#307 := (iff #253 #306)
-#304 := (iff #252 #303)
-#301 := (iff #251 #298)
-#291 := (+ #240 ?v0!3)
-#294 := (<= #291 0::Real)
-#299 := (iff #294 #298)
-#300 := [rewrite]: #299
-#295 := (iff #251 #294)
-#292 := (= #250 #291)
-#293 := [rewrite]: #292
-#296 := [monotonicity #293]: #295
-#302 := [trans #296 #300]: #301
-#305 := [monotonicity #302]: #304
-#289 := (iff #249 #288)
-#286 := (= #248 #285)
-#283 := (= #247 #282)
-#280 := (= #246 #279)
-#277 := (= #245 #276)
-#263 := (= #241 #262)
-#264 := [rewrite]: #263
-#274 := (= #244 #268)
-#275 := [rewrite]: #274
-#272 := (iff #242 #269)
-#265 := (<= #262 0::Real)
-#270 := (iff #265 #269)
-#271 := [rewrite]: #270
-#266 := (iff #242 #265)
-#267 := [monotonicity #264]: #266
-#273 := [trans #267 #271]: #272
-#278 := [monotonicity #273 #275 #264]: #277
-#281 := [monotonicity #278]: #280
-#284 := [monotonicity #281]: #283
-#287 := [monotonicity #284]: #286
-#290 := [monotonicity #287]: #289
-#308 := [monotonicity #290 #305]: #307
-#311 := [monotonicity #308]: #310
-#19 := (:var 2 Real)
-#95 := (* -1::Real #19)
-#7 := (:var 3 Real)
-#165 := (+ #7 #95)
-#166 := (<= #165 0::Real)
-#169 := (not #166)
-#14 := (:var 1 Real)
-#96 := (+ #14 #95)
-#67 := (* -1::Real #14)
-#86 := (+ #67 #19)
-#134 := (<= #96 0::Real)
-#141 := (if #134 #86 #96)
-#149 := (* -1::Real #141)
-#77 := (* -1/3::Real #14)
-#150 := (+ #77 #149)
-#8 := (:var 0 Real)
-#75 := (* 1/3::Real #8)
-#151 := (+ #75 #150)
-#152 := (<= #151 0::Real)
-#58 := (* -1::Real #7)
-#59 := (+ #58 #8)
-#48 := (* -1::Real #8)
-#49 := (+ #7 #48)
-#172 := (>= #49 0::Real)
-#179 := (if #172 #49 #59)
-#187 := (* -1::Real #179)
-#188 := (+ #77 #187)
-#189 := (+ #75 #188)
-#190 := (<= #189 0::Real)
-#209 := (or #190 #152 #169)
-#214 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #209)
-#217 := (not #214)
-#255 := (~ #217 #254)
-#256 := [sk]: #255
-#25 := (<= #7 #19)
-#26 := (implies #25 false)
-#16 := 3::Real
-#15 := (- #8 #14)
-#17 := (/ #15 3::Real)
-#20 := (- #19 #14)
-#22 := (- #20)
-#21 := (< #20 0::Real)
-#23 := (if #21 #22 #20)
-#24 := (< #23 #17)
-#27 := (implies #24 #26)
-#9 := (- #7 #8)
-#12 := (- #9)
-#11 := (< #9 0::Real)
-#13 := (if #11 #12 #9)
-#18 := (< #13 #17)
-#28 := (implies #18 #27)
-#29 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #28)
-#30 := (not #29)
-#220 := (iff #30 #217)
-#107 := (not #25)
-#78 := (+ #75 #77)
-#89 := (< #86 0::Real)
-#101 := (if #89 #96 #86)
-#104 := (< #101 #78)
-#113 := (not #104)
-#114 := (or #113 #107)
-#52 := (< #49 0::Real)
-#64 := (if #52 #59 #49)
-#83 := (< #64 #78)
-#122 := (not #83)
-#123 := (or #122 #114)
-#128 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #123)
-#131 := (not #128)
-#218 := (iff #131 #217)
-#215 := (iff #128 #214)
-#212 := (iff #123 #209)
-#203 := (or #152 #169)
-#206 := (or #190 #203)
-#210 := (iff #206 #209)
-#211 := [rewrite]: #210
-#207 := (iff #123 #206)
-#204 := (iff #114 #203)
-#170 := (iff #107 #169)
-#167 := (iff #25 #166)
-#168 := [rewrite]: #167
-#171 := [monotonicity #168]: #170
-#163 := (iff #113 #152)
-#153 := (not #152)
-#158 := (not #153)
-#161 := (iff #158 #152)
-#162 := [rewrite]: #161
-#159 := (iff #113 #158)
-#156 := (iff #104 #153)
-#146 := (< #141 #78)
-#154 := (iff #146 #153)
-#155 := [rewrite]: #154
-#147 := (iff #104 #146)
-#144 := (= #101 #141)
-#135 := (not #134)
-#138 := (if #135 #96 #86)
-#142 := (= #138 #141)
-#143 := [rewrite]: #142
-#139 := (= #101 #138)
-#136 := (iff #89 #135)
-#137 := [rewrite]: #136
-#140 := [monotonicity #137]: #139
-#145 := [trans #140 #143]: #144
-#148 := [monotonicity #145]: #147
-#157 := [trans #148 #155]: #156
-#160 := [monotonicity #157]: #159
-#164 := [trans #160 #162]: #163
-#205 := [monotonicity #164 #171]: #204
-#201 := (iff #122 #190)
-#191 := (not #190)
-#196 := (not #191)
-#199 := (iff #196 #190)
-#200 := [rewrite]: #199
-#197 := (iff #122 #196)
-#194 := (iff #83 #191)
-#184 := (< #179 #78)
-#192 := (iff #184 #191)
-#193 := [rewrite]: #192
-#185 := (iff #83 #184)
-#182 := (= #64 #179)
-#173 := (not #172)
-#176 := (if #173 #59 #49)
-#180 := (= #176 #179)
-#181 := [rewrite]: #180
-#177 := (= #64 #176)
-#174 := (iff #52 #173)
-#175 := [rewrite]: #174
-#178 := [monotonicity #175]: #177
-#183 := [trans #178 #181]: #182
-#186 := [monotonicity #183]: #185
-#195 := [trans #186 #193]: #194
-#198 := [monotonicity #195]: #197
-#202 := [trans #198 #200]: #201
-#208 := [monotonicity #202 #205]: #207
-#213 := [trans #208 #211]: #212
-#216 := [quant-intro #213]: #215
-#219 := [monotonicity #216]: #218
-#132 := (iff #30 #131)
-#129 := (iff #29 #128)
-#126 := (iff #28 #123)
-#119 := (implies #83 #114)
-#124 := (iff #119 #123)
-#125 := [rewrite]: #124
-#120 := (iff #28 #119)
-#117 := (iff #27 #114)
-#110 := (implies #104 #107)
-#115 := (iff #110 #114)
-#116 := [rewrite]: #115
-#111 := (iff #27 #110)
-#108 := (iff #26 #107)
-#109 := [rewrite]: #108
-#105 := (iff #24 #104)
-#81 := (= #17 #78)
-#68 := (+ #8 #67)
-#71 := (/ #68 3::Real)
-#79 := (= #71 #78)
-#80 := [rewrite]: #79
-#72 := (= #17 #71)
-#69 := (= #15 #68)
-#70 := [rewrite]: #69
-#73 := [monotonicity #70]: #72
-#82 := [trans #73 #80]: #81
-#102 := (= #23 #101)
-#87 := (= #20 #86)
-#88 := [rewrite]: #87
-#99 := (= #22 #96)
-#92 := (- #86)
-#97 := (= #92 #96)
-#98 := [rewrite]: #97
-#93 := (= #22 #92)
-#94 := [monotonicity #88]: #93
-#100 := [trans #94 #98]: #99
-#90 := (iff #21 #89)
-#91 := [monotonicity #88]: #90
-#103 := [monotonicity #91 #100 #88]: #102
-#106 := [monotonicity #103 #82]: #105
-#112 := [monotonicity #106 #109]: #111
-#118 := [trans #112 #116]: #117
-#84 := (iff #18 #83)
-#65 := (= #13 #64)
-#50 := (= #9 #49)
-#51 := [rewrite]: #50
-#62 := (= #12 #59)
-#55 := (- #49)
-#60 := (= #55 #59)
-#61 := [rewrite]: #60
-#56 := (= #12 #55)
-#57 := [monotonicity #51]: #56
-#63 := [trans #57 #61]: #62
-#53 := (iff #11 #52)
-#54 := [monotonicity #51]: #53
-#66 := [monotonicity #54 #63 #51]: #65
-#85 := [monotonicity #66 #82]: #84
-#121 := [monotonicity #85 #118]: #120
-#127 := [trans #121 #125]: #126
-#130 := [quant-intro #127]: #129
-#133 := [monotonicity #130]: #132
-#221 := [trans #133 #219]: #220
-#46 := [asserted]: #30
-#222 := [mp #46 #221]: #217
-#259 := [mp~ #222 #256]: #254
-#260 := [mp #259 #311]: #309
-#314 := [not-or-elim #260]: #313
-#390 := (+ #268 #279)
-#391 := (<= #390 0::Real)
-#383 := (= #268 #276)
-#386 := (or #385 #383)
-#387 := [def-axiom]: #386
-#397 := [unit-resolution #387 #396]: #383
-#398 := (not #383)
-#399 := (or #398 #391)
-#400 := [th-lemma arith triangle-eq]: #399
-#401 := [unit-resolution #400 #397]: #391
-#402 := [hypothesis]: #232
-#315 := [not-or-elim #260]: #298
-#403 := [th-lemma arith farkas 1/2 1/2 3/2 3/2 1 #315 #402 #401 #314 #396]: false
-#405 := [lemma #403]: #404
-#406 := [unit-resolution #405 #396]: #378
-#261 := (not #239)
-#312 := [not-or-elim #260]: #261
-#381 := (or #232 #377)
-#382 := [def-axiom]: #381
-#407 := [unit-resolution #382 #406]: #377
-#408 := (not #377)
-#409 := (or #408 #394)
-#410 := [th-lemma arith triangle-eq]: #409
-#411 := [unit-resolution #410 #407]: #394
-#412 := [th-lemma arith farkas 2 2 1 1 1 1 #411 #312 #401 #314 #315 #406]: false
-#413 := [lemma #412]: #385
-#388 := (or #269 #384)
-#389 := [def-axiom]: #388
-#416 := [unit-resolution #389 #413]: #384
-#417 := (not #384)
-#418 := (or #417 #395)
-#419 := [th-lemma arith triangle-eq]: #418
-#420 := [unit-resolution #419 #416]: #395
-#421 := (not #395)
-#422 := (or #378 #421 #303 #288 #269)
-#423 := [th-lemma arith assign-bounds 3 1 3 4]: #422
-#424 := [unit-resolution #423 #413 #314 #315 #420]: #378
-#425 := [unit-resolution #382 #424]: #377
-#426 := [unit-resolution #410 #425]: #394
-[th-lemma arith farkas 2 1 2 3 1 1 #420 #315 #314 #413 #312 #426]: false
-unsat
-30337497c57dec04cb45940d60f17c3a08d5b406 59 0
-#2 := false
-#41 := 0::Real
-decl f12 :: (-> S5 Real)
-decl f13 :: (-> S4 S4 S5)
-decl f14 :: (-> S6 S3 S4)
-decl f4 :: S3
-#7 := f4
-decl f15 :: S6
-#36 := f15
-#38 := (f14 f15 f4)
-decl f10 :: S3
-#24 := f10
-#37 := (f14 f15 f10)
-#39 := (f13 #37 #38)
-#40 := (f12 #39)
-#253 := (>= #40 0::Real)
-#255 := (not #253)
-#49 := (= #40 0::Real)
-#50 := (not #49)
-#134 := [asserted]: #50
-#261 := (or #49 #255)
-#42 := (<= #40 0::Real)
-#132 := [asserted]: #42
-#254 := (not #42)
-#259 := (or #49 #254 #255)
-#260 := [th-lemma arith triangle-eq]: #259
-#262 := [unit-resolution #260 #132]: #261
-#263 := [unit-resolution #262 #134]: #255
-#44 := (:var 0 S4)
-#43 := (:var 1 S4)
-#45 := (f13 #43 #44)
-#246 := (pattern #45)
-#46 := (f12 #45)
-#137 := (>= #46 0::Real)
-#247 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #246) #137)
-#139 := (forall (vars (?v0 S4) (?v1 S4)) #137)
-#250 := (iff #139 #247)
-#248 := (iff #137 #137)
-#249 := [refl]: #248
-#251 := [quant-intro #249]: #250
-#155 := (~ #139 #139)
-#143 := (~ #137 #137)
-#144 := [refl]: #143
-#156 := [nnf-pos #144]: #155
-#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
-#142 := [mp #133 #141]: #139
-#157 := [mp~ #142 #156]: #139
-#252 := [mp #157 #251]: #247
-#256 := (not #247)
-#257 := (or #256 #253)
-#258 := [quant-inst #37 #38]: #257
-[unit-resolution #258 #252 #263]: false
-unsat
-1da91241d9cef93f8c738b96ec6815cac1c1c9f8 220 0
-#2 := false
-#32 := 0::Real
-decl f3 :: (-> S2 S3 Real)
-decl f5 :: S3
-#8 := f5
-decl f12 :: S2
-#24 := f12
-#35 := (f3 f12 f5)
-#103 := -1::Real
-#311 := (* -1::Real #35)
-decl f6 :: S2
-#10 := f6
-#11 := (f3 f6 f5)
-#338 := (+ #11 #311)
-#339 := (>= #338 0::Real)
-#344 := (not #339)
-decl f4 :: S2
-#7 := f4
-#9 := (f3 f4 f5)
-#312 := (+ #9 #311)
-#313 := (<= #312 0::Real)
-#314 := (not #313)
-#347 := (or #314 #344)
-#350 := (not #347)
-#20 := (:var 0 S3)
-#27 := (f3 f6 #20)
-#282 := (pattern #27)
-#25 := (f3 f12 #20)
-#281 := (pattern #25)
-#23 := (f3 f4 #20)
-#280 := (pattern #23)
-decl f7 :: (-> S4 S3 Int)
-decl f8 :: S4
-#13 := f8
-#21 := (f7 f8 #20)
-#279 := (pattern #21)
-#109 := (* -1::Real #27)
-#110 := (+ #25 #109)
-#111 := (<= #110 0::Real)
-#205 := (not #111)
-#104 := (* -1::Real #25)
-#105 := (+ #23 #104)
-#106 := (<= #105 0::Real)
-#204 := (not #106)
-#206 := (or #204 #205)
-#207 := (not #206)
-#42 := 0::Int
-#76 := -1::Int
-#90 := (* -1::Int #21)
-decl f9 :: (-> S5 S6 S3)
-decl f11 :: S6
-#16 := f11
-decl f10 :: S5
-#15 := f10
-#17 := (f9 f10 f11)
-#18 := (f7 f8 #17)
-#91 := (+ #18 #90)
-#92 := (<= #91 0::Int)
-#210 := (or #92 #207)
-#283 := (forall (vars (?v0 S3)) (:pat #279 #280 #281 #282) #210)
-#213 := (forall (vars (?v0 S3)) #210)
-#286 := (iff #213 #283)
-#284 := (iff #210 #210)
-#285 := [refl]: #284
-#287 := [quant-intro #285]: #286
-#114 := (and #106 #111)
-#117 := (or #92 #114)
-#120 := (forall (vars (?v0 S3)) #117)
-#214 := (iff #120 #213)
-#211 := (iff #117 #210)
-#208 := (iff #114 #207)
-#209 := [rewrite]: #208
-#212 := [monotonicity #209]: #211
-#215 := [quant-intro #212]: #214
-#198 := (~ #120 #120)
-#200 := (~ #117 #117)
-#201 := [refl]: #200
-#199 := [nnf-pos #201]: #198
-#28 := (<= #25 #27)
-#26 := (<= #23 #25)
-#29 := (and #26 #28)
-#22 := (< #21 #18)
-#30 := (implies #22 #29)
-#31 := (forall (vars (?v0 S3)) #30)
-#123 := (iff #31 #120)
-#75 := (not #22)
-#84 := (or #75 #29)
-#87 := (forall (vars (?v0 S3)) #84)
-#121 := (iff #87 #120)
-#118 := (iff #84 #117)
-#115 := (iff #29 #114)
-#112 := (iff #28 #111)
-#113 := [rewrite]: #112
-#107 := (iff #26 #106)
-#108 := [rewrite]: #107
-#116 := [monotonicity #108 #113]: #115
-#101 := (iff #75 #92)
-#93 := (not #92)
-#96 := (not #93)
-#99 := (iff #96 #92)
-#100 := [rewrite]: #99
-#97 := (iff #75 #96)
-#94 := (iff #22 #93)
-#95 := [rewrite]: #94
-#98 := [monotonicity #95]: #97
-#102 := [trans #98 #100]: #101
-#119 := [monotonicity #102 #116]: #118
-#122 := [quant-intro #119]: #121
-#88 := (iff #31 #87)
-#85 := (iff #30 #84)
-#86 := [rewrite]: #85
-#89 := [quant-intro #86]: #88
-#124 := [trans #89 #122]: #123
-#74 := [asserted]: #31
-#125 := [mp #74 #124]: #120
-#196 := [mp~ #125 #199]: #120
-#216 := [mp #196 #215]: #213
-#288 := [mp #216 #287]: #283
-#79 := (* -1::Int #18)
-#14 := (f7 f8 f5)
-#80 := (+ #14 #79)
-#78 := (>= #80 0::Int)
-#77 := (not #78)
-#19 := (< #14 #18)
-#81 := (iff #19 #77)
-#82 := [rewrite]: #81
-#73 := [asserted]: #19
-#83 := [mp #73 #82]: #77
-#356 := (not #283)
-#357 := (or #356 #78 #350)
-#315 := (* -1::Real #11)
-#316 := (+ #35 #315)
-#317 := (<= #316 0::Real)
-#318 := (not #317)
-#319 := (or #314 #318)
-#320 := (not #319)
-#308 := (* -1::Int #14)
-#309 := (+ #18 #308)
-#310 := (<= #309 0::Int)
-#321 := (or #310 #320)
-#358 := (or #356 #321)
-#365 := (iff #358 #357)
-#353 := (or #78 #350)
-#360 := (or #356 #353)
-#363 := (iff #360 #357)
-#364 := [rewrite]: #363
-#361 := (iff #358 #360)
-#354 := (iff #321 #353)
-#351 := (iff #320 #350)
-#348 := (iff #319 #347)
-#345 := (iff #318 #344)
-#342 := (iff #317 #339)
-#332 := (+ #315 #35)
-#335 := (<= #332 0::Real)
-#340 := (iff #335 #339)
-#341 := [rewrite]: #340
-#336 := (iff #317 #335)
-#333 := (= #316 #332)
-#334 := [rewrite]: #333
-#337 := [monotonicity #334]: #336
-#343 := [trans #337 #341]: #342
-#346 := [monotonicity #343]: #345
-#349 := [monotonicity #346]: #348
-#352 := [monotonicity #349]: #351
-#330 := (iff #310 #78)
-#322 := (+ #308 #18)
-#325 := (<= #322 0::Int)
-#328 := (iff #325 #78)
-#329 := [rewrite]: #328
-#326 := (iff #310 #325)
-#323 := (= #309 #322)
-#324 := [rewrite]: #323
-#327 := [monotonicity #324]: #326
-#331 := [trans #327 #329]: #330
-#355 := [monotonicity #331 #352]: #354
-#362 := [monotonicity #355]: #361
-#366 := [trans #362 #364]: #365
-#359 := [quant-inst #8]: #358
-#367 := [mp #359 #366]: #357
-#435 := [unit-resolution #367 #83 #288]: #350
-#370 := (or #347 #339)
-#371 := [def-axiom]: #370
-#436 := [unit-resolution #371 #435]: #339
-#419 := (>= #312 0::Real)
-#457 := (not #419)
-#418 := (= #9 #35)
-#452 := (not #418)
-#36 := (= #35 #11)
-#37 := (not #36)
-#453 := (iff #37 #452)
-#450 := (iff #36 #418)
-#448 := (iff #418 #36)
-#443 := (= #11 #35)
-#446 := (iff #443 #36)
-#447 := [commutativity]: #446
-#444 := (iff #418 #443)
-#12 := (= #9 #11)
-#72 := [asserted]: #12
-#445 := [monotonicity #72]: #444
-#449 := [trans #445 #447]: #448
-#451 := [symm #449]: #450
-#454 := [monotonicity #451]: #453
-#127 := [asserted]: #37
-#455 := [mp #127 #454]: #452
-#460 := (or #418 #457)
-#368 := (or #347 #313)
-#369 := [def-axiom]: #368
-#456 := [unit-resolution #369 #435]: #313
-#458 := (or #418 #314 #457)
-#459 := [th-lemma arith triangle-eq]: #458
-#461 := [unit-resolution #459 #456]: #460
-#462 := [unit-resolution #461 #455]: #457
-#413 := (+ #9 #315)
-#417 := (>= #413 0::Real)
-#463 := (not #12)
-#464 := (or #463 #417)
-#465 := [th-lemma arith triangle-eq]: #464
-#466 := [unit-resolution #465 #72]: #417
-[th-lemma arith farkas 1 -1 1 #466 #462 #436]: false
-unsat
-6067cf487a9641d94ba72113a6d1147a045ae6d1 350 0
-#2 := false
-#7 := 0::Real
-decl f9 :: (-> S6 S2 Real)
-decl f12 :: S2
-#26 := f12
-decl f10 :: S6
-#18 := f10
-#33 := (f9 f10 f12)
-decl f13 :: S6
-#30 := f13
-#31 := (f9 f13 f12)
-#101 := -1::Real
-#137 := (* -1::Real #31)
-#138 := (+ #137 #33)
-decl f3 :: Real
-#8 := f3
-#193 := (* -1::Real #33)
-#194 := (+ #31 #193)
-#195 := (+ f3 #194)
-#196 := (<= #195 0::Real)
-#199 := (if #196 f3 #138)
-#558 := (* -1::Real #199)
-#559 := (+ f3 #558)
-#566 := (<= #559 0::Real)
-#573 := (not #566)
-#128 := 1/2::Real
-#202 := (* 1/2::Real #199)
-#460 := (<= #202 0::Real)
-#211 := (= #202 0::Real)
-#216 := (not #211)
-#130 := (* 1/2::Real #33)
-#190 := (+ #137 #130)
-decl f11 :: S6
-#20 := f11
-#29 := (f9 f11 f12)
-#129 := (* 1/2::Real #29)
-#191 := (+ #129 #190)
-#188 := (>= #191 0::Real)
-#186 := (not #188)
-#230 := (<= #194 0::Real)
-#226 := (+ #29 #137)
-#227 := (<= #226 0::Real)
-#233 := (and #227 #230)
-#55 := 0::Int
-decl f4 :: (-> S3 S2 Int)
-decl f5 :: S3
-#10 := f5
-#27 := (f4 f5 f12)
-#94 := -1::Int
-#118 := (* -1::Int #27)
-decl f6 :: (-> S4 S5 S2)
-decl f8 :: S5
-#14 := f8
-decl f7 :: S4
-#13 := f7
-#15 := (f6 f7 f8)
-#16 := (f4 f5 #15)
-#119 := (+ #16 #118)
-#120 := (<= #119 0::Int)
-#236 := (or #120 #233)
-#239 := (not #236)
-#248 := (or #239 #186 #216)
-#253 := (not #248)
-#38 := 2::Real
-#41 := (- #33 #31)
-#42 := (<= f3 #41)
-#43 := (if #42 f3 #41)
-#44 := (/ #43 2::Real)
-#45 := (+ #31 #44)
-#46 := (= #45 #31)
-#47 := (not #46)
-#37 := (+ #29 #33)
-#39 := (/ #37 2::Real)
-#40 := (<= #31 #39)
-#48 := (implies #40 #47)
-#34 := (<= #31 #33)
-#32 := (<= #29 #31)
-#35 := (and #32 #34)
-#28 := (< #27 #16)
-#36 := (implies #28 #35)
-#49 := (implies #36 #48)
-#50 := (not #49)
-#256 := (iff #50 #253)
-#141 := (<= f3 #138)
-#144 := (if #141 f3 #138)
-#150 := (* 1/2::Real #144)
-#155 := (+ #31 #150)
-#158 := (= #155 #31)
-#161 := (not #158)
-#131 := (+ #129 #130)
-#134 := (<= #31 #131)
-#167 := (not #134)
-#168 := (or #167 #161)
-#117 := (not #28)
-#125 := (or #117 #35)
-#176 := (not #125)
-#177 := (or #176 #168)
-#182 := (not #177)
-#254 := (iff #182 #253)
-#251 := (iff #177 #248)
-#242 := (or #186 #216)
-#245 := (or #239 #242)
-#249 := (iff #245 #248)
-#250 := [rewrite]: #249
-#246 := (iff #177 #245)
-#243 := (iff #168 #242)
-#217 := (iff #161 #216)
-#214 := (iff #158 #211)
-#205 := (+ #31 #202)
-#208 := (= #205 #31)
-#212 := (iff #208 #211)
-#213 := [rewrite]: #212
-#209 := (iff #158 #208)
-#206 := (= #155 #205)
-#203 := (= #150 #202)
-#200 := (= #144 #199)
-#197 := (iff #141 #196)
-#198 := [rewrite]: #197
-#201 := [monotonicity #198]: #200
-#204 := [monotonicity #201]: #203
-#207 := [monotonicity #204]: #206
-#210 := [monotonicity #207]: #209
-#215 := [trans #210 #213]: #214
-#218 := [monotonicity #215]: #217
-#189 := (iff #167 #186)
-#185 := (iff #134 #188)
-#187 := [rewrite]: #185
-#192 := [monotonicity #187]: #189
-#244 := [monotonicity #192 #218]: #243
-#240 := (iff #176 #239)
-#237 := (iff #125 #236)
-#234 := (iff #35 #233)
-#231 := (iff #34 #230)
-#232 := [rewrite]: #231
-#228 := (iff #32 #227)
-#229 := [rewrite]: #228
-#235 := [monotonicity #229 #232]: #234
-#224 := (iff #117 #120)
-#121 := (not #120)
-#219 := (not #121)
-#222 := (iff #219 #120)
-#223 := [rewrite]: #222
-#220 := (iff #117 #219)
-#122 := (iff #28 #121)
-#123 := [rewrite]: #122
-#221 := [monotonicity #123]: #220
-#225 := [trans #221 #223]: #224
-#238 := [monotonicity #225 #235]: #237
-#241 := [monotonicity #238]: #240
-#247 := [monotonicity #241 #244]: #246
-#252 := [trans #247 #250]: #251
-#255 := [monotonicity #252]: #254
-#183 := (iff #50 #182)
-#180 := (iff #49 #177)
-#173 := (implies #125 #168)
-#178 := (iff #173 #177)
-#179 := [rewrite]: #178
-#174 := (iff #49 #173)
-#171 := (iff #48 #168)
-#164 := (implies #134 #161)
-#169 := (iff #164 #168)
-#170 := [rewrite]: #169
-#165 := (iff #48 #164)
-#162 := (iff #47 #161)
-#159 := (iff #46 #158)
-#156 := (= #45 #155)
-#153 := (= #44 #150)
-#147 := (/ #144 2::Real)
-#151 := (= #147 #150)
-#152 := [rewrite]: #151
-#148 := (= #44 #147)
-#145 := (= #43 #144)
-#139 := (= #41 #138)
-#140 := [rewrite]: #139
-#142 := (iff #42 #141)
-#143 := [monotonicity #140]: #142
-#146 := [monotonicity #143 #140]: #145
-#149 := [monotonicity #146]: #148
-#154 := [trans #149 #152]: #153
-#157 := [monotonicity #154]: #156
-#160 := [monotonicity #157]: #159
-#163 := [monotonicity #160]: #162
-#135 := (iff #40 #134)
-#132 := (= #39 #131)
-#133 := [rewrite]: #132
-#136 := [monotonicity #133]: #135
-#166 := [monotonicity #136 #163]: #165
-#172 := [trans #166 #170]: #171
-#126 := (iff #36 #125)
-#127 := [rewrite]: #126
-#175 := [monotonicity #127 #172]: #174
-#181 := [trans #175 #179]: #180
-#184 := [monotonicity #181]: #183
-#257 := [trans #184 #255]: #256
-#93 := [asserted]: #50
-#258 := [mp #93 #257]: #253
-#261 := [not-or-elim #258]: #211
-#568 := (or #216 #460)
-#569 := [th-lemma arith triangle-eq]: #568
-#570 := [unit-resolution #569 #261]: #460
-#571 := [hypothesis]: #566
-#88 := (<= f3 0::Real)
-#89 := (not #88)
-#9 := (< 0::Real f3)
-#90 := (iff #9 #89)
-#91 := [rewrite]: #90
-#85 := [asserted]: #9
-#92 := [mp #85 #91]: #89
-#572 := [th-lemma arith farkas -1/2 1/2 1 #92 #571 #570]: false
-#574 := [lemma #572]: #573
-#453 := (= f3 #199)
-#454 := (= #138 #199)
-#583 := (not #454)
-#567 := (+ #138 #558)
-#575 := (<= #567 0::Real)
-#580 := (not #575)
-#515 := (+ #29 #193)
-#516 := (>= #515 0::Real)
-#521 := (not #516)
-#87 := [asserted]: #28
-#124 := [mp #87 #123]: #121
-#11 := (:var 0 S2)
-#21 := (f9 f11 #11)
-#427 := (pattern #21)
-#19 := (f9 f10 #11)
-#426 := (pattern #19)
-#12 := (f4 f5 #11)
-#425 := (pattern #12)
-#102 := (* -1::Real #21)
-#103 := (+ #19 #102)
-#104 := (<= #103 0::Real)
-#347 := (not #104)
-#97 := (* -1::Int #16)
-#98 := (+ #12 #97)
-#96 := (>= #98 0::Int)
-#348 := (or #96 #347)
-#428 := (forall (vars (?v0 S2)) (:pat #425 #426 #427) #348)
-#359 := (forall (vars (?v0 S2)) #348)
-#431 := (iff #359 #428)
-#429 := (iff #348 #348)
-#430 := [refl]: #429
-#432 := [quant-intro #430]: #431
-#95 := (not #96)
-#107 := (and #95 #104)
-#339 := (not #107)
-#338 := (forall (vars (?v0 S2)) #339)
-#360 := (iff #338 #359)
-#357 := (iff #339 #348)
-#349 := (not #348)
-#352 := (not #349)
-#355 := (iff #352 #348)
-#356 := [rewrite]: #355
-#353 := (iff #339 #352)
-#350 := (iff #107 #349)
-#351 := [rewrite]: #350
-#354 := [monotonicity #351]: #353
-#358 := [trans #354 #356]: #357
-#361 := [quant-intro #358]: #360
-#110 := (exists (vars (?v0 S2)) #107)
-#113 := (not #110)
-#335 := (~ #113 #338)
-#340 := (~ #339 #339)
-#337 := [refl]: #340
-#336 := [nnf-neg #337]: #335
-#22 := (<= #19 #21)
-#17 := (< #12 #16)
-#23 := (and #17 #22)
-#24 := (exists (vars (?v0 S2)) #23)
-#25 := (not #24)
-#114 := (iff #25 #113)
-#111 := (iff #24 #110)
-#108 := (iff #23 #107)
-#105 := (iff #22 #104)
-#106 := [rewrite]: #105
-#99 := (iff #17 #95)
-#100 := [rewrite]: #99
-#109 := [monotonicity #100 #106]: #108
-#112 := [quant-intro #109]: #111
-#115 := [monotonicity #112]: #114
-#86 := [asserted]: #25
-#116 := [mp #86 #115]: #113
-#333 := [mp~ #116 #336]: #338
-#362 := [mp #333 #361]: #359
-#433 := [mp #362 #432]: #428
-#527 := (not #428)
-#528 := (or #527 #120 #521)
-#494 := (* -1::Real #29)
-#495 := (+ #33 #494)
-#496 := (<= #495 0::Real)
-#497 := (not #496)
-#489 := (+ #27 #97)
-#490 := (>= #489 0::Int)
-#498 := (or #490 #497)
-#529 := (or #527 #498)
-#536 := (iff #529 #528)
-#524 := (or #120 #521)
-#531 := (or #527 #524)
-#534 := (iff #531 #528)
-#535 := [rewrite]: #534
-#532 := (iff #529 #531)
-#525 := (iff #498 #524)
-#522 := (iff #497 #521)
-#519 := (iff #496 #516)
-#509 := (+ #494 #33)
-#512 := (<= #509 0::Real)
-#517 := (iff #512 #516)
-#518 := [rewrite]: #517
-#513 := (iff #496 #512)
-#510 := (= #495 #509)
-#511 := [rewrite]: #510
-#514 := [monotonicity #511]: #513
-#520 := [trans #514 #518]: #519
-#523 := [monotonicity #520]: #522
-#507 := (iff #490 #120)
-#499 := (+ #97 #27)
-#502 := (>= #499 0::Int)
-#505 := (iff #502 #120)
-#506 := [rewrite]: #505
-#503 := (iff #490 #502)
-#500 := (= #489 #499)
-#501 := [rewrite]: #500
-#504 := [monotonicity #501]: #503
-#508 := [trans #504 #506]: #507
-#526 := [monotonicity #508 #523]: #525
-#533 := [monotonicity #526]: #532
-#537 := [trans #533 #535]: #536
-#530 := [quant-inst #26]: #529
-#538 := [mp #530 #537]: #528
-#577 := [unit-resolution #538 #433 #124]: #521
-#260 := [not-or-elim #258]: #188
-#578 := [hypothesis]: #575
-#579 := [th-lemma arith farkas 1/2 -1/2 1/4 1 #578 #260 #577 #570]: false
-#581 := [lemma #579]: #580
-#582 := [hypothesis]: #454
-#584 := (or #583 #575)
-#585 := [th-lemma arith triangle-eq]: #584
-#586 := [unit-resolution #585 #582 #581]: false
-#587 := [lemma #586]: #583
-#458 := (or #196 #454)
-#459 := [def-axiom]: #458
-#588 := [unit-resolution #459 #587]: #196
-#455 := (not #196)
-#456 := (or #455 #453)
-#457 := [def-axiom]: #456
-#589 := [unit-resolution #457 #588]: #453
-#590 := (not #453)
-#591 := (or #590 #566)
-#592 := [th-lemma arith triangle-eq]: #591
-[unit-resolution #592 #589 #574]: false
-unsat
-2f97dcfdcbc769d60cb4ae1079a5868256b79bd3 330 0
-#2 := false
-#7 := 0::Real
-decl f9 :: (-> S6 S2 Real)
-decl f12 :: S2
-#26 := f12
-decl f13 :: S6
-#30 := f13
-#31 := (f9 f13 f12)
-decl f11 :: S6
-#20 := f11
-#29 := (f9 f11 f12)
-#108 := -1::Real
-#168 := (* -1::Real #29)
-#169 := (+ #168 #31)
-decl f3 :: Real
-#8 := f3
-#147 := (* -1::Real #31)
-#256 := (+ #29 #147)
-#257 := (+ f3 #256)
-#258 := (<= #257 0::Real)
-#261 := (if #258 f3 #169)
-#635 := (* -1::Real #261)
-#636 := (+ f3 #635)
-#643 := (<= #636 0::Real)
-#651 := (not #643)
-#135 := 1/2::Real
-#402 := (* 1/2::Real #261)
-#538 := (<= #402 0::Real)
-#403 := (= #402 0::Real)
-#189 := -1/2::Real
-#264 := (* -1/2::Real #261)
-#267 := (+ #31 #264)
-decl f10 :: S6
-#18 := f10
-#33 := (f9 f10 f12)
-#148 := (+ #147 #33)
-#241 := (* -1::Real #33)
-#242 := (+ #31 #241)
-#243 := (+ f3 #242)
-#244 := (<= #243 0::Real)
-#247 := (if #244 f3 #148)
-#250 := (* 1/2::Real #247)
-#253 := (+ #31 #250)
-#137 := (* 1/2::Real #33)
-#230 := (+ #147 #137)
-#136 := (* 1/2::Real #29)
-#231 := (+ #136 #230)
-#228 := (>= #231 0::Real)
-#270 := (if #228 #253 #267)
-#273 := (= #270 #31)
-#406 := (iff #273 #403)
-#399 := (= #267 #31)
-#404 := (iff #399 #403)
-#405 := [rewrite]: #404
-#400 := (iff #273 #399)
-#397 := (= #270 #267)
-#392 := (if false #253 #267)
-#395 := (= #392 #267)
-#396 := [rewrite]: #395
-#393 := (= #270 #392)
-#390 := (iff #228 false)
-#227 := (not #228)
-#276 := (not #273)
-#289 := (<= #242 0::Real)
-#286 := (<= #256 0::Real)
-#292 := (and #286 #289)
-#62 := 0::Int
-decl f4 :: (-> S3 S2 Int)
-decl f5 :: S3
-#10 := f5
-#27 := (f4 f5 f12)
-#101 := -1::Int
-#125 := (* -1::Int #27)
-decl f6 :: (-> S4 S5 S2)
-decl f8 :: S5
-#14 := f8
-decl f7 :: S4
-#13 := f7
-#15 := (f6 f7 f8)
-#16 := (f4 f5 #15)
-#126 := (+ #16 #125)
-#127 := (<= #126 0::Int)
-#295 := (or #127 #292)
-#298 := (not #295)
-#307 := (or #298 #228 #276)
-#312 := (not #307)
-#38 := 2::Real
-#47 := (- #31 #29)
-#48 := (<= f3 #47)
-#49 := (if #48 f3 #47)
-#50 := (/ #49 2::Real)
-#51 := (- #31 #50)
-#42 := (- #33 #31)
-#43 := (<= f3 #42)
-#44 := (if #43 f3 #42)
-#45 := (/ #44 2::Real)
-#46 := (+ #31 #45)
-#37 := (+ #29 #33)
-#39 := (/ #37 2::Real)
-#41 := (<= #31 #39)
-#52 := (if #41 #46 #51)
-#53 := (= #52 #31)
-#54 := (not #53)
-#40 := (< #39 #31)
-#55 := (implies #40 #54)
-#34 := (<= #31 #33)
-#32 := (<= #29 #31)
-#35 := (and #32 #34)
-#28 := (< #27 #16)
-#36 := (implies #28 #35)
-#56 := (implies #36 #55)
-#57 := (not #56)
-#315 := (iff #57 #312)
-#172 := (<= f3 #169)
-#175 := (if #172 f3 #169)
-#190 := (* -1/2::Real #175)
-#191 := (+ #31 #190)
-#151 := (<= f3 #148)
-#154 := (if #151 f3 #148)
-#160 := (* 1/2::Real #154)
-#165 := (+ #31 #160)
-#138 := (+ #136 #137)
-#144 := (<= #31 #138)
-#196 := (if #144 #165 #191)
-#199 := (= #196 #31)
-#202 := (not #199)
-#141 := (< #138 #31)
-#208 := (not #141)
-#209 := (or #208 #202)
-#124 := (not #28)
-#132 := (or #124 #35)
-#217 := (not #132)
-#218 := (or #217 #209)
-#223 := (not #218)
-#313 := (iff #223 #312)
-#310 := (iff #218 #307)
-#301 := (or #228 #276)
-#304 := (or #298 #301)
-#308 := (iff #304 #307)
-#309 := [rewrite]: #308
-#305 := (iff #218 #304)
-#302 := (iff #209 #301)
-#277 := (iff #202 #276)
-#274 := (iff #199 #273)
-#271 := (= #196 #270)
-#268 := (= #191 #267)
-#265 := (= #190 #264)
-#262 := (= #175 #261)
-#259 := (iff #172 #258)
-#260 := [rewrite]: #259
-#263 := [monotonicity #260]: #262
-#266 := [monotonicity #263]: #265
-#269 := [monotonicity #266]: #268
-#254 := (= #165 #253)
-#251 := (= #160 #250)
-#248 := (= #154 #247)
-#245 := (iff #151 #244)
-#246 := [rewrite]: #245
-#249 := [monotonicity #246]: #248
-#252 := [monotonicity #249]: #251
-#255 := [monotonicity #252]: #254
-#240 := (iff #144 #228)
-#239 := [rewrite]: #240
-#272 := [monotonicity #239 #255 #269]: #271
-#275 := [monotonicity #272]: #274
-#278 := [monotonicity #275]: #277
-#237 := (iff #208 #228)
-#232 := (not #227)
-#235 := (iff #232 #228)
-#236 := [rewrite]: #235
-#233 := (iff #208 #232)
-#226 := (iff #141 #227)
-#229 := [rewrite]: #226
-#234 := [monotonicity #229]: #233
-#238 := [trans #234 #236]: #237
-#303 := [monotonicity #238 #278]: #302
-#299 := (iff #217 #298)
-#296 := (iff #132 #295)
-#293 := (iff #35 #292)
-#290 := (iff #34 #289)
-#291 := [rewrite]: #290
-#287 := (iff #32 #286)
-#288 := [rewrite]: #287
-#294 := [monotonicity #288 #291]: #293
-#284 := (iff #124 #127)
-#128 := (not #127)
-#279 := (not #128)
-#282 := (iff #279 #127)
-#283 := [rewrite]: #282
-#280 := (iff #124 #279)
-#129 := (iff #28 #128)
-#130 := [rewrite]: #129
-#281 := [monotonicity #130]: #280
-#285 := [trans #281 #283]: #284
-#297 := [monotonicity #285 #294]: #296
-#300 := [monotonicity #297]: #299
-#306 := [monotonicity #300 #303]: #305
-#311 := [trans #306 #309]: #310
-#314 := [monotonicity #311]: #313
-#224 := (iff #57 #223)
-#221 := (iff #56 #218)
-#214 := (implies #132 #209)
-#219 := (iff #214 #218)
-#220 := [rewrite]: #219
-#215 := (iff #56 #214)
-#212 := (iff #55 #209)
-#205 := (implies #141 #202)
-#210 := (iff #205 #209)
-#211 := [rewrite]: #210
-#206 := (iff #55 #205)
-#203 := (iff #54 #202)
-#200 := (iff #53 #199)
-#197 := (= #52 #196)
-#194 := (= #51 #191)
-#181 := (* 1/2::Real #175)
-#186 := (- #31 #181)
-#192 := (= #186 #191)
-#193 := [rewrite]: #192
-#187 := (= #51 #186)
-#184 := (= #50 #181)
-#178 := (/ #175 2::Real)
-#182 := (= #178 #181)
-#183 := [rewrite]: #182
-#179 := (= #50 #178)
-#176 := (= #49 #175)
-#170 := (= #47 #169)
-#171 := [rewrite]: #170
-#173 := (iff #48 #172)
-#174 := [monotonicity #171]: #173
-#177 := [monotonicity #174 #171]: #176
-#180 := [monotonicity #177]: #179
-#185 := [trans #180 #183]: #184
-#188 := [monotonicity #185]: #187
-#195 := [trans #188 #193]: #194
-#166 := (= #46 #165)
-#163 := (= #45 #160)
-#157 := (/ #154 2::Real)
-#161 := (= #157 #160)
-#162 := [rewrite]: #161
-#158 := (= #45 #157)
-#155 := (= #44 #154)
-#149 := (= #42 #148)
-#150 := [rewrite]: #149
-#152 := (iff #43 #151)
-#153 := [monotonicity #150]: #152
-#156 := [monotonicity #153 #150]: #155
-#159 := [monotonicity #156]: #158
-#164 := [trans #159 #162]: #163
-#167 := [monotonicity #164]: #166
-#145 := (iff #41 #144)
-#139 := (= #39 #138)
-#140 := [rewrite]: #139
-#146 := [monotonicity #140]: #145
-#198 := [monotonicity #146 #167 #195]: #197
-#201 := [monotonicity #198]: #200
-#204 := [monotonicity #201]: #203
-#142 := (iff #40 #141)
-#143 := [monotonicity #140]: #142
-#207 := [monotonicity #143 #204]: #206
-#213 := [trans #207 #211]: #212
-#133 := (iff #36 #132)
-#134 := [rewrite]: #133
-#216 := [monotonicity #134 #213]: #215
-#222 := [trans #216 #220]: #221
-#225 := [monotonicity #222]: #224
-#316 := [trans #225 #314]: #315
-#100 := [asserted]: #57
-#317 := [mp #100 #316]: #312
-#319 := [not-or-elim #317]: #227
-#391 := [iff-false #319]: #390
-#394 := [monotonicity #391]: #393
-#398 := [trans #394 #396]: #397
-#401 := [monotonicity #398]: #400
-#407 := [trans #401 #405]: #406
-#320 := [not-or-elim #317]: #273
-#408 := [mp #320 #407]: #403
-#645 := (not #403)
-#646 := (or #645 #538)
-#647 := [th-lemma arith triangle-eq]: #646
-#648 := [unit-resolution #647 #408]: #538
-#649 := [hypothesis]: #643
-#95 := (<= f3 0::Real)
-#96 := (not #95)
-#9 := (< 0::Real f3)
-#97 := (iff #9 #96)
-#98 := [rewrite]: #97
-#92 := [asserted]: #9
-#99 := [mp #92 #98]: #96
-#650 := [th-lemma arith farkas -1/2 1/2 1 #99 #649 #648]: false
-#652 := [lemma #650]: #651
-#531 := (= f3 #261)
-#532 := (= #169 #261)
-#660 := (not #532)
-#644 := (+ #169 #635)
-#653 := (<= #644 0::Real)
-#657 := (not #653)
-#385 := (iff #295 #292)
-#380 := (or false #292)
-#383 := (iff #380 #292)
-#384 := [rewrite]: #383
-#381 := (iff #295 #380)
-#378 := (iff #127 false)
-#94 := [asserted]: #28
-#131 := [mp #94 #130]: #128
-#379 := [iff-false #131]: #378
-#382 := [monotonicity #379]: #381
-#386 := [trans #382 #384]: #385
-#318 := [not-or-elim #317]: #295
-#387 := [mp #318 #386]: #292
-#377 := [and-elim #387]: #289
-#655 := [hypothesis]: #653
-#656 := [th-lemma arith farkas 1/2 1/2 1 1 #655 #377 #319 #648]: false
-#658 := [lemma #656]: #657
-#659 := [hypothesis]: #532
-#661 := (or #660 #653)
-#662 := [th-lemma arith triangle-eq]: #661
-#663 := [unit-resolution #662 #659 #658]: false
-#664 := [lemma #663]: #660
-#536 := (or #258 #532)
-#537 := [def-axiom]: #536
-#665 := [unit-resolution #537 #664]: #258
-#533 := (not #258)
-#534 := (or #533 #531)
-#535 := [def-axiom]: #534
-#666 := [unit-resolution #535 #665]: #531
-#667 := (not #531)
-#668 := (or #667 #643)
-#669 := [th-lemma arith triangle-eq]: #668
-[unit-resolution #669 #666 #652]: false
-unsat
-b9e1ece514fa963403f47578ecff6afc75e474ab 831 0
-#2 := false
-#10 := 0::Real
-decl ?v0!5 :: Real
-#445 := ?v0!5
-#78 := -1::Real
-#448 := (* -1::Real ?v0!5)
-decl f3 :: Real
-#8 := f3
-#517 := (+ f3 #448)
-#79 := (* -1::Real f3)
-#511 := (+ #79 ?v0!5)
-#518 := (<= #517 0::Real)
-#525 := (if #518 #511 #517)
-#528 := (* -1::Real #525)
-decl f4 :: Real
-#14 := f4
-#98 := 1/3::Real
-#99 := (* 1/3::Real f4)
-#531 := (+ #99 #528)
-#534 := (<= #531 0::Real)
-#537 := (not #534)
-decl ?v5!0 :: Real
-#442 := ?v5!0
-#487 := (* -1::Real ?v5!0)
-decl ?v3!2 :: Real
-#440 := ?v3!2
-#490 := (+ ?v3!2 #487)
-#491 := (>= #490 0::Real)
-decl ?v1!4 :: Real
-#444 := ?v1!4
-#455 := (* -1::Real ?v1!4)
-#587 := (+ ?v5!0 #455)
-#588 := (>= #587 0::Real)
-decl ?v4!1 :: Real
-#443 := ?v4!1
-#482 := (* -1::Real ?v4!1)
-decl ?v2!3 :: Real
-#441 := ?v2!3
-#485 := (+ ?v2!3 #482)
-#486 := (>= #485 0::Real)
-#575 := (+ ?v4!1 #448)
-#576 := (>= #575 0::Real)
-decl f5 :: Real
-#25 := f5
-#178 := (+ #79 f5)
-#126 := (* -1::Real f5)
-#169 := (+ f3 #126)
-#257 := (>= #169 0::Real)
-#264 := (if #257 #169 #178)
-#272 := (* -1::Real #264)
-#273 := (+ #99 #272)
-#274 := (<= #273 0::Real)
-#275 := (not #274)
-#473 := (* -1::Real ?v3!2)
-#474 := (+ f5 #473)
-#476 := (+ #126 ?v3!2)
-#475 := (<= #474 0::Real)
-#477 := (if #475 #476 #474)
-#478 := (* -1::Real #477)
-#479 := (+ #99 #478)
-#480 := (<= #479 0::Real)
-#481 := (not #480)
-#466 := (* -1::Real ?v2!3)
-#546 := (+ f5 #466)
-#540 := (+ #126 ?v2!3)
-#547 := (<= #546 0::Real)
-#554 := (if #547 #540 #546)
-#557 := (* -1::Real #554)
-#560 := (+ #99 #557)
-#563 := (<= #560 0::Real)
-#566 := (not #563)
-#456 := (+ f3 #455)
-#458 := (+ #79 ?v1!4)
-#457 := (<= #456 0::Real)
-#459 := (if #457 #458 #456)
-#460 := (* -1::Real #459)
-#461 := (+ #99 #460)
-#462 := (<= #461 0::Real)
-#463 := (not #462)
-#593 := (and #537 #463 #566 #481 #275 #576 #486 #588 #491)
-#605 := (+ ?v5!0 #482)
-#599 := (+ #487 ?v4!1)
-#606 := (<= #605 0::Real)
-#613 := (if #606 #599 #605)
-#616 := (* -1::Real #613)
-#619 := (+ f4 #616)
-#622 := (<= #619 0::Real)
-#625 := (not #622)
-#596 := (not #593)
-#628 := (or #596 #625)
-#631 := (not #628)
-#496 := (+ #482 ?v5!0)
-#494 := (+ ?v4!1 #487)
-#495 := (>= #494 0::Real)
-#497 := (if #495 #494 #496)
-#498 := (* -1::Real #497)
-#499 := (+ f4 #498)
-#500 := (<= #499 0::Real)
-#501 := (not #500)
-#488 := (+ ?v1!4 #487)
-#489 := (<= #488 0::Real)
-#483 := (+ ?v0!5 #482)
-#484 := (<= #483 0::Real)
-#467 := (+ #466 f5)
-#464 := (+ ?v2!3 #126)
-#465 := (>= #464 0::Real)
-#468 := (if #465 #464 #467)
-#469 := (* -1::Real #468)
-#470 := (+ #99 #469)
-#471 := (<= #470 0::Real)
-#472 := (not #471)
-#449 := (+ #448 f3)
-#446 := (+ ?v0!5 #79)
-#447 := (>= #446 0::Real)
-#450 := (if #447 #446 #449)
-#451 := (* -1::Real #450)
-#452 := (+ #99 #451)
-#453 := (<= #452 0::Real)
-#454 := (not #453)
-#492 := (and #454 #463 #472 #481 #275 #484 #486 #489 #491)
-#493 := (not #492)
-#502 := (or #493 #501)
-#503 := (not #502)
-#632 := (iff #503 #631)
-#629 := (iff #502 #628)
-#626 := (iff #501 #625)
-#623 := (iff #500 #622)
-#620 := (= #499 #619)
-#617 := (= #498 #616)
-#614 := (= #497 #613)
-#611 := (= #496 #605)
-#612 := [rewrite]: #611
-#600 := (= #494 #599)
-#601 := [rewrite]: #600
-#609 := (iff #495 #606)
-#602 := (>= #599 0::Real)
-#607 := (iff #602 #606)
-#608 := [rewrite]: #607
-#603 := (iff #495 #602)
-#604 := [monotonicity #601]: #603
-#610 := [trans #604 #608]: #609
-#615 := [monotonicity #610 #601 #612]: #614
-#618 := [monotonicity #615]: #617
-#621 := [monotonicity #618]: #620
-#624 := [monotonicity #621]: #623
-#627 := [monotonicity #624]: #626
-#597 := (iff #493 #596)
-#594 := (iff #492 #593)
-#591 := (iff #489 #588)
-#581 := (+ #487 ?v1!4)
-#584 := (<= #581 0::Real)
-#589 := (iff #584 #588)
-#590 := [rewrite]: #589
-#585 := (iff #489 #584)
-#582 := (= #488 #581)
-#583 := [rewrite]: #582
-#586 := [monotonicity #583]: #585
-#592 := [trans #586 #590]: #591
-#579 := (iff #484 #576)
-#569 := (+ #482 ?v0!5)
-#572 := (<= #569 0::Real)
-#577 := (iff #572 #576)
-#578 := [rewrite]: #577
-#573 := (iff #484 #572)
-#570 := (= #483 #569)
-#571 := [rewrite]: #570
-#574 := [monotonicity #571]: #573
-#580 := [trans #574 #578]: #579
-#567 := (iff #472 #566)
-#564 := (iff #471 #563)
-#561 := (= #470 #560)
-#558 := (= #469 #557)
-#555 := (= #468 #554)
-#552 := (= #467 #546)
-#553 := [rewrite]: #552
-#541 := (= #464 #540)
-#542 := [rewrite]: #541
-#550 := (iff #465 #547)
-#543 := (>= #540 0::Real)
-#548 := (iff #543 #547)
-#549 := [rewrite]: #548
-#544 := (iff #465 #543)
-#545 := [monotonicity #542]: #544
-#551 := [trans #545 #549]: #550
-#556 := [monotonicity #551 #542 #553]: #555
-#559 := [monotonicity #556]: #558
-#562 := [monotonicity #559]: #561
-#565 := [monotonicity #562]: #564
-#568 := [monotonicity #565]: #567
-#538 := (iff #454 #537)
-#535 := (iff #453 #534)
-#532 := (= #452 #531)
-#529 := (= #451 #528)
-#526 := (= #450 #525)
-#523 := (= #449 #517)
-#524 := [rewrite]: #523
-#512 := (= #446 #511)
-#513 := [rewrite]: #512
-#521 := (iff #447 #518)
-#514 := (>= #511 0::Real)
-#519 := (iff #514 #518)
-#520 := [rewrite]: #519
-#515 := (iff #447 #514)
-#516 := [monotonicity #513]: #515
-#522 := [trans #516 #520]: #521
-#527 := [monotonicity #522 #513 #524]: #526
-#530 := [monotonicity #527]: #529
-#533 := [monotonicity #530]: #532
-#536 := [monotonicity #533]: #535
-#539 := [monotonicity #536]: #538
-#595 := [monotonicity #539 #568 #580 #592]: #594
-#598 := [monotonicity #595]: #597
-#630 := [monotonicity #598 #627]: #629
-#633 := [monotonicity #630]: #632
-#45 := (:var 0 Real)
-#42 := (:var 1 Real)
-#214 := (* -1::Real #42)
-#215 := (+ #214 #45)
-#204 := (* -1::Real #45)
-#205 := (+ #42 #204)
-#404 := (>= #205 0::Real)
-#411 := (if #404 #205 #215)
-#419 := (* -1::Real #411)
-#420 := (+ f4 #419)
-#421 := (<= #420 0::Real)
-#422 := (not #421)
-#31 := (:var 2 Real)
-#246 := (+ #31 #204)
-#245 := (>= #246 0::Real)
-#18 := (:var 4 Real)
-#241 := (+ #18 #204)
-#242 := (<= #241 0::Real)
-#24 := (:var 3 Real)
-#250 := (+ #24 #214)
-#249 := (>= #250 0::Real)
-#7 := (:var 5 Real)
-#253 := (+ #7 #214)
-#254 := (<= #253 0::Real)
-#157 := (* -1::Real #31)
-#158 := (+ f5 #157)
-#148 := (+ #126 #31)
-#280 := (<= #158 0::Real)
-#287 := (if #280 #148 #158)
-#295 := (* -1::Real #287)
-#296 := (+ #99 #295)
-#297 := (<= #296 0::Real)
-#298 := (not #297)
-#136 := (* -1::Real #24)
-#137 := (+ #136 f5)
-#127 := (+ #24 #126)
-#303 := (>= #127 0::Real)
-#310 := (if #303 #127 #137)
-#318 := (* -1::Real #310)
-#319 := (+ #99 #318)
-#320 := (<= #319 0::Real)
-#321 := (not #320)
-#114 := (* -1::Real #18)
-#115 := (+ f3 #114)
-#105 := (+ #79 #18)
-#326 := (<= #115 0::Real)
-#333 := (if #326 #105 #115)
-#341 := (* -1::Real #333)
-#342 := (+ #99 #341)
-#343 := (<= #342 0::Real)
-#344 := (not #343)
-#89 := (* -1::Real #7)
-#90 := (+ #89 f3)
-#80 := (+ #7 #79)
-#349 := (>= #80 0::Real)
-#356 := (if #349 #80 #90)
-#364 := (* -1::Real #356)
-#365 := (+ #99 #364)
-#366 := (<= #365 0::Real)
-#367 := (not #366)
-#396 := (and #367 #344 #321 #298 #275 #254 #249 #242 #245)
-#401 := (not #396)
-#427 := (or #401 #422)
-#430 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real) (?v4 Real) (?v5 Real)) #427)
-#433 := (not #430)
-#504 := (~ #433 #503)
-#505 := [sk]: #504
-#56 := (- #42 #45)
-#58 := (- #56)
-#57 := (< #56 0::Real)
-#59 := (if #57 #58 #56)
-#60 := (< #59 f4)
-#47 := (<= #45 #31)
-#46 := (<= #18 #45)
-#48 := (and #46 #47)
-#44 := (<= #42 #24)
-#49 := (and #44 #48)
-#43 := (<= #7 #42)
-#50 := (and #43 #49)
-#15 := 3::Real
-#16 := (/ f4 3::Real)
-#37 := (- f3 f5)
-#39 := (- #37)
-#38 := (< #37 0::Real)
-#40 := (if #38 #39 #37)
-#41 := (< #40 #16)
-#51 := (and #41 #50)
-#32 := (- #31 f5)
-#34 := (- #32)
-#33 := (< #32 0::Real)
-#35 := (if #33 #34 #32)
-#36 := (< #35 #16)
-#52 := (and #36 #51)
-#26 := (- #24 f5)
-#28 := (- #26)
-#27 := (< #26 0::Real)
-#29 := (if #27 #28 #26)
-#30 := (< #29 #16)
-#53 := (and #30 #52)
-#19 := (- #18 f3)
-#21 := (- #19)
-#20 := (< #19 0::Real)
-#22 := (if #20 #21 #19)
-#23 := (< #22 #16)
-#54 := (and #23 #53)
-#9 := (- #7 f3)
-#12 := (- #9)
-#11 := (< #9 0::Real)
-#13 := (if #11 #12 #9)
-#17 := (< #13 #16)
-#55 := (and #17 #54)
-#61 := (implies #55 #60)
-#62 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real) (?v4 Real) (?v5 Real)) #61)
-#63 := (not #62)
-#436 := (iff #63 #433)
-#208 := (< #205 0::Real)
-#220 := (if #208 #215 #205)
-#223 := (< #220 f4)
-#172 := (< #169 0::Real)
-#183 := (if #172 #178 #169)
-#186 := (< #183 #99)
-#189 := (and #186 #50)
-#151 := (< #148 0::Real)
-#163 := (if #151 #158 #148)
-#166 := (< #163 #99)
-#192 := (and #166 #189)
-#130 := (< #127 0::Real)
-#142 := (if #130 #137 #127)
-#145 := (< #142 #99)
-#195 := (and #145 #192)
-#108 := (< #105 0::Real)
-#120 := (if #108 #115 #105)
-#123 := (< #120 #99)
-#198 := (and #123 #195)
-#83 := (< #80 0::Real)
-#95 := (if #83 #90 #80)
-#102 := (< #95 #99)
-#201 := (and #102 #198)
-#229 := (not #201)
-#230 := (or #229 #223)
-#235 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real) (?v4 Real) (?v5 Real)) #230)
-#238 := (not #235)
-#434 := (iff #238 #433)
-#431 := (iff #235 #430)
-#428 := (iff #230 #427)
-#425 := (iff #223 #422)
-#416 := (< #411 f4)
-#423 := (iff #416 #422)
-#424 := [rewrite]: #423
-#417 := (iff #223 #416)
-#414 := (= #220 #411)
-#405 := (not #404)
-#408 := (if #405 #215 #205)
-#412 := (= #408 #411)
-#413 := [rewrite]: #412
-#409 := (= #220 #408)
-#406 := (iff #208 #405)
-#407 := [rewrite]: #406
-#410 := [monotonicity #407]: #409
-#415 := [trans #410 #413]: #414
-#418 := [monotonicity #415]: #417
-#426 := [trans #418 #424]: #425
-#402 := (iff #229 #401)
-#399 := (iff #201 #396)
-#372 := (and #242 #245)
-#375 := (and #249 #372)
-#378 := (and #254 #375)
-#381 := (and #275 #378)
-#384 := (and #298 #381)
-#387 := (and #321 #384)
-#390 := (and #344 #387)
-#393 := (and #367 #390)
-#397 := (iff #393 #396)
-#398 := [rewrite]: #397
-#394 := (iff #201 #393)
-#391 := (iff #198 #390)
-#388 := (iff #195 #387)
-#385 := (iff #192 #384)
-#382 := (iff #189 #381)
-#379 := (iff #50 #378)
-#376 := (iff #49 #375)
-#373 := (iff #48 #372)
-#247 := (iff #47 #245)
-#248 := [rewrite]: #247
-#243 := (iff #46 #242)
-#244 := [rewrite]: #243
-#374 := [monotonicity #244 #248]: #373
-#251 := (iff #44 #249)
-#252 := [rewrite]: #251
-#377 := [monotonicity #252 #374]: #376
-#255 := (iff #43 #254)
-#256 := [rewrite]: #255
-#380 := [monotonicity #256 #377]: #379
-#278 := (iff #186 #275)
-#269 := (< #264 #99)
-#276 := (iff #269 #275)
-#277 := [rewrite]: #276
-#270 := (iff #186 #269)
-#267 := (= #183 #264)
-#258 := (not #257)
-#261 := (if #258 #178 #169)
-#265 := (= #261 #264)
-#266 := [rewrite]: #265
-#262 := (= #183 #261)
-#259 := (iff #172 #258)
-#260 := [rewrite]: #259
-#263 := [monotonicity #260]: #262
-#268 := [trans #263 #266]: #267
-#271 := [monotonicity #268]: #270
-#279 := [trans #271 #277]: #278
-#383 := [monotonicity #279 #380]: #382
-#301 := (iff #166 #298)
-#292 := (< #287 #99)
-#299 := (iff #292 #298)
-#300 := [rewrite]: #299
-#293 := (iff #166 #292)
-#290 := (= #163 #287)
-#281 := (not #280)
-#284 := (if #281 #158 #148)
-#288 := (= #284 #287)
-#289 := [rewrite]: #288
-#285 := (= #163 #284)
-#282 := (iff #151 #281)
-#283 := [rewrite]: #282
-#286 := [monotonicity #283]: #285
-#291 := [trans #286 #289]: #290
-#294 := [monotonicity #291]: #293
-#302 := [trans #294 #300]: #301
-#386 := [monotonicity #302 #383]: #385
-#324 := (iff #145 #321)
-#315 := (< #310 #99)
-#322 := (iff #315 #321)
-#323 := [rewrite]: #322
-#316 := (iff #145 #315)
-#313 := (= #142 #310)
-#304 := (not #303)
-#307 := (if #304 #137 #127)
-#311 := (= #307 #310)
-#312 := [rewrite]: #311
-#308 := (= #142 #307)
-#305 := (iff #130 #304)
-#306 := [rewrite]: #305
-#309 := [monotonicity #306]: #308
-#314 := [trans #309 #312]: #313
-#317 := [monotonicity #314]: #316
-#325 := [trans #317 #323]: #324
-#389 := [monotonicity #325 #386]: #388
-#347 := (iff #123 #344)
-#338 := (< #333 #99)
-#345 := (iff #338 #344)
-#346 := [rewrite]: #345
-#339 := (iff #123 #338)
-#336 := (= #120 #333)
-#327 := (not #326)
-#330 := (if #327 #115 #105)
-#334 := (= #330 #333)
-#335 := [rewrite]: #334
-#331 := (= #120 #330)
-#328 := (iff #108 #327)
-#329 := [rewrite]: #328
-#332 := [monotonicity #329]: #331
-#337 := [trans #332 #335]: #336
-#340 := [monotonicity #337]: #339
-#348 := [trans #340 #346]: #347
-#392 := [monotonicity #348 #389]: #391
-#370 := (iff #102 #367)
-#361 := (< #356 #99)
-#368 := (iff #361 #367)
-#369 := [rewrite]: #368
-#362 := (iff #102 #361)
-#359 := (= #95 #356)
-#350 := (not #349)
-#353 := (if #350 #90 #80)
-#357 := (= #353 #356)
-#358 := [rewrite]: #357
-#354 := (= #95 #353)
-#351 := (iff #83 #350)
-#352 := [rewrite]: #351
-#355 := [monotonicity #352]: #354
-#360 := [trans #355 #358]: #359
-#363 := [monotonicity #360]: #362
-#371 := [trans #363 #369]: #370
-#395 := [monotonicity #371 #392]: #394
-#400 := [trans #395 #398]: #399
-#403 := [monotonicity #400]: #402
-#429 := [monotonicity #403 #426]: #428
-#432 := [quant-intro #429]: #431
-#435 := [monotonicity #432]: #434
-#239 := (iff #63 #238)
-#236 := (iff #62 #235)
-#233 := (iff #61 #230)
-#226 := (implies #201 #223)
-#231 := (iff #226 #230)
-#232 := [rewrite]: #231
-#227 := (iff #61 #226)
-#224 := (iff #60 #223)
-#221 := (= #59 #220)
-#206 := (= #56 #205)
-#207 := [rewrite]: #206
-#218 := (= #58 #215)
-#211 := (- #205)
-#216 := (= #211 #215)
-#217 := [rewrite]: #216
-#212 := (= #58 #211)
-#213 := [monotonicity #207]: #212
-#219 := [trans #213 #217]: #218
-#209 := (iff #57 #208)
-#210 := [monotonicity #207]: #209
-#222 := [monotonicity #210 #219 #207]: #221
-#225 := [monotonicity #222]: #224
-#202 := (iff #55 #201)
-#199 := (iff #54 #198)
-#196 := (iff #53 #195)
-#193 := (iff #52 #192)
-#190 := (iff #51 #189)
-#187 := (iff #41 #186)
-#100 := (= #16 #99)
-#101 := [rewrite]: #100
-#184 := (= #40 #183)
-#170 := (= #37 #169)
-#171 := [rewrite]: #170
-#181 := (= #39 #178)
-#175 := (- #169)
-#179 := (= #175 #178)
-#180 := [rewrite]: #179
-#176 := (= #39 #175)
-#177 := [monotonicity #171]: #176
-#182 := [trans #177 #180]: #181
-#173 := (iff #38 #172)
-#174 := [monotonicity #171]: #173
-#185 := [monotonicity #174 #182 #171]: #184
-#188 := [monotonicity #185 #101]: #187
-#191 := [monotonicity #188]: #190
-#167 := (iff #36 #166)
-#164 := (= #35 #163)
-#149 := (= #32 #148)
-#150 := [rewrite]: #149
-#161 := (= #34 #158)
-#154 := (- #148)
-#159 := (= #154 #158)
-#160 := [rewrite]: #159
-#155 := (= #34 #154)
-#156 := [monotonicity #150]: #155
-#162 := [trans #156 #160]: #161
-#152 := (iff #33 #151)
-#153 := [monotonicity #150]: #152
-#165 := [monotonicity #153 #162 #150]: #164
-#168 := [monotonicity #165 #101]: #167
-#194 := [monotonicity #168 #191]: #193
-#146 := (iff #30 #145)
-#143 := (= #29 #142)
-#128 := (= #26 #127)
-#129 := [rewrite]: #128
-#140 := (= #28 #137)
-#133 := (- #127)
-#138 := (= #133 #137)
-#139 := [rewrite]: #138
-#134 := (= #28 #133)
-#135 := [monotonicity #129]: #134
-#141 := [trans #135 #139]: #140
-#131 := (iff #27 #130)
-#132 := [monotonicity #129]: #131
-#144 := [monotonicity #132 #141 #129]: #143
-#147 := [monotonicity #144 #101]: #146
-#197 := [monotonicity #147 #194]: #196
-#124 := (iff #23 #123)
-#121 := (= #22 #120)
-#106 := (= #19 #105)
-#107 := [rewrite]: #106
-#118 := (= #21 #115)
-#111 := (- #105)
-#116 := (= #111 #115)
-#117 := [rewrite]: #116
-#112 := (= #21 #111)
-#113 := [monotonicity #107]: #112
-#119 := [trans #113 #117]: #118
-#109 := (iff #20 #108)
-#110 := [monotonicity #107]: #109
-#122 := [monotonicity #110 #119 #107]: #121
-#125 := [monotonicity #122 #101]: #124
-#200 := [monotonicity #125 #197]: #199
-#103 := (iff #17 #102)
-#96 := (= #13 #95)
-#81 := (= #9 #80)
-#82 := [rewrite]: #81
-#93 := (= #12 #90)
-#86 := (- #80)
-#91 := (= #86 #90)
-#92 := [rewrite]: #91
-#87 := (= #12 #86)
-#88 := [monotonicity #82]: #87
-#94 := [trans #88 #92]: #93
-#84 := (iff #11 #83)
-#85 := [monotonicity #82]: #84
-#97 := [monotonicity #85 #94 #82]: #96
-#104 := [monotonicity #97 #101]: #103
-#203 := [monotonicity #104 #200]: #202
-#228 := [monotonicity #203 #225]: #227
-#234 := [trans #228 #232]: #233
-#237 := [quant-intro #234]: #236
-#240 := [monotonicity #237]: #239
-#437 := [trans #240 #435]: #436
-#77 := [asserted]: #63
-#438 := [mp #77 #437]: #433
-#508 := [mp~ #438 #505]: #503
-#509 := [mp #508 #633]: #631
-#510 := [not-or-elim #509]: #593
-#634 := [and-elim #510]: #537
-#637 := [and-elim #510]: #481
-#642 := [and-elim #510]: #491
-#733 := (= #178 #264)
-#808 := (not #733)
-#750 := (+ #178 #272)
-#751 := (<= #750 0::Real)
-#829 := (not #751)
-#639 := [and-elim #510]: #576
-#638 := [and-elim #510]: #275
-#850 := [hypothesis]: #751
-#844 := (+ #476 #478)
-#845 := (<= #844 0::Real)
-#725 := (= #476 #477)
-#841 := (+ #605 #616)
-#843 := (>= #841 0::Real)
-#739 := (= #605 #613)
-#740 := (not #606)
-#738 := (= #599 #613)
-#872 := (not #738)
-#745 := (+ #599 #616)
-#747 := (>= #745 0::Real)
-#771 := (not #747)
-#754 := (+ #540 #557)
-#755 := (<= #754 0::Real)
-#718 := (= #540 #554)
-#766 := [hypothesis]: #747
-#803 := (or #258 #771)
-#760 := [hypothesis]: #257
-#748 := (+ #169 #272)
-#749 := (<= #748 0::Real)
-#732 := (= #169 #264)
-#734 := (or #258 #732)
-#735 := [def-axiom]: #734
-#761 := [unit-resolution #735 #760]: #732
-#762 := (not #732)
-#763 := (or #762 #749)
-#764 := [th-lemma arith triangle-eq]: #763
-#765 := [unit-resolution #764 #761]: #749
-#641 := [and-elim #510]: #588
-#720 := (not #547)
-#789 := (not #718)
-#770 := (not #755)
-#781 := (or #770 #258 #771)
-#713 := (not #457)
-#767 := [hypothesis]: #755
-#772 := (or #713 #258 #770 #771)
-#636 := [and-elim #510]: #566
-#643 := [not-or-elim #509]: #622
-#640 := [and-elim #510]: #486
-#768 := [hypothesis]: #457
-#769 := [th-lemma arith farkas 1 3 1 1 1 1 2 2 1 1 #768 #760 #767 #640 #766 #643 #765 #638 #636 #641]: false
-#773 := [lemma #769]: #772
-#774 := [unit-resolution #773 #767 #760 #766]: #713
-#635 := [and-elim #510]: #463
-#757 := (+ #456 #460)
-#758 := (<= #757 0::Real)
-#712 := (= #456 #459)
-#716 := (or #457 #712)
-#717 := [def-axiom]: #716
-#775 := [unit-resolution #717 #774]: #712
-#776 := (not #712)
-#777 := (or #776 #758)
-#778 := [th-lemma arith triangle-eq]: #777
-#779 := [unit-resolution #778 #775]: #758
-#780 := [th-lemma arith farkas 1 1 1 1 1 1 2 2 1 1 #760 #767 #640 #766 #643 #636 #779 #635 #774 #641]: false
-#782 := [lemma #780]: #781
-#798 := [unit-resolution #782 #760 #766]: #770
-#790 := (or #789 #755)
-#753 := [hypothesis]: #770
-#756 := [hypothesis]: #718
-#791 := [th-lemma arith triangle-eq]: #790
-#792 := [unit-resolution #791 #756 #753]: false
-#793 := [lemma #792]: #790
-#799 := [unit-resolution #793 #798]: #789
-#721 := (or #720 #718)
-#722 := [def-axiom]: #721
-#800 := [unit-resolution #722 #799]: #720
-#787 := (or #547 #457 #771 #258)
-#759 := [hypothesis]: #720
-#783 := [hypothesis]: #713
-#784 := [unit-resolution #717 #783]: #712
-#785 := [unit-resolution #778 #784]: #758
-#786 := [th-lemma arith farkas 2 3 3 1 1 1 1 1 1 #783 #785 #635 #759 #640 #766 #643 #641 #760]: false
-#788 := [lemma #786]: #787
-#801 := [unit-resolution #788 #800 #766 #760]: #457
-#802 := [th-lemma arith farkas 1/4 1/4 1/4 -1/4 -1/4 1/4 -3/4 3/4 1 #800 #640 #766 #643 #801 #641 #765 #638 #760]: false
-#804 := [lemma #802]: #803
-#806 := [unit-resolution #804 #766]: #258
-#736 := (or #257 #733)
-#737 := [def-axiom]: #736
-#807 := [unit-resolution #737 #806]: #733
-#809 := (or #808 #751)
-#810 := [th-lemma arith triangle-eq]: #809
-#811 := [unit-resolution #810 #807]: #751
-#813 := (not #758)
-#818 := (or #813 #771)
-#805 := [hypothesis]: #758
-#814 := (or #547 #771 #813)
-#812 := [th-lemma arith farkas 1 2 2 1 1 1 1 1 1 1 #635 #811 #638 #806 #641 #759 #640 #766 #643 #805]: false
-#815 := [lemma #812]: #814
-#796 := [unit-resolution #815 #805 #766]: #547
-#797 := [unit-resolution #722 #796]: #718
-#816 := [unit-resolution #793 #797]: #755
-#817 := [th-lemma arith farkas 1 1 1 1 1 1 1 1 1 1 #805 #635 #811 #638 #640 #766 #643 #816 #636 #641]: false
-#819 := [lemma #817]: #818
-#826 := [unit-resolution #819 #766]: #813
-#822 := [hypothesis]: #813
-#823 := [hypothesis]: #712
-#824 := [unit-resolution #778 #823 #822]: false
-#825 := [lemma #824]: #777
-#827 := [unit-resolution #825 #826]: #776
-#828 := [unit-resolution #717 #827]: #457
-#831 := (not #486)
-#830 := (not #588)
-#832 := (or #713 #257 #829 #274 #830 #831 #771 #625 #547)
-#833 := [th-lemma arith assign-bounds 2 3 3 1 1 1 1 1]: #832
-#834 := [unit-resolution #833 #828 #806 #638 #640 #641 #643 #766 #811]: #547
-#835 := [unit-resolution #722 #834]: #718
-#836 := [unit-resolution #793 #835]: #755
-#837 := [th-lemma arith farkas 1 2 2 1 1 1 1 1 1 1 #636 #811 #638 #806 #828 #641 #640 #766 #643 #836]: false
-#838 := [lemma #837]: #771
-#871 := [hypothesis]: #738
-#873 := (or #872 #747)
-#874 := [th-lemma arith triangle-eq]: #873
-#875 := [unit-resolution #874 #871 #838]: false
-#876 := [lemma #875]: #872
-#741 := (or #740 #738)
-#742 := [def-axiom]: #741
-#869 := [unit-resolution #742 #876]: #740
-#743 := (or #606 #739)
-#744 := [def-axiom]: #743
-#870 := [unit-resolution #744 #869]: #739
-#877 := (not #739)
-#878 := (or #877 #843)
-#879 := [th-lemma arith triangle-eq]: #878
-#880 := [unit-resolution #879 #870]: #843
-#881 := (or #829 #518)
-#857 := (not #843)
-#867 := (or #857 #829 #518)
-#706 := (not #518)
-#847 := [hypothesis]: #706
-#848 := [hypothesis]: #843
-#858 := (or #475 #829 #857 #518)
-#727 := (not #475)
-#849 := [hypothesis]: #727
-#821 := (+ #517 #528)
-#839 := (<= #821 0::Real)
-#705 := (= #517 #525)
-#709 := (or #518 #705)
-#710 := [def-axiom]: #709
-#851 := [unit-resolution #710 #847]: #705
-#852 := (not #705)
-#853 := (or #852 #839)
-#854 := [th-lemma arith triangle-eq]: #853
-#855 := [unit-resolution #854 #851]: #839
-#856 := [th-lemma arith farkas 2 2 1 1 1 1 1 1 1 1 #855 #634 #850 #638 #642 #849 #639 #848 #643 #847]: false
-#859 := [lemma #856]: #858
-#860 := [unit-resolution #859 #848 #850 #847]: #475
-#728 := (or #727 #725)
-#729 := [def-axiom]: #728
-#861 := [unit-resolution #729 #860]: #725
-#862 := (not #725)
-#863 := (or #862 #845)
-#864 := [th-lemma arith triangle-eq]: #863
-#865 := [unit-resolution #864 #861]: #845
-#866 := [th-lemma arith farkas 1 1 1 1 1 1 1 1 1 1 #637 #850 #638 #642 #855 #639 #634 #848 #643 #865]: false
-#868 := [lemma #866]: #867
-#882 := [unit-resolution #868 #880]: #881
-#883 := [unit-resolution #882 #850]: #518
-#885 := (not #576)
-#884 := (not #491)
-#886 := (or #475 #606 #857 #625 #829 #274 #884 #706 #885)
-#887 := [th-lemma arith assign-bounds 2/3 1/3 1/3 1 1 1 1 1]: #886
-#888 := [unit-resolution #887 #883 #638 #639 #642 #869 #643 #850 #880]: #475
-#889 := [unit-resolution #729 #888]: #725
-#890 := [unit-resolution #864 #889]: #845
-#820 := (+ #511 #528)
-#840 := (<= #820 0::Real)
-#704 := (= #511 #525)
-#707 := (or #706 #704)
-#708 := [def-axiom]: #707
-#891 := [unit-resolution #708 #883]: #704
-#892 := (not #704)
-#893 := (or #892 #840)
-#894 := [th-lemma arith triangle-eq]: #893
-#895 := [unit-resolution #894 #891]: #840
-#896 := [th-lemma arith farkas 1 1 1 2 1 1 1 1 1 1 1 #895 #880 #643 #883 #890 #850 #638 #642 #639 #637 #634]: false
-#897 := [lemma #896]: #829
-#842 := [hypothesis]: #733
-#846 := [unit-resolution #810 #842 #897]: false
-#898 := [lemma #846]: #808
-#905 := [unit-resolution #737 #898]: #257
-#907 := (or #475 #518)
-#906 := [th-lemma arith farkas 1/2 1/2 1/2 1/2 3/2 3/2 1/2 1/2 1 #639 #905 #642 #849 #855 #634 #880 #643 #847]: false
-#908 := [lemma #906]: #907
-#902 := [unit-resolution #908 #847]: #475
-#903 := [unit-resolution #729 #902]: #725
-#904 := [unit-resolution #864 #903]: #845
-#909 := [th-lemma arith farkas 1 1 1 2 2 1 1 1 1 1 #639 #905 #642 #855 #634 #880 #643 #904 #637 #847]: false
-#910 := [lemma #909]: #518
-#911 := (or #475 #706 #885 #258 #884 #606)
-#912 := [th-lemma arith assign-bounds 1 1 1 1 1]: #911
-#913 := [unit-resolution #912 #910 #905 #639 #642 #869]: #475
-#914 := [unit-resolution #729 #913]: #725
-#915 := [unit-resolution #864 #914]: #845
-#916 := [unit-resolution #708 #910]: #704
-#917 := [unit-resolution #894 #916]: #840
-[th-lemma arith farkas 1 1/2 1/2 3/2 1/2 1/2 1/2 1/2 1/2 1 #917 #880 #643 #910 #915 #639 #905 #642 #637 #634]: false
-unsat
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 04 18:00:37 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 04 18:00:40 2012 +0100
@@ -8,10 +8,6 @@
"~~/src/HOL/Library/Indicator_Function"
begin
-declare [[smt_certificates = "Integration.certs"]]
-declare [[smt_read_only_certificates = true]]
-declare [[smt_oracle = false]]
-
(*declare not_less[simp] not_le[simp]*)
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -2770,16 +2766,21 @@
lemma has_integral_component_le: fixes f g::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "(f has_integral i) s" "(g has_integral j) s" "\<forall>x\<in>s. (f x)$$k \<le> (g x)$$k"
shows "i$$k \<le> j$$k"
-proof- have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow>
+proof -
+ have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow>
(g has_integral j) ({a..b}) \<Longrightarrow> \<forall>x\<in>{a..b}. (f x)$$k \<le> (g x)$$k \<Longrightarrow> i$$k \<le> j$$k"
- proof(rule ccontr) case goal1 hence *:"0 < (i$$k - j$$k) / 3" by auto
+ proof (rule ccontr)
+ case goal1
+ then have *: "0 < (i$$k - j$$k) / 3" by auto
guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d1=this[rule_format]
guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d2=this[rule_format]
guess p using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter .
note p = this(1) conjunctD2[OF this(2)] note le_less_trans[OF component_le_norm, of _ _ k] term g
note this[OF d1(2)[OF conjI[OF p(1,2)]]] this[OF d2(2)[OF conjI[OF p(1,3)]]]
- thus False unfolding euclidean_simps using rsum_component_le[OF p(1) goal1(3)] apply simp
- using [[z3_with_extensions]] by smt
+ thus False
+ unfolding euclidean_simps
+ using rsum_component_le[OF p(1) goal1(3)]
+ by (simp add: abs_real_def split: split_if_asm)
qed let ?P = "\<exists>a b. s = {a..b}"
{ presume "\<not> ?P \<Longrightarrow> ?thesis" thus ?thesis proof(cases ?P)
case True then guess a b apply-by(erule exE)+ note s=this
@@ -2793,7 +2794,8 @@
note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
- have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" using [[z3_with_extensions]] by smt
+ have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
+ by (simp add: abs_real_def split: split_if_asm)
note le_less_trans[OF component_le_norm[of _ k]] note this[OF w1(2)] this[OF w2(2)] moreover
have "w1$$k \<le> w2$$k" apply(rule lem[OF w1(1) w2(1)]) using assms by auto ultimately
show False unfolding euclidean_simps by(rule *) qed
@@ -3022,7 +3024,8 @@
also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<le> content {u..v}"
unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[THEN sym,OF k] by auto
- thus ?case unfolding goal1 unfolding interval_doublesplit[OF k] using content_pos_le by smt
+ thus ?case unfolding goal1 unfolding interval_doublesplit[OF k]
+ by (blast intro: antisym)
next have *:"setsum content {l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} |l. l \<in> snd ` p \<and> l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} \<noteq> {}} \<ge> 0"
apply(rule setsum_nonneg,rule) unfolding mem_Collect_eq image_iff apply(erule exE bexE conjE)+ unfolding split_paired_all
proof- fix x l a b assume as:"x = l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}" "(a, b) \<in> p" "l = snd (a, b)"
@@ -3516,7 +3519,7 @@
proof safe fix x and e::real assume as:"x\<in>k" "e>0"
from k(2)[unfolded k content_eq_0] guess i ..
hence i:"c$$i = d$$i" "i<DIM('a)" using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto
- hence xi:"x$$i = d$$i" using as unfolding k mem_interval by smt
+ hence xi:"x$$i = d$$i" using as unfolding k mem_interval by (metis antisym)
def y \<equiv> "(\<chi>\<chi> j. if j = i then if c$$i \<le> (a$$i + b$$i) / 2 then c$$i +
min e (b$$i - c$$i) / 2 else c$$i - min e (c$$i - a$$i) / 2 else x$$j)::'a"
show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x=y in bexI)
@@ -3524,7 +3527,8 @@
hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN spec[where x=i]]
hence xyi:"y$$i \<noteq> x$$i" unfolding y_def unfolding i xi euclidean_lambda_beta'[OF i(2)] if_P[OF refl]
apply(cases) apply(subst if_P,assumption) unfolding if_not_P not_le using as(2)
- using assms(2)[unfolded content_eq_0] using i(2) using [[z3_with_extensions]] by smt+
+ using assms(2)[unfolded content_eq_0] using i(2)
+ by (auto simp add: not_le min_def)
thus "y \<noteq> x" unfolding euclidean_eq[where 'a='a] using i by auto
have *:"{..<DIM('a)} = insert i ({..<DIM('a)} - {i})" using i by auto
have "norm (y - x) < e + setsum (\<lambda>i. 0) {..<DIM('a)}" apply(rule le_less_trans[OF norm_le_l1])
@@ -4710,7 +4714,8 @@
proof- fix a b c d::"'n::ordered_euclidean_space" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
have **:"ball 0 B1 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto
have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
- abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" using [[z3_with_extensions]] by smt
+ abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e"
+ by (simp add: abs_real_def split: split_if_asm)
show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
apply(rule B1(2),rule order_trans,rule **,rule as(1))
@@ -6057,7 +6062,4 @@
using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
qed qed(insert n,auto) qed qed qed
-declare [[smt_certificates = ""]]
-declare [[smt_read_only_certificates = false]]
-
end
--- a/src/HOL/ROOT Tue Dec 04 18:00:37 2012 +0100
+++ b/src/HOL/ROOT Tue Dec 04 18:00:40 2012 +0100
@@ -577,7 +577,6 @@
Multivariate_Analysis
Determinants
files
- "Integration.certs"
"document/root.tex"
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +