# HG changeset patch # User hoelzl # Date 1354640440 -3600 # Node ID 4b4fe0d5ee227aa5740573eafd116a67f8f0ab84 # Parent 77e3effa50b6710a414216383a6075eb7d7066d6 remove SMT proofs in Multivariate_Analysis diff -r 77e3effa50b6 -r 4b4fe0d5ee22 src/HOL/Multivariate_Analysis/Integration.certs --- 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 diff -r 77e3effa50b6 -r 4b4fe0d5ee22 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ 'b::euclidean_space" assumes "(f has_integral i) s" "(g has_integral j) s" "\x\s. (f x)$$k \ (g x)$$k" shows "i$$k \ j$$k" -proof- have lem:"\a b i (j::'b). \g f::'a \ 'b. (f has_integral i) ({a..b}) \ +proof - + have lem:"\a b i (j::'b). \g f::'a \ 'b. (f has_integral i) ({a..b}) \ (g has_integral j) ({a..b}) \ \x\{a..b}. (f x)$$k \ (g x)$$k \ i$$k \ 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 = "\a b. s = {a..b}" { presume "\ ?P \ ?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 *:"\w1 w2 j i::real .\w1 - i\ < (i - j) / 3 \ \w2 - j\ < (i - j) / 3 \ w1 \ w2 \ False" using [[z3_with_extensions]] by smt + have *:"\w1 w2 j i::real .\w1 - i\ < (i - j) / 3 \ \w2 - j\ < (i - j) / 3 \ w1 \ w2 \ 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 \ 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} \ {x. \x $$ k - c\ \ d}) \ 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 \ {x. \x $$ k - c\ \ d} |l. l \ snd ` p \ l \ {x. \x $$ k - c\ \ d} \ {}} \ 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 \ {x. \x $$ k - c\ \ d}" "(a, b) \ p" "l = snd (a, b)" @@ -3516,7 +3519,7 @@ proof safe fix x and e::real assume as:"x\k" "e>0" from k(2)[unfolded k content_eq_0] guess i .. hence i:"c$$i = d$$i" "i "(\\ j. if j = i then if c$$i \ (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 "\x'\\(s - {k}). x' \ x \ dist x' x < e" apply(rule_tac x=y in bexI) @@ -3524,7 +3527,8 @@ hence "d \ {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 \ 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 \ x" unfolding euclidean_eq[where 'a='a] using i by auto have *:"{..i. 0) {.. {a..b}" "ball 0 (max B1 B2) \ {c..d}" have **:"ball 0 B1 \ ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \ ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto have *:"\ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \ abs(gc - i) < e / 3 \ abs(ha - j) < e / 3 \ - abs(hc - j) < e / 3 \ abs(i - j) < e / 3 \ ga \ fa \ fa \ ha \ gc \ fc \ fc \ hc\ abs(fa - fc) < e" using [[z3_with_extensions]] by smt + abs(hc - j) < e / 3 \ abs(i - j) < e / 3 \ ga \ fa \ fa \ ha \ gc \ fc \ fc \ hc\ abs(fa - fc) < e" + by (simp add: abs_real_def split: split_if_asm) show "norm (integral {a..b} (\x. if x \ s then f x else 0) - integral {c..d} (\x. if x \ 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 diff -r 77e3effa50b6 -r 4b4fe0d5ee22 src/HOL/ROOT --- 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" +