src/HOL/Multivariate_Analysis/Integration.certs
author boehmes
Fri, 17 Dec 2010 14:59:06 +0100
changeset 41233 d4cb4d0c14a7
parent 41132 42384824b732
child 41282 a4d1b5eef12e
permissions -rw-r--r--
updated SMT certificates
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
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   624
f26ffd00d169b6b4684265a03d23c9e0efe94a58 57 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   625
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   626
#37 := 0::Real
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)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   629
decl f14 :: (-> S3 S4)
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   630
decl f10 :: S3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   631
#25 := f10
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   632
#45 := (f14 f10)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   633
decl f4 :: S3
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   634
#8 := f4
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   635
#44 := (f14 f4)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   636
#46 := (f13 #44 #45)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   637
#47 := (f12 #46)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   638
#258 := (>= #47 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   639
#260 := (not #258)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   640
#49 := (= #47 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   641
#50 := (not #49)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   642
#134 := [asserted]: #50
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   643
#266 := (or #49 #260)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   644
#48 := (<= #47 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   645
#114 := [asserted]: #48
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   646
#259 := (not #48)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   647
#264 := (or #49 #259 #260)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   648
#265 := [th-lemma arith triangle-eq]: #264
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   649
#267 := [unit-resolution #265 #114]: #266
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   650
#268 := [unit-resolution #267 #134]: #260
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   651
#39 := (:var 0 S4)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   652
#38 := (:var 1 S4)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   653
#40 := (f13 #38 #39)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   654
#251 := (pattern #40)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   655
#41 := (f12 #40)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   656
#136 := (>= #41 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   657
#252 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #251) #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   658
#138 := (forall (vars (?v0 S4) (?v1 S4)) #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   659
#255 := (iff #138 #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   660
#253 := (iff #136 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   661
#254 := [refl]: #253
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   662
#256 := [quant-intro #254]: #255
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   663
#165 := (~ #138 #138)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   664
#153 := (~ #136 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   665
#154 := [refl]: #153
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   666
#166 := [nnf-pos #154]: #165
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   667
#42 := (<= 0::Real #41)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   668
#43 := (forall (vars (?v0 S4) (?v1 S4)) #42)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   669
#139 := (iff #43 #138)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   670
#135 := (iff #42 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   671
#137 := [rewrite]: #135
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   672
#140 := [quant-intro #137]: #139
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   673
#113 := [asserted]: #43
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   674
#141 := [mp #113 #140]: #138
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   675
#167 := [mp~ #141 #166]: #138
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   676
#257 := [mp #167 #256]: #252
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   677
#261 := (not #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   678
#262 := (or #261 #258)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   679
#263 := [quant-inst #44 #45]: #262
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   680
[unit-resolution #263 #257 #268]: false
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   681
unsat
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   682
fe6d352e9186ccd9319b5d4bd3ff26ab342ba6c4 351 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
   683
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   684
#8 := 0::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   685
decl f7 :: (-> S4 S2 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   686
decl f10 :: S2
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   687
#25 := f10
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   688
decl f8 :: S4
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   689
#17 := f8
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   690
#32 := (f7 f8 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   691
decl f11 :: S4
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   692
#29 := f11
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   693
#30 := (f7 f11 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   694
#100 := -1::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   695
#136 := (* -1::Real #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   696
#137 := (+ #136 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   697
decl f3 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   698
#9 := f3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   699
#197 := (* -1::Real #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   700
#198 := (+ #30 #197)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   701
#199 := (+ f3 #198)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   702
#200 := (<= #199 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   703
#203 := (ite #200 f3 #137)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   704
#630 := (* -1::Real #203)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   705
#631 := (+ f3 #630)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   706
#632 := (<= #631 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   707
#639 := (not #632)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   708
#127 := 1/2::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   709
#206 := (* 1/2::Real #203)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   710
#494 := (<= #206 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   711
#217 := (= #206 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   712
#234 := (<= #198 0::Real)
40163
a462d5207aa6 changed SMT configuration options; updated SMT certificates
boehmes
parents: 37489
diff changeset
   713
decl f9 :: S4
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   714
#19 := f9
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   715
#28 := (f7 f9 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   716
#230 := (+ #28 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   717
#231 := (<= #230 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   718
#237 := (and #231 #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   719
#53 := 0::Int
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   720
decl f4 :: (-> S2 Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   721
#26 := (f4 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   722
#93 := -1::Int
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   723
#117 := (* -1::Int #26)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   724
decl f5 :: (-> S3 S2)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   725
decl f6 :: S3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   726
#13 := f6
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   727
#14 := (f5 f6)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   728
#15 := (f4 #14)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   729
#118 := (+ #15 #117)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   730
#119 := (<= #118 0::Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   731
#240 := (or #119 #237)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   732
#243 := (not #240)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   733
#220 := (not #217)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   734
#129 := (* 1/2::Real #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   735
#194 := (+ #136 #129)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   736
#128 := (* 1/2::Real #28)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   737
#195 := (+ #128 #194)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   738
#192 := (>= #195 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   739
#190 := (not #192)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   740
#252 := (or #190 #220 #243)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   741
#257 := (not #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   742
#37 := 2::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   743
#40 := (- #32 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   744
#41 := (<= f3 #40)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   745
#42 := (ite #41 f3 #40)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   746
#43 := (/ #42 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   747
#44 := (+ #30 #43)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   748
#45 := (= #44 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   749
#46 := (not #45)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   750
#36 := (+ #28 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   751
#38 := (/ #36 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   752
#39 := (<= #30 #38)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   753
#47 := (implies #39 #46)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   754
#33 := (<= #30 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   755
#31 := (<= #28 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   756
#34 := (and #31 #33)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   757
#27 := (< #26 #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   758
#35 := (implies #27 #34)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   759
#48 := (implies #35 #47)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   760
#49 := (not #48)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   761
#260 := (iff #49 #257)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   762
#140 := (<= f3 #137)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   763
#143 := (ite #140 f3 #137)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   764
#149 := (* 1/2::Real #143)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   765
#154 := (+ #30 #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   766
#160 := (= #30 #154)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   767
#165 := (not #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   768
#130 := (+ #128 #129)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   769
#133 := (<= #30 #130)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   770
#171 := (not #133)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   771
#172 := (or #171 #165)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   772
#116 := (not #27)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   773
#124 := (or #116 #34)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   774
#180 := (not #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   775
#181 := (or #180 #172)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   776
#186 := (not #181)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   777
#258 := (iff #186 #257)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   778
#255 := (iff #181 #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   779
#246 := (or #190 #220)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   780
#249 := (or #243 #246)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   781
#253 := (iff #249 #252)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   782
#254 := [rewrite]: #253
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   783
#250 := (iff #181 #249)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   784
#247 := (iff #172 #246)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   785
#221 := (iff #165 #220)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   786
#218 := (iff #160 #217)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   787
#209 := (+ #30 #206)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   788
#212 := (= #30 #209)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   789
#215 := (iff #212 #217)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   790
#216 := [rewrite]: #215
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   791
#213 := (iff #160 #212)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   792
#210 := (= #154 #209)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   793
#207 := (= #149 #206)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   794
#204 := (= #143 #203)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   795
#201 := (iff #140 #200)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   796
#202 := [rewrite]: #201
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   797
#205 := [monotonicity #202]: #204
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   798
#208 := [monotonicity #205]: #207
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   799
#211 := [monotonicity #208]: #210
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   800
#214 := [monotonicity #211]: #213
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   801
#219 := [trans #214 #216]: #218
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   802
#222 := [monotonicity #219]: #221
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   803
#193 := (iff #171 #190)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   804
#189 := (iff #133 #192)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   805
#191 := [rewrite]: #189
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   806
#196 := [monotonicity #191]: #193
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   807
#248 := [monotonicity #196 #222]: #247
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   808
#244 := (iff #180 #243)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   809
#241 := (iff #124 #240)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   810
#238 := (iff #34 #237)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   811
#235 := (iff #33 #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   812
#236 := [rewrite]: #235
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   813
#232 := (iff #31 #231)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   814
#233 := [rewrite]: #232
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   815
#239 := [monotonicity #233 #236]: #238
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   816
#228 := (iff #116 #119)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   817
#120 := (not #119)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   818
#223 := (not #120)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   819
#226 := (iff #223 #119)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   820
#227 := [rewrite]: #226
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   821
#224 := (iff #116 #223)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   822
#121 := (iff #27 #120)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   823
#122 := [rewrite]: #121
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   824
#225 := [monotonicity #122]: #224
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   825
#229 := [trans #225 #227]: #228
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   826
#242 := [monotonicity #229 #239]: #241
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   827
#245 := [monotonicity #242]: #244
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   828
#251 := [monotonicity #245 #248]: #250
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   829
#256 := [trans #251 #254]: #255
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   830
#259 := [monotonicity #256]: #258
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   831
#187 := (iff #49 #186)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   832
#184 := (iff #48 #181)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   833
#177 := (implies #124 #172)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   834
#182 := (iff #177 #181)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   835
#183 := [rewrite]: #182
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   836
#178 := (iff #48 #177)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   837
#175 := (iff #47 #172)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   838
#168 := (implies #133 #165)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   839
#173 := (iff #168 #172)
40163
a462d5207aa6 changed SMT configuration options; updated SMT certificates
boehmes
parents: 37489
diff changeset
   840
#174 := [rewrite]: #173
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   841
#169 := (iff #47 #168)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   842
#166 := (iff #46 #165)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   843
#163 := (iff #45 #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   844
#157 := (= #154 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   845
#161 := (iff #157 #160)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   846
#162 := [rewrite]: #161
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   847
#158 := (iff #45 #157)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   848
#155 := (= #44 #154)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   849
#152 := (= #43 #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   850
#146 := (/ #143 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   851
#150 := (= #146 #149)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   852
#151 := [rewrite]: #150
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   853
#147 := (= #43 #146)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   854
#144 := (= #42 #143)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   855
#138 := (= #40 #137)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   856
#139 := [rewrite]: #138
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   857
#141 := (iff #41 #140)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   858
#142 := [monotonicity #139]: #141
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   859
#145 := [monotonicity #142 #139]: #144
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   860
#148 := [monotonicity #145]: #147
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   861
#153 := [trans #148 #151]: #152
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   862
#156 := [monotonicity #153]: #155
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   863
#159 := [monotonicity #156]: #158
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   864
#164 := [trans #159 #162]: #163
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   865
#167 := [monotonicity #164]: #166
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   866
#134 := (iff #39 #133)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   867
#131 := (= #38 #130)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   868
#132 := [rewrite]: #131
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   869
#135 := [monotonicity #132]: #134
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   870
#170 := [monotonicity #135 #167]: #169
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   871
#176 := [trans #170 #174]: #175
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   872
#125 := (iff #35 #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   873
#126 := [rewrite]: #125
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   874
#179 := [monotonicity #126 #176]: #178
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   875
#185 := [trans #179 #183]: #184
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   876
#188 := [monotonicity #185]: #187
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   877
#261 := [trans #188 #259]: #260
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   878
#92 := [asserted]: #49
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   879
#262 := [mp #92 #261]: #257
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   880
#264 := [not-or-elim #262]: #217
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   881
#634 := (or #220 #494)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   882
#635 := [th-lemma arith triangle-eq]: #634
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   883
#636 := [unit-resolution #635 #264]: #494
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   884
#637 := [hypothesis]: #632
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   885
#87 := (<= f3 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   886
#88 := (not #87)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   887
#10 := (< 0::Real f3)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   888
#89 := (iff #10 #88)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   889
#90 := [rewrite]: #89
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   890
#84 := [asserted]: #10
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   891
#91 := [mp #84 #90]: #88
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   892
#638 := [th-lemma arith farkas -1/2 1/2 1 #91 #637 #636]: false
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   893
#640 := [lemma #638]: #639
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   894
#487 := (= f3 #203)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   895
#488 := (= #137 #203)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   896
#649 := (not #488)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   897
#633 := (+ #137 #630)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   898
#641 := (<= #633 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   899
#646 := (not #641)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   900
#565 := (+ #28 #197)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   901
#566 := (>= #565 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   902
#571 := (not #566)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   903
#86 := [asserted]: #27
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   904
#123 := [mp #86 #122]: #120
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   905
#11 := (:var 0 S2)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   906
#20 := (f7 f9 #11)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   907
#461 := (pattern #20)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   908
#18 := (f7 f8 #11)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   909
#460 := (pattern #18)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   910
#12 := (f4 #11)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   911
#459 := (pattern #12)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   912
#101 := (* -1::Real #20)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   913
#102 := (+ #18 #101)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   914
#103 := (<= #102 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   915
#386 := (not #103)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   916
#96 := (* -1::Int #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   917
#97 := (+ #12 #96)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   918
#95 := (>= #97 0::Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   919
#387 := (or #95 #386)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   920
#462 := (forall (vars (?v0 S2)) (:pat #459 #460 #461) #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   921
#398 := (forall (vars (?v0 S2)) #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   922
#465 := (iff #398 #462)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   923
#463 := (iff #387 #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   924
#464 := [refl]: #463
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   925
#466 := [quant-intro #464]: #465
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   926
#94 := (not #95)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   927
#106 := (and #94 #103)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   928
#378 := (not #106)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   929
#377 := (forall (vars (?v0 S2)) #378)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   930
#399 := (iff #377 #398)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   931
#396 := (iff #378 #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   932
#388 := (not #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   933
#391 := (not #388)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   934
#394 := (iff #391 #387)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   935
#395 := [rewrite]: #394
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   936
#392 := (iff #378 #391)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   937
#389 := (iff #106 #388)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   938
#390 := [rewrite]: #389
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   939
#393 := [monotonicity #390]: #392
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   940
#397 := [trans #393 #395]: #396
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   941
#400 := [quant-intro #397]: #399
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   942
#109 := (exists (vars (?v0 S2)) #106)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   943
#112 := (not #109)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   944
#374 := (~ #112 #377)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   945
#379 := (~ #378 #378)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   946
#376 := [refl]: #379
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   947
#375 := [nnf-neg #376]: #374
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   948
#21 := (<= #18 #20)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   949
#16 := (< #12 #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   950
#22 := (and #16 #21)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   951
#23 := (exists (vars (?v0 S2)) #22)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   952
#24 := (not #23)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   953
#113 := (iff #24 #112)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   954
#110 := (iff #23 #109)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   955
#107 := (iff #22 #106)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   956
#104 := (iff #21 #103)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   957
#105 := [rewrite]: #104
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   958
#98 := (iff #16 #94)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   959
#99 := [rewrite]: #98
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   960
#108 := [monotonicity #99 #105]: #107
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   961
#111 := [quant-intro #108]: #110
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   962
#114 := [monotonicity #111]: #113
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   963
#85 := [asserted]: #24
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   964
#115 := [mp #85 #114]: #112
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   965
#372 := [mp~ #115 #375]: #377
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   966
#401 := [mp #372 #400]: #398
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   967
#467 := [mp #401 #466]: #462
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   968
#577 := (not #462)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   969
#578 := (or #577 #119 #571)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   970
#539 := (* -1::Real #28)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   971
#540 := (+ #32 #539)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   972
#544 := (<= #540 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   973
#545 := (not #544)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   974
#546 := (+ #26 #96)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   975
#547 := (>= #546 0::Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   976
#548 := (or #547 #545)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   977
#579 := (or #577 #548)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   978
#586 := (iff #579 #578)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   979
#574 := (or #119 #571)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   980
#581 := (or #577 #574)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   981
#584 := (iff #581 #578)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   982
#585 := [rewrite]: #584
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   983
#582 := (iff #579 #581)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   984
#575 := (iff #548 #574)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   985
#572 := (iff #545 #571)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   986
#569 := (iff #544 #566)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   987
#559 := (+ #539 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   988
#562 := (<= #559 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   989
#567 := (iff #562 #566)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   990
#568 := [rewrite]: #567
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   991
#563 := (iff #544 #562)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   992
#560 := (= #540 #559)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   993
#561 := [rewrite]: #560
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   994
#564 := [monotonicity #561]: #563
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   995
#570 := [trans #564 #568]: #569
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   996
#573 := [monotonicity #570]: #572
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   997
#557 := (iff #547 #119)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   998
#549 := (+ #96 #26)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
   999
#552 := (>= #549 0::Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1000
#555 := (iff #552 #119)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1001
#556 := [rewrite]: #555
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1002
#553 := (iff #547 #552)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1003
#550 := (= #546 #549)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1004
#551 := [rewrite]: #550
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1005
#554 := [monotonicity #551]: #553
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1006
#558 := [trans #554 #556]: #557
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1007
#576 := [monotonicity #558 #573]: #575
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1008
#583 := [monotonicity #576]: #582
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1009
#587 := [trans #583 #585]: #586
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1010
#580 := [quant-inst #25]: #579
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1011
#588 := [mp #580 #587]: #578
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1012
#643 := [unit-resolution #588 #467 #123]: #571
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1013
#263 := [not-or-elim #262]: #192
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1014
#644 := [hypothesis]: #641
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1015
#645 := [th-lemma arith farkas 1/2 -1/2 1/4 1 #644 #263 #643 #636]: false
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1016
#647 := [lemma #645]: #646
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1017
#648 := [hypothesis]: #488
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1018
#650 := (or #649 #641)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1019
#651 := [th-lemma arith triangle-eq]: #650
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1020
#652 := [unit-resolution #651 #648 #647]: false
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1021
#653 := [lemma #652]: #649
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1022
#492 := (or #200 #488)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1023
#493 := [def-axiom]: #492
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1024
#654 := [unit-resolution #493 #653]: #200
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1025
#489 := (not #200)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1026
#490 := (or #489 #487)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1027
#491 := [def-axiom]: #490
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1028
#655 := [unit-resolution #491 #654]: #487
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1029
#656 := (not #487)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1030
#657 := (or #656 #632)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1031
#658 := [th-lemma arith triangle-eq]: #657
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1032
[unit-resolution #658 #655 #640]: false
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
  1033
unsat
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1034
7b7b29f11f061c77d0fa2db9bb640b09f44da643 331 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
  1035
#2 := false
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1036
#8 := 0::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1037
decl f7 :: (-> S4 S2 Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1038
decl f10 :: S2
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1039
#25 := f10
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1040
decl f11 :: S4
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1041
#29 := f11
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1042
#30 := (f7 f11 f10)
40163
a462d5207aa6 changed SMT configuration options; updated SMT certificates
boehmes
parents: 37489
diff changeset
  1043
decl f9 :: S4
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1044
#19 := f9
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1045
#28 := (f7 f9 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1046
#107 := -1::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1047
#167 := (* -1::Real #28)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1048
#168 := (+ #167 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1049
decl f3 :: Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1050
#9 := f3
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1051
#146 := (* -1::Real #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1052
#260 := (+ #28 #146)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1053
#261 := (+ f3 #260)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1054
#262 := (<= #261 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1055
#265 := (ite #262 f3 #168)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1056
#707 := (* -1::Real #265)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1057
#708 := (+ f3 #707)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1058
#709 := (<= #708 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1059
#717 := (not #709)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1060
#134 := 1/2::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1061
#431 := (* 1/2::Real #265)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1062
#572 := (<= #431 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1063
#432 := (= #431 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1064
#188 := -1/2::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1065
#268 := (* -1/2::Real #265)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1066
#271 := (+ #30 #268)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1067
decl f8 :: S4
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1068
#17 := f8
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1069
#32 := (f7 f8 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1070
#147 := (+ #146 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1071
#245 := (* -1::Real #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1072
#246 := (+ #30 #245)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1073
#247 := (+ f3 #246)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1074
#248 := (<= #247 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1075
#251 := (ite #248 f3 #147)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1076
#254 := (* 1/2::Real #251)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1077
#257 := (+ #30 #254)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1078
#136 := (* 1/2::Real #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1079
#234 := (+ #146 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1080
#135 := (* 1/2::Real #28)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1081
#235 := (+ #135 #234)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1082
#232 := (>= #235 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1083
#274 := (ite #232 #257 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1084
#277 := (= #30 #274)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1085
#435 := (iff #277 #432)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1086
#428 := (= #30 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1087
#433 := (iff #428 #432)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1088
#434 := [rewrite]: #433
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1089
#429 := (iff #277 #428)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1090
#426 := (= #274 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1091
#421 := (ite false #257 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1092
#424 := (= #421 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1093
#425 := [rewrite]: #424
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1094
#422 := (= #274 #421)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1095
#419 := (iff #232 false)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1096
#231 := (not #232)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1097
#293 := (<= #246 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1098
#290 := (<= #260 0::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1099
#296 := (and #290 #293)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1100
#60 := 0::Int
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1101
decl f4 :: (-> S2 Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1102
#26 := (f4 f10)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1103
#100 := -1::Int
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1104
#124 := (* -1::Int #26)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1105
decl f5 :: (-> S3 S2)
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset
  1106
decl f6 :: S3
41132
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1107
#13 := f6
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1108
#14 := (f5 f6)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1109
#15 := (f4 #14)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1110
#125 := (+ #15 #124)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1111
#126 := (<= #125 0::Int)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1112
#299 := (or #126 #296)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1113
#302 := (not #299)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1114
#280 := (not #277)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1115
#311 := (or #232 #280 #302)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1116
#316 := (not #311)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1117
#37 := 2::Real
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1118
#46 := (- #30 #28)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1119
#47 := (<= f3 #46)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1120
#48 := (ite #47 f3 #46)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1121
#49 := (/ #48 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1122
#50 := (- #30 #49)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1123
#41 := (- #32 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1124
#42 := (<= f3 #41)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1125
#43 := (ite #42 f3 #41)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1126
#44 := (/ #43 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1127
#45 := (+ #30 #44)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1128
#36 := (+ #28 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1129
#38 := (/ #36 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1130
#40 := (<= #30 #38)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1131
#51 := (ite #40 #45 #50)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1132
#52 := (= #51 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1133
#53 := (not #52)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1134
#39 := (< #38 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1135
#54 := (implies #39 #53)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1136
#33 := (<= #30 #32)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1137
#31 := (<= #28 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1138
#34 := (and #31 #33)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1139
#27 := (< #26 #15)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1140
#35 := (implies #27 #34)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1141
#55 := (implies #35 #54)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1142
#56 := (not #55)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1143
#319 := (iff #56 #316)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1144
#171 := (<= f3 #168)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1145
#174 := (ite #171 f3 #168)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1146
#189 := (* -1/2::Real #174)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1147
#190 := (+ #30 #189)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1148
#150 := (<= f3 #147)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1149
#153 := (ite #150 f3 #147)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1150
#159 := (* 1/2::Real #153)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1151
#164 := (+ #30 #159)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1152
#137 := (+ #135 #136)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1153
#143 := (<= #30 #137)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1154
#195 := (ite #143 #164 #190)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1155
#201 := (= #30 #195)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1156
#206 := (not #201)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1157
#140 := (< #137 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1158
#212 := (not #140)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1159
#213 := (or #212 #206)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1160
#123 := (not #27)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1161
#131 := (or #123 #34)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1162
#221 := (not #131)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1163
#222 := (or #221 #213)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1164
#227 := (not #222)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1165
#317 := (iff #227 #316)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1166
#314 := (iff #222 #311)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1167
#305 := (or #232 #280)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1168
#308 := (or #302 #305)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1169
#312 := (iff #308 #311)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1170
#313 := [rewrite]: #312
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1171
#309 := (iff #222 #308)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1172
#306 := (iff #213 #305)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1173
#281 := (iff #206 #280)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1174
#278 := (iff #201 #277)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1175
#275 := (= #195 #274)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1176
#272 := (= #190 #271)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1177
#269 := (= #189 #268)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1178
#266 := (= #174 #265)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1179
#263 := (iff #171 #262)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1180
#264 := [rewrite]: #263
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1181
#267 := [monotonicity #264]: #266
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1182
#270 := [monotonicity #267]: #269
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1183
#273 := [monotonicity #270]: #272
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1184
#258 := (= #164 #257)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1185
#255 := (= #159 #254)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1186
#252 := (= #153 #251)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1187
#249 := (iff #150 #248)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1188
#250 := [rewrite]: #249
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1189
#253 := [monotonicity #250]: #252
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1190
#256 := [monotonicity #253]: #255
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1191
#259 := [monotonicity #256]: #258
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1192
#244 := (iff #143 #232)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1193
#243 := [rewrite]: #244
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1194
#276 := [monotonicity #243 #259 #273]: #275
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1195
#279 := [monotonicity #276]: #278
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1196
#282 := [monotonicity #279]: #281
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1197
#241 := (iff #212 #232)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1198
#236 := (not #231)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1199
#239 := (iff #236 #232)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1200
#240 := [rewrite]: #239
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1201
#237 := (iff #212 #236)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1202
#230 := (iff #140 #231)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1203
#233 := [rewrite]: #230
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1204
#238 := [monotonicity #233]: #237
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1205
#242 := [trans #238 #240]: #241
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1206
#307 := [monotonicity #242 #282]: #306
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1207
#303 := (iff #221 #302)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1208
#300 := (iff #131 #299)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1209
#297 := (iff #34 #296)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1210
#294 := (iff #33 #293)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1211
#295 := [rewrite]: #294
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1212
#291 := (iff #31 #290)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1213
#292 := [rewrite]: #291
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1214
#298 := [monotonicity #292 #295]: #297
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1215
#288 := (iff #123 #126)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1216
#127 := (not #126)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1217
#283 := (not #127)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1218
#286 := (iff #283 #126)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1219
#287 := [rewrite]: #286
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1220
#284 := (iff #123 #283)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1221
#128 := (iff #27 #127)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1222
#129 := [rewrite]: #128
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1223
#285 := [monotonicity #129]: #284
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1224
#289 := [trans #285 #287]: #288
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1225
#301 := [monotonicity #289 #298]: #300
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1226
#304 := [monotonicity #301]: #303
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1227
#310 := [monotonicity #304 #307]: #309
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1228
#315 := [trans #310 #313]: #314
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1229
#318 := [monotonicity #315]: #317
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1230
#228 := (iff #56 #227)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1231
#225 := (iff #55 #222)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1232
#218 := (implies #131 #213)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1233
#223 := (iff #218 #222)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1234
#224 := [rewrite]: #223
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1235
#219 := (iff #55 #218)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1236
#216 := (iff #54 #213)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1237
#209 := (implies #140 #206)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1238
#214 := (iff #209 #213)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1239
#215 := [rewrite]: #214
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1240
#210 := (iff #54 #209)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1241
#207 := (iff #53 #206)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1242
#204 := (iff #52 #201)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1243
#198 := (= #195 #30)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1244
#202 := (iff #198 #201)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1245
#203 := [rewrite]: #202
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1246
#199 := (iff #52 #198)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1247
#196 := (= #51 #195)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1248
#193 := (= #50 #190)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1249
#180 := (* 1/2::Real #174)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1250
#185 := (- #30 #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1251
#191 := (= #185 #190)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1252
#192 := [rewrite]: #191
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1253
#186 := (= #50 #185)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1254
#183 := (= #49 #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1255
#177 := (/ #174 2::Real)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1256
#181 := (= #177 #180)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1257
#182 := [rewrite]: #181
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1258
#178 := (= #49 #177)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1259
#175 := (= #48 #174)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1260
#169 := (= #46 #168)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1261
#170 := [rewrite]: #169
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1262
#172 := (iff #47 #171)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1263
#173 := [monotonicity #170]: #172
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1264
#176 := [monotonicity #173 #170]: #175
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1265
#179 := [monotonicity #176]: #178
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1266
#184 := [trans #179 #182]: #183
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1267
#187 := [monotonicity #184]: #186
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1268
#194 := [trans #187 #192]: #193
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1269
#165 := (= #45 #164)
42384824b732 updated SMT certificates
boehmes
parents: 41064
diff changeset
  1270
#162 := (= #44 #159)
42384824b732 updated SMT certificates
boehmes
parents: 41064</