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

adopting Sequences

#2 := false
#6 := 1::int
decl uf_3 :: int
#8 := uf_3
#12 := (+ uf_3 1::int)
decl uf_1 :: int
#4 := uf_1
#13 := (* uf_1 #12)
decl uf_2 :: int
#5 := uf_2
#11 := (* uf_1 uf_2)
#14 := (+ #11 #13)
#7 := (+ uf_2 1::int)
#9 := (+ #7 uf_3)
#10 := (* uf_1 #9)
#15 := (= #10 #14)
#16 := (not #15)
#85 := (iff #16 false)
#1 := true
#80 := (not true)
#83 := (iff #80 false)
#84 := [rewrite]: #83
#81 := (iff #16 #80)
#78 := (iff #15 true)
#48 := (* uf_1 uf_3)
#49 := (+ #11 #48)
#50 := (+ uf_1 #49)
#73 := (= #50 #50)
#76 := (iff #73 true)
#77 := [rewrite]: #76
#74 := (iff #15 #73)
#71 := (= #14 #50)
#61 := (+ uf_1 #48)
#66 := (+ #11 #61)
#69 := (= #66 #50)
#70 := [rewrite]: #69
#67 := (= #14 #66)
#64 := (= #13 #61)
#55 := (+ 1::int uf_3)
#58 := (* uf_1 #55)
#62 := (= #58 #61)
#63 := [rewrite]: #62
#59 := (= #13 #58)
#56 := (= #12 #55)
#57 := [rewrite]: #56
#60 := [monotonicity #57]: #59
#65 := [trans #60 #63]: #64
#68 := [monotonicity #65]: #67
#72 := [trans #68 #70]: #71
#53 := (= #10 #50)
#39 := (+ uf_2 uf_3)
#40 := (+ 1::int #39)
#45 := (* uf_1 #40)
#51 := (= #45 #50)
#52 := [rewrite]: #51
#46 := (= #10 #45)
#43 := (= #9 #40)
#33 := (+ 1::int uf_2)
#36 := (+ #33 uf_3)
#41 := (= #36 #40)
#42 := [rewrite]: #41
#37 := (= #9 #36)
#34 := (= #7 #33)
#35 := [rewrite]: #34
#38 := [monotonicity #35]: #37
#44 := [trans #38 #42]: #43
#47 := [monotonicity #44]: #46
#54 := [trans #47 #52]: #53
#75 := [monotonicity #54 #72]: #74
#79 := [trans #75 #77]: #78
#82 := [monotonicity #79]: #81
#86 := [trans #82 #84]: #85
#32 := [asserted]: #16
[mp #32 #86]: false
unsat