src/HOL/SMT_Examples/SMT_Examples.certs
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 56727 75f4fdafb285
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
     2 #2 := false
     3 #10 := 0::Int
     4 decl f3 :: Int
     5 #7 := f3
     6 #12 := (<= f3 0::Int)
     7 #54 := (not #12)
     8 decl f4 :: Int
     9 #8 := f4
    10 #13 := (<= f4 0::Int)
    11 #9 := (* f3 f4)
    12 #11 := (<= #9 0::Int)
    13 #37 := (not #11)
    14 #44 := (or #37 #12 #13)
    15 #47 := (not #44)
    16 #14 := (or #12 #13)
    17 #15 := (implies #11 #14)
    18 #16 := (not #15)
    19 #50 := (iff #16 #47)
    20 #38 := (or #37 #14)
    21 #41 := (not #38)
    22 #48 := (iff #41 #47)
    23 #45 := (iff #38 #44)
    24 #46 := [rewrite]: #45
    25 #49 := [monotonicity #46]: #48
    26 #42 := (iff #16 #41)
    27 #39 := (iff #15 #38)
    28 #40 := [rewrite]: #39
    29 #43 := [monotonicity #40]: #42
    30 #51 := [trans #43 #49]: #50
    31 #36 := [asserted]: #16
    32 #52 := [mp #36 #51]: #47
    33 #55 := [not-or-elim #52]: #54
    34 #56 := (not #13)
    35 #57 := [not-or-elim #52]: #56
    36 #53 := [not-or-elim #52]: #11
    37 [th-lemma arith farkas 1 1 1 #53 #57 #55]: false
    38 unsat