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