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
blanchet@50662
     1
43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
blanchet@53824
     2
#2 := false
blanchet@53824
     3
#10 := 0::Int
blanchet@53824
     4
decl f3 :: Int
blanchet@53824
     5
#7 := f3
blanchet@53824
     6
#12 := (<= f3 0::Int)
blanchet@53824
     7
#54 := (not #12)
blanchet@53824
     8
decl f4 :: Int
blanchet@53824
     9
#8 := f4
blanchet@53824
    10
#13 := (<= f4 0::Int)
blanchet@53824
    11
#9 := (* f3 f4)
blanchet@53824
    12
#11 := (<= #9 0::Int)
blanchet@53824
    13
#37 := (not #11)
blanchet@53824
    14
#44 := (or #37 #12 #13)
blanchet@53824
    15
#47 := (not #44)
blanchet@53824
    16
#14 := (or #12 #13)
blanchet@53824
    17
#15 := (implies #11 #14)
blanchet@53824
    18
#16 := (not #15)
blanchet@53824
    19
#50 := (iff #16 #47)
blanchet@53824
    20
#38 := (or #37 #14)
blanchet@53824
    21
#41 := (not #38)
blanchet@53824
    22
#48 := (iff #41 #47)
blanchet@53824
    23
#45 := (iff #38 #44)
blanchet@53824
    24
#46 := [rewrite]: #45
blanchet@53824
    25
#49 := [monotonicity #46]: #48
blanchet@53824
    26
#42 := (iff #16 #41)
blanchet@53824
    27
#39 := (iff #15 #38)
blanchet@53824
    28
#40 := [rewrite]: #39
blanchet@53824
    29
#43 := [monotonicity #40]: #42
blanchet@53824
    30
#51 := [trans #43 #49]: #50
blanchet@53824
    31
#36 := [asserted]: #16
blanchet@53824
    32
#52 := [mp #36 #51]: #47
blanchet@53824
    33
#55 := [not-or-elim #52]: #54
blanchet@53824
    34
#56 := (not #13)
blanchet@53824
    35
#57 := [not-or-elim #52]: #56
blanchet@53824
    36
#53 := [not-or-elim #52]: #11
blanchet@53824
    37
[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
blanchet@53824
    38
unsat