src/HOL/Multivariate_Analysis/Integration.certs
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 43555 93c1fc6ac527
child 49996 64c8d9d3af18
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     1
8d81ff6f41bc1cff9f5c6454ee204d147f8e27b7 272 0
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 37156
diff changeset
     2
#2 := false
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     3
#48 := 0::Real
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     4
decl f17 :: (-> S3 S10 Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     5
decl f18 :: S10
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     6
#43 := f18
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 37156
diff changeset
     7
decl f4 :: S3
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 37156
diff changeset
     8
#8 := f4
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
     9
#58 := (f17 f4 f18)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    10
#94 := -1::Real
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    11
#138 := (* -1::Real #58)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
    12
decl f5 :: (-> S4 S5 Real)
40163
a462d5207aa6 changed SMT configuration options; updated SMT certificates
boehmes
parents: 37489
diff changeset
    13
decl f8 :: S5
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
    14
#14 := f8
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    15
decl f20 :: S4
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    16
#54 := f20
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    17
#55 := (f5 f20 f8)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    18
#139 := (+ #55 #138)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    19
#122 := (* -1::Real #55)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    20
#129 := (+ #122 #58)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    21
#189 := (<= #139 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    22
#196 := (ite #189 #129 #139)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    23
#372 := (* -1::Real #196)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    24
#373 := (+ #129 #372)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    25
#374 := (<= #373 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    26
#356 := (= #129 #196)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
    27
decl f19 :: S4
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    28
#45 := f19
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    29
#46 := (f5 f19 f8)
40163
a462d5207aa6 changed SMT configuration options; updated SMT certificates
boehmes
parents: 37489
diff changeset
    30
decl f9 :: S3
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
    31
#18 := f9
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    32
#44 := (f17 f9 f18)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    33
#105 := (* -1::Real #44)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    34
#106 := (+ #105 #46)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    35
#95 := (* -1::Real #46)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    36
#96 := (+ #44 #95)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    37
#224 := (>= #96 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    38
#231 := (ite #224 #96 #106)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    39
#368 := (* -1::Real #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    40
#371 := (+ #106 #368)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    41
#375 := (<= #371 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    42
#363 := (= #106 #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    43
#225 := (not #224)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    44
#376 := [hypothesis]: #224
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    45
#182 := (+ #44 #138)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    46
#183 := (<= #182 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    47
#207 := -3::Real
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    48
#242 := (* -3::Real #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    49
#243 := (+ #122 #242)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    50
#244 := (+ #46 #243)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    51
#245 := (<= #244 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    52
#208 := (* -3::Real #196)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    53
#209 := (+ #122 #208)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    54
#210 := (+ #46 #209)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    55
#211 := (<= #210 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    56
#186 := (not #183)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    57
#264 := (or #186 #211 #245)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    58
#269 := (not #264)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    59
#65 := (<= #44 #58)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    60
#66 := (implies #65 false)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    61
#56 := (- #46 #55)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    62
#52 := 3::Real
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    63
#59 := (- #58 #55)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    64
#61 := (- #59)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    65
#60 := (< #59 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    66
#62 := (ite #60 #61 #59)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    67
#63 := (* #62 3::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    68
#64 := (< #63 #56)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    69
#67 := (implies #64 #66)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    70
#47 := (- #44 #46)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    71
#50 := (- #47)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    72
#49 := (< #47 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    73
#51 := (ite #49 #50 #47)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    74
#53 := (* #51 3::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    75
#57 := (< #53 #56)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    76
#68 := (implies #57 #67)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    77
#69 := (not #68)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    78
#272 := (iff #69 #269)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    79
#123 := (+ #46 #122)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    80
#132 := (< #129 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    81
#144 := (ite #132 #139 #129)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    82
#150 := (* 3::Real #144)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    83
#155 := (< #150 #123)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    84
#164 := (not #155)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    85
#158 := (not #65)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    86
#165 := (or #158 #164)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    87
#99 := (< #96 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    88
#111 := (ite #99 #106 #96)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    89
#117 := (* 3::Real #111)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    90
#126 := (< #117 #123)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    91
#173 := (not #126)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    92
#174 := (or #173 #165)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    93
#179 := (not #174)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    94
#270 := (iff #179 #269)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    95
#267 := (iff #174 #264)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    96
#258 := (or #186 #211)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    97
#261 := (or #245 #258)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    98
#265 := (iff #261 #264)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
    99
#266 := [rewrite]: #265
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   100
#262 := (iff #174 #261)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   101
#259 := (iff #165 #258)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   102
#222 := (iff #164 #211)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   103
#212 := (not #211)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   104
#217 := (not #212)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   105
#220 := (iff #217 #211)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   106
#221 := [rewrite]: #220
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   107
#218 := (iff #164 #217)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   108
#215 := (iff #155 #212)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   109
#201 := (* 3::Real #196)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   110
#204 := (< #201 #123)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   111
#213 := (iff #204 #212)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   112
#214 := [rewrite]: #213
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   113
#205 := (iff #155 #204)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   114
#202 := (= #150 #201)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   115
#199 := (= #144 #196)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   116
#190 := (not #189)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   117
#193 := (ite #190 #139 #129)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   118
#197 := (= #193 #196)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   119
#198 := [rewrite]: #197
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   120
#194 := (= #144 #193)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   121
#191 := (iff #132 #190)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   122
#192 := [rewrite]: #191
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   123
#195 := [monotonicity #192]: #194
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   124
#200 := [trans #195 #198]: #199
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   125
#203 := [monotonicity #200]: #202
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   126
#206 := [monotonicity #203]: #205
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   127
#216 := [trans #206 #214]: #215
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   128
#219 := [monotonicity #216]: #218
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   129
#223 := [trans #219 #221]: #222
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   130
#187 := (iff #158 #186)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   131
#184 := (iff #65 #183)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   132
#185 := [rewrite]: #184
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   133
#188 := [monotonicity #185]: #187
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   134
#260 := [monotonicity #188 #223]: #259
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   135
#256 := (iff #173 #245)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   136
#246 := (not #245)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   137
#251 := (not #246)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   138
#254 := (iff #251 #245)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   139
#255 := [rewrite]: #254
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   140
#252 := (iff #173 #251)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   141
#249 := (iff #126 #246)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   142
#236 := (* 3::Real #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   143
#239 := (< #236 #123)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   144
#247 := (iff #239 #246)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   145
#248 := [rewrite]: #247
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   146
#240 := (iff #126 #239)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   147
#237 := (= #117 #236)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   148
#234 := (= #111 #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   149
#228 := (ite #225 #106 #96)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   150
#232 := (= #228 #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   151
#233 := [rewrite]: #232
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   152
#229 := (= #111 #228)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   153
#226 := (iff #99 #225)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   154
#227 := [rewrite]: #226
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   155
#230 := [monotonicity #227]: #229
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   156
#235 := [trans #230 #233]: #234
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   157
#238 := [monotonicity #235]: #237
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   158
#241 := [monotonicity #238]: #240
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   159
#250 := [trans #241 #248]: #249
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   160
#253 := [monotonicity #250]: #252
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   161
#257 := [trans #253 #255]: #256
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   162
#263 := [monotonicity #257 #260]: #262
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   163
#268 := [trans #263 #266]: #267
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   164
#271 := [monotonicity #268]: #270
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   165
#180 := (iff #69 #179)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   166
#177 := (iff #68 #174)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   167
#170 := (implies #126 #165)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   168
#175 := (iff #170 #174)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   169
#176 := [rewrite]: #175
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   170
#171 := (iff #68 #170)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   171
#168 := (iff #67 #165)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   172
#161 := (implies #155 #158)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   173
#166 := (iff #161 #165)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   174
#167 := [rewrite]: #166
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   175
#162 := (iff #67 #161)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   176
#159 := (iff #66 #158)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   177
#160 := [rewrite]: #159
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   178
#156 := (iff #64 #155)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   179
#124 := (= #56 #123)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   180
#125 := [rewrite]: #124
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   181
#153 := (= #63 #150)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   182
#147 := (* #144 3::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   183
#151 := (= #147 #150)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   184
#152 := [rewrite]: #151
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   185
#148 := (= #63 #147)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   186
#145 := (= #62 #144)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   187
#130 := (= #59 #129)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   188
#131 := [rewrite]: #130
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   189
#142 := (= #61 #139)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   190
#135 := (- #129)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   191
#140 := (= #135 #139)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   192
#141 := [rewrite]: #140
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   193
#136 := (= #61 #135)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   194
#137 := [monotonicity #131]: #136
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   195
#143 := [trans #137 #141]: #142
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   196
#133 := (iff #60 #132)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   197
#134 := [monotonicity #131]: #133
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   198
#146 := [monotonicity #134 #143 #131]: #145
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   199
#149 := [monotonicity #146]: #148
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   200
#154 := [trans #149 #152]: #153
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   201
#157 := [monotonicity #154 #125]: #156
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   202
#163 := [monotonicity #157 #160]: #162
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   203
#169 := [trans #163 #167]: #168
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   204
#127 := (iff #57 #126)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   205
#120 := (= #53 #117)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   206
#114 := (* #111 3::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   207
#118 := (= #114 #117)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   208
#119 := [rewrite]: #118
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   209
#115 := (= #53 #114)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   210
#112 := (= #51 #111)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   211
#97 := (= #47 #96)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   212
#98 := [rewrite]: #97
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   213
#109 := (= #50 #106)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   214
#102 := (- #96)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   215
#107 := (= #102 #106)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   216
#108 := [rewrite]: #107
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   217
#103 := (= #50 #102)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   218
#104 := [monotonicity #98]: #103
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   219
#110 := [trans #104 #108]: #109
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   220
#100 := (iff #49 #99)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   221
#101 := [monotonicity #98]: #100
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   222
#113 := [monotonicity #101 #110 #98]: #112
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   223
#116 := [monotonicity #113]: #115
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   224
#121 := [trans #116 #119]: #120
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   225
#128 := [monotonicity #121 #125]: #127
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   226
#172 := [monotonicity #128 #169]: #171
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   227
#178 := [trans #172 #176]: #177
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   228
#181 := [monotonicity #178]: #180
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   229
#273 := [trans #181 #271]: #272
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   230
#93 := [asserted]: #69
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   231
#274 := [mp #93 #273]: #269
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   232
#275 := [not-or-elim #274]: #183
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   233
#277 := [not-or-elim #274]: #246
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   234
#369 := (+ #96 #368)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   235
#370 := (<= #369 0::Real)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   236
#362 := (= #96 #231)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   237
#364 := (or #225 #362)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   238
#365 := [def-axiom]: #364
41233
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   239
#388 := [unit-resolution #365 #376]: #362
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   240
#389 := (not #362)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   241
#390 := (or #389 #370)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   242
#391 := [th-lemma arith triangle-eq]: #390
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   243
#392 := [unit-resolution #391 #388]: #370
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   244
#384 := (or #190 #225)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   245
#377 := [hypothesis]: #189
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   246
#276 := [not-or-elim #274]: #212
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   247
#358 := (or #190 #356)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   248
#359 := [def-axiom]: #358
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   249
#378 := [unit-resolution #359 #377]: #356
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   250
#379 := (not #356)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   251
#380 := (or #379 #374)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   252
#381 := [th-lemma arith triangle-eq]: #380
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   253
#382 := [unit-resolution #381 #378]: #374
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   254
#383 := [th-lemma arith farkas -1 -3 1 -2 1 #275 #382 #276 #377 #376]: false
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   255
#385 := [lemma #383]: #384
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   256
#393 := [unit-resolution #385 #376]: #190
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   257
#394 := [th-lemma arith farkas 1/4 -3/4 1/4 -1/4 1 #393 #392 #277 #275 #376]: false
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   258
#395 := [lemma #394]: #225
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   259
#366 := (or #224 #363)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   260
#367 := [def-axiom]: #366
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   261
#396 := [unit-resolution #367 #395]: #363
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   262
#397 := (not #363)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   263
#398 := (or #397 #375)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   264
#399 := [th-lemma arith triangle-eq]: #398
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   265
#400 := [unit-resolution #399 #396]: #375
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   266
#401 := (not #375)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   267
#402 := (or #189 #401 #245 #186 #224)
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   268
#403 := [th-lemma arith assign-bounds 3 1 1 2]: #402
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   269
#404 := [unit-resolution #403 #275 #395 #277 #400]: #189
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   270
#405 := [unit-resolution #359 #404]: #356
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   271
#406 := [unit-resolution #381 #405]: #374
d4cb4d0c14a7 updated SMT certificates
boehmes
parents: 41132
diff changeset
   272
[th-lemma arith farkas 2 2/3 1 1 1/3 1 #400 #277 #275 #395 #276 #406]: false
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 37156
diff changeset
   273
unsat
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   274
a66e77fbacece8ec9b71617769b478381e4da6e9 349 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   275
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   276
#11 := 0::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   277
decl ?v3!0 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   278
#227 := ?v3!0
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   279
decl ?v0!3 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   280
#226 := ?v0!3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   281
#48 := -1::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   282
#229 := (* -1::Real ?v0!3)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   283
#230 := (+ #229 ?v3!0)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   284
#231 := (* -1::Real ?v3!0)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   285
#232 := (+ ?v0!3 #231)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   286
#233 := (>= #232 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   287
#234 := (ite #233 #232 #230)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   288
#235 := (* -1::Real #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   289
#394 := (+ #230 #235)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   290
#395 := (<= #394 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   291
#378 := (= #230 #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   292
#379 := (not #233)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   293
decl ?v2!1 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   294
#228 := ?v2!1
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   295
decl ?v1!2 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   296
#225 := ?v1!2
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   297
#241 := (* -1::Real ?v1!2)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   298
#278 := (+ #241 ?v2!1)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   299
#243 := (* -1::Real ?v2!1)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   300
#284 := (+ ?v1!2 #243)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   301
#285 := (>= #284 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   302
#292 := (ite #285 #284 #278)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   303
#295 := (* -1::Real #292)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   304
#393 := (+ #278 #295)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   305
#396 := (<= #393 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   306
#385 := (= #278 #292)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   307
#386 := (not #285)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   308
#397 := [hypothesis]: #285
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   309
#405 := (or #379 #386)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   310
#77 := -1/3::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   311
#236 := (* -1/3::Real ?v2!1)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   312
#298 := (+ #236 #295)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   313
#75 := 1/3::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   314
#238 := (* 1/3::Real ?v3!0)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   315
#301 := (+ #238 #298)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   316
#304 := (<= #301 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   317
#320 := (not #304)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   318
#269 := (+ ?v1!2 #229)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   319
#270 := (>= #269 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   320
#275 := (not #270)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   321
#237 := (+ #236 #235)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   322
#239 := (+ #238 #237)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   323
#240 := (<= #239 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   324
#310 := (or #240 #275 #304)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   325
#315 := (not #310)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   326
#242 := (+ ?v2!1 #241)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   327
#244 := (+ #243 ?v1!2)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   328
#245 := (<= #242 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   329
#246 := (ite #245 #244 #242)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   330
#247 := (* -1::Real #246)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   331
#248 := (+ #236 #247)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   332
#249 := (+ #238 #248)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   333
#250 := (<= #249 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   334
#251 := (+ ?v0!3 #241)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   335
#252 := (<= #251 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   336
#253 := (not #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   337
#254 := (or #253 #250 #240)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   338
#255 := (not #254)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   339
#316 := (iff #255 #315)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   340
#313 := (iff #254 #310)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   341
#307 := (or #275 #304 #240)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   342
#311 := (iff #307 #310)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   343
#312 := [rewrite]: #311
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   344
#308 := (iff #254 #307)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   345
#305 := (iff #250 #304)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   346
#302 := (= #249 #301)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   347
#299 := (= #248 #298)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   348
#296 := (= #247 #295)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   349
#293 := (= #246 #292)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   350
#279 := (= #242 #278)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   351
#280 := [rewrite]: #279
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   352
#290 := (= #244 #284)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   353
#291 := [rewrite]: #290
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   354
#288 := (iff #245 #285)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   355
#281 := (<= #278 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   356
#286 := (iff #281 #285)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   357
#287 := [rewrite]: #286
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   358
#282 := (iff #245 #281)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   359
#283 := [monotonicity #280]: #282
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   360
#289 := [trans #283 #287]: #288
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   361
#294 := [monotonicity #289 #291 #280]: #293
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   362
#297 := [monotonicity #294]: #296
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   363
#300 := [monotonicity #297]: #299
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   364
#303 := [monotonicity #300]: #302
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   365
#306 := [monotonicity #303]: #305
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   366
#276 := (iff #253 #275)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   367
#273 := (iff #252 #270)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   368
#263 := (+ #241 ?v0!3)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   369
#266 := (<= #263 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   370
#271 := (iff #266 #270)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   371
#272 := [rewrite]: #271
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   372
#267 := (iff #252 #266)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   373
#264 := (= #251 #263)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   374
#265 := [rewrite]: #264
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   375
#268 := [monotonicity #265]: #267
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   376
#274 := [trans #268 #272]: #273
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   377
#277 := [monotonicity #274]: #276
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   378
#309 := [monotonicity #277 #306]: #308
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   379
#314 := [trans #309 #312]: #313
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   380
#317 := [monotonicity #314]: #316
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   381
#9 := (:var 0 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   382
#8 := (:var 3 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   383
#59 := (* -1::Real #8)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   384
#60 := (+ #59 #9)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   385
#49 := (* -1::Real #9)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   386
#50 := (+ #8 #49)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   387
#173 := (>= #50 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   388
#180 := (ite #173 #50 #60)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   389
#188 := (* -1::Real #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   390
#15 := (:var 1 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   391
#78 := (* -1/3::Real #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   392
#189 := (+ #78 #188)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   393
#76 := (* 1/3::Real #9)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   394
#190 := (+ #76 #189)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   395
#191 := (<= #190 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   396
#20 := (:var 2 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   397
#96 := (* -1::Real #20)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   398
#97 := (+ #15 #96)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   399
#68 := (* -1::Real #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   400
#87 := (+ #68 #20)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   401
#142 := (<= #97 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   402
#149 := (ite #142 #87 #97)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   403
#157 := (* -1::Real #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   404
#158 := (+ #78 #157)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   405
#159 := (+ #76 #158)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   406
#160 := (<= #159 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   407
#135 := (+ #8 #96)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   408
#136 := (<= #135 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   409
#139 := (not #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   410
#210 := (or #139 #160 #191)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   411
#215 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #210)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   412
#218 := (not #215)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   413
#256 := (~ #218 #255)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   414
#257 := [sk]: #256
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   415
#26 := (<= #8 #20)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   416
#27 := (implies #26 false)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   417
#17 := 3::Real
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   418
#16 := (- #9 #15)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   419
#18 := (/ #16 3::Real)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   420
#21 := (- #20 #15)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   421
#23 := (- #21)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   422
#22 := (< #21 0::Real)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   423
#24 := (ite #22 #23 #21)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   424
#25 := (< #24 #18)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   425
#28 := (implies #25 #27)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   426
#10 := (- #8 #9)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   427
#13 := (- #10)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   428
#12 := (< #10 0::Real)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   429
#14 := (ite #12 #13 #10)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   430
#19 := (< #14 #18)
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   431
#29 := (implies #19 #28)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   432
#30 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #29)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   433
#31 := (not #30)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   434
#221 := (iff #31 #218)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   435
#79 := (+ #76 #78)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   436
#90 := (< #87 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   437
#102 := (ite #90 #97 #87)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   438
#105 := (< #102 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   439
#114 := (not #105)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   440
#108 := (not #26)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   441
#115 := (or #108 #114)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   442
#53 := (< #50 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   443
#65 := (ite #53 #60 #50)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   444
#84 := (< #65 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   445
#123 := (not #84)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   446
#124 := (or #123 #115)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   447
#129 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   448
#132 := (not #129)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   449
#219 := (iff #132 #218)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   450
#216 := (iff #129 #215)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   451
#213 := (iff #124 #210)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   452
#204 := (or #139 #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   453
#207 := (or #191 #204)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   454
#211 := (iff #207 #210)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   455
#212 := [rewrite]: #211
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   456
#208 := (iff #124 #207)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   457
#205 := (iff #115 #204)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   458
#171 := (iff #114 #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   459
#161 := (not #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   460
#166 := (not #161)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   461
#169 := (iff #166 #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   462
#170 := [rewrite]: #169
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   463
#167 := (iff #114 #166)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   464
#164 := (iff #105 #161)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   465
#154 := (< #149 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   466
#162 := (iff #154 #161)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   467
#163 := [rewrite]: #162
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   468
#155 := (iff #105 #154)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   469
#152 := (= #102 #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   470
#143 := (not #142)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   471
#146 := (ite #143 #97 #87)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   472
#150 := (= #146 #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   473
#151 := [rewrite]: #150
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   474
#147 := (= #102 #146)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   475
#144 := (iff #90 #143)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   476
#145 := [rewrite]: #144
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   477
#148 := [monotonicity #145]: #147
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   478
#153 := [trans #148 #151]: #152
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   479
#156 := [monotonicity #153]: #155
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   480
#165 := [trans #156 #163]: #164
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   481
#168 := [monotonicity #165]: #167
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   482
#172 := [trans #168 #170]: #171
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   483
#140 := (iff #108 #139)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   484
#137 := (iff #26 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   485
#138 := [rewrite]: #137
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   486
#141 := [monotonicity #138]: #140
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   487
#206 := [monotonicity #141 #172]: #205
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   488
#202 := (iff #123 #191)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   489
#192 := (not #191)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   490
#197 := (not #192)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   491
#200 := (iff #197 #191)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   492
#201 := [rewrite]: #200
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   493
#198 := (iff #123 #197)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   494
#195 := (iff #84 #192)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   495
#185 := (< #180 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   496
#193 := (iff #185 #192)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   497
#194 := [rewrite]: #193
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   498
#186 := (iff #84 #185)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   499
#183 := (= #65 #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   500
#174 := (not #173)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   501
#177 := (ite #174 #60 #50)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   502
#181 := (= #177 #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   503
#182 := [rewrite]: #181
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   504
#178 := (= #65 #177)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   505
#175 := (iff #53 #174)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   506
#176 := [rewrite]: #175
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   507
#179 := [monotonicity #176]: #178
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   508
#184 := [trans #179 #182]: #183
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   509
#187 := [monotonicity #184]: #186
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   510
#196 := [trans #187 #194]: #195
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   511
#199 := [monotonicity #196]: #198
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   512
#203 := [trans #199 #201]: #202
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   513
#209 := [monotonicity #203 #206]: #208
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   514
#214 := [trans #209 #212]: #213
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   515
#217 := [quant-intro #214]: #216
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   516
#220 := [monotonicity #217]: #219
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   517
#133 := (iff #31 #132)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   518
#130 := (iff #30 #129)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   519
#127 := (iff #29 #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   520
#120 := (implies #84 #115)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   521
#125 := (iff #120 #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   522
#126 := [rewrite]: #125
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   523
#121 := (iff #29 #120)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   524
#118 := (iff #28 #115)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   525
#111 := (implies #105 #108)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   526
#116 := (iff #111 #115)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   527
#117 := [rewrite]: #116
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   528
#112 := (iff #28 #111)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   529
#109 := (iff #27 #108)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   530
#110 := [rewrite]: #109
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   531
#106 := (iff #25 #105)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   532
#82 := (= #18 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   533
#69 := (+ #9 #68)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   534
#72 := (/ #69 3::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   535
#80 := (= #72 #79)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   536
#81 := [rewrite]: #80
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   537
#73 := (= #18 #72)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   538
#70 := (= #16 #69)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   539
#71 := [rewrite]: #70
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   540
#74 := [monotonicity #71]: #73
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   541
#83 := [trans #74 #81]: #82
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   542
#103 := (= #24 #102)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   543
#88 := (= #21 #87)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   544
#89 := [rewrite]: #88
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   545
#100 := (= #23 #97)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   546
#93 := (- #87)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   547
#98 := (= #93 #97)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   548
#99 := [rewrite]: #98
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   549
#94 := (= #23 #93)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   550
#95 := [monotonicity #89]: #94
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   551
#101 := [trans #95 #99]: #100
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   552
#91 := (iff #22 #90)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   553
#92 := [monotonicity #89]: #91
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   554
#104 := [monotonicity #92 #101 #89]: #103
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   555
#107 := [monotonicity #104 #83]: #106
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   556
#113 := [monotonicity #107 #110]: #112
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   557
#119 := [trans #113 #117]: #118
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   558
#85 := (iff #19 #84)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   559
#66 := (= #14 #65)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   560
#51 := (= #10 #50)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   561
#52 := [rewrite]: #51
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   562
#63 := (= #13 #60)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   563
#56 := (- #50)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   564
#61 := (= #56 #60)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   565
#62 := [rewrite]: #61
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   566
#57 := (= #13 #56)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   567
#58 := [monotonicity #52]: #57
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   568
#64 := [trans #58 #62]: #63
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   569
#54 := (iff #12 #53)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   570
#55 := [monotonicity #52]: #54
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   571
#67 := [monotonicity #55 #64 #52]: #66
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   572
#86 := [monotonicity #67 #83]: #85
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   573
#122 := [monotonicity #86 #119]: #121
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   574
#128 := [trans #122 #126]: #127
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   575
#131 := [quant-intro #128]: #130
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   576
#134 := [monotonicity #131]: #133
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   577
#222 := [trans #134 #220]: #221
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   578
#47 := [asserted]: #31
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   579
#223 := [mp #47 #222]: #218
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   580
#260 := [mp~ #223 #257]: #255
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   581
#261 := [mp #260 #317]: #315
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   582
#321 := [not-or-elim #261]: #320
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   583
#391 := (+ #284 #295)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   584
#392 := (<= #391 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   585
#384 := (= #284 #292)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   586
#387 := (or #386 #384)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   587
#388 := [def-axiom]: #387
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   588
#398 := [unit-resolution #388 #397]: #384
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   589
#399 := (not #384)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   590
#400 := (or #399 #392)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   591
#401 := [th-lemma arith triangle-eq]: #400
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   592
#402 := [unit-resolution #401 #398]: #392
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   593
#403 := [hypothesis]: #233
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   594
#319 := [not-or-elim #261]: #270
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   595
#404 := [th-lemma arith farkas 1/2 1/2 3/2 3/2 1 #319 #403 #402 #321 #397]: false
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   596
#406 := [lemma #404]: #405
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   597
#407 := [unit-resolution #406 #397]: #379
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   598
#262 := (not #240)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   599
#318 := [not-or-elim #261]: #262
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   600
#382 := (or #233 #378)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   601
#383 := [def-axiom]: #382
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   602
#408 := [unit-resolution #383 #407]: #378
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   603
#409 := (not #378)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   604
#410 := (or #409 #395)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   605
#411 := [th-lemma arith triangle-eq]: #410
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   606
#412 := [unit-resolution #411 #408]: #395
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   607
#413 := [th-lemma arith farkas 2 2 1 1 1 1 #412 #318 #402 #321 #319 #407]: false
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   608
#414 := [lemma #413]: #386
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   609
#389 := (or #285 #385)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   610
#390 := [def-axiom]: #389
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   611
#417 := [unit-resolution #390 #414]: #385
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   612
#418 := (not #385)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   613
#419 := (or #418 #396)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   614
#420 := [th-lemma arith triangle-eq]: #419
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   615
#421 := [unit-resolution #420 #417]: #396
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   616
#422 := (not #396)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   617
#423 := (or #379 #422 #275 #304 #285)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   618
#424 := [th-lemma arith assign-bounds 3 1 3 4]: #423
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   619
#425 := [unit-resolution #424 #319 #414 #321 #421]: #379
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   620
#426 := [unit-resolution #383 #425]: #378
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   621
#427 := [unit-resolution #411 #426]: #395
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   622
[th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   623
unsat
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   624
9e23136a6273b9d99bb60a03d2e785bc24c9efdf 59 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   625
#2 := false
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   626
#42 := 0::Real
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   627
decl f12 :: (-> S5 Real)
41064
0c447a17770a updated SMT certificates
boehmes
parents: 40333
diff changeset
   628
decl f13 :: (-> S4 S4 S5)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   629
decl f14 :: (-> S6 S3 S4)
41282
a4d1b5eef12e updated SMT certificates
boehmes
parents: 41233
diff changeset
   630
decl f4 :: S3
a4d1b5eef12e updated SMT certificates
boehmes
parents: 41233
diff changeset
   631
#8 := f4
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   632
decl f15 :: S6
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   633
#37 := f15
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   634
#39 := (f14 f15 f4)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   635
decl f10 :: S3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   636
#25 := f10
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   637
#38 := (f14 f15 f10)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   638
#40 := (f13 #38 #39)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   639
#41 := (f12 #40)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   640
#249 := (>= #41 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   641
#251 := (not #249)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   642
#50 := (= #41 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   643
#51 := (not #50)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   644
#135 := [asserted]: #51
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   645
#257 := (or #50 #251)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   646
#43 := (<= #41 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   647
#133 := [asserted]: #43
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   648
#250 := (not #43)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   649
#255 := (or #50 #250 #251)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   650
#256 := [th-lemma arith triangle-eq]: #255
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   651
#258 := [unit-resolution #256 #133]: #257
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   652
#259 := [unit-resolution #258 #135]: #251
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   653
#45 := (:var 0 S4)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   654
#44 := (:var 1 S4)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   655
#46 := (f13 #44 #45)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   656
#242 := (pattern #46)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   657
#47 := (f12 #46)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   658
#138 := (>= #47 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   659
#243 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #242) #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   660
#140 := (forall (vars (?v0 S4) (?v1 S4)) #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   661
#246 := (iff #140 #243)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   662
#244 := (iff #138 #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   663
#245 := [refl]: #244
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   664
#247 := [quant-intro #245]: #246
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   665
#156 := (~ #140 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   666
#144 := (~ #138 #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   667
#145 := [refl]: #144
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   668
#157 := [nnf-pos #145]: #156
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   669
#48 := (<= 0::Real #47)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   670
#49 := (forall (vars (?v0 S4) (?v1 S4)) #48)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   671
#141 := (iff #49 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   672
#137 := (iff #48 #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   673
#139 := [rewrite]: #137
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   674
#142 := [quant-intro #139]: #141
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   675
#134 := [asserted]: #49
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   676
#143 := [mp #134 #142]: #140
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   677
#158 := [mp~ #143 #157]: #140
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   678
#248 := [mp #158 #247]: #243
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   679
#252 := (not #243)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   680
#253 := (or #252 #249)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   681
#254 := [quant-inst #38 #39]: #253
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   682
[unit-resolution #254 #248 #259]: false
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   683
unsat
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   684
10ecdce54c6fd7d6b28756c68a32c55633241d44 222 0
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   685
#2 := false
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   686
#33 := 0::Real
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   687
decl f3 :: (-> S2 S3 Real)
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   688
decl f5 :: S3
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   689
#9 := f5
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   690
decl f12 :: S2
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   691
#25 := f12
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   692
#36 := (f3 f12 f5)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   693
#105 := -1::Real
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   694
#351 := (* -1::Real #36)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   695
decl f6 :: S2
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   696
#11 := f6
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   697
#12 := (f3 f6 f5)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   698
#377 := (+ #12 #351)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   699
#378 := (>= #377 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   700
#383 := (not #378)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   701
decl f4 :: S2
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   702
#8 := f4
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   703
#10 := (f3 f4 f5)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   704
#352 := (+ #10 #351)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   705
#353 := (<= #352 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   706
#354 := (not #353)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   707
#386 := (or #354 #383)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   708
#389 := (not #386)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   709
#21 := (:var 0 S3)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   710
#28 := (f3 f6 #21)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   711
#321 := (pattern #28)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   712
#26 := (f3 f12 #21)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   713
#320 := (pattern #26)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   714
#24 := (f3 f4 #21)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   715
#319 := (pattern #24)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   716
decl f7 :: (-> S4 S3 Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   717
decl f8 :: S4
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   718
#14 := f8
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   719
#22 := (f7 f8 #21)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   720
#318 := (pattern #22)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   721
#111 := (* -1::Real #28)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   722
#112 := (+ #26 #111)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   723
#113 := (<= #112 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   724
#249 := (not #113)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   725
#106 := (* -1::Real #26)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   726
#107 := (+ #24 #106)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   727
#108 := (<= #107 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   728
#248 := (not #108)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   729
#250 := (or #248 #249)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   730
#251 := (not #250)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   731
#43 := 0::Int
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   732
#78 := -1::Int
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   733
#92 := (* -1::Int #22)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   734
decl f9 :: (-> S5 S6 S3)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   735
decl f11 :: S6
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   736
#17 := f11
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   737
decl f10 :: S5
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   738
#16 := f10
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   739
#18 := (f9 f10 f11)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   740
#19 := (f7 f8 #18)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   741
#93 := (+ #19 #92)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   742
#94 := (<= #93 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   743
#254 := (or #94 #251)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   744
#322 := (forall (vars (?v0 S3)) (:pat #318 #319 #320 #321) #254)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   745
#257 := (forall (vars (?v0 S3)) #254)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   746
#325 := (iff #257 #322)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   747
#323 := (iff #254 #254)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   748
#324 := [refl]: #323
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   749
#326 := [quant-intro #324]: #325
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   750
#116 := (and #108 #113)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   751
#119 := (or #94 #116)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   752
#122 := (forall (vars (?v0 S3)) #119)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   753
#258 := (iff #122 #257)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   754
#255 := (iff #119 #254)
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   755
#252 := (iff #116 #251)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   756
#253 := [rewrite]: #252
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   757
#256 := [monotonicity #253]: #255
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   758
#259 := [quant-intro #256]: #258
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   759
#242 := (~ #122 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   760
#244 := (~ #119 #119)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   761
#245 := [refl]: #244
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   762
#243 := [nnf-pos #245]: #242
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   763
#29 := (<= #26 #28)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   764
#27 := (<= #24 #26)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   765
#30 := (and #27 #29)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   766
#23 := (< #22 #19)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   767
#31 := (implies #23 #30)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   768
#32 := (forall (vars (?v0 S3)) #31)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   769
#125 := (iff #32 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   770
#77 := (not #23)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   771
#86 := (or #77 #30)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   772
#89 := (forall (vars (?v0 S3)) #86)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   773
#123 := (iff #89 #122)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   774
#120 := (iff #86 #119)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   775
#117 := (iff #30 #116)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   776
#114 := (iff #29 #113)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   777
#115 := [rewrite]: #114
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   778
#109 := (iff #27 #108)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   779
#110 := [rewrite]: #109
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   780
#118 := [monotonicity #110 #115]: #117
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   781
#103 := (iff #77 #94)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   782
#95 := (not #94)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   783
#98 := (not #95)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   784
#101 := (iff #98 #94)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   785
#102 := [rewrite]: #101
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   786
#99 := (iff #77 #98)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   787
#96 := (iff #23 #95)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   788
#97 := [rewrite]: #96
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   789
#100 := [monotonicity #97]: #99
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   790
#104 := [trans #100 #102]: #103
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   791
#121 := [monotonicity #104 #118]: #120
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   792
#124 := [quant-intro #121]: #123
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   793
#90 := (iff #32 #89)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   794
#87 := (iff #31 #86)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   795
#88 := [rewrite]: #87
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   796
#91 := [quant-intro #88]: #90
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   797
#126 := [trans #91 #124]: #125
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   798
#76 := [asserted]: #32
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   799
#127 := [mp #76 #126]: #122
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   800
#240 := [mp~ #127 #243]: #122
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   801
#260 := [mp #240 #259]: #257
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   802
#327 := [mp #260 #326]: #322
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   803
#81 := (* -1::Int #19)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   804
#15 := (f7 f8 f5)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   805
#82 := (+ #15 #81)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   806
#80 := (>= #82 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   807
#79 := (not #80)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   808
#20 := (< #15 #19)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   809
#83 := (iff #20 #79)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   810
#84 := [rewrite]: #83
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   811
#75 := [asserted]: #20
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   812
#85 := [mp #75 #84]: #79
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   813
#395 := (not #322)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   814
#396 := (or #395 #80 #389)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   815
#347 := (* -1::Real #12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   816
#348 := (+ #36 #347)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   817
#349 := (<= #348 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   818
#350 := (not #349)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   819
#355 := (or #354 #350)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   820
#356 := (not #355)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   821
#357 := (* -1::Int #15)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   822
#358 := (+ #19 #357)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   823
#359 := (<= #358 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   824
#360 := (or #359 #356)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   825
#397 := (or #395 #360)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   826
#404 := (iff #397 #396)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   827
#392 := (or #80 #389)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   828
#399 := (or #395 #392)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   829
#402 := (iff #399 #396)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   830
#403 := [rewrite]: #402
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   831
#400 := (iff #397 #399)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   832
#393 := (iff #360 #392)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   833
#390 := (iff #356 #389)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   834
#387 := (iff #355 #386)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   835
#384 := (iff #350 #383)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   836
#381 := (iff #349 #378)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   837
#371 := (+ #347 #36)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   838
#374 := (<= #371 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   839
#379 := (iff #374 #378)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   840
#380 := [rewrite]: #379
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   841
#375 := (iff #349 #374)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   842
#372 := (= #348 #371)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   843
#373 := [rewrite]: #372
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   844
#376 := [monotonicity #373]: #375
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   845
#382 := [trans #376 #380]: #381
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   846
#385 := [monotonicity #382]: #384
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   847
#388 := [monotonicity #385]: #387
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   848
#391 := [monotonicity #388]: #390
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   849
#369 := (iff #359 #80)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   850
#361 := (+ #357 #19)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   851
#364 := (<= #361 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   852
#367 := (iff #364 #80)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   853
#368 := [rewrite]: #367
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   854
#365 := (iff #359 #364)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   855
#362 := (= #358 #361)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   856
#363 := [rewrite]: #362
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   857
#366 := [monotonicity #363]: #365
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   858
#370 := [trans #366 #368]: #369
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   859
#394 := [monotonicity #370 #391]: #393
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   860
#401 := [monotonicity #394]: #400
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   861
#405 := [trans #401 #403]: #404
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   862
#398 := [quant-inst #9]: #397
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   863
#406 := [mp #398 #405]: #396
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   864
#533 := [unit-resolution #406 #85 #327]: #389
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   865
#409 := (or #386 #378)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   866
#410 := [def-axiom]: #409
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   867
#534 := [unit-resolution #410 #533]: #378
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   868
#495 := (>= #352 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   869
#544 := (not #495)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   870
#494 := (= #10 #36)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   871
#539 := (not #494)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   872
#130 := (= #12 #36)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   873
#138 := (not #130)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   874
#540 := (iff #138 #539)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   875
#537 := (iff #130 #494)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   876
#535 := (iff #494 #130)
43118
e3c7b07704bc updated SMT certificates
boehmes
parents: 41282
diff changeset
   877
#13 := (= #10 #12)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   878
#74 := [asserted]: #13
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   879
#536 := [monotonicity #74]: #535
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   880
#538 := [symm #536]: #537
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   881
#541 := [monotonicity #538]: #540
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   882
#37 := (= #36 #12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   883
#38 := (not #37)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   884
#139 := (iff #38 #138)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   885
#136 := (iff #37 #130)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   886
#137 := [rewrite]: #136
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   887
#140 := [monotonicity #137]: #139
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   888
#129 := [asserted]: #38
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   889
#143 := [mp #129 #140]: #138
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   890
#542 := [mp #143 #541]: #539
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   891
#547 := (or #494 #544)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   892
#407 := (or #386 #353)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   893
#408 := [def-axiom]: #407
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   894
#543 := [unit-resolution #408 #533]: #353
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   895
#545 := (or #494 #354 #544)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   896
#546 := [th-lemma arith triangle-eq]: #545
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   897
#548 := [unit-resolution #546 #543]: #547
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   898
#549 := [unit-resolution #548 #542]: #544
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   899
#489 := (+ #10 #347)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   900
#493 := (>= #489 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   901
#550 := (not #13)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   902
#551 := (or #550 #493)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   903
#552 := [th-lemma arith triangle-eq]: #551
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   904
#553 := [unit-resolution #552 #74]: #493
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   905
[th-lemma arith farkas 1 -1 1 #553 #549 #534]: false
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   906
unsat
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   907
c1e03e8f48834847dc1db09cf1e1405081da91b1 355 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   908
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   909
#8 := 0::Real
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   910
decl f9 :: (-> S6 S2 Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   911
decl f12 :: S2
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   912
#27 := f12
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   913
decl f10 :: S6
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   914
#19 := f10
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   915
#34 := (f9 f10 f12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   916
decl f13 :: S6
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   917
#31 := f13
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   918
#32 := (f9 f13 f12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   919
#103 := -1::Real
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   920
#139 := (* -1::Real #32)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   921
#140 := (+ #139 #34)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   922
decl f3 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   923
#9 := f3
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   924
#200 := (* -1::Real #34)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   925
#201 := (+ #32 #200)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   926
#202 := (+ f3 #201)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   927
#203 := (<= #202 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   928
#206 := (ite #203 f3 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   929
#633 := (* -1::Real #206)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   930
#634 := (+ f3 #633)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   931
#635 := (<= #634 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   932
#642 := (not #635)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   933
#130 := 1/2::Real
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   934
#209 := (* 1/2::Real #206)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   935
#497 := (<= #209 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   936
#220 := (= #209 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   937
#237 := (<= #201 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   938
decl f11 :: S6
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   939
#21 := f11
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   940
#30 := (f9 f11 f12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   941
#233 := (+ #30 #139)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   942
#234 := (<= #233 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   943
#240 := (and #234 #237)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   944
#56 := 0::Int
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   945
decl f4 :: (-> S3 S2 Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   946
decl f5 :: S3
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   947
#11 := f5
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   948
#28 := (f4 f5 f12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   949
#96 := -1::Int
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   950
#120 := (* -1::Int #28)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   951
decl f6 :: (-> S4 S5 S2)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   952
decl f8 :: S5
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   953
#15 := f8
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   954
decl f7 :: S4
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   955
#14 := f7
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   956
#16 := (f6 f7 f8)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   957
#17 := (f4 f5 #16)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   958
#121 := (+ #17 #120)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   959
#122 := (<= #121 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   960
#243 := (or #122 #240)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   961
#246 := (not #243)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   962
#223 := (not #220)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   963
#132 := (* 1/2::Real #34)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   964
#197 := (+ #139 #132)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   965
#131 := (* 1/2::Real #30)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   966
#198 := (+ #131 #197)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   967
#195 := (>= #198 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   968
#193 := (not #195)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   969
#255 := (or #193 #223 #246)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   970
#260 := (not #255)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   971
#39 := 2::Real
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   972
#42 := (- #34 #32)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   973
#43 := (<= f3 #42)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   974
#44 := (ite #43 f3 #42)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   975
#45 := (/ #44 2::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   976
#46 := (+ #32 #45)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   977
#47 := (= #46 #32)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   978
#48 := (not #47)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   979
#38 := (+ #30 #34)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   980
#40 := (/ #38 2::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   981
#41 := (<= #32 #40)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   982
#49 := (implies #41 #48)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   983
#35 := (<= #32 #34)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   984
#33 := (<= #30 #32)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   985
#36 := (and #33 #35)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   986
#29 := (< #28 #17)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   987
#37 := (implies #29 #36)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   988
#50 := (implies #37 #49)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   989
#51 := (not #50)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   990
#263 := (iff #51 #260)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   991
#143 := (<= f3 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   992
#146 := (ite #143 f3 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   993
#152 := (* 1/2::Real #146)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   994
#157 := (+ #32 #152)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   995
#163 := (= #32 #157)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   996
#168 := (not #163)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   997
#133 := (+ #131 #132)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   998
#136 := (<= #32 #133)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
   999
#174 := (not #136)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1000
#175 := (or #174 #168)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1001
#119 := (not #29)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1002
#127 := (or #119 #36)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1003
#183 := (not #127)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1004
#184 := (or #183 #175)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1005
#189 := (not #184)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1006
#261 := (iff #189 #260)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1007
#258 := (iff #184 #255)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1008
#249 := (or #193 #223)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1009
#252 := (or #246 #249)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1010
#256 := (iff #252 #255)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1011
#257 := [rewrite]: #256
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1012
#253 := (iff #184 #252)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1013
#250 := (iff #175 #249)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1014
#224 := (iff #168 #223)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1015
#221 := (iff #163 #220)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1016
#212 := (+ #32 #209)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1017
#215 := (= #32 #212)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1018
#218 := (iff #215 #220)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1019
#219 := [rewrite]: #218
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1020
#216 := (iff #163 #215)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1021
#213 := (= #157 #212)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1022
#210 := (= #152 #209)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1023
#207 := (= #146 #206)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1024
#204 := (iff #143 #203)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1025
#205 := [rewrite]: #204
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1026
#208 := [monotonicity #205]: #207
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1027
#211 := [monotonicity #208]: #210
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1028
#214 := [monotonicity #211]: #213
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1029
#217 := [monotonicity #214]: #216
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1030
#222 := [trans #217 #219]: #221
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1031
#225 := [monotonicity #222]: #224
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1032
#196 := (iff #174 #193)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1033
#192 := (iff #136 #195)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1034
#194 := [rewrite]: #192
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1035
#199 := [monotonicity #194]: #196
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1036
#251 := [monotonicity #199 #225]: #250
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1037
#247 := (iff #183 #246)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1038
#244 := (iff #127 #243)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1039
#241 := (iff #36 #240)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1040
#238 := (iff #35 #237)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1041
#239 := [rewrite]: #238
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1042
#235 := (iff #33 #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1043
#236 := [rewrite]: #235
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1044
#242 := [monotonicity #236 #239]: #241
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1045
#231 := (iff #119 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1046
#123 := (not #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1047
#226 := (not #123)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1048
#229 := (iff #226 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1049
#230 := [rewrite]: #229
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1050
#227 := (iff #119 #226)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1051
#124 := (iff #29 #123)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1052
#125 := [rewrite]: #124
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1053
#228 := [monotonicity #125]: #227
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1054
#232 := [trans #228 #230]: #231
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1055
#245 := [monotonicity #232 #242]: #244
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1056
#248 := [monotonicity #245]: #247
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1057
#254 := [monotonicity #248 #251]: #253
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1058
#259 := [trans #254 #257]: #258
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1059
#262 := [monotonicity #259]: #261
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1060
#190 := (iff #51 #189)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1061
#187 := (iff #50 #184)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1062
#180 := (implies #127 #175)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1063
#185 := (iff #180 #184)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1064
#186 := [rewrite]: #185
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1065
#181 := (iff #50 #180)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1066
#178 := (iff #49 #175)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1067
#171 := (implies #136 #168)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1068
#176 := (iff #171 #175)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1069
#177 := [rewrite]: #176
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1070
#172 := (iff #49 #171)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1071
#169 := (iff #48 #168)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1072
#166 := (iff #47 #163)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1073
#160 := (= #157 #32)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1074
#164 := (iff #160 #163)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1075
#165 := [rewrite]: #164
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1076
#161 := (iff #47 #160)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1077
#158 := (= #46 #157)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1078
#155 := (= #45 #152)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1079
#149 := (/ #146 2::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1080
#153 := (= #149 #152)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1081
#154 := [rewrite]: #153
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1082
#150 := (= #45 #149)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1083
#147 := (= #44 #146)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1084
#141 := (= #42 #140)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1085
#142 := [rewrite]: #141
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1086
#144 := (iff #43 #143)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1087
#145 := [monotonicity #142]: #144
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1088
#148 := [monotonicity #145 #142]: #147
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1089
#151 := [monotonicity #148]: #150
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1090
#156 := [trans #151 #154]: #155
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1091
#159 := [monotonicity #156]: #158
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1092
#162 := [monotonicity #159]: #161
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1093
#167 := [trans #162 #165]: #166
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1094
#170 := [monotonicity #167]: #169
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1095
#137 := (iff #41 #136)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1096
#134 := (= #40 #133)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1097
#135 := [rewrite]: #134
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1098
#138 := [monotonicity #135]: #137
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1099
#173 := [monotonicity #138 #170]: #172
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1100
#179 := [trans #173 #177]: #178
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1101
#128 := (iff #37 #127)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1102
#129 := [rewrite]: #128
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1103
#182 := [monotonicity #129 #179]: #181
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1104
#188 := [trans #182 #186]: #187
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1105
#191 := [monotonicity #188]: #190
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1106
#264 := [trans #191 #262]: #263
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1107
#95 := [asserted]: #51
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1108
#265 := [mp #95 #264]: #260
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1109
#267 := [not-or-elim #265]: #220
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1110
#637 := (or #223 #497)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1111
#638 := [th-lemma arith triangle-eq]: #637
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1112
#639 := [unit-resolution #638 #267]: #497
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1113
#640 := [hypothesis]: #635
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1114
#90 := (<= f3 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1115
#91 := (not #90)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1116
#10 := (< 0::Real f3)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1117
#92 := (iff #10 #91)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1118
#93 := [rewrite]: #92
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1119
#87 := [asserted]: #10
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1120
#94 := [mp #87 #93]: #91
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1121
#641 := [th-lemma arith farkas -1/2 1/2 1 #94 #640 #639]: false
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1122
#643 := [lemma #641]: #642
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1123
#490 := (= f3 #206)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1124
#491 := (= #140 #206)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1125
#652 := (not #491)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1126
#636 := (+ #140 #633)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1127
#644 := (<= #636 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1128
#649 := (not #644)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1129
#568 := (+ #30 #200)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1130
#569 := (>= #568 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1131
#574 := (not #569)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1132
#89 := [asserted]: #29
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1133
#126 := [mp #89 #125]: #123
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1134
#12 := (:var 0 S2)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1135
#22 := (f9 f11 #12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1136
#464 := (pattern #22)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1137
#20 := (f9 f10 #12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1138
#463 := (pattern #20)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1139
#13 := (f4 f5 #12)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1140
#462 := (pattern #13)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1141
#104 := (* -1::Real #22)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1142
#105 := (+ #20 #104)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1143
#106 := (<= #105 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1144
#389 := (not #106)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1145
#99 := (* -1::Int #17)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1146
#100 := (+ #13 #99)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1147
#98 := (>= #100 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1148
#390 := (or #98 #389)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1149
#465 := (forall (vars (?v0 S2)) (:pat #462 #463 #464) #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1150
#401 := (forall (vars (?v0 S2)) #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1151
#468 := (iff #401 #465)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1152
#466 := (iff #390 #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1153
#467 := [refl]: #466
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1154
#469 := [quant-intro #467]: #468
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1155
#97 := (not #98)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1156
#109 := (and #97 #106)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1157
#381 := (not #109)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1158
#380 := (forall (vars (?v0 S2)) #381)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1159
#402 := (iff #380 #401)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1160
#399 := (iff #381 #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1161
#391 := (not #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1162
#394 := (not #391)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1163
#397 := (iff #394 #390)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1164
#398 := [rewrite]: #397
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1165
#395 := (iff #381 #394)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1166
#392 := (iff #109 #391)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1167
#393 := [rewrite]: #392
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1168
#396 := [monotonicity #393]: #395
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1169
#400 := [trans #396 #398]: #399
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1170
#403 := [quant-intro #400]: #402
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1171
#112 := (exists (vars (?v0 S2)) #109)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1172
#115 := (not #112)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1173
#377 := (~ #115 #380)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1174
#382 := (~ #381 #381)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1175
#379 := [refl]: #382
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1176
#378 := [nnf-neg #379]: #377
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1177
#23 := (<= #20 #22)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1178
#18 := (< #13 #17)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1179
#24 := (and #18 #23)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1180
#25 := (exists (vars (?v0 S2)) #24)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1181
#26 := (not #25)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1182
#116 := (iff #26 #115)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1183
#113 := (iff #25 #112)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1184
#110 := (iff #24 #109)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1185
#107 := (iff #23 #106)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1186
#108 := [rewrite]: #107
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1187
#101 := (iff #18 #97)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1188
#102 := [rewrite]: #101
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1189
#111 := [monotonicity #102 #108]: #110
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1190
#114 := [quant-intro #111]: #113
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1191
#117 := [monotonicity #114]: #116
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1192
#88 := [asserted]: #26
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1193
#118 := [mp #88 #117]: #115
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1194
#375 := [mp~ #118 #378]: #380
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1195
#404 := [mp #375 #403]: #401
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1196
#470 := [mp #404 #469]: #465
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1197
#580 := (not #465)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1198
#581 := (or #580 #122 #574)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1199
#542 := (* -1::Real #30)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1200
#543 := (+ #34 #542)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1201
#547 := (<= #543 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1202
#548 := (not #547)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1203
#549 := (+ #28 #99)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1204
#550 := (>= #549 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1205
#551 := (or #550 #548)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1206
#582 := (or #580 #551)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1207
#589 := (iff #582 #581)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1208
#577 := (or #122 #574)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1209
#584 := (or #580 #577)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1210
#587 := (iff #584 #581)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1211
#588 := [rewrite]: #587
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1212
#585 := (iff #582 #584)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1213
#578 := (iff #551 #577)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1214
#575 := (iff #548 #574)
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1215
#572 := (iff #547 #569)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1216
#562 := (+ #542 #34)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1217
#565 := (<= #562 0::Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1218
#570 := (iff #565 #569)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1219
#571 := [rewrite]: #570
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1220
#566 := (iff #547 #565)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1221
#563 := (= #543 #562)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1222
#564 := [rewrite]: #563
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1223
#567 := [monotonicity #564]: #566
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1224
#573 := [trans #567 #571]: #572
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1225
#576 := [monotonicity #573]: #575
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1226
#560 := (iff #550 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1227
#552 := (+ #99 #28)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1228
#555 := (>= #552 0::Int)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1229
#558 := (iff #555 #122)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1230
#559 := [rewrite]: #558
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1231
#556 := (iff #550 #555)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1232
#553 := (= #549 #552)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1233
#554 := [rewrite]: #553
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1234
#557 := [monotonicity #554]: #556
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1235
#561 := [trans #557 #559]: #560
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1236
#579 := [monotonicity #561 #576]: #578
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1237
#586 := [monotonicity #579]: #585
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1238
#590 := [trans #586 #588]: #589
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1239
#583 := [quant-inst #27]: #582
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1240
#591 := [mp #583 #590]: #581
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1241
#646 := [unit-resolution #591 #470 #126]: #574
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1242
#266 := [not-or-elim #265]: #195
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1243
#647 := [hypothesis]: #644
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1244
#648 := [th-lemma arith farkas 1/2 -1/2 1/4 1 #647 #266 #646 #639]: false
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1245
#650 := [lemma #648]: #649
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1246
#651 := [hypothesis]: #491
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1247
#653 := (or #652 #644)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1248
#654 := [th-lemma arith triangle-eq]: #653
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1249
#655 := [unit-resolution #654 #651 #650]: false
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1250
#656 := [lemma #655]: #652
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1251
#495 := (or #203 #491)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1252
#496 := [def-axiom]: #495
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1253
#657 := [unit-resolution #496 #656]: #203
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1254
#492 := (not #203)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1255
#493 := (or #492 #490)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1256
#494 := [def-axiom]: #493
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1257
#658 := [unit-resolution #494 #657]: #490
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1258
#659 := (not #490)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1259
#660 := (or #659 #635)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1260
#661 := [th-lemma arith triangle-eq]: #660
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1261
[unit-resolution #661 #658 #643]: false
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
  1262
unsat
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1263
a7c1eea206143dd61561c7993b895cfbb2daa5bc 335 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
  1264
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1265
#8 := 0::Real
43555
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1266
decl f9 :: (-> S6 S2 Real)
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1267
decl f12 :: S2
93c1fc6ac527 updated SMT certificates
boehmes
parents: 43273
diff changeset
  1268
#27 := f12
93c1fc6ac527 updated SMT certificates