src/HOL/SMT/Examples/cert/z3_prop_06.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
+
−decl up_3 :: bool
+
−#7 := up_3
+
−#10 := (and up_1 up_3)
+
−decl up_2 :: bool
+
−#5 := up_2
+
−#9 := (and up_3 up_2)
+
−#11 := (or #9 #10)
+
−#12 := (implies up_1 #11)
+
−#13 := (or #12 up_1)
+
−#6 := (and up_1 up_2)
+
−#8 := (or #6 up_3)
+
−#14 := (implies #8 #13)
+
−#15 := (not #14)
+
−#81 := (iff #15 false)
+
−#32 := (and up_2 up_3)
+
−#38 := (or #10 #32)
+
−#46 := (not up_1)
+
−#47 := (or #46 #38)
+
−#55 := (or up_1 #47)
+
−#63 := (not #8)
+
−#64 := (or #63 #55)
+
−#69 := (not #64)
+
−#79 := (iff #69 false)
+
−#1 := true
+
−#74 := (not true)
+
−#77 := (iff #74 false)
+
−#78 := [rewrite]: #77
+
−#75 := (iff #69 #74)
+
−#72 := (iff #64 true)
+
−#73 := [rewrite]: #72
+
−#76 := [monotonicity #73]: #75
+
−#80 := [trans #76 #78]: #79
+
−#70 := (iff #15 #69)
+
−#67 := (iff #14 #64)
+
−#60 := (implies #8 #55)
+
−#65 := (iff #60 #64)
+
−#66 := [rewrite]: #65
+
−#61 := (iff #14 #60)
+
−#58 := (iff #13 #55)
+
−#52 := (or #47 up_1)
+
−#56 := (iff #52 #55)
+
−#57 := [rewrite]: #56
+
−#53 := (iff #13 #52)
+
−#50 := (iff #12 #47)
+
−#43 := (implies up_1 #38)
+
−#48 := (iff #43 #47)
+
−#49 := [rewrite]: #48
+
−#44 := (iff #12 #43)
+
−#41 := (iff #11 #38)
+
−#35 := (or #32 #10)
+
−#39 := (iff #35 #38)
+
−#40 := [rewrite]: #39
+
−#36 := (iff #11 #35)
+
−#33 := (iff #9 #32)
+
−#34 := [rewrite]: #33
+
−#37 := [monotonicity #34]: #36
+
−#42 := [trans #37 #40]: #41
+
−#45 := [monotonicity #42]: #44
+
−#51 := [trans #45 #49]: #50
+
−#54 := [monotonicity #51]: #53
+
−#59 := [trans #54 #57]: #58
+
−#62 := [monotonicity #59]: #61
+
−#68 := [trans #62 #66]: #67
+
−#71 := [monotonicity #68]: #70
+
−#82 := [trans #71 #80]: #81
+
−#31 := [asserted]: #15
+
−[mp #31 #82]: false
+
−unsat