src/HOL/Boogie/Examples/Boogie_Max.certs
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 37156 42c53229800d
child 40163 a462d5207aa6
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
boehmes@37156
     1
3e8da1e086888bc525192984192051f1e39c6752 2224 0
boehmes@34994
     2
#2 := false
boehmes@36900
     3
#8 := 0::int
boehmes@36900
     4
decl f5 :: (-> int int)
boehmes@36900
     5
decl ?v0!3 :: int
boehmes@36900
     6
#1153 := ?v0!3
boehmes@36900
     7
#1154 := (f5 ?v0!3)
boehmes@36900
     8
#652 := -1::int
boehmes@36900
     9
#1356 := (* -1::int #1154)
boehmes@36900
    10
decl f7 :: int
boehmes@36900
    11
#31 := f7
boehmes@36900
    12
#68 := (f5 f7)
boehmes@36900
    13
#2646 := (+ #68 #1356)
boehmes@36900
    14
#2648 := (>= #2646 0::int)
boehmes@36900
    15
#2645 := (= #68 #1154)
boehmes@36900
    16
#2494 := (= f7 ?v0!3)
boehmes@36900
    17
#1334 := (* -1::int ?v0!3)
boehmes@36900
    18
#2380 := (+ f7 #1334)
boehmes@36900
    19
#2496 := (>= #2380 0::int)
boehmes@36900
    20
decl f15 :: int
boehmes@36900
    21
#79 := f15
boehmes@36900
    22
#1335 := (+ f15 #1334)
boehmes@36900
    23
#1336 := (<= #1335 0::int)
boehmes@36900
    24
#1341 := (not #1336)
boehmes@36900
    25
decl f14 :: int
boehmes@36900
    26
#75 := f14
boehmes@36900
    27
#1357 := (+ f14 #1356)
boehmes@36900
    28
#1358 := (>= #1357 0::int)
boehmes@36900
    29
#1160 := (>= ?v0!3 0::int)
boehmes@36900
    30
#1609 := (not #1160)
boehmes@36900
    31
#1624 := (or #1609 #1336 #1358)
boehmes@36900
    32
#1629 := (not #1624)
boehmes@36900
    33
#20 := (:var 0 int)
boehmes@36900
    34
#24 := (f5 #20)
boehmes@36900
    35
#2199 := (pattern #24)
boehmes@36900
    36
#777 := (* -1::int f14)
boehmes@36900
    37
#778 := (+ #24 #777)
boehmes@36900
    38
#779 := (<= #778 0::int)
boehmes@36900
    39
#766 := (* -1::int f15)
boehmes@36900
    40
#767 := (+ #20 #766)
boehmes@36900
    41
#765 := (>= #767 0::int)
boehmes@36900
    42
#641 := (>= #20 0::int)
boehmes@36900
    43
#1440 := (not #641)
boehmes@36900
    44
#1591 := (or #1440 #765 #779)
boehmes@36900
    45
#2216 := (forall (vars (?v0 int)) (:pat #2199) #1591)
boehmes@36900
    46
#2221 := (not #2216)
boehmes@36900
    47
decl f13 :: int
boehmes@36900
    48
#73 := f13
boehmes@36900
    49
#90 := (f5 f13)
boehmes@36900
    50
#307 := (= f14 #90)
boehmes@36900
    51
#2224 := (or #307 #2221)
boehmes@36900
    52
#2227 := (not #2224)
boehmes@36900
    53
#2230 := (or #2227 #1629)
boehmes@36900
    54
#2233 := (not #2230)
boehmes@36900
    55
#820 := (* -1::int #68)
boehmes@36900
    56
decl f8 :: int
boehmes@36900
    57
#36 := f8
boehmes@36900
    58
#821 := (+ f8 #820)
boehmes@36900
    59
#819 := (>= #821 0::int)
boehmes@36900
    60
#818 := (not #819)
boehmes@36900
    61
#803 := (+ f7 #766)
boehmes@36900
    62
#802 := (= #803 -1::int)
boehmes@36900
    63
#806 := (not #802)
boehmes@36900
    64
#82 := 2::int
boehmes@36900
    65
#757 := (>= f15 2::int)
boehmes@36900
    66
#1639 := (not #757)
boehmes@36900
    67
#754 := (>= f13 0::int)
boehmes@36900
    68
#1638 := (not #754)
boehmes@36900
    69
#15 := 1::int
boehmes@36900
    70
#671 := (>= f7 1::int)
boehmes@36900
    71
#815 := (not #671)
boehmes@36900
    72
decl f6 :: int
boehmes@36900
    73
#29 := f6
boehmes@36900
    74
#668 := (>= f6 0::int)
boehmes@36900
    75
#1569 := (not #668)
boehmes@36900
    76
#426 := (= f8 f14)
boehmes@36900
    77
#432 := (not #426)
boehmes@36900
    78
#423 := (= f6 f13)
boehmes@36900
    79
#441 := (not #423)
boehmes@36900
    80
#2242 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #2233)
boehmes@36900
    81
#2245 := (not #2242)
boehmes@36900
    82
decl f12 :: int
boehmes@36900
    83
#70 := f12
boehmes@36900
    84
#288 := (= f12 f14)
boehmes@36900
    85
#366 := (not #288)
boehmes@36900
    86
#285 := (= f7 f13)
boehmes@36900
    87
#375 := (not #285)
boehmes@36900
    88
#280 := (= #68 f12)
boehmes@36900
    89
#393 := (not #280)
boehmes@36900
    90
#2236 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #2233)
boehmes@36900
    91
#2239 := (not #2236)
boehmes@36900
    92
#2248 := (or #2239 #2245)
boehmes@36900
    93
#2251 := (not #2248)
boehmes@36900
    94
#722 := (* -1::int f7)
boehmes@36900
    95
decl f3 :: int
boehmes@36900
    96
#9 := f3
boehmes@36900
    97
#723 := (+ f3 #722)
boehmes@36900
    98
#724 := (<= #723 0::int)
boehmes@36900
    99
#2254 := (or #1569 #815 #724 #2251)
boehmes@36900
   100
#2257 := (not #2254)
boehmes@36900
   101
decl ?v0!1 :: int
boehmes@36900
   102
#1086 := ?v0!1
boehmes@36900
   103
#1094 := (f5 ?v0!1)
boehmes@36900
   104
decl f10 :: int
boehmes@36900
   105
#45 := f10
boehmes@36900
   106
#1267 := (= f10 #1094)
boehmes@36900
   107
#1091 := (>= ?v0!1 0::int)
boehmes@36900
   108
#1510 := (not #1091)
boehmes@36900
   109
#1087 := (* -1::int ?v0!1)
boehmes@36900
   110
#1088 := (+ f3 #1087)
boehmes@36900
   111
#1089 := (<= #1088 0::int)
boehmes@36900
   112
#1525 := (or #1089 #1510 #1267)
boehmes@36900
   113
#1556 := (not #1525)
boehmes@36900
   114
decl ?v0!2 :: int
boehmes@36900
   115
#1104 := ?v0!2
boehmes@36900
   116
#1105 := (f5 ?v0!2)
boehmes@36900
   117
#1291 := (* -1::int #1105)
boehmes@36900
   118
#1292 := (+ f10 #1291)
boehmes@36900
   119
#1293 := (>= #1292 0::int)
boehmes@36900
   120
#1112 := (>= ?v0!2 0::int)
boehmes@36900
   121
#1530 := (not #1112)
boehmes@36900
   122
#1108 := (* -1::int ?v0!2)
boehmes@36900
   123
#1109 := (+ f3 #1108)
boehmes@36900
   124
#1110 := (<= #1109 0::int)
boehmes@36900
   125
#1687 := (or #1110 #1530 #1293 #1556)
boehmes@36900
   126
#1690 := (not #1687)
boehmes@36900
   127
#679 := (* -1::int #20)
boehmes@36900
   128
#680 := (+ f3 #679)
boehmes@36900
   129
#681 := (<= #680 0::int)
boehmes@36900
   130
#51 := (= #24 f10)
boehmes@36900
   131
#1499 := (or #51 #1440 #681)
boehmes@36900
   132
#1504 := (not #1499)
boehmes@36900
   133
#2260 := (forall (vars (?v0 int)) (:pat #2199) #1504)
boehmes@36900
   134
#2265 := (or #2260 #1690)
boehmes@36900
   135
#2268 := (not #2265)
boehmes@36900
   136
#727 := (not #724)
boehmes@36900
   137
decl f11 :: int
boehmes@36900
   138
#47 := f11
boehmes@36900
   139
#185 := (= f7 f11)
boehmes@36900
   140
#223 := (not #185)
boehmes@36900
   141
#182 := (= f8 f10)
boehmes@36900
   142
#232 := (not #182)
boehmes@36900
   143
decl f9 :: int
boehmes@36900
   144
#43 := f9
boehmes@36900
   145
#179 := (= f6 f9)
boehmes@36900
   146
#241 := (not #179)
boehmes@36900
   147
#2271 := (or #241 #232 #223 #1569 #815 #727 #2268)
boehmes@36900
   148
#927 := (* -1::int f8)
boehmes@36900
   149
#928 := (+ #24 #927)
boehmes@36900
   150
#929 := (<= #928 0::int)
boehmes@36900
   151
#917 := (+ #20 #722)
boehmes@36900
   152
#916 := (>= #917 0::int)
boehmes@36900
   153
#1477 := (or #1440 #916 #929)
boehmes@36900
   154
#2208 := (forall (vars (?v0 int)) (:pat #2199) #1477)
boehmes@36900
   155
#2274 := (not #2271)
boehmes@36900
   156
#2277 := (or #2257 #2274)
boehmes@36900
   157
#2280 := (not #2277)
boehmes@36900
   158
#2213 := (not #2208)
boehmes@36900
   159
#655 := (* -1::int #24)
boehmes@36900
   160
decl f4 :: int
boehmes@36900
   161
#11 := f4
boehmes@36900
   162
#656 := (+ f4 #655)
boehmes@36900
   163
#654 := (>= #656 0::int)
boehmes@36900
   164
#644 := (>= #20 1::int)
boehmes@36900
   165
#1455 := (or #1440 #644 #654)
boehmes@36900
   166
#2200 := (forall (vars (?v0 int)) (:pat #2199) #1455)
boehmes@36900
   167
#2205 := (not #2200)
boehmes@36900
   168
#40 := (f5 f6)
boehmes@36900
   169
#176 := (= f8 #40)
boehmes@36900
   170
#528 := (not #176)
boehmes@36900
   171
#2283 := (or #528 #1569 #815 #2205 #2213 #2280)
boehmes@36900
   172
#2286 := (not #2283)
boehmes@36900
   173
decl ?v0!0 :: int
boehmes@36900
   174
#1046 := ?v0!0
boehmes@36900
   175
#1049 := (>= ?v0!0 0::int)
boehmes@36900
   176
#1167 := (not #1049)
boehmes@36900
   177
#1047 := (f5 ?v0!0)
boehmes@36900
   178
#1044 := (* -1::int #1047)
boehmes@36900
   179
#1045 := (+ f4 #1044)
boehmes@36900
   180
#1007 := (>= #1045 0::int)
boehmes@36900
   181
#1005 := (>= ?v0!0 1::int)
boehmes@36900
   182
#1432 := (or #1005 #1007 #1167)
boehmes@36900
   183
#2072 := (= f4 #1047)
boehmes@36900
   184
#12 := (f5 0::int)
boehmes@36900
   185
#2053 := (= #12 #1047)
boehmes@36900
   186
#1941 := (= #1047 #12)
boehmes@36900
   187
#2071 := (= ?v0!0 0::int)
boehmes@36900
   188
#1048 := (not #1005)
boehmes@36900
   189
#1437 := (not #1432)
boehmes@36900
   190
#2073 := [hypothesis]: #1437
boehmes@36900
   191
#1785 := (or #1432 #1048)
boehmes@36900
   192
#1870 := [def-axiom]: #1785
boehmes@36900
   193
#2046 := [unit-resolution #1870 #2073]: #1048
boehmes@36900
   194
#1863 := (or #1432 #1049)
boehmes@36900
   195
#1874 := [def-axiom]: #1863
boehmes@36900
   196
#2047 := [unit-resolution #1874 #2073]: #1049
boehmes@36900
   197
#2048 := [th-lemma #2047 #2046]: #2071
boehmes@36900
   198
#2052 := [monotonicity #2048]: #1941
boehmes@36900
   199
#2054 := [symm #2052]: #2053
boehmes@36900
   200
#13 := (= f4 #12)
boehmes@36900
   201
#970 := (<= f3 0::int)
boehmes@36900
   202
#918 := (not #916)
boehmes@36900
   203
#921 := (and #641 #918)
boehmes@36900
   204
#924 := (not #921)
boehmes@36900
   205
#932 := (or #924 #929)
boehmes@36900
   206
#935 := (forall (vars (?v0 int)) #932)
boehmes@36900
   207
#938 := (not #935)
boehmes@36900
   208
#809 := (and #671 #754)
boehmes@36900
   209
#812 := (not #809)
boehmes@36900
   210
#768 := (not #765)
boehmes@36900
   211
#771 := (and #641 #768)
boehmes@36900
   212
#774 := (not #771)
boehmes@36900
   213
#782 := (or #774 #779)
boehmes@36900
   214
#785 := (forall (vars (?v0 int)) #782)
boehmes@36900
   215
#788 := (not #785)
boehmes@36900
   216
#794 := (or #307 #788)
boehmes@36900
   217
#799 := (and #785 #794)
boehmes@36900
   218
#759 := (and #754 #757)
boehmes@36900
   219
#762 := (not #759)
boehmes@36900
   220
#673 := (and #668 #671)
boehmes@36900
   221
#676 := (not #673)
boehmes@36900
   222
#882 := (or #441 #432 #676 #762 #799 #806 #812 #818)
boehmes@36900
   223
#858 := (or #393 #375 #366 #815 #676 #762 #799 #806 #812 #819)
boehmes@36900
   224
#887 := (and #858 #882)
boehmes@36900
   225
#908 := (or #676 #724 #887)
boehmes@36900
   226
#705 := (* -1::int f10)
boehmes@36900
   227
#706 := (+ #24 #705)
boehmes@36900
   228
#707 := (<= #706 0::int)
boehmes@36900
   229
#682 := (not #681)
boehmes@36900
   230
#685 := (and #641 #682)
boehmes@36900
   231
#688 := (not #685)
boehmes@36900
   232
#710 := (or #688 #707)
boehmes@36900
   233
#713 := (forall (vars (?v0 int)) #710)
boehmes@36900
   234
#694 := (or #51 #688)
boehmes@36900
   235
#699 := (exists (vars (?v0 int)) #694)
boehmes@36900
   236
#702 := (not #699)
boehmes@36900
   237
#716 := (or #702 #713)
boehmes@36900
   238
#719 := (and #699 #716)
boehmes@36900
   239
#748 := (or #241 #232 #223 #676 #719 #727)
boehmes@36900
   240
#913 := (and #748 #908)
boehmes@36900
   241
#561 := (not #13)
boehmes@36900
   242
#956 := (or #561 #528 #676 #913 #938)
boehmes@36900
   243
#961 := (and #13 #956)
boehmes@36900
   244
#642 := (not #644)
boehmes@36900
   245
#646 := (and #641 #642)
boehmes@36900
   246
#649 := (not #646)
boehmes@36900
   247
#658 := (or #649 #654)
boehmes@36900
   248
#661 := (forall (vars (?v0 int)) #658)
boehmes@36900
   249
#664 := (not #661)
boehmes@36900
   250
#964 := (or #664 #961)
boehmes@36900
   251
#967 := (and #661 #964)
boehmes@36900
   252
#990 := (or #561 #967 #970)
boehmes@36900
   253
#995 := (not #990)
boehmes@34994
   254
#1 := true
boehmes@36900
   255
#91 := (= #90 f14)
boehmes@36900
   256
#92 := (and #91 true)
boehmes@36900
   257
#87 := (<= #24 f14)
boehmes@36900
   258
#85 := (< #20 f15)
boehmes@36900
   259
#21 := (<= 0::int #20)
boehmes@36900
   260
#86 := (and #21 #85)
boehmes@36900
   261
#88 := (implies #86 #87)
boehmes@36900
   262
#89 := (forall (vars (?v0 int)) #88)
boehmes@36900
   263
#93 := (implies #89 #92)
boehmes@36900
   264
#94 := (and #89 #93)
boehmes@36900
   265
#83 := (<= 2::int f15)
boehmes@36900
   266
#77 := (<= 0::int f13)
boehmes@36900
   267
#84 := (and #77 #83)
boehmes@36900
   268
#95 := (implies #84 #94)
boehmes@36900
   269
#80 := (+ f7 1::int)
boehmes@36900
   270
#81 := (= f15 #80)
boehmes@36900
   271
#96 := (implies #81 #95)
boehmes@36900
   272
#32 := (<= 1::int f7)
boehmes@36900
   273
#78 := (and #77 #32)
boehmes@36900
   274
#97 := (implies #78 #96)
boehmes@36900
   275
#98 := (implies true #97)
boehmes@36900
   276
#108 := (= f14 f8)
boehmes@36900
   277
#109 := (implies #108 #98)
boehmes@36900
   278
#107 := (= f13 f6)
boehmes@36900
   279
#110 := (implies #107 #109)
boehmes@36900
   280
#30 := (<= 0::int f6)
boehmes@36900
   281
#33 := (and #30 #32)
boehmes@36900
   282
#111 := (implies #33 #110)
boehmes@36900
   283
#106 := (<= #68 f8)
boehmes@36900
   284
#112 := (implies #106 #111)
boehmes@36900
   285
#113 := (implies #33 #112)
boehmes@36900
   286
#114 := (implies true #113)
boehmes@36900
   287
#76 := (= f14 f12)
boehmes@36900
   288
#99 := (implies #76 #98)
boehmes@36900
   289
#74 := (= f13 f7)
boehmes@36900
   290
#100 := (implies #74 #99)
boehmes@36900
   291
#72 := (and #32 #32)
boehmes@36900
   292
#101 := (implies #72 #100)
boehmes@36900
   293
#71 := (= f12 #68)
boehmes@36900
   294
#102 := (implies #71 #101)
boehmes@36900
   295
#69 := (< f8 #68)
boehmes@36900
   296
#103 := (implies #69 #102)
boehmes@36900
   297
#104 := (implies #33 #103)
boehmes@36900
   298
#105 := (implies true #104)
boehmes@36900
   299
#115 := (and #105 #114)
boehmes@36900
   300
#116 := (implies #33 #115)
boehmes@36900
   301
#67 := (< f7 f3)
boehmes@36900
   302
#117 := (implies #67 #116)
boehmes@36900
   303
#118 := (implies #33 #117)
boehmes@36900
   304
#119 := (implies true #118)
boehmes@36900
   305
#54 := (<= #24 f10)
boehmes@36900
   306
#49 := (< #20 f3)
boehmes@36900
   307
#50 := (and #21 #49)
boehmes@36900
   308
#55 := (implies #50 #54)
boehmes@36900
   309
#56 := (forall (vars (?v0 int)) #55)
boehmes@36900
   310
#57 := (and #56 true)
boehmes@36900
   311
#52 := (implies #50 #51)
boehmes@36900
   312
#53 := (exists (vars (?v0 int)) #52)
boehmes@36900
   313
#58 := (implies #53 #57)
boehmes@36900
   314
#59 := (and #53 #58)
boehmes@36900
   315
#48 := (= f11 f7)
boehmes@36900
   316
#60 := (implies #48 #59)
boehmes@36900
   317
#46 := (= f10 f8)
boehmes@36900
   318
#61 := (implies #46 #60)
boehmes@36900
   319
#44 := (= f9 f6)
boehmes@36900
   320
#62 := (implies #44 #61)
boehmes@36900
   321
#63 := (implies #33 #62)
boehmes@36900
   322
#42 := (<= f3 f7)
boehmes@36900
   323
#64 := (implies #42 #63)
boehmes@36900
   324
#65 := (implies #33 #64)
boehmes@36900
   325
#66 := (implies true #65)
boehmes@36900
   326
#120 := (and #66 #119)
boehmes@36900
   327
#121 := (implies #33 #120)
boehmes@36900
   328
#41 := (= #40 f8)
boehmes@36900
   329
#122 := (implies #41 #121)
boehmes@36900
   330
#37 := (<= #24 f8)
boehmes@36900
   331
#34 := (< #20 f7)
boehmes@36900
   332
#35 := (and #21 #34)
boehmes@36900
   333
#38 := (implies #35 #37)
boehmes@36900
   334
#39 := (forall (vars (?v0 int)) #38)
boehmes@36900
   335
#123 := (implies #39 #122)
boehmes@36900
   336
#124 := (implies #33 #123)
boehmes@36900
   337
#125 := (implies true #124)
boehmes@36900
   338
#28 := (= #12 f4)
boehmes@36900
   339
#126 := (implies #28 #125)
boehmes@36900
   340
#127 := (and #28 #126)
boehmes@36900
   341
#25 := (<= #24 f4)
boehmes@36900
   342
#22 := (< #20 1::int)
boehmes@36900
   343
#23 := (and #21 #22)
boehmes@36900
   344
#26 := (implies #23 #25)
boehmes@36900
   345
#27 := (forall (vars (?v0 int)) #26)
boehmes@36900
   346
#128 := (implies #27 #127)
boehmes@36900
   347
#129 := (and #27 #128)
boehmes@36900
   348
#16 := (<= 1::int 1::int)
boehmes@36900
   349
#17 := (and #16 #16)
boehmes@36900
   350
#14 := (<= 0::int 0::int)
boehmes@36900
   351
#18 := (and #14 #17)
boehmes@36900
   352
#19 := (and #14 #18)
boehmes@36900
   353
#130 := (implies #19 #129)
boehmes@36900
   354
#131 := (implies #13 #130)
boehmes@36900
   355
#10 := (< 0::int f3)
boehmes@36900
   356
#132 := (implies #10 #131)
boehmes@36900
   357
#133 := (implies true #132)
boehmes@36900
   358
#134 := (not #133)
boehmes@36900
   359
#998 := (iff #134 #995)
boehmes@36900
   360
#300 := (not #86)
boehmes@36900
   361
#301 := (or #300 #87)
boehmes@36900
   362
#304 := (forall (vars (?v0 int)) #301)
boehmes@36900
   363
#320 := (not #304)
boehmes@36900
   364
#321 := (or #320 #307)
boehmes@36900
   365
#326 := (and #304 #321)
boehmes@36900
   366
#332 := (not #84)
boehmes@36900
   367
#333 := (or #332 #326)
boehmes@36900
   368
#294 := (+ 1::int f7)
boehmes@36900
   369
#297 := (= f15 #294)
boehmes@36900
   370
#341 := (not #297)
boehmes@36900
   371
#342 := (or #341 #333)
boehmes@36900
   372
#291 := (and #32 #77)
boehmes@36900
   373
#350 := (not #291)
boehmes@36900
   374
#351 := (or #350 #342)
boehmes@36900
   375
#433 := (or #351 #432)
boehmes@36900
   376
#442 := (or #441 #433)
boehmes@36900
   377
#250 := (not #33)
boehmes@36900
   378
#450 := (or #250 #442)
boehmes@36900
   379
#458 := (not #106)
boehmes@36900
   380
#459 := (or #458 #450)
boehmes@36900
   381
#467 := (or #250 #459)
boehmes@36900
   382
#367 := (or #366 #351)
boehmes@36900
   383
#376 := (or #375 #367)
boehmes@36900
   384
#384 := (not #32)
boehmes@36900
   385
#385 := (or #384 #376)
boehmes@36900
   386
#394 := (or #393 #385)
boehmes@36900
   387
#402 := (not #69)
boehmes@36900
   388
#403 := (or #402 #394)
boehmes@36900
   389
#411 := (or #250 #403)
boehmes@36900
   390
#479 := (and #411 #467)
boehmes@36900
   391
#485 := (or #250 #479)
boehmes@36900
   392
#493 := (not #67)
boehmes@36900
   393
#494 := (or #493 #485)
boehmes@36900
   394
#502 := (or #250 #494)
boehmes@36900
   395
#188 := (not #50)
boehmes@36900
   396
#195 := (or #188 #54)
boehmes@36900
   397
#198 := (forall (vars (?v0 int)) #195)
boehmes@36900
   398
#189 := (or #188 #51)
boehmes@36900
   399
#192 := (exists (vars (?v0 int)) #189)
boehmes@36900
   400
#211 := (not #192)
boehmes@36900
   401
#212 := (or #211 #198)
boehmes@36900
   402
#217 := (and #192 #212)
boehmes@36900
   403
#224 := (or #223 #217)
boehmes@36900
   404
#233 := (or #232 #224)
boehmes@36900
   405
#242 := (or #241 #233)
boehmes@36900
   406
#251 := (or #250 #242)
boehmes@36900
   407
#259 := (not #42)
boehmes@36900
   408
#260 := (or #259 #251)
boehmes@36900
   409
#268 := (or #250 #260)
boehmes@36900
   410
#514 := (and #268 #502)
boehmes@36900
   411
#520 := (or #250 #514)
boehmes@36900
   412
#529 := (or #528 #520)
boehmes@36900
   413
#169 := (not #35)
boehmes@36900
   414
#170 := (or #169 #37)
boehmes@36900
   415
#173 := (forall (vars (?v0 int)) #170)
boehmes@36900
   416
#537 := (not #173)
boehmes@36900
   417
#538 := (or #537 #529)
boehmes@36900
   418
#546 := (or #250 #538)
boehmes@36900
   419
#562 := (or #561 #546)
boehmes@36900
   420
#567 := (and #13 #562)
boehmes@36900
   421
#160 := (not #23)
boehmes@36900
   422
#161 := (or #160 #25)
boehmes@36900
   423
#164 := (forall (vars (?v0 int)) #161)
boehmes@36900
   424
#573 := (not #164)
boehmes@36900
   425
#574 := (or #573 #567)
boehmes@36900
   426
#579 := (and #164 #574)
boehmes@36900
   427
#154 := (and #14 #16)
boehmes@36900
   428
#157 := (and #14 #154)
boehmes@36900
   429
#585 := (not #157)
boehmes@36900
   430
#586 := (or #585 #579)
boehmes@36900
   431
#594 := (or #561 #586)
boehmes@36900
   432
#602 := (not #10)
boehmes@36900
   433
#603 := (or #602 #594)
boehmes@36900
   434
#615 := (not #603)
boehmes@36900
   435
#996 := (iff #615 #995)
boehmes@36900
   436
#993 := (iff #603 #990)
boehmes@36900
   437
#981 := (or false #967)
boehmes@36900
   438
#984 := (or #561 #981)
boehmes@36900
   439
#987 := (or #970 #984)
boehmes@36900
   440
#991 := (iff #987 #990)
boehmes@36900
   441
#992 := [rewrite]: #991
boehmes@36900
   442
#988 := (iff #603 #987)
boehmes@36900
   443
#985 := (iff #594 #984)
boehmes@36900
   444
#982 := (iff #586 #981)
boehmes@36900
   445
#968 := (iff #579 #967)
boehmes@36900
   446
#965 := (iff #574 #964)
boehmes@36900
   447
#962 := (iff #567 #961)
boehmes@36900
   448
#959 := (iff #562 #956)
boehmes@36900
   449
#941 := (or #676 #913)
boehmes@36900
   450
#944 := (or #528 #941)
boehmes@36900
   451
#947 := (or #938 #944)
boehmes@36900
   452
#950 := (or #676 #947)
boehmes@36900
   453
#953 := (or #561 #950)
boehmes@36900
   454
#957 := (iff #953 #956)
boehmes@36900
   455
#958 := [rewrite]: #957
boehmes@36900
   456
#954 := (iff #562 #953)
boehmes@36900
   457
#951 := (iff #546 #950)
boehmes@36900
   458
#948 := (iff #538 #947)
boehmes@36900
   459
#945 := (iff #529 #944)
boehmes@36900
   460
#942 := (iff #520 #941)
boehmes@36900
   461
#914 := (iff #514 #913)
boehmes@36900
   462
#911 := (iff #502 #908)
boehmes@36900
   463
#899 := (or #676 #887)
boehmes@36900
   464
#902 := (or #724 #899)
boehmes@36900
   465
#905 := (or #676 #902)
boehmes@36900
   466
#909 := (iff #905 #908)
boehmes@36900
   467
#910 := [rewrite]: #909
boehmes@36900
   468
#906 := (iff #502 #905)
boehmes@36900
   469
#903 := (iff #494 #902)
boehmes@36900
   470
#900 := (iff #485 #899)
boehmes@36900
   471
#888 := (iff #479 #887)
boehmes@36900
   472
#885 := (iff #467 #882)
boehmes@36900
   473
#831 := (or #762 #799)
boehmes@36900
   474
#834 := (or #806 #831)
boehmes@36900
   475
#837 := (or #812 #834)
boehmes@36900
   476
#867 := (or #837 #432)
boehmes@36900
   477
#870 := (or #441 #867)
boehmes@36900
   478
#873 := (or #676 #870)
boehmes@36900
   479
#876 := (or #818 #873)
boehmes@36900
   480
#879 := (or #676 #876)
boehmes@36900
   481
#883 := (iff #879 #882)
boehmes@36900
   482
#884 := [rewrite]: #883
boehmes@36900
   483
#880 := (iff #467 #879)
boehmes@36900
   484
#877 := (iff #459 #876)
boehmes@36900
   485
#874 := (iff #450 #873)
boehmes@36900
   486
#871 := (iff #442 #870)
boehmes@36900
   487
#868 := (iff #433 #867)
boehmes@36900
   488
#838 := (iff #351 #837)
boehmes@36900
   489
#835 := (iff #342 #834)
boehmes@36900
   490
#832 := (iff #333 #831)
boehmes@36900
   491
#800 := (iff #326 #799)
boehmes@36900
   492
#797 := (iff #321 #794)
boehmes@36900
   493
#791 := (or #788 #307)
boehmes@36900
   494
#795 := (iff #791 #794)
boehmes@36900
   495
#796 := [rewrite]: #795
boehmes@36900
   496
#792 := (iff #321 #791)
boehmes@36900
   497
#789 := (iff #320 #788)
boehmes@36900
   498
#786 := (iff #304 #785)
boehmes@36900
   499
#783 := (iff #301 #782)
boehmes@36900
   500
#780 := (iff #87 #779)
boehmes@36900
   501
#781 := [rewrite]: #780
boehmes@36900
   502
#775 := (iff #300 #774)
boehmes@36900
   503
#772 := (iff #86 #771)
boehmes@36900
   504
#769 := (iff #85 #768)
boehmes@36900
   505
#770 := [rewrite]: #769
boehmes@36900
   506
#639 := (iff #21 #641)
boehmes@36900
   507
#640 := [rewrite]: #639
boehmes@36900
   508
#773 := [monotonicity #640 #770]: #772
boehmes@36900
   509
#776 := [monotonicity #773]: #775
boehmes@36900
   510
#784 := [monotonicity #776 #781]: #783
boehmes@36900
   511
#787 := [quant-intro #784]: #786
boehmes@36900
   512
#790 := [monotonicity #787]: #789
boehmes@36900
   513
#793 := [monotonicity #790]: #792
boehmes@36900
   514
#798 := [trans #793 #796]: #797
boehmes@36900
   515
#801 := [monotonicity #787 #798]: #800
boehmes@36900
   516
#763 := (iff #332 #762)
boehmes@36900
   517
#760 := (iff #84 #759)
boehmes@36900
   518
#756 := (iff #83 #757)
boehmes@36900
   519
#758 := [rewrite]: #756
boehmes@36900
   520
#753 := (iff #77 #754)
boehmes@36900
   521
#755 := [rewrite]: #753
boehmes@36900
   522
#761 := [monotonicity #755 #758]: #760
boehmes@36900
   523
#764 := [monotonicity #761]: #763
boehmes@36900
   524
#833 := [monotonicity #764 #801]: #832
boehmes@36900
   525
#807 := (iff #341 #806)
boehmes@36900
   526
#804 := (iff #297 #802)
boehmes@36900
   527
#805 := [rewrite]: #804
boehmes@36900
   528
#808 := [monotonicity #805]: #807
boehmes@36900
   529
#836 := [monotonicity #808 #833]: #835
boehmes@36900
   530
#813 := (iff #350 #812)
boehmes@36900
   531
#810 := (iff #291 #809)
boehmes@36900
   532
#670 := (iff #32 #671)
boehmes@36900
   533
#672 := [rewrite]: #670
boehmes@36900
   534
#811 := [monotonicity #672 #755]: #810
boehmes@36900
   535
#814 := [monotonicity #811]: #813
boehmes@36900
   536
#839 := [monotonicity #814 #836]: #838
boehmes@36900
   537
#869 := [monotonicity #839]: #868
boehmes@36900
   538
#872 := [monotonicity #869]: #871
boehmes@36900
   539
#677 := (iff #250 #676)
boehmes@36900
   540
#674 := (iff #33 #673)
boehmes@36900
   541
#667 := (iff #30 #668)
boehmes@36900
   542
#669 := [rewrite]: #667
boehmes@36900
   543
#675 := [monotonicity #669 #672]: #674
boehmes@36900
   544
#678 := [monotonicity #675]: #677
boehmes@36900
   545
#875 := [monotonicity #678 #872]: #874
boehmes@36900
   546
#865 := (iff #458 #818)
boehmes@36900
   547
#863 := (iff #106 #819)
boehmes@36900
   548
#864 := [rewrite]: #863
boehmes@36900
   549
#866 := [monotonicity #864]: #865
boehmes@36900
   550
#878 := [monotonicity #866 #875]: #877
boehmes@36900
   551
#881 := [monotonicity #678 #878]: #880
boehmes@36900
   552
#886 := [trans #881 #884]: #885
boehmes@36900
   553
#861 := (iff #411 #858)
boehmes@36900
   554
#840 := (or #366 #837)
boehmes@36900
   555
#843 := (or #375 #840)
boehmes@36900
   556
#846 := (or #815 #843)
boehmes@36900
   557
#849 := (or #393 #846)
boehmes@36900
   558
#852 := (or #819 #849)
boehmes@36900
   559
#855 := (or #676 #852)
boehmes@36900
   560
#859 := (iff #855 #858)
boehmes@36900
   561
#860 := [rewrite]: #859
boehmes@36900
   562
#856 := (iff #411 #855)
boehmes@36900
   563
#853 := (iff #403 #852)
boehmes@36900
   564
#850 := (iff #394 #849)
boehmes@36900
   565
#847 := (iff #385 #846)
boehmes@36900
   566
#844 := (iff #376 #843)
boehmes@36900
   567
#841 := (iff #367 #840)
boehmes@36900
   568
#842 := [monotonicity #839]: #841
boehmes@36900
   569
#845 := [monotonicity #842]: #844
boehmes@36900
   570
#816 := (iff #384 #815)
boehmes@36900
   571
#817 := [monotonicity #672]: #816
boehmes@36900
   572
#848 := [monotonicity #817 #845]: #847
boehmes@36900
   573
#851 := [monotonicity #848]: #850
boehmes@36900
   574
#829 := (iff #402 #819)
boehmes@36900
   575
#824 := (not #818)
boehmes@36900
   576
#827 := (iff #824 #819)
boehmes@36900
   577
#828 := [rewrite]: #827
boehmes@36900
   578
#825 := (iff #402 #824)
boehmes@36900
   579
#822 := (iff #69 #818)
boehmes@34994
   580
#823 := [rewrite]: #822
boehmes@36900
   581
#826 := [monotonicity #823]: #825
boehmes@36900
   582
#830 := [trans #826 #828]: #829
boehmes@36900
   583
#854 := [monotonicity #830 #851]: #853
boehmes@36900
   584
#857 := [monotonicity #678 #854]: #856
boehmes@36900
   585
#862 := [trans #857 #860]: #861
boehmes@36900
   586
#889 := [monotonicity #862 #886]: #888
boehmes@36900
   587
#901 := [monotonicity #678 #889]: #900
boehmes@36900
   588
#897 := (iff #493 #724)
boehmes@36900
   589
#892 := (not #727)
boehmes@36900
   590
#895 := (iff #892 #724)
boehmes@36900
   591
#896 := [rewrite]: #895
boehmes@36900
   592
#893 := (iff #493 #892)
boehmes@36900
   593
#890 := (iff #67 #727)
boehmes@34994
   594
#891 := [rewrite]: #890
boehmes@36900
   595
#894 := [monotonicity #891]: #893
boehmes@36900
   596
#898 := [trans #894 #896]: #897
boehmes@36900
   597
#904 := [monotonicity #898 #901]: #903
boehmes@36900
   598
#907 := [monotonicity #678 #904]: #906
boehmes@36900
   599
#912 := [trans #907 #910]: #911
boehmes@36900
   600
#751 := (iff #268 #748)
boehmes@36900
   601
#730 := (or #223 #719)
boehmes@36900
   602
#733 := (or #232 #730)
boehmes@36900
   603
#736 := (or #241 #733)
boehmes@36900
   604
#739 := (or #676 #736)
boehmes@36900
   605
#742 := (or #727 #739)
boehmes@36900
   606
#745 := (or #676 #742)
boehmes@36900
   607
#749 := (iff #745 #748)
boehmes@36900
   608
#750 := [rewrite]: #749
boehmes@36900
   609
#746 := (iff #268 #745)
boehmes@36900
   610
#743 := (iff #260 #742)
boehmes@36900
   611
#740 := (iff #251 #739)
boehmes@36900
   612
#737 := (iff #242 #736)
boehmes@36900
   613
#734 := (iff #233 #733)
boehmes@36900
   614
#731 := (iff #224 #730)
boehmes@36900
   615
#720 := (iff #217 #719)
boehmes@36900
   616
#717 := (iff #212 #716)
boehmes@36900
   617
#714 := (iff #198 #713)
boehmes@36900
   618
#711 := (iff #195 #710)
boehmes@36900
   619
#708 := (iff #54 #707)
boehmes@36900
   620
#709 := [rewrite]: #708
boehmes@36900
   621
#689 := (iff #188 #688)
boehmes@36900
   622
#686 := (iff #50 #685)
boehmes@36900
   623
#683 := (iff #49 #682)
boehmes@36900
   624
#684 := [rewrite]: #683
boehmes@36900
   625
#687 := [monotonicity #640 #684]: #686
boehmes@36900
   626
#690 := [monotonicity #687]: #689
boehmes@36900
   627
#712 := [monotonicity #690 #709]: #711
boehmes@36900
   628
#715 := [quant-intro #712]: #714
boehmes@36900
   629
#703 := (iff #211 #702)
boehmes@36900
   630
#700 := (iff #192 #699)
boehmes@36900
   631
#697 := (iff #189 #694)
boehmes@36900
   632
#691 := (or #688 #51)
boehmes@36900
   633
#695 := (iff #691 #694)
boehmes@36900
   634
#696 := [rewrite]: #695
boehmes@36900
   635
#692 := (iff #189 #691)
boehmes@36900
   636
#693 := [monotonicity #690]: #692
boehmes@36900
   637
#698 := [trans #693 #696]: #697
boehmes@36900
   638
#701 := [quant-intro #698]: #700
boehmes@36900
   639
#704 := [monotonicity #701]: #703
boehmes@36900
   640
#718 := [monotonicity #704 #715]: #717
boehmes@36900
   641
#721 := [monotonicity #701 #718]: #720
boehmes@36900
   642
#732 := [monotonicity #721]: #731
boehmes@36900
   643
#735 := [monotonicity #732]: #734
boehmes@36900
   644
#738 := [monotonicity #735]: #737
boehmes@36900
   645
#741 := [monotonicity #678 #738]: #740
boehmes@36900
   646
#728 := (iff #259 #727)
boehmes@36900
   647
#725 := (iff #42 #724)
boehmes@36900
   648
#726 := [rewrite]: #725
boehmes@36900
   649
#729 := [monotonicity #726]: #728
boehmes@36900
   650
#744 := [monotonicity #729 #741]: #743
boehmes@36900
   651
#747 := [monotonicity #678 #744]: #746
boehmes@36900
   652
#752 := [trans #747 #750]: #751
boehmes@36900
   653
#915 := [monotonicity #752 #912]: #914
boehmes@36900
   654
#943 := [monotonicity #678 #915]: #942
boehmes@36900
   655
#946 := [monotonicity #943]: #945
boehmes@36900
   656
#939 := (iff #537 #938)
boehmes@36900
   657
#936 := (iff #173 #935)
boehmes@36900
   658
#933 := (iff #170 #932)
boehmes@36900
   659
#930 := (iff #37 #929)
boehmes@36900
   660
#931 := [rewrite]: #930
boehmes@36900
   661
#925 := (iff #169 #924)
boehmes@36900
   662
#922 := (iff #35 #921)
boehmes@36900
   663
#919 := (iff #34 #918)
boehmes@36900
   664
#920 := [rewrite]: #919
boehmes@36900
   665
#923 := [monotonicity #640 #920]: #922
boehmes@36900
   666
#926 := [monotonicity #923]: #925
boehmes@36900
   667
#934 := [monotonicity #926 #931]: #933
boehmes@36900
   668
#937 := [quant-intro #934]: #936
boehmes@36900
   669
#940 := [monotonicity #937]: #939
boehmes@36900
   670
#949 := [monotonicity #940 #946]: #948
boehmes@36900
   671
#952 := [monotonicity #678 #949]: #951
boehmes@36900
   672
#955 := [monotonicity #952]: #954
boehmes@36900
   673
#960 := [trans #955 #958]: #959
boehmes@36900
   674
#963 := [monotonicity #960]: #962
boehmes@36900
   675
#665 := (iff #573 #664)
boehmes@36900
   676
#662 := (iff #164 #661)
boehmes@36900
   677
#659 := (iff #161 #658)
boehmes@36900
   678
#653 := (iff #25 #654)
boehmes@36900
   679
#657 := [rewrite]: #653
boehmes@36900
   680
#650 := (iff #160 #649)
boehmes@36900
   681
#647 := (iff #23 #646)
boehmes@36900
   682
#643 := (iff #22 #642)
boehmes@36900
   683
#645 := [rewrite]: #643
boehmes@36900
   684
#648 := [monotonicity #640 #645]: #647
boehmes@36900
   685
#651 := [monotonicity #648]: #650
boehmes@36900
   686
#660 := [monotonicity #651 #657]: #659
boehmes@36900
   687
#663 := [quant-intro #660]: #662
boehmes@36900
   688
#666 := [monotonicity #663]: #665
boehmes@36900
   689
#966 := [monotonicity #666 #963]: #965
boehmes@36900
   690
#969 := [monotonicity #663 #966]: #968
boehmes@36900
   691
#637 := (iff #585 false)
boehmes@36900
   692
#632 := (not true)
boehmes@36900
   693
#635 := (iff #632 false)
boehmes@36900
   694
#636 := [rewrite]: #635
boehmes@36900
   695
#633 := (iff #585 #632)
boehmes@36900
   696
#630 := (iff #157 true)
boehmes@36900
   697
#622 := (and true true)
boehmes@36900
   698
#625 := (and true #622)
boehmes@36900
   699
#628 := (iff #625 true)
boehmes@36900
   700
#629 := [rewrite]: #628
boehmes@36900
   701
#626 := (iff #157 #625)
boehmes@36900
   702
#623 := (iff #154 #622)
boehmes@36900
   703
#620 := (iff #16 true)
boehmes@36900
   704
#621 := [rewrite]: #620
boehmes@36900
   705
#618 := (iff #14 true)
boehmes@36900
   706
#619 := [rewrite]: #618
boehmes@36900
   707
#624 := [monotonicity #619 #621]: #623
boehmes@36900
   708
#627 := [monotonicity #619 #624]: #626
boehmes@36900
   709
#631 := [trans #627 #629]: #630
boehmes@36900
   710
#634 := [monotonicity #631]: #633
boehmes@36900
   711
#638 := [trans #634 #636]: #637
boehmes@36900
   712
#983 := [monotonicity #638 #969]: #982
boehmes@36900
   713
#986 := [monotonicity #983]: #985
boehmes@36900
   714
#979 := (iff #602 #970)
boehmes@36900
   715
#971 := (not #970)
boehmes@36900
   716
#974 := (not #971)
boehmes@36900
   717
#977 := (iff #974 #970)
boehmes@36900
   718
#978 := [rewrite]: #977
boehmes@36900
   719
#975 := (iff #602 #974)
boehmes@36900
   720
#972 := (iff #10 #971)
boehmes@34994
   721
#973 := [rewrite]: #972
boehmes@36900
   722
#976 := [monotonicity #973]: #975
boehmes@36900
   723
#980 := [trans #976 #978]: #979
boehmes@36900
   724
#989 := [monotonicity #980 #986]: #988
boehmes@36900
   725
#994 := [trans #989 #992]: #993
boehmes@36900
   726
#997 := [monotonicity #994]: #996
boehmes@36900
   727
#616 := (iff #134 #615)
boehmes@36900
   728
#613 := (iff #133 #603)
boehmes@36900
   729
#608 := (implies true #603)
boehmes@36900
   730
#611 := (iff #608 #603)
boehmes@36900
   731
#612 := [rewrite]: #611
boehmes@36900
   732
#609 := (iff #133 #608)
boehmes@36900
   733
#606 := (iff #132 #603)
boehmes@36900
   734
#599 := (implies #10 #594)
boehmes@36900
   735
#604 := (iff #599 #603)
boehmes@36900
   736
#605 := [rewrite]: #604
boehmes@36900
   737
#600 := (iff #132 #599)
boehmes@36900
   738
#597 := (iff #131 #594)
boehmes@36900
   739
#591 := (implies #13 #586)
boehmes@36900
   740
#595 := (iff #591 #594)
boehmes@36900
   741
#596 := [rewrite]: #595
boehmes@36900
   742
#592 := (iff #131 #591)
boehmes@36900
   743
#589 := (iff #130 #586)
boehmes@36900
   744
#582 := (implies #157 #579)
boehmes@36900
   745
#587 := (iff #582 #586)
boehmes@36900
   746
#588 := [rewrite]: #587
boehmes@36900
   747
#583 := (iff #130 #582)
boehmes@36900
   748
#580 := (iff #129 #579)
boehmes@36900
   749
#577 := (iff #128 #574)
boehmes@36900
   750
#570 := (implies #164 #567)
boehmes@36900
   751
#575 := (iff #570 #574)
boehmes@36900
   752
#576 := [rewrite]: #575
boehmes@36900
   753
#571 := (iff #128 #570)
boehmes@36900
   754
#568 := (iff #127 #567)
boehmes@36900
   755
#565 := (iff #126 #562)
boehmes@36900
   756
#558 := (implies #13 #546)
boehmes@36900
   757
#563 := (iff #558 #562)
boehmes@36900
   758
#564 := [rewrite]: #563
boehmes@36900
   759
#559 := (iff #126 #558)
boehmes@36900
   760
#556 := (iff #125 #546)
boehmes@36900
   761
#551 := (implies true #546)
boehmes@36900
   762
#554 := (iff #551 #546)
boehmes@36900
   763
#555 := [rewrite]: #554
boehmes@36900
   764
#552 := (iff #125 #551)
boehmes@36900
   765
#549 := (iff #124 #546)
boehmes@36900
   766
#543 := (implies #33 #538)
boehmes@36900
   767
#547 := (iff #543 #546)
boehmes@36900
   768
#548 := [rewrite]: #547
boehmes@36900
   769
#544 := (iff #124 #543)
boehmes@36900
   770
#541 := (iff #123 #538)
boehmes@36900
   771
#534 := (implies #173 #529)
boehmes@36900
   772
#539 := (iff #534 #538)
boehmes@36900
   773
#540 := [rewrite]: #539
boehmes@36900
   774
#535 := (iff #123 #534)
boehmes@36900
   775
#532 := (iff #122 #529)
boehmes@36900
   776
#525 := (implies #176 #520)
boehmes@36900
   777
#530 := (iff #525 #529)
boehmes@36900
   778
#531 := [rewrite]: #530
boehmes@36900
   779
#526 := (iff #122 #525)
boehmes@36900
   780
#523 := (iff #121 #520)
boehmes@36900
   781
#517 := (implies #33 #514)
boehmes@36900
   782
#521 := (iff #517 #520)
boehmes@36900
   783
#522 := [rewrite]: #521
boehmes@36900
   784
#518 := (iff #121 #517)
boehmes@36900
   785
#515 := (iff #120 #514)
boehmes@36900
   786
#512 := (iff #119 #502)
boehmes@36900
   787
#507 := (implies true #502)
boehmes@36900
   788
#510 := (iff #507 #502)
boehmes@36900
   789
#511 := [rewrite]: #510
boehmes@36900
   790
#508 := (iff #119 #507)
boehmes@36900
   791
#505 := (iff #118 #502)
boehmes@36900
   792
#499 := (implies #33 #494)
boehmes@36900
   793
#503 := (iff #499 #502)
boehmes@36900
   794
#504 := [rewrite]: #503
boehmes@36900
   795
#500 := (iff #118 #499)
boehmes@36900
   796
#497 := (iff #117 #494)
boehmes@36900
   797
#490 := (implies #67 #485)
boehmes@36900
   798
#495 := (iff #490 #494)
boehmes@36900
   799
#496 := [rewrite]: #495
boehmes@36900
   800
#491 := (iff #117 #490)
boehmes@36900
   801
#488 := (iff #116 #485)
boehmes@36900
   802
#482 := (implies #33 #479)
boehmes@36900
   803
#486 := (iff #482 #485)
boehmes@36900
   804
#487 := [rewrite]: #486
boehmes@36900
   805
#483 := (iff #116 #482)
boehmes@36900
   806
#480 := (iff #115 #479)
boehmes@36900
   807
#477 := (iff #114 #467)
boehmes@36900
   808
#472 := (implies true #467)
boehmes@36900
   809
#475 := (iff #472 #467)
boehmes@36900
   810
#476 := [rewrite]: #475
boehmes@36900
   811
#473 := (iff #114 #472)
boehmes@36900
   812
#470 := (iff #113 #467)
boehmes@36900
   813
#464 := (implies #33 #459)
boehmes@36900
   814
#468 := (iff #464 #467)
boehmes@36900
   815
#469 := [rewrite]: #468
boehmes@36900
   816
#465 := (iff #113 #464)
boehmes@36900
   817
#462 := (iff #112 #459)
boehmes@36900
   818
#455 := (implies #106 #450)
boehmes@36900
   819
#460 := (iff #455 #459)
boehmes@36900
   820
#461 := [rewrite]: #460
boehmes@36900
   821
#456 := (iff #112 #455)
boehmes@36900
   822
#453 := (iff #111 #450)
boehmes@36900
   823
#447 := (implies #33 #442)
boehmes@36900
   824
#451 := (iff #447 #450)
boehmes@36900
   825
#452 := [rewrite]: #451
boehmes@36900
   826
#448 := (iff #111 #447)
boehmes@36900
   827
#445 := (iff #110 #442)
boehmes@36900
   828
#438 := (implies #423 #433)
boehmes@36900
   829
#443 := (iff #438 #442)
boehmes@36900
   830
#444 := [rewrite]: #443
boehmes@36900
   831
#439 := (iff #110 #438)
boehmes@36900
   832
#436 := (iff #109 #433)
boehmes@36900
   833
#429 := (implies #426 #351)
boehmes@36900
   834
#434 := (iff #429 #433)
boehmes@36900
   835
#435 := [rewrite]: #434
boehmes@36900
   836
#430 := (iff #109 #429)
boehmes@36900
   837
#361 := (iff #98 #351)
boehmes@36900
   838
#356 := (implies true #351)
boehmes@36900
   839
#359 := (iff #356 #351)
boehmes@36900
   840
#360 := [rewrite]: #359
boehmes@36900
   841
#357 := (iff #98 #356)
boehmes@36900
   842
#354 := (iff #97 #351)
boehmes@36900
   843
#347 := (implies #291 #342)
boehmes@36900
   844
#352 := (iff #347 #351)
boehmes@36900
   845
#353 := [rewrite]: #352
boehmes@36900
   846
#348 := (iff #97 #347)
boehmes@36900
   847
#345 := (iff #96 #342)
boehmes@36900
   848
#338 := (implies #297 #333)
boehmes@36900
   849
#343 := (iff #338 #342)
boehmes@36900
   850
#344 := [rewrite]: #343
boehmes@36900
   851
#339 := (iff #96 #338)
boehmes@36900
   852
#336 := (iff #95 #333)
boehmes@36900
   853
#329 := (implies #84 #326)
boehmes@36900
   854
#334 := (iff #329 #333)
boehmes@36900
   855
#335 := [rewrite]: #334
boehmes@36900
   856
#330 := (iff #95 #329)
boehmes@36900
   857
#327 := (iff #94 #326)
boehmes@36900
   858
#324 := (iff #93 #321)
boehmes@36900
   859
#317 := (implies #304 #307)
boehmes@36900
   860
#322 := (iff #317 #321)
boehmes@36900
   861
#323 := [rewrite]: #322
boehmes@36900
   862
#318 := (iff #93 #317)
boehmes@36900
   863
#315 := (iff #92 #307)
boehmes@36900
   864
#310 := (and #307 true)
boehmes@36900
   865
#313 := (iff #310 #307)
boehmes@36900
   866
#314 := [rewrite]: #313
boehmes@36900
   867
#311 := (iff #92 #310)
boehmes@36900
   868
#308 := (iff #91 #307)
boehmes@34994
   869
#309 := [rewrite]: #308
boehmes@36900
   870
#312 := [monotonicity #309]: #311
boehmes@36900
   871
#316 := [trans #312 #314]: #315
boehmes@36900
   872
#305 := (iff #89 #304)
boehmes@36900
   873
#302 := (iff #88 #301)
boehmes@36900
   874
#303 := [rewrite]: #302
boehmes@36900
   875
#306 := [quant-intro #303]: #305
boehmes@36900
   876
#319 := [monotonicity #306 #316]: #318
boehmes@36900
   877
#325 := [trans #319 #323]: #324
boehmes@36900
   878
#328 := [monotonicity #306 #325]: #327
boehmes@36900
   879
#331 := [monotonicity #328]: #330
boehmes@36900
   880
#337 := [trans #331 #335]: #336
boehmes@36900
   881
#298 := (iff #81 #297)
boehmes@36900
   882
#295 := (= #80 #294)
boehmes@36900
   883
#296 := [rewrite]: #295
boehmes@36900
   884
#299 := [monotonicity #296]: #298
boehmes@36900
   885
#340 := [monotonicity #299 #337]: #339
boehmes@36900
   886
#346 := [trans #340 #344]: #345
boehmes@36900
   887
#292 := (iff #78 #291)
boehmes@36900
   888
#293 := [rewrite]: #292
boehmes@36900
   889
#349 := [monotonicity #293 #346]: #348
boehmes@36900
   890
#355 := [trans #349 #353]: #354
boehmes@36900
   891
#358 := [monotonicity #355]: #357
boehmes@36900
   892
#362 := [trans #358 #360]: #361
boehmes@36900
   893
#427 := (iff #108 #426)
boehmes@36900
   894
#428 := [rewrite]: #427
boehmes@36900
   895
#431 := [monotonicity #428 #362]: #430
boehmes@36900
   896
#437 := [trans #431 #435]: #436
boehmes@36900
   897
#424 := (iff #107 #423)
boehmes@36900
   898
#425 := [rewrite]: #424
boehmes@36900
   899
#440 := [monotonicity #425 #437]: #439
boehmes@36900
   900
#446 := [trans #440 #444]: #445
boehmes@36900
   901
#449 := [monotonicity #446]: #448
boehmes@36900
   902
#454 := [trans #449 #452]: #453
boehmes@36900
   903
#457 := [monotonicity #454]: #456
boehmes@36900
   904
#463 := [trans #457 #461]: #462
boehmes@36900
   905
#466 := [monotonicity #463]: #465
boehmes@36900
   906
#471 := [trans #466 #469]: #470
boehmes@36900
   907
#474 := [monotonicity #471]: #473
boehmes@36900
   908
#478 := [trans #474 #476]: #477
boehmes@36900
   909
#421 := (iff #105 #411)
boehmes@36900
   910
#416 := (implies true #411)
boehmes@36900
   911
#419 := (iff #416 #411)
boehmes@34994
   912
#420 := [rewrite]: #419
boehmes@36900
   913
#417 := (iff #105 #416)
boehmes@36900
   914
#414 := (iff #104 #411)
boehmes@36900
   915
#408 := (implies #33 #403)
boehmes@36900
   916
#412 := (iff #408 #411)
boehmes@36900
   917
#413 := [rewrite]: #412
boehmes@36900
   918
#409 := (iff #104 #408)
boehmes@36900
   919
#406 := (iff #103 #403)
boehmes@36900
   920
#399 := (implies #69 #394)
boehmes@36900
   921
#404 := (iff #399 #403)
boehmes@36900
   922
#405 := [rewrite]: #404
boehmes@36900
   923
#400 := (iff #103 #399)
boehmes@36900
   924
#397 := (iff #102 #394)
boehmes@36900
   925
#390 := (implies #280 #385)
boehmes@36900
   926
#395 := (iff #390 #394)
boehmes@36900
   927
#396 := [rewrite]: #395
boehmes@36900
   928
#391 := (iff #102 #390)
boehmes@36900
   929
#388 := (iff #101 #385)
boehmes@36900
   930
#381 := (implies #32 #376)
boehmes@36900
   931
#386 := (iff #381 #385)
boehmes@36900
   932
#387 := [rewrite]: #386
boehmes@36900
   933
#382 := (iff #101 #381)
boehmes@36900
   934
#379 := (iff #100 #376)
boehmes@36900
   935
#372 := (implies #285 #367)
boehmes@36900
   936
#377 := (iff #372 #376)
boehmes@36900
   937
#378 := [rewrite]: #377
boehmes@36900
   938
#373 := (iff #100 #372)
boehmes@36900
   939
#370 := (iff #99 #367)
boehmes@36900
   940
#363 := (implies #288 #351)
boehmes@36900
   941
#368 := (iff #363 #367)
boehmes@36900
   942
#369 := [rewrite]: #368
boehmes@36900
   943
#364 := (iff #99 #363)
boehmes@36900
   944
#289 := (iff #76 #288)
boehmes@36900
   945
#290 := [rewrite]: #289
boehmes@36900
   946
#365 := [monotonicity #290 #362]: #364
boehmes@36900
   947
#371 := [trans #365 #369]: #370
boehmes@36900
   948
#286 := (iff #74 #285)
boehmes@36900
   949
#287 := [rewrite]: #286
boehmes@36900
   950
#374 := [monotonicity #287 #371]: #373
boehmes@36900
   951
#380 := [trans #374 #378]: #379
boehmes@36900
   952
#283 := (iff #72 #32)
boehmes@36900
   953
#284 := [rewrite]: #283
boehmes@36900
   954
#383 := [monotonicity #284 #380]: #382
boehmes@36900
   955
#389 := [trans #383 #387]: #388
boehmes@36900
   956
#281 := (iff #71 #280)
boehmes@34994
   957
#282 := [rewrite]: #281
boehmes@36900
   958
#392 := [monotonicity #282 #389]: #391
boehmes@36900
   959
#398 := [trans #392 #396]: #397
boehmes@36900
   960
#401 := [monotonicity #398]: #400
boehmes@36900
   961
#407 := [trans #401 #405]: #406
boehmes@36900
   962
#410 := [monotonicity #407]: #409
boehmes@36900
   963
#415 := [trans #410 #413]: #414
boehmes@36900
   964
#418 := [monotonicity #415]: #417
boehmes@36900
   965
#422 := [trans #418 #420]: #421
boehmes@36900
   966
#481 := [monotonicity #422 #478]: #480
boehmes@36900
   967
#484 := [monotonicity #481]: #483
boehmes@36900
   968
#489 := [trans #484 #487]: #488
boehmes@36900
   969
#492 := [monotonicity #489]: #491
boehmes@36900
   970
#498 := [trans #492 #496]: #497
boehmes@36900
   971
#501 := [monotonicity #498]: #500
boehmes@36900
   972
#506 := [trans #501 #504]: #505
boehmes@36900
   973
#509 := [monotonicity #506]: #508
boehmes@36900
   974
#513 := [trans #509 #511]: #512
boehmes@36900
   975
#278 := (iff #66 #268)
boehmes@36900
   976
#273 := (implies true #268)
boehmes@36900
   977
#276 := (iff #273 #268)
boehmes@34994
   978
#277 := [rewrite]: #276
boehmes@36900
   979
#274 := (iff #66 #273)
boehmes@36900
   980
#271 := (iff #65 #268)
boehmes@36900
   981
#265 := (implies #33 #260)
boehmes@36900
   982
#269 := (iff #265 #268)
boehmes@36900
   983
#270 := [rewrite]: #269
boehmes@36900
   984
#266 := (iff #65 #265)
boehmes@36900
   985
#263 := (iff #64 #260)
boehmes@36900
   986
#256 := (implies #42 #251)
boehmes@36900
   987
#261 := (iff #256 #260)
boehmes@36900
   988
#262 := [rewrite]: #261
boehmes@36900
   989
#257 := (iff #64 #256)
boehmes@36900
   990
#254 := (iff #63 #251)
boehmes@36900
   991
#247 := (implies #33 #242)
boehmes@36900
   992
#252 := (iff #247 #251)
boehmes@36900
   993
#253 := [rewrite]: #252
boehmes@36900
   994
#248 := (iff #63 #247)
boehmes@36900
   995
#245 := (iff #62 #242)
boehmes@36900
   996
#238 := (implies #179 #233)
boehmes@36900
   997
#243 := (iff #238 #242)
boehmes@36900
   998
#244 := [rewrite]: #243
boehmes@36900
   999
#239 := (iff #62 #238)
boehmes@36900
  1000
#236 := (iff #61 #233)
boehmes@36900
  1001
#229 := (implies #182 #224)
boehmes@36900
  1002
#234 := (iff #229 #233)
boehmes@36900
  1003
#235 := [rewrite]: #234
boehmes@36900
  1004
#230 := (iff #61 #229)
boehmes@36900
  1005
#227 := (iff #60 #224)
boehmes@36900
  1006
#220 := (implies #185 #217)
boehmes@36900
  1007
#225 := (iff #220 #224)
boehmes@36900
  1008
#226 := [rewrite]: #225
boehmes@36900
  1009
#221 := (iff #60 #220)
boehmes@36900
  1010
#218 := (iff #59 #217)
boehmes@36900
  1011
#215 := (iff #58 #212)
boehmes@36900
  1012
#208 := (implies #192 #198)
boehmes@36900
  1013
#213 := (iff #208 #212)
boehmes@36900
  1014
#214 := [rewrite]: #213
boehmes@36900
  1015
#209 := (iff #58 #208)
boehmes@36900
  1016
#206 := (iff #57 #198)
boehmes@36900
  1017
#201 := (and #198 true)
boehmes@36900
  1018
#204 := (iff #201 #198)
boehmes@36900
  1019
#205 := [rewrite]: #204
boehmes@36900
  1020
#202 := (iff #57 #201)
boehmes@36900
  1021
#199 := (iff #56 #198)
boehmes@36900
  1022
#196 := (iff #55 #195)
boehmes@36900
  1023
#197 := [rewrite]: #196
boehmes@36900
  1024
#200 := [quant-intro #197]: #199
boehmes@36900
  1025
#203 := [monotonicity #200]: #202
boehmes@36900
  1026
#207 := [trans #203 #205]: #206
boehmes@36900
  1027
#193 := (iff #53 #192)
boehmes@36900
  1028
#190 := (iff #52 #189)
boehmes@36900
  1029
#191 := [rewrite]: #190
boehmes@36900
  1030
#194 := [quant-intro #191]: #193
boehmes@36900
  1031
#210 := [monotonicity #194 #207]: #209
boehmes@36900
  1032
#216 := [trans #210 #214]: #215
boehmes@36900
  1033
#219 := [monotonicity #194 #216]: #218
boehmes@36900
  1034
#186 := (iff #48 #185)
boehmes@36900
  1035
#187 := [rewrite]: #186
boehmes@36900
  1036
#222 := [monotonicity #187 #219]: #221
boehmes@36900
  1037
#228 := [trans #222 #226]: #227
boehmes@36900
  1038
#183 := (iff #46 #182)
boehmes@36900
  1039
#184 := [rewrite]: #183
boehmes@36900
  1040
#231 := [monotonicity #184 #228]: #230
boehmes@36900
  1041
#237 := [trans #231 #235]: #236
boehmes@36900
  1042
#180 := (iff #44 #179)
boehmes@36900
  1043
#181 := [rewrite]: #180
boehmes@36900
  1044
#240 := [monotonicity #181 #237]: #239
boehmes@36900
  1045
#246 := [trans #240 #244]: #245
boehmes@36900
  1046
#249 := [monotonicity #246]: #248
boehmes@36900
  1047
#255 := [trans #249 #253]: #254
boehmes@36900
  1048
#258 := [monotonicity #255]: #257
boehmes@36900
  1049
#264 := [trans #258 #262]: #263
boehmes@36900
  1050
#267 := [monotonicity #264]: #266
boehmes@36900
  1051
#272 := [trans #267 #270]: #271
boehmes@36900
  1052
#275 := [monotonicity #272]: #274
boehmes@36900
  1053
#279 := [trans #275 #277]: #278
boehmes@36900
  1054
#516 := [monotonicity #279 #513]: #515
boehmes@36900
  1055
#519 := [monotonicity #516]: #518
boehmes@36900
  1056
#524 := [trans #519 #522]: #523
boehmes@36900
  1057
#177 := (iff #41 #176)
boehmes@36900
  1058
#178 := [rewrite]: #177
boehmes@36900
  1059
#527 := [monotonicity #178 #524]: #526
boehmes@36900
  1060
#533 := [trans #527 #531]: #532
boehmes@36900
  1061
#174 := (iff #39 #173)
boehmes@36900
  1062
#171 := (iff #38 #170)
boehmes@36900
  1063
#172 := [rewrite]: #171
boehmes@36900
  1064
#175 := [quant-intro #172]: #174
boehmes@36900
  1065
#536 := [monotonicity #175 #533]: #535
boehmes@36900
  1066
#542 := [trans #536 #540]: #541
boehmes@36900
  1067
#545 := [monotonicity #542]: #544
boehmes@36900
  1068
#550 := [trans #545 #548]: #549
boehmes@36900
  1069
#553 := [monotonicity #550]: #552
boehmes@36900
  1070
#557 := [trans #553 #555]: #556
boehmes@36900
  1071
#167 := (iff #28 #13)
boehmes@36900
  1072
#168 := [rewrite]: #167
boehmes@36900
  1073
#560 := [monotonicity #168 #557]: #559
boehmes@36900
  1074
#566 := [trans #560 #564]: #565
boehmes@36900
  1075
#569 := [monotonicity #168 #566]: #568
boehmes@36900
  1076
#165 := (iff #27 #164)
boehmes@36900
  1077
#162 := (iff #26 #161)
boehmes@34994
  1078
#163 := [rewrite]: #162
boehmes@36900
  1079
#166 := [quant-intro #163]: #165
boehmes@36900
  1080
#572 := [monotonicity #166 #569]: #571
boehmes@36900
  1081
#578 := [trans #572 #576]: #577
boehmes@36900
  1082
#581 := [monotonicity #166 #578]: #580
boehmes@36900
  1083
#158 := (iff #19 #157)
boehmes@36900
  1084
#155 := (iff #18 #154)
boehmes@36900
  1085
#152 := (iff #17 #16)
boehmes@36900
  1086
#153 := [rewrite]: #152
boehmes@36900
  1087
#156 := [monotonicity #153]: #155
boehmes@36900
  1088
#159 := [monotonicity #156]: #158
boehmes@36900
  1089
#584 := [monotonicity #159 #581]: #583
boehmes@36900
  1090
#590 := [trans #584 #588]: #589
boehmes@36900
  1091
#593 := [monotonicity #590]: #592
boehmes@36900
  1092
#598 := [trans #593 #596]: #597
boehmes@36900
  1093
#601 := [monotonicity #598]: #600
boehmes@36900
  1094
#607 := [trans #601 #605]: #606
boehmes@36900
  1095
#610 := [monotonicity #607]: #609
boehmes@36900
  1096
#614 := [trans #610 #612]: #613
boehmes@36900
  1097
#617 := [monotonicity #614]: #616
boehmes@36900
  1098
#999 := [trans #617 #997]: #998
boehmes@36900
  1099
#151 := [asserted]: #134
boehmes@36900
  1100
#1000 := [mp #151 #999]: #995
boehmes@36900
  1101
#1001 := [not-or-elim #1000]: #13
boehmes@36900
  1102
#2045 := [trans #1001 #2054]: #2072
boehmes@36900
  1103
#1786 := (not #1007)
boehmes@36900
  1104
#1871 := (or #1432 #1786)
boehmes@36900
  1105
#1872 := [def-axiom]: #1871
boehmes@36900
  1106
#2051 := [unit-resolution #1872 #2073]: #1786
boehmes@36900
  1107
#2050 := (not #2072)
boehmes@36900
  1108
#2019 := (or #2050 #1007)
boehmes@36900
  1109
#2026 := [th-lemma]: #2019
boehmes@36900
  1110
#1985 := [unit-resolution #2026 #2051 #2045]: false
boehmes@36900
  1111
#2016 := [lemma #1985]: #1432
boehmes@36900
  1112
#2289 := (or #1437 #2286)
boehmes@36900
  1113
#1507 := (forall (vars (?v0 int)) #1504)
boehmes@36900
  1114
#1693 := (or #1507 #1690)
boehmes@36900
  1115
#1696 := (not #1693)
boehmes@36900
  1116
#1699 := (or #241 #232 #223 #1569 #815 #727 #1696)
boehmes@36900
  1117
#1702 := (not #1699)
boehmes@36900
  1118
#1596 := (forall (vars (?v0 int)) #1591)
boehmes@36900
  1119
#1602 := (not #1596)
boehmes@36900
  1120
#1603 := (or #307 #1602)
boehmes@36900
  1121
#1604 := (not #1603)
boehmes@36900
  1122
#1632 := (or #1604 #1629)
boehmes@36900
  1123
#1640 := (not #1632)
boehmes@36900
  1124
#1650 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #1640)
boehmes@36900
  1125
#1651 := (not #1650)
boehmes@36900
  1126
#1641 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #1640)
boehmes@36900
  1127
#1642 := (not #1641)
boehmes@36900
  1128
#1656 := (or #1642 #1651)
boehmes@36900
  1129
#1662 := (not #1656)
boehmes@36900
  1130
#1663 := (or #1569 #815 #724 #1662)
boehmes@36900
  1131
#1664 := (not #1663)
boehmes@36900
  1132
#1708 := (or #1664 #1702)
boehmes@36900
  1133
#1713 := (not #1708)
boehmes@36900
  1134
#1482 := (forall (vars (?v0 int)) #1477)
boehmes@36900
  1135
#1676 := (not #1482)
boehmes@36900
  1136
#1460 := (forall (vars (?v0 int)) #1455)
boehmes@36900
  1137
#1675 := (not #1460)
boehmes@36900
  1138
#1716 := (or #528 #1569 #815 #1675 #1676 #1713)
boehmes@36900
  1139
#1719 := (not #1716)
boehmes@36900
  1140
#1722 := (or #1437 #1719)
boehmes@36900
  1141
#2290 := (iff #1722 #2289)
boehmes@36900
  1142
#2287 := (iff #1719 #2286)
boehmes@36900
  1143
#2284 := (iff #1716 #2283)
boehmes@36900
  1144
#2281 := (iff #1713 #2280)
boehmes@36900
  1145
#2278 := (iff #1708 #2277)
boehmes@36900
  1146
#2275 := (iff #1702 #2274)
boehmes@36900
  1147
#2272 := (iff #1699 #2271)
boehmes@36900
  1148
#2269 := (iff #1696 #2268)
boehmes@36900
  1149
#2266 := (iff #1693 #2265)
boehmes@36900
  1150
#2263 := (iff #1507 #2260)
boehmes@36900
  1151
#2261 := (iff #1504 #1504)
boehmes@36900
  1152
#2262 := [refl]: #2261
boehmes@36900
  1153
#2264 := [quant-intro #2262]: #2263
boehmes@36900
  1154
#2267 := [monotonicity #2264]: #2266
boehmes@36900
  1155
#2270 := [monotonicity #2267]: #2269
boehmes@36900
  1156
#2273 := [monotonicity #2270]: #2272
boehmes@36900
  1157
#2276 := [monotonicity #2273]: #2275
boehmes@36900
  1158
#2258 := (iff #1664 #2257)
boehmes@36900
  1159
#2255 := (iff #1663 #2254)
boehmes@36900
  1160
#2252 := (iff #1662 #2251)
boehmes@36900
  1161
#2249 := (iff #1656 #2248)
boehmes@36900
  1162
#2246 := (iff #1651 #2245)
boehmes@36900
  1163
#2243 := (iff #1650 #2242)
boehmes@36900
  1164
#2234 := (iff #1640 #2233)
boehmes@36900
  1165
#2231 := (iff #1632 #2230)
boehmes@36900
  1166
#2228 := (iff #1604 #2227)
boehmes@36900
  1167
#2225 := (iff #1603 #2224)
boehmes@36900
  1168
#2222 := (iff #1602 #2221)
boehmes@36900
  1169
#2219 := (iff #1596 #2216)
boehmes@36900
  1170
#2217 := (iff #1591 #1591)
boehmes@36900
  1171
#2218 := [refl]: #2217
boehmes@36900
  1172
#2220 := [quant-intro #2218]: #2219
boehmes@36900
  1173
#2223 := [monotonicity #2220]: #2222
boehmes@36900
  1174
#2226 := [monotonicity #2223]: #2225
boehmes@36900
  1175
#2229 := [monotonicity #2226]: #2228
boehmes@36900
  1176
#2232 := [monotonicity #2229]: #2231
boehmes@36900
  1177
#2235 := [monotonicity #2232]: #2234
boehmes@36900
  1178
#2244 := [monotonicity #2235]: #2243
boehmes@36900
  1179
#2247 := [monotonicity #2244]: #2246
boehmes@36900
  1180
#2240 := (iff #1642 #2239)
boehmes@36900
  1181
#2237 := (iff #1641 #2236)
boehmes@36900
  1182
#2238 := [monotonicity #2235]: #2237
boehmes@36900
  1183
#2241 := [monotonicity #2238]: #2240
boehmes@36900
  1184
#2250 := [monotonicity #2241 #2247]: #2249
boehmes@36900
  1185
#2253 := [monotonicity #2250]: #2252
boehmes@36900
  1186
#2256 := [monotonicity #2253]: #2255
boehmes@36900
  1187
#2259 := [monotonicity #2256]: #2258
boehmes@36900
  1188
#2279 := [monotonicity #2259 #2276]: #2278
boehmes@36900
  1189
#2282 := [monotonicity #2279]: #2281
boehmes@36900
  1190
#2214 := (iff #1676 #2213)
boehmes@36900
  1191
#2211 := (iff #1482 #2208)
boehmes@36900
  1192
#2209 := (iff #1477 #1477)
boehmes@36900
  1193
#2210 := [refl]: #2209
boehmes@36900
  1194
#2212 := [quant-intro #2210]: #2211
boehmes@36900
  1195
#2215 := [monotonicity #2212]: #2214
boehmes@36900
  1196
#2206 := (iff #1675 #2205)
boehmes@36900
  1197
#2203 := (iff #1460 #2200)
boehmes@36900
  1198
#2201 := (iff #1455 #1455)
boehmes@36900
  1199
#2202 := [refl]: #2201
boehmes@36900
  1200
#2204 := [quant-intro #2202]: #2203
boehmes@36900
  1201
#2207 := [monotonicity #2204]: #2206
boehmes@36900
  1202
#2285 := [monotonicity #2207 #2215 #2282]: #2284
boehmes@36900
  1203
#2288 := [monotonicity #2285]: #2287
boehmes@36900
  1204
#2291 := [monotonicity #2288]: #2290
boehmes@36900
  1205
#1344 := (and #1160 #1341)
boehmes@36900
  1206
#1347 := (not #1344)
boehmes@36900
  1207
#1363 := (or #1347 #1358)
boehmes@36900
  1208
#1366 := (not #1363)
boehmes@36900
  1209
#1169 := (not #307)
boehmes@36900
  1210
#1179 := (and #1169 #785)
boehmes@36900
  1211
#1372 := (or #1179 #1366)
boehmes@36900
  1212
#1396 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1372)
boehmes@36900
  1213
#1384 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1372)
boehmes@36900
  1214
#1401 := (or #1384 #1396)
boehmes@36900
  1215
#1407 := (and #668 #671 #727 #1401)
boehmes@36900
  1216
#1111 := (not #1110)
boehmes@36900
  1217
#1279 := (and #1111 #1112)
boehmes@36900
  1218
#1282 := (not #1279)
boehmes@36900
  1219
#1298 := (or #1282 #1293)
boehmes@36900
  1220
#1301 := (not #1298)
boehmes@36900
  1221
#1090 := (not #1089)
boehmes@36900
  1222
#1270 := (and #1090 #1091)
boehmes@36900
  1223
#1273 := (not #1270)
boehmes@36900
  1224
#1276 := (or #1267 #1273)
boehmes@36900
  1225
#1304 := (and #1276 #1301)
boehmes@36900
  1226
#1080 := (not #694)
boehmes@36900
  1227
#1083 := (forall (vars (?v0 int)) #1080)
boehmes@36900
  1228
#1307 := (or #1083 #1304)
boehmes@36900
  1229
#1313 := (and #179 #182 #185 #668 #671 #724 #1307)
boehmes@36900
  1230
#1412 := (or #1313 #1407)
boehmes@36900
  1231
#1418 := (and #176 #661 #668 #671 #935 #1412)
boehmes@36900
  1232
#1240 := (and #1048 #1049)
boehmes@36900
  1233
#1243 := (not #1240)
boehmes@36900
  1234
#1249 := (or #1007 #1243)
boehmes@36900
  1235
#1254 := (not #1249)
boehmes@36900
  1236
#1423 := (or #1254 #1418)
boehmes@36900
  1237
#1725 := (iff #1423 #1722)
boehmes@36900
  1238
#1545 := (or #1110 #1530 #1293)
boehmes@36900
  1239
#1557 := (or #1556 #1545)
boehmes@36900
  1240
#1558 := (not #1557)
boehmes@36900
  1241
#1563 := (or #1507 #1558)
boehmes@36900
  1242
#1570 := (not #1563)
boehmes@36900
  1243
#1571 := (or #241 #232 #223 #1569 #815 #727 #1570)
boehmes@36900
  1244
#1572 := (not #1571)
boehmes@36900
  1245
#1669 := (or #1572 #1664)
boehmes@36900
  1246
#1677 := (not #1669)
boehmes@36900
  1247
#1678 := (or #528 #1569 #815 #1675 #1676 #1677)
boehmes@36900
  1248
#1679 := (not #1678)
boehmes@36900
  1249
#1684 := (or #1437 #1679)
boehmes@36900
  1250
#1723 := (iff #1684 #1722)
boehmes@36900
  1251
#1720 := (iff #1679 #1719)
boehmes@36900
  1252
#1717 := (iff #1678 #1716)
boehmes@36900
  1253
#1714 := (iff #1677 #1713)
boehmes@36900
  1254
#1711 := (iff #1669 #1708)
boehmes@36900
  1255
#1705 := (or #1702 #1664)
boehmes@36900
  1256
#1709 := (iff #1705 #1708)
boehmes@36900
  1257
#1710 := [rewrite]: #1709
boehmes@36900
  1258
#1706 := (iff #1669 #1705)
boehmes@36900
  1259
#1703 := (iff #1572 #1702)
boehmes@36900
  1260
#1700 := (iff #1571 #1699)
boehmes@36900
  1261
#1697 := (iff #1570 #1696)
boehmes@36900
  1262
#1694 := (iff #1563 #1693)
boehmes@36900
  1263
#1691 := (iff #1558 #1690)
boehmes@36900
  1264
#1688 := (iff #1557 #1687)
boehmes@36900
  1265
#1689 := [rewrite]: #1688
boehmes@36900
  1266
#1692 := [monotonicity #1689]: #1691
boehmes@36900
  1267
#1695 := [monotonicity #1692]: #1694
boehmes@36900
  1268
#1698 := [monotonicity #1695]: #1697
boehmes@36900
  1269
#1701 := [monotonicity #1698]: #1700
boehmes@36900
  1270
#1704 := [monotonicity #1701]: #1703
boehmes@36900
  1271
#1707 := [monotonicity #1704]: #1706
boehmes@36900
  1272
#1712 := [trans #1707 #1710]: #1711
boehmes@36900
  1273
#1715 := [monotonicity #1712]: #1714
boehmes@36900
  1274
#1718 := [monotonicity #1715]: #1717
boehmes@36900
  1275
#1721 := [monotonicity #1718]: #1720
boehmes@36900
  1276
#1724 := [monotonicity #1721]: #1723
boehmes@36900
  1277
#1685 := (iff #1423 #1684)
boehmes@36900
  1278
#1682 := (iff #1418 #1679)
boehmes@36900
  1279
#1672 := (and #176 #1460 #668 #671 #1482 #1669)
boehmes@36900
  1280
#1680 := (iff #1672 #1679)
boehmes@36900
  1281
#1681 := [rewrite]: #1680
boehmes@36900
  1282
#1673 := (iff #1418 #1672)
boehmes@36900
  1283
#1670 := (iff #1412 #1669)
boehmes@36900
  1284
#1667 := (iff #1407 #1664)
boehmes@36900
  1285
#1659 := (and #668 #671 #727 #1656)
boehmes@36900
  1286
#1665 := (iff #1659 #1664)
boehmes@36900
  1287
#1666 := [rewrite]: #1665
boehmes@36900
  1288
#1660 := (iff #1407 #1659)
boehmes@36900
  1289
#1657 := (iff #1401 #1656)
boehmes@36900
  1290
#1654 := (iff #1396 #1651)
boehmes@36900
  1291
#1647 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1632)
boehmes@36900
  1292
#1652 := (iff #1647 #1651)
boehmes@36900
  1293
#1653 := [rewrite]: #1652
boehmes@36900
  1294
#1648 := (iff #1396 #1647)
boehmes@36900
  1295
#1633 := (iff #1372 #1632)
boehmes@36900
  1296
#1630 := (iff #1366 #1629)
boehmes@36900
  1297
#1627 := (iff #1363 #1624)
boehmes@36900
  1298
#1610 := (or #1609 #1336)
boehmes@36900
  1299
#1621 := (or #1610 #1358)
boehmes@36900
  1300
#1625 := (iff #1621 #1624)
boehmes@36900
  1301
#1626 := [rewrite]: #1625
boehmes@36900
  1302
#1622 := (iff #1363 #1621)
boehmes@36900
  1303
#1619 := (iff #1347 #1610)
boehmes@36900
  1304
#1611 := (not #1610)
boehmes@36900
  1305
#1614 := (not #1611)
boehmes@36900
  1306
#1617 := (iff #1614 #1610)
boehmes@36900
  1307
#1618 := [rewrite]: #1617
boehmes@36900
  1308
#1615 := (iff #1347 #1614)
boehmes@36900
  1309
#1612 := (iff #1344 #1611)
boehmes@34994
  1310
#1613 := [rewrite]: #1612
boehmes@36900
  1311
#1616 := [monotonicity #1613]: #1615
boehmes@36900
  1312
#1620 := [trans #1616 #1618]: #1619
boehmes@36900
  1313
#1623 := [monotonicity #1620]: #1622
boehmes@36900
  1314
#1628 := [trans #1623 #1626]: #1627
boehmes@36900
  1315
#1631 := [monotonicity #1628]: #1630
boehmes@36900
  1316
#1607 := (iff #1179 #1604)
boehmes@36900
  1317
#1599 := (and #1169 #1596)
boehmes@36900
  1318
#1605 := (iff #1599 #1604)
boehmes@36900
  1319
#1606 := [rewrite]: #1605
boehmes@36900
  1320
#1600 := (iff #1179 #1599)
boehmes@36900
  1321
#1597 := (iff #785 #1596)
boehmes@36900
  1322
#1594 := (iff #782 #1591)
boehmes@36900
  1323
#1577 := (or #1440 #765)
boehmes@36900
  1324
#1588 := (or #1577 #779)
boehmes@36900
  1325
#1592 := (iff #1588 #1591)
boehmes@36900
  1326
#1593 := [rewrite]: #1592
boehmes@36900
  1327
#1589 := (iff #782 #1588)
boehmes@36900
  1328
#1586 := (iff #774 #1577)
boehmes@36900
  1329
#1578 := (not #1577)
boehmes@36900
  1330
#1581 := (not #1578)
boehmes@36900
  1331
#1584 := (iff #1581 #1577)
boehmes@36900
  1332
#1585 := [rewrite]: #1584
boehmes@36900
  1333
#1582 := (iff #774 #1581)
boehmes@36900
  1334
#1579 := (iff #771 #1578)
boehmes@34994
  1335
#1580 := [rewrite]: #1579
boehmes@36900
  1336
#1583 := [monotonicity #1580]: #1582
boehmes@36900
  1337
#1587 := [trans #1583 #1585]: #1586
boehmes@36900
  1338
#1590 := [monotonicity #1587]: #1589
boehmes@36900
  1339
#1595 := [trans #1590 #1593]: #1594
boehmes@36900
  1340
#1598 := [quant-intro #1595]: #1597
boehmes@36900
  1341
#1601 := [monotonicity #1598]: #1600
boehmes@36900
  1342
#1608 := [trans #1601 #1606]: #1607
boehmes@36900
  1343
#1634 := [monotonicity #1608 #1631]: #1633
boehmes@36900
  1344
#1649 := [monotonicity #1634]: #1648
boehmes@36900
  1345
#1655 := [trans #1649 #1653]: #1654
boehmes@36900
  1346
#1645 := (iff #1384 #1642)
boehmes@36900
  1347
#1635 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1632)
boehmes@36900
  1348
#1643 := (iff #1635 #1642)
boehmes@36900
  1349
#1644 := [rewrite]: #1643
boehmes@36900
  1350
#1636 := (iff #1384 #1635)
boehmes@36900
  1351
#1637 := [monotonicity #1634]: #1636
boehmes@36900
  1352
#1646 := [trans #1637 #1644]: #1645
boehmes@36900
  1353
#1658 := [monotonicity #1646 #1655]: #1657
boehmes@36900
  1354
#1661 := [monotonicity #1658]: #1660
boehmes@36900
  1355
#1668 := [trans #1661 #1666]: #1667
boehmes@36900
  1356
#1575 := (iff #1313 #1572)
boehmes@36900
  1357
#1566 := (and #179 #182 #185 #668 #671 #724 #1563)
boehmes@36900
  1358
#1573 := (iff #1566 #1572)
boehmes@36900
  1359
#1574 := [rewrite]: #1573
boehmes@36900
  1360
#1567 := (iff #1313 #1566)
boehmes@36900
  1361
#1564 := (iff #1307 #1563)
boehmes@36900
  1362
#1561 := (iff #1304 #1558)
boehmes@36900
  1363
#1550 := (not #1545)
boehmes@36900
  1364
#1553 := (and #1525 #1550)
boehmes@36900
  1365
#1559 := (iff #1553 #1558)
boehmes@36900
  1366
#1560 := [rewrite]: #1559
boehmes@36900
  1367
#1554 := (iff #1304 #1553)
boehmes@36900
  1368
#1551 := (iff #1301 #1550)
boehmes@36900
  1369
#1548 := (iff #1298 #1545)
boehmes@36900
  1370
#1531 := (or #1110 #1530)
boehmes@36900
  1371
#1542 := (or #1531 #1293)
boehmes@36900
  1372
#1546 := (iff #1542 #1545)
boehmes@36900
  1373
#1547 := [rewrite]: #1546
boehmes@36900
  1374
#1543 := (iff #1298 #1542)
boehmes@36900
  1375
#1540 := (iff #1282 #1531)
boehmes@36900
  1376
#1532 := (not #1531)
boehmes@36900
  1377
#1535 := (not #1532)
boehmes@36900
  1378
#1538 := (iff #1535 #1531)
boehmes@36900
  1379
#1539 := [rewrite]: #1538
boehmes@36900
  1380
#1536 := (iff #1282 #1535)
boehmes@36900
  1381
#1533 := (iff #1279 #1532)
boehmes@34994
  1382
#1534 := [rewrite]: #1533
boehmes@36900
  1383
#1537 := [monotonicity #1534]: #1536
boehmes@36900
  1384
#1541 := [trans #1537 #1539]: #1540
boehmes@36900
  1385
#1544 := [monotonicity #1541]: #1543
boehmes@36900
  1386
#1549 := [trans #1544 #1547]: #1548
boehmes@36900
  1387
#1552 := [monotonicity #1549]: #1551
boehmes@36900
  1388
#1528 := (iff #1276 #1525)
boehmes@36900
  1389
#1511 := (or #1089 #1510)
boehmes@36900
  1390
#1522 := (or #1267 #1511)
boehmes@36900
  1391
#1526 := (iff #1522 #1525)
boehmes@36900
  1392
#1527 := [rewrite]: #1526
boehmes@36900
  1393
#1523 := (iff #1276 #1522)
boehmes@36900
  1394
#1520 := (iff #1273 #1511)
boehmes@36900
  1395
#1512 := (not #1511)
boehmes@36900
  1396
#1515 := (not #1512)
boehmes@36900
  1397
#1518 := (iff #1515 #1511)
boehmes@36900
  1398
#1519 := [rewrite]: #1518
boehmes@36900
  1399
#1516 := (iff #1273 #1515)
boehmes@36900
  1400
#1513 := (iff #1270 #1512)
boehmes@34994
  1401
#1514 := [rewrite]: #1513
boehmes@36900
  1402
#1517 := [monotonicity #1514]: #1516
boehmes@36900
  1403
#1521 := [trans #1517 #1519]: #1520
boehmes@36900
  1404
#1524 := [monotonicity #1521]: #1523
boehmes@36900
  1405
#1529 := [trans #1524 #1527]: #1528
boehmes@36900
  1406
#1555 := [monotonicity #1529 #1552]: #1554
boehmes@36900
  1407
#1562 := [trans #1555 #1560]: #1561
boehmes@36900
  1408
#1508 := (iff #1083 #1507)
boehmes@36900
  1409
#1505 := (iff #1080 #1504)
boehmes@36900
  1410
#1502 := (iff #694 #1499)
boehmes@36900
  1411
#1485 := (or #1440 #681)
boehmes@36900
  1412
#1496 := (or #51 #1485)
boehmes@36900
  1413
#1500 := (iff #1496 #1499)
boehmes@36900
  1414
#1501 := [rewrite]: #1500
boehmes@36900
  1415
#1497 := (iff #694 #1496)
boehmes@36900
  1416
#1494 := (iff #688 #1485)
boehmes@36900
  1417
#1486 := (not #1485)
boehmes@36900
  1418
#1489 := (not #1486)
boehmes@36900
  1419
#1492 := (iff #1489 #1485)
boehmes@36900
  1420
#1493 := [rewrite]: #1492
boehmes@36900
  1421
#1490 := (iff #688 #1489)
boehmes@36900
  1422
#1487 := (iff #685 #1486)
boehmes@34994
  1423
#1488 := [rewrite]: #1487
boehmes@36900
  1424
#1491 := [monotonicity #1488]: #1490
boehmes@36900
  1425
#1495 := [trans #1491 #1493]: #1494
boehmes@36900
  1426
#1498 := [monotonicity #1495]: #1497
boehmes@36900
  1427
#1503 := [trans #1498 #1501]: #1502
boehmes@36900
  1428
#1506 := [monotonicity #1503]: #1505
boehmes@36900
  1429
#1509 := [quant-intro #1506]: #1508
boehmes@36900
  1430
#1565 := [monotonicity #1509 #1562]: #1564
boehmes@36900
  1431
#1568 := [monotonicity #1565]: #1567
boehmes@36900
  1432
#1576 := [trans #1568 #1574]: #1575
boehmes@36900
  1433
#1671 := [monotonicity #1576 #1668]: #1670
boehmes@36900
  1434
#1483 := (iff #935 #1482)
boehmes@36900
  1435
#1480 := (iff #932 #1477)
boehmes@36900
  1436
#1463 := (or #1440 #916)
boehmes@36900
  1437
#1474 := (or #1463 #929)
boehmes@36900
  1438
#1478 := (iff #1474 #1477)
boehmes@36900
  1439
#1479 := [rewrite]: #1478
boehmes@36900
  1440
#1475 := (iff #932 #1474)
boehmes@36900
  1441
#1472 := (iff #924 #1463)
boehmes@36900
  1442
#1464 := (not #1463)
boehmes@36900
  1443
#1467 := (not #1464)
boehmes@36900
  1444
#1470 := (iff #1467 #1463)
boehmes@36900
  1445
#1471 := [rewrite]: #1470
boehmes@36900
  1446
#1468 := (iff #924 #1467)
boehmes@36900
  1447
#1465 := (iff #921 #1464)
boehmes@34994
  1448
#1466 := [rewrite]: #1465
boehmes@36900
  1449
#1469 := [monotonicity #1466]: #1468
boehmes@36900
  1450
#1473 := [trans #1469 #1471]: #1472
boehmes@36900
  1451
#1476 := [monotonicity #1473]: #1475
boehmes@36900
  1452
#1481 := [trans #1476 #1479]: #1480
boehmes@36900
  1453
#1484 := [quant-intro #1481]: #1483
boehmes@36900
  1454
#1461 := (iff #661 #1460)
boehmes@36900
  1455
#1458 := (iff #658 #1455)
boehmes@36900
  1456
#1441 := (or #1440 #644)
boehmes@36900
  1457
#1452 := (or #1441 #654)
boehmes@36900
  1458
#1456 := (iff #1452 #1455)
boehmes@36900
  1459
#1457 := [rewrite]: #1456
boehmes@36900
  1460
#1453 := (iff #658 #1452)
boehmes@36900
  1461
#1450 := (iff #649 #1441)
boehmes@36900
  1462
#1442 := (not #1441)
boehmes@36900
  1463
#1445 := (not #1442)
boehmes@36900
  1464
#1448 := (iff #1445 #1441)
boehmes@36900
  1465
#1449 := [rewrite]: #1448
boehmes@36900
  1466
#1446 := (iff #649 #1445)
boehmes@36900
  1467
#1443 := (iff #646 #1442)
boehmes@34994
  1468
#1444 := [rewrite]: #1443
boehmes@36900
  1469
#1447 := [monotonicity #1444]: #1446
boehmes@36900
  1470
#1451 := [trans #1447 #1449]: #1450
boehmes@36900
  1471
#1454 := [monotonicity #1451]: #1453
boehmes@36900
  1472
#1459 := [trans #1454 #1457]: #1458
boehmes@36900
  1473
#1462 := [quant-intro #1459]: #1461
boehmes@36900
  1474
#1674 := [monotonicity #1462 #1484 #1671]: #1673
boehmes@36900
  1475
#1683 := [trans #1674 #1681]: #1682
boehmes@36900
  1476
#1438 := (iff #1254 #1437)
boehmes@36900
  1477
#1435 := (iff #1249 #1432)
boehmes@36900
  1478
#1168 := (or #1005 #1167)
boehmes@36900
  1479
#1429 := (or #1007 #1168)
boehmes@36900
  1480
#1433 := (iff #1429 #1432)
boehmes@36900
  1481
#1434 := [rewrite]: #1433
boehmes@36900
  1482
#1430 := (iff #1249 #1429)
boehmes@36900
  1483
#1427 := (iff #1243 #1168)
boehmes@36900
  1484
#1099 := (not #1168)
boehmes@36900
  1485
#1057 := (not #1099)
boehmes@36900
  1486
#1239 := (iff #1057 #1168)
boehmes@36900
  1487
#1426 := [rewrite]: #1239
boehmes@36900
  1488
#1120 := (iff #1243 #1057)
boehmes@36900
  1489
#1100 := (iff #1240 #1099)
boehmes@36900
  1490
#1056 := [rewrite]: #1100
boehmes@36900
  1491
#1121 := [monotonicity #1056]: #1120
boehmes@36900
  1492
#1428 := [trans #1121 #1426]: #1427
boehmes@36900
  1493
#1431 := [monotonicity #1428]: #1430
boehmes@36900
  1494
#1436 := [trans #1431 #1434]: #1435
boehmes@36900
  1495
#1439 := [monotonicity #1436]: #1438
boehmes@36900
  1496
#1686 := [monotonicity #1439 #1683]: #1685
boehmes@36900
  1497
#1726 := [trans #1686 #1724]: #1725
boehmes@36900
  1498
#1190 := (not #812)
boehmes@36900
  1499
#1187 := (not #806)
boehmes@36900
  1500
#1155 := (+ #1154 #777)
boehmes@36900
  1501
#1156 := (<= #1155 0::int)
boehmes@36900
  1502
#1157 := (+ ?v0!3 #766)
boehmes@36900
  1503
#1158 := (>= #1157 0::int)
boehmes@34994
  1504
#1159 := (not #1158)
boehmes@36900
  1505
#1161 := (and #1160 #1159)
boehmes@36900
  1506
#1162 := (not #1161)
boehmes@36900
  1507
#1163 := (or #1162 #1156)
boehmes@36900
  1508
#1164 := (not #1163)
boehmes@36900
  1509
#1183 := (or #1164 #1179)
boehmes@36900
  1510
#1150 := (not #762)
boehmes@36900
  1511
#1068 := (not #676)
boehmes@36900
  1512
#1202 := (not #432)
boehmes@36900
  1513
#1199 := (not #441)
boehmes@36900
  1514
#1207 := (and #1199 #1202 #1068 #1150 #1183 #1187 #1190 #824)
boehmes@36900
  1515
#1147 := (not #815)
boehmes@36900
  1516
#1144 := (not #366)
boehmes@36900
  1517
#1141 := (not #375)
boehmes@36900
  1518
#1138 := (not #393)
boehmes@36900
  1519
#1195 := (and #1138 #1141 #1144 #1147 #1068 #1150 #1183 #1187 #1190 #818)
boehmes@36900
  1520
#1211 := (or #1195 #1207)
boehmes@36900
  1521
#1215 := (and #1068 #727 #1211)
boehmes@36900
  1522
#1106 := (+ #1105 #705)
boehmes@36900
  1523
#1107 := (<= #1106 0::int)
boehmes@36900
  1524
#1113 := (and #1112 #1111)
boehmes@36900
  1525
#1114 := (not #1113)
boehmes@36900
  1526
#1115 := (or #1114 #1107)
boehmes@36900
  1527
#1116 := (not #1115)
boehmes@36900
  1528
#1092 := (and #1091 #1090)
boehmes@36900
  1529
#1093 := (not #1092)
boehmes@36900
  1530
#1095 := (= #1094 f10)
boehmes@36900
  1531
#1096 := (or #1095 #1093)
boehmes@36900
  1532
#1122 := (and #1096 #1116)
boehmes@36900
  1533
#1126 := (or #1083 #1122)
boehmes@36900
  1534
#1077 := (not #223)
boehmes@36900
  1535
#1074 := (not #232)
boehmes@36900
  1536
#1071 := (not #241)
boehmes@36900
  1537
#1132 := (and #1071 #1074 #1077 #1068 #1126 #892)
boehmes@36900
  1538
#1219 := (or #1132 #1215)
boehmes@36900
  1539
#1058 := (not #528)
boehmes@36900
  1540
#1230 := (and #1058 #661 #1068 #1219 #935)
boehmes@36900
  1541
#1050 := (and #1049 #1048)
boehmes@36900
  1542
#1051 := (not #1050)
boehmes@36900
  1543
#1052 := (or #1051 #1007)
boehmes@36900
  1544
#1053 := (not #1052)
boehmes@36900
  1545
#1234 := (or #1053 #1230)
boehmes@36900
  1546
#1424 := (iff #1234 #1423)
boehmes@36900
  1547
#1421 := (iff #1230 #1418)
boehmes@36900
  1548
#1415 := (and #176 #661 #673 #1412 #935)
boehmes@36900
  1549
#1419 := (iff #1415 #1418)
boehmes@36900
  1550
#1420 := [rewrite]: #1419
boehmes@36900
  1551
#1416 := (iff #1230 #1415)
boehmes@36900
  1552
#1413 := (iff #1219 #1412)
boehmes@36900
  1553
#1410 := (iff #1215 #1407)
boehmes@36900
  1554
#1404 := (and #673 #727 #1401)
boehmes@36900
  1555
#1408 := (iff #1404 #1407)
boehmes@36900
  1556
#1409 := [rewrite]: #1408
boehmes@36900
  1557
#1405 := (iff #1215 #1404)
boehmes@36900
  1558
#1402 := (iff #1211 #1401)
boehmes@36900
  1559
#1399 := (iff #1207 #1396)
boehmes@36900
  1560
#1393 := (and #423 #426 #673 #759 #1372 #802 #809 #819)
boehmes@36900
  1561
#1397 := (iff #1393 #1396)
boehmes@36900
  1562
#1398 := [rewrite]: #1397
boehmes@36900
  1563
#1394 := (iff #1207 #1393)
boehmes@36900
  1564
#1379 := (iff #1190 #809)
boehmes@36900
  1565
#1380 := [rewrite]: #1379
boehmes@36900
  1566
#1377 := (iff #1187 #802)
boehmes@36900
  1567
#1378 := [rewrite]: #1377
boehmes@36900
  1568
#1375 := (iff #1183 #1372)
boehmes@36900
  1569
#1369 := (or #1366 #1179)
boehmes@36900
  1570
#1373 := (iff #1369 #1372)
boehmes@36900
  1571
#1374 := [rewrite]: #1373
boehmes@36900
  1572
#1370 := (iff #1183 #1369)
boehmes@36900
  1573
#1367 := (iff #1164 #1366)
boehmes@36900
  1574
#1364 := (iff #1163 #1363)
boehmes@36900
  1575
#1361 := (iff #1156 #1358)
boehmes@36900
  1576
#1350 := (+ #777 #1154)
boehmes@36900
  1577
#1353 := (<= #1350 0::int)
boehmes@36900
  1578
#1359 := (iff #1353 #1358)
boehmes@36900
  1579
#1360 := [rewrite]: #1359
boehmes@36900
  1580
#1354 := (iff #1156 #1353)
boehmes@36900
  1581
#1351 := (= #1155 #1350)
boehmes@36900
  1582
#1352 := [rewrite]: #1351
boehmes@36900
  1583
#1355 := [monotonicity #1352]: #1354
boehmes@36900
  1584
#1362 := [trans #1355 #1360]: #1361
boehmes@36900
  1585
#1348 := (iff #1162 #1347)
boehmes@36900
  1586
#1345 := (iff #1161 #1344)
boehmes@36900
  1587
#1342 := (iff #1159 #1341)
boehmes@36900
  1588
#1339 := (iff #1158 #1336)
boehmes@36900
  1589
#1328 := (+ #766 ?v0!3)
boehmes@36900
  1590
#1331 := (>= #1328 0::int)
boehmes@36900
  1591
#1337 := (iff #1331 #1336)
boehmes@36900
  1592
#1338 := [rewrite]: #1337
boehmes@36900
  1593
#1332 := (iff #1158 #1331)
boehmes@36900
  1594
#1329 := (= #1157 #1328)
boehmes@36900
  1595
#1330 := [rewrite]: #1329
boehmes@36900
  1596
#1333 := [monotonicity #1330]: #1332
boehmes@36900
  1597
#1340 := [trans #1333 #1338]: #1339
boehmes@36900
  1598
#1343 := [monotonicity #1340]: #1342
boehmes@36900
  1599
#1346 := [monotonicity #1343]: #1345
boehmes@36900
  1600
#1349 := [monotonicity #1346]: #1348
boehmes@36900
  1601
#1365 := [monotonicity #1349 #1362]: #1364
boehmes@36900
  1602
#1368 := [monotonicity #1365]: #1367
boehmes@36900
  1603
#1371 := [monotonicity #1368]: #1370
boehmes@36900
  1604
#1376 := [trans #1371 #1374]: #1375
boehmes@36900
  1605
#1326 := (iff #1150 #759)
boehmes@36900
  1606
#1327 := [rewrite]: #1326
boehmes@36900
  1607
#1259 := (iff #1068 #673)
boehmes@36900
  1608
#1260 := [rewrite]: #1259
boehmes@36900
  1609
#1391 := (iff #1202 #426)
boehmes@36900
  1610
#1392 := [rewrite]: #1391
boehmes@36900
  1611
#1389 := (iff #1199 #423)
boehmes@36900
  1612
#1390 := [rewrite]: #1389
boehmes@36900
  1613
#1395 := [monotonicity #1390 #1392 #1260 #1327 #1376 #1378 #1380 #828]: #1394
boehmes@36900
  1614
#1400 := [trans #1395 #1398]: #1399
boehmes@36900
  1615
#1387 := (iff #1195 #1384)
boehmes@36900
  1616
#1381 := (and #280 #285 #288 #671 #673 #759 #1372 #802 #809 #818)
boehmes@36900
  1617
#1385 := (iff #1381 #1384)
boehmes@36900
  1618
#1386 := [rewrite]: #1385
boehmes@36900
  1619
#1382 := (iff #1195 #1381)
boehmes@36900
  1620
#1324 := (iff #1147 #671)
boehmes@34994
  1621
#1325 := [rewrite]: #1324
boehmes@36900
  1622
#1322 := (iff #1144 #288)
boehmes@36900
  1623
#1323 := [rewrite]: #1322
boehmes@36900
  1624
#1320 := (iff #1141 #285)
boehmes@36900
  1625
#1321 := [rewrite]: #1320
boehmes@36900
  1626
#1318 := (iff #1138 #280)
boehmes@36900
  1627
#1319 := [rewrite]: #1318
boehmes@36900
  1628
#1383 := [monotonicity #1319 #1321 #1323 #1325 #1260 #1327 #1376 #1378 #1380]: #1382
boehmes@36900
  1629
#1388 := [trans #1383 #1386]: #1387
boehmes@36900
  1630
#1403 := [monotonicity #1388 #1400]: #1402
boehmes@36900
  1631
#1406 := [monotonicity #1260 #1403]: #1405
boehmes@36900
  1632
#1411 := [trans #1406 #1409]: #1410
boehmes@36900
  1633
#1316 := (iff #1132 #1313)
boehmes@36900
  1634
#1310 := (and #179 #182 #185 #673 #1307 #724)
boehmes@36900
  1635
#1314 := (iff #1310 #1313)
boehmes@36900
  1636
#1315 := [rewrite]: #1314
boehmes@36900
  1637
#1311 := (iff #1132 #1310)
boehmes@36900
  1638
#1308 := (iff #1126 #1307)
boehmes@36900
  1639
#1305 := (iff #1122 #1304)
boehmes@36900
  1640
#1302 := (iff #1116 #1301)
boehmes@36900
  1641
#1299 := (iff #1115 #1298)
boehmes@36900
  1642
#1296 := (iff #1107 #1293)
boehmes@36900
  1643
#1285 := (+ #705 #1105)
boehmes@36900
  1644
#1288 := (<= #1285 0::int)
boehmes@36900
  1645
#1294 := (iff #1288 #1293)
boehmes@36900
  1646
#1295 := [rewrite]: #1294
boehmes@36900
  1647
#1289 := (iff #1107 #1288)
boehmes@36900
  1648
#1286 := (= #1106 #1285)
boehmes@36900
  1649
#1287 := [rewrite]: #1286
boehmes@36900
  1650
#1290 := [monotonicity #1287]: #1289
boehmes@36900
  1651
#1297 := [trans #1290 #1295]: #1296
boehmes@36900
  1652
#1283 := (iff #1114 #1282)
boehmes@36900
  1653
#1280 := (iff #1113 #1279)
boehmes@36900
  1654
#1281 := [rewrite]: #1280
boehmes@36900
  1655
#1284 := [monotonicity #1281]: #1283
boehmes@36900
  1656
#1300 := [monotonicity #1284 #1297]: #1299
boehmes@36900
  1657
#1303 := [monotonicity #1300]: #1302
boehmes@36900
  1658
#1277 := (iff #1096 #1276)
boehmes@36900
  1659
#1274 := (iff #1093 #1273)
boehmes@36900
  1660
#1271 := (iff #1092 #1270)
boehmes@36900
  1661
#1272 := [rewrite]: #1271
boehmes@36900
  1662
#1275 := [monotonicity #1272]: #1274
boehmes@36900
  1663
#1268 := (iff #1095 #1267)
boehmes@36900
  1664
#1269 := [rewrite]: #1268
boehmes@36900
  1665
#1278 := [monotonicity #1269 #1275]: #1277
boehmes@36900
  1666
#1306 := [monotonicity #1278 #1303]: #1305
boehmes@36900
  1667
#1309 := [monotonicity #1306]: #1308
boehmes@36900
  1668
#1265 := (iff #1077 #185)
boehmes@36900
  1669
#1266 := [rewrite]: #1265
boehmes@36900
  1670
#1263 := (iff #1074 #182)
boehmes@34994
  1671
#1264 := [rewrite]: #1263
boehmes@36900
  1672
#1261 := (iff #1071 #179)
boehmes@36900
  1673
#1262 := [rewrite]: #1261
boehmes@36900
  1674
#1312 := [monotonicity #1262 #1264 #1266 #1260 #1309 #896]: #1311
boehmes@36900
  1675
#1317 := [trans #1312 #1315]: #1316
boehmes@36900
  1676
#1414 := [monotonicity #1317 #1411]: #1413
boehmes@36900
  1677
#1257 := (iff #1058 #176)
boehmes@36900
  1678
#1258 := [rewrite]: #1257
boehmes@36900
  1679
#1417 := [monotonicity #1258 #1260 #1414]: #1416
boehmes@36900
  1680
#1422 := [trans #1417 #1420]: #1421
boehmes@36900
  1681
#1255 := (iff #1053 #1254)
boehmes@36900
  1682
#1252 := (iff #1052 #1249)
boehmes@36900
  1683
#1246 := (or #1243 #1007)
boehmes@36900
  1684
#1250 := (iff #1246 #1249)
boehmes@36900
  1685
#1251 := [rewrite]: #1250
boehmes@36900
  1686
#1247 := (iff #1052 #1246)
boehmes@36900
  1687
#1244 := (iff #1051 #1243)
boehmes@36900
  1688
#1241 := (iff #1050 #1240)
boehmes@36900
  1689
#1242 := [rewrite]: #1241
boehmes@36900
  1690
#1245 := [monotonicity #1242]: #1244
boehmes@36900
  1691
#1248 := [monotonicity #1245]: #1247
boehmes@36900
  1692
#1253 := [trans #1248 #1251]: #1252
boehmes@36900
  1693
#1256 := [monotonicity #1253]: #1255
boehmes@36900
  1694
#1425 := [monotonicity #1256 #1422]: #1424
boehmes@36900
  1695
#1032 := (or #528 #664 #676 #913 #938)
boehmes@36900
  1696
#1037 := (and #661 #1032)
boehmes@36900
  1697
#1040 := (not #1037)
boehmes@36900
  1698
#1235 := (~ #1040 #1234)
boehmes@36900
  1699
#1231 := (not #1032)
boehmes@36900
  1700
#1232 := (~ #1231 #1230)
boehmes@36900
  1701
#1227 := (not #938)
boehmes@36900
  1702
#1228 := (~ #1227 #935)
boehmes@36900
  1703
#1225 := (~ #935 #935)
boehmes@36900
  1704
#1223 := (~ #932 #932)
boehmes@36900
  1705
#1224 := [refl]: #1223
boehmes@36900
  1706
#1226 := [nnf-pos #1224]: #1225
boehmes@36900
  1707
#1229 := [nnf-neg #1226]: #1228
boehmes@36900
  1708
#1220 := (not #913)
boehmes@36900
  1709
#1221 := (~ #1220 #1219)
boehmes@36900
  1710
#1216 := (not #908)
boehmes@36900
  1711
#1217 := (~ #1216 #1215)
boehmes@36900
  1712
#1212 := (not #887)
boehmes@36900
  1713
#1213 := (~ #1212 #1211)
boehmes@36900
  1714
#1208 := (not #882)
boehmes@36900
  1715
#1209 := (~ #1208 #1207)
boehmes@36900
  1716
#1205 := (~ #824 #824)
boehmes@36900
  1717
#1206 := [refl]: #1205
boehmes@36900
  1718
#1191 := (~ #1190 #1190)
boehmes@36900
  1719
#1192 := [refl]: #1191
boehmes@36900
  1720
#1188 := (~ #1187 #1187)
boehmes@34994
  1721
#1189 := [refl]: #1188
boehmes@36900
  1722
#1184 := (not #799)
boehmes@36900
  1723
#1185 := (~ #1184 #1183)
boehmes@36900
  1724
#1180 := (not #794)
boehmes@36900
  1725
#1181 := (~ #1180 #1179)
boehmes@36900
  1726
#1176 := (not #788)
boehmes@36900
  1727
#1177 := (~ #1176 #785)
boehmes@36900
  1728
#1174 := (~ #785 #785)
boehmes@36900
  1729
#1172 := (~ #782 #782)
boehmes@36900
  1730
#1173 := [refl]: #1172
boehmes@36900
  1731
#1175 := [nnf-pos #1173]: #1174
boehmes@36900
  1732
#1178 := [nnf-neg #1175]: #1177
boehmes@36900
  1733
#1170 := (~ #1169 #1169)
boehmes@36900
  1734
#1171 := [refl]: #1170
boehmes@36900
  1735
#1182 := [nnf-neg #1171 #1178]: #1181
boehmes@36900
  1736
#1165 := (~ #788 #1164)
boehmes@36900
  1737
#1166 := [sk]: #1165
boehmes@36900
  1738
#1186 := [nnf-neg #1166 #1182]: #1185
boehmes@36900
  1739
#1151 := (~ #1150 #1150)
boehmes@36900
  1740
#1152 := [refl]: #1151
boehmes@36900
  1741
#1069 := (~ #1068 #1068)
boehmes@36900
  1742
#1070 := [refl]: #1069
boehmes@36900
  1743
#1203 := (~ #1202 #1202)
boehmes@36900
  1744
#1204 := [refl]: #1203
boehmes@36900
  1745
#1200 := (~ #1199 #1199)
boehmes@36900
  1746
#1201 := [refl]: #1200
boehmes@36900
  1747
#1210 := [nnf-neg #1201 #1204 #1070 #1152 #1186 #1189 #1192 #1206]: #1209
boehmes@36900
  1748
#1196 := (not #858)
boehmes@36900
  1749
#1197 := (~ #1196 #1195)
boehmes@36900
  1750
#1193 := (~ #818 #818)
boehmes@36900
  1751
#1194 := [refl]: #1193
boehmes@36900
  1752
#1148 := (~ #1147 #1147)
boehmes@36900
  1753
#1149 := [refl]: #1148
boehmes@36900
  1754
#1145 := (~ #1144 #1144)
boehmes@36900
  1755
#1146 := [refl]: #1145
boehmes@36900
  1756
#1142 := (~ #1141 #1141)
boehmes@36900
  1757
#1143 := [refl]: #1142
boehmes@36900
  1758
#1139 := (~ #1138 #1138)
boehmes@36900
  1759
#1140 := [refl]: #1139
boehmes@36900
  1760
#1198 := [nnf-neg #1140 #1143 #1146 #1149 #1070 #1152 #1186 #1189 #1192 #1194]: #1197
boehmes@36900
  1761
#1214 := [nnf-neg #1198 #1210]: #1213
boehmes@36900
  1762
#1136 := (~ #727 #727)
boehmes@36900
  1763
#1137 := [refl]: #1136
boehmes@36900
  1764
#1218 := [nnf-neg #1070 #1137 #1214]: #1217
boehmes@36900
  1765
#1133 := (not #748)
boehmes@36900
  1766
#1134 := (~ #1133 #1132)
boehmes@36900
  1767
#1130 := (~ #892 #892)
boehmes@36900
  1768
#1131 := [refl]: #1130
boehmes@36900
  1769
#1127 := (not #719)
boehmes@36900
  1770
#1128 := (~ #1127 #1126)
boehmes@36900
  1771
#1123 := (not #716)
boehmes@36900
  1772
#1124 := (~ #1123 #1122)
boehmes@36900
  1773
#1117 := (not #713)
boehmes@36900
  1774
#1118 := (~ #1117 #1116)
boehmes@36900
  1775
#1119 := [sk]: #1118
boehmes@36900
  1776
#1101 := (not #702)
boehmes@36900
  1777
#1102 := (~ #1101 #1096)
boehmes@36900
  1778
#1097 := (~ #699 #1096)
boehmes@36900
  1779
#1098 := [sk]: #1097
boehmes@36900
  1780
#1103 := [nnf-neg #1098]: #1102
boehmes@36900
  1781
#1125 := [nnf-neg #1103 #1119]: #1124
boehmes@36900
  1782
#1084 := (~ #702 #1083)
boehmes@36900
  1783
#1081 := (~ #1080 #1080)
boehmes@36900
  1784
#1082 := [refl]: #1081
boehmes@36900
  1785
#1085 := [nnf-neg #1082]: #1084
boehmes@36900
  1786
#1129 := [nnf-neg #1085 #1125]: #1128
boehmes@36900
  1787
#1078 := (~ #1077 #1077)
boehmes@36900
  1788
#1079 := [refl]: #1078
boehmes@36900
  1789
#1075 := (~ #1074 #1074)
boehmes@36900
  1790
#1076 := [refl]: #1075
boehmes@36900
  1791
#1072 := (~ #1071 #1071)
boehmes@36900
  1792
#1073 := [refl]: #1072
boehmes@36900
  1793
#1135 := [nnf-neg #1073 #1076 #1079 #1070 #1129 #1131]: #1134
boehmes@36900
  1794
#1222 := [nnf-neg #1135 #1218]: #1221
boehmes@36900
  1795
#1065 := (not #664)
boehmes@36900
  1796
#1066 := (~ #1065 #661)
boehmes@36900
  1797
#1063 := (~ #661 #661)
boehmes@36900
  1798
#1061 := (~ #658 #658)
boehmes@36900
  1799
#1062 := [refl]: #1061
boehmes@36900
  1800
#1064 := [nnf-pos #1062]: #1063
boehmes@36900
  1801
#1067 := [nnf-neg #1064]: #1066
boehmes@36900
  1802
#1059 := (~ #1058 #1058)
boehmes@36900
  1803
#1060 := [refl]: #1059
boehmes@36900
  1804
#1233 := [nnf-neg #1060 #1067 #1070 #1222 #1229]: #1232
boehmes@36900
  1805
#1054 := (~ #664 #1053)
boehmes@36900
  1806
#1055 := [sk]: #1054
boehmes@36900
  1807
#1236 := [nnf-neg #1055 #1233]: #1235
boehmes@36900
  1808
#1002 := (not #967)
boehmes@36900
  1809
#1041 := (iff #1002 #1040)
boehmes@36900
  1810
#1038 := (iff #967 #1037)
boehmes@36900
  1811
#1035 := (iff #964 #1032)
boehmes@36900
  1812
#1017 := (or #528 #676 #913 #938)
boehmes@36900
  1813
#1029 := (or #664 #1017)
boehmes@36900
  1814
#1033 := (iff #1029 #1032)
boehmes@36900
  1815
#1034 := [rewrite]: #1033
boehmes@36900
  1816
#1030 := (iff #964 #1029)
boehmes@36900
  1817
#1027 := (iff #961 #1017)
boehmes@36900
  1818
#1022 := (and true #1017)
boehmes@36900
  1819
#1025 := (iff #1022 #1017)
boehmes@36900
  1820
#1026 := [rewrite]: #1025
boehmes@36900
  1821
#1023 := (iff #961 #1022)
boehmes@36900
  1822
#1020 := (iff #956 #1017)
boehmes@36900
  1823
#1014 := (or false #528 #676 #913 #938)
boehmes@36900
  1824
#1018 := (iff #1014 #1017)
boehmes@34994
  1825
#1019 := [rewrite]: #1018
boehmes@36900
  1826
#1015 := (iff #956 #1014)
boehmes@36900
  1827
#1012 := (iff #561 false)
boehmes@36900
  1828
#1010 := (iff #561 #632)
boehmes@36900
  1829
#1008 := (iff #13 true)
boehmes@36900
  1830
#1009 := [iff-true #1001]: #1008
boehmes@36900
  1831
#1011 := [monotonicity #1009]: #1010
boehmes@36900
  1832
#1013 := [trans #1011 #636]: #1012
boehmes@36900
  1833
#1016 := [monotonicity #1013]: #1015
boehmes@36900
  1834
#1021 := [trans #1016 #1019]: #1020
boehmes@36900
  1835
#1024 := [monotonicity #1009 #1021]: #1023
boehmes@36900
  1836
#1028 := [trans #1024 #1026]: #1027
boehmes@36900
  1837
#1031 := [monotonicity #1028]: #1030
boehmes@36900
  1838
#1036 := [trans #1031 #1034]: #1035
boehmes@36900
  1839
#1039 := [monotonicity #1036]: #1038
boehmes@36900
  1840
#1042 := [monotonicity #1039]: #1041
boehmes@36900
  1841
#1003 := [not-or-elim #1000]: #1002
boehmes@36900
  1842
#1043 := [mp #1003 #1042]: #1040
boehmes@36900
  1843
#1237 := [mp~ #1043 #1236]: #1234
boehmes@36900
  1844
#1238 := [mp #1237 #1425]: #1423
boehmes@36900
  1845
#1727 := [mp #1238 #1726]: #1722
boehmes@36900
  1846
#2292 := [mp #1727 #2291]: #2289
boehmes@36900
  1847
#2556 := [unit-resolution #2292 #2016]: #2286
boehmes@36900
  1848
#2111 := (or #2283 #2208)
boehmes@36900
  1849
#2097 := [def-axiom]: #2111
boehmes@36900
  1850
#2557 := [unit-resolution #2097 #2556]: #2208
boehmes@36900
  1851
#2120 := (or #2283 #176)
boehmes@36900
  1852
#2104 := [def-axiom]: #2120
boehmes@36900
  1853
#2620 := [unit-resolution #2104 #2556]: #176
boehmes@36900
  1854
#2352 := (or #2271 #528 #2213)
boehmes@36900
  1855
#1791 := (f5 f9)
boehmes@36900
  1856
#2296 := (= f10 #1791)
boehmes@36900
  1857
#2346 := (= #40 #1791)
boehmes@36900
  1858
#2344 := (= #1791 #40)
boehmes@36900
  1859
#2329 := [hypothesis]: #2274
boehmes@36900
  1860
#2037 := (or #2271 #179)
boehmes@36900
  1861
#2038 := [def-axiom]: #2037
boehmes@36900
  1862
#2340 := [unit-resolution #2038 #2329]: #179
boehmes@36900
  1863
#2341 := [symm #2340]: #44
boehmes@36900
  1864
#2345 := [monotonicity #2341]: #2344
boehmes@36900
  1865
#2347 := [symm #2345]: #2346
boehmes@36900
  1866
#2348 := (= f10 #40)
boehmes@36900
  1867
#2342 := [hypothesis]: #176
boehmes@36900
  1868
#2039 := (or #2271 #182)
boehmes@36900
  1869
#2040 := [def-axiom]: #2039
boehmes@36900
  1870
#2331 := [unit-resolution #2040 #2329]: #182
boehmes@36900
  1871
#2343 := [symm #2331]: #46
boehmes@36900
  1872
#2349 := [trans #2343 #2342]: #2348
boehmes@36900
  1873
#2350 := [trans #2349 #2347]: #2296
boehmes@36900
  1874
#2324 := (not #2296)
boehmes@36900
  1875
#1790 := (>= f9 0::int)
boehmes@36900
  1876
#1788 := (not #1790)
boehmes@36900
  1877
#1800 := (* -1::int f9)
boehmes@36900
  1878
#1787 := (+ f3 #1800)
boehmes@36900
  1879
#1789 := (<= #1787 0::int)
boehmes@36900
  1880
#2302 := (or #1789 #1788 #2296)
boehmes@36900
  1881
#2307 := (not #2302)
boehmes@36900
  1882
#2124 := (or #2271 #2265)
boehmes@36900
  1883
#2125 := [def-axiom]: #2124
boehmes@36900
  1884
#2330 := [unit-resolution #2125 #2329]: #2265
boehmes@36900
  1885
#1958 := (+ f8 #705)
boehmes@36900
  1886
#1959 := (<= #1958 0::int)
boehmes@36900
  1887
#2332 := (or #232 #1959)
boehmes@36900
  1888
#2333 := [th-lemma]: #2332
boehmes@36900
  1889
#2334 := [unit-resolution #2333 #2331]: #1959
boehmes@36900
  1890
#1836 := [hypothesis]: #2208
boehmes@36900
  1891
#2112 := (or #2271 #724)
boehmes@36900
  1892
#2114 := [def-axiom]: #2112
boehmes@36900
  1893
#2335 := [unit-resolution #2114 #2329]: #724
boehmes@36900
  1894
#1867 := (not #1959)
boehmes@36900
  1895
#1846 := (or #1687 #727 #2213 #1867)
boehmes@36900
  1896
#1869 := [hypothesis]: #724
boehmes@36900
  1897
#1948 := (+ f7 #1108)
boehmes@36900
  1898
#1949 := (<= #1948 0::int)
boehmes@36900
  1899
#1927 := (+ f8 #1291)
boehmes@36900
  1900
#1928 := (>= #1927 0::int)
boehmes@36900
  1901
#1866 := (not #1928)
boehmes@36900
  1902
#1860 := [hypothesis]: #1959
boehmes@36900
  1903
#2023 := (not #1293)
boehmes@36900
  1904
#1852 := [hypothesis]: #1690
boehmes@36900
  1905
#2024 := (or #1687 #2023)
boehmes@36900
  1906
#1983 := [def-axiom]: #2024
boehmes@36900
  1907
#1854 := [unit-resolution #1983 #1852]: #2023
boehmes@36900
  1908
#1868 := (or #1866 #1293 #1867)
boehmes@36900
  1909
#1851 := [hypothesis]: #2023
boehmes@36900
  1910
#1864 := [hypothesis]: #1928
boehmes@36900
  1911
#1865 := [th-lemma #1864 #1851 #1860]: false
boehmes@36900
  1912
#1858 := [lemma #1865]: #1868
boehmes@36900
  1913
#1855 := [unit-resolution #1858 #1854 #1860]: #1866
boehmes@36900
  1914
#1841 := (or #1928 #1949)
boehmes@36900
  1915
#2140 := (or #1687 #1112)
boehmes@36900
  1916
#2022 := [def-axiom]: #2140
boehmes@36900
  1917
#1834 := [unit-resolution #2022 #1852]: #1112
boehmes@36900
  1918
#1917 := (or #2213 #1530 #1928 #1949)
boehmes@36900
  1919
#1960 := (+ #1105 #927)
boehmes@36900
  1920
#1950 := (<= #1960 0::int)
boehmes@36900
  1921
#1940 := (+ ?v0!2 #722)
boehmes@36900
  1922
#1942 := (>= #1940 0::int)
boehmes@36900
  1923
#1943 := (or #1530 #1942 #1950)
boehmes@36900
  1924
#1918 := (or #2213 #1943)
boehmes@36900
  1925
#1909 := (iff #1918 #1917)
boehmes@36900
  1926
#1911 := (or #1530 #1928 #1949)
boehmes@36900
  1927
#1912 := (or #2213 #1911)
boehmes@36900
  1928
#1906 := (iff #1912 #1917)
boehmes@36900
  1929
#1907 := [rewrite]: #1906
boehmes@36900
  1930
#1920 := (iff #1918 #1912)
boehmes@36900
  1931
#1915 := (iff #1943 #1911)
boehmes@36900
  1932
#1933 := (or #1530 #1949 #1928)
boehmes@36900
  1933
#1913 := (iff #1933 #1911)
boehmes@36900
  1934
#1914 := [rewrite]: #1913
boehmes@36900
  1935
#1922 := (iff #1943 #1933)
boehmes@36900
  1936
#1931 := (iff #1950 #1928)
boehmes@36900
  1937
#1939 := (+ #927 #1105)
boehmes@36900
  1938
#1924 := (<= #1939 0::int)
boehmes@36900
  1939
#1929 := (iff #1924 #1928)
boehmes@36900
  1940
#1930 := [rewrite]: #1929
boehmes@36900
  1941
#1925 := (iff #1950 #1924)
boehmes@36900
  1942
#1921 := (= #1960 #1939)
boehmes@36900
  1943
#1923 := [rewrite]: #1921
boehmes@36900
  1944
#1926 := [monotonicity #1923]: #1925
boehmes@36900
  1945
#1932 := [trans #1926 #1930]: #1931
boehmes@36900
  1946
#1938 := (iff #1942 #1949)
boehmes@36900
  1947
#1946 := (+ #722 ?v0!2)
boehmes@36900
  1948
#1944 := (>= #1946 0::int)
boehmes@36900
  1949
#1935 := (iff #1944 #1949)
boehmes@36900
  1950
#1937 := [rewrite]: #1935
boehmes@36900
  1951
#1952 := (iff #1942 #1944)
boehmes@36900
  1952
#1947 := (= #1940 #1946)
boehmes@36900
  1953
#1951 := [rewrite]: #1947
boehmes@36900
  1954
#1945 := [monotonicity #1951]: #1952
boehmes@36900
  1955
#1936 := [trans #1945 #1937]: #1938
boehmes@36900
  1956
#1934 := [monotonicity #1936 #1932]: #1922
boehmes@36900
  1957
#1916 := [trans #1934 #1914]: #1915
boehmes@36900
  1958
#1905 := [monotonicity #1916]: #1920
boehmes@36900
  1959
#1908 := [trans #1905 #1907]: #1909
boehmes@36900
  1960
#1919 := [quant-inst]: #1918
boehmes@36900
  1961
#1910 := [mp #1919 #1908]: #1917
boehmes@36900
  1962
#1842 := [unit-resolution #1910 #1836 #1834]: #1841
boehmes@36900
  1963
#1843 := [unit-resolution #1842 #1855]: #1949
boehmes@36900
  1964
#2139 := (or #1687 #1111)
boehmes@36900
  1965
#2137 := [def-axiom]: #2139
boehmes@36900
  1966
#1844 := [unit-resolution #2137 #1852]: #1111
boehmes@36900
  1967
#1845 := [th-lemma #1844 #1843 #1869]: false
boehmes@36900
  1968
#1835 := [lemma #1845]: #1846
boehmes@36900
  1969
#2336 := [unit-resolution #1835 #2335 #1836 #2334]: #1687
boehmes@36900
  1970
#2028 := (or #2268 #2260 #1690)
boehmes@36900
  1971
#2036 := [def-axiom]: #2028
boehmes@36900
  1972
#2337 := [unit-resolution #2036 #2336 #2330]: #2260
boehmes@36900
  1973
#2132 := (not #2260)
boehmes@36900
  1974
#2310 := (or #2132 #2307)
boehmes@36900
  1975
#2293 := (= #1791 f10)
boehmes@36900
  1976
#2294 := (or #2293 #1788 #1789)
boehmes@36900
  1977
#2295 := (not #2294)
boehmes@36900
  1978
#2311 := (or #2132 #2295)
boehmes@36900
  1979
#2313 := (iff #2311 #2310)
boehmes@36900
  1980
#2315 := (iff #2310 #2310)
boehmes@36900
  1981
#2316 := [rewrite]: #2315
boehmes@36900
  1982
#2308 := (iff #2295 #2307)
boehmes@36900
  1983
#2305 := (iff #2294 #2302)
boehmes@36900
  1984
#2299 := (or #2296 #1788 #1789)
boehmes@36900
  1985
#2303 := (iff #2299 #2302)
boehmes@36900
  1986
#2304 := [rewrite]: #2303
boehmes@36900
  1987
#2300 := (iff #2294 #2299)
boehmes@36900
  1988
#2297 := (iff #2293 #2296)
boehmes@36900
  1989
#2298 := [rewrite]: #2297
boehmes@36900
  1990
#2301 := [monotonicity #2298]: #2300
boehmes@36900
  1991
#2306 := [trans #2301 #2304]: #2305
boehmes@36900
  1992
#2309 := [monotonicity #2306]: #2308
boehmes@36900
  1993
#2314 := [monotonicity #2309]: #2313
boehmes@36900
  1994
#2317 := [trans #2314 #2316]: #2313
boehmes@36900
  1995
#2312 := [quant-inst]: #2311
boehmes@36900
  1996
#2318 := [mp #2312 #2317]: #2310
boehmes@36900
  1997
#2338 := [unit-resolution #2318 #2337]: #2307
boehmes@36900
  1998
#2325 := (or #2302 #2324)
boehmes@36900
  1999
#2326 := [def-axiom]: #2325
boehmes@36900
  2000
#2339 := [unit-resolution #2326 #2338]: #2324
boehmes@36900
  2001
#2351 := [unit-resolution #2339 #2350]: false
boehmes@36900
  2002
#2353 := [lemma #2351]: #2352
boehmes@36900
  2003
#2621 := [unit-resolution #2353 #2620 #2557]: #2271
boehmes@36900
  2004
#2098 := (or #2283 #2277)
boehmes@36900
  2005
#2100 := [def-axiom]: #2098
boehmes@36900
  2006
#2622 := [unit-resolution #2100 #2556]: #2277
boehmes@36900
  2007
#2119 := (or #2280 #2257 #2274)
boehmes@36900
  2008
#2113 := [def-axiom]: #2119
boehmes@36900
  2009
#2623 := [unit-resolution #2113 #2622 #2621]: #2257
boehmes@36900
  2010
#2147 := (or #2254 #2248)
boehmes@36900
  2011
#2141 := [def-axiom]: #2147
boehmes@36900
  2012
#2624 := [unit-resolution #2141 #2623]: #2248
boehmes@36900
  2013
#1793 := [hypothesis]: #2239
boehmes@36900
  2014
#2183 := (or #2236 #2230)
boehmes@36900
  2015
#2186 := [def-axiom]: #2183
boehmes@36900
  2016
#2528 := [unit-resolution #2186 #1793]: #2230
boehmes@36900
  2017
#2319 := (or #2236 #307)
boehmes@36900
  2018
#1818 := (= #68 #90)
boehmes@36900
  2019
#1795 := (= #90 #68)
boehmes@36900
  2020
#1838 := (or #2236 #285)
boehmes@36900
  2021
#1839 := [def-axiom]: #1838
boehmes@36900
  2022
#1798 := [unit-resolution #1839 #1793]: #285
boehmes@36900
  2023
#1799 := [symm #1798]: #74
boehmes@36900
  2024
#1817 := [monotonicity #1799]: #1795
boehmes@36900
  2025
#1801 := [symm #1817]: #1818
boehmes@36900
  2026
#1804 := (= f14 #68)
boehmes@36900
  2027
#2174 := (or #2236 #280)
boehmes@36900
  2028
#1837 := [def-axiom]: #2174
boehmes@36900
  2029
#1797 := [unit-resolution #1837 #1793]: #280
boehmes@36900
  2030
#1815 := [symm #1797]: #71
boehmes@36900
  2031
#1840 := (or #2236 #288)
boehmes@36900
  2032
#2176 := [def-axiom]: #1840
boehmes@36900
  2033
#1794 := [unit-resolution #2176 #1793]: #288
boehmes@36900
  2034
#1813 := [symm #1794]: #76
boehmes@36900
  2035
#1805 := [trans #1813 #1815]: #1804
boehmes@36900
  2036
#1808 := [trans #1805 #1801]: #307
boehmes@36900
  2037
#1796 := [hypothesis]: #1169
boehmes@36900
  2038
#1809 := [unit-resolution #1796 #1808]: false
boehmes@36900
  2039
#2320 := [lemma #1809]: #2319
boehmes@36900
  2040
#2529 := [unit-resolution #2320 #1793]: #307
boehmes@36900
  2041
#1856 := (or #2224 #1169)
boehmes@36900
  2042
#2191 := [def-axiom]: #1856
boehmes@36900
  2043
#2530 := [unit-resolution #2191 #2529]: #2224
boehmes@36900
  2044
#2190 := (or #2233 #2227 #1629)
boehmes@36900
  2045
#1833 := [def-axiom]: #2190
boehmes@36900
  2046
#2531 := [unit-resolution #1833 #2530 #2528]: #1629
boehmes@36900
  2047
#2194 := (or #1624 #1341)
boehmes@36900
  2048
#2195 := [def-axiom]: #2194
boehmes@36900
  2049
#2532 := [unit-resolution #2195 #2531]: #1341
boehmes@36900
  2050
#1877 := (>= #803 -1::int)
boehmes@36900
  2051
#2184 := (or #2236 #802)
boehmes@36900
  2052
#1824 := [def-axiom]: #2184
boehmes@36900
  2053
#2533 := [unit-resolution #1824 #1793]: #802
boehmes@36900
  2054
#2534 := (or #806 #1877)
boehmes@36900
  2055
#2535 := [th-lemma]: #2534
boehmes@36900
  2056
#2536 := [unit-resolution #2535 #2533]: #1877
boehmes@36900
  2057
#2562 := (not #2496)
boehmes@36900
  2058
#2525 := (not #2494)
boehmes@36900
  2059
#2495 := (= #90 #1154)
boehmes@36900
  2060
#2499 := (not #2495)
boehmes@36900
  2061
#2502 := (+ #90 #1356)
boehmes@36900
  2062
#2504 := (>= #2502 0::int)
boehmes@36900
  2063
#2509 := (not #2504)
boehmes@36900
  2064
#2196 := (not #1358)
boehmes@36900
  2065
#2197 := (or #1624 #2196)
boehmes@36900
  2066
#2192 := [def-axiom]: #2197
boehmes@36900
  2067
#2537 := [unit-resolution #2192 #2531]: #2196
boehmes@36900
  2068
#2451 := (* -1::int #90)
boehmes@36900
  2069
#2490 := (+ f14 #2451)
boehmes@36900
  2070
#2492 := (>= #2490 0::int)
boehmes@36900
  2071
#2538 := (or #1169 #2492)
boehmes@36900
  2072
#2539 := [th-lemma]: #2538
boehmes@36900
  2073
#2540 := [unit-resolution #2539 #2529]: #2492
boehmes@36900
  2074
#2510 := (not #2492)
boehmes@36900
  2075
#2511 := (or #2509 #2510 #1358)
boehmes@36900
  2076
#2505 := [hypothesis]: #2504
boehmes@36900
  2077
#2506 := [hypothesis]: #2196
boehmes@36900
  2078
#2507 := [hypothesis]: #2492
boehmes@36900
  2079
#2508 := [th-lemma #2507 #2506 #2505]: false
boehmes@36900
  2080
#2512 := [lemma #2508]: #2511
boehmes@36900
  2081
#2541 := [unit-resolution #2512 #2540 #2537]: #2509
boehmes@36900
  2082
#2500 := (or #2499 #2504)
boehmes@36900
  2083
#2501 := [th-lemma]: #2500
boehmes@36900
  2084
#2542 := [unit-resolution #2501 #2541]: #2499
boehmes@36900
  2085
#2526 := (or #2525 #2495 #375)
boehmes@36900
  2086
#2521 := (= #1154 #90)
boehmes@36900
  2087
#2519 := (= ?v0!3 f13)
boehmes@36900
  2088
#2515 := [hypothesis]: #285
boehmes@36900
  2089
#2517 := (= ?v0!3 f7)
boehmes@36900
  2090
#2516 := [hypothesis]: #2494
boehmes@36900
  2091
#2518 := [symm #2516]: #2517
boehmes@36900
  2092
#2520 := [trans #2518 #2515]: #2519
boehmes@36900
  2093
#2522 := [monotonicity #2520]: #2521
boehmes@36900
  2094
#2523 := [symm #2522]: #2495
boehmes@36900
  2095
#2514 := [hypothesis]: #2499
boehmes@36900
  2096
#2524 := [unit-resolution #2514 #2523]: false
boehmes@36900
  2097
#2527 := [lemma #2524]: #2526
boehmes@36900
  2098
#2543 := [unit-resolution #2527 #2542 #1798]: #2525
boehmes@36900
  2099
#2565 := (or #2494 #2562)
boehmes@36900
  2100
#2381 := (<= #2380 0::int)
boehmes@36900
  2101
#2392 := (+ f8 #1356)
boehmes@36900
  2102
#2393 := (>= #2392 0::int)
boehmes@36900
  2103
#2550 := (not #2393)
boehmes@36900
  2104
#1825 := (or #2236 #818)
boehmes@36900
  2105
#2185 := [def-axiom]: #1825
boehmes@36900
  2106
#2544 := [unit-resolution #2185 #1793]: #818
boehmes@36900
  2107
#2366 := (+ #68 #777)
boehmes@36900
  2108
#2367 := (<= #2366 0::int)
boehmes@36900
  2109
#2365 := (= #68 f14)
boehmes@36900
  2110
#2545 := [trans #1797 #1794]: #2365
boehmes@36900
  2111
#2546 := (not #2365)
boehmes@36900
  2112
#2547 := (or #2546 #2367)
boehmes@36900
  2113
#2548 := [th-lemma]: #2547
boehmes@36900
  2114
#2549 := [unit-resolution #2548 #2545]: #2367
boehmes@36900
  2115
#2551 := (not #2367)
boehmes@36900
  2116
#2552 := (or #2550 #1358 #2551 #819)
boehmes@36900
  2117
#2553 := [th-lemma]: #2552
boehmes@36900
  2118
#2554 := [unit-resolution #2553 #2537 #2549 #2544]: #2550
boehmes@36900
  2119
#2558 := (or #2381 #2393)
boehmes@36900
  2120
#1861 := (or #1624 #1160)
boehmes@36900
  2121
#1862 := [def-axiom]: #1861
boehmes@36900
  2122
#2555 := [unit-resolution #1862 #2531]: #1160
boehmes@36900
  2123
#2401 := (or #2213 #1609 #2381 #2393)
boehmes@36900
  2124
#2369 := (+ #1154 #927)
boehmes@36900
  2125
#2370 := (<= #2369 0::int)
boehmes@36900
  2126
#2371 := (+ ?v0!3 #722)
boehmes@36900
  2127
#2372 := (>= #2371 0::int)
boehmes@36900
  2128
#2373 := (or #1609 #2372 #2370)
boehmes@36900
  2129
#2402 := (or #2213 #2373)
boehmes@36900
  2130
#2409 := (iff #2402 #2401)
boehmes@36900
  2131
#2398 := (or #1609 #2381 #2393)
boehmes@36900
  2132
#2404 := (or #2213 #2398)
boehmes@36900
  2133
#2407 := (iff #2404 #2401)
boehmes@36900
  2134
#2408 := [rewrite]: #2407
boehmes@36900
  2135
#2405 := (iff #2402 #2404)
boehmes@36900
  2136
#2399 := (iff #2373 #2398)
boehmes@36900
  2137
#2396 := (iff #2370 #2393)
boehmes@36900
  2138
#2386 := (+ #927 #1154)
boehmes@36900
  2139
#2389 := (<= #2386 0::int)
boehmes@36900
  2140
#2394 := (iff #2389 #2393)
boehmes@36900
  2141
#2395 := [rewrite]: #2394
boehmes@36900
  2142
#2390 := (iff #2370 #2389)
boehmes@36900
  2143
#2387 := (= #2369 #2386)
boehmes@36900
  2144
#2388 := [rewrite]: #2387
boehmes@36900
  2145
#2391 := [monotonicity #2388]: #2390
boehmes@36900
  2146
#2397 := [trans #2391 #2395]: #2396
boehmes@36900
  2147
#2384 := (iff #2372 #2381)
boehmes@36900
  2148
#2374 := (+ #722 ?v0!3)
boehmes@36900
  2149
#2377 := (>= #2374 0::int)
boehmes@36900
  2150
#2382 := (iff #2377 #2381)
boehmes@36900
  2151
#2383 := [rewrite]: #2382
boehmes@36900
  2152
#2378 := (iff #2372 #2377)
boehmes@36900
  2153
#2375 := (= #2371 #2374)
boehmes@36900
  2154
#2376 := [rewrite]: #2375
boehmes@36900
  2155
#2379 := [monotonicity #2376]: #2378
boehmes@36900
  2156
#2385 := [trans #2379 #2383]: #2384
boehmes@36900
  2157
#2400 := [monotonicity #2385 #2397]: #2399
boehmes@36900
  2158
#2406 := [monotonicity #2400]: #2405
boehmes@36900
  2159
#2410 := [trans #2406 #2408]: #2409
boehmes@36900
  2160
#2403 := [quant-inst]: #2402
boehmes@36900
  2161
#2411 := [mp #2403 #2410]: #2401
boehmes@36900
  2162
#2559 := [unit-resolution #2411 #2557 #2555]: #2558
boehmes@36900
  2163
#2560 := [unit-resolution #2559 #2554]: #2381
boehmes@36900
  2164
#2561 := (not #2381)
boehmes@36900
  2165
#2563 := (or #2494 #2561 #2562)
boehmes@36900
  2166
#2564 := [th-lemma]: #2563
boehmes@36900
  2167
#2566 := [unit-resolution #2564 #2560]: #2565
boehmes@36900
  2168
#2567 := [unit-resolution #2566 #2543]: #2562
boehmes@36900
  2169
#2568 := [th-lemma #2567 #2536 #2532]: false
boehmes@36900
  2170
#2569 := [lemma #2568]: #2236
boehmes@36900
  2171
#2153 := (or #2251 #2239 #2245)
boehmes@36900
  2172
#2159 := [def-axiom]: #2153
boehmes@36900
  2173
#2625 := [unit-resolution #2159 #2569 #2624]: #2245
boehmes@36900
  2174
#2165 := (or #2242 #2230)
boehmes@36900
  2175
#2154 := [def-axiom]: #2165
boehmes@36900
  2176
#2626 := [unit-resolution #2154 #2625]: #2230
boehmes@36900
  2177
#2421 := (= #40 #90)
boehmes@36900
  2178
#2631 := (= #90 #40)
boehmes@36900
  2179
#1891 := (or #2242 #423)
boehmes@36900
  2180
#1892 := [def-axiom]: #1891
boehmes@36900
  2181
#2627 := [unit-resolution #1892 #2625]: #423
boehmes@36900
  2182
#2628 := [symm #2627]: #107
boehmes@36900
  2183
#2632 := [monotonicity #2628]: #2631
boehmes@36900
  2184
#2633 := [symm #2632]: #2421
boehmes@36900
  2185
#2634 := (= f14 #40)
boehmes@36900
  2186
#2166 := (or #2242 #426)
boehmes@36900
  2187
#2170 := [def-axiom]: #2166
boehmes@36900
  2188
#2629 := [unit-resolution #2170 #2625]: #426
boehmes@36900
  2189
#2630 := [symm #2629]: #108
boehmes@36900
  2190
#2635 := [trans #2630 #2620]: #2634
boehmes@36900
  2191
#2636 := [trans #2635 #2633]: #307
boehmes@36900
  2192
#2637 := [unit-resolution #2191 #2636]: #2224
boehmes@36900
  2193
#2638 := [unit-resolution #1833 #2637 #2626]: #1629
boehmes@36900
  2194
#2639 := [unit-resolution #2195 #2638]: #1341
boehmes@36900
  2195
#1878 := (or #2242 #802)
boehmes@36900
  2196
#2160 := [def-axiom]: #1878
boehmes@36900
  2197
#2640 := [unit-resolution #2160 #2625]: #802
boehmes@36900
  2198
#2641 := [unit-resolution #2535 #2640]: #1877
boehmes@36900
  2199
#2642 := [hypothesis]: #2562
boehmes@36900
  2200
#2643 := [th-lemma #2642 #2641 #2639]: false
boehmes@36900
  2201
#2644 := [lemma #2643]: #2496
boehmes@36900
  2202
#2649 := [unit-resolution #2192 #2638]: #2196
boehmes@36900
  2203
#1792 := (+ f8 #777)
boehmes@36900
  2204
#2168 := (<= #1792 0::int)
boehmes@36900
  2205
#2650 := (or #432 #2168)
boehmes@36900
  2206
#2651 := [th-lemma]: #2650
boehmes@36900
  2207
#2652 := [unit-resolution #2651 #2629]: #2168
boehmes@36900
  2208
#2653 := (not #2168)
boehmes@36900
  2209
#2654 := (or #2550 #1358 #2653)
boehmes@36900
  2210
#2655 := [th-lemma]: #2654
boehmes@36900
  2211
#2656 := [unit-resolution #2655 #2652 #2649]: #2550
boehmes@36900
  2212
#2657 := [unit-resolution #1862 #2638]: #1160
boehmes@36900
  2213
#2658 := [unit-resolution #2411 #2557 #2657 #2656]: #2381
boehmes@36900
  2214
#2659 := [unit-resolution #2564 #2658]: #2565
boehmes@36900
  2215
#2660 := [unit-resolution #2659 #2644]: #2494
boehmes@36900
  2216
#2661 := [monotonicity #2660]: #2645
boehmes@36900
  2217
#2662 := (not #2645)
boehmes@36900
  2218
#2663 := (or #2662 #2648)
boehmes@36900
  2219
#2664 := [th-lemma]: #2663
boehmes@36900
  2220
#2665 := [unit-resolution #2664 #2661]: #2648
boehmes@36900
  2221
#2164 := (or #2242 #819)
boehmes@36900
  2222
#2161 := [def-axiom]: #2164
boehmes@36900
  2223
#2666 := [unit-resolution #2161 #2625]: #819
boehmes@36900
  2224
[th-lemma #2666 #2649 #2652 #2665]: false
boehmes@34994
  2225
unsat