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

merged

#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