src/HOL/SMT/Examples/cert/z3_linarith_05.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
+
−#5 := 3::int
+
−#6 := 8::int
+
−#7 := (<= 3::int 8::int)
+
−#8 := (ite #7 8::int 3::int)
+
−#4 := 5::int
+
−#9 := (< 5::int #8)
+
−#10 := (not #9)
+
−#50 := (iff #10 false)
+
−#1 := true
+
−#45 := (not true)
+
−#48 := (iff #45 false)
+
−#49 := [rewrite]: #48
+
−#46 := (iff #10 #45)
+
−#43 := (iff #9 true)
+
−#38 := (< 5::int 8::int)
+
−#41 := (iff #38 true)
+
−#42 := [rewrite]: #41
+
−#39 := (iff #9 #38)
+
−#36 := (= #8 8::int)
+
−#31 := (ite true 8::int 3::int)
+
−#34 := (= #31 8::int)
+
−#35 := [rewrite]: #34
+
−#32 := (= #8 #31)
+
−#29 := (iff #7 true)
+
−#30 := [rewrite]: #29
+
−#33 := [monotonicity #30]: #32
+
−#37 := [trans #33 #35]: #36
+
−#40 := [monotonicity #37]: #39
+
−#44 := [trans #40 #42]: #43
+
−#47 := [monotonicity #44]: #46
+
−#51 := [trans #47 #49]: #50
+
−#26 := [asserted]: #10
+
−[mp #26 #51]: false
+
−unsat