src/HOL/SMT/Examples/cert/z3_prop_08.proof

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
custom-made (top-down) atomize_conv,
store predicate and function symbols in a table instead of a list for faster lookup,
updated certificates

+
−#2 := false
+
−decl up_1 :: bool
+
−#4 := up_1
+
−#75 := (not up_1)
+
−#246 := (iff #75 false)
+
−#1 := true
+
−#214 := (not true)
+
−#217 := (iff #214 false)
+
−#218 := [rewrite]: #217
+
−#244 := (iff #75 #214)
+
−#238 := (iff up_1 true)
+
−#241 := (iff up_1 #238)
+
−#239 := (iff #238 up_1)
+
−#240 := [rewrite]: #239
+
−#242 := [symm #240]: #241
+
−decl up_4 :: bool
+
−#7 := up_4
+
−decl up_2 :: bool
+
−#5 := up_2
+
−#161 := (or up_1 up_2 up_4)
+
−#200 := (iff #161 up_1)
+
−#195 := (or up_1 false false)
+
−#198 := (iff #195 up_1)
+
−#199 := [rewrite]: #198
+
−#196 := (iff #161 #195)
+
−#189 := (iff up_4 false)
+
−#102 := (not up_4)
+
−#192 := (iff #102 #189)
+
−#190 := (iff #189 #102)
+
−#191 := [rewrite]: #190
+
−#193 := [symm #191]: #192
+
−decl up_3 :: bool
+
−#6 := up_3
+
−#108 := (or up_3 #102)
+
−#180 := (iff #108 #102)
+
−#175 := (or false #102)
+
−#178 := (iff #175 #102)
+
−#179 := [rewrite]: #178
+
−#176 := (iff #108 #175)
+
−#152 := (iff up_3 false)
+
−#16 := (not up_3)
+
−#155 := (iff #16 #152)
+
−#153 := (iff #152 #16)
+
−#154 := [rewrite]: #153
+
−#156 := [symm #154]: #155
+
−decl up_9 :: bool
+
−#32 := up_9
+
−#33 := (not up_9)
+
−#34 := (and up_9 #33)
+
−decl up_8 :: bool
+
−#30 := up_8
+
−#35 := (or up_8 #34)
+
−#31 := (not up_8)
+
−#36 := (and #31 #35)
+
−#37 := (or up_3 #36)
+
−#38 := (not #37)
+
−#138 := (iff #38 #16)
+
−#136 := (iff #37 up_3)
+
−#131 := (or up_3 false)
+
−#134 := (iff #131 up_3)
+
−#135 := [rewrite]: #134
+
−#132 := (iff #37 #131)
+
−#129 := (iff #36 false)
+
−#124 := (and #31 up_8)
+
−#127 := (iff #124 false)
+
−#128 := [rewrite]: #127
+
−#125 := (iff #36 #124)
+
−#122 := (iff #35 up_8)
+
−#117 := (or up_8 false)
+
−#120 := (iff #117 up_8)
+
−#121 := [rewrite]: #120
+
−#118 := (iff #35 #117)
+
−#114 := (iff #34 false)
+
−#116 := [rewrite]: #114
+
−#119 := [monotonicity #116]: #118
+
−#123 := [trans #119 #121]: #122
+
−#126 := [monotonicity #123]: #125
+
−#130 := [trans #126 #128]: #129
+
−#133 := [monotonicity #130]: #132
+
−#137 := [trans #133 #135]: #136
+
−#139 := [monotonicity #137]: #138
+
−#113 := [asserted]: #38
+
−#142 := [mp #113 #139]: #16
+
−#157 := [mp #142 #156]: #152
+
−#177 := [monotonicity #157]: #176
+
−#181 := [trans #177 #179]: #180
+
−#27 := (or up_4 false)
+
−#28 := (not #27)
+
−#29 := (or #28 up_3)
+
−#111 := (iff #29 #108)
+
−#105 := (or #102 up_3)
+
−#109 := (iff #105 #108)
+
−#110 := [rewrite]: #109
+
−#106 := (iff #29 #105)
+
−#103 := (iff #28 #102)
+
−#99 := (iff #27 up_4)
+
−#101 := [rewrite]: #99
+
−#104 := [monotonicity #101]: #103
+
−#107 := [monotonicity #104]: #106
+
−#112 := [trans #107 #110]: #111
+
−#98 := [asserted]: #29
+
−#115 := [mp #98 #112]: #108
+
−#182 := [mp #115 #181]: #102
+
−#194 := [mp #182 #193]: #189
+
−#183 := (iff up_2 false)
+
−#92 := (not up_2)
+
−#186 := (iff #92 #183)
+
−#184 := (iff #183 #92)
+
−#185 := [rewrite]: #184
+
−#187 := [symm #185]: #186
+
−#95 := (or #92 up_3)
+
−#172 := (iff #95 #92)
+
−#167 := (or #92 false)
+
−#170 := (iff #167 #92)
+
−#171 := [rewrite]: #170
+
−#168 := (iff #95 #167)
+
−#169 := [monotonicity #157]: #168
+
−#173 := [trans #169 #171]: #172
+
−decl up_7 :: bool
+
−#21 := up_7
+
−#22 := (not up_7)
+
−#23 := (or up_7 #22)
+
−#24 := (and up_2 #23)
+
−#25 := (not #24)
+
−#26 := (or #25 up_3)
+
−#96 := (iff #26 #95)
+
−#93 := (iff #25 #92)
+
−#90 := (iff #24 up_2)
+
−#85 := (and up_2 true)
+
−#88 := (iff #85 up_2)
+
−#89 := [rewrite]: #88
+
−#86 := (iff #24 #85)
+
−#82 := (iff #23 true)
+
−#84 := [rewrite]: #82
+
−#87 := [monotonicity #84]: #86
+
−#91 := [trans #87 #89]: #90
+
−#94 := [monotonicity #91]: #93
+
−#97 := [monotonicity #94]: #96
+
−#81 := [asserted]: #26
+
−#100 := [mp #81 #97]: #95
+
−#174 := [mp #100 #173]: #92
+
−#188 := [mp #174 #187]: #183
+
−#197 := [monotonicity #188 #194]: #196
+
−#201 := [trans #197 #199]: #200
+
−#58 := (or up_1 up_2 up_3 up_4)
+
−#164 := (iff #58 #161)
+
−#158 := (or up_1 up_2 false up_4)
+
−#162 := (iff #158 #161)
+
−#163 := [rewrite]: #162
+
−#159 := (iff #58 #158)
+
−#160 := [monotonicity #157]: #159
+
−#165 := [trans #160 #163]: #164
+
−#8 := (or up_3 up_4)
+
−#9 := (or up_2 #8)
+
−#10 := (or up_1 #9)
+
−#59 := (iff #10 #58)
+
−#60 := [rewrite]: #59
+
−#55 := [asserted]: #10
+
−#61 := [mp #55 #60]: #58
+
−#166 := [mp #61 #165]: #161
+
−#202 := [mp #166 #201]: up_1
+
−#243 := [mp #202 #242]: #238
+
−#245 := [monotonicity #243]: #244
+
−#247 := [trans #245 #218]: #246
+
−#78 := (or #75 up_2)
+
−#235 := (iff #78 #75)
+
−#230 := (or #75 false)
+
−#233 := (iff #230 #75)
+
−#234 := [rewrite]: #233
+
−#231 := (iff #78 #230)
+
−#232 := [monotonicity #188]: #231
+
−#236 := [trans #232 #234]: #235
+
−#17 := (and up_3 #16)
+
−#18 := (or up_1 #17)
+
−#19 := (not #18)
+
−#20 := (or #19 up_2)
+
−#79 := (iff #20 #78)
+
−#76 := (iff #19 #75)
+
−#73 := (iff #18 up_1)
+
−#68 := (or up_1 false)
+
−#71 := (iff #68 up_1)
+
−#72 := [rewrite]: #71
+
−#69 := (iff #18 #68)
+
−#62 := (iff #17 false)
+
−#67 := [rewrite]: #62
+
−#70 := [monotonicity #67]: #69
+
−#74 := [trans #70 #72]: #73
+
−#77 := [monotonicity #74]: #76
+
−#80 := [monotonicity #77]: #79
+
−#57 := [asserted]: #20
+
−#83 := [mp #57 #80]: #78
+
−#237 := [mp #83 #236]: #75
+
−[mp #237 #247]: false
+
−unsat