src/HOL/SMT_Examples/SMT_Examples.certs
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45393 13ab80eafd71
child 46084 dd7fb9e651ad
permissions -rw-r--r--
Quotient_Info stores only relation maps
boehmes@41132
     1
8c0dd63633148cae631c41716f59fedf31aaf85f 8 0
boehmes@41132
     2
#2 := false
boehmes@41132
     3
#1 := true
boehmes@41132
     4
#8 := (not true)
boehmes@41132
     5
#29 := (iff #8 false)
boehmes@41132
     6
#30 := [rewrite]: #29
boehmes@41132
     7
#28 := [asserted]: #8
boehmes@41132
     8
[mp #28 #30]: false
boehmes@41132
     9
unsat
boehmes@41132
    10
4e759d02d4de42cc8b917c1ee399e500780bf8d9 33 0
boehmes@36900
    11
#2 := false
boehmes@36900
    12
decl f1 :: S1
boehmes@36900
    13
#4 := f1
boehmes@36900
    14
decl f3 :: S1
boehmes@36900
    15
#8 := f3
boehmes@36900
    16
#9 := (= f3 f1)
boehmes@36900
    17
#10 := (not #9)
boehmes@36900
    18
#11 := (or #9 #10)
boehmes@36900
    19
#12 := (not #11)
boehmes@41132
    20
#51 := (iff #12 false)
boehmes@36900
    21
#1 := true
boehmes@41132
    22
#46 := (not true)
boehmes@41132
    23
#49 := (iff #46 false)
boehmes@41132
    24
#50 := [rewrite]: #49
boehmes@41132
    25
#47 := (iff #12 #46)
boehmes@41132
    26
#44 := (iff #11 true)
boehmes@41132
    27
#33 := (= f1 f3)
boehmes@41132
    28
#36 := (not #33)
boehmes@41132
    29
#39 := (or #33 #36)
boehmes@41132
    30
#42 := (iff #39 true)
boehmes@41132
    31
#43 := [rewrite]: #42
boehmes@41132
    32
#40 := (iff #11 #39)
boehmes@41132
    33
#37 := (iff #10 #36)
boehmes@41132
    34
#34 := (iff #9 #33)
boehmes@41132
    35
#35 := [rewrite]: #34
boehmes@41132
    36
#38 := [monotonicity #35]: #37
boehmes@41132
    37
#41 := [monotonicity #35 #38]: #40
boehmes@41132
    38
#45 := [trans #41 #43]: #44
boehmes@41132
    39
#48 := [monotonicity #45]: #47
boehmes@41132
    40
#52 := [trans #48 #50]: #51
boehmes@41132
    41
#32 := [asserted]: #12
boehmes@41132
    42
[mp #32 #52]: false
boehmes@41132
    43
unsat
boehmes@41132
    44
964f9fc947278fe63d579d7e942d63db70d69508 37 0
boehmes@36900
    45
#2 := false
boehmes@36900
    46
decl f1 :: S1
boehmes@36900
    47
#4 := f1
boehmes@36900
    48
decl f3 :: S1
boehmes@36900
    49
#8 := f3
boehmes@36900
    50
#9 := (= f3 f1)
boehmes@36900
    51
#1 := true
boehmes@36900
    52
#10 := (and #9 true)
boehmes@36900
    53
#11 := (iff #10 #9)
boehmes@36900
    54
#12 := (not #11)
boehmes@41132
    55
#55 := (iff #12 false)
boehmes@41132
    56
#50 := (not true)
boehmes@41132
    57
#53 := (iff #50 false)
boehmes@41132
    58
#54 := [rewrite]: #53
boehmes@41132
    59
#51 := (iff #12 #50)
boehmes@41132
    60
#48 := (iff #11 true)
boehmes@41132
    61
#33 := (= f1 f3)
boehmes@41132
    62
#43 := (iff #33 #33)
boehmes@41132
    63
#46 := (iff #43 true)
boehmes@41132
    64
#47 := [rewrite]: #46
boehmes@41132
    65
#44 := (iff #11 #43)
boehmes@41132
    66
#34 := (iff #9 #33)
boehmes@41132
    67
#35 := [rewrite]: #34
boehmes@41132
    68
#41 := (iff #10 #33)
boehmes@41132
    69
#36 := (and #33 true)
boehmes@41132
    70
#39 := (iff #36 #33)
boehmes@41132
    71
#40 := [rewrite]: #39
boehmes@41132
    72
#37 := (iff #10 #36)
boehmes@41132
    73
#38 := [monotonicity #35]: #37
boehmes@41132
    74
#42 := [trans #38 #40]: #41
boehmes@41132
    75
#45 := [monotonicity #42 #35]: #44
boehmes@41132
    76
#49 := [trans #45 #47]: #48
boehmes@41132
    77
#52 := [monotonicity #49]: #51
boehmes@41132
    78
#56 := [trans #52 #54]: #55
boehmes@41132
    79
#32 := [asserted]: #12
boehmes@41132
    80
[mp #32 #56]: false
boehmes@41132
    81
unsat
boehmes@41132
    82
6f5c195ed8186ea009f805e2f8ea8ad3b1ee6432 66 0
boehmes@36900
    83
#2 := false
boehmes@36900
    84
decl f4 :: S1
boehmes@36900
    85
#10 := f4
boehmes@36900
    86
decl f1 :: S1
boehmes@36900
    87
#4 := f1
boehmes@41132
    88
#40 := (= f1 f4)
boehmes@36900
    89
decl f3 :: S1
boehmes@36900
    90
#8 := f3
boehmes@41132
    91
#37 := (= f1 f3)
boehmes@41132
    92
#43 := (or #37 #40)
boehmes@41132
    93
#87 := (iff #43 false)
boehmes@41132
    94
#82 := (or false false)
boehmes@41132
    95
#85 := (iff #82 false)
boehmes@41132
    96
#86 := [rewrite]: #85
boehmes@41132
    97
#83 := (iff #43 #82)
boehmes@41132
    98
#78 := (iff #40 false)
boehmes@41132
    99
#69 := (not #40)
boehmes@41132
   100
#46 := (not #37)
boehmes@41132
   101
#52 := (and #46 #43)
boehmes@41132
   102
#60 := (not #52)
boehmes@41132
   103
#61 := (or #40 #60)
boehmes@41132
   104
#66 := (not #61)
boehmes@36900
   105
#11 := (= f4 f1)
boehmes@36900
   106
#9 := (= f3 f1)
boehmes@36900
   107
#13 := (not #9)
boehmes@36900
   108
#12 := (or #9 #11)
boehmes@36900
   109
#14 := (and #12 #13)
boehmes@36900
   110
#15 := (implies #14 #11)
boehmes@36900
   111
#16 := (not #15)
boehmes@41132
   112
#67 := (iff #16 #66)
boehmes@41132
   113
#64 := (iff #15 #61)
boehmes@41132
   114
#57 := (implies #52 #40)
boehmes@41132
   115
#62 := (iff #57 #61)
boehmes@41132
   116
#63 := [rewrite]: #62
boehmes@41132
   117
#58 := (iff #15 #57)
boehmes@41132
   118
#41 := (iff #11 #40)
boehmes@41132
   119
#42 := [rewrite]: #41
boehmes@41132
   120
#55 := (iff #14 #52)
boehmes@41132
   121
#49 := (and #43 #46)
boehmes@41132
   122
#53 := (iff #49 #52)
boehmes@41132
   123
#54 := [rewrite]: #53
boehmes@41132
   124
#50 := (iff #14 #49)
boehmes@41132
   125
#47 := (iff #13 #46)
boehmes@41132
   126
#38 := (iff #9 #37)
boehmes@36900
   127
#39 := [rewrite]: #38
boehmes@41132
   128
#48 := [monotonicity #39]: #47
boehmes@41132
   129
#44 := (iff #12 #43)
boehmes@41132
   130
#45 := [monotonicity #39 #42]: #44
boehmes@41132
   131
#51 := [monotonicity #45 #48]: #50
boehmes@41132
   132
#56 := [trans #51 #54]: #55
boehmes@41132
   133
#59 := [monotonicity #56 #42]: #58
boehmes@41132
   134
#65 := [trans #59 #63]: #64
boehmes@41132
   135
#68 := [monotonicity #65]: #67
boehmes@41132
   136
#36 := [asserted]: #16
boehmes@41132
   137
#71 := [mp #36 #68]: #66
boehmes@41132
   138
#70 := [not-or-elim #71]: #69
boehmes@41132
   139
#79 := [iff-false #70]: #78
boehmes@41132
   140
#80 := (iff #37 false)
boehmes@41132
   141
#72 := [not-or-elim #71]: #52
boehmes@41132
   142
#73 := [and-elim #72]: #46
boehmes@41132
   143
#81 := [iff-false #73]: #80
boehmes@41132
   144
#84 := [monotonicity #81 #79]: #83
boehmes@41132
   145
#88 := [trans #84 #86]: #87
boehmes@41132
   146
#74 := [and-elim #72]: #43
boehmes@41132
   147
[mp #74 #88]: false
boehmes@41132
   148
unsat
boehmes@41282
   149
bc6de36d6c86b416e91711bb23067cc8250ac153 59 0
boehmes@41282
   150
#2 := false
boehmes@41282
   151
decl f1 :: S1
boehmes@41282
   152
#4 := f1
boehmes@41282
   153
decl f6 :: S1
boehmes@41282
   154
#15 := f6
boehmes@41282
   155
#16 := (= f6 f1)
boehmes@41282
   156
decl f5 :: S1
boehmes@41282
   157
#13 := f5
boehmes@41282
   158
#14 := (= f5 f1)
boehmes@41282
   159
#17 := (and #14 #16)
boehmes@41282
   160
decl f4 :: S1
boehmes@41282
   161
#10 := f4
boehmes@41282
   162
#11 := (= f4 f1)
boehmes@41282
   163
decl f3 :: S1
boehmes@41282
   164
#8 := f3
boehmes@41282
   165
#9 := (= f3 f1)
boehmes@41282
   166
#12 := (and #9 #11)
boehmes@41282
   167
#18 := (or #12 #17)
boehmes@41282
   168
#19 := (implies #18 #18)
boehmes@41282
   169
#20 := (not #19)
boehmes@41282
   170
#74 := (iff #20 false)
boehmes@41282
   171
#1 := true
boehmes@41282
   172
#69 := (not true)
boehmes@41282
   173
#72 := (iff #69 false)
boehmes@41282
   174
#73 := [rewrite]: #72
boehmes@41282
   175
#70 := (iff #20 #69)
boehmes@41282
   176
#67 := (iff #19 true)
boehmes@41282
   177
#53 := (= f1 f6)
boehmes@41282
   178
#50 := (= f1 f5)
boehmes@41282
   179
#56 := (and #50 #53)
boehmes@41282
   180
#44 := (= f1 f4)
boehmes@41282
   181
#41 := (= f1 f3)
boehmes@41282
   182
#47 := (and #41 #44)
boehmes@41282
   183
#59 := (or #47 #56)
boehmes@41282
   184
#62 := (implies #59 #59)
boehmes@41282
   185
#65 := (iff #62 true)
boehmes@41282
   186
#66 := [rewrite]: #65
boehmes@41282
   187
#63 := (iff #19 #62)
boehmes@41282
   188
#60 := (iff #18 #59)
boehmes@41282
   189
#57 := (iff #17 #56)
boehmes@41282
   190
#54 := (iff #16 #53)
boehmes@41282
   191
#55 := [rewrite]: #54
boehmes@41282
   192
#51 := (iff #14 #50)
boehmes@41282
   193
#52 := [rewrite]: #51
boehmes@41282
   194
#58 := [monotonicity #52 #55]: #57
boehmes@41282
   195
#48 := (iff #12 #47)
boehmes@41282
   196
#45 := (iff #11 #44)
boehmes@41282
   197
#46 := [rewrite]: #45
boehmes@41282
   198
#42 := (iff #9 #41)
boehmes@41282
   199
#43 := [rewrite]: #42
boehmes@41282
   200
#49 := [monotonicity #43 #46]: #48
boehmes@41282
   201
#61 := [monotonicity #49 #58]: #60
boehmes@41282
   202
#64 := [monotonicity #61 #61]: #63
boehmes@41282
   203
#68 := [trans #64 #66]: #67
boehmes@41282
   204
#71 := [monotonicity #68]: #70
boehmes@41282
   205
#75 := [trans #71 #73]: #74
boehmes@41282
   206
#40 := [asserted]: #20
boehmes@41282
   207
[mp #40 #75]: false
boehmes@41132
   208
unsat
boehmes@41132
   209
e334e079d0f61721e404e4ca140ce40c317189ba 94 0
boehmes@36900
   210
#2 := false
boehmes@36900
   211
decl f1 :: S1
boehmes@36900
   212
#4 := f1
boehmes@36900
   213
decl f3 :: S1
boehmes@36900
   214
#8 := f3
boehmes@36900
   215
#9 := (= f3 f1)
boehmes@36900
   216
decl f5 :: S1
boehmes@36900
   217
#13 := f5
boehmes@36900
   218
#14 := (= f5 f1)
boehmes@36900
   219
#17 := (and #9 #14)
boehmes@36900
   220
decl f4 :: S1
boehmes@36900
   221
#10 := f4
boehmes@36900
   222
#11 := (= f4 f1)
boehmes@36900
   223
#16 := (and #14 #11)
boehmes@36900
   224
#18 := (or #16 #17)
boehmes@36900
   225
#19 := (implies #9 #18)
boehmes@36900
   226
#20 := (or #19 #9)
boehmes@36900
   227
#12 := (and #9 #11)
boehmes@36900
   228
#15 := (or #12 #14)
boehmes@36900
   229
#21 := (implies #15 #20)
boehmes@36900
   230
#22 := (not #21)
boehmes@41132
   231
#110 := (iff #22 false)
boehmes@41132
   232
#52 := (= f1 f5)
boehmes@41132
   233
#43 := (= f1 f3)
boehmes@41132
   234
#66 := (and #43 #52)
boehmes@41132
   235
#46 := (= f1 f4)
boehmes@41132
   236
#61 := (and #46 #52)
boehmes@41132
   237
#69 := (or #61 #66)
boehmes@41132
   238
#75 := (not #43)
boehmes@41132
   239
#76 := (or #75 #69)
boehmes@41132
   240
#84 := (or #43 #76)
boehmes@41132
   241
#49 := (and #43 #46)
boehmes@41132
   242
#55 := (or #49 #52)
boehmes@41132
   243
#92 := (not #55)
boehmes@41132
   244
#93 := (or #92 #84)
boehmes@41132
   245
#98 := (not #93)
boehmes@41132
   246
#108 := (iff #98 false)
boehmes@36900
   247
#1 := true
boehmes@41132
   248
#103 := (not true)
boehmes@41132
   249
#106 := (iff #103 false)
boehmes@41132
   250
#107 := [rewrite]: #106
boehmes@41132
   251
#104 := (iff #98 #103)
boehmes@41132
   252
#101 := (iff #93 true)
boehmes@41132
   253
#102 := [rewrite]: #101
boehmes@41132
   254
#105 := [monotonicity #102]: #104
boehmes@41132
   255
#109 := [trans #105 #107]: #108
boehmes@41132
   256
#99 := (iff #22 #98)
boehmes@41132
   257
#96 := (iff #21 #93)
boehmes@41132
   258
#89 := (implies #55 #84)
boehmes@41132
   259
#94 := (iff #89 #93)
boehmes@41132
   260
#95 := [rewrite]: #94
boehmes@41132
   261
#90 := (iff #21 #89)
boehmes@41132
   262
#87 := (iff #20 #84)
boehmes@41132
   263
#81 := (or #76 #43)
boehmes@41132
   264
#85 := (iff #81 #84)
boehmes@41132
   265
#86 := [rewrite]: #85
boehmes@41132
   266
#82 := (iff #20 #81)
boehmes@41132
   267
#44 := (iff #9 #43)
boehmes@36900
   268
#45 := [rewrite]: #44
boehmes@41132
   269
#79 := (iff #19 #76)
boehmes@41132
   270
#72 := (implies #43 #69)
boehmes@41132
   271
#77 := (iff #72 #76)
boehmes@41132
   272
#78 := [rewrite]: #77
boehmes@41132
   273
#73 := (iff #19 #72)
boehmes@41132
   274
#70 := (iff #18 #69)
boehmes@41132
   275
#67 := (iff #17 #66)
boehmes@41132
   276
#53 := (iff #14 #52)
boehmes@41132
   277
#54 := [rewrite]: #53
boehmes@41132
   278
#68 := [monotonicity #45 #54]: #67
boehmes@41132
   279
#64 := (iff #16 #61)
boehmes@41132
   280
#58 := (and #52 #46)
boehmes@41132
   281
#62 := (iff #58 #61)
boehmes@41132
   282
#63 := [rewrite]: #62
boehmes@41132
   283
#59 := (iff #16 #58)
boehmes@41132
   284
#47 := (iff #11 #46)
boehmes@41132
   285
#48 := [rewrite]: #47
boehmes@41132
   286
#60 := [monotonicity #54 #48]: #59
boehmes@41132
   287
#65 := [trans #60 #63]: #64
boehmes@41132
   288
#71 := [monotonicity #65 #68]: #70
boehmes@41132
   289
#74 := [monotonicity #45 #71]: #73
boehmes@41132
   290
#80 := [trans #74 #78]: #79
boehmes@41132
   291
#83 := [monotonicity #80 #45]: #82
boehmes@41132
   292
#88 := [trans #83 #86]: #87
boehmes@41132
   293
#56 := (iff #15 #55)
boehmes@41132
   294
#50 := (iff #12 #49)
boehmes@41132
   295
#51 := [monotonicity #45 #48]: #50
boehmes@41132
   296
#57 := [monotonicity #51 #54]: #56
boehmes@41132
   297
#91 := [monotonicity #57 #88]: #90
boehmes@41132
   298
#97 := [trans #91 #95]: #96
boehmes@41132
   299
#100 := [monotonicity #97]: #99
boehmes@41132
   300
#111 := [trans #100 #109]: #110
boehmes@41132
   301
#42 := [asserted]: #22
boehmes@41132
   302
[mp #42 #111]: false
boehmes@41132
   303
unsat
boehmes@41132
   304
778009f890fff5d244f6b4e04a54c69b4023bcd7 72 0
boehmes@36900
   305
#2 := false
boehmes@36900
   306
decl f1 :: S1
boehmes@36900
   307
#4 := f1
boehmes@36900
   308
decl f3 :: S1
boehmes@36900
   309
#8 := f3
boehmes@36900
   310
#9 := (= f3 f1)
boehmes@36900
   311
#10 := (iff #9 #9)
boehmes@36900
   312
#11 := (iff #10 #9)
boehmes@36900
   313
#12 := (iff #11 #9)
boehmes@36900
   314
#13 := (iff #12 #9)
boehmes@36900
   315
#14 := (iff #13 #9)
boehmes@36900
   316
#15 := (iff #14 #9)
boehmes@36900
   317
#16 := (iff #15 #9)
boehmes@36900
   318
#17 := (iff #16 #9)
boehmes@36900
   319
#18 := (iff #17 #9)
boehmes@36900
   320
#19 := (not #18)
boehmes@41132
   321
#90 := (iff #19 false)
boehmes@36900
   322
#1 := true
boehmes@41132
   323
#85 := (not true)
boehmes@41132
   324
#88 := (iff #85 false)
boehmes@41132
   325
#89 := [rewrite]: #88
boehmes@41132
   326
#86 := (iff #19 #85)
boehmes@41132
   327
#83 := (iff #18 true)
boehmes@41132
   328
#40 := (= f1 f3)
boehmes@41132
   329
#43 := (iff #40 #40)
boehmes@41132
   330
#46 := (iff #43 true)
boehmes@41132
   331
#47 := [rewrite]: #46
boehmes@41132
   332
#81 := (iff #18 #43)
boehmes@41132
   333
#41 := (iff #9 #40)
boehmes@41132
   334
#42 := [rewrite]: #41
boehmes@41132
   335
#79 := (iff #17 #40)
boehmes@41132
   336
#50 := (iff true #40)
boehmes@41132
   337
#53 := (iff #50 #40)
boehmes@41132
   338
#54 := [rewrite]: #53
boehmes@41132
   339
#77 := (iff #17 #50)
boehmes@41132
   340
#75 := (iff #16 true)
boehmes@41132
   341
#73 := (iff #16 #43)
boehmes@41132
   342
#71 := (iff #15 #40)
boehmes@41132
   343
#69 := (iff #15 #50)
boehmes@41132
   344
#67 := (iff #14 true)
boehmes@41132
   345
#65 := (iff #14 #43)
boehmes@41132
   346
#63 := (iff #13 #40)
boehmes@41132
   347
#61 := (iff #13 #50)
boehmes@41132
   348
#59 := (iff #12 true)
boehmes@41132
   349
#57 := (iff #12 #43)
boehmes@41132
   350
#55 := (iff #11 #40)
boehmes@41132
   351
#51 := (iff #11 #50)
boehmes@41132
   352
#48 := (iff #10 true)
boehmes@41132
   353
#44 := (iff #10 #43)
boehmes@41132
   354
#45 := [monotonicity #42 #42]: #44
boehmes@41132
   355
#49 := [trans #45 #47]: #48
boehmes@41132
   356
#52 := [monotonicity #49 #42]: #51
boehmes@41132
   357
#56 := [trans #52 #54]: #55
boehmes@41132
   358
#58 := [monotonicity #56 #42]: #57
boehmes@41132
   359
#60 := [trans #58 #47]: #59
boehmes@41132
   360
#62 := [monotonicity #60 #42]: #61
boehmes@41132
   361
#64 := [trans #62 #54]: #63
boehmes@41132
   362
#66 := [monotonicity #64 #42]: #65
boehmes@41132
   363
#68 := [trans #66 #47]: #67
boehmes@41132
   364
#70 := [monotonicity #68 #42]: #69
boehmes@41132
   365
#72 := [trans #70 #54]: #71
boehmes@41132
   366
#74 := [monotonicity #72 #42]: #73
boehmes@41132
   367
#76 := [trans #74 #47]: #75
boehmes@41132
   368
#78 := [monotonicity #76 #42]: #77
boehmes@41132
   369
#80 := [trans #78 #54]: #79
boehmes@41132
   370
#82 := [monotonicity #80 #42]: #81
boehmes@41132
   371
#84 := [trans #82 #47]: #83
boehmes@41132
   372
#87 := [monotonicity #84]: #86
boehmes@41132
   373
#91 := [trans #87 #89]: #90
boehmes@41132
   374
#39 := [asserted]: #19
boehmes@41132
   375
[mp #39 #91]: false
boehmes@41132
   376
unsat
boehmes@41132
   377
1d6ace6138adeb11b9c9952f896f225452c30f9e 234 0
boehmes@36900
   378
#2 := false
boehmes@36900
   379
decl f6 :: S1
boehmes@36900
   380
#14 := f6
boehmes@36900
   381
decl f1 :: S1
boehmes@36900
   382
#4 := f1
boehmes@41132
   383
#82 := (= f1 f6)
boehmes@36900
   384
decl f5 :: S1
boehmes@36900
   385
#12 := f5
boehmes@41132
   386
#79 := (= f1 f5)
boehmes@36900
   387
decl f4 :: S1
boehmes@36900
   388
#10 := f4
boehmes@41132
   389
#76 := (= f1 f4)
boehmes@36900
   390
decl f3 :: S1
boehmes@36900
   391
#8 := f3
boehmes@41132
   392
#73 := (= f1 f3)
boehmes@41132
   393
#94 := (or #73 #76 #79 #82)
boehmes@41132
   394
#301 := (iff #94 false)
boehmes@41132
   395
#296 := (or false false false false)
boehmes@41132
   396
#299 := (iff #296 false)
boehmes@41132
   397
#300 := [rewrite]: #299
boehmes@41132
   398
#297 := (iff #94 #296)
boehmes@41132
   399
#253 := (iff #82 false)
boehmes@41132
   400
#183 := (not #82)
boehmes@41132
   401
#189 := (or #79 #183)
boehmes@41132
   402
#261 := (iff #189 #183)
boehmes@41132
   403
#256 := (or false #183)
boehmes@41132
   404
#259 := (iff #256 #183)
boehmes@41132
   405
#260 := [rewrite]: #259
boehmes@41132
   406
#257 := (iff #189 #256)
boehmes@41132
   407
#254 := (iff #79 false)
boehmes@41132
   408
#123 := (not #79)
boehmes@36900
   409
decl f11 :: S1
boehmes@36900
   410
#44 := f11
boehmes@36900
   411
#45 := (= f11 f1)
boehmes@36900
   412
#46 := (not #45)
boehmes@36900
   413
#47 := (and #45 #46)
boehmes@36900
   414
decl f10 :: S1
boehmes@36900
   415
#41 := f10
boehmes@36900
   416
#42 := (= f10 f1)
boehmes@36900
   417
#48 := (or #42 #47)
boehmes@36900
   418
#43 := (not #42)
boehmes@36900
   419
#49 := (and #43 #48)
boehmes@36900
   420
#13 := (= f5 f1)
boehmes@36900
   421
#50 := (or #13 #49)
boehmes@36900
   422
#51 := (not #50)
boehmes@41132
   423
#236 := (iff #51 #123)
boehmes@41132
   424
#234 := (iff #50 #79)
boehmes@41132
   425
#229 := (or #79 false)
boehmes@41132
   426
#232 := (iff #229 #79)
boehmes@41132
   427
#233 := [rewrite]: #232
boehmes@41132
   428
#230 := (iff #50 #229)
boehmes@41132
   429
#227 := (iff #49 false)
boehmes@41132
   430
#195 := (= f1 f10)
boehmes@41132
   431
#199 := (not #195)
boehmes@41132
   432
#222 := (and #199 #195)
boehmes@41132
   433
#225 := (iff #222 false)
boehmes@41132
   434
#226 := [rewrite]: #225
boehmes@41132
   435
#223 := (iff #49 #222)
boehmes@41132
   436
#220 := (iff #48 #195)
boehmes@41132
   437
#215 := (or #195 false)
boehmes@41132
   438
#218 := (iff #215 #195)
boehmes@41132
   439
#219 := [rewrite]: #218
boehmes@41132
   440
#216 := (iff #48 #215)
boehmes@41132
   441
#213 := (iff #47 false)
boehmes@41132
   442
#202 := (= f1 f11)
boehmes@41132
   443
#205 := (not #202)
boehmes@41132
   444
#208 := (and #202 #205)
boehmes@41132
   445
#211 := (iff #208 false)
boehmes@41132
   446
#212 := [rewrite]: #211
boehmes@41132
   447
#209 := (iff #47 #208)
boehmes@41132
   448
#206 := (iff #46 #205)
boehmes@41132
   449
#203 := (iff #45 #202)
boehmes@41132
   450
#204 := [rewrite]: #203
boehmes@41132
   451
#207 := [monotonicity #204]: #206
boehmes@41132
   452
#210 := [monotonicity #204 #207]: #209
boehmes@41132
   453
#214 := [trans #210 #212]: #213
boehmes@41132
   454
#197 := (iff #42 #195)
boehmes@41132
   455
#198 := [rewrite]: #197
boehmes@41132
   456
#217 := [monotonicity #198 #214]: #216
boehmes@41132
   457
#221 := [trans #217 #219]: #220
boehmes@41132
   458
#200 := (iff #43 #199)
boehmes@41132
   459
#201 := [monotonicity #198]: #200
boehmes@41132
   460
#224 := [monotonicity #201 #221]: #223
boehmes@41132
   461
#228 := [trans #224 #226]: #227
boehmes@41132
   462
#80 := (iff #13 #79)
boehmes@41132
   463
#81 := [rewrite]: #80
boehmes@41132
   464
#231 := [monotonicity #81 #228]: #230
boehmes@41132
   465
#235 := [trans #231 #233]: #234
boehmes@41132
   466
#237 := [monotonicity #235]: #236
boehmes@41132
   467
#194 := [asserted]: #51
boehmes@41132
   468
#240 := [mp #194 #237]: #123
boehmes@41132
   469
#255 := [iff-false #240]: #254
boehmes@41132
   470
#258 := [monotonicity #255]: #257
boehmes@41132
   471
#262 := [trans #258 #260]: #261
boehmes@36900
   472
#15 := (= f6 f1)
boehmes@36900
   473
#38 := (or #15 false)
boehmes@36900
   474
#39 := (not #38)
boehmes@36900
   475
#40 := (or #39 #13)
boehmes@41132
   476
#192 := (iff #40 #189)
boehmes@41132
   477
#186 := (or #183 #79)
boehmes@41132
   478
#190 := (iff #186 #189)
boehmes@41132
   479
#191 := [rewrite]: #190
boehmes@41132
   480
#187 := (iff #40 #186)
boehmes@41132
   481
#184 := (iff #39 #183)
boehmes@41132
   482
#181 := (iff #38 #82)
boehmes@41132
   483
#175 := (or #82 false)
boehmes@41132
   484
#179 := (iff #175 #82)
boehmes@41132
   485
#180 := [rewrite]: #179
boehmes@41132
   486
#177 := (iff #38 #175)
boehmes@41132
   487
#83 := (iff #15 #82)
boehmes@41132
   488
#84 := [rewrite]: #83
boehmes@41132
   489
#178 := [monotonicity #84]: #177
boehmes@41132
   490
#182 := [trans #178 #180]: #181
boehmes@41132
   491
#185 := [monotonicity #182]: #184
boehmes@41132
   492
#188 := [monotonicity #185 #81]: #187
boehmes@41132
   493
#193 := [trans #188 #191]: #192
boehmes@41132
   494
#174 := [asserted]: #40
boehmes@41132
   495
#196 := [mp #174 #193]: #189
boehmes@41132
   496
#252 := [mp #196 #262]: #183
boehmes@41132
   497
#263 := [iff-false #252]: #253
boehmes@41132
   498
#251 := (iff #76 false)
boehmes@41132
   499
#168 := (not #76)
boehmes@41132
   500
#171 := (or #168 #79)
boehmes@41132
   501
#269 := (iff #171 #168)
boehmes@41132
   502
#264 := (or #168 false)
boehmes@41132
   503
#267 := (iff #264 #168)
boehmes@41132
   504
#268 := [rewrite]: #267
boehmes@41132
   505
#265 := (iff #171 #264)
boehmes@41132
   506
#266 := [monotonicity #255]: #265
boehmes@41132
   507
#270 := [trans #266 #268]: #269
boehmes@36900
   508
decl f9 :: S1
boehmes@36900
   509
#31 := f9
boehmes@36900
   510
#32 := (= f9 f1)
boehmes@36900
   511
#33 := (not #32)
boehmes@36900
   512
#34 := (or #32 #33)
boehmes@36900
   513
#11 := (= f4 f1)
boehmes@36900
   514
#35 := (and #11 #34)
boehmes@36900
   515
#36 := (not #35)
boehmes@36900
   516
#37 := (or #36 #13)
boehmes@41132
   517
#172 := (iff #37 #171)
boehmes@41132
   518
#169 := (iff #36 #168)
boehmes@41132
   519
#166 := (iff #35 #76)
boehmes@36900
   520
#1 := true
boehmes@41132
   521
#161 := (and #76 true)
boehmes@41132
   522
#164 := (iff #161 #76)
boehmes@41132
   523
#165 := [rewrite]: #164
boehmes@41132
   524
#162 := (iff #35 #161)
boehmes@41132
   525
#159 := (iff #34 true)
boehmes@41132
   526
#147 := (= f1 f9)
boehmes@41132
   527
#151 := (not #147)
boehmes@41132
   528
#154 := (or #147 #151)
boehmes@41132
   529
#157 := (iff #154 true)
boehmes@41132
   530
#158 := [rewrite]: #157
boehmes@41132
   531
#155 := (iff #34 #154)
boehmes@41132
   532
#152 := (iff #33 #151)
boehmes@41132
   533
#149 := (iff #32 #147)
boehmes@41132
   534
#150 := [rewrite]: #149
boehmes@41132
   535
#153 := [monotonicity #150]: #152
boehmes@41132
   536
#156 := [monotonicity #150 #153]: #155
boehmes@41132
   537
#160 := [trans #156 #158]: #159
boehmes@41132
   538
#77 := (iff #11 #76)
boehmes@41132
   539
#78 := [rewrite]: #77
boehmes@41132
   540
#163 := [monotonicity #78 #160]: #162
boehmes@41132
   541
#167 := [trans #163 #165]: #166
boehmes@41132
   542
#170 := [monotonicity #167]: #169
boehmes@41132
   543
#173 := [monotonicity #170 #81]: #172
boehmes@41132
   544
#146 := [asserted]: #37
boehmes@41132
   545
#176 := [mp #146 #173]: #171
boehmes@41132
   546
#250 := [mp #176 #270]: #168
boehmes@41132
   547
#271 := [iff-false #250]: #251
boehmes@41132
   548
#249 := (iff #73 false)
boehmes@41132
   549
#140 := (not #73)
boehmes@41132
   550
#143 := (or #140 #76)
boehmes@41132
   551
#277 := (iff #143 #140)
boehmes@41132
   552
#272 := (or #140 false)
boehmes@41132
   553
#275 := (iff #272 #140)
boehmes@41132
   554
#276 := [rewrite]: #275
boehmes@41132
   555
#273 := (iff #143 #272)
boehmes@41132
   556
#274 := [monotonicity #271]: #273
boehmes@41132
   557
#278 := [trans #274 #276]: #277
boehmes@36900
   558
#26 := (not #13)
boehmes@36900
   559
#27 := (and #13 #26)
boehmes@36900
   560
#9 := (= f3 f1)
boehmes@36900
   561
#28 := (or #9 #27)
boehmes@36900
   562
#29 := (not #28)
boehmes@36900
   563
#30 := (or #29 #11)
boehmes@41132
   564
#144 := (iff #30 #143)
boehmes@41132
   565
#141 := (iff #29 #140)
boehmes@41132
   566
#138 := (iff #28 #73)
boehmes@41132
   567
#133 := (or #73 false)
boehmes@41132
   568
#136 := (iff #133 #73)
boehmes@41132
   569
#137 := [rewrite]: #136
boehmes@41132
   570
#134 := (iff #28 #133)
boehmes@41132
   571
#131 := (iff #27 false)
boehmes@41132
   572
#126 := (and #79 #123)
boehmes@41132
   573
#129 := (iff #126 false)
boehmes@41132
   574
#130 := [rewrite]: #129
boehmes@41132
   575
#127 := (iff #27 #126)
boehmes@41132
   576
#124 := (iff #26 #123)
boehmes@41132
   577
#125 := [monotonicity #81]: #124
boehmes@41132
   578
#128 := [monotonicity #81 #125]: #127
boehmes@41132
   579
#132 := [trans #128 #130]: #131
boehmes@41132
   580
#74 := (iff #9 #73)
boehmes@41132
   581
#75 := [rewrite]: #74
boehmes@41132
   582
#135 := [monotonicity #75 #132]: #134
boehmes@41132
   583
#139 := [trans #135 #137]: #138
boehmes@41132
   584
#142 := [monotonicity #139]: #141
boehmes@41132
   585
#145 := [monotonicity #142 #78]: #144
boehmes@41132
   586
#122 := [asserted]: #30
boehmes@41132
   587
#148 := [mp #122 #145]: #143
boehmes@41132
   588
#248 := [mp #148 #278]: #140
boehmes@41132
   589
#279 := [iff-false #248]: #249
boehmes@41132
   590
#298 := [monotonicity #279 #271 #255 #263]: #297
boehmes@41132
   591
#302 := [trans #298 #300]: #301
boehmes@36900
   592
#16 := (or #13 #15)
boehmes@36900
   593
#17 := (or #11 #16)
boehmes@36900
   594
#18 := (or #9 #17)
boehmes@41132
   595
#97 := (iff #18 #94)
boehmes@41132
   596
#85 := (or #79 #82)
boehmes@41132
   597
#88 := (or #76 #85)
boehmes@41132
   598
#91 := (or #73 #88)
boehmes@41132
   599
#95 := (iff #91 #94)
boehmes@41132
   600
#96 := [rewrite]: #95
boehmes@41132
   601
#92 := (iff #18 #91)
boehmes@41132
   602
#89 := (iff #17 #88)
boehmes@41132
   603
#86 := (iff #16 #85)
boehmes@41132
   604
#87 := [monotonicity #81 #84]: #86
boehmes@41132
   605
#90 := [monotonicity #78 #87]: #89
boehmes@41132
   606
#93 := [monotonicity #75 #90]: #92
boehmes@41132
   607
#98 := [trans #93 #96]: #97
boehmes@41132
   608
#72 := [asserted]: #18
boehmes@41132
   609
#99 := [mp #72 #98]: #94
boehmes@41132
   610
[mp #99 #302]: false
boehmes@41132
   611
unsat
boehmes@43555
   612
dd0cba0a17795cc066f8c77647c6bcb52b690616 59 0
boehmes@43555
   613
#2 := false
boehmes@43555
   614
decl f3 :: (-> S3 S2 S2)
boehmes@43555
   615
decl f6 :: S2
boehmes@43555
   616
#17 := f6
boehmes@43555
   617
decl f4 :: (-> S4 S2 S3)
boehmes@43555
   618
decl f7 :: S2
boehmes@43555
   619
#20 := f7
boehmes@43555
   620
decl f5 :: S4
boehmes@43555
   621
#8 := f5
boehmes@43555
   622
#22 := (f4 f5 f7)
boehmes@43555
   623
#23 := (f3 #22 f6)
boehmes@43555
   624
#19 := (f4 f5 f6)
boehmes@43555
   625
#21 := (f3 #19 f7)
boehmes@43555
   626
#24 := (= #21 #23)
boehmes@43555
   627
#57 := (not #24)
boehmes@43555
   628
#18 := (= f6 f6)
boehmes@43555
   629
#25 := (and #18 #24)
boehmes@43555
   630
#26 := (not #25)
boehmes@43555
   631
#58 := (iff #26 #57)
boehmes@43555
   632
#55 := (iff #25 #24)
boehmes@41064
   633
#1 := true
boehmes@43555
   634
#50 := (and true #24)
boehmes@43555
   635
#53 := (iff #50 #24)
boehmes@43555
   636
#54 := [rewrite]: #53
boehmes@43555
   637
#51 := (iff #25 #50)
boehmes@43555
   638
#48 := (iff #18 true)
boehmes@41132
   639
#49 := [rewrite]: #48
boehmes@43555
   640
#52 := [monotonicity #49]: #51
boehmes@43555
   641
#56 := [trans #52 #54]: #55
boehmes@43555
   642
#59 := [monotonicity #56]: #58
boehmes@43555
   643
#47 := [asserted]: #26
boehmes@43555
   644
#62 := [mp #47 #59]: #57
boehmes@43555
   645
#9 := (:var 1 S2)
boehmes@43555
   646
#11 := (:var 0 S2)
boehmes@43555
   647
#13 := (f4 f5 #11)
boehmes@43555
   648
#14 := (f3 #13 #9)
boehmes@43555
   649
#543 := (pattern #14)
boehmes@43555
   650
#10 := (f4 f5 #9)
boehmes@43555
   651
#12 := (f3 #10 #11)
boehmes@43555
   652
#542 := (pattern #12)
boehmes@43555
   653
#15 := (= #12 #14)
boehmes@43555
   654
#544 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #542 #543) #15)
boehmes@43555
   655
#16 := (forall (vars (?v0 S2) (?v1 S2)) #15)
boehmes@43555
   656
#547 := (iff #16 #544)
boehmes@43555
   657
#545 := (iff #15 #15)
boehmes@43555
   658
#546 := [refl]: #545
boehmes@43555
   659
#548 := [quant-intro #546]: #547
boehmes@43555
   660
#70 := (~ #16 #16)
boehmes@43555
   661
#68 := (~ #15 #15)
boehmes@43555
   662
#69 := [refl]: #68
boehmes@43555
   663
#71 := [nnf-pos #69]: #70
boehmes@43555
   664
#46 := [asserted]: #16
boehmes@43555
   665
#61 := [mp~ #46 #71]: #16
boehmes@43555
   666
#549 := [mp #61 #548]: #544
boehmes@43555
   667
#125 := (not #544)
boehmes@43555
   668
#212 := (or #125 #24)
boehmes@43555
   669
#126 := [quant-inst #17 #20]: #212
boehmes@43555
   670
[unit-resolution #126 #549 #62]: false
boehmes@41132
   671
unsat
boehmes@41132
   672
0863329327da9e45e4d77f7bc111e467c5d58d3c 2526 0
boehmes@41132
   673
#2 := false
boehmes@41132
   674
decl f9 :: S1
boehmes@41132
   675
#26 := f9
boehmes@36900
   676
decl f1 :: S1
boehmes@36900
   677
#4 := f1
boehmes@41132
   678
#493 := (= f1 f9)
boehmes@41132
   679
decl f20 :: S1
boehmes@41132
   680
#60 := f20
boehmes@41132
   681
#629 := (= f1 f20)
boehmes@41132
   682
decl f21 :: S1
boehmes@41132
   683
#62 := f21
boehmes@41132
   684
#632 := (= f1 f21)
boehmes@41132
   685
#1513 := (not #632)
boehmes@41132
   686
decl f31 :: S1
boehmes@41132
   687
#98 := f31
boehmes@41132
   688
#782 := (= f1 f31)
boehmes@41132
   689
decl f62 :: S1
boehmes@41132
   690
#208 := f62
boehmes@41132
   691
#1242 := (= f1 f62)
boehmes@41132
   692
decl f58 :: S1
boehmes@41132
   693
#190 := f58
boehmes@41132
   694
#1145 := (= f1 f58)
boehmes@41132
   695
#2559 := (not #1145)
boehmes@36900
   696
decl f47 :: S1
boehmes@36900
   697
#152 := f47
boehmes@41132
   698
#992 := (= f1 f47)
boehmes@41132
   699
#1817 := (not #782)
boehmes@41132
   700
#3000 := [hypothesis]: #1817
boehmes@36900
   701
decl f46 :: S1
boehmes@36900
   702
#150 := f46
boehmes@41132
   703
#989 := (= f1 f46)
boehmes@41132
   704
#2247 := (not #989)
boehmes@41132
   705
decl f48 :: S1
boehmes@41132
   706
#157 := f48
boehmes@41132
   707
#1016 := (= f1 f48)
boehmes@41132
   708
decl f57 :: S1
boehmes@41132
   709
#188 := f57
boehmes@41132
   710
#1142 := (= f1 f57)
boehmes@41132
   711
#2555 := (not #1142)
boehmes@36900
   712
decl f45 :: S1
boehmes@36900
   713
#145 := f45
boehmes@41132
   714
#965 := (= f1 f45)
boehmes@41132
   715
#2190 := (not #965)
boehmes@41132
   716
decl f42 :: S1
boehmes@41132
   717
#136 := f42
boehmes@41132
   718
#935 := (= f1 f42)
boehmes@41132
   719
#3487 := (or #935 #782)
boehmes@41132
   720
decl f40 :: S1
boehmes@41132
   721
#129 := f40
boehmes@41132
   722
#908 := (= f1 f40)
boehmes@41132
   723
#2125 := (not #935)
boehmes@41132
   724
#3115 := [hypothesis]: #2125
boehmes@41132
   725
decl f32 :: S1
boehmes@41132
   726
#100 := f32
boehmes@41132
   727
#785 := (= f1 f32)
boehmes@41132
   728
#1821 := (not #785)
boehmes@41132
   729
decl f16 :: S1
boehmes@41132
   730
#47 := f16
boehmes@41132
   731
#577 := (= f1 f16)
boehmes@41132
   732
decl f17 :: S1
boehmes@41132
   733
#49 := f17
boehmes@41132
   734
#581 := (= f1 f17)
boehmes@41132
   735
#1421 := (not #581)
boehmes@41132
   736
decl f28 :: S1
boehmes@41132
   737
#87 := f28
boehmes@41132
   738
#734 := (= f1 f28)
boehmes@41132
   739
#3470 := (or #734 #782 #935)
boehmes@41132
   740
decl f29 :: S1
boehmes@41132
   741
#91 := f29
boehmes@41132
   742
#755 := (= f1 f29)
boehmes@41132
   743
#1756 := (not #755)
boehmes@41132
   744
#2064 := (not #908)
boehmes@41132
   745
#1729 := (not #734)
boehmes@41132
   746
#2887 := [hypothesis]: #1729
boehmes@41132
   747
#3447 := (or #2064 #734)
boehmes@41132
   748
decl f51 :: S1
boehmes@41132
   749
#167 := f51
boehmes@41132
   750
#1061 := (= f1 f51)
boehmes@41132
   751
#2372 := (not #1061)
boehmes@41132
   752
decl f54 :: S1
boehmes@41132
   753
#176 := f54
boehmes@41132
   754
#1091 := (= f1 f54)
boehmes@36900
   755
decl f56 :: S1
boehmes@36900
   756
#183 := f56
boehmes@41132
   757
#1118 := (= f1 f56)
boehmes@41132
   758
#2498 := (not #1118)
boehmes@41132
   759
#2437 := (not #1091)
boehmes@41132
   760
#3180 := [hypothesis]: #2437
boehmes@41132
   761
#3209 := (or #2559 #1091)
boehmes@41132
   762
decl f18 :: S1
boehmes@41132
   763
#53 := f18
boehmes@41132
   764
#602 := (= f1 f18)
boehmes@41132
   765
decl f33 :: S1
boehmes@41132
   766
#105 := f33
boehmes@41132
   767
#809 := (= f1 f33)
boehmes@41132
   768
#1878 := (not #809)
boehmes@41132
   769
decl f36 :: S1
boehmes@41132
   770
#114 := f36
boehmes@41132
   771
#839 := (= f1 f36)
boehmes@41132
   772
#2251 := (not #992)
boehmes@41132
   773
#3175 := [hypothesis]: #1145
boehmes@41132
   774
#2600 := (or #2251 #2559)
boehmes@41132
   775
#153 := (= f47 f1)
boehmes@41132
   776
#348 := (not #153)
boehmes@36900
   777
#191 := (= f58 f1)
boehmes@36900
   778
#389 := (not #191)
boehmes@41132
   779
#394 := (or #389 #348)
boehmes@41132
   780
#2603 := (iff #394 #2600)
boehmes@41132
   781
#2596 := (or #2559 #2251)
boehmes@41132
   782
#2601 := (iff #2596 #2600)
boehmes@41132
   783
#2602 := [rewrite]: #2601
boehmes@41132
   784
#2598 := (iff #394 #2596)
boehmes@41132
   785
#2252 := (iff #348 #2251)
boehmes@41132
   786
#993 := (iff #153 #992)
boehmes@41132
   787
#994 := [rewrite]: #993
boehmes@41132
   788
#2253 := [monotonicity #994]: #2252
boehmes@41132
   789
#2560 := (iff #389 #2559)
boehmes@41132
   790
#1146 := (iff #191 #1145)
boehmes@41132
   791
#1147 := [rewrite]: #1146
boehmes@41132
   792
#2561 := [monotonicity #1147]: #2560
boehmes@41132
   793
#2599 := [monotonicity #2561 #2253]: #2598
boehmes@41132
   794
#2604 := [trans #2599 #2602]: #2603
boehmes@41132
   795
#2595 := [asserted]: #394
boehmes@41132
   796
#2607 := [mp #2595 #2604]: #2600
boehmes@41132
   797
#3176 := [unit-resolution #2607 #3175]: #2251
boehmes@41132
   798
#2562 := (or #2555 #2559)
boehmes@41132
   799
#189 := (= f57 f1)
boehmes@41132
   800
#388 := (not #189)
boehmes@36900
   801
#390 := (or #388 #389)
boehmes@41132
   802
#2563 := (iff #390 #2562)
boehmes@41132
   803
#2557 := (iff #388 #2555)
boehmes@41132
   804
#1143 := (iff #189 #1142)
boehmes@36900
   805
#1144 := [rewrite]: #1143
boehmes@36900
   806
#2558 := [monotonicity #1144]: #2557
boehmes@41132
   807
#2564 := [monotonicity #2558 #2561]: #2563
boehmes@41132
   808
#2554 := [asserted]: #390
boehmes@41132
   809
#2567 := [mp #2554 #2564]: #2562
boehmes@41132
   810
#3177 := [unit-resolution #2567 #3175]: #2555
boehmes@41132
   811
#1172 := (or #1016 #1142)
boehmes@41132
   812
decl f6 :: S1
boehmes@41132
   813
#17 := f6
boehmes@41132
   814
#460 := (= f1 f6)
boehmes@41132
   815
#1180 := (or #460 #1016 #1142)
boehmes@41132
   816
#2860 := (iff #1180 #1172)
boehmes@41132
   817
#2855 := (or false #1016 #1142)
boehmes@41132
   818
#2858 := (iff #2855 #1172)
boehmes@41132
   819
#2859 := [rewrite]: #2858
boehmes@41132
   820
#2856 := (iff #1180 #2855)
boehmes@41132
   821
#2779 := (iff #460 false)
boehmes@41132
   822
#464 := (not #460)
boehmes@41132
   823
#18 := (= f6 f1)
boehmes@41132
   824
#19 := (not #18)
boehmes@41132
   825
#465 := (iff #19 #464)
boehmes@41132
   826
#462 := (iff #18 #460)
boehmes@41132
   827
#463 := [rewrite]: #462
boehmes@41132
   828
#466 := [monotonicity #463]: #465
boehmes@41132
   829
#459 := [asserted]: #19
boehmes@41132
   830
#469 := [mp #459 #466]: #464
boehmes@41132
   831
#2780 := [iff-false #469]: #2779
boehmes@41132
   832
#2857 := [monotonicity #2780]: #2856
boehmes@41132
   833
#2861 := [trans #2857 #2859]: #2860
boehmes@41132
   834
#158 := (= f48 f1)
boehmes@41132
   835
#195 := (or #189 #158)
boehmes@41132
   836
#196 := (or #18 #195)
boehmes@41132
   837
#1183 := (iff #196 #1180)
boehmes@41132
   838
#1177 := (or #460 #1172)
boehmes@41132
   839
#1181 := (iff #1177 #1180)
boehmes@41132
   840
#1182 := [rewrite]: #1181
boehmes@41132
   841
#1178 := (iff #196 #1177)
boehmes@41132
   842
#1175 := (iff #195 #1172)
boehmes@41132
   843
#1169 := (or #1142 #1016)
boehmes@41132
   844
#1173 := (iff #1169 #1172)
boehmes@41132
   845
#1174 := [rewrite]: #1173
boehmes@41132
   846
#1170 := (iff #195 #1169)
boehmes@41132
   847
#1017 := (iff #158 #1016)
boehmes@41132
   848
#1018 := [rewrite]: #1017
boehmes@41132
   849
#1171 := [monotonicity #1144 #1018]: #1170
boehmes@41132
   850
#1176 := [trans #1171 #1174]: #1175
boehmes@41132
   851
#1179 := [monotonicity #463 #1176]: #1178
boehmes@41132
   852
#1184 := [trans #1179 #1182]: #1183
boehmes@41132
   853
#1168 := [asserted]: #196
boehmes@41132
   854
#1185 := [mp #1168 #1184]: #1180
boehmes@41132
   855
#2862 := [mp #1185 #2861]: #1172
boehmes@41132
   856
#3178 := [unit-resolution #2862 #3177]: #1016
boehmes@41132
   857
#2308 := (not #1016)
boehmes@41132
   858
#2315 := (or #2247 #2308)
boehmes@41132
   859
#151 := (= f46 f1)
boehmes@41132
   860
#347 := (not #151)
boehmes@41132
   861
#355 := (not #158)
boehmes@41132
   862
#356 := (or #355 #347)
boehmes@41132
   863
#2318 := (iff #356 #2315)
boehmes@41132
   864
#2312 := (or #2308 #2247)
boehmes@41132
   865
#2316 := (iff #2312 #2315)
boehmes@41132
   866
#2317 := [rewrite]: #2316
boehmes@41132
   867
#2313 := (iff #356 #2312)
boehmes@41132
   868
#2249 := (iff #347 #2247)
boehmes@41132
   869
#990 := (iff #151 #989)
boehmes@41132
   870
#991 := [rewrite]: #990
boehmes@41132
   871
#2250 := [monotonicity #991]: #2249
boehmes@41132
   872
#2310 := (iff #355 #2308)
boehmes@41132
   873
#2311 := [monotonicity #1018]: #2310
boehmes@41132
   874
#2314 := [monotonicity #2311 #2250]: #2313
boehmes@41132
   875
#2319 := [trans #2314 #2317]: #2318
boehmes@41132
   876
#2307 := [asserted]: #356
boehmes@41132
   877
#2322 := [mp #2307 #2319]: #2315
boehmes@41132
   878
#3179 := [unit-resolution #2322 #3178]: #2247
boehmes@41132
   879
decl f44 :: S1
boehmes@41132
   880
#143 := f44
boehmes@41132
   881
#962 := (= f1 f44)
boehmes@41132
   882
#2186 := (not #962)
boehmes@36900
   883
decl f61 :: S1
boehmes@36900
   884
#204 := f61
boehmes@41132
   885
#1221 := (= f1 f61)
boehmes@36900
   886
decl f60 :: S1
boehmes@36900
   887
#200 := f60
boehmes@41132
   888
#1199 := (= f1 f60)
boehmes@41132
   889
#2649 := (not #1199)
boehmes@41132
   890
decl f37 :: S1
boehmes@41132
   891
#119 := f37
boehmes@41132
   892
#863 := (= f1 f37)
boehmes@41132
   893
#2000 := (not #863)
boehmes@41132
   894
#2325 := (or #2000 #2308)
boehmes@41132
   895
#120 := (= f37 f1)
boehmes@41132
   896
#314 := (not #120)
boehmes@41132
   897
#357 := (or #355 #314)
boehmes@41132
   898
#2328 := (iff #357 #2325)
boehmes@41132
   899
#2321 := (or #2308 #2000)
boehmes@41132
   900
#2326 := (iff #2321 #2325)
boehmes@41132
   901
#2327 := [rewrite]: #2326
boehmes@41132
   902
#2323 := (iff #357 #2321)
boehmes@41132
   903
#2002 := (iff #314 #2000)
boehmes@41132
   904
#864 := (iff #120 #863)
boehmes@41132
   905
#865 := [rewrite]: #864
boehmes@41132
   906
#2003 := [monotonicity #865]: #2002
boehmes@41132
   907
#2324 := [monotonicity #2311 #2003]: #2323
boehmes@41132
   908
#2329 := [trans #2324 #2327]: #2328
boehmes@41132
   909
#2320 := [asserted]: #357
boehmes@41132
   910
#2332 := [mp #2320 #2329]: #2325
boehmes@41132
   911
#3181 := [unit-resolution #2332 #3178]: #2000
boehmes@41132
   912
#3003 := (or #2649 #989 #992 #863)
boehmes@41132
   913
#1509 := (not #629)
boehmes@41132
   914
decl f23 :: S1
boehmes@41132
   915
#69 := f23
boehmes@41132
   916
#659 := (= f1 f23)
boehmes@41132
   917
decl f34 :: S1
boehmes@41132
   918
#107 := f34
boehmes@41132
   919
#812 := (= f1 f34)
boehmes@41132
   920
#1882 := (not #812)
boehmes@41132
   921
#3071 := [hypothesis]: #2251
boehmes@41132
   922
#3072 := [hypothesis]: #2247
boehmes@41132
   923
#1943 := (not #839)
boehmes@41132
   924
decl f25 :: S1
boehmes@41132
   925
#76 := f25
boehmes@41132
   926
#686 := (= f1 f25)
boehmes@41132
   927
decl f39 :: S1
boehmes@41132
   928
#125 := f39
boehmes@41132
   929
#887 := (= f1 f39)
boehmes@41132
   930
#2037 := (not #887)
boehmes@41132
   931
decl f50 :: S1
boehmes@41132
   932
#163 := f50
boehmes@41132
   933
#1040 := (= f1 f50)
boehmes@41132
   934
decl f59 :: S1
boehmes@41132
   935
#197 := f59
boehmes@41132
   936
#1187 := (= f1 f59)
boehmes@41132
   937
#2636 := (not #1187)
boehmes@41132
   938
#3044 := [hypothesis]: #1199
boehmes@41132
   939
#2656 := (or #2636 #2649)
boehmes@41132
   940
#198 := (= f59 f1)
boehmes@41132
   941
#399 := (not #198)
boehmes@36900
   942
#201 := (= f60 f1)
boehmes@41132
   943
#401 := (not #201)
boehmes@41132
   944
#402 := (or #401 #399)
boehmes@41132
   945
#2659 := (iff #402 #2656)
boehmes@41132
   946
#2653 := (or #2649 #2636)
boehmes@41132
   947
#2657 := (iff #2653 #2656)
boehmes@41132
   948
#2658 := [rewrite]: #2657
boehmes@41132
   949
#2654 := (iff #402 #2653)
boehmes@41132
   950
#2638 := (iff #399 #2636)
boehmes@41132
   951
#1188 := (iff #198 #1187)
boehmes@41132
   952
#1189 := [rewrite]: #1188
boehmes@41132
   953
#2639 := [monotonicity #1189]: #2638
boehmes@41132
   954
#2651 := (iff #401 #2649)
boehmes@41132
   955
#1201 := (iff #201 #1199)
boehmes@41132
   956
#1202 := [rewrite]: #1201
boehmes@41132
   957
#2652 := [monotonicity #1202]: #2651
boehmes@41132
   958
#2655 := [monotonicity #2652 #2639]: #2654
boehmes@41132
   959
#2660 := [trans #2655 #2658]: #2659
boehmes@41132
   960
#2648 := [asserted]: #402
boehmes@41132
   961
#2663 := [mp #2648 #2660]: #2656
boehmes@41132
   962
#3041 := [unit-resolution #2663 #3044]: #2636
boehmes@41132
   963
#1193 := (or #1040 #1187)
boehmes@41132
   964
#164 := (= f50 f1)
boehmes@41132
   965
#199 := (or #198 #164)
boehmes@41132
   966
#1196 := (iff #199 #1193)
boehmes@41132
   967
#1190 := (or #1187 #1040)
boehmes@41132
   968
#1194 := (iff #1190 #1193)
boehmes@41132
   969
#1195 := [rewrite]: #1194
boehmes@41132
   970
#1191 := (iff #199 #1190)
boehmes@41132
   971
#1041 := (iff #164 #1040)
boehmes@41132
   972
#1042 := [rewrite]: #1041
boehmes@41132
   973
#1192 := [monotonicity #1189 #1042]: #1191
boehmes@41132
   974
#1197 := [trans #1192 #1195]: #1196
boehmes@41132
   975
#1186 := [asserted]: #199
boehmes@41132
   976
#1200 := [mp #1186 #1197]: #1193
boehmes@41132
   977
#3042 := [unit-resolution #1200 #3041]: #1040
boehmes@41132
   978
#2345 := (not #1040)
boehmes@41132
   979
#2366 := (or #2037 #2345)
boehmes@41132
   980
#126 := (= f39 f1)
boehmes@41132
   981
#319 := (not #126)
boehmes@41132
   982
#360 := (not #164)
boehmes@41132
   983
#363 := (or #360 #319)
boehmes@41132
   984
#2369 := (iff #363 #2366)
boehmes@41132
   985
#2362 := (or #2345 #2037)
boehmes@41132
   986
#2367 := (iff #2362 #2366)
boehmes@41132
   987
#2368 := [rewrite]: #2367
boehmes@41132
   988
#2364 := (iff #363 #2362)
boehmes@41132
   989
#2038 := (iff #319 #2037)
boehmes@41132
   990
#888 := (iff #126 #887)
boehmes@41132
   991
#889 := [rewrite]: #888
boehmes@41132
   992
#2039 := [monotonicity #889]: #2038
boehmes@41132
   993
#2346 := (iff #360 #2345)
boehmes@41132
   994
#2347 := [monotonicity #1042]: #2346
boehmes@41132
   995
#2365 := [monotonicity #2347 #2039]: #2364
boehmes@41132
   996
#2370 := [trans #2365 #2368]: #2369
boehmes@41132
   997
#2361 := [asserted]: #363
boehmes@41132
   998
#2373 := [mp #2361 #2370]: #2366
boehmes@41132
   999
#3039 := [unit-resolution #2373 #3042]: #2037
boehmes@41132
  1000
decl f26 :: S1
boehmes@41132
  1001
#81 := f26
boehmes@41132
  1002
#710 := (= f1 f26)
boehmes@41132
  1003
#3173 := [hypothesis]: #2000
boehmes@41132
  1004
decl f35 :: S1
boehmes@41132
  1005
#112 := f35
boehmes@41132
  1006
#836 := (= f1 f35)
boehmes@41132
  1007
#1939 := (not #836)
boehmes@41132
  1008
decl f43 :: S1
boehmes@41132
  1009
#138 := f43
boehmes@41132
  1010
#938 := (= f1 f43)
boehmes@41132
  1011
#2129 := (not #938)
boehmes@41132
  1012
decl f52 :: S1
boehmes@41132
  1013
#169 := f52
boehmes@41132
  1014
#1064 := (= f1 f52)
boehmes@41132
  1015
#2376 := (not #1064)
boehmes@41132
  1016
#2666 := (or #2376 #2649)
boehmes@36900
  1017
#170 := (= f52 f1)
boehmes@36900
  1018
#365 := (not #170)
boehmes@36900
  1019
#403 := (or #401 #365)
boehmes@41132
  1020
#2669 := (iff #403 #2666)
boehmes@41132
  1021
#2662 := (or #2649 #2376)
boehmes@41132
  1022
#2667 := (iff #2662 #2666)
boehmes@41132
  1023
#2668 := [rewrite]: #2667
boehmes@41132
  1024
#2664 := (iff #403 #2662)
boehmes@41132
  1025
#2377 := (iff #365 #2376)
boehmes@41132
  1026
#1065 := (iff #170 #1064)
boehmes@41132
  1027
#1066 := [rewrite]: #1065
boehmes@41132
  1028
#2378 := [monotonicity #1066]: #2377
boehmes@41132
  1029
#2665 := [monotonicity #2652 #2378]: #2664
boehmes@41132
  1030
#2670 := [trans #2665 #2668]: #2669
boehmes@41132
  1031
#2661 := [asserted]: #403
boehmes@41132
  1032
#2673 := [mp #2661 #2670]: #2666
boehmes@41132
  1033
#3040 := [unit-resolution #2673 #3044]: #2376
boehmes@36900
  1034
decl f49 :: S1
boehmes@36900
  1035
#161 := f49
boehmes@41132
  1036
#1037 := (= f1 f49)
boehmes@41132
  1037
#2341 := (not #1037)
boehmes@41132
  1038
#2348 := (or #2341 #2345)
boehmes@36900
  1039
#162 := (= f49 f1)
boehmes@36900
  1040
#359 := (not #162)
boehmes@36900
  1041
#361 := (or #359 #360)
boehmes@41132
  1042
#2349 := (iff #361 #2348)
boehmes@41132
  1043
#2343 := (iff #359 #2341)
boehmes@41132
  1044
#1038 := (iff #162 #1037)
boehmes@41132
  1045
#1039 := [rewrite]: #1038
boehmes@36900
  1046
#2344 := [monotonicity #1039]: #2343
boehmes@41132
  1047
#2350 := [monotonicity #2344 #2347]: #2349
boehmes@41132
  1048
#2340 := [asserted]: #361
boehmes@41132
  1049
#2353 := [mp #2340 #2350]: #2348
boehmes@41132
  1050
#3037 := [unit-resolution #2353 #3042]: #2341
boehmes@41132
  1051
decl f41 :: S1
boehmes@41132
  1052
#131 := f41
boehmes@41132
  1053
#911 := (= f1 f41)
boehmes@41132
  1054
#2068 := (not #911)
boehmes@41132
  1055
#3146 := (or #2068 #863 #887)
boehmes@41132
  1056
#1692 := (not #710)
boehmes@41132
  1057
decl f15 :: S1
boehmes@41132
  1058
#44 := f15
boehmes@41132
  1059
#565 := (= f1 f15)
boehmes@41132
  1060
decl f13 :: S1
boehmes@41132
  1061
#38 := f13
boehmes@41132
  1062
#541 := (= f1 f13)
boehmes@41132
  1063
#1373 := (not #541)
boehmes@41132
  1064
decl f11 :: S1
boehmes@41132
  1065
#32 := f11
boehmes@41132
  1066
#517 := (= f1 f11)
boehmes@41132
  1067
#1311 := (not #493)
boehmes@41132
  1068
decl f7 :: S1
boehmes@41132
  1069
#20 := f7
boehmes@41132
  1070
#468 := (= f1 f7)
boehmes@41132
  1071
decl f8 :: S1
boehmes@41132
  1072
#22 := f8
boehmes@41132
  1073
#472 := (= f1 f8)
boehmes@41132
  1074
#1284 := (not #472)
boehmes@41132
  1075
#3174 := [hypothesis]: #2037
boehmes@41132
  1076
decl f38 :: S1
boehmes@41132
  1077
#123 := f38
boehmes@41132
  1078
#884 := (= f1 f38)
boehmes@41132
  1079
#2033 := (not #884)
boehmes@41132
  1080
#3171 := [hypothesis]: #911
boehmes@41132
  1081
#2099 := (or #2033 #2068)
boehmes@41132
  1082
#124 := (= f38 f1)
boehmes@41132
  1083
#318 := (not #124)
boehmes@36900
  1084
#132 := (= f41 f1)
boehmes@36900
  1085
#324 := (not #132)
boehmes@41132
  1086
#328 := (or #324 #318)
boehmes@41132
  1087
#2102 := (iff #328 #2099)
boehmes@41132
  1088
#2095 := (or #2068 #2033)
boehmes@41132
  1089
#2100 := (iff #2095 #2099)
boehmes@41132
  1090
#2101 := [rewrite]: #2100
boehmes@41132
  1091
#2097 := (iff #328 #2095)
boehmes@41132
  1092
#2035 := (iff #318 #2033)
boehmes@41132
  1093
#885 := (iff #124 #884)
boehmes@36900
  1094
#886 := [rewrite]: #885
boehmes@36900
  1095
#2036 := [monotonicity #886]: #2035
boehmes@41132
  1096
#2069 := (iff #324 #2068)
boehmes@41132
  1097
#912 := (iff #132 #911)
boehmes@41132
  1098
#913 := [rewrite]: #912
boehmes@41132
  1099
#2070 := [monotonicity #913]: #2069
boehmes@41132
  1100
#2098 := [monotonicity #2070 #2036]: #2097
boehmes@41132
  1101
#2103 := [trans #2098 #2101]: #2102
boehmes@41132
  1102
#2094 := [asserted]: #328
boehmes@41132
  1103
#2106 := [mp #2094 #2103]: #2099
boehmes@41132
  1104
#3172 := [unit-resolution #2106 #3171]: #2033
boehmes@41132
  1105
#901 := (or #734 #884 #887)
boehmes@36900
  1106
#88 := (= f28 f1)
boehmes@36900
  1107
#127 := (or #126 #88)
boehmes@36900
  1108
#128 := (or #124 #127)
boehmes@41132
  1109
#904 := (iff #128 #901)
boehmes@41132
  1110
#893 := (or #734 #887)
boehmes@41132
  1111
#898 := (or #884 #893)
boehmes@41132
  1112
#902 := (iff #898 #901)
boehmes@41132
  1113
#903 := [rewrite]: #902
boehmes@41132
  1114
#899 := (iff #128 #898)
boehmes@41132
  1115
#896 := (iff #127 #893)
boehmes@41132
  1116
#890 := (or #887 #734)
boehmes@41132
  1117
#894 := (iff #890 #893)
boehmes@41132
  1118
#895 := [rewrite]: #894
boehmes@41132
  1119
#891 := (iff #127 #890)
boehmes@41132
  1120
#735 := (iff #88 #734)
boehmes@41132
  1121
#736 := [rewrite]: #735
boehmes@41132
  1122
#892 := [monotonicity #889 #736]: #891
boehmes@41132
  1123
#897 := [trans #892 #895]: #896
boehmes@41132
  1124
#900 := [monotonicity #886 #897]: #899
boehmes@41132
  1125
#905 := [trans #900 #903]: #904
boehmes@41132
  1126
#883 := [asserted]: #128
boehmes@41132
  1127
#906 := [mp #883 #905]: #901
boehmes@41132
  1128
#3169 := [unit-resolution #906 #3172 #3174]: #734
boehmes@41132
  1129
#1750 := (or #1421 #1729)
boehmes@41132
  1130
#50 := (= f17 f1)
boehmes@41132
  1131
#237 := (not #50)
boehmes@36900
  1132
#278 := (not #88)
boehmes@41132
  1133
#281 := (or #278 #237)
boehmes@41132
  1134
#1753 := (iff #281 #1750)
boehmes@41132
  1135
#1746 := (or #1729 #1421)
boehmes@41132
  1136
#1751 := (iff #1746 #1750)
boehmes@41132
  1137
#1752 := [rewrite]: #1751
boehmes@41132
  1138
#1748 := (iff #281 #1746)
boehmes@41132
  1139
#1422 := (iff #237 #1421)
boehmes@41132
  1140
#582 := (iff #50 #581)
boehmes@41132
  1141
#583 := [rewrite]: #582
boehmes@41132
  1142
#1423 := [monotonicity #583]: #1422
boehmes@41132
  1143
#1730 := (iff #278 #1729)
boehmes@41132
  1144
#1731 := [monotonicity #736]: #1730
boehmes@41132
  1145
#1749 := [monotonicity #1731 #1423]: #1748
boehmes@41132
  1146
#1754 := [trans #1749 #1752]: #1753
boehmes@41132
  1147
#1745 := [asserted]: #281
boehmes@41132
  1148
#1757 := [mp #1745 #1754]: #1750
boehmes@41132
  1149
#3170 := [unit-resolution #1757 #3169]: #1421
boehmes@41132
  1150
#2803 := (or #577 #581)
boehmes@41132
  1151
decl f4 :: S1
boehmes@41132
  1152
#11 := f4
boehmes@41132
  1153
#444 := (= f1 f4)
boehmes@41132
  1154
#595 := (or #444 #577 #581)
boehmes@41132
  1155
#2806 := (iff #595 #2803)
boehmes@41132
  1156
#2800 := (or false #577 #581)
boehmes@41132
  1157
#2804 := (iff #2800 #2803)
boehmes@41132
  1158
#2805 := [rewrite]: #2804
boehmes@41132
  1159
#2801 := (iff #595 #2800)
boehmes@41132
  1160
#2775 := (iff #444 false)
boehmes@41132
  1161
#448 := (not #444)
boehmes@41132
  1162
#12 := (= f4 f1)
boehmes@41132
  1163
#13 := (not #12)
boehmes@41132
  1164
#449 := (iff #13 #448)
boehmes@41132
  1165
#446 := (iff #12 #444)
boehmes@41132
  1166
#447 := [rewrite]: #446
boehmes@41132
  1167
#450 := [monotonicity #447]: #449
boehmes@41132
  1168
#443 := [asserted]: #13
boehmes@41132
  1169
#453 := [mp #443 #450]: #448
boehmes@41132
  1170
#2776 := [iff-false #453]: #2775
boehmes@41132
  1171
#2802 := [monotonicity #2776]: #2801
boehmes@41132
  1172
#2807 := [trans #2802 #2805]: #2806
boehmes@41132
  1173
#51 := (or #50 #12)
boehmes@41132
  1174
#48 := (= f16 f1)
boehmes@41132
  1175
#52 := (or #48 #51)
boehmes@41132
  1176
#598 := (iff #52 #595)
boehmes@41132
  1177
#587 := (or #444 #581)
boehmes@41132
  1178
#592 := (or #577 #587)
boehmes@41132
  1179
#596 := (iff #592 #595)
boehmes@41132
  1180
#597 := [rewrite]: #596
boehmes@41132
  1181
#593 := (iff #52 #592)
boehmes@41132
  1182
#590 := (iff #51 #587)
boehmes@41132
  1183
#584 := (or #581 #444)
boehmes@41132
  1184
#588 := (iff #584 #587)
boehmes@41132
  1185
#589 := [rewrite]: #588
boehmes@41132
  1186
#585 := (iff #51 #584)
boehmes@41132
  1187
#586 := [monotonicity #583 #447]: #585
boehmes@41132
  1188
#591 := [trans #586 #589]: #590
boehmes@41132
  1189
#579 := (iff #48 #577)
boehmes@41132
  1190
#580 := [rewrite]: #579
boehmes@41132
  1191
#594 := [monotonicity #580 #591]: #593
boehmes@41132
  1192
#599 := [trans #594 #597]: #598
boehmes@41132
  1193
#576 := [asserted]: #52
boehmes@41132
  1194
#600 := [mp #576 #599]: #595
boehmes@41132
  1195
#2808 := [mp #600 #2807]: #2803
boehmes@41132
  1196
#3167 := [unit-resolution #2808 #3170]: #577
boehmes@41132
  1197
#1417 := (not #577)
boehmes@41132
  1198
#1503 := (or #1284 #1417)
boehmes@41132
  1199
#23 := (= f8 f1)
boehmes@41132
  1200
#215 := (not #23)
boehmes@41132
  1201
#236 := (not #48)
boehmes@41132
  1202
#248 := (or #236 #215)
boehmes@41132
  1203
#1506 := (iff #248 #1503)
boehmes@41132
  1204
#1499 := (or #1417 #1284)
boehmes@41132
  1205
#1504 := (iff #1499 #1503)
boehmes@41132
  1206
#1505 := [rewrite]: #1504
boehmes@41132
  1207
#1501 := (iff #248 #1499)
boehmes@41132
  1208
#1285 := (iff #215 #1284)
boehmes@41132
  1209
#473 := (iff #23 #472)
boehmes@41132
  1210
#474 := [rewrite]: #473
boehmes@41132
  1211
#1286 := [monotonicity #474]: #1285
boehmes@41132
  1212
#1419 := (iff #236 #1417)
boehmes@41132
  1213
#1420 := [monotonicity #580]: #1419
boehmes@41132
  1214
#1502 := [monotonicity #1420 #1286]: #1501
boehmes@41132
  1215
#1507 := [trans #1502 #1505]: #1506
boehmes@41132
  1216
#1498 := [asserted]: #248
boehmes@41132
  1217
#1510 := [mp #1498 #1507]: #1503
boehmes@41132
  1218
#3168 := [unit-resolution #1510 #3167]: #1284
boehmes@41132
  1219
#2784 := (or #468 #472)
boehmes@41132
  1220
decl f3 :: S1
boehmes@41132
  1221
#8 := f3
boehmes@41132
  1222
#437 := (= f1 f3)
boehmes@41132
  1223
#486 := (or #437 #468 #472)
boehmes@41132
  1224
#2787 := (iff #486 #2784)
boehmes@41132
  1225
#2781 := (or false #468 #472)
boehmes@41132
  1226
#2785 := (iff #2781 #2784)
boehmes@41132
  1227
#2786 := [rewrite]: #2785
boehmes@41132
  1228
#2782 := (iff #486 #2781)
boehmes@41132
  1229
#2772 := (iff #437 false)
boehmes@41132
  1230
#440 := (not #437)
boehmes@41132
  1231
#9 := (= f3 f1)
boehmes@41132
  1232
#10 := (not #9)
boehmes@41132
  1233
#441 := (iff #10 #440)
boehmes@41132
  1234
#438 := (iff #9 #437)
boehmes@41132
  1235
#439 := [rewrite]: #438
boehmes@41132
  1236
#442 := [monotonicity #439]: #441
boehmes@41132
  1237
#436 := [asserted]: #10
boehmes@41132
  1238
#445 := [mp #436 #442]: #440
boehmes@41132
  1239
#2774 := [iff-false #445]: #2772
boehmes@41132
  1240
#2783 := [monotonicity #2774]: #2782
boehmes@41132
  1241
#2788 := [trans #2783 #2786]: #2787
boehmes@41132
  1242
#24 := (or #23 #9)
boehmes@41132
  1243
#21 := (= f7 f1)
boehmes@41132
  1244
#25 := (or #21 #24)
boehmes@41132
  1245
#489 := (iff #25 #486)
boehmes@41132
  1246
#478 := (or #437 #472)
boehmes@41132
  1247
#483 := (or #468 #478)
boehmes@41132
  1248
#487 := (iff #483 #486)
boehmes@41132
  1249
#488 := [rewrite]: #487
boehmes@41132
  1250
#484 := (iff #25 #483)
boehmes@41132
  1251
#481 := (iff #24 #478)
boehmes@41132
  1252
#475 := (or #472 #437)
boehmes@41132
  1253
#479 := (iff #475 #478)
boehmes@41132
  1254
#480 := [rewrite]: #479
boehmes@41132
  1255
#476 := (iff #24 #475)
boehmes@41132
  1256
#477 := [monotonicity #474 #439]: #476
boehmes@41132
  1257
#482 := [trans #477 #480]: #481
boehmes@41132
  1258
#470 := (iff #21 #468)
boehmes@41132
  1259
#471 := [rewrite]: #470
boehmes@41132
  1260
#485 := [monotonicity #471 #482]: #484
boehmes@41132
  1261
#490 := [trans #485 #488]: #489
boehmes@41132
  1262
#467 := [asserted]: #25
boehmes@41132
  1263
#491 := [mp #467 #490]: #486
boehmes@41132
  1264
#2789 := [mp #491 #2788]: #2784
boehmes@41132
  1265
#3165 := [unit-resolution #2789 #3168]: #468
boehmes@41132
  1266
#1281 := (not #468)
boehmes@41132
  1267
#1326 := (or #1281 #1311)
boehmes@41132
  1268
#214 := (not #21)
boehmes@41132
  1269
#27 := (= f9 f1)
boehmes@41132
  1270
#219 := (not #27)
boehmes@41132
  1271
#222 := (or #219 #214)
boehmes@41132
  1272
#1329 := (iff #222 #1326)
boehmes@41132
  1273
#1322 := (or #1311 #1281)
boehmes@41132
  1274
#1327 := (iff #1322 #1326)
boehmes@41132
  1275
#1328 := [rewrite]: #1327
boehmes@41132
  1276
#1324 := (iff #222 #1322)
boehmes@41132
  1277
#1282 := (iff #214 #1281)
boehmes@41132
  1278
#1283 := [monotonicity #471]: #1282
boehmes@41132
  1279
#1313 := (iff #219 #1311)
boehmes@41132
  1280
#494 := (iff #27 #493)
boehmes@41132
  1281
#495 := [rewrite]: #494
boehmes@41132
  1282
#1314 := [monotonicity #495]: #1313
boehmes@41132
  1283
#1325 := [monotonicity #1314 #1283]: #1324
boehmes@41132
  1284
#1330 := [trans #1325 #1328]: #1329
boehmes@41132
  1285
#1321 := [asserted]: #222
boehmes@41132
  1286
#1333 := [mp #1321 #1330]: #1326
boehmes@41132
  1287
#3166 := [unit-resolution #1333 #3165]: #1311
boehmes@41132
  1288
decl f12 :: S1
boehmes@41132
  1289
#34 := f12
boehmes@41132
  1290
#520 := (= f1 f12)
boehmes@41132
  1291
#1346 := (not #520)
boehmes@41132
  1292
decl f30 :: S1
boehmes@41132
  1293
#93 := f30
boehmes@41132
  1294
#758 := (= f1 f30)
boehmes@41132
  1295
#1760 := (not #758)
boehmes@41132
  1296
#2109 := (or #1760 #2068)
boehmes@41132
  1297
#94 := (= f30 f1)
boehmes@41132
  1298
#283 := (not #94)
boehmes@41132
  1299
#329 := (or #324 #283)
boehmes@41132
  1300
#2112 := (iff #329 #2109)
boehmes@41132
  1301
#2105 := (or #2068 #1760)
boehmes@41132
  1302
#2110 := (iff #2105 #2109)
boehmes@41132
  1303
#2111 := [rewrite]: #2110
boehmes@41132
  1304
#2107 := (iff #329 #2105)
boehmes@41132
  1305
#1761 := (iff #283 #1760)
boehmes@41132
  1306
#759 := (iff #94 #758)
boehmes@41132
  1307
#760 := [rewrite]: #759
boehmes@41132
  1308
#1762 := [monotonicity #760]: #1761
boehmes@41132
  1309
#2108 := [monotonicity #2070 #1762]: #2107
boehmes@41132
  1310
#2113 := [trans #2108 #2111]: #2112
boehmes@41132
  1311
#2104 := [asserted]: #329
boehmes@41132
  1312
#2116 := [mp #2104 #2113]: #2109
boehmes@41132
  1313
#3163 := [unit-resolution #2116 #3171]: #1760
boehmes@41132
  1314
decl f27 :: S1
boehmes@41132
  1315
#85 := f27
boehmes@41132
  1316
#731 := (= f1 f27)
boehmes@41132
  1317
#1725 := (not #731)
boehmes@41132
  1318
#1732 := (or #1725 #1729)
boehmes@36900
  1319
#86 := (= f27 f1)
boehmes@36900
  1320
#277 := (not #86)
boehmes@36900
  1321
#279 := (or #277 #278)
boehmes@41132
  1322
#1733 := (iff #279 #1732)
boehmes@41132
  1323
#1727 := (iff #277 #1725)
boehmes@41132
  1324
#732 := (iff #86 #731)
boehmes@41132
  1325
#733 := [rewrite]: #732
boehmes@36900
  1326
#1728 := [monotonicity #733]: #1727
boehmes@41132
  1327
#1734 := [monotonicity #1728 #1731]: #1733
boehmes@41132
  1328
#1724 := [asserted]: #279
boehmes@41132
  1329
#1737 := [mp #1724 #1734]: #1732
boehmes@41132
  1330
#3164 := [unit-resolution #1737 #3169]: #1725
boehmes@41132
  1331
decl f19 :: S1
boehmes@41132
  1332
#55 := f19
boehmes@41132
  1333
#605 := (= f1 f19)
boehmes@41132
  1334
#1452 := (not #605)
boehmes@41132
  1335
#1483 := (or #1417 #1452)
boehmes@41132
  1336
#56 := (= f19 f1)
boehmes@41132
  1337
#242 := (not #56)
boehmes@41132
  1338
#246 := (or #242 #236)
boehmes@41132
  1339
#1486 := (iff #246 #1483)
boehmes@41132
  1340
#1479 := (or #1452 #1417)
boehmes@41132
  1341
#1484 := (iff #1479 #1483)
boehmes@41132
  1342
#1485 := [rewrite]: #1484
boehmes@41132
  1343
#1481 := (iff #246 #1479)
boehmes@41132
  1344
#1453 := (iff #242 #1452)
boehmes@41132
  1345
#606 := (iff #56 #605)
boehmes@41132
  1346
#607 := [rewrite]: #606
boehmes@41132
  1347
#1454 := [monotonicity #607]: #1453
boehmes@41132
  1348
#1482 := [monotonicity #1454 #1420]: #1481
boehmes@41132
  1349
#1487 := [trans #1482 #1485]: #1486
boehmes@41132
  1350
#1478 := [asserted]: #246
boehmes@41132
  1351
#1490 := [mp #1478 #1487]: #1483
boehmes@41132
  1352
#3161 := [unit-resolution #1490 #3167]: #1452
boehmes@41132
  1353
#775 := (or #605 #731 #755 #758)
boehmes@41132
  1354
#95 := (or #86 #56)
boehmes@41132
  1355
#96 := (or #94 #95)
boehmes@41132
  1356
#92 := (= f29 f1)
boehmes@41132
  1357
#97 := (or #92 #96)
boehmes@41132
  1358
#778 := (iff #97 #775)
boehmes@41132
  1359
#764 := (or #605 #731)
boehmes@41132
  1360
#769 := (or #758 #764)
boehmes@41132
  1361
#772 := (or #755 #769)
boehmes@41132
  1362
#776 := (iff #772 #775)
boehmes@41132
  1363
#777 := [rewrite]: #776
boehmes@41132
  1364
#773 := (iff #97 #772)
boehmes@41132
  1365
#770 := (iff #96 #769)
boehmes@41132
  1366
#767 := (iff #95 #764)
boehmes@41132
  1367
#761 := (or #731 #605)
boehmes@41132
  1368
#765 := (iff #761 #764)
boehmes@41132
  1369
#766 := [rewrite]: #765
boehmes@41132
  1370
#762 := (iff #95 #761)
boehmes@41132
  1371
#763 := [monotonicity #733 #607]: #762
boehmes@41132
  1372
#768 := [trans #763 #766]: #767
boehmes@41132
  1373
#771 := [monotonicity #760 #768]: #770
boehmes@41132
  1374
#756 := (iff #92 #755)
boehmes@41132
  1375
#757 := [rewrite]: #756
boehmes@41132
  1376
#774 := [monotonicity #757 #771]: #773
boehmes@41132
  1377
#779 := [trans #774 #777]: #778
boehmes@41132
  1378
#754 := [asserted]: #97
boehmes@41132
  1379
#780 := [mp #754 #779]: #775
boehmes@41132
  1380
#3162 := [unit-resolution #780 #3161 #3164 #3163]: #755
boehmes@41132
  1381
#1872 := (or #1513 #1756)
boehmes@41132
  1382
#63 := (= f21 f1)
boehmes@41132
  1383
#250 := (not #63)
boehmes@41132
  1384
#282 := (not #92)
boehmes@41132
  1385
#297 := (or #282 #250)
boehmes@41132
  1386
#1875 := (iff #297 #1872)
boehmes@41132
  1387
#1868 := (or #1756 #1513)
boehmes@41132
  1388
#1873 := (iff #1868 #1872)
boehmes@41132
  1389
#1874 := [rewrite]: #1873
boehmes@41132
  1390
#1870 := (iff #297 #1868)
boehmes@41132
  1391
#1514 := (iff #250 #1513)
boehmes@41132
  1392
#633 := (iff #63 #632)
boehmes@41132
  1393
#634 := [rewrite]: #633
boehmes@41132
  1394
#1515 := [monotonicity #634]: #1514
boehmes@41132
  1395
#1758 := (iff #282 #1756)
boehmes@41132
  1396
#1759 := [monotonicity #757]: #1758
boehmes@41132
  1397
#1871 := [monotonicity #1759 #1515]: #1870
boehmes@41132
  1398
#1876 := [trans #1871 #1874]: #1875
boehmes@41132
  1399
#1867 := [asserted]: #297
boehmes@41132
  1400
#1879 := [mp #1867 #1876]: #1872
boehmes@41132
  1401
#3159 := [unit-resolution #1879 #3162]: #1513
boehmes@41132
  1402
#1448 := (not #602)
boehmes@41132
  1403
#1463 := (or #1417 #1448)
boehmes@41132
  1404
#54 := (= f18 f1)
boehmes@41132
  1405
#241 := (not #54)
boehmes@41132
  1406
#244 := (or #241 #236)
boehmes@41132
  1407
#1466 := (iff #244 #1463)
boehmes@41132
  1408
#1459 := (or #1448 #1417)
boehmes@41132
  1409
#1464 := (iff #1459 #1463)
boehmes@41132
  1410
#1465 := [rewrite]: #1464
boehmes@41132
  1411
#1461 := (iff #244 #1459)
boehmes@41132
  1412
#1450 := (iff #241 #1448)
boehmes@41132
  1413
#603 := (iff #54 #602)
boehmes@41132
  1414
#604 := [rewrite]: #603
boehmes@41132
  1415
#1451 := [monotonicity #604]: #1450
boehmes@41132
  1416
#1462 := [monotonicity #1451 #1420]: #1461
boehmes@41132
  1417
#1467 := [trans #1462 #1465]: #1466
boehmes@41132
  1418
#1458 := [asserted]: #244
boehmes@41132
  1419
#1470 := [mp #1458 #1467]: #1463
boehmes@41132
  1420
#3160 := [unit-resolution #1470 #3167]: #1448
boehmes@41132
  1421
decl f10 :: S1
boehmes@41132
  1422
#28 := f10
boehmes@41132
  1423
#496 := (= f1 f10)
boehmes@41132
  1424
#1315 := (not #496)
boehmes@41132
  1425
#1336 := (or #1281 #1315)
boehmes@41132
  1426
#29 := (= f10 f1)
boehmes@41132
  1427
#220 := (not #29)
boehmes@41132
  1428
#223 := (or #220 #214)
boehmes@41132
  1429
#1339 := (iff #223 #1336)
boehmes@41132
  1430
#1332 := (or #1315 #1281)
boehmes@41132
  1431
#1337 := (iff #1332 #1336)
boehmes@41132
  1432
#1338 := [rewrite]: #1337
boehmes@41132
  1433
#1334 := (iff #223 #1332)
boehmes@41132
  1434
#1316 := (iff #220 #1315)
boehmes@41132
  1435
#497 := (iff #29 #496)
boehmes@41132
  1436
#498 := [rewrite]: #497
boehmes@41132
  1437
#1317 := [monotonicity #498]: #1316
boehmes@41132
  1438
#1335 := [monotonicity #1317 #1283]: #1334
boehmes@41132
  1439
#1340 := [trans #1335 #1338]: #1339
boehmes@41132
  1440
#1331 := [asserted]: #223
boehmes@41132
  1441
#1343 := [mp #1331 #1340]: #1336
boehmes@41132
  1442
#3157 := [unit-resolution #1343 #3165]: #1315
boehmes@41132
  1443
#649 := (or #496 #602 #629 #632)
boehmes@41132
  1444
#64 := (or #54 #29)
boehmes@41132
  1445
#65 := (or #63 #64)
boehmes@41132
  1446
#61 := (= f20 f1)
boehmes@41132
  1447
#66 := (or #61 #65)
boehmes@41132
  1448
#652 := (iff #66 #649)
boehmes@41132
  1449
#638 := (or #496 #602)
boehmes@41132
  1450
#643 := (or #632 #638)
boehmes@41132
  1451
#646 := (or #629 #643)
boehmes@41132
  1452
#650 := (iff #646 #649)
boehmes@41132
  1453
#651 := [rewrite]: #650
boehmes@41132
  1454
#647 := (iff #66 #646)
boehmes@41132
  1455
#644 := (iff #65 #643)
boehmes@41132
  1456
#641 := (iff #64 #638)
boehmes@41132
  1457
#635 := (or #602 #496)
boehmes@41132
  1458
#639 := (iff #635 #638)
boehmes@41132
  1459
#640 := [rewrite]: #639
boehmes@41132
  1460
#636 := (iff #64 #635)
boehmes@41132
  1461
#637 := [monotonicity #604 #498]: #636
boehmes@41132
  1462
#642 := [trans #637 #640]: #641
boehmes@41132
  1463
#645 := [monotonicity #634 #642]: #644
boehmes@41132
  1464
#630 := (iff #61 #629)
boehmes@41132
  1465
#631 := [rewrite]: #630
boehmes@41132
  1466
#648 := [monotonicity #631 #645]: #647
boehmes@41132
  1467
#653 := [trans #648 #651]: #652
boehmes@41132
  1468
#628 := [asserted]: #66
boehmes@41132
  1469
#654 := [mp #628 #653]: #649
boehmes@41132
  1470
#3158 := [unit-resolution #654 #3157 #3160 #3159]: #629
boehmes@41132
  1471
#1625 := (or #1346 #1509)
boehmes@36900
  1472
#35 := (= f12 f1)
boehmes@36900
  1473
#225 := (not #35)
boehmes@41132
  1474
#249 := (not #61)
boehmes@41132
  1475
#264 := (or #249 #225)
boehmes@41132
  1476
#1628 := (iff #264 #1625)
boehmes@41132
  1477
#1621 := (or #1509 #1346)
boehmes@41132
  1478
#1626 := (iff #1621 #1625)
boehmes@41132
  1479
#1627 := [rewrite]: #1626
boehmes@41132
  1480
#1623 := (iff #264 #1621)
boehmes@41132
  1481
#1347 := (iff #225 #1346)
boehmes@41132
  1482
#521 := (iff #35 #520)
boehmes@41132
  1483
#522 := [rewrite]: #521
boehmes@41132
  1484
#1348 := [monotonicity #522]: #1347
boehmes@41132
  1485
#1511 := (iff #249 #1509)
boehmes@41132
  1486
#1512 := [monotonicity #631]: #1511
boehmes@41132
  1487
#1624 := [monotonicity #1512 #1348]: #1623
boehmes@41132
  1488
#1629 := [trans #1624 #1627]: #1628
boehmes@41132
  1489
#1620 := [asserted]: #264
boehmes@41132
  1490
#1632 := [mp #1620 #1629]: #1625
boehmes@41132
  1491
#3155 := [unit-resolution #1632 #3158]: #1346
boehmes@41132
  1492
#534 := (or #493 #517 #520)
boehmes@36900
  1493
#36 := (or #35 #27)
boehmes@36900
  1494
#33 := (= f11 f1)
boehmes@36900
  1495
#37 := (or #33 #36)
boehmes@41132
  1496
#537 := (iff #37 #534)
boehmes@41132
  1497
#526 := (or #493 #520)
boehmes@41132
  1498
#531 := (or #517 #526)
boehmes@41132
  1499
#535 := (iff #531 #534)
boehmes@41132
  1500
#536 := [rewrite]: #535
boehmes@41132
  1501
#532 := (iff #37 #531)
boehmes@41132
  1502
#529 := (iff #36 #526)
boehmes@41132
  1503
#523 := (or #520 #493)
boehmes@41132
  1504
#527 := (iff #523 #526)
boehmes@41132
  1505
#528 := [rewrite]: #527
boehmes@41132
  1506
#524 := (iff #36 #523)
boehmes@41132
  1507
#525 := [monotonicity #522 #495]: #524
boehmes@41132
  1508
#530 := [trans #525 #528]: #529
boehmes@41132
  1509
#518 := (iff #33 #517)
boehmes@41132
  1510
#519 := [rewrite]: #518
boehmes@41132
  1511
#533 := [monotonicity #519 #530]: #532
boehmes@41132
  1512
#538 := [trans #533 #536]: #537
boehmes@41132
  1513
#516 := [asserted]: #37
boehmes@41132
  1514
#539 := [mp #516 #538]: #534
boehmes@41132
  1515
#3156 := [unit-resolution #539 #3155 #3166]: #517
boehmes@41132
  1516
#1342 := (not #517)
boehmes@41132
  1517
#1388 := (or #1342 #1373)
boehmes@41132
  1518
#224 := (not #33)
boehmes@41132
  1519
#39 := (= f13 f1)
boehmes@41132
  1520
#229 := (not #39)
boehmes@41132
  1521
#232 := (or #229 #224)
boehmes@41132
  1522
#1391 := (iff #232 #1388)
boehmes@41132
  1523
#1384 := (or #1373 #1342)
boehmes@41132
  1524
#1389 := (iff #1384 #1388)
boehmes@41132
  1525
#1390 := [rewrite]: #1389
boehmes@41132
  1526
#1386 := (iff #232 #1384)
boehmes@41132
  1527
#1344 := (iff #224 #1342)
boehmes@41132
  1528
#1345 := [monotonicity #519]: #1344
boehmes@41132
  1529
#1375 := (iff #229 #1373)
boehmes@41132
  1530
#542 := (iff #39 #541)
boehmes@41132
  1531
#543 := [rewrite]: #542
boehmes@41132
  1532
#1376 := [monotonicity #543]: #1375
boehmes@41132
  1533
#1387 := [monotonicity #1376 #1345]: #1386
boehmes@41132
  1534
#1392 := [trans #1387 #1390]: #1391
boehmes@41132
  1535
#1383 := [asserted]: #232
boehmes@41132
  1536
#1395 := [mp #1383 #1392]: #1388
boehmes@41132
  1537
#3153 := [unit-resolution #1395 #3156]: #1373
boehmes@41132
  1538
#571 := (or #541 #565)
boehmes@36900
  1539
#45 := (= f15 f1)
boehmes@41132
  1540
#46 := (or #45 #39)
boehmes@41132
  1541
#574 := (iff #46 #571)
boehmes@41132
  1542
#568 := (or #565 #541)
boehmes@41132
  1543
#572 := (iff #568 #571)
boehmes@41132
  1544
#573 := [rewrite]: #572
boehmes@41132
  1545
#569 := (iff #46 #568)
boehmes@41132
  1546
#566 := (iff #45 #565)
boehmes@41132
  1547
#567 := [rewrite]: #566
boehmes@41132
  1548
#570 := [monotonicity #567 #543]: #569
boehmes@41132
  1549
#575 := [trans #570 #573]: #574
boehmes@41132
  1550
#564 := [asserted]: #46
boehmes@41132
  1551
#578 := [mp #564 #575]: #571
boehmes@41132
  1552
#3154 := [unit-resolution #578 #3153]: #565
boehmes@41132
  1553
#1404 := (not #565)
boehmes@41132
  1554
#1709 := (or #1404 #1692)
boehmes@36900
  1555
#234 := (not #45)
boehmes@36900
  1556
#82 := (= f26 f1)
boehmes@36900
  1557
#273 := (not #82)
boehmes@36900
  1558
#275 := (or #273 #234)
boehmes@41132
  1559
#1712 := (iff #275 #1709)
boehmes@41132
  1560
#1705 := (or #1692 #1404)
boehmes@41132
  1561
#1710 := (iff #1705 #1709)
boehmes@41132
  1562
#1711 := [rewrite]: #1710
boehmes@41132
  1563
#1707 := (iff #275 #1705)
boehmes@41132
  1564
#1406 := (iff #234 #1404)
boehmes@41132
  1565
#1407 := [monotonicity #567]: #1406
boehmes@41132
  1566
#1694 := (iff #273 #1692)
boehmes@41132
  1567
#711 := (iff #82 #710)
boehmes@41132
  1568
#712 := [rewrite]: #711
boehmes@41132
  1569
#1695 := [monotonicity #712]: #1694
boehmes@41132
  1570
#1708 := [monotonicity #1695 #1407]: #1707
boehmes@41132
  1571
#1713 := [trans #1708 #1711]: #1712
boehmes@41132
  1572
#1704 := [asserted]: #275
boehmes@41132
  1573
#1716 := [mp #1704 #1713]: #1709
boehmes@41132
  1574
#3151 := [unit-resolution #1716 #3154]: #1692
boehmes@41132
  1575
#877 := (or #710 #836 #863)
boehmes@41132
  1576
#113 := (= f35 f1)
boehmes@41132
  1577
#121 := (or #113 #82)
boehmes@41132
  1578
#122 := (or #120 #121)
boehmes@41132
  1579
#880 := (iff #122 #877)
boehmes@41132
  1580
#869 := (or #710 #836)
boehmes@41132
  1581
#874 := (or #863 #869)
boehmes@41132
  1582
#878 := (iff #874 #877)
boehmes@41132
  1583
#879 := [rewrite]: #878
boehmes@41132
  1584
#875 := (iff #122 #874)
boehmes@41132
  1585
#872 := (iff #121 #869)
boehmes@41132
  1586
#866 := (or #836 #710)
boehmes@41132
  1587
#870 := (iff #866 #869)
boehmes@41132
  1588
#871 := [rewrite]: #870
boehmes@41132
  1589
#867 := (iff #121 #866)
boehmes@41132
  1590
#837 := (iff #113 #836)
boehmes@41132
  1591
#838 := [rewrite]: #837
boehmes@41132
  1592
#868 := [monotonicity #838 #712]: #867
boehmes@41132
  1593
#873 := [trans #868 #871]: #872
boehmes@41132
  1594
#876 := [monotonicity #865 #873]: #875
boehmes@41132
  1595
#881 := [trans #876 #879]: #880
boehmes@41132
  1596
#862 := [asserted]: #122
boehmes@41132
  1597
#882 := [mp #862 #881]: #877
boehmes@41132
  1598
#3152 := [unit-resolution #882 #3151 #3173]: #836
boehmes@41132
  1599
decl f14 :: S1
boehmes@41132
  1600
#40 := f14
boehmes@41132
  1601
#544 := (= f1 f14)
boehmes@41132
  1602
#1377 := (not #544)
boehmes@41132
  1603
#1398 := (or #1342 #1377)
boehmes@36900
  1604
#41 := (= f14 f1)
boehmes@36900
  1605
#230 := (not #41)
boehmes@41132
  1606
#233 := (or #230 #224)
boehmes@41132
  1607
#1401 := (iff #233 #1398)
boehmes@41132
  1608
#1394 := (or #1377 #1342)
boehmes@41132
  1609
#1399 := (iff #1394 #1398)
boehmes@41132
  1610
#1400 := [rewrite]: #1399
boehmes@41132
  1611
#1396 := (iff #233 #1394)
boehmes@41132
  1612
#1378 := (iff #230 #1377)
boehmes@41132
  1613
#545 := (iff #41 #544)
boehmes@41132
  1614
#546 := [rewrite]: #545
boehmes@41132
  1615
#1379 := [monotonicity #546]: #1378
boehmes@41132
  1616
#1397 := [monotonicity #1379 #1345]: #1396
boehmes@41132
  1617
#1402 := [trans #1397 #1400]: #1401
boehmes@41132
  1618
#1393 := [asserted]: #233
boehmes@41132
  1619
#1405 := [mp #1393 #1402]: #1398
boehmes@41132
  1620
#3149 := [unit-resolution #1405 #3156]: #1377
boehmes@41132
  1621
decl f22 :: S1
boehmes@41132
  1622
#67 := f22
boehmes@41132
  1623
#656 := (= f1 f22)
boehmes@41132
  1624
#1570 := (not #656)
boehmes@41132
  1625
#1585 := (or #1509 #1570)
boehmes@41132
  1626
#68 := (= f22 f1)
boehmes@41132
  1627
#257 := (not #68)
boehmes@41132
  1628
#260 := (or #257 #249)
boehmes@41132
  1629
#1588 := (iff #260 #1585)
boehmes@41132
  1630
#1581 := (or #1570 #1509)
boehmes@41132
  1631
#1586 := (iff #1581 #1585)
boehmes@41132
  1632
#1587 := [rewrite]: #1586
boehmes@41132
  1633
#1583 := (iff #260 #1581)
boehmes@41132
  1634
#1572 := (iff #257 #1570)
boehmes@41132
  1635
#657 := (iff #68 #656)
boehmes@41132
  1636
#658 := [rewrite]: #657
boehmes@41132
  1637
#1573 := [monotonicity #658]: #1572
boehmes@41132
  1638
#1584 := [monotonicity #1573 #1512]: #1583
boehmes@41132
  1639
#1589 := [trans #1584 #1587]: #1588
boehmes@41132
  1640
#1580 := [asserted]: #260
boehmes@41132
  1641
#1592 := [mp #1580 #1589]: #1585
boehmes@41132
  1642
#3150 := [unit-resolution #1592 #3158]: #1570
boehmes@41132
  1643
decl f24 :: S1
boehmes@41132
  1644
#74 := f24
boehmes@41132
  1645
#683 := (= f1 f24)
boehmes@41132
  1646
#1631 := (not #683)
boehmes@41132
  1647
#1719 := (or #1404 #1631)
boehmes@36900
  1648
#75 := (= f24 f1)
boehmes@36900
  1649
#265 := (not #75)
boehmes@41132
  1650
#276 := (or #265 #234)
boehmes@41132
  1651
#1722 := (iff #276 #1719)
boehmes@41132
  1652
#1715 := (or #1631 #1404)
boehmes@41132
  1653
#1720 := (iff #1715 #1719)
boehmes@41132
  1654
#1721 := [rewrite]: #1720
boehmes@41132
  1655
#1717 := (iff #276 #1715)
boehmes@41132
  1656
#1633 := (iff #265 #1631)
boehmes@41132
  1657
#684 := (iff #75 #683)
boehmes@41132
  1658
#685 := [rewrite]: #684
boehmes@41132
  1659
#1634 := [monotonicity #685]: #1633
boehmes@41132
  1660
#1718 := [monotonicity #1634 #1407]: #1717
boehmes@41132
  1661
#1723 := [trans #1718 #1721]: #1722
boehmes@41132
  1662
#1714 := [asserted]: #276
boehmes@41132
  1663
#1726 := [mp #1714 #1723]: #1719
boehmes@41132
  1664
#3147 := [unit-resolution #1726 #3154]: #1631
boehmes@41132
  1665
#703 := (or #544 #656 #683 #686)
boehmes@36900
  1666
#78 := (or #68 #41)
boehmes@36900
  1667
#77 := (= f25 f1)
boehmes@36900
  1668
#79 := (or #77 #78)
boehmes@36900
  1669
#80 := (or #75 #79)
boehmes@41132
  1670
#706 := (iff #80 #703)
boehmes@41132
  1671
#692 := (or #544 #656)
boehmes@41132
  1672
#697 := (or #686 #692)
boehmes@41132
  1673
#700 := (or #683 #697)
boehmes@41132
  1674
#704 := (iff #700 #703)
boehmes@41132
  1675
#705 := [rewrite]: #704
boehmes@41132
  1676
#701 := (iff #80 #700)
boehmes@41132
  1677
#698 := (iff #79 #697)
boehmes@41132
  1678
#695 := (iff #78 #692)
boehmes@41132
  1679
#689 := (or #656 #544)
boehmes@41132
  1680
#693 := (iff #689 #692)
boehmes@41132
  1681
#694 := [rewrite]: #693
boehmes@41132
  1682
#690 := (iff #78 #689)
boehmes@41132
  1683
#691 := [monotonicity #658 #546]: #690
boehmes@41132
  1684
#696 := [trans #691 #694]: #695
boehmes@41132
  1685
#687 := (iff #77 #686)
boehmes@41132
  1686
#688 := [rewrite]: #687
boehmes@41132
  1687
#699 := [monotonicity #688 #696]: #698
boehmes@41132
  1688
#702 := [monotonicity #685 #699]: #701
boehmes@41132
  1689
#707 := [trans #702 #705]: #706
boehmes@41132
  1690
#682 := [asserted]: #80
boehmes@41132
  1691
#708 := [mp #682 #707]: #703
boehmes@41132
  1692
#3148 := [unit-resolution #708 #3147 #3150 #3149]: #686
boehmes@41132
  1693
#1635 := (not #686)
boehmes@41132
  1694
#1964 := (or #1635 #1939)
boehmes@36900
  1695
#266 := (not #77)
boehmes@41132
  1696
#306 := (not #113)
boehmes@41132
  1697
#310 := (or #306 #266)
boehmes@41132
  1698
#1967 := (iff #310 #1964)
boehmes@41132
  1699
#1960 := (or #1939 #1635)
boehmes@41132
  1700
#1965 := (iff #1960 #1964)
boehmes@41132
  1701
#1966 := [rewrite]: #1965
boehmes@41132
  1702
#1962 := (iff #310 #1960)
boehmes@41132
  1703
#1636 := (iff #266 #1635)
boehmes@41132
  1704
#1637 := [monotonicity #688]: #1636
boehmes@41132
  1705
#1941 := (iff #306 #1939)
boehmes@41132
  1706
#1942 := [monotonicity #838]: #1941
boehmes@41132
  1707
#1963 := [monotonicity #1942 #1637]: #1962
boehmes@41132
  1708
#1968 := [trans #1963 #1966]: #1967
boehmes@41132
  1709
#1959 := [asserted]: #310
boehmes@41132
  1710
#1971 := [mp #1959 #1968]: #1964
boehmes@41132
  1711
#3145 := [unit-resolution #1971 #3148 #3152]: false
boehmes@41132
  1712
#3143 := [lemma #3145]: #3146
boehmes@41132
  1713
#3038 := [unit-resolution #3143 #3039 #3173]: #2068
boehmes@41132
  1714
#1081 := (or #911 #1037 #1061 #1064)
boehmes@41132
  1715
#171 := (or #162 #132)
boehmes@41132
  1716
#172 := (or #170 #171)
boehmes@41132
  1717
#168 := (= f51 f1)
boehmes@41132
  1718
#173 := (or #168 #172)
boehmes@41132
  1719
#1084 := (iff #173 #1081)
boehmes@41132
  1720
#1070 := (or #911 #1037)
boehmes@41132
  1721
#1075 := (or #1064 #1070)
boehmes@41132
  1722
#1078 := (or #1061 #1075)
boehmes@41132
  1723
#1082 := (iff #1078 #1081)
boehmes@41132
  1724
#1083 := [rewrite]: #1082
boehmes@41132
  1725
#1079 := (iff #173 #1078)
boehmes@41132
  1726
#1076 := (iff #172 #1075)
boehmes@41132
  1727
#1073 := (iff #171 #1070)
boehmes@41132
  1728
#1067 := (or #1037 #911)
boehmes@41132
  1729
#1071 := (iff #1067 #1070)
boehmes@41132
  1730
#1072 := [rewrite]: #1071
boehmes@41132
  1731
#1068 := (iff #171 #1067)
boehmes@41132
  1732
#1069 := [monotonicity #1039 #913]: #1068
boehmes@41132
  1733
#1074 := [trans #1069 #1072]: #1073
boehmes@41132
  1734
#1077 := [monotonicity #1066 #1074]: #1076
boehmes@41132
  1735
#1062 := (iff #168 #1061)
boehmes@41132
  1736
#1063 := [rewrite]: #1062
boehmes@41132
  1737
#1080 := [monotonicity #1063 #1077]: #1079
boehmes@41132
  1738
#1085 := [trans #1080 #1083]: #1084
boehmes@41132
  1739
#1060 := [asserted]: #173
boehmes@41132
  1740
#1086 := [mp #1060 #1085]: #1081
boehmes@41132
  1741
#3035 := [unit-resolution #1086 #3038 #3037 #3040]: #1061
boehmes@41132
  1742
#2488 := (or #2129 #2372)
boehmes@41132
  1743
#139 := (= f43 f1)
boehmes@41132
  1744
#332 := (not #139)
boehmes@41132
  1745
#364 := (not #168)
boehmes@41132
  1746
#379 := (or #364 #332)
boehmes@41132
  1747
#2491 := (iff #379 #2488)
boehmes@41132
  1748
#2484 := (or #2372 #2129)
boehmes@41132
  1749
#2489 := (iff #2484 #2488)
boehmes@41132
  1750
#2490 := [rewrite]: #2489
boehmes@41132
  1751
#2486 := (iff #379 #2484)
boehmes@41132
  1752
#2130 := (iff #332 #2129)
boehmes@41132
  1753
#939 := (iff #139 #938)
boehmes@41132
  1754
#940 := [rewrite]: #939
boehmes@41132
  1755
#2131 := [monotonicity #940]: #2130
boehmes@41132
  1756
#2374 := (iff #364 #2372)
boehmes@41132
  1757
#2375 := [monotonicity #1063]: #2374
boehmes@41132
  1758
#2487 := [monotonicity #2375 #2131]: #2486
boehmes@41132
  1759
#2492 := [trans #2487 #2490]: #2491
boehmes@41132
  1760
#2483 := [asserted]: #379
boehmes@41132
  1761
#2495 := [mp #2483 #2492]: #2488
boehmes@41132
  1762
#3036 := [unit-resolution #2495 #3035]: #2129
boehmes@41132
  1763
#3046 := (or #1939 #938 #887 #989 #992)
boehmes@41132
  1764
#3069 := [hypothesis]: #836
boehmes@41132
  1765
#1946 := (or #1939 #1943)
boehmes@36900
  1766
#115 := (= f36 f1)
boehmes@36900
  1767
#307 := (not #115)
boehmes@41132
  1768
#308 := (or #306 #307)
boehmes@41132
  1769
#1947 := (iff #308 #1946)
boehmes@41132
  1770
#1944 := (iff #307 #1943)
boehmes@41132
  1771
#840 := (iff #115 #839)
boehmes@41132
  1772
#841 := [rewrite]: #840
boehmes@41132
  1773
#1945 := [monotonicity #841]: #1944
boehmes@41132
  1774
#1948 := [monotonicity #1942 #1945]: #1947
boehmes@41132
  1775
#1938 := [asserted]: #308
boehmes@41132
  1776
#1951 := [mp #1938 #1948]: #1946
boehmes@41132
  1777
#3070 := [unit-resolution #1951 #3069]: #1943
boehmes@41132
  1778
#1009 := (or #839 #962 #989 #992)
boehmes@36900
  1779
#144 := (= f44 f1)
boehmes@36900
  1780
#154 := (or #144 #115)
boehmes@36900
  1781
#155 := (or #153 #154)
boehmes@36900
  1782
#156 := (or #151 #155)
boehmes@41132
  1783
#1012 := (iff #156 #1009)
boehmes@41132
  1784
#998 := (or #839 #962)
boehmes@41132
  1785
#1003 := (or #992 #998)
boehmes@41132
  1786
#1006 := (or #989 #1003)
boehmes@41132
  1787
#1010 := (iff #1006 #1009)
boehmes@41132
  1788
#1011 := [rewrite]: #1010
boehmes@41132
  1789
#1007 := (iff #156 #1006)
boehmes@41132
  1790
#1004 := (iff #155 #1003)
boehmes@41132
  1791
#1001 := (iff #154 #998)
boehmes@41132
  1792
#995 := (or #962 #839)
boehmes@41132
  1793
#999 := (iff #995 #998)
boehmes@41132
  1794
#1000 := [rewrite]: #999
boehmes@41132
  1795
#996 := (iff #154 #995)
boehmes@41132
  1796
#963 := (iff #144 #962)
boehmes@41132
  1797
#964 := [rewrite]: #963
boehmes@41132
  1798
#997 := [monotonicity #964 #841]: #996
boehmes@41132
  1799
#1002 := [trans #997 #1000]: #1001
boehmes@41132
  1800
#1005 := [monotonicity #994 #1002]: #1004
boehmes@41132
  1801
#1008 := [monotonicity #991 #1005]: #1007
boehmes@41132
  1802
#1013 := [trans #1008 #1011]: #1012
boehmes@41132
  1803
#988 := [asserted]: #156
boehmes@41132
  1804
#1014 := [mp #988 #1013]: #1009
boehmes@41132
  1805
#3067 := [unit-resolution #1014 #3070 #3072 #3071]: #962
boehmes@41132
  1806
#2211 := (or #1882 #2186)
boehmes@36900
  1807
#108 := (= f34 f1)
boehmes@36900
  1808
#299 := (not #108)
boehmes@36900
  1809
#339 := (not #144)
boehmes@36900
  1810
#343 := (or #339 #299)
boehmes@41132
  1811
#2214 := (iff #343 #2211)
boehmes@41132
  1812
#2207 := (or #2186 #1882)
boehmes@41132
  1813
#2212 := (iff #2207 #2211)
boehmes@41132
  1814
#2213 := [rewrite]: #2212
boehmes@41132
  1815
#2209 := (iff #343 #2207)
boehmes@41132
  1816
#1883 := (iff #299 #1882)
boehmes@41132
  1817
#813 := (iff #108 #812)
boehmes@41132
  1818
#814 := [rewrite]: #813
boehmes@41132
  1819
#1884 := [monotonicity #814]: #1883
boehmes@41132
  1820
#2188 := (iff #339 #2186)
boehmes@41132
  1821
#2189 := [monotonicity #964]: #2188
boehmes@41132
  1822
#2210 := [monotonicity #2189 #1884]: #2209
boehmes@41132
  1823
#2215 := [trans #2210 #2213]: #2214
boehmes@41132
  1824
#2206 := [asserted]: #343
boehmes@41132
  1825
#2218 := [mp #2206 #2215]: #2211
boehmes@41132
  1826
#3068 := [unit-resolution #2218 #3067]: #1882
boehmes@41132
  1827
#1954 := (or #1878 #1939)
boehmes@41132
  1828
#106 := (= f33 f1)
boehmes@41132
  1829
#298 := (not #106)
boehmes@36900
  1830
#309 := (or #306 #298)
boehmes@41132
  1831
#1957 := (iff #309 #1954)
boehmes@41132
  1832
#1950 := (or #1939 #1878)
boehmes@41132
  1833
#1955 := (iff #1950 #1954)
boehmes@41132
  1834
#1956 := [rewrite]: #1955
boehmes@41132
  1835
#1952 := (iff #309 #1950)
boehmes@41132
  1836
#1880 := (iff #298 #1878)
boehmes@41132
  1837
#810 := (iff #106 #809)
boehmes@41132
  1838
#811 := [rewrite]: #810
boehmes@41132
  1839
#1881 := [monotonicity #811]: #1880
boehmes@41132
  1840
#1953 := [monotonicity #1942 #1881]: #1952
boehmes@41132
  1841
#1958 := [trans #1953 #1956]: #1957
boehmes@41132
  1842
#1949 := [asserted]: #309
boehmes@41132
  1843
#1961 := [mp #1949 #1958]: #1954
boehmes@41132
  1844
#3065 := [unit-resolution #1961 #3069]: #1878
boehmes@41132
  1845
#2201 := (or #2125 #2186)
boehmes@36900
  1846
#137 := (= f42 f1)
boehmes@36900
  1847
#331 := (not #137)
boehmes@36900
  1848
#342 := (or #339 #331)
boehmes@41132
  1849
#2204 := (iff #342 #2201)
boehmes@41132
  1850
#2197 := (or #2186 #2125)
boehmes@41132
  1851
#2202 := (iff #2197 #2201)
boehmes@41132
  1852
#2203 := [rewrite]: #2202
boehmes@41132
  1853
#2199 := (iff #342 #2197)
boehmes@41132
  1854
#2127 := (iff #331 #2125)
boehmes@41132
  1855
#936 := (iff #137 #935)
boehmes@41132
  1856
#937 := [rewrite]: #936
boehmes@41132
  1857
#2128 := [monotonicity #937]: #2127
boehmes@41132
  1858
#2200 := [monotonicity #2189 #2128]: #2199
boehmes@41132
  1859
#2205 := [trans #2200 #2203]: #2204
boehmes@41132
  1860
#2196 := [asserted]: #342
boehmes@41132
  1861
#2208 := [mp #2196 #2205]: #2201
boehmes@41132
  1862
#3066 := [unit-resolution #2208 #3067]: #2125
boehmes@41132
  1863
#3116 := [hypothesis]: #2129
boehmes@41132
  1864
#3083 := (or #1729 #938 #935 #809 #812)
boehmes@41132
  1865
#3103 := [hypothesis]: #734
boehmes@41132
  1866
#3104 := [unit-resolution #1757 #3103]: #1421
boehmes@41132
  1867
#3101 := [unit-resolution #2808 #3104]: #577
boehmes@41132
  1868
#3102 := [unit-resolution #1510 #3101]: #1284
boehmes@41132
  1869
#3099 := [unit-resolution #2789 #3102]: #468
boehmes@41132
  1870
#3100 := [unit-resolution #1343 #3099]: #1315
boehmes@41132
  1871
#3097 := [unit-resolution #1470 #3101]: #1448
boehmes@41132
  1872
#3098 := [hypothesis]: #1882
boehmes@41132
  1873
#3095 := [hypothesis]: #1878
boehmes@41132
  1874
#3096 := [unit-resolution #1490 #3101]: #1452
boehmes@41132
  1875
#3093 := [unit-resolution #1737 #3103]: #1725
boehmes@41132
  1876
#3105 := (or #1817 #731 #605 #938 #935)
boehmes@41132
  1877
#3113 := [hypothesis]: #782
boehmes@41132
  1878
#1824 := (or #1817 #1821)
boehmes@41132
  1879
#101 := (= f32 f1)
boehmes@41132
  1880
#291 := (not #101)
boehmes@41132
  1881
#99 := (= f31 f1)
boehmes@41132
  1882
#290 := (not #99)
boehmes@41132
  1883
#292 := (or #290 #291)
boehmes@41132
  1884
#1825 := (iff #292 #1824)
boehmes@41132
  1885
#1822 := (iff #291 #1821)
boehmes@41132
  1886
#786 := (iff #101 #785)
boehmes@41132
  1887
#787 := [rewrite]: #786
boehmes@41132
  1888
#1823 := [monotonicity #787]: #1822
boehmes@41132
  1889
#1819 := (iff #290 #1817)
boehmes@41132
  1890
#783 := (iff #99 #782)
boehmes@41132
  1891
#784 := [rewrite]: #783
boehmes@41132
  1892
#1820 := [monotonicity #784]: #1819
boehmes@41132
  1893
#1826 := [monotonicity #1820 #1823]: #1825
boehmes@41132
  1894
#1816 := [asserted]: #292
boehmes@41132
  1895
#1829 := [mp #1816 #1826]: #1824
boehmes@41132
  1896
#3114 := [unit-resolution #1829 #3113]: #1821
boehmes@41132
  1897
#955 := (or #785 #908 #935 #938)
boehmes@36900
  1898
#130 := (= f40 f1)
boehmes@36900
  1899
#140 := (or #130 #101)
boehmes@36900
  1900
#141 := (or #139 #140)
boehmes@36900
  1901
#142 := (or #137 #141)
boehmes@41132
  1902
#958 := (iff #142 #955)
boehmes@41132
  1903
#944 := (or #785 #908)
boehmes@41132
  1904
#949 := (or #938 #944)
boehmes@41132
  1905
#952 := (or #935 #949)
boehmes@41132
  1906
#956 := (iff #952 #955)
boehmes@41132
  1907
#957 := [rewrite]: #956
boehmes@41132
  1908
#953 := (iff #142 #952)
boehmes@41132
  1909
#950 := (iff #141 #949)
boehmes@41132
  1910
#947 := (iff #140 #944)
boehmes@41132
  1911
#941 := (or #908 #785)
boehmes@41132
  1912
#945 := (iff #941 #944)
boehmes@41132
  1913
#946 := [rewrite]: #945
boehmes@41132
  1914
#942 := (iff #140 #941)
boehmes@41132
  1915
#909 := (iff #130 #908)
boehmes@41132
  1916
#910 := [rewrite]: #909
boehmes@41132
  1917
#943 := [monotonicity #910 #787]: #942
boehmes@41132
  1918
#948 := [trans #943 #946]: #947
boehmes@41132
  1919
#951 := [monotonicity #940 #948]: #950
boehmes@41132
  1920
#954 := [monotonicity #937 #951]: #953
boehmes@41132
  1921
#959 := [trans #954 #957]: #958
boehmes@41132
  1922
#934 := [asserted]: #142
boehmes@41132
  1923
#960 := [mp #934 #959]: #955
boehmes@41132
  1924
#3111 := [unit-resolution #960 #3114 #3116 #3115]: #908
boehmes@41132
  1925
#3112 := [hypothesis]: #1452
boehmes@41132
  1926
#3109 := [hypothesis]: #1725
boehmes@41132
  1927
#1832 := (or #1756 #1817)
boehmes@36900
  1928
#293 := (or #290 #282)
boehmes@41132
  1929
#1835 := (iff #293 #1832)
boehmes@41132
  1930
#1828 := (or #1817 #1756)
boehmes@41132
  1931
#1833 := (iff #1828 #1832)
boehmes@41132
  1932
#1834 := [rewrite]: #1833
boehmes@41132
  1933
#1830 := (iff #293 #1828)
boehmes@41132
  1934
#1831 := [monotonicity #1820 #1759]: #1830
boehmes@41132
  1935
#1836 := [trans #1831 #1834]: #1835
boehmes@41132
  1936
#1827 := [asserted]: #293
boehmes@41132
  1937
#1839 := [mp #1827 #1836]: #1832
boehmes@41132
  1938
#3110 := [unit-resolution #1839 #3113]: #1756
boehmes@41132
  1939
#3107 := [unit-resolution #780 #3110 #3109 #3112]: #758
boehmes@41132
  1940
#2089 := (or #1760 #2064)
boehmes@41132
  1941
#323 := (not #130)
boehmes@41132
  1942
#327 := (or #323 #283)
boehmes@41132
  1943
#2092 := (iff #327 #2089)
boehmes@41132
  1944
#2085 := (or #2064 #1760)
boehmes@41132
  1945
#2090 := (iff #2085 #2089)
boehmes@41132
  1946
#2091 := [rewrite]: #2090
boehmes@41132
  1947
#2087 := (iff #327 #2085)
boehmes@41132
  1948
#2066 := (iff #323 #2064)
boehmes@41132
  1949
#2067 := [monotonicity #910]: #2066
boehmes@41132
  1950
#2088 := [monotonicity #2067 #1762]: #2087
boehmes@41132
  1951
#2093 := [trans #2088 #2091]: #2092
boehmes@41132
  1952
#2084 := [asserted]: #327
boehmes@41132
  1953
#2096 := [mp #2084 #2093]: #2089
boehmes@41132
  1954
#3108 := [unit-resolution #2096 #3107 #3111]: false
boehmes@41132
  1955
#3106 := [lemma #3108]: #3105
boehmes@41132
  1956
#3094 := [unit-resolution #3106 #3093 #3096 #3116 #3115]: #1817
boehmes@41132
  1957
#829 := (or #659 #782 #809 #812)
boehmes@41132
  1958
#70 := (= f23 f1)
boehmes@41132
  1959
#109 := (or #99 #70)
boehmes@41132
  1960
#110 := (or #108 #109)
boehmes@41132
  1961
#111 := (or #106 #110)
boehmes@41132
  1962
#832 := (iff #111 #829)
boehmes@41132
  1963
#818 := (or #659 #782)
boehmes@41132
  1964
#823 := (or #812 #818)
boehmes@41132
  1965
#826 := (or #809 #823)
boehmes@41132
  1966
#830 := (iff #826 #829)
boehmes@41132
  1967
#831 := [rewrite]: #830
boehmes@41132
  1968
#827 := (iff #111 #826)
boehmes@41132
  1969
#824 := (iff #110 #823)
boehmes@41132
  1970
#821 := (iff #109 #818)
boehmes@41132
  1971
#815 := (or #782 #659)
boehmes@41132
  1972
#819 := (iff #815 #818)
boehmes@41132
  1973
#820 := [rewrite]: #819
boehmes@41132
  1974
#816 := (iff #109 #815)
boehmes@41132
  1975
#660 := (iff #70 #659)
boehmes@41132
  1976
#661 := [rewrite]: #660
boehmes@41132
  1977
#817 := [monotonicity #784 #661]: #816
boehmes@41132
  1978
#822 := [trans #817 #820]: #821
boehmes@41132
  1979
#825 := [monotonicity #814 #822]: #824
boehmes@41132
  1980
#828 := [monotonicity #811 #825]: #827
boehmes@41132
  1981
#833 := [trans #828 #831]: #832
boehmes@41132
  1982
#808 := [asserted]: #111
boehmes@41132
  1983
#834 := [mp #808 #833]: #829
boehmes@41132
  1984
#3091 := [unit-resolution #834 #3094 #3095 #3098]: #659
boehmes@41132
  1985
#1574 := (not #659)
boehmes@41132
  1986
#1605 := (or #1509 #1574)
boehmes@41132
  1987
#258 := (not #70)
boehmes@41132
  1988
#262 := (or #258 #249)
boehmes@41132
  1989
#1608 := (iff #262 #1605)
boehmes@41132
  1990
#1601 := (or #1574 #1509)
boehmes@41132
  1991
#1606 := (iff #1601 #1605)
boehmes@41132
  1992
#1607 := [rewrite]: #1606
boehmes@41132
  1993
#1603 := (iff #262 #1601)
boehmes@41132
  1994
#1575 := (iff #258 #1574)
boehmes@41132
  1995
#1576 := [monotonicity #661]: #1575
boehmes@41132
  1996
#1604 := [monotonicity #1576 #1512]: #1603
boehmes@41132
  1997
#1609 := [trans #1604 #1607]: #1608
boehmes@41132
  1998
#1600 := [asserted]: #262
boehmes@41132
  1999
#1612 := [mp #1600 #1609]: #1605
boehmes@41132
  2000
#3092 := [unit-resolution #1612 #3091]: #1509
boehmes@41132
  2001
#3089 := [unit-resolution #654 #3092 #3097 #3100]: #632
boehmes@41132
  2002
#1862 := (or #1513 #1821)
boehmes@41132
  2003
#296 := (or #291 #250)
boehmes@41132
  2004
#1865 := (iff #296 #1862)
boehmes@41132
  2005
#1858 := (or #1821 #1513)
boehmes@41132
  2006
#1863 := (iff #1858 #1862)
boehmes@41132
  2007
#1864 := [rewrite]: #1863
boehmes@41132
  2008
#1860 := (iff #296 #1858)
boehmes@41132
  2009
#1861 := [monotonicity #1823 #1515]: #1860
boehmes@41132
  2010
#1866 := [trans #1861 #1864]: #1865
boehmes@41132
  2011
#1857 := [asserted]: #296
boehmes@41132
  2012
#1869 := [mp #1857 #1866]: #1862
boehmes@41132
  2013
#3090 := [unit-resolution #1869 #3089]: #1821
boehmes@41132
  2014
#3087 := [unit-resolution #960 #3090 #3116 #3115]: #908
boehmes@41132
  2015
#3088 := [unit-resolution #1879 #3089]: #1756
boehmes@41132
  2016
#3085 := [unit-resolution #780 #3088 #3093 #3096]: #758
boehmes@41132
  2017
#3086 := [unit-resolution #2096 #3085 #3087]: false
boehmes@41132
  2018
#3084 := [lemma #3086]: #3083
boehmes@41132
  2019
#3063 := [unit-resolution #3084 #3066 #3116 #3065 #3068]: #1729
boehmes@41132
  2020
#3064 := [unit-resolution #906 #3063 #3174]: #884
boehmes@41132
  2021
#2079 := (or #2033 #2064)
boehmes@41132
  2022
#326 := (or #323 #318)
boehmes@41132
  2023
#2082 := (iff #326 #2079)
boehmes@41132
  2024
#2075 := (or #2064 #2033)
boehmes@41132
  2025
#2080 := (iff #2075 #2079)
boehmes@41132
  2026
#2081 := [rewrite]: #2080
boehmes@41132
  2027
#2077 := (iff #326 #2075)
boehmes@41132
  2028
#2078 := [monotonicity #2067 #2036]: #2077
boehmes@41132
  2029
#2083 := [trans #2078 #2081]: #2082
boehmes@41132
  2030
#2074 := [asserted]: #326
boehmes@41132
  2031
#2086 := [mp #2074 #2083]: #2079
boehmes@41132
  2032
#3061 := [unit-resolution #2086 #3064]: #2064
boehmes@41132
  2033
#3062 := [unit-resolution #960 #3061 #3116 #3066]: #785
boehmes@41132
  2034
#3059 := [unit-resolution #1829 #3062]: #1817
boehmes@41132
  2035
#3060 := [unit-resolution #834 #3059 #3065 #3068]: #659
boehmes@41132
  2036
#3057 := [unit-resolution #1612 #3060]: #1509
boehmes@41132
  2037
#3058 := [unit-resolution #1869 #3062]: #1513
boehmes@41132
  2038
#1852 := (or #1756 #1821)
boehmes@41132
  2039
#295 := (or #291 #282)
boehmes@41132
  2040
#1855 := (iff #295 #1852)
boehmes@41132
  2041
#1848 := (or #1821 #1756)
boehmes@41132
  2042
#1853 := (iff #1848 #1852)
boehmes@41132
  2043
#1854 := [rewrite]: #1853
boehmes@41132
  2044
#1850 := (iff #295 #1848)
boehmes@41132
  2045
#1851 := [monotonicity #1823 #1759]: #1850
boehmes@41132
  2046
#1856 := [trans #1851 #1854]: #1855
boehmes@41132
  2047
#1847 := [asserted]: #295
boehmes@41132
  2048
#1859 := [mp #1847 #1856]: #1852
boehmes@41132
  2049
#3055 := [unit-resolution #1859 #3062]: #1756
boehmes@41132
  2050
#2119 := (or #1760 #2033)
boehmes@41132
  2051
#330 := (or #318 #283)
boehmes@41132
  2052
#2122 := (iff #330 #2119)
boehmes@41132
  2053
#2115 := (or #2033 #1760)
boehmes@41132
  2054
#2120 := (iff #2115 #2119)
boehmes@41132
  2055
#2121 := [rewrite]: #2120
boehmes@41132
  2056
#2117 := (iff #330 #2115)
boehmes@41132
  2057
#2118 := [monotonicity #2036 #1762]: #2117
boehmes@41132
  2058
#2123 := [trans #2118 #2121]: #2122
boehmes@41132
  2059
#2114 := [asserted]: #330
boehmes@41132
  2060
#2126 := [mp #2114 #2123]: #2119
boehmes@41132
  2061
#3056 := [unit-resolution #2126 #3064]: #1760
boehmes@41132
  2062
#3073 := (or #1417 #632 #629)
boehmes@41132
  2063
#3081 := [hypothesis]: #1509
boehmes@41132
  2064
#3082 := [hypothesis]: #1513
boehmes@41132
  2065
#3079 := [hypothesis]: #577
boehmes@41132
  2066
#3080 := [unit-resolution #1470 #3079]: #1448
boehmes@41132
  2067
#3077 := [unit-resolution #654 #3080 #3082 #3081]: #496
boehmes@41132
  2068
#3078 := [unit-resolution #1510 #3079]: #1284
boehmes@41132
  2069
#3075 := [unit-resolution #2789 #3078]: #468
boehmes@41132
  2070
#3076 := [unit-resolution #1343 #3075 #3077]: false
boehmes@41132
  2071
#3074 := [lemma #3076]: #3073
boehmes@41132
  2072
#3053 := [unit-resolution #3074 #3058 #3057]: #1417
boehmes@41132
  2073
#3054 := [unit-resolution #2808 #3053]: #581
boehmes@41132
  2074
#1740 := (or #1421 #1725)
boehmes@41132
  2075
#280 := (or #277 #237)
boehmes@41132
  2076
#1743 := (iff #280 #1740)
boehmes@41132
  2077
#1736 := (or #1725 #1421)
boehmes@41132
  2078
#1741 := (iff #1736 #1740)
boehmes@41132
  2079
#1742 := [rewrite]: #1741
boehmes@41132
  2080
#1738 := (iff #280 #1736)
boehmes@41132
  2081
#1739 := [monotonicity #1728 #1423]: #1738
boehmes@41132
  2082
#1744 := [trans #1739 #1742]: #1743
boehmes@41132
  2083
#1735 := [asserted]: #280
boehmes@41132
  2084
#1747 := [mp #1735 #1744]: #1740
boehmes@41132
  2085
#3051 := [unit-resolution #1747 #3054]: #1725
boehmes@41132
  2086
#3052 := [unit-resolution #780 #3051 #3056 #3055]: #605
boehmes@41132
  2087
#1455 := (or #1448 #1452)
boehmes@41132
  2088
#243 := (or #241 #242)
boehmes@41132
  2089
#1456 := (iff #243 #1455)
boehmes@41132
  2090
#1457 := [monotonicity #1451 #1454]: #1456
boehmes@41132
  2091
#1447 := [asserted]: #243
boehmes@41132
  2092
#1460 := [mp #1447 #1457]: #1455
boehmes@41132
  2093
#3049 := [unit-resolution #1460 #3052]: #1448
boehmes@41132
  2094
#3050 := [unit-resolution #654 #3049 #3058 #3057]: #496
boehmes@41132
  2095
#1493 := (or #1284 #1452)
boehmes@36900
  2096
#247 := (or #242 #215)
boehmes@41132
  2097
#1496 := (iff #247 #1493)
boehmes@41132
  2098
#1489 := (or #1452 #1284)
boehmes@41132
  2099
#1494 := (iff #1489 #1493)
boehmes@41132
  2100
#1495 := [rewrite]: #1494
boehmes@41132
  2101
#1491 := (iff #247 #1489)
boehmes@41132
  2102
#1492 := [monotonicity #1454 #1286]: #1491
boehmes@41132
  2103
#1497 := [trans #1492 #1495]: #1496
boehmes@41132
  2104
#1488 := [asserted]: #247
boehmes@41132
  2105
#1500 := [mp #1488 #1497]: #1493
boehmes@41132
  2106
#3047 := [unit-resolution #1500 #3052]: #1284
boehmes@41132
  2107
#3048 := [unit-resolution #2789 #3047]: #468
boehmes@41132
  2108
#3045 := [unit-resolution #1343 #3048 #3050]: false
boehmes@41132
  2109
#3043 := [lemma #3045]: #3046
boehmes@41132
  2110
#3033 := [unit-resolution #3043 #3036 #3039 #3072 #3071]: #1939
boehmes@41132
  2111
#3034 := [unit-resolution #882 #3033 #3173]: #710
boehmes@41132
  2112
#3117 := (or #1692 #887 #686)
boehmes@41132
  2113
#3144 := [hypothesis]: #710
boehmes@41132
  2114
#3141 := [unit-resolution #1716 #3144]: #1404
boehmes@41132
  2115
#3142 := [unit-resolution #578 #3141]: #541
boehmes@41132
  2116
#3139 := [unit-resolution #1395 #3142]: #1342
boehmes@41132
  2117
#1699 := (or #1631 #1692)
boehmes@41132
  2118
#274 := (or #273 #265)
boehmes@41132
  2119
#1702 := (iff #274 #1699)
boehmes@41132
  2120
#1696 := (or #1692 #1631)
boehmes@41132
  2121
#1700 := (iff #1696 #1699)
boehmes@41132
  2122
#1701 := [rewrite]: #1700
boehmes@41132
  2123
#1697 := (iff #274 #1696)
boehmes@41132
  2124
#1698 := [monotonicity #1695 #1634]: #1697
boehmes@41132
  2125
#1703 := [trans #1698 #1701]: #1702
boehmes@41132
  2126
#1691 := [asserted]: #274
boehmes@41132
  2127
#1706 := [mp #1691 #1703]: #1699
boehmes@41132
  2128
#3140 := [unit-resolution #1706 #3144]: #1631
boehmes@41132
  2129
#3137 := [hypothesis]: #1635
boehmes@41132
  2130
#1380 := (or #1373 #1377)
boehmes@41132
  2131
#231 := (or #229 #230)
boehmes@41132
  2132
#1381 := (iff #231 #1380)
boehmes@41132
  2133
#1382 := [monotonicity #1376 #1379]: #1381
boehmes@41132
  2134
#1372 := [asserted]: #231
boehmes@41132
  2135
#1385 := [mp #1372 #1382]: #1380
boehmes@41132
  2136
#3138 := [unit-resolution #1385 #3142]: #1377
boehmes@41132
  2137
#3135 := [unit-resolution #708 #3138 #3137 #3140]: #656
boehmes@41132
  2138
#1595 := (or #1346 #1570)
boehmes@41132
  2139
#261 := (or #257 #225)
boehmes@41132
  2140
#1598 := (iff #261 #1595)
boehmes@41132
  2141
#1591 := (or #1570 #1346)
boehmes@41132
  2142
#1596 := (iff #1591 #1595)
boehmes@41132
  2143
#1597 := [rewrite]: #1596
boehmes@41132
  2144
#1593 := (iff #261 #1591)
boehmes@41132
  2145
#1594 := [monotonicity #1573 #1348]: #1593
boehmes@41132
  2146
#1599 := [trans #1594 #1597]: #1598
boehmes@41132
  2147
#1590 := [asserted]: #261
boehmes@41132
  2148
#1602 := [mp #1590 #1599]: #1595
boehmes@41132
  2149
#3136 := [unit-resolution #1602 #3135]: #1346
boehmes@41132
  2150
#3133 := [unit-resolution #539 #3136 #3139]: #493
boehmes@41132
  2151
#1318 := (or #1311 #1315)
boehmes@41132
  2152
#221 := (or #219 #220)
boehmes@41132
  2153
#1319 := (iff #221 #1318)
boehmes@41132
  2154
#1320 := [monotonicity #1314 #1317]: #1319
boehmes@41132
  2155
#1310 := [asserted]: #221
boehmes@41132
  2156
#1323 := [mp #1310 #1320]: #1318
boehmes@41132
  2157
#3134 := [unit-resolution #1323 #3133]: #1315
boehmes@41132
  2158
#3131 := [unit-resolution #1592 #3135]: #1509
boehmes@41132
  2159
#3132 := [unit-resolution #1333 #3133]: #1281
boehmes@41132
  2160
#3129 := [unit-resolution #2789 #3132]: #472
boehmes@41132
  2161
#1473 := (or #1284 #1448)
boehmes@41132
  2162
#245 := (or #241 #215)
boehmes@41132
  2163
#1476 := (iff #245 #1473)
boehmes@41132
  2164
#1469 := (or #1448 #1284)
boehmes@41132
  2165
#1474 := (iff #1469 #1473)
boehmes@41132
  2166
#1475 := [rewrite]: #1474
boehmes@41132
  2167
#1471 := (iff #245 #1469)
boehmes@41132
  2168
#1472 := [monotonicity #1451 #1286]: #1471
boehmes@41132
  2169
#1477 := [trans #1472 #1475]: #1476
boehmes@41132
  2170
#1468 := [asserted]: #245
boehmes@41132
  2171
#1480 := [mp #1468 #1477]: #1473
boehmes@41132
  2172
#3130 := [unit-resolution #1480 #3129]: #1448
boehmes@41132
  2173
#3127 := [unit-resolution #654 #3130 #3131 #3134]: #632
boehmes@41132
  2174
#3128 := [unit-resolution #1879 #3127]: #1756
boehmes@41132
  2175
#3125 := [unit-resolution #1500 #3129]: #1452
boehmes@41132
  2176
#3126 := [unit-resolution #1510 #3129]: #1417
boehmes@41132
  2177
#3123 := [unit-resolution #2808 #3126]: #581
boehmes@41132
  2178
#3124 := [unit-resolution #1747 #3123]: #1725
boehmes@41132
  2179
#3121 := [unit-resolution #780 #3124 #3125 #3128]: #758
boehmes@41132
  2180
#3122 := [unit-resolution #1757 #3123]: #1729
boehmes@41132
  2181
#3119 := [unit-resolution #906 #3122 #3174]: #884
boehmes@41132
  2182
#3120 := [unit-resolution #2126 #3119 #3121]: false
boehmes@41132
  2183
#3118 := [lemma #3120]: #3117
boehmes@41132
  2184
#3031 := [unit-resolution #3118 #3034 #3039]: #686
boehmes@41132
  2185
#1984 := (or #1635 #1943)
boehmes@41132
  2186
#312 := (or #307 #266)
boehmes@41132
  2187
#1987 := (iff #312 #1984)
boehmes@41132
  2188
#1980 := (or #1943 #1635)
boehmes@41132
  2189
#1985 := (iff #1980 #1984)
boehmes@41132
  2190
#1986 := [rewrite]: #1985
boehmes@41132
  2191
#1982 := (iff #312 #1980)
boehmes@41132
  2192
#1983 := [monotonicity #1945 #1637]: #1982
boehmes@41132
  2193
#1988 := [trans #1983 #1986]: #1987
boehmes@41132
  2194
#1979 := [asserted]: #312
boehmes@41132
  2195
#1991 := [mp #1979 #1988]: #1984
boehmes@41132
  2196
#3032 := [unit-resolution #1991 #3031]: #1943
boehmes@41132
  2197
#3029 := [unit-resolution #1014 #3032 #3072 #3071]: #962
boehmes@41132
  2198
#3030 := [unit-resolution #2218 #3029]: #1882
boehmes@41132
  2199
#1994 := (or #1635 #1878)
boehmes@41132
  2200
#313 := (or #298 #266)
boehmes@41132
  2201
#1997 := (iff #313 #1994)
boehmes@41132
  2202
#1990 := (or #1878 #1635)
boehmes@41132
  2203
#1995 := (iff #1990 #1994)
boehmes@41132
  2204
#1996 := [rewrite]: #1995
boehmes@41132
  2205
#1992 := (iff #313 #1990)
boehmes@41132
  2206
#1993 := [monotonicity #1881 #1637]: #1992
boehmes@41132
  2207
#1998 := [trans #1993 #1996]: #1997
boehmes@41132
  2208
#1989 := [asserted]: #313
boehmes@41132
  2209
#2001 := [mp #1989 #1998]: #1994
boehmes@41132
  2210
#3027 := [unit-resolution #2001 #3031]: #1878
boehmes@41132
  2211
#3028 := [unit-resolution #2208 #3029]: #2125
boehmes@41132
  2212
#3025 := [unit-resolution #3084 #3028 #3036 #3027 #3030]: #1729
boehmes@41132
  2213
#3026 := [unit-resolution #906 #3025 #3039]: #884
boehmes@41132
  2214
#3023 := [unit-resolution #2086 #3026]: #2064
boehmes@41132
  2215
#3024 := [unit-resolution #960 #3023 #3036 #3028]: #785
boehmes@41132
  2216
#3021 := [unit-resolution #1829 #3024]: #1817
boehmes@41132
  2217
#3022 := [unit-resolution #834 #3021 #3027 #3030]: #659
boehmes@41132
  2218
#3019 := [unit-resolution #1612 #3022]: #1509
boehmes@41132
  2219
#3020 := [unit-resolution #1869 #3024]: #1513
boehmes@41132
  2220
#3017 := [unit-resolution #1716 #3034]: #1404
boehmes@41132
  2221
#3018 := [unit-resolution #578 #3017]: #541
boehmes@41132
  2222
#3015 := [unit-resolution #1395 #3018]: #1342
boehmes@41132
  2223
#1615 := (or #1346 #1574)
boehmes@41132
  2224
#263 := (or #258 #225)
boehmes@41132
  2225
#1618 := (iff #263 #1615)
boehmes@41132
  2226
#1611 := (or #1574 #1346)
boehmes@41132
  2227
#1616 := (iff #1611 #1615)
boehmes@41132
  2228
#1617 := [rewrite]: #1616
boehmes@41132
  2229
#1613 := (iff #263 #1611)
boehmes@41132
  2230
#1614 := [monotonicity #1576 #1348]: #1613
boehmes@41132
  2231
#1619 := [trans #1614 #1617]: #1618
boehmes@41132
  2232
#1610 := [asserted]: #263
boehmes@41132
  2233
#1622 := [mp #1610 #1619]: #1615
boehmes@41132
  2234
#3016 := [unit-resolution #1622 #3022]: #1346
boehmes@41132
  2235
#3013 := [unit-resolution #539 #3016 #3015]: #493
boehmes@41132
  2236
#3014 := [unit-resolution #1323 #3013]: #1315
boehmes@41132
  2237
#3011 := [unit-resolution #654 #3014 #3020 #3019]: #602
boehmes@41132
  2238
#3012 := [unit-resolution #1859 #3024]: #1756
boehmes@41132
  2239
#3009 := [unit-resolution #2126 #3026]: #1760
boehmes@41132
  2240
#3010 := [unit-resolution #3074 #3019 #3020]: #1417
boehmes@41132
  2241
#3007 := [unit-resolution #2808 #3010]: #581
boehmes@41132
  2242
#3008 := [unit-resolution #1747 #3007]: #1725
boehmes@41132
  2243
#3005 := [unit-resolution #780 #3008 #3009 #3012]: #605
boehmes@41132
  2244
#3006 := [unit-resolution #1460 #3005 #3011]: false
boehmes@41132
  2245
#3004 := [lemma #3006]: #3003
boehmes@41132
  2246
#3182 := [unit-resolution #3004 #3179 #3176 #3181]: #2649
boehmes@41132
  2247
#1235 := (or #1091 #1199 #1221)
boehmes@41132
  2248
#177 := (= f54 f1)
boehmes@41132
  2249
#206 := (or #201 #177)
boehmes@41132
  2250
#205 := (= f61 f1)
boehmes@41132
  2251
#207 := (or #205 #206)
boehmes@41132
  2252
#1238 := (iff #207 #1235)
boehmes@41132
  2253
#1227 := (or #1091 #1199)
boehmes@41132
  2254
#1232 := (or #1221 #1227)
boehmes@41132
  2255
#1236 := (iff #1232 #1235)
boehmes@41132
  2256
#1237 := [rewrite]: #1236
boehmes@41132
  2257
#1233 := (iff #207 #1232)
boehmes@41132
  2258
#1230 := (iff #206 #1227)
boehmes@41132
  2259
#1224 := (or #1199 #1091)
boehmes@41132
  2260
#1228 := (iff #1224 #1227)
boehmes@41132
  2261
#1229 := [rewrite]: #1228
boehmes@41132
  2262
#1225 := (iff #206 #1224)
boehmes@41132
  2263
#1092 := (iff #177 #1091)
boehmes@41132
  2264
#1093 := [rewrite]: #1092
boehmes@41132
  2265
#1226 := [monotonicity #1202 #1093]: #1225
boehmes@41132
  2266
#1231 := [trans #1226 #1229]: #1230
boehmes@41132
  2267
#1222 := (iff #205 #1221)
boehmes@41132
  2268
#1223 := [rewrite]: #1222
boehmes@41132
  2269
#1234 := [monotonicity #1223 #1231]: #1233
boehmes@41132
  2270
#1239 := [trans #1234 #1237]: #1238
boehmes@41132
  2271
#1220 := [asserted]: #207
boehmes@41132
  2272
#1240 := [mp #1220 #1239]: #1235
boehmes@41132
  2273
#3183 := [unit-resolution #1240 #3182 #3180]: #1221
boehmes@41132
  2274
#2682 := (not #1221)
boehmes@41132
  2275
#2742 := (or #2498 #2682)
boehmes@41132
  2276
#184 := (= f56 f1)
boehmes@41132
  2277
#381 := (not #184)
boehmes@41132
  2278
#405 := (not #205)
boehmes@41132
  2279
#412 := (or #405 #381)
boehmes@41132
  2280
#2745 := (iff #412 #2742)
boehmes@41132
  2281
#2738 := (or #2682 #2498)
boehmes@41132
  2282
#2743 := (iff #2738 #2742)
boehmes@41132
  2283
#2744 := [rewrite]: #2743
boehmes@41132
  2284
#2740 := (iff #412 #2738)
boehmes@41132
  2285
#2499 := (iff #381 #2498)
boehmes@41132
  2286
#1119 := (iff #184 #1118)
boehmes@41132
  2287
#1120 := [rewrite]: #1119
boehmes@41132
  2288
#2500 := [monotonicity #1120]: #2499
boehmes@41132
  2289
#2684 := (iff #405 #2682)
boehmes@41132
  2290
#2685 := [monotonicity #1223]: #2684
boehmes@41132
  2291
#2741 := [monotonicity #2685 #2500]: #2740
boehmes@41132
  2292
#2746 := [trans #2741 #2744]: #2745
boehmes@41132
  2293
#2737 := [asserted]: #412
boehmes@41132
  2294
#2749 := [mp #2737 #2746]: #2742
boehmes@41132
  2295
#3184 := [unit-resolution #2749 #3183]: #2498
boehmes@41132
  2296
decl f55 :: S1
boehmes@41132
  2297
#181 := f55
boehmes@41132
  2298
#1115 := (= f1 f55)
boehmes@41132
  2299
#2494 := (not #1115)
boehmes@41132
  2300
#2590 := (or #2494 #2559)
boehmes@41132
  2301
#182 := (= f55 f1)
boehmes@41132
  2302
#380 := (not #182)
boehmes@41132
  2303
#393 := (or #389 #380)
boehmes@41132
  2304
#2593 := (iff #393 #2590)
boehmes@41132
  2305
#2586 := (or #2559 #2494)
boehmes@41132
  2306
#2591 := (iff #2586 #2590)
boehmes@41132
  2307
#2592 := [rewrite]: #2591
boehmes@41132
  2308
#2588 := (iff #393 #2586)
boehmes@41132
  2309
#2496 := (iff #380 #2494)
boehmes@41132
  2310
#1116 := (iff #182 #1115)
boehmes@41132
  2311
#1117 := [rewrite]: #1116
boehmes@41132
  2312
#2497 := [monotonicity #1117]: #2496
boehmes@41132
  2313
#2589 := [monotonicity #2561 #2497]: #2588
boehmes@41132
  2314
#2594 := [trans #2589 #2592]: #2593
boehmes@41132
  2315
#2585 := [asserted]: #393
boehmes@41132
  2316
#2597 := [mp #2585 #2594]: #2590
boehmes@41132
  2317
#3185 := [unit-resolution #2597 #3175]: #2494
boehmes@41132
  2318
decl f53 :: S1
boehmes@41132
  2319
#174 := f53
boehmes@41132
  2320
#1088 := (= f1 f53)
boehmes@41132
  2321
#2433 := (not #1088)
boehmes@41132
  2322
#2933 := (or #1509 #1115 #1118 #989 #992 #863)
boehmes@41132
  2323
#2957 := [hypothesis]: #629
boehmes@41132
  2324
#2958 := [unit-resolution #1592 #2957]: #1570
boehmes@41132
  2325
#2959 := (or #1943 #656 #863)
boehmes@41132
  2326
#2991 := [hypothesis]: #1570
boehmes@41132
  2327
#2970 := [hypothesis]: #839
boehmes@41132
  2328
#2967 := [unit-resolution #1991 #2970]: #1635
boehmes@41132
  2329
#2968 := [unit-resolution #1951 #2970]: #1939
boehmes@41132
  2330
#2965 := [unit-resolution #882 #2968 #3173]: #710
boehmes@41132
  2331
#2966 := [unit-resolution #1706 #2965]: #1631
boehmes@41132
  2332
#2963 := [unit-resolution #708 #2966 #2967 #2991]: #544
boehmes@41132
  2333
#2964 := [unit-resolution #1716 #2965]: #1404
boehmes@41132
  2334
#2961 := [unit-resolution #578 #2964]: #541
boehmes@41132
  2335
#2962 := [unit-resolution #1385 #2961 #2963]: false
boehmes@41132
  2336
#2960 := [lemma #2962]: #2959
boehmes@41132
  2337
#2955 := [unit-resolution #2960 #2958 #3173]: #1943
boehmes@41132
  2338
#2956 := [unit-resolution #1014 #2955 #3072 #3071]: #962
boehmes@41132
  2339
#2953 := [unit-resolution #2208 #2956]: #2125
boehmes@41132
  2340
#2954 := [unit-resolution #1632 #2957]: #1346
boehmes@41132
  2341
#2972 := (or #1342 #656 #863)
boehmes@41132
  2342
#2979 := [hypothesis]: #517
boehmes@41132
  2343
#2980 := [unit-resolution #1395 #2979]: #1373
boehmes@41132
  2344
#2977 := [unit-resolution #578 #2980]: #565
boehmes@41132
  2345
#2978 := [unit-resolution #1716 #2977]: #1692
boehmes@41132
  2346
#2975 := [unit-resolution #882 #2978 #3173]: #836
boehmes@41132
  2347
#2976 := [unit-resolution #1405 #2979]: #1377
boehmes@41132
  2348
#2973 := [unit-resolution #1726 #2977]: #1631
boehmes@41132
  2349
#2974 := [unit-resolution #708 #2973 #2976 #2991]: #686
boehmes@41132
  2350
#2971 := [unit-resolution #1971 #2974 #2975]: false
boehmes@41132
  2351
#2969 := [lemma #2971]: #2972
boehmes@41132
  2352
#2951 := [unit-resolution #2969 #2958 #3173]: #1342
boehmes@41132
  2353
#2952 := [unit-resolution #539 #2951 #2954]: #493
boehmes@41132
  2354
#2949 := [unit-resolution #1333 #2952]: #1281
boehmes@41132
  2355
#2950 := [unit-resolution #2789 #2949]: #472
boehmes@41132
  2356
#2947 := [unit-resolution #1500 #2950]: #1452
boehmes@41132
  2357
#2948 := [unit-resolution #1510 #2950]: #1417
boehmes@41132
  2358
#2945 := [unit-resolution #2808 #2948]: #581
boehmes@41132
  2359
#2946 := [unit-resolution #1747 #2945]: #1725
boehmes@41132
  2360
#2981 := (or #1878 #656 #863)
boehmes@41132
  2361
#2992 := [hypothesis]: #809
boehmes@41132
  2362
#2989 := [unit-resolution #2001 #2992]: #1635
boehmes@41132
  2363
#2990 := [unit-resolution #1961 #2992]: #1939
boehmes@41132
  2364
#2987 := [unit-resolution #882 #2990 #3173]: #710
boehmes@41132
  2365
#2988 := [unit-resolution #1706 #2987]: #1631
boehmes@41132
  2366
#2985 := [unit-resolution #708 #2988 #2989 #2991]: #544
boehmes@41132
  2367
#2986 := [unit-resolution #1716 #2987]: #1404
boehmes@41132
  2368
#2983 := [unit-resolution #578 #2986]: #541
boehmes@41132
  2369
#2984 := [unit-resolution #1385 #2983 #2985]: false
boehmes@41132
  2370
#2982 := [lemma #2984]: #2981
boehmes@41132
  2371
#2943 := [unit-resolution #2982 #2958 #3173]: #1878
boehmes@41132
  2372
#2944 := [unit-resolution #1612 #2957]: #1574
boehmes@41132
  2373
#2941 := [unit-resolution #2218 #2956]: #1882
boehmes@41132
  2374
#2942 := [unit-resolution #834 #2941 #2944 #2943]: #782
boehmes@41132
  2375
#2939 := [hypothesis]: #2498
boehmes@41132
  2376
#2940 := [hypothesis]: #2494
boehmes@41132
  2377
#2193 := (or #2186 #2190)
boehmes@36900
  2378
#146 := (= f45 f1)
boehmes@36900
  2379
#340 := (not #146)
boehmes@41132
  2380
#341 := (or #339 #340)
boehmes@41132
  2381
#2194 := (iff #341 #2193)
boehmes@41132
  2382
#2191 := (iff #340 #2190)
boehmes@41132
  2383
#966 := (iff #146 #965)
boehmes@41132
  2384
#967 := [rewrite]: #966
boehmes@41132
  2385
#2192 := [monotonicity #967]: #2191
boehmes@41132
  2386
#2195 := [monotonicity #2189 #2192]: #2194
boehmes@41132
  2387
#2185 := [asserted]: #341
boehmes@41132
  2388
#2198 := [mp #2185 #2195]: #2193
boehmes@41132
  2389
#2937 := [unit-resolution #2198 #2956]: #2190
boehmes@41132
  2390
#1135 := (or #965 #1088 #1115 #1118)
boehmes@41132
  2391
#175 := (= f53 f1)
boehmes@36900
  2392
#185 := (or #175 #146)
boehmes@36900
  2393
#186 := (or #184 #185)
boehmes@36900
  2394
#187 := (or #182 #186)
boehmes@41132
  2395
#1138 := (iff #187 #1135)
boehmes@41132
  2396
#1124 := (or #965 #1088)
boehmes@41132
  2397
#1129 := (or #1118 #1124)
boehmes@41132
  2398
#1132 := (or #1115 #1129)
boehmes@41132
  2399
#1136 := (iff #1132 #1135)
boehmes@41132
  2400
#1137 := [rewrite]: #1136
boehmes@41132
  2401
#1133 := (iff #187 #1132)
boehmes@41132
  2402
#1130 := (iff #186 #1129)
boehmes@41132
  2403
#1127 := (iff #185 #1124)
boehmes@41132
  2404
#1121 := (or #1088 #965)
boehmes@41132
  2405
#1125 := (iff #1121 #1124)
boehmes@41132
  2406
#1126 := [rewrite]: #1125
boehmes@41132
  2407
#1122 := (iff #185 #1121)
boehmes@41132
  2408
#1089 := (iff #175 #1088)
boehmes@41132
  2409
#1090 := [rewrite]: #1089
boehmes@41132
  2410
#1123 := [monotonicity #1090 #967]: #1122
boehmes@41132
  2411
#1128 := [trans #1123 #1126]: #1127
boehmes@41132
  2412
#1131 := [monotonicity #1120 #1128]: #1130
boehmes@41132
  2413
#1134 := [monotonicity #1117 #1131]: #1133
boehmes@41132
  2414
#1139 := [trans #1134 #1137]: #1138
boehmes@41132
  2415
#1114 := [asserted]: #187
boehmes@41132
  2416
#1140 := [mp #1114 #1139]: #1135
boehmes@41132
  2417
#2938 := [unit-resolution #1140 #2937 #2940 #2939]: #1088
boehmes@41132
  2418
#2458 := (or #2129 #2433)
boehmes@41132
  2419
#372 := (not #175)
boehmes@41132
  2420
#376 := (or #372 #332)
boehmes@41132
  2421
#2461 := (iff #376 #2458)
boehmes@41132
  2422
#2454 := (or #2433 #2129)
boehmes@41132
  2423
#2459 := (iff #2454 #2458)
boehmes@41132
  2424
#2460 := [rewrite]: #2459
boehmes@41132
  2425
#2456 := (iff #376 #2454)
boehmes@41132
  2426
#2435 := (iff #372 #2433)
boehmes@41132
  2427
#2436 := [monotonicity #1090]: #2435
boehmes@41132
  2428
#2457 := [monotonicity #2436 #2131]: #2456
boehmes@41132
  2429
#2462 := [trans #2457 #2460]: #2461
boehmes@41132
  2430
#2453 := [asserted]: #376
boehmes@41132
  2431
#2465 := [mp #2453 #2462]: #2458
boehmes@41132
  2432
#2935 := [unit-resolution #2465 #2938]: #2129
boehmes@41132
  2433
#2936 := [unit-resolution #3106 #2935 #2942 #2946 #2947 #2953]: false
boehmes@41132
  2434
#2934 := [lemma #2936]: #2933
boehmes@41132
  2435
#3186 := [unit-resolution #2934 #3185 #3184 #3179 #3176 #3181]: #1509
boehmes@41132
  2436
#2773 := (or #2433 #989 #992 #863 #629)
boehmes@41132
  2437
#2813 := [hypothesis]: #1088
boehmes@41132
  2438
#2448 := (or #2372 #2433)
boehmes@41132
  2439
#375 := (or #372 #364)
boehmes@41132
  2440
#2451 := (iff #375 #2448)
boehmes@41132
  2441
#2444 := (or #2433 #2372)
boehmes@41132
  2442
#2449 := (iff #2444 #2448)
boehmes@41132
  2443
#2450 := [rewrite]: #2449
boehmes@41132
  2444
#2446 := (iff #375 #2444)
boehmes@41132
  2445
#2447 := [monotonicity #2436 #2375]: #2446
boehmes@41132
  2446
#2452 := [trans #2447 #2450]: #2451
boehmes@41132
  2447
#2443 := [asserted]: #375
boehmes@41132
  2448
#2455 := [mp #2443 #2452]: #2448
boehmes@41132
  2449
#2814 := [unit-resolution #2455 #2813]: #2372
boehmes@41132
  2450
#2811 := [unit-resolution #2465 #2813]: #2129
boehmes@41132
  2451
#2822 := (or #1421 #863 #989 #992 #938 #629 #1061)
boehmes@41132
  2452
#2901 := [hypothesis]: #2372
boehmes@41132
  2453
#2839 := [hypothesis]: #581
boehmes@41132
  2454
#2840 := [unit-resolution #1757 #2839]: #1729
boehmes@41132
  2455
#2854 := (or #2064 #1061 #734)
boehmes@41132
  2456
#2869 := [hypothesis]: #908
boehmes@41132
  2457
#2071 := (or #2064 #2068)
boehmes@41132
  2458
#325 := (or #323 #324)
boehmes@41132
  2459
#2072 := (iff #325 #2071)
boehmes@41132
  2460
#2073 := [monotonicity #2067 #2070]: #2072
boehmes@41132
  2461
#2063 := [asserted]: #325
boehmes@41132
  2462
#2076 := [mp #2063 #2073]: #2071
boehmes@41132
  2463
#2870 := [unit-resolution #2076 #2869]: #2068
boehmes@41132
  2464
#2867 := [unit-resolution #2086 #2869]: #2033
boehmes@41132
  2465
#2868 := [unit-resolution #906 #2867 #2887]: #887
boehmes@41132
  2466
#2356 := (or #2037 #2341)
boehmes@41132
  2467
#362 := (or #359 #319)
boehmes@41132
  2468
#2359 := (iff #362 #2356)
boehmes@41132
  2469
#2352 := (or #2341 #2037)
boehmes@41132
  2470
#2357 := (iff #2352 #2356)
boehmes@41132
  2471
#2358 := [rewrite]: #2357
boehmes@41132
  2472
#2354 := (iff #362 #2352)
boehmes@41132
  2473
#2355 := [monotonicity #2344 #2039]: #2354
boehmes@41132
  2474
#2360 := [trans #2355 #2358]: #2359
boehmes@41132
  2475
#2351 := [asserted]: #362
boehmes@41132
  2476
#2363 := [mp #2351 #2360]: #2356
boehmes@41132
  2477
#2865 := [unit-resolution #2363 #2868]: #2341
boehmes@41132
  2478
#2866 := [unit-resolution #1086 #2865 #2901 #2870]: #1064
boehmes@41132
  2479
#2863 := [unit-resolution #2373 #2868]: #2345
boehmes@41132
  2480
#2864 := [unit-resolution #1200 #2863]: #1187
boehmes@41132
  2481
#2676 := (or #2376 #2636)
boehmes@41132
  2482
#404 := (or #399 #365)
boehmes@41132
  2483
#2679 := (iff #404 #2676)
boehmes@41132
  2484
#2672 := (or #2636 #2376)
boehmes@41132
  2485
#2677 := (iff #2672 #2676)
boehmes@41132
  2486
#2678 := [rewrite]: #2677
boehmes@41132
  2487
#2674 := (iff #404 #2672)
boehmes@41132
  2488
#2675 := [monotonicity #2639 #2378]: #2674
boehmes@41132
  2489
#2680 := [trans #2675 #2678]: #2679
boehmes@41132
  2490
#2671 := [asserted]: #404
boehmes@41132
  2491
#2683 := [mp #2671 #2680]: #2676
boehmes@41132
  2492
#2853 := [unit-resolution #2683 #2864 #2866]: false
boehmes@41132
  2493
#2851 := [lemma #2853]: #2854
boehmes@41132
  2494
#2837 := [unit-resolution #2851 #2840 #2901]: #2064
boehmes@41132
  2495
#2838 := [unit-resolution #1747 #2839]: #1725
boehmes@41132
  2496
#2871 := (or #1760 #1061 #734)
boehmes@41132
  2497
#2889 := [hypothesis]: #758
boehmes@41132
  2498
#2890 := [unit-resolution #2116 #2889]: #2068
boehmes@41132
  2499
#2888 := [unit-resolution #2126 #2889]: #2033
boehmes@41132
  2500
#2885 := [unit-resolution #906 #2888 #2887]: #887
boehmes@41132
  2501
#2886 := [unit-resolution #2363 #2885]: #2341
boehmes@41132
  2502
#2883 := [unit-resolution #1086 #2886 #2901 #2890]: #1064
boehmes@41132
  2503
#2884 := [unit-resolution #2373 #2885]: #2345
boehmes@41132
  2504
#2881 := [unit-resolution #1200 #2884]: #1187
boehmes@41132
  2505
#2882 := [unit-resolution #2683 #2881 #2883]: false
boehmes@41132
  2506
#2872 := [lemma #2882]: #2871
boehmes@41132
  2507
#2835 := [unit-resolution #2872 #2840 #2901]: #1760
boehmes@41132
  2508
#2841 := (or #605 #938 #908 #989 #992 #758 #731 #629 #863)
boehmes@41132
  2509
#2852 := [hypothesis]: #2064
boehmes@41132
  2510
#2849 := [hypothesis]: #1760
boehmes@41132
  2511
#2850 := [unit-resolution #780 #3112 #2849 #3109]: #755
boehmes@41132
  2512
#2847 := [unit-resolution #1859 #2850]: #1821
boehmes@41132
  2513
#2911 := (or #656 #605 #731 #938 #629 #989 #992 #863)
boehmes@41132
  2514
#2931 := [unit-resolution #2960 #2991 #3173]: #1943
boehmes@41132
  2515
#2932 := [unit-resolution #1014 #2931 #3072 #3071]: #962
boehmes@41132
  2516
#2929 := [unit-resolution #2208 #2932]: #2125
boehmes@41132
  2517
#2930 := [unit-resolution #2969 #2991 #3173]: #1342
boehmes@41132
  2518
#2927 := [unit-resolution #2982 #2991 #3173]: #1878
boehmes@41132
  2519
#2928 := [unit-resolution #2218 #2932]: #1882
boehmes@41132
  2520
#2925 := [unit-resolution #3106 #2929 #3116 #3109 #3112]: #1817
boehmes@41132
  2521
#2926 := [unit-resolution #834 #2925 #2928 #2927]: #659
boehmes@41132
  2522
#2923 := [unit-resolution #1622 #2926]: #1346
boehmes@41132
  2523
#2924 := [unit-resolution #539 #2923 #2930]: #493
boehmes@41132
  2524
#2921 := [unit-resolution #1323 #2924]: #1315
boehmes@41132
  2525
#2922 := [unit-resolution #1333 #2924]: #1281
boehmes@41132
  2526
#2919 := [unit-resolution #2789 #2922]: #472
boehmes@41132
  2527
#2920 := [unit-resolution #1480 #2919]: #1448
boehmes@41132
  2528
#2917 := [unit-resolution #654 #2920 #3081 #2921]: #632
boehmes@41132
  2529
#2918 := [unit-resolution #1869 #2917]: #1821
boehmes@41132
  2530
#2915 := [unit-resolution #960 #2918 #3116 #2929]: #908
boehmes@41132
  2531
#2916 := [unit-resolution #1879 #2917]: #1756
boehmes@41132
  2532
#2913 := [unit-resolution #780 #2916 #3112 #3109]: #758
boehmes@41132
  2533
#2914 := [unit-resolution #2096 #2913 #2915]: false
boehmes@41132
  2534
#2912 := [lemma #2914]: #2911
boehmes@41132
  2535
#2848 := [unit-resolution #2912 #3112 #3109 #3116 #3081 #3072 #3071 #3173]: #656
boehmes@41132
  2536
#1577 := (or #1570 #1574)
boehmes@41132
  2537
#259 := (or #257 #258)
boehmes@41132
  2538
#1578 := (iff #259 #1577)
boehmes@41132
  2539
#1579 := [monotonicity #1573 #1576]: #1578
boehmes@41132
  2540
#1569 := [asserted]: #259
boehmes@41132
  2541
#1582 := [mp #1569 #1579]: #1577
boehmes@41132
  2542
#2845 := [unit-resolution #1582 #2848]: #1574
boehmes@41132
  2543
#2846 := [unit-resolution #1839 #2850]: #1817
boehmes@41132
  2544
#2993 := (or #2125 #659 #782 #989 #992)
boehmes@41132
  2545
#3001 := [hypothesis]: #935
boehmes@41132
  2546
#3002 := [unit-resolution #2208 #3001]: #2186
boehmes@41132
  2547
#2999 := [unit-resolution #1014 #3002 #3072 #3071]: #839
boehmes@41132
  2548
#2997 := [hypothesis]: #1574
boehmes@41132
  2549
#2241 := (or #1882 #2125)
boehmes@41132
  2550
#346 := (or #331 #299)
boehmes@41132
  2551
#2244 := (iff #346 #2241)
boehmes@41132
  2552
#2237 := (or #2125 #1882)
boehmes@41132
  2553
#2242 := (iff #2237 #2241)
boehmes@41132
  2554
#2243 := [rewrite]: #2242
boehmes@41132
  2555
#2239 := (iff #346 #2237)
boehmes@41132
  2556
#2240 := [monotonicity #2128 #1884]: #2239
boehmes@41132
  2557
#2245 := [trans #2240 #2243]: #2244
boehmes@41132
  2558
#2236 := [asserted]: #346
boehmes@41132
  2559
#2248 := [mp #2236 #2245]: #2241
boehmes@41132
  2560
#2998 := [unit-resolution #2248 #3001]: #1882
boehmes@41132
  2561
#2995 := [unit-resolution #834 #2998 #2997 #3000]: #809
boehmes@41132
  2562
#1974 := (or #1878 #1943)
boehmes@41132
  2563
#311 := (or #307 #298)
boehmes@41132
  2564
#1977 := (iff #311 #1974)
boehmes@41132
  2565
#1970 := (or #1943 #1878)
boehmes@41132
  2566
#1975 := (iff #1970 #1974)
boehmes@41132
  2567
#1976 := [rewrite]: #1975
boehmes@41132
  2568
#1972 := (iff #311 #1970)
boehmes@41132
  2569
#1973 := [monotonicity #1945 #1881]: #1972
boehmes@41132
  2570
#1978 := [trans #1973 #1976]: #1977
boehmes@41132
  2571
#1969 := [asserted]: #311
boehmes@41132
  2572
#1981 := [mp #1969 #1978]: #1974
boehmes@41132
  2573
#2996 := [unit-resolution #1981 #2995 #2999]: false
boehmes@41132
  2574
#2994 := [lemma #2996]: #2993
boehmes@41132
  2575
#2843 := [unit-resolution #2994 #2846 #2845 #3072 #3071]: #2125
boehmes@41132
  2576
#2844 := [unit-resolution #960 #2843 #2847 #3116 #2852]: false
boehmes@41132
  2577
#2842 := [lemma #2844]: #2841
boehmes@41132
  2578
#2836 := [unit-resolution #2842 #2837 #3116 #3072 #3071 #2835 #2838 #3081 #3173]: #605
boehmes@41132
  2579
#2833 := [unit-resolution #1460 #2836]: #1448
boehmes@41132
  2580
#2834 := [unit-resolution #1500 #2836]: #1284
boehmes@41132
  2581
#2831 := [unit-resolution #2789 #2834]: #468
boehmes@41132
  2582
#2832 := [unit-resolution #1343 #2831]: #1315
boehmes@41132
  2583
#2829 := [unit-resolution #654 #2832 #3081 #2833]: #632
boehmes@41132
  2584
#2830 := [unit-resolution #1869 #2829]: #1821
boehmes@41132
  2585
#2827 := [unit-resolution #960 #2830 #3116 #2837]: #935
boehmes@41132
  2586
#2828 := [unit-resolution #2208 #2827]: #2186
boehmes@41132
  2587
#2825 := [unit-resolution #1014 #2828 #3072 #3071]: #839
boehmes@41132
  2588
#1842 := (or #1513 #1817)
boehmes@41132
  2589
#294 := (or #290 #250)
boehmes@41132
  2590
#1845 := (iff #294 #1842)
boehmes@41132
  2591
#1838 := (or #1817 #1513)
boehmes@41132
  2592
#1843 := (iff #1838 #1842)
boehmes@41132
  2593
#1844 := [rewrite]: #1843
boehmes@41132
  2594
#1840 := (iff #294 #1838)
boehmes@41132
  2595
#1841 := [monotonicity #1820 #1515]: #1840
boehmes@41132
  2596
#1846 := [trans #1841 #1844]: #1845
boehmes@41132
  2597
#1837 := [asserted]: #294
boehmes@41132
  2598
#1849 := [mp #1837 #1846]: #1842
boehmes@41132
  2599
#2826 := [unit-resolution #1849 #2829]: #1817
boehmes@41132
  2600
#2823 := [unit-resolution #2994 #2827 #2826 #3072 #3071]: #659
boehmes@41132
  2601
#2824 := [unit-resolution #1582 #2823]: #1570
boehmes@41132
  2602
#2821 := [unit-resolution #2960 #2824 #2825 #3173]: false
boehmes@41132
  2603
#2819 := [lemma #2821]: #2822
boehmes@41132
  2604
#2812 := [unit-resolution #2819 #2811 #3072 #3071 #3173 #3081 #2814]: #1421
boehmes@41132
  2605
#2809 := [unit-resolution #2808 #2812]: #577
boehmes@41132
  2606
#2810 := [unit-resolution #3074 #2809 #3081]: #632
boehmes@41132
  2607
#2798 := [unit-resolution #1869 #2810]: #1821
boehmes@41132
  2608
#2799 := [unit-resolution #1849 #2810]: #1817
boehmes@41132
  2609
#2815 := (or #2125 #863 #989 #992 #782)
boehmes@41132
  2610
#2820 := [unit-resolution #2994 #3001 #3000 #3072 #3071]: #659
boehmes@41132
  2611
#2817 := [unit-resolution #1582 #2820]: #1570
boehmes@41132
  2612
#2818 := [unit-resolution #2960 #2817 #2999 #3173]: false
boehmes@41132
  2613
#2816 := [lemma #2818]: #2815
boehmes@41132
  2614
#2796 := [unit-resolution #2816 #2799 #3072 #3071 #3173]: #2125
boehmes@41132
  2615
#2797 := [unit-resolution #960 #2796 #2811 #2798]: #908
boehmes@41132
  2616
#2794 := [unit-resolution #2851 #2797 #2814]: #734
boehmes@41132
  2617
#2795 := [unit-resolution #1879 #2810]: #1756
boehmes@41132
  2618
#2792 := [unit-resolution #1490 #2809]: #1452
boehmes@41132
  2619
#2793 := [unit-resolution #2096 #2797]: #1760
boehmes@41132
  2620
#2790 := [unit-resolution #780 #2793 #2792 #2795]: #731
boehmes@41132
  2621
#2791 := [unit-resolution #1737 #2790 #2794]: false
boehmes@41132
  2622
#2771 := [lemma #2791]: #2773
boehmes@41132
  2623
#3187 := [unit-resolution #2771 #3179 #3176 #3181 #3186]: #2433
boehmes@41132
  2624
#3188 := [unit-resolution #1140 #3187 #3185 #3184]: #965
boehmes@41132
  2625
#3189 := [unit-resolution #2198 #3188]: #2186
boehmes@41132
  2626
#3190 := [unit-resolution #1014 #3189 #3179 #3176]: #839
boehmes@41132
  2627
#3191 := [unit-resolution #1981 #3190]: #1878
boehmes@41132
  2628
#2231 := (or #1882 #2190)
boehmes@41132
  2629
#345 := (or #340 #299)
boehmes@41132
  2630
#2234 := (iff #345 #2231)
boehmes@41132
  2631
#2227 := (or #2190 #1882)
boehmes@41132
  2632
#2232 := (iff #2227 #2231)
boehmes@41132
  2633
#2233 := [rewrite]: #2232
boehmes@41132
  2634
#2229 := (iff #345 #2227)
boehmes@41132
  2635
#2230 := [monotonicity #2192 #1884]: #2229
boehmes@41132
  2636
#2235 := [trans #2230 #2233]: #2234
boehmes@41132
  2637
#2226 := [asserted]: #345
boehmes@41132
  2638
#2238 := [mp #2226 #2235]: #2231
boehmes@41132
  2639
#3192 := [unit-resolution #2238 #3188]: #1882
boehmes@41132
  2640
#3193 := [unit-resolution #2960 #3190 #3181]: #656
boehmes@41132
  2641
#3194 := [unit-resolution #1582 #3193]: #1574
boehmes@41132
  2642
#3195 := [unit-resolution #834 #3194 #3192 #3191]: #782
boehmes@41132
  2643
#3196 := [unit-resolution #1849 #3195]: #1513
boehmes@41132
  2644
#3197 := [unit-resolution #1602 #3193]: #1346
boehmes@41132
  2645
#3198 := [unit-resolution #1951 #3190]: #1939
boehmes@41132
  2646
#3199 := [unit-resolution #882 #3198 #3181]: #710
boehmes@41132
  2647
#3200 := [unit-resolution #1716 #3199]: #1404
boehmes@41132
  2648
#3201 := [unit-resolution #578 #3200]: #541
boehmes@41132
  2649
#3202 := [unit-resolution #1395 #3201]: #1342
boehmes@41132
  2650
#3203 := [unit-resolution #539 #3202 #3197]: #493
boehmes@41132
  2651
#3204 := [unit-resolution #1323 #3203]: #1315
boehmes@41132
  2652
#3205 := [unit-resolution #654 #3204 #3186 #3196]: #602
boehmes@41132
  2653
#3206 := [unit-resolution #1333 #3203]: #1281
boehmes@41132
  2654
#3207 := [unit-resolution #2789 #3206]: #472
boehmes@41132
  2655
#3208 := [unit-resolution #1480 #3207 #3205]: false
boehmes@41132
  2656
#3210 := [lemma #3208]: #3209
boehmes@41132
  2657
#3385 := [unit-resolution #3210 #3180]: #2559
boehmes@41132
  2658
#1266 := (or #1145 #1242)
boehmes@41132
  2659
decl f5 :: S1
boehmes@41132
  2660
#14 := f5
boehmes@41132
  2661
#452 := (= f1 f5)
boehmes@41132
  2662
#1274 := (or #452 #1145 #1242)
boehmes@41132
  2663
#2878 := (iff #1274 #1266)
boehmes@41132
  2664
#2873 := (or false #1145 #1242)
boehmes@41132
  2665
#2876 := (iff #2873 #1266)
boehmes@41132
  2666
#2877 := [rewrite]: #2876
boehmes@41132
  2667
#2874 := (iff #1274 #2873)
boehmes@41132
  2668
#2777 := (iff #452 false)
boehmes@41132
  2669
#456 := (not #452)
boehmes@41132
  2670
#15 := (= f5 f1)
boehmes@41132
  2671
#16 := (not #15)
boehmes@41132
  2672
#457 := (iff #16 #456)
boehmes@41132
  2673
#454 := (iff #15 #452)
boehmes@41132
  2674
#455 := [rewrite]: #454
boehmes@41132
  2675
#458 := [monotonicity #455]: #457
boehmes@41132
  2676
#451 := [asserted]: #16
boehmes@41132
  2677
#461 := [mp #451 #458]: #456
boehmes@41132
  2678
<