src/HOL/Boogie/Examples/Boogie_Dijkstra.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
585d6a826013e58a18631a689e131cc7e15b8538 6889 0
boehmes@34994
     2
#2 := false
boehmes@36900
     3
decl f11 :: (-> S5 S2 S1)
boehmes@36900
     4
decl ?v1!7 :: (-> S2 S2)
boehmes@36900
     5
decl ?v0!20 :: S2
boehmes@36900
     6
#2295 := ?v0!20
boehmes@36900
     7
#6027 := (?v1!7 ?v0!20)
boehmes@36900
     8
decl f20 :: S5
boehmes@36900
     9
#146 := f20
boehmes@36900
    10
#12518 := (f11 f20 #6027)
boehmes@36900
    11
decl f1 :: S1
boehmes@36900
    12
#4 := f1
boehmes@36900
    13
#16616 := (= f1 #12518)
boehmes@36900
    14
decl f23 :: (-> S3 S2)
boehmes@36900
    15
decl f5 :: (-> S2 S2 S3)
boehmes@36900
    16
#6032 := (f5 #6027 ?v0!20)
boehmes@36900
    17
#19988 := (f23 #6032)
boehmes@36900
    18
decl f21 :: (-> S5 S2 S1 S5)
boehmes@36900
    19
decl f19 :: S2
boehmes@36900
    20
#137 := f19
boehmes@36900
    21
decl f12 :: S5
boehmes@36900
    22
#71 := f12
boehmes@36900
    23
#147 := (f21 f12 f19 f1)
boehmes@36900
    24
#3738 := (f11 #147 f19)
boehmes@36900
    25
decl f24 :: (-> S3 S2)
boehmes@36900
    26
#4718 := (f5 f19 f19)
boehmes@36900
    27
#9605 := (f24 #4718)
boehmes@36900
    28
#10278 := (f21 f12 #9605 #3738)
boehmes@36900
    29
#30481 := (f11 #10278 #19988)
boehmes@36900
    30
#24597 := (= #30481 #12518)
boehmes@36900
    31
#24573 := (= #12518 #30481)
boehmes@36900
    32
#20012 := (= #6027 #19988)
boehmes@36900
    33
#12 := (:var 0 S2)
boehmes@36900
    34
#11 := (:var 1 S2)
boehmes@36900
    35
#14 := (f5 #11 #12)
boehmes@36900
    36
#4135 := (pattern #14)
boehmes@36900
    37
#259 := (f23 #14)
boehmes@36900
    38
#1779 := (= #11 #259)
boehmes@36900
    39
#4555 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4135) #1779)
boehmes@36900
    40
#1783 := (forall (vars (?v0 S2) (?v1 S2)) #1779)
boehmes@36900
    41
#4558 := (iff #1783 #4555)
boehmes@36900
    42
#4556 := (iff #1779 #1779)
boehmes@36900
    43
#4557 := [refl]: #4556
boehmes@36900
    44
#4559 := [quant-intro #4557]: #4558
boehmes@36900
    45
#1822 := (~ #1783 #1783)
boehmes@36900
    46
#2078 := (~ #1779 #1779)
boehmes@36900
    47
#2228 := [refl]: #2078
boehmes@36900
    48
#1823 := [nnf-pos #2228]: #1822
boehmes@36900
    49
#260 := (= #259 #11)
boehmes@36900
    50
#261 := (forall (vars (?v0 S2) (?v1 S2)) #260)
boehmes@36900
    51
#1784 := (iff #261 #1783)
boehmes@36900
    52
#1781 := (iff #260 #1779)
boehmes@36900
    53
#1782 := [rewrite]: #1781
boehmes@36900
    54
#1785 := [quant-intro #1782]: #1784
boehmes@36900
    55
#1778 := [asserted]: #261
boehmes@36900
    56
#1788 := [mp #1778 #1785]: #1783
boehmes@36900
    57
#2229 := [mp~ #1788 #1823]: #1783
boehmes@36900
    58
#4560 := [mp #2229 #4559]: #4555
boehmes@36900
    59
#9574 := (not #4555)
boehmes@36900
    60
#20097 := (or #9574 #20012)
boehmes@36900
    61
#16830 := [quant-inst]: #20097
boehmes@36900
    62
#30680 := [unit-resolution #16830 #4560]: #20012
boehmes@36900
    63
#13558 := (= f20 #10278)
boehmes@36900
    64
#13508 := (= #147 #10278)
boehmes@36900
    65
#11165 := (= #10278 #147)
boehmes@36900
    66
#11163 := (= #3738 f1)
boehmes@36900
    67
#3747 := (= f1 #3738)
boehmes@36900
    68
#239 := (:var 0 S1)
boehmes@36900
    69
#238 := (:var 2 S5)
boehmes@36900
    70
#240 := (f21 #238 #11 #239)
boehmes@36900
    71
#4541 := (pattern #240)
boehmes@36900
    72
#1749 := (= f1 #239)
boehmes@36900
    73
#241 := (f11 #240 #11)
boehmes@36900
    74
#1746 := (= f1 #241)
boehmes@36900
    75
#1752 := (iff #1746 #1749)
boehmes@36900
    76
#4542 := (forall (vars (?v0 S5) (?v1 S2) (?v2 S1)) (:pat #4541) #1752)
boehmes@36900
    77
#1755 := (forall (vars (?v0 S5) (?v1 S2) (?v2 S1)) #1752)
boehmes@36900
    78
#4545 := (iff #1755 #4542)
boehmes@36900
    79
#4543 := (iff #1752 #1752)
boehmes@36900
    80
#4544 := [refl]: #4543
boehmes@36900
    81
#4546 := [quant-intro #4544]: #4545
boehmes@36900
    82
#1818 := (~ #1755 #1755)
boehmes@36900
    83
#2003 := (~ #1752 #1752)
boehmes@36900
    84
#1849 := [refl]: #2003
boehmes@36900
    85
#1819 := [nnf-pos #1849]: #1818
boehmes@36900
    86
#243 := (= #239 f1)
boehmes@36900
    87
#242 := (= #241 f1)
boehmes@36900
    88
#244 := (iff #242 #243)
boehmes@36900
    89
#245 := (forall (vars (?v0 S5) (?v1 S2) (?v2 S1)) #244)
boehmes@36900
    90
#1756 := (iff #245 #1755)
boehmes@36900
    91
#1753 := (iff #244 #1752)
boehmes@36900
    92
#1750 := (iff #243 #1749)
boehmes@36900
    93
#1751 := [rewrite]: #1750
boehmes@36900
    94
#1747 := (iff #242 #1746)
boehmes@36900
    95
#1748 := [rewrite]: #1747
boehmes@36900
    96
#1754 := [monotonicity #1748 #1751]: #1753
boehmes@36900
    97
#1757 := [quant-intro #1754]: #1756
boehmes@36900
    98
#1745 := [asserted]: #245
boehmes@36900
    99
#1760 := [mp #1745 #1757]: #1755
boehmes@36900
   100
#1850 := [mp~ #1760 #1819]: #1755
boehmes@36900
   101
#4547 := [mp #1850 #4546]: #4542
boehmes@36900
   102
#6762 := (not #4542)
boehmes@36900
   103
#6880 := (or #6762 #3747)
boehmes@36900
   104
#3746 := (= f1 f1)
boehmes@36900
   105
#3734 := (iff #3747 #3746)
boehmes@36900
   106
#6881 := (or #6762 #3734)
boehmes@36900
   107
#6895 := (iff #6881 #6880)
boehmes@36900
   108
#7240 := (iff #6880 #6880)
boehmes@36900
   109
#7241 := [rewrite]: #7240
boehmes@36900
   110
#4575 := (iff #3734 #3747)
boehmes@36900
   111
#1 := true
boehmes@36900
   112
#3724 := (iff #3747 true)
boehmes@36900
   113
#3730 := (iff #3724 #3747)
boehmes@36900
   114
#3726 := [rewrite]: #3730
boehmes@36900
   115
#3725 := (iff #3734 #3724)
boehmes@36900
   116
#3735 := (iff #3746 true)
boehmes@36900
   117
#3722 := [rewrite]: #3735
boehmes@36900
   118
#3723 := [monotonicity #3722]: #3725
boehmes@36900
   119
#4576 := [trans #3723 #3726]: #4575
boehmes@36900
   120
#7239 := [monotonicity #4576]: #6895
boehmes@36900
   121
#7243 := [trans #7239 #7241]: #6895
boehmes@36900
   122
#6896 := [quant-inst]: #6881
boehmes@36900
   123
#7244 := [mp #6896 #7243]: #6880
boehmes@36900
   124
#11162 := [unit-resolution #7244 #4547]: #3747
boehmes@36900
   125
#11164 := [symm #11162]: #11163
boehmes@36900
   126
#10825 := (= #9605 f19)
boehmes@36900
   127
#9606 := (= f19 #9605)
boehmes@36900
   128
#262 := (f24 #14)
boehmes@36900
   129
#1787 := (= #12 #262)
boehmes@36900
   130
#4561 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4135) #1787)
boehmes@36900
   131
#1791 := (forall (vars (?v0 S2) (?v1 S2)) #1787)
boehmes@36900
   132
#4564 := (iff #1791 #4561)
boehmes@36900
   133
#4562 := (iff #1787 #1787)
boehmes@36900
   134
#4563 := [refl]: #4562
boehmes@36900
   135
#4565 := [quant-intro #4563]: #4564
boehmes@36900
   136
#1824 := (~ #1791 #1791)
boehmes@36900
   137
#1876 := (~ #1787 #1787)
boehmes@36900
   138
#1877 := [refl]: #1876
boehmes@36900
   139
#1825 := [nnf-pos #1877]: #1824
boehmes@36900
   140
#263 := (= #262 #12)
boehmes@36900
   141
#264 := (forall (vars (?v0 S2) (?v1 S2)) #263)
boehmes@36900
   142
#1792 := (iff #264 #1791)
boehmes@36900
   143
#1789 := (iff #263 #1787)
boehmes@36900
   144
#1790 := [rewrite]: #1789
boehmes@36900
   145
#1793 := [quant-intro #1790]: #1792
boehmes@36900
   146
#1786 := [asserted]: #264
boehmes@36900
   147
#1796 := [mp #1786 #1793]: #1791
boehmes@36900
   148
#2188 := [mp~ #1796 #1825]: #1791
boehmes@36900
   149
#4566 := [mp #2188 #4565]: #4561
boehmes@36900
   150
#7210 := (not #4561)
boehmes@36900
   151
#9608 := (or #7210 #9606)
boehmes@36900
   152
#9609 := [quant-inst]: #9608
boehmes@36900
   153
#10824 := [unit-resolution #9609 #4566]: #9606
boehmes@36900
   154
#10826 := [symm #10824]: #10825
boehmes@36900
   155
#11166 := [monotonicity #10826 #11164]: #11165
boehmes@36900
   156
#13557 := [symm #11166]: #13508
boehmes@36900
   157
#148 := (= f20 #147)
boehmes@36900
   158
#2299 := (f5 #12 ?v0!20)
boehmes@36900
   159
#4384 := (pattern #2299)
boehmes@36900
   160
decl f22 :: (-> S2 int)
boehmes@36900
   161
#155 := (f22 #12)
boehmes@36900
   162
#4324 := (pattern #155)
boehmes@36900
   163
#165 := (f11 f20 #12)
boehmes@36900
   164
#4350 := (pattern #165)
boehmes@36900
   165
#8 := 0::int
boehmes@36900
   166
decl f4 :: (-> S3 int)
boehmes@36900
   167
#2300 := (f4 #2299)
boehmes@36900
   168
#2296 := (f22 ?v0!20)
boehmes@36900
   169
#1114 := -1::int
boehmes@36900
   170
#2297 := (* -1::int #2296)
boehmes@36900
   171
#2899 := (+ #2297 #2300)
boehmes@36900
   172
#2900 := (+ #155 #2899)
boehmes@36900
   173
#2903 := (= #2900 0::int)
boehmes@36900
   174
#3480 := (not #2903)
boehmes@36900
   175
#2298 := (+ #155 #2297)
boehmes@36900
   176
#2303 := (>= #2298 0::int)
boehmes@36900
   177
#713 := (= f1 #165)
boehmes@36900
   178
#719 := (not #713)
boehmes@36900
   179
#3481 := (or #719 #2303 #3480)
boehmes@36900
   180
#4385 := (forall (vars (?v1 S2)) (:pat #4350 #4324 #4384) #3481)
boehmes@36900
   181
#4390 := (not #4385)
boehmes@36900
   182
#48 := (f5 #12 #11)
boehmes@36900
   183
#4179 := (pattern #48)
boehmes@36900
   184
#177 := (f22 #11)
boehmes@36900
   185
#1409 := (* -1::int #177)
boehmes@36900
   186
#1410 := (+ #155 #1409)
boehmes@36900
   187
#49 := (f4 #48)
boehmes@36900
   188
#1440 := (+ #49 #1410)
boehmes@36900
   189
#1438 := (>= #1440 0::int)
boehmes@36900
   190
#1137 := (* -1::int #49)
boehmes@36900
   191
decl f3 :: int
boehmes@36900
   192
#9 := f3
boehmes@36900
   193
#1140 := (+ f3 #1137)
boehmes@36900
   194
#1141 := (<= #1140 0::int)
boehmes@36900
   195
#3472 := (or #719 #1141 #1438)
boehmes@36900
   196
#4376 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4179) #3472)
boehmes@36900
   197
#4381 := (not #4376)
boehmes@36900
   198
decl f6 :: S2
boehmes@36900
   199
#23 := f6
boehmes@36900
   200
#2875 := (= f6 ?v0!20)
boehmes@36900
   201
#2307 := (+ f3 #2297)
boehmes@36900
   202
#2308 := (<= #2307 0::int)
boehmes@36900
   203
#4393 := (or #2308 #2875 #4381 #4390)
boehmes@36900
   204
#4396 := (not #4393)
boehmes@36900
   205
decl ?v0!19 :: S2
boehmes@36900
   206
#2265 := ?v0!19
boehmes@36900
   207
decl ?v1!18 :: S2
boehmes@36900
   208
#2264 := ?v1!18
boehmes@36900
   209
#2270 := (f5 ?v1!18 ?v0!19)
boehmes@36900
   210
#2271 := (f4 #2270)
boehmes@36900
   211
#2274 := (* -1::int #2271)
boehmes@36900
   212
#2268 := (f22 ?v1!18)
boehmes@36900
   213
#2861 := (* -1::int #2268)
boehmes@36900
   214
#2862 := (+ #2861 #2274)
boehmes@36900
   215
#2266 := (f22 ?v0!19)
boehmes@36900
   216
#2863 := (+ #2266 #2862)
boehmes@36900
   217
#2864 := (<= #2863 0::int)
boehmes@36900
   218
#2278 := (f11 f20 ?v1!18)
boehmes@36900
   219
#2279 := (= f1 #2278)
boehmes@36900
   220
#3435 := (not #2279)
boehmes@36900
   221
#2275 := (+ f3 #2274)
boehmes@36900
   222
#2276 := (<= #2275 0::int)
boehmes@36900
   223
#3450 := (or #2276 #3435 #2864)
boehmes@36900
   224
#3455 := (not #3450)
boehmes@36900
   225
#4399 := (or #3455 #4396)
boehmes@36900
   226
#4402 := (not #4399)
boehmes@36900
   227
#4367 := (pattern #155 #177)
boehmes@36900
   228
#1408 := (>= #1410 0::int)
boehmes@36900
   229
#174 := (f11 f20 #11)
boehmes@36900
   230
#733 := (= f1 #174)
boehmes@36900
   231
#3412 := (not #733)
boehmes@36900
   232
#3427 := (or #713 #3412 #1408)
boehmes@36900
   233
#4368 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4367) #3427)
boehmes@36900
   234
#4373 := (not #4368)
boehmes@36900
   235
#4405 := (or #4373 #4402)
boehmes@36900
   236
#4408 := (not #4405)
boehmes@36900
   237
decl ?v1!16 :: S2
boehmes@36900
   238
#2237 := ?v1!16
boehmes@36900
   239
#2241 := (f22 ?v1!16)
boehmes@36900
   240
#2835 := (* -1::int #2241)
boehmes@36900
   241
decl ?v0!17 :: S2
boehmes@36900
   242
#2238 := ?v0!17
boehmes@36900
   243
#2239 := (f22 ?v0!17)
boehmes@36900
   244
#2836 := (+ #2239 #2835)
boehmes@36900
   245
#2837 := (<= #2836 0::int)
boehmes@36900
   246
#2246 := (f11 f20 ?v1!16)
boehmes@36900
   247
#2247 := (= f1 #2246)
boehmes@36900
   248
#2244 := (f11 f20 ?v0!17)
boehmes@36900
   249
#2245 := (= f1 #2244)
boehmes@36900
   250
#3389 := (not #2245)
boehmes@36900
   251
#3404 := (or #3389 #2247 #2837)
boehmes@36900
   252
#3409 := (not #3404)
boehmes@36900
   253
#4411 := (or #3409 #4408)
boehmes@36900
   254
#4414 := (not #4411)
boehmes@36900
   255
#1399 := (>= #155 0::int)
boehmes@36900
   256
#4359 := (forall (vars (?v0 S2)) (:pat #4324) #1399)
boehmes@36900
   257
#4364 := (not #4359)
boehmes@36900
   258
#4417 := (or #4364 #4414)
boehmes@36900
   259
#4420 := (not #4417)
boehmes@36900
   260
decl ?v0!15 :: S2
boehmes@36900
   261
#2222 := ?v0!15
boehmes@36900
   262
#2223 := (f22 ?v0!15)
boehmes@36900
   263
#2224 := (>= #2223 0::int)
boehmes@36900
   264
#2225 := (not #2224)
boehmes@36900
   265
#4423 := (or #2225 #4420)
boehmes@36900
   266
#4426 := (not #4423)
boehmes@36900
   267
#169 := (f22 f6)
boehmes@36900
   268
#170 := (= #169 0::int)
boehmes@36900
   269
#1396 := (not #170)
boehmes@36900
   270
#4429 := (or #1396 #4426)
boehmes@36900
   271
#4432 := (not #4429)
boehmes@36900
   272
#4435 := (or #1396 #4432)
boehmes@36900
   273
#4438 := (not #4435)
boehmes@36900
   274
decl f9 :: (-> S4 S2 int)
boehmes@36900
   275
decl f10 :: S4
boehmes@36900
   276
#65 := f10
boehmes@36900
   277
#68 := (f9 f10 #12)
boehmes@36900
   278
#4203 := (pattern #68)
boehmes@36900
   279
#699 := (= #68 #155)
boehmes@36900
   280
#720 := (or #699 #719)
boehmes@36900
   281
#4351 := (forall (vars (?v0 S2)) (:pat #4203 #4324 #4350) #720)
boehmes@36900
   282
#4356 := (not #4351)
boehmes@36900
   283
#4441 := (or #4356 #4438)
boehmes@36900
   284
#4444 := (not #4441)
boehmes@36900
   285
decl ?v0!14 :: S2
boehmes@36900
   286
#2197 := ?v0!14
boehmes@36900
   287
#2202 := (f9 f10 ?v0!14)
boehmes@36900
   288
#2201 := (f22 ?v0!14)
boehmes@36900
   289
#2807 := (= #2201 #2202)
boehmes@36900
   290
#2198 := (f11 f20 ?v0!14)
boehmes@36900
   291
#2199 := (= f1 #2198)
boehmes@36900
   292
#2200 := (not #2199)
boehmes@36900
   293
#2813 := (or #2200 #2807)
boehmes@36900
   294
#2818 := (not #2813)
boehmes@36900
   295
#4447 := (or #2818 #4444)
boehmes@36900
   296
#4450 := (not #4447)
boehmes@36900
   297
#1384 := (* -1::int #155)
boehmes@36900
   298
#1385 := (+ #68 #1384)
boehmes@36900
   299
#1383 := (>= #1385 0::int)
boehmes@36900
   300
#4342 := (forall (vars (?v0 S2)) (:pat #4203 #4324) #1383)
boehmes@36900
   301
#4347 := (not #4342)
boehmes@36900
   302
#4453 := (or #4347 #4450)
boehmes@36900
   303
#4456 := (not #4453)
boehmes@36900
   304
decl ?v0!13 :: S2
boehmes@36900
   305
#2179 := ?v0!13
boehmes@36900
   306
#2182 := (f9 f10 ?v0!13)
boehmes@36900
   307
#2797 := (* -1::int #2182)
boehmes@36900
   308
#2180 := (f22 ?v0!13)
boehmes@36900
   309
#2798 := (+ #2180 #2797)
boehmes@36900
   310
#2799 := (<= #2798 0::int)
boehmes@36900
   311
#2804 := (not #2799)
boehmes@36900
   312
#4459 := (or #2804 #4456)
boehmes@36900
   313
#4462 := (not #4459)
boehmes@36900
   314
#149 := (f5 f19 #12)
boehmes@36900
   315
#4325 := (pattern #149)
boehmes@36900
   316
#150 := (f4 #149)
boehmes@36900
   317
#1527 := (+ #150 #1384)
boehmes@36900
   318
#141 := (f9 f10 f19)
boehmes@36900
   319
#1528 := (+ #141 #1527)
boehmes@36900
   320
#1529 := (= #1528 0::int)
boehmes@36900
   321
#1353 := (* -1::int #150)
boehmes@36900
   322
#1359 := (* -1::int #141)
boehmes@36900
   323
#1360 := (+ #1359 #1353)
boehmes@36900
   324
#1361 := (+ #68 #1360)
boehmes@36900
   325
#1362 := (<= #1361 0::int)
boehmes@36900
   326
#1354 := (+ f3 #1353)
boehmes@36900
   327
#1355 := (<= #1354 0::int)
boehmes@36900
   328
#3381 := (or #1355 #1362 #1529)
boehmes@36900
   329
#4334 := (forall (vars (?v0 S2)) (:pat #4325 #4203 #4324) #3381)
boehmes@36900
   330
#4339 := (not #4334)
boehmes@36900
   331
#3361 := (or #1355 #1362)
boehmes@36900
   332
#3362 := (not #3361)
boehmes@36900
   333
#3365 := (or #699 #3362)
boehmes@36900
   334
#4326 := (forall (vars (?v0 S2)) (:pat #4203 #4324 #4325) #3365)
boehmes@36900
   335
#4331 := (not #4326)
boehmes@36900
   336
decl ?v0!12 :: S2
boehmes@36900
   337
#2155 := ?v0!12
boehmes@36900
   338
#2161 := (f11 f12 ?v0!12)
boehmes@36900
   339
#2162 := (= f1 #2161)
boehmes@36900
   340
#2156 := (f9 f10 ?v0!12)
boehmes@36900
   341
#2157 := (* -1::int #2156)
boehmes@36900
   342
#2158 := (+ f3 #2157)
boehmes@34994
   343
#2159 := (<= #2158 0::int)
boehmes@36900
   344
#1559 := (+ f3 #1359)
boehmes@36900
   345
#1560 := (<= #1559 0::int)
boehmes@36900
   346
#72 := (f11 f12 #12)
boehmes@36900
   347
#4245 := (pattern #72)
boehmes@36900
   348
#1542 := (+ #68 #1359)
boehmes@36900
   349
#1541 := (>= #1542 0::int)
boehmes@36900
   350
#447 := (= f1 #72)
boehmes@36900
   351
#1548 := (or #447 #1541)
boehmes@36900
   352
#4316 := (forall (vars (?v0 S2)) (:pat #4245 #4203) #1548)
boehmes@36900
   353
#4321 := (not #4316)
boehmes@36900
   354
#138 := (f11 f12 f19)
boehmes@36900
   355
#668 := (= f1 #138)
boehmes@36900
   356
#901 := (not #148)
boehmes@36900
   357
#4465 := (or #901 #668 #4321 #1560 #2159 #2162 #4331 #4339 #4462)
boehmes@36900
   358
#4468 := (not #4465)
boehmes@36900
   359
decl ?v0!11 :: S2
boehmes@36900
   360
#2089 := ?v0!11
boehmes@36900
   361
decl ?v1!10 :: S2
boehmes@36900
   362
#2088 := ?v1!10
boehmes@36900
   363
#2094 := (f5 ?v1!10 ?v0!11)
boehmes@36900
   364
#2095 := (f4 #2094)
boehmes@36900
   365
#2102 := (* -1::int #2095)
boehmes@36900
   366
decl f16 :: S4
boehmes@36900
   367
#104 := f16
boehmes@36900
   368
#2092 := (f9 f16 ?v1!10)
boehmes@36900
   369
#2098 := (* -1::int #2092)
boehmes@36900
   370
#2754 := (+ #2098 #2102)
boehmes@36900
   371
#2090 := (f9 f16 ?v0!11)
boehmes@36900
   372
#2755 := (+ #2090 #2754)
boehmes@36900
   373
#2756 := (<= #2755 0::int)
boehmes@36900
   374
#2103 := (+ f3 #2102)
boehmes@36900
   375
#2104 := (<= #2103 0::int)
boehmes@36900
   376
#2099 := (+ f3 #2098)
boehmes@36900
   377
#2100 := (<= #2099 0::int)
boehmes@36900
   378
#3325 := (or #2100 #2104 #2756)
boehmes@36900
   379
#3330 := (not #3325)
boehmes@36900
   380
#112 := (f9 f16 #11)
boehmes@36900
   381
#1261 := (* -1::int #112)
boehmes@36900
   382
#109 := (f9 f16 #12)
boehmes@36900
   383
#1262 := (+ #109 #1261)
boehmes@36900
   384
#1268 := (+ #49 #1262)
boehmes@36900
   385
#1291 := (>= #1268 0::int)
boehmes@36900
   386
#1248 := (* -1::int #109)
boehmes@36900
   387
#1249 := (+ f3 #1248)
boehmes@36900
   388
#1250 := (<= #1249 0::int)
boehmes@36900
   389
#3293 := (or #1141 #1250 #1291)
boehmes@36900
   390
#4278 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4179) #3293)
boehmes@36900
   391
#4283 := (not #4278)
boehmes@36900
   392
#124 := (f9 f16 f6)
boehmes@36900
   393
#125 := (= #124 0::int)
boehmes@36900
   394
#4286 := (or #125 #4283)
boehmes@34994
   395
#4289 := (not #4286)
boehmes@36900
   396
#4292 := (or #4289 #3330)
boehmes@34994
   397
#4295 := (not #4292)
boehmes@36900
   398
#4254 := (pattern #109)
boehmes@36900
   399
decl ?v1!9 :: (-> S2 S2)
boehmes@36900
   400
#2065 := (?v1!9 #12)
boehmes@36900
   401
#2068 := (f5 #2065 #12)
boehmes@36900
   402
#2069 := (f4 #2068)
boehmes@36900
   403
#2724 := (* -1::int #2069)
boehmes@36900
   404
#2066 := (f9 f16 #2065)
boehmes@36900
   405
#2707 := (* -1::int #2066)
boehmes@36900
   406
#2725 := (+ #2707 #2724)
boehmes@36900
   407
#2726 := (+ #109 #2725)
boehmes@36900
   408
#2727 := (= #2726 0::int)
boehmes@36900
   409
#3263 := (not #2727)
boehmes@36900
   410
#2708 := (+ #109 #2707)
boehmes@36900
   411
#2709 := (<= #2708 0::int)
boehmes@36900
   412
#3264 := (or #2709 #3263)
boehmes@36900
   413
#3265 := (not #3264)
boehmes@36900
   414
#24 := (= #12 f6)
boehmes@36900
   415
#3271 := (or #24 #1250 #3265)
boehmes@36900
   416
#4270 := (forall (vars (?v0 S2)) (:pat #4254) #3271)
boehmes@36900
   417
#4275 := (not #4270)
boehmes@36900
   418
#4298 := (or #4275 #4295)
boehmes@34994
   419
#4301 := (not #4298)
boehmes@36900
   420
decl ?v0!8 :: S2
boehmes@36900
   421
#2025 := ?v0!8
boehmes@36900
   422
#2029 := (f5 #12 ?v0!8)
boehmes@36900
   423
#4255 := (pattern #2029)
boehmes@36900
   424
#2030 := (f4 #2029)
boehmes@36900
   425
#2026 := (f9 f16 ?v0!8)
boehmes@36900
   426
#2027 := (* -1::int #2026)
boehmes@36900
   427
#2677 := (+ #2027 #2030)
boehmes@36900
   428
#2678 := (+ #109 #2677)
boehmes@36900
   429
#2681 := (= #2678 0::int)
boehmes@36900
   430
#3227 := (not #2681)
boehmes@36900
   431
#2028 := (+ #109 #2027)
boehmes@36900
   432
#2033 := (>= #2028 0::int)
boehmes@36900
   433
#3228 := (or #2033 #3227)
boehmes@36900
   434
#4256 := (forall (vars (?v1 S2)) (:pat #4254 #4255) #3228)
boehmes@36900
   435
#4261 := (not #4256)
boehmes@36900
   436
#2653 := (= f6 ?v0!8)
boehmes@36900
   437
#2037 := (+ f3 #2027)
boehmes@36900
   438
#2038 := (<= #2037 0::int)
boehmes@36900
   439
#4264 := (or #2038 #2653 #4261)
boehmes@36900
   440
#4267 := (not #4264)
boehmes@36900
   441
#4304 := (or #4267 #4301)
boehmes@34994
   442
#4307 := (not #4304)
boehmes@36900
   443
#1203 := (* -1::int #68)
boehmes@36900
   444
#1204 := (+ f3 #1203)
boehmes@36900
   445
#1205 := (<= #1204 0::int)
boehmes@36900
   446
#3213 := (or #447 #1205)
boehmes@36900
   447
#4246 := (forall (vars (?v0 S2)) (:pat #4245 #4203) #3213)
boehmes@36900
   448
#4251 := (not #4246)
boehmes@36900
   449
#538 := (= f10 f16)
boehmes@36900
   450
#629 := (not #538)
boehmes@36900
   451
decl f13 :: S5
boehmes@36900
   452
#99 := f13
boehmes@36900
   453
#535 := (= f12 f13)
boehmes@36900
   454
#647 := (not #535)
boehmes@36900
   455
decl f18 :: S4
boehmes@36900
   456
#107 := f18
boehmes@36900
   457
decl f17 :: S4
boehmes@36900
   458
#106 := f17
boehmes@36900
   459
#108 := (= f17 f18)
boehmes@36900
   460
#620 := (not #108)
boehmes@36900
   461
decl f15 :: S2
boehmes@36900
   462
#102 := f15
boehmes@36900
   463
decl f14 :: S2
boehmes@36900
   464
#101 := f14
boehmes@36900
   465
#103 := (= f14 f15)
boehmes@36900
   466
#638 := (not #103)
boehmes@36900
   467
#4310 := (or #638 #620 #647 #629 #4251 #4307)
boehmes@34994
   468
#4313 := (not #4310)
boehmes@36900
   469
#4471 := (or #4313 #4468)
boehmes@36900
   470
#4474 := (not #4471)
boehmes@36900
   471
#1988 := (?v1!7 #12)
boehmes@36900
   472
#1989 := (f9 f10 #1988)
boehmes@36900
   473
#2612 := (* -1::int #1989)
boehmes@36900
   474
#2627 := (+ #68 #2612)
boehmes@36900
   475
#2628 := (<= #2627 0::int)
boehmes@36900
   476
#1993 := (f5 #1988 #12)
boehmes@36900
   477
#1994 := (f4 #1993)
boehmes@36900
   478
#2613 := (* -1::int #1994)
boehmes@36900
   479
#2614 := (+ #2612 #2613)
boehmes@36900
   480
#2615 := (+ #68 #2614)
boehmes@36900
   481
#2616 := (= #2615 0::int)
boehmes@36900
   482
#3197 := (not #2616)
boehmes@36900
   483
#1997 := (f11 f12 #1988)
boehmes@36900
   484
#1998 := (= f1 #1997)
boehmes@36900
   485
#3196 := (not #1998)
boehmes@36900
   486
#3198 := (or #3196 #3197 #2628)
boehmes@36900
   487
#3199 := (not #3198)
boehmes@36900
   488
#3205 := (or #24 #1205 #3199)
boehmes@36900
   489
#4237 := (forall (vars (?v0 S2)) (:pat #4203) #3205)
boehmes@36900
   490
#4242 := (not #4237)
boehmes@36900
   491
decl f7 :: (-> S2 int)
boehmes@36900
   492
#25 := (f7 #12)
boehmes@36900
   493
#4148 := (pattern #25)
boehmes@36900
   494
decl ?v1!6 :: (-> S2 S2)
boehmes@36900
   495
#1960 := (?v1!6 #12)
boehmes@36900
   496
#1964 := (f7 #1960)
boehmes@36900
   497
#2571 := (* -1::int #1964)
boehmes@36900
   498
#1961 := (f5 #1960 #12)
boehmes@36900
   499
#1962 := (f4 #1961)
boehmes@36900
   500
#2588 := (* -1::int #1962)
boehmes@36900
   501
#2589 := (+ #2588 #2571)
boehmes@36900
   502
#2590 := (+ #25 #2589)
boehmes@36900
   503
#2591 := (= #2590 0::int)
boehmes@36900
   504
#3169 := (not #2591)
boehmes@36900
   505
#2572 := (+ #25 #2571)
boehmes@36900
   506
#2573 := (<= #2572 0::int)
boehmes@36900
   507
decl f8 :: (-> S2 S1)
boehmes@36900
   508
#1970 := (f8 #1960)
boehmes@36900
   509
#1971 := (= f1 #1970)
boehmes@36900
   510
#3168 := (not #1971)
boehmes@36900
   511
#3170 := (or #3168 #2573 #3169)
boehmes@36900
   512
#3171 := (not #3170)
boehmes@36900
   513
#1165 := (* -1::int #25)
boehmes@36900
   514
#1166 := (+ f3 #1165)
boehmes@36900
   515
#1167 := (<= #1166 0::int)
boehmes@36900
   516
#3177 := (or #24 #1167 #3171)
boehmes@36900
   517
#4229 := (forall (vars (?v0 S2)) (:pat #4148) #3177)
boehmes@34994
   518
#4234 := (not #4229)
boehmes@36900
   519
#75 := (f11 f12 #11)
boehmes@36900
   520
#4220 := (pattern #72 #75)
boehmes@36900
   521
#78 := (f9 f10 #11)
boehmes@36900
   522
#1217 := (* -1::int #78)
boehmes@36900
   523
#1218 := (+ #68 #1217)
boehmes@36900
   524
#1221 := (>= #1218 0::int)
boehmes@36900
   525
#453 := (= f1 #75)
boehmes@36900
   526
#3134 := (not #453)
boehmes@36900
   527
#3149 := (or #447 #3134 #1221)
boehmes@36900
   528
#4221 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4220) #3149)
boehmes@34994
   529
#4226 := (not #4221)
boehmes@36900
   530
#1219 := (+ #49 #1218)
boehmes@36900
   531
#1614 := (>= #1219 0::int)
boehmes@36900
   532
#450 := (not #447)
boehmes@36900
   533
#3126 := (or #450 #1141 #1614)
boehmes@36900
   534
#4212 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4179) #3126)
boehmes@36900
   535
#4217 := (not #4212)
boehmes@36900
   536
#1642 := (>= #68 0::int)
boehmes@36900
   537
#4204 := (forall (vars (?v0 S2)) (:pat #4203) #1642)
boehmes@36900
   538
#4209 := (not #4204)
boehmes@36900
   539
#66 := (f9 f10 f6)
boehmes@34994
   540
#67 := (= #66 0::int)
boehmes@36900
   541
#1653 := (not #67)
boehmes@36900
   542
#4477 := (or #1653 #4209 #4217 #4226 #4234 #4242 #4474)
boehmes@36900
   543
#4480 := (not #4477)
boehmes@36900
   544
decl ?v0!5 :: S2
boehmes@36900
   545
#1916 := ?v0!5
boehmes@36900
   546
#1917 := (f5 #12 ?v0!5)
boehmes@36900
   547
#4188 := (pattern #1917)
boehmes@36900
   548
#33 := (f8 #12)
boehmes@36900
   549
#4155 := (pattern #33)
boehmes@36900
   550
#1919 := (f7 ?v0!5)
boehmes@36900
   551
#1920 := (* -1::int #1919)
boehmes@36900
   552
#1918 := (f4 #1917)
boehmes@36900
   553
#2539 := (+ #1918 #1920)
boehmes@36900
   554
#2540 := (+ #25 #2539)
boehmes@36900
   555
#2543 := (= #2540 0::int)
boehmes@36900
   556
#3087 := (not #2543)
boehmes@36900
   557
#1924 := (+ #25 #1920)
boehmes@36900
   558
#1925 := (>= #1924 0::int)
boehmes@36900
   559
#368 := (= f1 #33)
boehmes@36900
   560
#371 := (not #368)
boehmes@36900
   561
#3088 := (or #371 #1925 #3087)
boehmes@36900
   562
#4189 := (forall (vars (?v1 S2)) (:pat #4155 #4148 #4188) #3088)
boehmes@36900
   563
#4194 := (not #4189)
boehmes@36900
   564
#2515 := (= f6 ?v0!5)
boehmes@36900
   565
#1929 := (+ f3 #1920)
boehmes@36900
   566
#1930 := (<= #1929 0::int)
boehmes@36900
   567
#4197 := (or #1930 #2515 #4194)
boehmes@36900
   568
#4200 := (not #4197)
boehmes@36900
   569
#4483 := (or #4200 #4480)
boehmes@36900
   570
#4486 := (not #4483)
boehmes@36900
   571
#44 := (f7 #11)
boehmes@36900
   572
#1117 := (* -1::int #44)
boehmes@36900
   573
#1138 := (+ #1117 #49)
boehmes@36900
   574
#1139 := (+ #25 #1138)
boehmes@36900
   575
#1136 := (>= #1139 0::int)
boehmes@36900
   576
#3079 := (or #371 #1136 #1141)
boehmes@36900
   577
#4180 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4179) #3079)
boehmes@36900
   578
#4185 := (not #4180)
boehmes@36900
   579
#4489 := (or #4185 #4486)
boehmes@36900
   580
#4492 := (not #4489)
boehmes@36900
   581
decl ?v1!3 :: S2
boehmes@36900
   582
#1885 := ?v1!3
boehmes@36900
   583
#1900 := (f7 ?v1!3)
boehmes@36900
   584
decl ?v0!4 :: S2
boehmes@36900
   585
#1886 := ?v0!4
boehmes@36900
   586
#1897 := (f7 ?v0!4)
boehmes@36900
   587
#1898 := (* -1::int #1897)
boehmes@36900
   588
#2496 := (+ #1898 #1900)
boehmes@36900
   589
#1887 := (f5 ?v1!3 ?v0!4)
boehmes@36900
   590
#1888 := (f4 #1887)
boehmes@36900
   591
#2497 := (+ #1888 #2496)
boehmes@36900
   592
#2500 := (>= #2497 0::int)
boehmes@36900
   593
#1893 := (f8 ?v1!3)
boehmes@36900
   594
#1894 := (= f1 #1893)
boehmes@36900
   595
#3042 := (not #1894)
boehmes@36900
   596
#1889 := (* -1::int #1888)
boehmes@36900
   597
#1890 := (+ f3 #1889)
boehmes@36900
   598
#1891 := (<= #1890 0::int)
boehmes@36900
   599
#3057 := (or #1891 #3042 #2500)
boehmes@36900
   600
#3062 := (not #3057)
boehmes@36900
   601
#4495 := (or #3062 #4492)
boehmes@36900
   602
#4498 := (not #4495)
boehmes@36900
   603
#41 := (f8 #11)
boehmes@36900
   604
#4170 := (pattern #33 #41)
boehmes@36900
   605
#1118 := (+ #25 #1117)
boehmes@36900
   606
#1116 := (>= #1118 0::int)
boehmes@36900
   607
#380 := (= f1 #41)
boehmes@36900
   608
#3019 := (not #380)
boehmes@36900
   609
#3034 := (or #368 #3019 #1116)
boehmes@36900
   610
#4171 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #4170) #3034)
boehmes@36900
   611
#4176 := (not #4171)
boehmes@36900
   612
#4501 := (or #4176 #4498)
boehmes@36900
   613
#4504 := (not #4501)
boehmes@36900
   614
decl ?v1!1 :: S2
boehmes@36900
   615
#1858 := ?v1!1
boehmes@36900
   616
#1862 := (f7 ?v1!1)
boehmes@36900
   617
#2483 := (* -1::int #1862)
boehmes@36900
   618
decl ?v0!2 :: S2
boehmes@36900
   619
#1859 := ?v0!2
boehmes@36900
   620
#1860 := (f7 ?v0!2)
boehmes@36900
   621
#2484 := (+ #1860 #2483)
boehmes@36900
   622
#2485 := (<= #2484 0::int)
boehmes@36900
   623
#1867 := (f8 ?v1!1)
boehmes@36900
   624
#1868 := (= f1 #1867)
boehmes@36900
   625
#1865 := (f8 ?v0!2)
boehmes@36900
   626
#1866 := (= f1 #1865)
boehmes@36900
   627
#2112 := (not #1866)
boehmes@36900
   628
#3011 := (or #2112 #1868 #2485)
boehmes@36900
   629
#3016 := (not #3011)
boehmes@36900
   630
#4507 := (or #3016 #4504)
boehmes@36900
   631
#4510 := (not #4507)
boehmes@36900
   632
#1107 := (>= #25 0::int)
boehmes@36900
   633
#4162 := (forall (vars (?v0 S2)) (:pat #4148) #1107)
boehmes@36900
   634
#4167 := (not #4162)
boehmes@36900
   635
#4513 := (or #4167 #4510)
boehmes@36900
   636
#4516 := (not #4513)
boehmes@36900
   637
decl ?v0!0 :: S2
boehmes@36900
   638
#1843 := ?v0!0
boehmes@36900
   639
#1844 := (f7 ?v0!0)
boehmes@36900
   640
#1845 := (>= #1844 0::int)
boehmes@36900
   641
#1846 := (not #1845)
boehmes@36900
   642
#4519 := (or #1846 #4516)
boehmes@36900
   643
#4522 := (not #4519)
boehmes@36900
   644
#37 := (f7 f6)
boehmes@36900
   645
#38 := (= #37 0::int)
boehmes@36900
   646
#1102 := (not #38)
boehmes@36900
   647
#4525 := (or #1102 #4522)
boehmes@36900
   648
#4528 := (not #4525)
boehmes@36900
   649
#26 := (= #25 0::int)
boehmes@36900
   650
#29 := (not #24)
boehmes@36900
   651
#1711 := (or #29 #26)
boehmes@36900
   652
#4535 := (forall (vars (?v0 S2)) (:pat #4148) #1711)
boehmes@36900
   653
#1714 := (forall (vars (?v0 S2)) #1711)
boehmes@36900
   654
#4538 := (iff #1714 #4535)
boehmes@36900
   655
#4536 := (iff #1711 #1711)
boehmes@36900
   656
#4537 := [refl]: #4536
boehmes@36900
   657
#4539 := [quant-intro #4537]: #4538
boehmes@36900
   658
#2167 := (~ #1714 #1714)
boehmes@36900
   659
#2286 := (~ #1711 #1711)
boehmes@36900
   660
#2287 := [refl]: #2286
boehmes@36900
   661
#2168 := [nnf-pos #2287]: #2167
boehmes@36900
   662
#1717 := (not #1714)
boehmes@36900
   663
#1645 := (forall (vars (?v0 S2)) #1642)
boehmes@36900
   664
#1648 := (not #1645)
boehmes@36900
   665
#456 := (and #450 #453)
boehmes@36900
   666
#462 := (not #456)
boehmes@36900
   667
#1631 := (or #462 #1221)
boehmes@36900
   668
#1636 := (forall (vars (?v0 S2) (?v1 S2)) #1631)
boehmes@36900
   669
#1639 := (not #1636)
boehmes@36900
   670
#1142 := (not #1141)
boehmes@36900
   671
#1606 := (and #447 #1142)
boehmes@36900
   672
#1611 := (not #1606)
boehmes@36900
   673
#1617 := (or #1611 #1614)
boehmes@36900
   674
#1620 := (forall (vars (?v0 S2) (?v1 S2)) #1617)
boehmes@36900
   675
#1623 := (not #1620)
boehmes@36900
   676
#1553 := (forall (vars (?v0 S2)) #1548)
boehmes@36900
   677
#1556 := (not #1553)
boehmes@36900
   678
#1363 := (not #1362)
boehmes@36900
   679
#1356 := (not #1355)
boehmes@36900
   680
#1366 := (and #1356 #1363)
boehmes@36900
   681
#1524 := (not #1366)
boehmes@36900
   682
#1532 := (or #1524 #1529)
boehmes@36900
   683
#1535 := (forall (vars (?v0 S2)) #1532)
boehmes@36900
   684
#1538 := (not #1535)
boehmes@36900
   685
#1462 := (= #1440 0::int)
boehmes@36900
   686
#1465 := (not #1408)
boehmes@36900
   687
#1474 := (and #713 #1465 #1462)
boehmes@36900
   688
#1479 := (exists (vars (?v1 S2)) #1474)
boehmes@36900
   689
#1451 := (+ f3 #1384)
boehmes@36900
   690
#1452 := (<= #1451 0::int)
boehmes@36900
   691
#1453 := (not #1452)
boehmes@36900
   692
#1456 := (and #29 #1453)
boehmes@36900
   693
#1459 := (not #1456)
boehmes@36900
   694
#1482 := (or #1459 #1479)
boehmes@36900
   695
#1485 := (forall (vars (?v0 S2)) #1482)
boehmes@36900
   696
#1430 := (and #713 #1142)
boehmes@36900
   697
#1435 := (not #1430)
boehmes@36900
   698
#1442 := (or #1435 #1438)
boehmes@36900
   699
#1445 := (forall (vars (?v0 S2) (?v1 S2)) #1442)
boehmes@36900
   700
#1448 := (not #1445)
boehmes@36900
   701
#1488 := (or #1448 #1485)
boehmes@36900
   702
#1491 := (and #1445 #1488)
boehmes@36900
   703
#736 := (and #719 #733)
boehmes@36900
   704
#742 := (not #736)
boehmes@36900
   705
#1416 := (or #742 #1408)
boehmes@36900
   706
#1421 := (forall (vars (?v0 S2) (?v1 S2)) #1416)
boehmes@36900
   707
#1424 := (not #1421)
boehmes@36900
   708
#1494 := (or #1424 #1491)
boehmes@36900
   709
#1497 := (and #1421 #1494)
boehmes@36900
   710
#1402 := (forall (vars (?v0 S2)) #1399)
boehmes@36900
   711
#1405 := (not #1402)
boehmes@36900
   712
#1500 := (or #1405 #1497)
boehmes@36900
   713
#1503 := (and #1402 #1500)
boehmes@36900
   714
#1506 := (or #1396 #1503)
boehmes@36900
   715
#1509 := (and #170 #1506)
boehmes@36900
   716
#725 := (forall (vars (?v0 S2)) #720)
boehmes@36900
   717
#859 := (not #725)
boehmes@36900
   718
#1512 := (or #859 #1509)
boehmes@36900
   719
#1515 := (and #725 #1512)
boehmes@36900
   720
#1388 := (forall (vars (?v0 S2)) #1383)
boehmes@36900
   721
#1391 := (not #1388)
boehmes@36900
   722
#1518 := (or #1391 #1515)
boehmes@36900
   723
#1521 := (and #1388 #1518)
boehmes@36900
   724
#1372 := (or #699 #1366)
boehmes@36900
   725
#1377 := (forall (vars (?v0 S2)) #1372)
boehmes@36900
   726
#1380 := (not #1377)
boehmes@36900
   727
#1206 := (not #1205)
boehmes@36900
   728
#1325 := (and #450 #1206)
boehmes@36900
   729
#1330 := (exists (vars (?v0 S2)) #1325)
boehmes@36900
   730
#1571 := (not #1330)
boehmes@36900
   731
#1595 := (or #901 #668 #1571 #1380 #1521 #1538 #1556 #1560)
boehmes@36900
   732
#1251 := (not #1250)
boehmes@36900
   733
#1285 := (and #1142 #1251)
boehmes@36900
   734
#1288 := (not #1285)
boehmes@36900
   735
#1294 := (or #1288 #1291)
boehmes@36900
   736
#1297 := (forall (vars (?v0 S2) (?v1 S2)) #1294)
boehmes@34994
   737
#1300 := (not #1297)
boehmes@36900
   738
#1308 := (or #125 #1300)
boehmes@36900
   739
#1313 := (and #1297 #1308)
boehmes@36900
   740
#1266 := (= #1268 0::int)
boehmes@36900
   741
#1260 := (>= #1262 0::int)
boehmes@36900
   742
#1263 := (not #1260)
boehmes@36900
   743
#1270 := (and #1263 #1266)
boehmes@36900
   744
#1273 := (exists (vars (?v1 S2)) #1270)
boehmes@36900
   745
#1254 := (and #29 #1251)
boehmes@36900
   746
#1257 := (not #1254)
boehmes@36900
   747
#1276 := (or #1257 #1273)
boehmes@36900
   748
#1279 := (forall (vars (?v0 S2)) #1276)
boehmes@36900
   749
#1282 := (not #1279)
boehmes@36900
   750
#1316 := (or #1282 #1313)
boehmes@36900
   751
#1319 := (and #1279 #1316)
boehmes@36900
   752
#1348 := (or #638 #620 #647 #629 #1319 #1330)
boehmes@36900
   753
#1600 := (and #1348 #1595)
boehmes@36900
   754
#1222 := (not #1221)
boehmes@36900
   755
#1215 := (= #1219 0::int)
boehmes@36900
   756
#1231 := (and #447 #1215 #1222)
boehmes@36900
   757
#1236 := (exists (vars (?v1 S2)) #1231)
boehmes@36900
   758
#1209 := (and #29 #1206)
boehmes@36900
   759
#1212 := (not #1209)
boehmes@36900
   760
#1239 := (or #1212 #1236)
boehmes@36900
   761
#1242 := (forall (vars (?v0 S2)) #1239)
boehmes@36900
   762
#1245 := (not #1242)
boehmes@36900
   763
#1177 := (= #1139 0::int)
boehmes@36900
   764
#1180 := (not #1116)
boehmes@36900
   765
#1189 := (and #368 #1180 #1177)
boehmes@36900
   766
#1194 := (exists (vars (?v1 S2)) #1189)
boehmes@36900
   767
#1168 := (not #1167)
boehmes@36900
   768
#1171 := (and #29 #1168)
boehmes@36900
   769
#1174 := (not #1171)
boehmes@36900
   770
#1197 := (or #1174 #1194)
boehmes@36900
   771
#1200 := (forall (vars (?v0 S2)) #1197)
boehmes@36900
   772
#1656 := (not #1200)
boehmes@36900
   773
#1677 := (or #1653 #1656 #1245 #1600 #1623 #1639 #1648)
boehmes@36900
   774
#1682 := (and #1200 #1677)
boehmes@36900
   775
#1148 := (and #368 #1142)
boehmes@36900
   776
#1153 := (not #1148)
boehmes@36900
   777
#1156 := (or #1136 #1153)
boehmes@36900
   778
#1159 := (forall (vars (?v0 S2) (?v1 S2)) #1156)
boehmes@36900
   779
#1162 := (not #1159)
boehmes@36900
   780
#1685 := (or #1162 #1682)
boehmes@36900
   781
#1688 := (and #1159 #1685)
boehmes@36900
   782
#383 := (and #371 #380)
boehmes@36900
   783
#389 := (not #383)
boehmes@36900
   784
#1123 := (or #389 #1116)
boehmes@36900
   785
#1128 := (forall (vars (?v0 S2) (?v1 S2)) #1123)
boehmes@36900
   786
#1131 := (not #1128)
boehmes@36900
   787
#1691 := (or #1131 #1688)
boehmes@36900
   788
#1694 := (and #1128 #1691)
boehmes@36900
   789
#1108 := (forall (vars (?v0 S2)) #1107)
boehmes@36900
   790
#1111 := (not #1108)
boehmes@36900
   791
#1697 := (or #1111 #1694)
boehmes@36900
   792
#1700 := (and #1108 #1697)
boehmes@36900
   793
#1703 := (or #1102 #1700)
boehmes@36900
   794
#1706 := (and #38 #1703)
boehmes@36900
   795
#374 := (forall (vars (?v0 S2)) #371)
boehmes@36900
   796
#1066 := (not #374)
boehmes@36900
   797
#354 := (= f3 #25)
boehmes@36900
   798
#360 := (or #24 #354)
boehmes@36900
   799
#365 := (forall (vars (?v0 S2)) #360)
boehmes@36900
   800
#1075 := (not #365)
boehmes@36900
   801
#1729 := (or #1075 #1066 #1706 #1717)
boehmes@36900
   802
#1734 := (not #1729)
boehmes@36900
   803
#182 := (+ #155 #49)
boehmes@36900
   804
#189 := (= #177 #182)
boehmes@36900
   805
#166 := (= #165 f1)
boehmes@36900
   806
#190 := (and #166 #189)
boehmes@36900
   807
#188 := (< #155 #177)
boehmes@36900
   808
#191 := (and #188 #190)
boehmes@36900
   809
#192 := (exists (vars (?v1 S2)) #191)
boehmes@36900
   810
#186 := (< #155 f3)
boehmes@36900
   811
#187 := (and #29 #186)
boehmes@36900
   812
#193 := (implies #187 #192)
boehmes@36900
   813
#194 := (forall (vars (?v0 S2)) #193)
boehmes@36900
   814
#195 := (and #194 true)
boehmes@36900
   815
#183 := (<= #177 #182)
boehmes@36900
   816
#50 := (< #49 f3)
boehmes@36900
   817
#181 := (and #166 #50)
boehmes@36900
   818
#184 := (implies #181 #183)
boehmes@36900
   819
#185 := (forall (vars (?v0 S2) (?v1 S2)) #184)
boehmes@36900
   820
#196 := (implies #185 #195)
boehmes@36900
   821
#197 := (and #185 #196)
boehmes@36900
   822
#178 := (<= #177 #155)
boehmes@36900
   823
#175 := (= #174 f1)
boehmes@36900
   824
#173 := (not #166)
boehmes@36900
   825
#176 := (and #173 #175)
boehmes@36900
   826
#179 := (implies #176 #178)
boehmes@36900
   827
#180 := (forall (vars (?v0 S2) (?v1 S2)) #179)
boehmes@36900
   828
#198 := (implies #180 #197)
boehmes@36900
   829
#199 := (and #180 #198)
boehmes@36900
   830
#171 := (<= 0::int #155)
boehmes@36900
   831
#172 := (forall (vars (?v0 S2)) #171)
boehmes@36900
   832
#200 := (implies #172 #199)
boehmes@36900
   833
#201 := (and #172 #200)
boehmes@36900
   834
#202 := (implies #170 #201)
boehmes@36900
   835
#203 := (and #170 #202)
boehmes@36900
   836
#160 := (= #155 #68)
boehmes@36900
   837
#167 := (implies #166 #160)
boehmes@36900
   838
#168 := (forall (vars (?v0 S2)) #167)
boehmes@36900
   839
#204 := (implies #168 #203)
boehmes@36900
   840
#205 := (and #168 #204)
boehmes@36900
   841
#163 := (<= #155 #68)
boehmes@36900
   842
#164 := (forall (vars (?v0 S2)) #163)
boehmes@36900
   843
#206 := (implies #164 #205)
boehmes@36900
   844
#207 := (and #164 #206)
boehmes@36900
   845
#152 := (+ #141 #150)
boehmes@36900
   846
#153 := (< #152 #68)
boehmes@36900
   847
#151 := (< #150 f3)
boehmes@36900
   848
#154 := (and #151 #153)
boehmes@36900
   849
#159 := (not #154)
boehmes@36900
   850
#161 := (implies #159 #160)
boehmes@36900
   851
#162 := (forall (vars (?v0 S2)) #161)
boehmes@36900
   852
#208 := (implies #162 #207)
boehmes@36900
   853
#156 := (= #155 #152)
boehmes@36900
   854
#157 := (implies #154 #156)
boehmes@36900
   855
#158 := (forall (vars (?v0 S2)) #157)
boehmes@36900
   856
#209 := (implies #158 #208)
boehmes@36900
   857
#210 := (implies #148 #209)
boehmes@36900
   858
#143 := (<= #141 #68)
boehmes@36900
   859
#73 := (= #72 f1)
boehmes@36900
   860
#74 := (not #73)
boehmes@36900
   861
#144 := (implies #74 #143)
boehmes@36900
   862
#145 := (forall (vars (?v0 S2)) #144)
boehmes@36900
   863
#211 := (implies #145 #210)
boehmes@36900
   864
#142 := (< #141 f3)
boehmes@36900
   865
#212 := (implies #142 #211)
boehmes@36900
   866
#139 := (= #138 f1)
boehmes@36900
   867
#140 := (not #139)
boehmes@36900
   868
#213 := (implies #140 #212)
boehmes@36900
   869
#87 := (< #68 f3)
boehmes@36900
   870
#96 := (and #74 #87)
boehmes@36900
   871
#97 := (exists (vars (?v0 S2)) #96)
boehmes@36900
   872
#214 := (implies #97 #213)
boehmes@36900
   873
#215 := (implies true #214)
boehmes@36900
   874
#126 := (and #125 true)
boehmes@36900
   875
#114 := (+ #109 #49)
boehmes@36900
   876
#121 := (<= #112 #114)
boehmes@36900
   877
#110 := (< #109 f3)
boehmes@36900
   878
#120 := (and #110 #50)
boehmes@36900
   879
#122 := (implies #120 #121)
boehmes@36900
   880
#123 := (forall (vars (?v0 S2) (?v1 S2)) #122)
boehmes@36900
   881
#127 := (implies #123 #126)
boehmes@36900
   882
#128 := (and #123 #127)
boehmes@36900
   883
#115 := (= #112 #114)
boehmes@36900
   884
#113 := (< #109 #112)
boehmes@36900
   885
#116 := (and #113 #115)
boehmes@36900
   886
#117 := (exists (vars (?v1 S2)) #116)
boehmes@36900
   887
#111 := (and #29 #110)
boehmes@36900
   888
#118 := (implies #111 #117)
boehmes@36900
   889
#119 := (forall (vars (?v0 S2)) #118)
boehmes@36900
   890
#129 := (implies #119 #128)
boehmes@36900
   891
#130 := (and #119 #129)
boehmes@36900
   892
#131 := (implies #108 #130)
boehmes@36900
   893
#105 := (= f16 f10)
boehmes@36900
   894
#132 := (implies #105 #131)
boehmes@36900
   895
#133 := (implies #103 #132)
boehmes@36900
   896
#100 := (= f13 f12)
boehmes@36900
   897
#134 := (implies #100 #133)
boehmes@36900
   898
#98 := (not #97)
boehmes@36900
   899
#135 := (implies #98 #134)
boehmes@36900
   900
#136 := (implies true #135)
boehmes@36900
   901
#216 := (and #136 #215)
boehmes@36900
   902
#83 := (+ #68 #49)
boehmes@36900
   903
#90 := (= #78 #83)
boehmes@36900
   904
#91 := (and #73 #90)
boehmes@36900
   905
#89 := (< #68 #78)
boehmes@36900
   906
#92 := (and #89 #91)
boehmes@36900
   907
#93 := (exists (vars (?v1 S2)) #92)
boehmes@36900
   908
#88 := (and #29 #87)
boehmes@36900
   909
#94 := (implies #88 #93)
boehmes@36900
   910
#95 := (forall (vars (?v0 S2)) #94)
boehmes@36900
   911
#217 := (implies #95 #216)
boehmes@36900
   912
#84 := (<= #78 #83)
boehmes@36900
   913
#82 := (and #73 #50)
boehmes@34994
   914
#85 := (implies #82 #84)
boehmes@36900
   915
#86 := (forall (vars (?v0 S2) (?v1 S2)) #85)
boehmes@36900
   916
#218 := (implies #86 #217)
boehmes@36900
   917
#79 := (<= #78 #68)
boehmes@36900
   918
#76 := (= #75 f1)
boehmes@36900
   919
#77 := (and #74 #76)
boehmes@36900
   920
#80 := (implies #77 #79)
boehmes@36900
   921
#81 := (forall (vars (?v0 S2) (?v1 S2)) #80)
boehmes@36900
   922
#219 := (implies #81 #218)
boehmes@36900
   923
#69 := (<= 0::int #68)
boehmes@36900
   924
#70 := (forall (vars (?v0 S2)) #69)
boehmes@36900
   925
#220 := (implies #70 #219)
boehmes@36900
   926
#221 := (implies #67 #220)
boehmes@36900
   927
#222 := (implies true #221)
boehmes@36900
   928
#52 := (+ #25 #49)
boehmes@36900
   929
#59 := (= #44 #52)
boehmes@36900
   930
#34 := (= #33 f1)
boehmes@36900
   931
#60 := (and #34 #59)
boehmes@36900
   932
#58 := (< #25 #44)
boehmes@36900
   933
#61 := (and #58 #60)
boehmes@36900
   934
#62 := (exists (vars (?v1 S2)) #61)
boehmes@36900
   935
#56 := (< #25 f3)
boehmes@36900
   936
#57 := (and #29 #56)
boehmes@36900
   937
#63 := (implies #57 #62)
boehmes@36900
   938
#64 := (forall (vars (?v0 S2)) #63)
boehmes@36900
   939
#223 := (implies #64 #222)
boehmes@36900
   940
#224 := (and #64 #223)
boehmes@36900
   941
#53 := (<= #44 #52)
boehmes@36900
   942
#51 := (and #34 #50)
boehmes@36900
   943
#54 := (implies #51 #53)
boehmes@36900
   944
#55 := (forall (vars (?v0 S2) (?v1 S2)) #54)
boehmes@36900
   945
#225 := (implies #55 #224)
boehmes@36900
   946
#226 := (and #55 #225)
boehmes@36900
   947
#45 := (<= #44 #25)
boehmes@36900
   948
#42 := (= #41 f1)
boehmes@36900
   949
#35 := (not #34)
boehmes@36900
   950
#43 := (and #35 #42)
boehmes@36900
   951
#46 := (implies #43 #45)
boehmes@36900
   952
#47 := (forall (vars (?v0 S2) (?v1 S2)) #46)
boehmes@36900
   953
#227 := (implies #47 #226)
boehmes@36900
   954
#228 := (and #47 #227)
boehmes@36900
   955
#39 := (<= 0::int #25)
boehmes@36900
   956
#40 := (forall (vars (?v0 S2)) #39)
boehmes@36900
   957
#229 := (implies #40 #228)
boehmes@36900
   958
#230 := (and #40 #229)
boehmes@36900
   959
#231 := (implies #38 #230)
boehmes@36900
   960
#232 := (and #38 #231)
boehmes@36900
   961
#36 := (forall (vars (?v0 S2)) #35)
boehmes@36900
   962
#233 := (implies #36 #232)
boehmes@36900
   963
#30 := (= #25 f3)
boehmes@36900
   964
#31 := (implies #29 #30)
boehmes@36900
   965
#32 := (forall (vars (?v0 S2)) #31)
boehmes@36900
   966
#234 := (implies #32 #233)
boehmes@36900
   967
#27 := (implies #24 #26)
boehmes@36900
   968
#28 := (forall (vars (?v0 S2)) #27)
boehmes@36900
   969
#235 := (implies #28 #234)
boehmes@36900
   970
#236 := (implies true #235)
boehmes@36900
   971
#237 := (not #236)
boehmes@36900
   972
#1737 := (iff #237 #1734)
boehmes@36900
   973
#759 := (+ #49 #155)
boehmes@36900
   974
#777 := (= #177 #759)
boehmes@36900
   975
#780 := (and #713 #777)
boehmes@36900
   976
#783 := (and #188 #780)
boehmes@36900
   977
#786 := (exists (vars (?v1 S2)) #783)
boehmes@36900
   978
#792 := (not #187)
boehmes@36900
   979
#793 := (or #792 #786)
boehmes@36900
   980
#798 := (forall (vars (?v0 S2)) #793)
boehmes@36900
   981
#762 := (<= #177 #759)
boehmes@36900
   982
#754 := (and #50 #713)
boehmes@36900
   983
#768 := (not #754)
boehmes@36900
   984
#769 := (or #768 #762)
boehmes@36900
   985
#774 := (forall (vars (?v0 S2) (?v1 S2)) #769)
boehmes@36900
   986
#811 := (not #774)
boehmes@36900
   987
#812 := (or #811 #798)
boehmes@36900
   988
#817 := (and #774 #812)
boehmes@36900
   989
#743 := (or #178 #742)
boehmes@36900
   990
#748 := (forall (vars (?v0 S2) (?v1 S2)) #743)
boehmes@36900
   991
#823 := (not #748)
boehmes@36900
   992
#824 := (or #823 #817)
boehmes@36900
   993
#829 := (and #748 #824)
boehmes@36900
   994
#835 := (not #172)
boehmes@36900
   995
#836 := (or #835 #829)
boehmes@36900
   996
#841 := (and #172 #836)
boehmes@36900
   997
#728 := (= 0::int #169)
boehmes@36900
   998
#847 := (not #728)
boehmes@36900
   999
#848 := (or #847 #841)
boehmes@36900
  1000
#853 := (and #728 #848)
boehmes@36900
  1001
#860 := (or #859 #853)
boehmes@36900
  1002
#865 := (and #725 #860)
boehmes@36900
  1003
#871 := (not #164)
boehmes@36900
  1004
#872 := (or #871 #865)
boehmes@36900
  1005
#877 := (and #164 #872)
boehmes@36900
  1006
#705 := (or #154 #699)
boehmes@36900
  1007
#710 := (forall (vars (?v0 S2)) #705)
boehmes@36900
  1008
#883 := (not #710)
boehmes@36900
  1009
#884 := (or #883 #877)
boehmes@36900
  1010
#685 := (= #152 #155)
boehmes@36900
  1011
#691 := (or #159 #685)
boehmes@36900
  1012
#696 := (forall (vars (?v0 S2)) #691)
boehmes@36900
  1013
#892 := (not #696)
boehmes@36900
  1014
#893 := (or #892 #884)
boehmes@36900
  1015
#902 := (or #901 #893)
boehmes@36900
  1016
#677 := (or #143 #447)
boehmes@36900
  1017
#682 := (forall (vars (?v0 S2)) #677)
boehmes@36900
  1018
#910 := (not #682)
boehmes@36900
  1019
#911 := (or #910 #902)
boehmes@36900
  1020
#919 := (not #142)
boehmes@36900
  1021
#920 := (or #919 #911)
boehmes@36900
  1022
#928 := (or #668 #920)
boehmes@36900
  1023
#524 := (and #87 #450)
boehmes@36900
  1024
#529 := (exists (vars (?v0 S2)) #524)
boehmes@36900
  1025
#532 := (not #529)
boehmes@36900
  1026
#936 := (or #532 #928)
boehmes@36900
  1027
#583 := (= 0::int #124)
boehmes@36900
  1028
#541 := (+ #49 #109)
boehmes@36900
  1029
#568 := (<= #112 #541)
boehmes@36900
  1030
#565 := (and #50 #110)
boehmes@36900
  1031
#574 := (not #565)
boehmes@36900
  1032
#575 := (or #574 #568)
boehmes@36900
  1033
#580 := (forall (vars (?v0 S2) (?v1 S2)) #575)
boehmes@36900
  1034
#596 := (not #580)
boehmes@36900
  1035
#597 := (or #596 #583)
boehmes@36900
  1036
#602 := (and #580 #597)
boehmes@36900
  1037
#544 := (= #112 #541)
boehmes@36900
  1038
#547 := (and #113 #544)
boehmes@36900
  1039
#550 := (exists (vars (?v1 S2)) #547)
boehmes@36900
  1040
#556 := (not #111)
boehmes@36900
  1041
#557 := (or #556 #550)
boehmes@36900
  1042
#562 := (forall (vars (?v0 S2)) #557)
boehmes@36900
  1043
#608 := (not #562)
boehmes@36900
  1044
#609 := (or #608 #602)
boehmes@36900
  1045
#614 := (and #562 #609)
boehmes@36900
  1046
#621 := (or #620 #614)
boehmes@36900
  1047
#630 := (or #629 #621)
boehmes@36900
  1048
#639 := (or #638 #630)
boehmes@36900
  1049
#648 := (or #647 #639)
boehmes@36900
  1050
#656 := (or #529 #648)
boehmes@36900
  1051
#948 := (and #656 #936)
boehmes@36900
  1052
#479 := (+ #49 #68)
boehmes@36900
  1053
#497 := (= #78 #479)
boehmes@36900
  1054
#500 := (and #447 #497)
boehmes@36900
  1055
#503 := (and #89 #500)
boehmes@36900
  1056
#506 := (exists (vars (?v1 S2)) #503)
boehmes@36900
  1057
#512 := (not #88)
boehmes@36900
  1058
#513 := (or #512 #506)
boehmes@36900
  1059
#518 := (forall (vars (?v0 S2)) #513)
boehmes@36900
  1060
#954 := (not #518)
boehmes@34994
  1061
#955 := (or #954 #948)
boehmes@36900
  1062
#482 := (<= #78 #479)
boehmes@36900
  1063
#474 := (and #50 #447)
boehmes@36900
  1064
#488 := (not #474)
boehmes@36900
  1065
#489 := (or #488 #482)
boehmes@36900
  1066
#494 := (forall (vars (?v0 S2) (?v1 S2)) #489)
boehmes@36900
  1067
#963 := (not #494)
boehmes@36900
  1068
#964 := (or #963 #955)
boehmes@36900
  1069
#463 := (or #79 #462)
boehmes@36900
  1070
#468 := (forall (vars (?v0 S2) (?v1 S2)) #463)
boehmes@36900
  1071
#972 := (not #468)
boehmes@36900
  1072
#973 := (or #972 #964)
boehmes@36900
  1073
#981 := (not #70)
boehmes@36900
  1074
#982 := (or #981 #973)
boehmes@36900
  1075
#444 := (= 0::int #66)
boehmes@36900
  1076
#990 := (not #444)
boehmes@36900
  1077
#991 := (or #990 #982)
boehmes@36900
  1078
#421 := (and #59 #368)
boehmes@36900
  1079
#426 := (and #58 #421)
boehmes@36900
  1080
#429 := (exists (vars (?v1 S2)) #426)
boehmes@36900
  1081
#435 := (not #57)
boehmes@36900
  1082
#436 := (or #435 #429)
boehmes@36900
  1083
#441 := (forall (vars (?v0 S2)) #436)
boehmes@36900
  1084
#1006 := (not #441)
boehmes@36900
  1085
#1007 := (or #1006 #991)
boehmes@36900
  1086
#1012 := (and #441 #1007)
boehmes@36900
  1087
#401 := (and #50 #368)
boehmes@36900
  1088
#409 := (not #401)
boehmes@36900
  1089
#410 := (or #53 #409)
boehmes@36900
  1090
#415 := (forall (vars (?v0 S2) (?v1 S2)) #410)
boehmes@36900
  1091
#1018 := (not #415)
boehmes@36900
  1092
#1019 := (or #1018 #1012)
boehmes@36900
  1093
#1024 := (and #415 #1019)
boehmes@36900
  1094
#390 := (or #45 #389)
boehmes@36900
  1095
#395 := (forall (vars (?v0 S2) (?v1 S2)) #390)
boehmes@36900
  1096
#1030 := (not #395)
boehmes@36900
  1097
#1031 := (or #1030 #1024)
boehmes@36900
  1098
#1036 := (and #395 #1031)
boehmes@36900
  1099
#1042 := (not #40)
boehmes@36900
  1100
#1043 := (or #1042 #1036)
boehmes@36900
  1101
#1048 := (and #40 #1043)
boehmes@36900
  1102
#377 := (= 0::int #37)
boehmes@36900
  1103
#1054 := (not #377)
boehmes@36900
  1104
#1055 := (or #1054 #1048)
boehmes@36900
  1105
#1060 := (and #377 #1055)
boehmes@36900
  1106
#1067 := (or #1066 #1060)
boehmes@36900
  1107
#1076 := (or #1075 #1067)
boehmes@36900
  1108
#340 := (= 0::int #25)
boehmes@36900
  1109
#346 := (or #29 #340)
boehmes@36900
  1110
#351 := (forall (vars (?v0 S2)) #346)
boehmes@36900
  1111
#1084 := (not #351)
boehmes@36900
  1112
#1085 := (or #1084 #1076)
boehmes@36900
  1113
#1097 := (not #1085)
boehmes@36900
  1114
#1735 := (iff #1097 #1734)
boehmes@36900
  1115
#1732 := (iff #1085 #1729)
boehmes@36900
  1116
#1720 := (or #1066 #1706)
boehmes@36900
  1117
#1723 := (or #1075 #1720)
boehmes@36900
  1118
#1726 := (or #1717 #1723)
boehmes@36900
  1119
#1730 := (iff #1726 #1729)
boehmes@36900
  1120
#1731 := [rewrite]: #1730
boehmes@36900
  1121
#1727 := (iff #1085 #1726)
boehmes@36900
  1122
#1724 := (iff #1076 #1723)
boehmes@36900
  1123
#1721 := (iff #1067 #1720)
boehmes@36900
  1124
#1707 := (iff #1060 #1706)
boehmes@36900
  1125
#1704 := (iff #1055 #1703)
boehmes@36900
  1126
#1701 := (iff #1048 #1700)
boehmes@36900
  1127
#1698 := (iff #1043 #1697)
boehmes@36900
  1128
#1695 := (iff #1036 #1694)
boehmes@36900
  1129
#1692 := (iff #1031 #1691)
boehmes@36900
  1130
#1689 := (iff #1024 #1688)
boehmes@36900
  1131
#1686 := (iff #1019 #1685)
boehmes@36900
  1132
#1683 := (iff #1012 #1682)
boehmes@36900
  1133
#1680 := (iff #1007 #1677)
boehmes@36900
  1134
#1659 := (or #1245 #1600)
boehmes@36900
  1135
#1662 := (or #1623 #1659)
boehmes@36900
  1136
#1665 := (or #1639 #1662)
boehmes@36900
  1137
#1668 := (or #1648 #1665)
boehmes@36900
  1138
#1671 := (or #1653 #1668)
boehmes@36900
  1139
#1674 := (or #1656 #1671)
boehmes@36900
  1140
#1678 := (iff #1674 #1677)
boehmes@36900
  1141
#1679 := [rewrite]: #1678
boehmes@36900
  1142
#1675 := (iff #1007 #1674)
boehmes@36900
  1143
#1672 := (iff #991 #1671)
boehmes@36900
  1144
#1669 := (iff #982 #1668)
boehmes@36900
  1145
#1666 := (iff #973 #1665)
boehmes@36900
  1146
#1663 := (iff #964 #1662)
boehmes@36900
  1147
#1660 := (iff #955 #1659)
boehmes@36900
  1148
#1601 := (iff #948 #1600)
boehmes@36900
  1149
#1598 := (iff #936 #1595)
boehmes@36900
  1150
#1574 := (or #1380 #1521)
boehmes@36900
  1151
#1577 := (or #1538 #1574)
boehmes@36900
  1152
#1580 := (or #901 #1577)
boehmes@36900
  1153
#1583 := (or #1556 #1580)
boehmes@36900
  1154
#1586 := (or #1560 #1583)
boehmes@36900
  1155
#1589 := (or #668 #1586)
boehmes@36900
  1156
#1592 := (or #1571 #1589)
boehmes@36900
  1157
#1596 := (iff #1592 #1595)
boehmes@36900
  1158
#1597 := [rewrite]: #1596
boehmes@36900
  1159
#1593 := (iff #936 #1592)
boehmes@36900
  1160
#1590 := (iff #928 #1589)
boehmes@36900
  1161
#1587 := (iff #920 #1586)
boehmes@36900
  1162
#1584 := (iff #911 #1583)
boehmes@36900
  1163
#1581 := (iff #902 #1580)
boehmes@36900
  1164
#1578 := (iff #893 #1577)
boehmes@36900
  1165
#1575 := (iff #884 #1574)
boehmes@36900
  1166
#1522 := (iff #877 #1521)
boehmes@36900
  1167
#1519 := (iff #872 #1518)
boehmes@36900
  1168
#1516 := (iff #865 #1515)
boehmes@36900
  1169
#1513 := (iff #860 #1512)
boehmes@36900
  1170
#1510 := (iff #853 #1509)
boehmes@36900
  1171
#1507 := (iff #848 #1506)
boehmes@36900
  1172
#1504 := (iff #841 #1503)
boehmes@36900
  1173
#1501 := (iff #836 #1500)
boehmes@36900
  1174
#1498 := (iff #829 #1497)
boehmes@36900
  1175
#1495 := (iff #824 #1494)
boehmes@36900
  1176
#1492 := (iff #817 #1491)
boehmes@36900
  1177
#1489 := (iff #812 #1488)
boehmes@36900
  1178
#1486 := (iff #798 #1485)
boehmes@36900
  1179
#1483 := (iff #793 #1482)
boehmes@36900
  1180
#1480 := (iff #786 #1479)
boehmes@36900
  1181
#1477 := (iff #783 #1474)
boehmes@36900
  1182
#1468 := (and #713 #1462)
boehmes@36900
  1183
#1471 := (and #1465 #1468)
boehmes@36900
  1184
#1475 := (iff #1471 #1474)
boehmes@36900
  1185
#1476 := [rewrite]: #1475
boehmes@36900
  1186
#1472 := (iff #783 #1471)
boehmes@36900
  1187
#1469 := (iff #780 #1468)
boehmes@36900
  1188
#1463 := (iff #777 #1462)
boehmes@36900
  1189
#1464 := [rewrite]: #1463
boehmes@36900
  1190
#1470 := [monotonicity #1464]: #1469
boehmes@36900
  1191
#1466 := (iff #188 #1465)
boehmes@36900
  1192
#1467 := [rewrite]: #1466
boehmes@36900
  1193
#1473 := [monotonicity #1467 #1470]: #1472
boehmes@36900
  1194
#1478 := [trans #1473 #1476]: #1477
boehmes@36900
  1195
#1481 := [quant-intro #1478]: #1480
boehmes@36900
  1196
#1460 := (iff #792 #1459)
boehmes@36900
  1197
#1457 := (iff #187 #1456)
boehmes@36900
  1198
#1454 := (iff #186 #1453)
boehmes@36900
  1199
#1455 := [rewrite]: #1454
boehmes@36900
  1200
#1458 := [monotonicity #1455]: #1457
boehmes@36900
  1201
#1461 := [monotonicity #1458]: #1460
boehmes@36900
  1202
#1484 := [monotonicity #1461 #1481]: #1483
boehmes@36900
  1203
#1487 := [quant-intro #1484]: #1486
boehmes@36900
  1204
#1449 := (iff #811 #1448)
boehmes@36900
  1205
#1446 := (iff #774 #1445)
boehmes@36900
  1206
#1443 := (iff #769 #1442)
boehmes@36900
  1207
#1439 := (iff #762 #1438)
boehmes@36900
  1208
#1441 := [rewrite]: #1439
boehmes@36900
  1209
#1436 := (iff #768 #1435)
boehmes@36900
  1210
#1433 := (iff #754 #1430)
boehmes@36900
  1211
#1427 := (and #1142 #713)
boehmes@36900
  1212
#1431 := (iff #1427 #1430)
boehmes@36900
  1213
#1432 := [rewrite]: #1431
boehmes@36900
  1214
#1428 := (iff #754 #1427)
boehmes@36900
  1215
#1143 := (iff #50 #1142)
boehmes@36900
  1216
#1144 := [rewrite]: #1143
boehmes@36900
  1217
#1429 := [monotonicity #1144]: #1428
boehmes@36900
  1218
#1434 := [trans #1429 #1432]: #1433
boehmes@36900
  1219
#1437 := [monotonicity #1434]: #1436
boehmes@36900
  1220
#1444 := [monotonicity #1437 #1441]: #1443
boehmes@36900
  1221
#1447 := [quant-intro #1444]: #1446
boehmes@36900
  1222
#1450 := [monotonicity #1447]: #1449
boehmes@36900
  1223
#1490 := [monotonicity #1450 #1487]: #1489
boehmes@36900
  1224
#1493 := [monotonicity #1447 #1490]: #1492
boehmes@36900
  1225
#1425 := (iff #823 #1424)
boehmes@36900
  1226
#1422 := (iff #748 #1421)
boehmes@36900
  1227
#1419 := (iff #743 #1416)
boehmes@36900
  1228
#1413 := (or #1408 #742)
boehmes@36900
  1229
#1417 := (iff #1413 #1416)
boehmes@36900
  1230
#1418 := [rewrite]: #1417
boehmes@36900
  1231
#1414 := (iff #743 #1413)
boehmes@36900
  1232
#1411 := (iff #178 #1408)
boehmes@36900
  1233
#1412 := [rewrite]: #1411
boehmes@36900
  1234
#1415 := [monotonicity #1412]: #1414
boehmes@36900
  1235
#1420 := [trans #1415 #1418]: #1419
boehmes@36900
  1236
#1423 := [quant-intro #1420]: #1422
boehmes@36900
  1237
#1426 := [monotonicity #1423]: #1425
boehmes@36900
  1238
#1496 := [monotonicity #1426 #1493]: #1495
boehmes@36900
  1239
#1499 := [monotonicity #1423 #1496]: #1498
boehmes@36900
  1240
#1406 := (iff #835 #1405)
boehmes@36900
  1241
#1403 := (iff #172 #1402)
boehmes@36900
  1242
#1400 := (iff #171 #1399)
boehmes@36900
  1243
#1401 := [rewrite]: #1400
boehmes@36900
  1244
#1404 := [quant-intro #1401]: #1403
boehmes@36900
  1245
#1407 := [monotonicity #1404]: #1406
boehmes@36900
  1246
#1502 := [monotonicity #1407 #1499]: #1501
boehmes@36900
  1247
#1505 := [monotonicity #1404 #1502]: #1504
boehmes@36900
  1248
#1397 := (iff #847 #1396)
boehmes@36900
  1249
#1394 := (iff #728 #170)
boehmes@36900
  1250
#1395 := [rewrite]: #1394
boehmes@36900
  1251
#1398 := [monotonicity #1395]: #1397
boehmes@36900
  1252
#1508 := [monotonicity #1398 #1505]: #1507
boehmes@36900
  1253
#1511 := [monotonicity #1395 #1508]: #1510
boehmes@36900
  1254
#1514 := [monotonicity #1511]: #1513
boehmes@36900
  1255
#1517 := [monotonicity #1514]: #1516
boehmes@36900
  1256
#1392 := (iff #871 #1391)
boehmes@36900
  1257
#1389 := (iff #164 #1388)
boehmes@36900
  1258
#1386 := (iff #163 #1383)
boehmes@36900
  1259
#1387 := [rewrite]: #1386
boehmes@36900
  1260
#1390 := [quant-intro #1387]: #1389
boehmes@36900
  1261
#1393 := [monotonicity #1390]: #1392
boehmes@36900
  1262
#1520 := [monotonicity #1393 #1517]: #1519
boehmes@36900
  1263
#1523 := [monotonicity #1390 #1520]: #1522
boehmes@36900
  1264
#1381 := (iff #883 #1380)
boehmes@36900
  1265
#1378 := (iff #710 #1377)
boehmes@36900
  1266
#1375 := (iff #705 #1372)
boehmes@36900
  1267
#1369 := (or #1366 #699)
boehmes@36900
  1268
#1373 := (iff #1369 #1372)
boehmes@36900
  1269
#1374 := [rewrite]: #1373
boehmes@36900
  1270
#1370 := (iff #705 #1369)
boehmes@36900
  1271
#1367 := (iff #154 #1366)
boehmes@36900
  1272
#1364 := (iff #153 #1363)
boehmes@36900
  1273
#1365 := [rewrite]: #1364
boehmes@36900
  1274
#1357 := (iff #151 #1356)
boehmes@36900
  1275
#1358 := [rewrite]: #1357
boehmes@36900
  1276
#1368 := [monotonicity #1358 #1365]: #1367
boehmes@36900
  1277
#1371 := [monotonicity #1368]: #1370
boehmes@36900
  1278
#1376 := [trans #1371 #1374]: #1375
boehmes@36900
  1279
#1379 := [quant-intro #1376]: #1378
boehmes@36900
  1280
#1382 := [monotonicity #1379]: #1381
boehmes@36900
  1281
#1576 := [monotonicity #1382 #1523]: #1575
boehmes@36900
  1282
#1539 := (iff #892 #1538)
boehmes@36900
  1283
#1536 := (iff #696 #1535)
boehmes@36900
  1284
#1533 := (iff #691 #1532)
boehmes@36900
  1285
#1530 := (iff #685 #1529)
boehmes@36900
  1286
#1531 := [rewrite]: #1530
boehmes@36900
  1287
#1525 := (iff #159 #1524)
boehmes@36900
  1288
#1526 := [monotonicity #1368]: #1525
boehmes@36900
  1289
#1534 := [monotonicity #1526 #1531]: #1533
boehmes@36900
  1290
#1537 := [quant-intro #1534]: #1536
boehmes@36900
  1291
#1540 := [monotonicity #1537]: #1539
boehmes@36900
  1292
#1579 := [monotonicity #1540 #1576]: #1578
boehmes@36900
  1293
#1582 := [monotonicity #1579]: #1581
boehmes@36900
  1294
#1557 := (iff #910 #1556)
boehmes@36900
  1295
#1554 := (iff #682 #1553)
boehmes@36900
  1296
#1551 := (iff #677 #1548)
boehmes@36900
  1297
#1545 := (or #1541 #447)
boehmes@36900
  1298
#1549 := (iff #1545 #1548)
boehmes@36900
  1299
#1550 := [rewrite]: #1549
boehmes@36900
  1300
#1546 := (iff #677 #1545)
boehmes@36900
  1301
#1543 := (iff #143 #1541)
boehmes@36900
  1302
#1544 := [rewrite]: #1543
boehmes@36900
  1303
#1547 := [monotonicity #1544]: #1546
boehmes@36900
  1304
#1552 := [trans #1547 #1550]: #1551
boehmes@36900
  1305
#1555 := [quant-intro #1552]: #1554
boehmes@36900
  1306
#1558 := [monotonicity #1555]: #1557
boehmes@36900
  1307
#1585 := [monotonicity #1558 #1582]: #1584
boehmes@36900
  1308
#1569 := (iff #919 #1560)
boehmes@36900
  1309
#1561 := (not #1560)
boehmes@36900
  1310
#1564 := (not #1561)
boehmes@36900
  1311
#1567 := (iff #1564 #1560)
boehmes@36900
  1312
#1568 := [rewrite]: #1567
boehmes@36900
  1313
#1565 := (iff #919 #1564)
boehmes@36900
  1314
#1562 := (iff #142 #1561)
boehmes@36900
  1315
#1563 := [rewrite]: #1562
boehmes@36900
  1316
#1566 := [monotonicity #1563]: #1565
boehmes@36900
  1317
#1570 := [trans #1566 #1568]: #1569
boehmes@36900
  1318
#1588 := [monotonicity #1570 #1585]: #1587
boehmes@36900
  1319
#1591 := [monotonicity #1588]: #1590
boehmes@36900
  1320
#1572 := (iff #532 #1571)
boehmes@36900
  1321
#1331 := (iff #529 #1330)
boehmes@36900
  1322
#1328 := (iff #524 #1325)
boehmes@36900
  1323
#1322 := (and #1206 #450)
boehmes@36900
  1324
#1326 := (iff #1322 #1325)
boehmes@36900
  1325
#1327 := [rewrite]: #1326
boehmes@36900
  1326
#1323 := (iff #524 #1322)
boehmes@36900
  1327
#1207 := (iff #87 #1206)
boehmes@36900
  1328
#1208 := [rewrite]: #1207
boehmes@36900
  1329
#1324 := [monotonicity #1208]: #1323
boehmes@36900
  1330
#1329 := [trans #1324 #1327]: #1328
boehmes@36900
  1331
#1332 := [quant-intro #1329]: #1331
boehmes@36900
  1332
#1573 := [monotonicity #1332]: #1572
boehmes@36900
  1333
#1594 := [monotonicity #1573 #1591]: #1593
boehmes@36900
  1334
#1599 := [trans #1594 #1597]: #1598
boehmes@36900
  1335
#1351 := (iff #656 #1348)
boehmes@36900
  1336
#1333 := (or #620 #1319)
boehmes@36900
  1337
#1336 := (or #629 #1333)
boehmes@36900
  1338
#1339 := (or #638 #1336)
boehmes@36900
  1339
#1342 := (or #647 #1339)
boehmes@36900
  1340
#1345 := (or #1330 #1342)
boehmes@36900
  1341
#1349 := (iff #1345 #1348)
boehmes@36900
  1342
#1350 := [rewrite]: #1349
boehmes@36900
  1343
#1346 := (iff #656 #1345)
boehmes@36900
  1344
#1343 := (iff #648 #1342)
boehmes@36900
  1345
#1340 := (iff #639 #1339)
boehmes@36900
  1346
#1337 := (iff #630 #1336)
boehmes@36900
  1347
#1334 := (iff #621 #1333)
boehmes@36900
  1348
#1320 := (iff #614 #1319)
boehmes@36900
  1349
#1317 := (iff #609 #1316)
boehmes@36900
  1350
#1314 := (iff #602 #1313)
boehmes@36900
  1351
#1311 := (iff #597 #1308)
boehmes@36900
  1352
#1305 := (or #1300 #125)
boehmes@36900
  1353
#1309 := (iff #1305 #1308)
boehmes@34994
  1354
#1310 := [rewrite]: #1309
boehmes@36900
  1355
#1306 := (iff #597 #1305)
boehmes@36900
  1356
#1303 := (iff #583 #125)
boehmes@34994
  1357
#1304 := [rewrite]: #1303
boehmes@36900
  1358
#1301 := (iff #596 #1300)
boehmes@36900
  1359
#1298 := (iff #580 #1297)
boehmes@36900
  1360
#1295 := (iff #575 #1294)
boehmes@36900
  1361
#1292 := (iff #568 #1291)
boehmes@36900
  1362
#1293 := [rewrite]: #1292
boehmes@36900
  1363
#1289 := (iff #574 #1288)
boehmes@36900
  1364
#1286 := (iff #565 #1285)
boehmes@36900
  1365
#1252 := (iff #110 #1251)
boehmes@36900
  1366
#1253 := [rewrite]: #1252
boehmes@36900
  1367
#1287 := [monotonicity #1144 #1253]: #1286
boehmes@36900
  1368
#1290 := [monotonicity #1287]: #1289
boehmes@36900
  1369
#1296 := [monotonicity #1290 #1293]: #1295
boehmes@34994
  1370
#1299 := [quant-intro #1296]: #1298
boehmes@34994
  1371
#1302 := [monotonicity #1299]: #1301
boehmes@36900
  1372
#1307 := [monotonicity #1302 #1304]: #1306
boehmes@36900
  1373
#1312 := [trans #1307 #1310]: #1311
boehmes@36900
  1374
#1315 := [monotonicity #1299 #1312]: #1314
boehmes@36900
  1375
#1283 := (iff #608 #1282)
boehmes@36900
  1376
#1280 := (iff #562 #1279)
boehmes@36900
  1377
#1277 := (iff #557 #1276)
boehmes@36900
  1378
#1274 := (iff #550 #1273)
boehmes@36900
  1379
#1271 := (iff #547 #1270)
boehmes@36900
  1380
#1267 := (iff #544 #1266)
boehmes@36900
  1381
#1269 := [rewrite]: #1267
boehmes@36900
  1382
#1264 := (iff #113 #1263)
boehmes@36900
  1383
#1265 := [rewrite]: #1264
boehmes@36900
  1384
#1272 := [monotonicity #1265 #1269]: #1271
boehmes@36900
  1385
#1275 := [quant-intro #1272]: #1274
boehmes@36900
  1386
#1258 := (iff #556 #1257)
boehmes@36900
  1387
#1255 := (iff #111 #1254)
boehmes@36900
  1388
#1256 := [monotonicity #1253]: #1255
boehmes@36900
  1389
#1259 := [monotonicity #1256]: #1258
boehmes@36900
  1390
#1278 := [monotonicity #1259 #1275]: #1277
boehmes@36900
  1391
#1281 := [quant-intro #1278]: #1280
boehmes@36900
  1392
#1284 := [monotonicity #1281]: #1283
boehmes@36900
  1393
#1318 := [monotonicity #1284 #1315]: #1317
boehmes@36900
  1394
#1321 := [monotonicity #1281 #1318]: #1320
boehmes@36900
  1395
#1335 := [monotonicity #1321]: #1334
boehmes@36900
  1396
#1338 := [monotonicity #1335]: #1337
boehmes@36900
  1397
#1341 := [monotonicity #1338]: #1340
boehmes@36900
  1398
#1344 := [monotonicity #1341]: #1343
boehmes@36900
  1399
#1347 := [monotonicity #1332 #1344]: #1346
boehmes@36900
  1400
#1352 := [trans #1347 #1350]: #1351
boehmes@36900
  1401
#1602 := [monotonicity #1352 #1599]: #1601
boehmes@36900
  1402
#1246 := (iff #954 #1245)
boehmes@36900
  1403
#1243 := (iff #518 #1242)
boehmes@36900
  1404
#1240 := (iff #513 #1239)
boehmes@36900
  1405
#1237 := (iff #506 #1236)
boehmes@36900
  1406
#1234 := (iff #503 #1231)
boehmes@36900
  1407
#1225 := (and #447 #1215)
boehmes@36900
  1408
#1228 := (and #1222 #1225)
boehmes@36900
  1409
#1232 := (iff #1228 #1231)
boehmes@36900
  1410
#1233 := [rewrite]: #1232
boehmes@36900
  1411
#1229 := (iff #503 #1228)
boehmes@36900
  1412
#1226 := (iff #500 #1225)
boehmes@36900
  1413
#1216 := (iff #497 #1215)
boehmes@36900
  1414
#1220 := [rewrite]: #1216
boehmes@36900
  1415
#1227 := [monotonicity #1220]: #1226
boehmes@36900
  1416
#1223 := (iff #89 #1222)
boehmes@34994
  1417
#1224 := [rewrite]: #1223
boehmes@36900
  1418
#1230 := [monotonicity #1224 #1227]: #1229
boehmes@36900
  1419
#1235 := [trans #1230 #1233]: #1234
boehmes@36900
  1420
#1238 := [quant-intro #1235]: #1237
boehmes@36900
  1421
#1213 := (iff #512 #1212)
boehmes@36900
  1422
#1210 := (iff #88 #1209)
boehmes@36900
  1423
#1211 := [monotonicity #1208]: #1210
boehmes@36900
  1424
#1214 := [monotonicity #1211]: #1213
boehmes@36900
  1425
#1241 := [monotonicity #1214 #1238]: #1240
boehmes@36900
  1426
#1244 := [quant-intro #1241]: #1243
boehmes@34994
  1427
#1247 := [monotonicity #1244]: #1246
boehmes@36900
  1428
#1661 := [monotonicity #1247 #1602]: #1660
boehmes@36900
  1429
#1624 := (iff #963 #1623)
boehmes@36900
  1430
#1621 := (iff #494 #1620)
boehmes@36900
  1431
#1618 := (iff #489 #1617)
boehmes@36900
  1432
#1615 := (iff #482 #1614)
boehmes@36900
  1433
#1616 := [rewrite]: #1615
boehmes@36900
  1434
#1612 := (iff #488 #1611)
boehmes@36900
  1435
#1609 := (iff #474 #1606)
boehmes@36900
  1436
#1603 := (and #1142 #447)
boehmes@36900
  1437
#1607 := (iff #1603 #1606)
boehmes@36900
  1438
#1608 := [rewrite]: #1607
boehmes@36900
  1439
#1604 := (iff #474 #1603)
boehmes@36900
  1440
#1605 := [monotonicity #1144]: #1604
boehmes@36900
  1441
#1610 := [trans #1605 #1608]: #1609
boehmes@34994
  1442
#1613 := [monotonicity #1610]: #1612
boehmes@36900
  1443
#1619 := [monotonicity #1613 #1616]: #1618
boehmes@36900
  1444
#1622 := [quant-intro #1619]: #1621
boehmes@36900
  1445
#1625 := [monotonicity #1622]: #1624
boehmes@36900
  1446
#1664 := [monotonicity #1625 #1661]: #1663
boehmes@36900
  1447
#1640 := (iff #972 #1639)
boehmes@36900
  1448
#1637 := (iff #468 #1636)
boehmes@36900
  1449
#1634 := (iff #463 #1631)
boehmes@36900
  1450
#1628 := (or #1221 #462)
boehmes@36900
  1451
#1632 := (iff #1628 #1631)
boehmes@36900
  1452
#1633 := [rewrite]: #1632
boehmes@36900
  1453
#1629 := (iff #463 #1628)
boehmes@36900
  1454
#1626 := (iff #79 #1221)
boehmes@36900
  1455
#1627 := [rewrite]: #1626
boehmes@34994
  1456
#1630 := [monotonicity #1627]: #1629
boehmes@36900
  1457
#1635 := [trans #1630 #1633]: #1634
boehmes@36900
  1458
#1638 := [quant-intro #1635]: #1637
boehmes@36900
  1459
#1641 := [monotonicity #1638]: #1640
boehmes@36900
  1460
#1667 := [monotonicity #1641 #1664]: #1666
boehmes@36900
  1461
#1649 := (iff #981 #1648)
boehmes@36900
  1462
#1646 := (iff #70 #1645)
boehmes@36900
  1463
#1643 := (iff #69 #1642)
boehmes@36900
  1464
#1644 := [rewrite]: #1643
boehmes@36900
  1465
#1647 := [quant-intro #1644]: #1646
boehmes@36900
  1466
#1650 := [monotonicity #1647]: #1649
boehmes@36900
  1467
#1670 := [monotonicity #1650 #1667]: #1669
boehmes@36900
  1468
#1654 := (iff #990 #1653)
boehmes@36900
  1469
#1651 := (iff #444 #67)
boehmes@36900
  1470
#1652 := [rewrite]: #1651
boehmes@36900
  1471
#1655 := [monotonicity #1652]: #1654
boehmes@36900
  1472
#1673 := [monotonicity #1655 #1670]: #1672
boehmes@36900
  1473
#1657 := (iff #1006 #1656)
boehmes@36900
  1474
#1201 := (iff #441 #1200)
boehmes@36900
  1475
#1198 := (iff #436 #1197)
boehmes@36900
  1476
#1195 := (iff #429 #1194)
boehmes@36900
  1477
#1192 := (iff #426 #1189)
boehmes@36900
  1478
#1183 := (and #1177 #368)
boehmes@36900
  1479
#1186 := (and #1180 #1183)
boehmes@36900
  1480
#1190 := (iff #1186 #1189)
boehmes@36900
  1481
#1191 := [rewrite]: #1190
boehmes@36900
  1482
#1187 := (iff #426 #1186)
boehmes@36900
  1483
#1184 := (iff #421 #1183)
boehmes@36900
  1484
#1178 := (iff #59 #1177)
boehmes@36900
  1485
#1179 := [rewrite]: #1178
boehmes@36900
  1486
#1185 := [monotonicity #1179]: #1184
boehmes@36900
  1487
#1181 := (iff #58 #1180)
boehmes@36900
  1488
#1182 := [rewrite]: #1181
boehmes@36900
  1489
#1188 := [monotonicity #1182 #1185]: #1187
boehmes@36900
  1490
#1193 := [trans #1188 #1191]: #1192
boehmes@36900
  1491
#1196 := [quant-intro #1193]: #1195
boehmes@36900
  1492
#1175 := (iff #435 #1174)
boehmes@36900
  1493
#1172 := (iff #57 #1171)
boehmes@36900
  1494
#1169 := (iff #56 #1168)
boehmes@36900
  1495
#1170 := [rewrite]: #1169
boehmes@36900
  1496
#1173 := [monotonicity #1170]: #1172
boehmes@36900
  1497
#1176 := [monotonicity #1173]: #1175
boehmes@36900
  1498
#1199 := [monotonicity #1176 #1196]: #1198
boehmes@36900
  1499
#1202 := [quant-intro #1199]: #1201
boehmes@36900
  1500
#1658 := [monotonicity #1202]: #1657
boehmes@36900
  1501
#1676 := [monotonicity #1658 #1673]: #1675
boehmes@36900
  1502
#1681 := [trans #1676 #1679]: #1680
boehmes@36900
  1503
#1684 := [monotonicity #1202 #1681]: #1683
boehmes@36900
  1504
#1163 := (iff #1018 #1162)
boehmes@36900
  1505
#1160 := (iff #415 #1159)
boehmes@36900
  1506
#1157 := (iff #410 #1156)
boehmes@36900
  1507
#1154 := (iff #409 #1153)
boehmes@36900
  1508
#1151 := (iff #401 #1148)
boehmes@36900
  1509
#1145 := (and #1142 #368)
boehmes@36900
  1510
#1149 := (iff #1145 #1148)
boehmes@36900
  1511
#1150 := [rewrite]: #1149
boehmes@36900
  1512
#1146 := (iff #401 #1145)
boehmes@36900
  1513
#1147 := [monotonicity #1144]: #1146
boehmes@36900
  1514
#1152 := [trans #1147 #1150]: #1151
boehmes@36900
  1515
#1155 := [monotonicity #1152]: #1154
boehmes@36900
  1516
#1135 := (iff #53 #1136)
boehmes@36900
  1517
#1134 := [rewrite]: #1135
boehmes@36900
  1518
#1158 := [monotonicity #1134 #1155]: #1157
boehmes@36900
  1519
#1161 := [quant-intro #1158]: #1160
boehmes@36900
  1520
#1164 := [monotonicity #1161]: #1163
boehmes@36900
  1521
#1687 := [monotonicity #1164 #1684]: #1686
boehmes@36900
  1522
#1690 := [monotonicity #1161 #1687]: #1689
boehmes@36900
  1523
#1132 := (iff #1030 #1131)
boehmes@36900
  1524
#1129 := (iff #395 #1128)
boehmes@36900
  1525
#1126 := (iff #390 #1123)
boehmes@36900
  1526
#1120 := (or #1116 #389)
boehmes@36900
  1527
#1124 := (iff #1120 #1123)
boehmes@36900
  1528
#1125 := [rewrite]: #1124
boehmes@36900
  1529
#1121 := (iff #390 #1120)
boehmes@36900
  1530
#1115 := (iff #45 #1116)
boehmes@36900
  1531
#1119 := [rewrite]: #1115
boehmes@36900
  1532
#1122 := [monotonicity #1119]: #1121
boehmes@36900
  1533
#1127 := [trans #1122 #1125]: #1126
boehmes@36900
  1534
#1130 := [quant-intro #1127]: #1129
boehmes@36900
  1535
#1133 := [monotonicity #1130]: #1132
boehmes@36900
  1536
#1693 := [monotonicity #1133 #1690]: #1692
boehmes@36900
  1537
#1696 := [monotonicity #1130 #1693]: #1695
boehmes@36900
  1538
#1112 := (iff #1042 #1111)
boehmes@36900
  1539
#1109 := (iff #40 #1108)
boehmes@36900
  1540
#1105 := (iff #39 #1107)
boehmes@36900
  1541
#1106 := [rewrite]: #1105
boehmes@36900
  1542
#1110 := [quant-intro #1106]: #1109
boehmes@36900
  1543
#1113 := [monotonicity #1110]: #1112
boehmes@36900
  1544
#1699 := [monotonicity #1113 #1696]: #1698
boehmes@36900
  1545
#1702 := [monotonicity #1110 #1699]: #1701
boehmes@36900
  1546
#1103 := (iff #1054 #1102)
boehmes@36900
  1547
#1100 := (iff #377 #38)
boehmes@36900
  1548
#1101 := [rewrite]: #1100
boehmes@36900
  1549
#1104 := [monotonicity #1101]: #1103
boehmes@36900
  1550
#1705 := [monotonicity #1104 #1702]: #1704
boehmes@36900
  1551
#1708 := [monotonicity #1101 #1705]: #1707
boehmes@36900
  1552
#1722 := [monotonicity #1708]: #1721
boehmes@36900
  1553
#1725 := [monotonicity #1722]: #1724
boehmes@36900
  1554
#1718 := (iff #1084 #1717)
boehmes@36900
  1555
#1715 := (iff #351 #1714)
boehmes@36900
  1556
#1712 := (iff #346 #1711)
boehmes@36900
  1557
#1709 := (iff #340 #26)
boehmes@36900
  1558
#1710 := [rewrite]: #1709
boehmes@36900
  1559
#1713 := [monotonicity #1710]: #1712
boehmes@36900
  1560
#1716 := [quant-intro #1713]: #1715
boehmes@36900
  1561
#1719 := [monotonicity #1716]: #1718
boehmes@36900
  1562
#1728 := [monotonicity #1719 #1725]: #1727
boehmes@36900
  1563
#1733 := [trans #1728 #1731]: #1732
boehmes@36900
  1564
#1736 := [monotonicity #1733]: #1735
boehmes@36900
  1565
#1098 := (iff #237 #1097)
boehmes@36900
  1566
#1095 := (iff #236 #1085)
boehmes@36900
  1567
#1090 := (implies true #1085)
boehmes@36900
  1568
#1093 := (iff #1090 #1085)
boehmes@36900
  1569
#1094 := [rewrite]: #1093
boehmes@36900
  1570
#1091 := (iff #236 #1090)
boehmes@36900
  1571
#1088 := (iff #235 #1085)
boehmes@36900
  1572
#1081 := (implies #351 #1076)
boehmes@36900
  1573
#1086 := (iff #1081 #1085)
boehmes@36900
  1574
#1087 := [rewrite]: #1086
boehmes@36900
  1575
#1082 := (iff #235 #1081)
boehmes@36900
  1576
#1079 := (iff #234 #1076)
boehmes@36900
  1577
#1072 := (implies #365 #1067)
boehmes@36900
  1578
#1077 := (iff #1072 #1076)
boehmes@36900
  1579
#1078 := [rewrite]: #1077
boehmes@36900
  1580
#1073 := (iff #234 #1072)
boehmes@36900
  1581
#1070 := (iff #233 #1067)
boehmes@36900
  1582
#1063 := (implies #374 #1060)
boehmes@36900
  1583
#1068 := (iff #1063 #1067)
boehmes@36900
  1584
#1069 := [rewrite]: #1068
boehmes@36900
  1585
#1064 := (iff #233 #1063)
boehmes@36900
  1586
#1061 := (iff #232 #1060)
boehmes@36900
  1587
#1058 := (iff #231 #1055)
boehmes@36900
  1588
#1051 := (implies #377 #1048)
boehmes@36900
  1589
#1056 := (iff #1051 #1055)
boehmes@36900
  1590
#1057 := [rewrite]: #1056
boehmes@36900
  1591
#1052 := (iff #231 #1051)
boehmes@36900
  1592
#1049 := (iff #230 #1048)
boehmes@36900
  1593
#1046 := (iff #229 #1043)
boehmes@36900
  1594
#1039 := (implies #40 #1036)
boehmes@36900
  1595
#1044 := (iff #1039 #1043)
boehmes@36900
  1596
#1045 := [rewrite]: #1044
boehmes@36900
  1597
#1040 := (iff #229 #1039)
boehmes@36900
  1598
#1037 := (iff #228 #1036)
boehmes@36900
  1599
#1034 := (iff #227 #1031)
boehmes@36900
  1600
#1027 := (implies #395 #1024)
boehmes@36900
  1601
#1032 := (iff #1027 #1031)
boehmes@36900
  1602
#1033 := [rewrite]: #1032
boehmes@36900
  1603
#1028 := (iff #227 #1027)
boehmes@36900
  1604
#1025 := (iff #226 #1024)
boehmes@36900
  1605
#1022 := (iff #225 #1019)
boehmes@36900
  1606
#1015 := (implies #415 #1012)
boehmes@36900
  1607
#1020 := (iff #1015 #1019)
boehmes@36900
  1608
#1021 := [rewrite]: #1020
boehmes@36900
  1609
#1016 := (iff #225 #1015)
boehmes@36900
  1610
#1013 := (iff #224 #1012)
boehmes@36900
  1611
#1010 := (iff #223 #1007)
boehmes@36900
  1612
#1003 := (implies #441 #991)
boehmes@36900
  1613
#1008 := (iff #1003 #1007)
boehmes@36900
  1614
#1009 := [rewrite]: #1008
boehmes@36900
  1615
#1004 := (iff #223 #1003)
boehmes@36900
  1616
#1001 := (iff #222 #991)
boehmes@36900
  1617
#996 := (implies true #991)
boehmes@36900
  1618
#999 := (iff #996 #991)
boehmes@36900
  1619
#1000 := [rewrite]: #999
boehmes@36900
  1620
#997 := (iff #222 #996)
boehmes@36900
  1621
#994 := (iff #221 #991)
boehmes@36900
  1622
#987 := (implies #444 #982)
boehmes@34994
  1623
#992 := (iff #987 #991)
boehmes@34994
  1624
#993 := [rewrite]: #992
boehmes@36900
  1625
#988 := (iff #221 #987)
boehmes@36900
  1626
#985 := (iff #220 #982)
boehmes@36900
  1627
#978 := (implies #70 #973)
boehmes@36900
  1628
#983 := (iff #978 #982)
boehmes@36900
  1629
#984 := [rewrite]: #983
boehmes@36900
  1630
#979 := (iff #220 #978)
boehmes@36900
  1631
#976 := (iff #219 #973)
boehmes@36900
  1632
#969 := (implies #468 #964)
boehmes@36900
  1633
#974 := (iff #969 #973)
boehmes@36900
  1634
#975 := [rewrite]: #974
boehmes@36900
  1635
#970 := (iff #219 #969)
boehmes@36900
  1636
#967 := (iff #218 #964)
boehmes@36900
  1637
#960 := (implies #494 #955)
boehmes@36900
  1638
#965 := (iff #960 #964)
boehmes@36900
  1639
#966 := [rewrite]: #965
boehmes@36900
  1640
#961 := (iff #218 #960)
boehmes@36900
  1641
#958 := (iff #217 #955)
boehmes@36900
  1642
#951 := (implies #518 #948)
boehmes@34994
  1643
#956 := (iff #951 #955)
boehmes@34994
  1644
#957 := [rewrite]: #956
boehmes@36900
  1645
#952 := (iff #217 #951)
boehmes@36900
  1646
#949 := (iff #216 #948)
boehmes@36900
  1647
#946 := (iff #215 #936)
boehmes@36900
  1648
#941 := (implies true #936)
boehmes@36900
  1649
#944 := (iff #941 #936)
boehmes@34994
  1650
#945 := [rewrite]: #944
boehmes@36900
  1651
#942 := (iff #215 #941)
boehmes@36900
  1652
#939 := (iff #214 #936)
boehmes@36900
  1653
#933 := (implies #529 #928)
boehmes@36900
  1654
#937 := (iff #933 #936)
boehmes@36900
  1655
#938 := [rewrite]: #937
boehmes@36900
  1656
#934 := (iff #214 #933)
boehmes@36900
  1657
#931 := (iff #213 #928)
boehmes@36900
  1658
#671 := (not #668)
boehmes@36900
  1659
#925 := (implies #671 #920)
boehmes@36900
  1660
#929 := (iff #925 #928)
boehmes@36900
  1661
#930 := [rewrite]: #929
boehmes@36900
  1662
#926 := (iff #213 #925)
boehmes@36900
  1663
#923 := (iff #212 #920)
boehmes@36900
  1664
#916 := (implies #142 #911)
boehmes@36900
  1665
#921 := (iff #916 #920)
boehmes@36900
  1666
#922 := [rewrite]: #921
boehmes@36900
  1667
#917 := (iff #212 #916)
boehmes@36900
  1668
#914 := (iff #211 #911)
boehmes@36900
  1669
#907 := (implies #682 #902)
boehmes@36900
  1670
#912 := (iff #907 #911)
boehmes@36900
  1671
#913 := [rewrite]: #912
boehmes@36900
  1672
#908 := (iff #211 #907)
boehmes@36900
  1673
#905 := (iff #210 #902)
boehmes@36900
  1674
#898 := (implies #148 #893)
boehmes@36900
  1675
#903 := (iff #898 #902)
boehmes@36900
  1676
#904 := [rewrite]: #903
boehmes@36900
  1677
#899 := (iff #210 #898)
boehmes@36900
  1678
#896 := (iff #209 #893)
boehmes@36900
  1679
#889 := (implies #696 #884)
boehmes@36900
  1680
#894 := (iff #889 #893)
boehmes@36900
  1681
#895 := [rewrite]: #894
boehmes@36900
  1682
#890 := (iff #209 #889)
boehmes@36900
  1683
#887 := (iff #208 #884)
boehmes@36900
  1684
#880 := (implies #710 #877)
boehmes@36900
  1685
#885 := (iff #880 #884)
boehmes@36900
  1686
#886 := [rewrite]: #885
boehmes@36900
  1687
#881 := (iff #208 #880)
boehmes@36900
  1688
#878 := (iff #207 #877)
boehmes@36900
  1689
#875 := (iff #206 #872)
boehmes@36900
  1690
#868 := (implies #164 #865)
boehmes@36900
  1691
#873 := (iff #868 #872)
boehmes@36900
  1692
#874 := [rewrite]: #873
boehmes@36900
  1693
#869 := (iff #206 #868)
boehmes@36900
  1694
#866 := (iff #205 #865)
boehmes@36900
  1695
#863 := (iff #204 #860)
boehmes@36900
  1696
#856 := (implies #725 #853)
boehmes@36900
  1697
#861 := (iff #856 #860)
boehmes@34994
  1698
#862 := [rewrite]: #861
boehmes@36900
  1699
#857 := (iff #204 #856)
boehmes@36900
  1700
#854 := (iff #203 #853)
boehmes@36900
  1701
#851 := (iff #202 #848)
boehmes@36900
  1702
#844 := (implies #728 #841)
boehmes@36900
  1703
#849 := (iff #844 #848)
boehmes@36900
  1704
#850 := [rewrite]: #849
boehmes@36900
  1705
#845 := (iff #202 #844)
boehmes@36900
  1706
#842 := (iff #201 #841)
boehmes@36900
  1707
#839 := (iff #200 #836)
boehmes@36900
  1708
#832 := (implies #172 #829)
boehmes@36900
  1709
#837 := (iff #832 #836)
boehmes@36900
  1710
#838 := [rewrite]: #837
boehmes@36900
  1711
#833 := (iff #200 #832)
boehmes@36900
  1712
#830 := (iff #199 #829)
boehmes@36900
  1713
#827 := (iff #198 #824)
boehmes@36900
  1714
#820 := (implies #748 #817)
boehmes@36900
  1715
#825 := (iff #820 #824)
boehmes@36900
  1716
#826 := [rewrite]: #825
boehmes@36900
  1717
#821 := (iff #198 #820)
boehmes@36900
  1718
#818 := (iff #197 #817)
boehmes@36900
  1719
#815 := (iff #196 #812)
boehmes@36900
  1720
#808 := (implies #774 #798)
boehmes@36900
  1721
#813 := (iff #808 #812)
boehmes@36900
  1722
#814 := [rewrite]: #813
boehmes@36900
  1723
#809 := (iff #196 #808)
boehmes@36900
  1724
#806 := (iff #195 #798)
boehmes@36900
  1725
#801 := (and #798 true)
boehmes@36900
  1726
#804 := (iff #801 #798)
boehmes@36900
  1727
#805 := [rewrite]: #804
boehmes@36900
  1728
#802 := (iff #195 #801)
boehmes@36900
  1729
#799 := (iff #194 #798)
boehmes@36900
  1730
#796 := (iff #193 #793)
boehmes@36900
  1731
#789 := (implies #187 #786)
boehmes@36900
  1732
#794 := (iff #789 #793)
boehmes@36900
  1733
#795 := [rewrite]: #794
boehmes@36900
  1734
#790 := (iff #193 #789)
boehmes@36900
  1735
#787 := (iff #192 #786)
boehmes@36900
  1736
#784 := (iff #191 #783)
boehmes@36900
  1737
#781 := (iff #190 #780)
boehmes@36900
  1738
#778 := (iff #189 #777)
boehmes@36900
  1739
#760 := (= #182 #759)
boehmes@36900
  1740
#761 := [rewrite]: #760
boehmes@36900
  1741
#779 := [monotonicity #761]: #778
boehmes@36900
  1742
#714 := (iff #166 #713)
boehmes@36900
  1743
#715 := [rewrite]: #714
boehmes@36900
  1744
#782 := [monotonicity #715 #779]: #781
boehmes@36900
  1745
#785 := [monotonicity #782]: #784
boehmes@36900
  1746
#788 := [quant-intro #785]: #787
boehmes@36900
  1747
#791 := [monotonicity #788]: #790
boehmes@36900
  1748
#797 := [trans #791 #795]: #796
boehmes@36900
  1749
#800 := [quant-intro #797]: #799
boehmes@34994
  1750
#803 := [monotonicity #800]: #802
boehmes@36900
  1751
#807 := [trans #803 #805]: #806
boehmes@36900
  1752
#775 := (iff #185 #774)
boehmes@36900
  1753
#772 := (iff #184 #769)
boehmes@36900
  1754
#765 := (implies #754 #762)
boehmes@36900
  1755
#770 := (iff #765 #769)
boehmes@36900
  1756
#771 := [rewrite]: #770
boehmes@36900
  1757
#766 := (iff #184 #765)
boehmes@36900
  1758
#763 := (iff #183 #762)
boehmes@36900
  1759
#764 := [monotonicity #761]: #763
boehmes@36900
  1760
#757 := (iff #181 #754)
boehmes@36900
  1761
#751 := (and #713 #50)
boehmes@36900
  1762
#755 := (iff #751 #754)
boehmes@36900
  1763
#756 := [rewrite]: #755
boehmes@36900
  1764
#752 := (iff #181 #751)
boehmes@36900
  1765
#753 := [monotonicity #715]: #752
boehmes@36900
  1766
#758 := [trans #753 #756]: #757
boehmes@36900
  1767
#767 := [monotonicity #758 #764]: #766
boehmes@36900
  1768
#773 := [trans #767 #771]: #772
boehmes@36900
  1769
#776 := [quant-intro #773]: #775
boehmes@36900
  1770
#810 := [monotonicity #776 #807]: #809
boehmes@36900
  1771
#816 := [trans #810 #814]: #815
boehmes@36900
  1772
#819 := [monotonicity #776 #816]: #818
boehmes@36900
  1773
#749 := (iff #180 #748)
boehmes@36900
  1774
#746 := (iff #179 #743)
boehmes@36900
  1775
#739 := (implies #736 #178)
boehmes@36900
  1776
#744 := (iff #739 #743)
boehmes@36900
  1777
#745 := [rewrite]: #744
boehmes@36900
  1778
#740 := (iff #179 #739)
boehmes@36900
  1779
#737 := (iff #176 #736)
boehmes@36900
  1780
#734 := (iff #175 #733)
boehmes@36900
  1781
#735 := [rewrite]: #734
boehmes@36900
  1782
#731 := (iff #173 #719)
boehmes@36900
  1783
#732 := [monotonicity #715]: #731
boehmes@36900
  1784
#738 := [monotonicity #732 #735]: #737
boehmes@36900
  1785
#741 := [monotonicity #738]: #740
boehmes@36900
  1786
#747 := [trans #741 #745]: #746
boehmes@36900
  1787
#750 := [quant-intro #747]: #749
boehmes@36900
  1788
#822 := [monotonicity #750 #819]: #821
boehmes@36900
  1789
#828 := [trans #822 #826]: #827
boehmes@36900
  1790
#831 := [monotonicity #750 #828]: #830
boehmes@36900
  1791
#834 := [monotonicity #831]: #833
boehmes@36900
  1792
#840 := [trans #834 #838]: #839
boehmes@36900
  1793
#843 := [monotonicity #840]: #842
boehmes@36900
  1794
#729 := (iff #170 #728)
boehmes@36900
  1795
#730 := [rewrite]: #729
boehmes@36900
  1796
#846 := [monotonicity #730 #843]: #845
boehmes@36900
  1797
#852 := [trans #846 #850]: #851
boehmes@36900
  1798
#855 := [monotonicity #730 #852]: #854
boehmes@36900
  1799
#726 := (iff #168 #725)
boehmes@36900
  1800
#723 := (iff #167 #720)
boehmes@36900
  1801
#716 := (implies #713 #699)
boehmes@36900
  1802
#721 := (iff #716 #720)
boehmes@36900
  1803
#722 := [rewrite]: #721
boehmes@36900
  1804
#717 := (iff #167 #716)
boehmes@36900
  1805
#700 := (iff #160 #699)
boehmes@36900
  1806
#701 := [rewrite]: #700
boehmes@36900
  1807
#718 := [monotonicity #715 #701]: #717
boehmes@36900
  1808
#724 := [trans #718 #722]: #723
boehmes@36900
  1809
#727 := [quant-intro #724]: #726
boehmes@36900
  1810
#858 := [monotonicity #727 #855]: #857
boehmes@36900
  1811
#864 := [trans #858 #862]: #863
boehmes@36900
  1812
#867 := [monotonicity #727 #864]: #866
boehmes@36900
  1813
#870 := [monotonicity #867]: #869
boehmes@36900
  1814
#876 := [trans #870 #874]: #875
boehmes@36900
  1815
#879 := [monotonicity #876]: #878
boehmes@36900
  1816
#711 := (iff #162 #710)
boehmes@36900
  1817
#708 := (iff #161 #705)
boehmes@36900
  1818
#702 := (implies #159 #699)
boehmes@36900
  1819
#706 := (iff #702 #705)
boehmes@36900
  1820
#707 := [rewrite]: #706
boehmes@36900
  1821
#703 := (iff #161 #702)
boehmes@36900
  1822
#704 := [monotonicity #701]: #703
boehmes@36900
  1823
#709 := [trans #704 #707]: #708
boehmes@36900
  1824
#712 := [quant-intro #709]: #711
boehmes@36900
  1825
#882 := [monotonicity #712 #879]: #881
boehmes@36900
  1826
#888 := [trans #882 #886]: #887
boehmes@36900
  1827
#697 := (iff #158 #696)
boehmes@36900
  1828
#694 := (iff #157 #691)
boehmes@36900
  1829
#688 := (implies #154 #685)
boehmes@36900
  1830
#692 := (iff #688 #691)
boehmes@36900
  1831
#693 := [rewrite]: #692
boehmes@36900
  1832
#689 := (iff #157 #688)
boehmes@36900
  1833
#686 := (iff #156 #685)
boehmes@36900
  1834
#687 := [rewrite]: #686
boehmes@36900
  1835
#690 := [monotonicity #687]: #689
boehmes@36900
  1836
#695 := [trans #690 #693]: #694
boehmes@36900
  1837
#698 := [quant-intro #695]: #697
boehmes@36900
  1838
#891 := [monotonicity #698 #888]: #890
boehmes@36900
  1839
#897 := [trans #891 #895]: #896
boehmes@36900
  1840
#900 := [monotonicity #897]: #899
boehmes@36900
  1841
#906 := [trans #900 #904]: #905
boehmes@36900
  1842
#683 := (iff #145 #682)
boehmes@36900
  1843
#680 := (iff #144 #677)
boehmes@36900
  1844
#674 := (implies #450 #143)
boehmes@36900
  1845
#678 := (iff #674 #677)
boehmes@36900
  1846
#679 := [rewrite]: #678
boehmes@36900
  1847
#675 := (iff #144 #674)
boehmes@36900
  1848
#451 := (iff #74 #450)
boehmes@36900
  1849
#448 := (iff #73 #447)
boehmes@34994
  1850
#449 := [rewrite]: #448
boehmes@36900
  1851
#452 := [monotonicity #449]: #451
boehmes@36900
  1852
#676 := [monotonicity #452]: #675
boehmes@36900
  1853
#681 := [trans #676 #679]: #680
boehmes@36900
  1854
#684 := [quant-intro #681]: #683
boehmes@36900
  1855
#909 := [monotonicity #684 #906]: #908
boehmes@36900
  1856
#915 := [trans #909 #913]: #914
boehmes@36900
  1857
#918 := [monotonicity #915]: #917
boehmes@36900
  1858
#924 := [trans #918 #922]: #923
boehmes@36900
  1859
#672 := (iff #140 #671)
boehmes@36900
  1860
#669 := (iff #139 #668)
boehmes@36900
  1861
#670 := [rewrite]: #669
boehmes@36900
  1862
#673 := [monotonicity #670]: #672
boehmes@36900
  1863
#927 := [monotonicity #673 #924]: #926
boehmes@36900
  1864
#932 := [trans #927 #930]: #931
boehmes@36900
  1865
#530 := (iff #97 #529)
boehmes@36900
  1866
#527 := (iff #96 #524)
boehmes@36900
  1867
#521 := (and #450 #87)
boehmes@36900
  1868
#525 := (iff #521 #524)
boehmes@36900
  1869
#526 := [rewrite]: #525
boehmes@36900
  1870
#522 := (iff #96 #521)
boehmes@36900
  1871
#523 := [monotonicity #452]: #522
boehmes@36900
  1872
#528 := [trans #523 #526]: #527
boehmes@36900
  1873
#531 := [quant-intro #528]: #530
boehmes@36900
  1874
#935 := [monotonicity #531 #932]: #934
boehmes@36900
  1875
#940 := [trans #935 #938]: #939
boehmes@36900
  1876
#943 := [monotonicity #940]: #942
boehmes@36900
  1877
#947 := [trans #943 #945]: #946
boehmes@36900
  1878
#666 := (iff #136 #656)
boehmes@36900
  1879
#661 := (implies true #656)
boehmes@36900
  1880
#664 := (iff #661 #656)
boehmes@36900
  1881
#665 := [rewrite]: #664
boehmes@36900
  1882
#662 := (iff #136 #661)
boehmes@36900
  1883
#659 := (iff #135 #656)
boehmes@36900
  1884
#653 := (implies #532 #648)
boehmes@36900
  1885
#657 := (iff #653 #656)
boehmes@36900
  1886
#658 := [rewrite]: #657
boehmes@36900
  1887
#654 := (iff #135 #653)
boehmes@36900
  1888
#651 := (iff #134 #648)
boehmes@36900
  1889
#644 := (implies #535 #639)
boehmes@36900
  1890
#649 := (iff #644 #648)
boehmes@36900
  1891
#650 := [rewrite]: #649
boehmes@36900
  1892
#645 := (iff #134 #644)
boehmes@36900
  1893
#642 := (iff #133 #639)
boehmes@36900
  1894
#635 := (implies #103 #630)
boehmes@36900
  1895
#640 := (iff #635 #639)
boehmes@36900
  1896
#641 := [rewrite]: #640
boehmes@36900
  1897
#636 := (iff #133 #635)
boehmes@36900
  1898
#633 := (iff #132 #630)
boehmes@36900
  1899
#626 := (implies #538 #621)
boehmes@36900
  1900
#631 := (iff #626 #630)
boehmes@36900
  1901
#632 := [rewrite]: #631
boehmes@36900
  1902
#627 := (iff #132 #626)
boehmes@36900
  1903
#624 := (iff #131 #621)
boehmes@36900
  1904
#617 := (implies #108 #614)
boehmes@36900
  1905
#622 := (iff #617 #621)
boehmes@36900
  1906
#623 := [rewrite]: #622
boehmes@36900
  1907
#618 := (iff #131 #617)
boehmes@36900
  1908
#615 := (iff #130 #614)
boehmes@36900
  1909
#612 := (iff #129 #609)
boehmes@36900
  1910
#605 := (implies #562 #602)
boehmes@36900
  1911
#610 := (iff #605 #609)
boehmes@36900
  1912
#611 := [rewrite]: #610
boehmes@36900
  1913
#606 := (iff #129 #605)
boehmes@36900
  1914
#603 := (iff #128 #602)
boehmes@36900
  1915
#600 := (iff #127 #597)
boehmes@36900
  1916
#593 := (implies #580 #583)
boehmes@36900
  1917
#598 := (iff #593 #597)
boehmes@36900
  1918
#599 := [rewrite]: #598
boehmes@36900
  1919
#594 := (iff #127 #593)
boehmes@36900
  1920
#591 := (iff #126 #583)
boehmes@36900
  1921
#586 := (and #583 true)
boehmes@36900
  1922
#589 := (iff #586 #583)
boehmes@36900
  1923
#590 := [rewrite]: #589
boehmes@36900
  1924
#587 := (iff #126 #586)
boehmes@36900
  1925
#584 := (iff #125 #583)
boehmes@36900
  1926
#585 := [rewrite]: #584
boehmes@36900
  1927
#588 := [monotonicity #585]: #587
boehmes@36900
  1928
#592 := [trans #588 #590]: #591
boehmes@36900
  1929
#581 := (iff #123 #580)
boehmes@36900
  1930
#578 := (iff #122 #575)
boehmes@36900
  1931
#571 := (implies #565 #568)
boehmes@36900
  1932
#576 := (iff #571 #575)
boehmes@36900
  1933
#577 := [rewrite]: #576
boehmes@36900
  1934
#572 := (iff #122 #571)
boehmes@36900
  1935
#569 := (iff #121 #568)
boehmes@36900
  1936
#542 := (= #114 #541)
boehmes@36900
  1937
#543 := [rewrite]: #542
boehmes@36900
  1938
#570 := [monotonicity #543]: #569
boehmes@36900
  1939
#566 := (iff #120 #565)
boehmes@36900
  1940
#567 := [rewrite]: #566
boehmes@36900
  1941
#573 := [monotonicity #567 #570]: #572
boehmes@36900
  1942
#579 := [trans #573 #577]: #578
boehmes@36900
  1943
#582 := [quant-intro #579]: #581
boehmes@36900
  1944
#595 := [monotonicity #582 #592]: #594
boehmes@36900
  1945
#601 := [trans #595 #599]: #600
boehmes@36900
  1946
#604 := [monotonicity #582 #601]: #603
boehmes@36900
  1947
#563 := (iff #119 #562)
boehmes@36900
  1948
#560 := (iff #118 #557)
boehmes@36900
  1949
#553 := (implies #111 #550)
boehmes@36900
  1950
#558 := (iff #553 #557)
boehmes@36900
  1951
#559 := [rewrite]: #558
boehmes@36900
  1952
#554 := (iff #118 #553)
boehmes@36900
  1953
#551 := (iff #117 #550)
boehmes@36900
  1954
#548 := (iff #116 #547)
boehmes@36900
  1955
#545 := (iff #115 #544)
boehmes@36900
  1956
#546 := [monotonicity #543]: #545
boehmes@36900
  1957
#549 := [monotonicity #546]: #548
boehmes@36900
  1958
#552 := [quant-intro #549]: #551
boehmes@36900
  1959
#555 := [monotonicity #552]: #554
boehmes@36900
  1960
#561 := [trans #555 #559]: #560
boehmes@36900
  1961
#564 := [quant-intro #561]: #563
boehmes@36900
  1962
#607 := [monotonicity #564 #604]: #606
boehmes@36900
  1963
#613 := [trans #607 #611]: #612
boehmes@36900
  1964
#616 := [monotonicity #564 #613]: #615
boehmes@36900
  1965
#619 := [monotonicity #616]: #618
boehmes@36900
  1966
#625 := [trans #619 #623]: #624
boehmes@36900
  1967
#539 := (iff #105 #538)
boehmes@36900
  1968
#540 := [rewrite]: #539
boehmes@36900
  1969
#628 := [monotonicity #540 #625]: #627
boehmes@36900
  1970
#634 := [trans #628 #632]: #633
boehmes@36900
  1971
#637 := [monotonicity #634]: #636
boehmes@36900
  1972
#643 := [trans #637 #641]: #642
boehmes@36900
  1973
#536 := (iff #100 #535)
boehmes@36900
  1974
#537 := [rewrite]: #536
boehmes@36900
  1975
#646 := [monotonicity #537 #643]: #645
boehmes@36900
  1976
#652 := [trans #646 #650]: #651
boehmes@36900
  1977
#533 := (iff #98 #532)
boehmes@36900
  1978
#534 := [monotonicity #531]: #533
boehmes@36900
  1979
#655 := [monotonicity #534 #652]: #654
boehmes@36900
  1980
#660 := [trans #655 #658]: #659
boehmes@36900
  1981
#663 := [monotonicity #660]: #662
boehmes@36900
  1982
#667 := [trans #663 #665]: #666
boehmes@36900
  1983
#950 := [monotonicity #667 #947]: #949
boehmes@36900
  1984
#519 := (iff #95 #518)
boehmes@36900
  1985
#516 := (iff #94 #513)
boehmes@36900
  1986
#509 := (implies #88 #506)
boehmes@36900
  1987
#514 := (iff #509 #513)
boehmes@36900
  1988
#515 := [rewrite]: #514
boehmes@36900
  1989
#510 := (iff #94 #509)
boehmes@36900
  1990
#507 := (iff #93 #506)
boehmes@36900
  1991
#504 := (iff #92 #503)
boehmes@36900
  1992
#501 := (iff #91 #500)
boehmes@36900
  1993
#498 := (iff #90 #497)
boehmes@36900
  1994
#480 := (= #83 #479)
boehmes@36900
  1995
#481 := [rewrite]: #480
boehmes@36900
  1996
#499 := [monotonicity #481]: #498
boehmes@36900
  1997
#502 := [monotonicity #449 #499]: #501
boehmes@36900
  1998
#505 := [monotonicity #502]: #504
boehmes@36900
  1999
#508 := [quant-intro #505]: #507
boehmes@36900
  2000
#511 := [monotonicity #508]: #510
boehmes@36900
  2001
#517 := [trans #511 #515]: #516
boehmes@36900
  2002
#520 := [quant-intro #517]: #519
boehmes@36900
  2003
#953 := [monotonicity #520 #950]: #952
boehmes@34994
  2004
#959 := [trans #953 #957]: #958
boehmes@36900
  2005
#495 := (iff #86 #494)
boehmes@36900
  2006
#492 := (iff #85 #489)
boehmes@36900
  2007
#485 := (implies #474 #482)
boehmes@36900
  2008
#490 := (iff #485 #489)
boehmes@36900
  2009
#491 := [rewrite]: #490
boehmes@36900
  2010
#486 := (iff #85 #485)
boehmes@36900
  2011
#483 := (iff #84 #482)
boehmes@36900
  2012
#484 := [monotonicity #481]: #483
boehmes@36900
  2013
#477 := (iff #82 #474)
boehmes@36900
  2014
#471 := (and #447 #50)
boehmes@36900
  2015
#475 := (iff #471 #474)
boehmes@36900
  2016
#476 := [rewrite]: #475
boehmes@36900
  2017
#472 := (iff #82 #471)
boehmes@36900
  2018
#473 := [monotonicity #449]: #472
boehmes@36900
  2019
#478 := [trans #473 #476]: #477
boehmes@36900
  2020
#487 := [monotonicity #478 #484]: #486
boehmes@36900
  2021
#493 := [trans #487 #491]: #492
boehmes@36900
  2022
#496 := [quant-intro #493]: #495
boehmes@36900
  2023
#962 := [monotonicity #496 #959]: #961
boehmes@36900
  2024
#968 := [trans #962 #966]: #967
boehmes@36900
  2025
#469 := (iff #81 #468)
boehmes@36900
  2026
#466 := (iff #80 #463)
boehmes@36900
  2027
#459 := (implies #456 #79)
boehmes@36900
  2028
#464 := (iff #459 #463)
boehmes@36900
  2029
#465 := [rewrite]: #464
boehmes@36900
  2030
#460 := (iff #80 #459)
boehmes@36900
  2031
#457 := (iff #77 #456)
boehmes@36900
  2032
#454 := (iff #76 #453)
boehmes@36900
  2033
#455 := [rewrite]: #454
boehmes@36900
  2034
#458 := [monotonicity #452 #455]: #457
boehmes@36900
  2035
#461 := [monotonicity #458]: #460
boehmes@36900
  2036
#467 := [trans #461 #465]: #466
boehmes@36900
  2037
#470 := [quant-intro #467]: #469
boehmes@36900
  2038
#971 := [monotonicity #470 #968]: #970
boehmes@36900
  2039
#977 := [trans #971 #975]: #976
boehmes@36900
  2040
#980 := [monotonicity #977]: #979
boehmes@36900
  2041
#986 := [trans #980 #984]: #985
boehmes@36900
  2042
#445 := (iff #67 #444)
boehmes@36900
  2043
#446 := [rewrite]: #445
boehmes@36900
  2044
#989 := [monotonicity #446 #986]: #988
boehmes@34994
  2045
#995 := [trans #989 #993]: #994
boehmes@36900
  2046
#998 := [monotonicity #995]: #997
boehmes@36900
  2047
#1002 := [trans #998 #1000]: #1001
boehmes@36900
  2048
#442 := (iff #64 #441)
boehmes@36900
  2049
#439 := (iff #63 #436)
boehmes@36900
  2050
#432 := (implies #57 #429)
boehmes@36900
  2051
#437 := (iff #432 #436)
boehmes@36900
  2052
#438 := [rewrite]: #437
boehmes@36900
  2053
#433 := (iff #63 #432)
boehmes@36900
  2054
#430 := (iff #62 #429)
boehmes@36900
  2055
#427 := (iff #61 #426)
boehmes@36900
  2056
#424 := (iff #60 #421)
boehmes@36900
  2057
#418 := (and #368 #59)
boehmes@36900
  2058
#422 := (iff #418 #421)
boehmes@36900
  2059
#423 := [rewrite]: #422
boehmes@36900
  2060
#419 := (iff #60 #418)
boehmes@36900
  2061
#369 := (iff #34 #368)
boehmes@36900
  2062
#370 := [rewrite]: #369
boehmes@36900
  2063
#420 := [monotonicity #370]: #419
boehmes@36900
  2064
#425 := [trans #420 #423]: #424
boehmes@36900
  2065
#428 := [monotonicity #425]: #427
boehmes@36900
  2066
#431 := [quant-intro #428]: #430
boehmes@36900
  2067
#434 := [monotonicity #431]: #433
boehmes@36900
  2068
#440 := [trans #434 #438]: #439
boehmes@36900
  2069
#443 := [quant-intro #440]: #442
boehmes@36900
  2070
#1005 := [monotonicity #443 #1002]: #1004
boehmes@36900
  2071
#1011 := [trans #1005 #1009]: #1010
boehmes@36900
  2072
#1014 := [monotonicity #443 #1011]: #1013
boehmes@36900
  2073
#416 := (iff #55 #415)
boehmes@36900
  2074
#413 := (iff #54 #410)
boehmes@36900
  2075
#406 := (implies #401 #53)
boehmes@36900
  2076
#411 := (iff #406 #410)
boehmes@36900
  2077
#412 := [rewrite]: #411
boehmes@36900
  2078
#407 := (iff #54 #406)
boehmes@36900
  2079
#404 := (iff #51 #401)
boehmes@36900
  2080
#398 := (and #368 #50)
boehmes@36900
  2081
#402 := (iff #398 #401)
boehmes@36900
  2082
#403 := [rewrite]: #402
boehmes@36900
  2083
#399 := (iff #51 #398)
boehmes@36900
  2084
#400 := [monotonicity #370]: #399
boehmes@36900
  2085
#405 := [trans #400 #403]: #404
boehmes@36900
  2086
#408 := [monotonicity #405]: #407
boehmes@36900
  2087
#414 := [trans #408 #412]: #413
boehmes@36900
  2088
#417 := [quant-intro #414]: #416
boehmes@36900
  2089
#1017 := [monotonicity #417 #1014]: #1016
boehmes@36900
  2090
#1023 := [trans #1017 #1021]: #1022
boehmes@36900
  2091
#1026 := [monotonicity #417 #1023]: #1025
boehmes@36900
  2092
#396 := (iff #47 #395)
boehmes@36900
  2093
#393 := (iff #46 #390)
boehmes@36900
  2094
#386 := (implies #383 #45)
boehmes@36900
  2095
#391 := (iff #386 #390)
boehmes@36900
  2096
#392 := [rewrite]: #391
boehmes@36900
  2097
#387 := (iff #46 #386)
boehmes@36900
  2098
#384 := (iff #43 #383)
boehmes@36900
  2099
#381 := (iff #42 #380)
boehmes@36900
  2100
#382 := [rewrite]: #381
boehmes@36900
  2101
#372 := (iff #35 #371)
boehmes@36900
  2102
#373 := [monotonicity #370]: #372
boehmes@36900
  2103
#385 := [monotonicity #373 #382]: #384
boehmes@36900
  2104
#388 := [monotonicity #385]: #387
boehmes@36900
  2105
#394 := [trans #388 #392]: #393
boehmes@36900
  2106
#397 := [quant-intro #394]: #396
boehmes@36900
  2107
#1029 := [monotonicity #397 #1026]: #1028
boehmes@36900
  2108
#1035 := [trans #1029 #1033]: #1034
boehmes@36900
  2109
#1038 := [monotonicity #397 #1035]: #1037
boehmes@36900
  2110
#1041 := [monotonicity #1038]: #1040
boehmes@36900
  2111
#1047 := [trans #1041 #1045]: #1046
boehmes@36900
  2112
#1050 := [monotonicity #1047]: #1049
boehmes@36900
  2113
#378 := (iff #38 #377)
boehmes@36900
  2114
#379 := [rewrite]: #378
boehmes@36900
  2115
#1053 := [monotonicity #379 #1050]: #1052
boehmes@36900
  2116
#1059 := [trans #1053 #1057]: #1058
boehmes@36900
  2117
#1062 := [monotonicity #379 #1059]: #1061
boehmes@36900
  2118
#375 := (iff #36 #374)
boehmes@36900
  2119
#376 := [quant-intro #373]: #375
boehmes@36900
  2120
#1065 := [monotonicity #376 #1062]: #1064
boehmes@36900
  2121
#1071 := [trans #1065 #1069]: #1070
boehmes@36900
  2122
#366 := (iff #32 #365)
boehmes@36900
  2123
#363 := (iff #31 #360)
boehmes@36900
  2124
#357 := (implies #29 #354)
boehmes@36900
  2125
#361 := (iff #357 #360)
boehmes@36900
  2126
#362 := [rewrite]: #361
boehmes@36900
  2127
#358 := (iff #31 #357)
boehmes@36900
  2128
#355 := (iff #30 #354)
boehmes@36900
  2129
#356 := [rewrite]: #355
boehmes@36900
  2130
#359 := [monotonicity #356]: #358
boehmes@36900
  2131
#364 := [trans #359 #362]: #363
boehmes@36900
  2132
#367 := [quant-intro #364]: #366
boehmes@36900
  2133
#1074 := [monotonicity #367 #1071]: #1073
boehmes@36900
  2134
#1080 := [trans #1074 #1078]: #1079
boehmes@36900
  2135
#352 := (iff #28 #351)
boehmes@36900
  2136
#349 := (iff #27 #346)
boehmes@36900
  2137
#343 := (implies #24 #340)
boehmes@36900
  2138
#347 := (iff #343 #346)
boehmes@36900
  2139
#348 := [rewrite]: #347
boehmes@36900
  2140
#344 := (iff #27 #343)
boehmes@36900
  2141
#341 := (iff #26 #340)
boehmes@36900
  2142
#342 := [rewrite]: #341
boehmes@36900
  2143
#345 := [monotonicity #342]: #344
boehmes@36900
  2144
#350 := [trans #345 #348]: #349
boehmes@36900
  2145
#353 := [quant-intro #350]: #352
boehmes@36900
  2146
#1083 := [monotonicity #353 #1080]: #1082
boehmes@36900
  2147
#1089 := [trans #1083 #1087]: #1088
boehmes@36900
  2148
#1092 := [monotonicity #1089]: #1091
boehmes@36900
  2149
#1096 := [trans #1092 #1094]: #1095
boehmes@36900
  2150
#1099 := [monotonicity #1096]: #1098
boehmes@36900
  2151
#1738 := [trans #1099 #1736]: #1737
boehmes@36900
  2152
#339 := [asserted]: #237
boehmes@36900
  2153
#1739 := [mp #339 #1738]: #1734
boehmes@36900
  2154
#1744 := [not-or-elim #1739]: #1714
boehmes@36900
  2155
#2002 := [mp~ #1744 #2168]: #1714
boehmes@36900
  2156
#4540 := [mp #2002 #4539]: #4535
boehmes@36900
  2157
#4634 := [hypothesis]: #1102
boehmes@36900
  2158
#4588 := (not #4535)
boehmes@36900
  2159
#4586 := (or #4588 #38)
boehmes@36900
  2160
#3871 := (= f6 f6)
boehmes@36900
  2161
#3836 := (not #3871)
boehmes@36900
  2162
#3837 := (or #3836 #38)
boehmes@36900
  2163
#4589 := (or #4588 #3837)
boehmes@36900
  2164
#4591 := (iff #4589 #4586)
boehmes@36900
  2165
#4630 := (iff #4586 #4586)
boehmes@36900
  2166
#4631 := [rewrite]: #4630
boehmes@36900
  2167
#4587 := (iff #3837 #38)
boehmes@36900
  2168
#3800 := (or false #38)
boehmes@36900
  2169
#4577 := (iff #3800 #38)
boehmes@36900
  2170
#4585 := [rewrite]: #4577
boehmes@36900
  2171
#3801 := (iff #3837 #3800)
boehmes@36900
  2172
#3796 := (iff #3836 false)
boehmes@36900
  2173
#9474 := (not true)
boehmes@36900
  2174
#9477 := (iff #9474 false)
boehmes@36900
  2175
#9478 := [rewrite]: #9477
boehmes@36900
  2176
#3795 := (iff #3836 #9474)
boehmes@36900
  2177
#3840 := (iff #3871 true)
boehmes@36900
  2178
#3821 := [rewrite]: #3840
boehmes@36900
  2179
#3835 := [monotonicity #3821]: #3795
boehmes@36900
  2180
#3787 := [trans #3835 #9478]: #3796
boehmes@36900
  2181
#3793 := [monotonicity #3787]: #3801
boehmes@36900
  2182
#4578 := [trans #3793 #4585]: #4587
boehmes@36900
  2183
#3911 := [monotonicity #4578]: #4591
boehmes@36900
  2184
#4632 := [trans #3911 #4631]: #4591
boehmes@36900
  2185
#4590 := [quant-inst]: #4589
boehmes@36900
  2186
#4633 := [mp #4590 #4632]: #4586
boehmes@36900
  2187
#4635 := [unit-resolution #4633 #4634 #4540]: false
boehmes@36900
  2188
#4636 := [lemma #4635]: #38
boehmes@36900
  2189
#4531 := (or #1102 #4528)
boehmes@36900
  2190
#3492 := (forall (vars (?v1 S2)) #3481)
boehmes@36900
  2191
#3499 := (not #3492)
boehmes@36900
  2192
#3477 := (forall (vars (?v0 S2) (?v1 S2)) #3472)
boehmes@36900
  2193
#3498 := (not #3477)
boehmes@36900
  2194
#3500 := (or #2308 #2875 #3498 #3499)
boehmes@36900
  2195
#3501 := (not #3500)
boehmes@36900
  2196
#3506 := (or #3455 #3501)
boehmes@36900
  2197
#3513 := (not #3506)
boehmes@36900
  2198
#3432 := (forall (vars (?v0 S2) (?v1 S2)) #3427)
boehmes@36900
  2199
#3512 := (not #3432)
boehmes@36900
  2200
#3514 := (or #3512 #3513)
boehmes@36900
  2201
#3515 := (not #3514)
boehmes@36900
  2202
#3520 := (or #3409 #3515)
boehmes@36900
  2203
#3526 := (not #3520)
boehmes@36900
  2204
#3527 := (or #1405 #3526)
boehmes@36900
  2205
#3528 := (not #3527)
boehmes@36900
  2206
#3533 := (or #2225 #3528)
boehmes@36900
  2207
#3539 := (not #3533)
boehmes@36900
  2208
#3540 := (or #1396 #3539)
boehmes@36900
  2209
#3541 := (not #3540)
boehmes@36900
  2210
#3546 := (or #1396 #3541)
boehmes@36900
  2211
#3552 := (not #3546)
boehmes@36900
  2212
#3553 := (or #859 #3552)
boehmes@36900
  2213
#3554 := (not #3553)
boehmes@36900
  2214
#3559 := (or #2818 #3554)
boehmes@36900
  2215
#3565 := (not #3559)
boehmes@36900
  2216
#3566 := (or #1391 #3565)
boehmes@36900
  2217
#3567 := (not #3566)
boehmes@36900
  2218
#3572 := (or #2804 #3567)
boehmes@36900
  2219
#3580 := (not #3572)
boehmes@36900
  2220
#3386 := (forall (vars (?v0 S2)) #3381)
boehmes@36900
  2221
#3579 := (not #3386)
boehmes@36900
  2222
#3368 := (forall (vars (?v0 S2)) #3365)
boehmes@36900
  2223
#3578 := (not #3368)
boehmes@36900
  2224
#3581 := (or #901 #668 #1556 #1560 #2159 #2162 #3578 #3579 #3580)
boehmes@36900
  2225
#3582 := (not #3581)
boehmes@36900
  2226
#3298 := (forall (vars (?v0 S2) (?v1 S2)) #3293)
boehmes@36900
  2227
#3304 := (not #3298)
boehmes@36900
  2228
#3305 := (or #125 #3304)
boehmes@36900
  2229
#3306 := (not #3305)
boehmes@36900
  2230
#3333 := (or #3306 #3330)
boehmes@36900
  2231
#3340 := (not #3333)
boehmes@36900
  2232
#3276 := (forall (vars (?v0 S2)) #3271)
boehmes@36900
  2233
#3339 := (not #3276)
boehmes@36900
  2234
#3341 := (or #3339 #3340)
boehmes@36900
  2235
#3342 := (not #3341)
boehmes@36900
  2236
#3239 := (forall (vars (?v1 S2)) #3228)
boehmes@36900
  2237
#3245 := (not #3239)
boehmes@36900
  2238
#3246 := (or #2038 #2653 #3245)
boehmes@36900
  2239
#3247 := (not #3246)
boehmes@36900
  2240
#3347 := (or #3247 #3342)
boehmes@36900
  2241
#3354 := (not #3347)
boehmes@36900
  2242
#3224 := (forall (vars (?v0 S2)) #3213)
boehmes@36900
  2243
#3353 := (not #3224)
boehmes@36900
  2244
#3355 := (or #638 #620 #647 #629 #3353 #3354)
boehmes@36900
  2245
#3356 := (not #3355)
boehmes@36900
  2246
#3587 := (or #3356 #3582)
boehmes@36900
  2247
#3597 := (not #3587)
boehmes@36900
  2248
#3210 := (forall (vars (?v0 S2)) #3205)
boehmes@36900
  2249
#3596 := (not #3210)
boehmes@36900
  2250
#3182 := (forall (vars (?v0 S2)) #3177)
boehmes@36900
  2251
#3595 := (not #3182)
boehmes@36900
  2252
#3154 := (forall (vars (?v0 S2) (?v1 S2)) #3149)
boehmes@36900
  2253
#3594 := (not #3154)
boehmes@36900
  2254
#3131 := (forall (vars (?v0 S2) (?v1 S2)) #3126)
boehmes@36900
  2255
#3593 := (not #3131)
boehmes@36900
  2256
#3598 := (or #1653 #1648 #3593 #3594 #3595 #3596 #3597)
boehmes@36900
  2257
#3599 := (not #3598)
boehmes@36900
  2258
#3099 := (forall (vars (?v1 S2)) #3088)
boehmes@36900
  2259
#3105 := (not #3099)
boehmes@36900
  2260
#3106 := (or #1930 #2515 #3105)
boehmes@36900
  2261
#3107 := (not #3106)
boehmes@36900
  2262
#3604 := (or #3107 #3599)
boehmes@36900
  2263
#3611 := (not #3604)
boehmes@36900
  2264
#3084 := (forall (vars (?v0 S2) (?v1 S2)) #3079)
boehmes@36900
  2265
#3610 := (not #3084)
boehmes@36900
  2266
#3612 := (or #3610 #3611)
boehmes@36900
  2267
#3613 := (not #3612)
boehmes@36900
  2268
#3618 := (or #3062 #3613)
boehmes@36900
  2269
#3625 := (not #3618)
boehmes@36900
  2270
#3039 := (forall (vars (?v0 S2) (?v1 S2)) #3034)
boehmes@36900
  2271
#3624 := (not #3039)
boehmes@36900
  2272
#3626 := (or #3624 #3625)
boehmes@36900
  2273
#3627 := (not #3626)
boehmes@36900
  2274
#3632 := (or #3016 #3627)
boehmes@36900
  2275
#3638 := (not #3632)
boehmes@36900
  2276
#3639 := (or #1111 #3638)
boehmes@36900
  2277
#3640 := (not #3639)
boehmes@36900
  2278
#3645 := (or #1846 #3640)
boehmes@36900
  2279
#3651 := (not #3645)
boehmes@36900
  2280
#3652 := (or #1102 #3651)
boehmes@36900
  2281
#3653 := (not #3652)
boehmes@36900
  2282
#3658 := (or #1102 #3653)
boehmes@36900
  2283
#4532 := (iff #3658 #4531)
boehmes@36900
  2284
#4529 := (iff #3653 #4528)
boehmes@36900
  2285
#4526 := (iff #3652 #4525)
boehmes@36900
  2286
#4523 := (iff #3651 #4522)
boehmes@36900
  2287
#4520 := (iff #3645 #4519)
boehmes@36900
  2288
#4517 := (iff #3640 #4516)
boehmes@36900
  2289
#4514 := (iff #3639 #4513)
boehmes@36900
  2290
#4511 := (iff #3638 #4510)
boehmes@36900
  2291
#4508 := (iff #3632 #4507)
boehmes@36900
  2292
#4505 := (iff #3627 #4504)
boehmes@36900
  2293
#4502 := (iff #3626 #4501)
boehmes@36900
  2294
#4499 := (iff #3625 #4498)
boehmes@36900
  2295
#4496 := (iff #3618 #4495)
boehmes@36900
  2296
#4493 := (iff #3613 #4492)
boehmes@36900
  2297
#4490 := (iff #3612 #4489)
boehmes@36900
  2298
#4487 := (iff #3611 #4486)
boehmes@36900
  2299
#4484 := (iff #3604 #4483)
boehmes@36900
  2300
#4481 := (iff #3599 #4480)
boehmes@36900
  2301
#4478 := (iff #3598 #4477)
boehmes@36900
  2302
#4475 := (iff #3597 #4474)
boehmes@36900
  2303
#4472 := (iff #3587 #4471)
boehmes@36900
  2304
#4469 := (iff #3582 #4468)
boehmes@36900
  2305
#4466 := (iff #3581 #4465)
boehmes@36900
  2306
#4463 := (iff #3580 #4462)
boehmes@36900
  2307
#4460 := (iff #3572 #4459)
boehmes@36900
  2308
#4457 := (iff #3567 #4456)
boehmes@36900
  2309
#4454 := (iff #3566 #4453)
boehmes@36900
  2310
#4451 := (iff #3565 #4450)
boehmes@36900
  2311
#4448 := (iff #3559 #4447)
boehmes@36900
  2312
#4445 := (iff #3554 #4444)
boehmes@36900
  2313
#4442 := (iff #3553 #4441)
boehmes@36900
  2314
#4439 := (iff #3552 #4438)
boehmes@36900
  2315
#4436 := (iff #3546 #4435)
boehmes@36900
  2316
#4433 := (iff #3541 #4432)
boehmes@36900
  2317
#4430 := (iff #3540 #4429)
boehmes@36900
  2318
#4427 := (iff #3539 #4426)
boehmes@36900
  2319
#4424 := (iff #3533 #4423)
boehmes@36900
  2320
#4421 := (iff #3528 #4420)
boehmes@36900
  2321
#4418 := (iff #3527 #4417)
boehmes@36900
  2322
#4415 := (iff #3526 #4414)
boehmes@36900
  2323
#4412 := (iff #3520 #4411)
boehmes@36900
  2324
#4409 := (iff #3515 #4408)
boehmes@36900
  2325
#4406 := (iff #3514 #4405)
boehmes@36900
  2326
#4403 := (iff #3513 #4402)
boehmes@36900
  2327
#4400 := (iff #3506 #4399)
boehmes@36900
  2328
#4397 := (iff #3501 #4396)
boehmes@36900
  2329
#4394 := (iff #3500 #4393)
boehmes@36900
  2330
#4391 := (iff #3499 #4390)
boehmes@36900
  2331
#4388 := (iff #3492 #4385)
boehmes@36900
  2332
#4386 := (iff #3481 #3481)
boehmes@36900
  2333
#4387 := [refl]: #4386
boehmes@36900
  2334
#4389 := [quant-intro #4387]: #4388
boehmes@36900
  2335
#4392 := [monotonicity #4389]: #4391
boehmes@36900
  2336
#4382 := (iff #3498 #4381)
boehmes@36900
  2337
#4379 := (iff #3477 #4376)
boehmes@36900
  2338
#4377 := (iff #3472 #3472)
boehmes@36900
  2339
#4378 := [refl]: #4377
boehmes@36900
  2340
#4380 := [quant-intro #4378]: #4379
boehmes@36900
  2341
#4383 := [monotonicity #4380]: #4382
boehmes@36900
  2342
#4395 := [monotonicity #4383 #4392]: #4394
boehmes@36900
  2343
#4398 := [monotonicity #4395]: #4397
boehmes@36900
  2344
#4401 := [monotonicity #4398]: #4400
boehmes@36900
  2345
#4404 := [monotonicity #4401]: #4403
boehmes@36900
  2346
#4374 := (iff #3512 #4373)
boehmes@36900
  2347
#4371 := (iff #3432 #4368)
boehmes@36900
  2348
#4369 := (iff #3427 #3427)
boehmes@36900
  2349
#4370 := [refl]: #4369
boehmes@36900
  2350
#4372 := [quant-intro #4370]: #4371
boehmes@36900
  2351
#4375 := [monotonicity #4372]: #4374
boehmes@36900
  2352
#4407 := [monotonicity #4375 #4404]: #4406
boehmes@36900
  2353
#4410 := [monotonicity #4407]: #4409
boehmes@36900
  2354
#4413 := [monotonicity #4410]: #4412
boehmes@36900
  2355
#4416 := [monotonicity #4413]: #4415
boehmes@36900
  2356
#4365 := (iff #1405 #4364)
boehmes@36900
  2357
#4362 := (iff #1402 #4359)
boehmes@36900
  2358
#4360 := (iff #1399 #1399)
boehmes@36900
  2359
#4361 := [refl]: #4360
boehmes@36900
  2360
#4363 := [quant-intro #4361]: #4362
boehmes@36900
  2361
#4366 := [monotonicity #4363]: #4365
boehmes@36900
  2362
#4419 := [monotonicity #4366 #4416]: #4418
boehmes@36900
  2363
#4422 := [monotonicity #4419]: #4421
boehmes@36900
  2364
#4425 := [monotonicity #4422]: #4424
boehmes@36900
  2365
#4428 := [monotonicity #4425]: #4427
boehmes@36900
  2366
#4431 := [monotonicity #4428]: #4430
boehmes@36900
  2367
#4434 := [monotonicity #4431]: #4433
boehmes@36900
  2368
#4437 := [monotonicity #4434]: #4436
boehmes@36900
  2369
#4440 := [monotonicity #4437]: #4439
boehmes@36900
  2370
#4357 := (iff #859 #4356)
boehmes@36900
  2371
#4354 := (iff #725 #4351)
boehmes@36900
  2372
#4352 := (iff #720 #720)
boehmes@36900
  2373
#4353 := [refl]: #4352
boehmes@36900
  2374
#4355 := [quant-intro #4353]: #4354
boehmes@36900
  2375
#4358 := [monotonicity #4355]: #4357
boehmes@36900
  2376
#4443 := [monotonicity #4358 #4440]: #4442
boehmes@36900
  2377
#4446 := [monotonicity #4443]: #4445
boehmes@36900
  2378
#4449 := [monotonicity #4446]: #4448
boehmes@36900
  2379
#4452 := [monotonicity #4449]: #4451
boehmes@36900
  2380
#4348 := (iff #1391 #4347)
boehmes@36900
  2381
#4345 := (iff #1388 #4342)
boehmes@36900
  2382
#4343 := (iff #1383 #1383)
boehmes@36900
  2383
#4344 := [refl]: #4343
boehmes@36900
  2384
#4346 := [quant-intro #4344]: #4345
boehmes@36900
  2385
#4349 := [monotonicity #4346]: #4348
boehmes@36900
  2386
#4455 := [monotonicity #4349 #4452]: #4454
boehmes@36900
  2387
#4458 := [monotonicity #4455]: #4457
boehmes@36900
  2388
#4461 := [monotonicity #4458]: #4460
boehmes@36900
  2389
#4464 := [monotonicity #4461]: #4463
boehmes@36900
  2390
#4340 := (iff #3579 #4339)
boehmes@36900
  2391
#4337 := (iff #3386 #4334)
boehmes@36900
  2392
#4335 := (iff #3381 #3381)
boehmes@36900
  2393
#4336 := [refl]: #4335
boehmes@36900
  2394
#4338 := [quant-intro #4336]: #4337
boehmes@36900
  2395
#4341 := [monotonicity #4338]: #4340
boehmes@36900
  2396
#4332 := (iff #3578 #4331)
boehmes@36900
  2397
#4329 := (iff #3368 #4326)
boehmes@36900
  2398
#4327 := (iff #3365 #3365)
boehmes@36900
  2399
#4328 := [refl]: #4327
boehmes@36900
  2400
#4330 := [quant-intro #4328]: #4329
boehmes@36900
  2401
#4333 := [monotonicity #4330]: #4332
boehmes@36900
  2402
#4322 := (iff #1556 #4321)
boehmes@36900
  2403
#4319 := (iff #1553 #4316)
boehmes@36900
  2404
#4317 := (iff #1548 #1548)
boehmes@36900
  2405
#4318 := [refl]: #4317
boehmes@36900
  2406
#4320 := [quant-intro #4318]: #4319
boehmes@36900
  2407
#4323 := [monotonicity #4320]: #4322
boehmes@36900
  2408
#4467 := [monotonicity #4323 #4333 #4341 #4464]: #4466
boehmes@36900
  2409
#4470 := [monotonicity #4467]: #4469
boehmes@36900
  2410
#4314 := (iff #3356 #4313)
boehmes@36900
  2411
#4311 := (iff #3355 #4310)
boehmes@36900
  2412
#4308 := (iff #3354 #4307)
boehmes@36900
  2413
#4305 := (iff #3347 #4304)
boehmes@36900
  2414
#4302 := (iff #3342 #4301)
boehmes@36900
  2415
#4299 := (iff #3341 #4298)
boehmes@36900
  2416
#4296 := (iff #3340 #4295)
boehmes@36900
  2417
#4293 := (iff #3333 #4292)
boehmes@36900
  2418
#4290 := (iff #3306 #4289)
boehmes@36900
  2419
#4287 := (iff #3305 #4286)
boehmes@36900
  2420
#4284 := (iff #3304 #4283)
boehmes@36900
  2421
#4281 := (iff #3298 #4278)
boehmes@36900
  2422
#4279 := (iff #3293 #3293)
boehmes@36900
  2423
#4280 := [refl]: #4279
boehmes@36900
  2424
#4282 := [quant-intro #4280]: #4281
boehmes@34994
  2425
#4285 := [monotonicity #4282]: #4284
boehmes@34994
  2426
#4288 := [monotonicity #4285]: #4287
boehmes@34994
  2427
#4291 := [monotonicity #4288]: #4290
boehmes@36900
  2428
#4294 := [monotonicity #4291]: #4293
boehmes@34994
  2429
#4297 := [monotonicity #4294]: #4296
boehmes@36900
  2430
#4276 := (iff #3339 #4275)
boehmes@36900
  2431
#4273 := (iff #3276 #4270)
boehmes@36900
  2432
#4271 := (iff #3271 #3271)
boehmes@36900
  2433
#4272 := [refl]: #4271
boehmes@36900
  2434
#4274 := [quant-intro #4272]: #4273
boehmes@36900
  2435
#4277 := [monotonicity #4274]: #4276
boehmes@36900
  2436
#4300 := [monotonicity #4277 #4297]: #4299
boehmes@34994
  2437
#4303 := [monotonicity #4300]: #4302
boehmes@36900
  2438
#4268 := (iff #3247 #4267)
boehmes@36900
  2439
#4265 := (iff #3246 #4264)
boehmes@36900
  2440
#4262 := (iff #3245 #4261)
boehmes@36900
  2441
#4259 := (iff #3239 #4256)
boehmes@36900
  2442
#4257 := (iff #3228 #3228)
boehmes@36900
  2443
#4258 := [refl]: #4257
boehmes@36900
  2444
#4260 := [quant-intro #4258]: #4259
boehmes@36900
  2445
#4263 := [monotonicity #4260]: #4262
boehmes@36900
  2446
#4266 := [monotonicity #4263]: #4265
boehmes@36900
  2447
#4269 := [monotonicity #4266]: #4268
boehmes@36900
  2448
#4306 := [monotonicity #4269 #4303]: #4305
boehmes@36900
  2449
#4309 := [monotonicity #4306]: #4308
boehmes@36900
  2450
#4252 := (iff #3353 #4251)
boehmes@36900
  2451
#4249 := (iff #3224 #4246)
boehmes@36900
  2452
#4247 := (iff #3213 #3213)
boehmes@34994
  2453
#4248 := [refl]: #4247
boehmes@34994
  2454
#4250 := [quant-intro #4248]: #4249
boehmes@34994
  2455
#4253 := [monotonicity #4250]: #4252
boehmes@36900
  2456
#4312 := [monotonicity #4253 #4309]: #4311
boehmes@34994
  2457
#4315 := [monotonicity #4312]: #4314
boehmes@36900
  2458
#4473 := [monotonicity #4315 #4470]: #4472
boehmes@36900
  2459
#4476 := [monotonicity #4473]: #4475
boehmes@36900
  2460
#4243 := (iff #3596 #4242)
boehmes@36900
  2461
#4240 := (iff #3210 #4237)
boehmes@36900
  2462
#4238 := (iff #3205 #3205)
boehmes@36900
  2463
#4239 := [refl]: #4238
boehmes@36900
  2464
#4241 := [quant-intro #4239]: #4240
boehmes@36900
  2465
#4244 := [monotonicity #4241]: #4243
boehmes@36900
  2466
#4235 := (iff #3595 #4234)
boehmes@36900
  2467
#4232 := (iff #3182 #4229)
boehmes@36900
  2468
#4230 := (iff #3177 #3177)
boehmes@34994
  2469
#4231 := [refl]: #4230
boehmes@34994
  2470
#4233 := [quant-intro #4231]: #4232
boehmes@34994
  2471
#4236 := [monotonicity #4233]: #4235
boehmes@36900
  2472
#4227 := (iff #3594 #4226)
boehmes@36900
  2473
#4224 := (iff #3154 #4221)
boehmes@36900
  2474
#4222 := (iff #3149 #3149)
boehmes@34994
  2475
#4223 := [refl]: #4222
boehmes@34994
  2476
#4225 := [quant-intro #4223]: #4224
boehmes@34994
  2477
#4228 := [monotonicity #4225]: #4227
boehmes@36900
  2478
#4218 := (iff #3593 #4217)
boehmes@36900
  2479
#4215 := (iff #3131 #4212)
boehmes@36900
  2480
#4213 := (iff #3126 #3126)
boehmes@36900
  2481
#4214 := [refl]: #4213
boehmes@36900
  2482
#4216 := [quant-intro #4214]: #4215
boehmes@36900
  2483
#4219 := [monotonicity #4216]: #4218
boehmes@36900
  2484
#4210 := (iff #1648 #4209)
boehmes@36900
  2485
#4207 := (iff #1645 #4204)
boehmes@36900
  2486
#4205 := (iff #1642 #1642)
boehmes@36900
  2487
#4206 := [refl]: #4205
boehmes@36900
  2488
#4208 := [quant-intro #4206]: #4207
boehmes@36900
  2489
#4211 := [monotonicity #4208]: #4210
boehmes@36900
  2490
#4479 := [monotonicity #4211 #4219 #4228 #4236 #4244 #4476]: #4478
boehmes@36900
  2491
#4482 := [monotonicity #4479]: #4481
boehmes@36900
  2492
#4201 := (iff #3107 #4200)
boehmes@36900
  2493
#4198 := (iff #3106 #4197)
boehmes@36900
  2494
#4195 := (iff #3105 #4194)
boehmes@36900
  2495
#4192 := (iff #3099 #4189)
boehmes@36900
  2496
#4190 := (iff #3088 #3088)
boehmes@36900
  2497
#4191 := [refl]: #4190
boehmes@36900
  2498
#4193 := [quant-intro #4191]: #4192
boehmes@34994
  2499
#4196 := [monotonicity #4193]: #4195
boehmes@36900
  2500
#4199 := [monotonicity #4196]: #4198
boehmes@34994
  2501
#4202 := [monotonicity #4199]: #4201
boehmes@36900
  2502
#4485 := [monotonicity #4202 #4482]: #4484
boehmes@36900
  2503
#4488 := [monotonicity #4485]: #4487
boehmes@36900
  2504
#4186 := (iff #3610 #4185)
boehmes@36900
  2505
#4183 := (iff #3084 #4180)
boehmes@36900
  2506
#4181 := (iff #3079 #3079)
boehmes@36900
  2507
#4182 := [refl]: #4181
boehmes@36900
  2508
#4184 := [quant-intro #4182]: #4183
boehmes@36900
  2509
#4187 := [monotonicity #4184]: #4186
boehmes@36900
  2510
#4491 := [monotonicity #4187 #4488]: #4490
boehmes@36900
  2511
#4494 := [monotonicity #4491]: #4493
boehmes@36900
  2512
#4497 := [monotonicity #4494]: #4496
boehmes@36900
  2513
#4500 := [monotonicity #4497]: #4499
boehmes@36900
  2514
#4177 := (iff #3624 #4176)
boehmes@36900
  2515
#4174 := (iff #3039 #4171)
boehmes@36900
  2516
#4172 := (iff #3034 #3034)
boehmes@36900
  2517
#4173 := [refl]: #4172
boehmes@36900
  2518
#4175 := [quant-intro #4173]: #4174
boehmes@36900
  2519
#4178 := [monotonicity #4175]: #4177
boehmes@36900
  2520
#4503 := [monotonicity #4178 #4500]: #4502
boehmes@36900
  2521
#4506 := [monotonicity #4503]: #4505
boehmes@36900
  2522
#4509 := [monotonicity #4506]: #4508
boehmes@36900
  2523
#4512 := [monotonicity #4509]: #4511
boehmes@36900
  2524
#4168 := (iff #1111 #4167)
boehmes@36900
  2525
#4165 := (iff #1108 #4162)
boehmes@36900
  2526
#4163 := (iff #1107 #1107)
boehmes@36900
  2527
#4164 := [refl]: #4163
boehmes@36900
  2528
#4166 := [quant-intro #4164]: #4165
boehmes@36900
  2529
#4169 := [monotonicity #4166]: #4168
boehmes@36900
  2530
#4515 := [monotonicity #4169 #4512]: #4514
boehmes@36900
  2531
#4518 := [monotonicity #4515]: #4517
boehmes@36900
  2532
#4521 := [monotonicity #4518]: #4520
boehmes@36900
  2533
#4524 := [monotonicity #4521]: #4523
boehmes@36900
  2534
#4527 := [monotonicity #4524]: #4526
boehmes@36900
  2535
#4530 := [monotonicity #4527]: #4529
boehmes@36900
  2536
#4533 := [monotonicity #4530]: #4532
boehmes@36900
  2537
#2304 := (not #2303)
boehmes@36900
  2538
#2906 := (and #713 #2304 #2903)
boehmes@36900
  2539
#2909 := (not #2906)
boehmes@36900
  2540
#2912 := (forall (vars (?v1 S2)) #2909)
boehmes@36900
  2541
#2878 := (not #2875)
boehmes@36900
  2542
#2309 := (not #2308)
boehmes@36900
  2543
#2921 := (and #1445 #2309 #2878 #2912)
boehmes@36900
  2544
#2277 := (not #2276)
boehmes@36900
  2545
#2848 := (and #2277 #2279)
boehmes@36900
  2546
#2851 := (not #2848)
boehmes@36900
  2547
#2869 := (or #2851 #2864)
boehmes@36900
  2548
#2872 := (not #2869)
boehmes@36900
  2549
#2926 := (or #2872 #2921)
boehmes@36900
  2550
#2929 := (and #1421 #2926)
boehmes@36900
  2551
#2248 := (not #2247)
boehmes@36900
  2552
#2823 := (and #2245 #2248)
boehmes@36900
  2553
#2826 := (not #2823)
boehmes@36900
  2554
#2842 := (or #2826 #2837)
boehmes@36900
  2555
#2845 := (not #2842)
boehmes@36900
  2556
#2932 := (or #2845 #2929)
boehmes@36900
  2557
#2935 := (and #1402 #2932)
boehmes@36900
  2558
#2938 := (or #2225 #2935)
boehmes@36900
  2559
#2941 := (and #170 #2938)
boehmes@36900
  2560
#2944 := (or #1396 #2941)
boehmes@36900
  2561
#2947 := (and #725 #2944)
boehmes@36900
  2562
#2950 := (or #2818 #2947)
boehmes@36900
  2563
#2953 := (and #1388 #2950)
boehmes@36900
  2564
#2956 := (or #2804 #2953)
boehmes@36900
  2565
#2163 := (not #2162)
boehmes@34994
  2566
#2160 := (not #2159)
boehmes@36900
  2567
#2962 := (and #148 #671 #1377 #1535 #1553 #1561 #2160 #2163 #2956)
boehmes@36900
  2568
#2105 := (not #2104)
boehmes@36900
  2569
#2101 := (not #2100)
boehmes@36900
  2570
#2741 := (and #2101 #2105)
boehmes@36900
  2571
#2744 := (not #2741)
boehmes@36900
  2572
#2761 := (or #2744 #2756)
boehmes@36900
  2573
#2764 := (not #2761)
boehmes@36900
  2574
#2114 := (not #125)
boehmes@36900
  2575
#2124 := (and #2114 #1297)
boehmes@36900
  2576
#2770 := (or #2124 #2764)
boehmes@36900
  2577
#2714 := (not #2709)
boehmes@36900
  2578
#2732 := (and #2714 #2727)
boehmes@36900
  2579
#2735 := (or #1257 #2732)
boehmes@36900
  2580
#2738 := (forall (vars (?v0 S2)) #2735)
boehmes@36900
  2581
#2775 := (and #2738 #2770)
boehmes@36900
  2582
#2034 := (not #2033)
boehmes@36900
  2583
#2684 := (and #2034 #2681)
boehmes@36900
  2584
#2687 := (not #2684)
boehmes@36900
  2585
#2690 := (forall (vars (?v1 S2)) #2687)
boehmes@36900
  2586
#2656 := (not #2653)
boehmes@36900
  2587
#2039 := (not #2038)
boehmes@36900
  2588
#2696 := (and #2039 #2656 #2690)
boehmes@36900
  2589
#2778 := (or #2696 #2775)
boehmes@36900
  2590
#2140 := (not #1325)
boehmes@36900
  2591
#2143 := (forall (vars (?v0 S2)) #2140)
boehmes@36900
  2592
#2784 := (and #103 #108 #535 #538 #2143 #2778)
boehmes@36900
  2593
#2967 := (or #2784 #2962)
boehmes@36900
  2594
#2633 := (not #2628)
boehmes@36900
  2595
#2636 := (and #1998 #2616 #2633)
boehmes@36900
  2596
#2639 := (or #1212 #2636)
boehmes@36900
  2597
#2642 := (forall (vars (?v0 S2)) #2639)
boehmes@36900
  2598
#2578 := (not #2573)
boehmes@36900
  2599
#2596 := (and #1971 #2578 #2591)
boehmes@36900
  2600
#2599 := (or #1174 #2596)
boehmes@36900
  2601
#2602 := (forall (vars (?v0 S2)) #2599)
boehmes@36900
  2602
#2973 := (and #67 #1620 #1636 #1645 #2602 #2642 #2967)
boehmes@36900
  2603
#1926 := (not #1925)
boehmes@36900
  2604
#2546 := (and #368 #1926 #2543)
boehmes@36900
  2605
#2549 := (not #2546)
boehmes@36900
  2606
#2552 := (forall (vars (?v1 S2)) #2549)
boehmes@36900
  2607
#2518 := (not #2515)
boehmes@36900
  2608
#1931 := (not #1930)
boehmes@36900
  2609
#2558 := (and #1931 #2518 #2552)
boehmes@36900
  2610
#2978 := (or #2558 #2973)
boehmes@36900
  2611
#2981 := (and #1159 #2978)
boehmes@36900
  2612
#1892 := (not #1891)
boehmes@36900
  2613
#2503 := (and #1892 #1894)
boehmes@36900
  2614
#2506 := (not #2503)
boehmes@36900
  2615
#2509 := (or #2500 #2506)
boehmes@36900
  2616
#2512 := (not #2509)
boehmes@36900
  2617
#2984 := (or #2512 #2981)
boehmes@36900
  2618
#2987 := (and #1128 #2984)
boehmes@36900
  2619
#1869 := (not #1868)
boehmes@36900
  2620
#2471 := (and #1866 #1869)
boehmes@36900
  2621
#2474 := (not #2471)
boehmes@36900
  2622
#2490 := (or #2474 #2485)
boehmes@36900
  2623
#2493 := (not #2490)
boehmes@36900
  2624
#2990 := (or #2493 #2987)
boehmes@36900
  2625
#2993 := (and #1108 #2990)
boehmes@36900
  2626
#2996 := (or #1846 #2993)
boehmes@36900
  2627
#2999 := (and #38 #2996)
boehmes@36900
  2628
#3002 := (or #1102 #2999)
boehmes@36900
  2629
#3659 := (iff #3002 #3658)
boehmes@36900
  2630
#3656 := (iff #2999 #3653)
boehmes@36900
  2631
#3648 := (and #38 #3645)
boehmes@36900
  2632
#3654 := (iff #3648 #3653)
boehmes@36900
  2633
#3655 := [rewrite]: #3654
boehmes@36900
  2634
#3649 := (iff #2999 #3648)
boehmes@36900
  2635
#3646 := (iff #2996 #3645)
boehmes@36900
  2636
#3643 := (iff #2993 #3640)
boehmes@36900
  2637
#3635 := (and #1108 #3632)