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

adapted Function_Lib (cf. b8cdd3d73022);

#2 := false
#5 := 0::int
#8 := 1::int
#143 := (= 1::int 0::int)
#145 := (iff #143 false)
#146 := [rewrite]: #145
decl ?x1!1 :: int
#47 := ?x1!1
#51 := (= ?x1!1 0::int)
decl ?x2!0 :: int
#46 := ?x2!0
#50 := (= ?x2!0 1::int)
#63 := (and #50 #51)
#69 := (= ?x2!0 ?x1!1)
#72 := (not #69)
#66 := (not #63)
#75 := (or #66 #72)
#78 := (not #75)
#48 := (= ?x1!1 ?x2!0)
#49 := (not #48)
#52 := (and #51 #50)
#53 := (not #52)
#54 := (or #53 #49)
#55 := (not #54)
#79 := (iff #55 #78)
#76 := (iff #54 #75)
#73 := (iff #49 #72)
#70 := (iff #48 #69)
#71 := [rewrite]: #70
#74 := [monotonicity #71]: #73
#67 := (iff #53 #66)
#64 := (iff #52 #63)
#65 := [rewrite]: #64
#68 := [monotonicity #65]: #67
#77 := [monotonicity #68 #74]: #76
#80 := [monotonicity #77]: #79
#7 := (:var 0 int)
#4 := (:var 1 int)
#11 := (= #4 #7)
#12 := (not #11)
#9 := (= #7 1::int)
#6 := (= #4 0::int)
#10 := (and #6 #9)
#32 := (not #10)
#33 := (or #32 #12)
#36 := (forall (vars (?x1 int) (?x2 int)) #33)
#39 := (not #36)
#56 := (~ #39 #55)
#57 := [sk]: #56
#13 := (implies #10 #12)
#14 := (forall (vars (?x1 int) (?x2 int)) #13)
#15 := (not #14)
#40 := (iff #15 #39)
#37 := (iff #14 #36)
#34 := (iff #13 #33)
#35 := [rewrite]: #34
#38 := [quant-intro #35]: #37
#41 := [monotonicity #38]: #40
#31 := [asserted]: #15
#44 := [mp #31 #41]: #39
#60 := [mp~ #44 #57]: #55
#61 := [mp #60 #80]: #78
#62 := [not-or-elim #61]: #63
#82 := [and-elim #62]: #51
#141 := (= 1::int ?x1!1)
#83 := [not-or-elim #61]: #69
#139 := (= 1::int ?x2!0)
#81 := [and-elim #62]: #50
#140 := [symm #81]: #139
#142 := [trans #140 #83]: #141
#144 := [trans #142 #82]: #143
[mp #144 #146]: false
unsat