Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT/Examples/cert/z3_linarith_20.proof
author boehmes
Thu, 03 Dec 2009 15:56:06 +0100
changeset 34010 ac78f5cdc430
parent 33446 153a27370a42
permissions -rw-r--r--
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33446
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     1
 
#2 := false
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     2
 
#5 := 0::real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     3
 
decl uf_1 :: real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     4
 
#4 := uf_1
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     5
 
#94 := (<= uf_1 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     6
 
#17 := 2::real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     7
 
#40 := (* 2::real uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     8
 
#102 := (<= #40 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
     9
 
#103 := (>= #40 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    10
 
#105 := (not #103)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    11
 
#104 := (not #102)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    12
 
#106 := (or #104 #105)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    13
 
#107 := (not #106)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    14
 
#88 := (= #40 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    15
 
#108 := (iff #88 #107)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    16
 
#109 := [rewrite]: #108
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    17
 
#16 := 4::real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    18
 
#11 := (- uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    19
 
#10 := (< uf_1 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    20
 
#12 := (ite #10 #11 uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    21
 
#9 := 1::real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    22
 
#13 := (< 1::real #12)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    23
 
#14 := (not #13)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    24
 
#15 := (or #13 #14)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    25
 
#18 := (ite #15 4::real 2::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    26
 
#19 := (* #18 uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    27
 
#8 := (+ uf_1 uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    28
 
#20 := (= #8 #19)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    29
 
#21 := (not #20)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    30
 
#22 := (not #21)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    31
 
#89 := (iff #22 #88)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    32
 
#70 := (* 4::real uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    33
 
#73 := (= #40 #70)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    34
 
#86 := (iff #73 #88)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    35
 
#87 := [rewrite]: #86
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    36
 
#84 := (iff #22 #73)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    37
 
#76 := (not #73)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    38
 
#79 := (not #76)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    39
 
#82 := (iff #79 #73)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    40
 
#83 := [rewrite]: #82
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    41
 
#80 := (iff #22 #79)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    42
 
#77 := (iff #21 #76)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    43
 
#74 := (iff #20 #73)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    44
 
#71 := (= #19 #70)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    45
 
#68 := (= #18 4::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    46
 
#1 := true
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    47
 
#63 := (ite true 4::real 2::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    48
 
#66 := (= #63 4::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    49
 
#67 := [rewrite]: #66
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    50
 
#64 := (= #18 #63)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    51
 
#61 := (iff #15 true)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    52
 
#43 := -1::real
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    53
 
#44 := (* -1::real uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    54
 
#47 := (ite #10 #44 uf_1)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    55
 
#50 := (< 1::real #47)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    56
 
#53 := (not #50)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    57
 
#56 := (or #50 #53)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    58
 
#59 := (iff #56 true)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    59
 
#60 := [rewrite]: #59
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    60
 
#57 := (iff #15 #56)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    61
 
#54 := (iff #14 #53)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    62
 
#51 := (iff #13 #50)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    63
 
#48 := (= #12 #47)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    64
 
#45 := (= #11 #44)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    65
 
#46 := [rewrite]: #45
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    66
 
#49 := [monotonicity #46]: #48
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    67
 
#52 := [monotonicity #49]: #51
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    68
 
#55 := [monotonicity #52]: #54
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    69
 
#58 := [monotonicity #52 #55]: #57
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    70
 
#62 := [trans #58 #60]: #61
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    71
 
#65 := [monotonicity #62]: #64
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    72
 
#69 := [trans #65 #67]: #68
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    73
 
#72 := [monotonicity #69]: #71
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    74
 
#41 := (= #8 #40)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    75
 
#42 := [rewrite]: #41
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    76
 
#75 := [monotonicity #42 #72]: #74
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    77
 
#78 := [monotonicity #75]: #77
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    78
 
#81 := [monotonicity #78]: #80
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    79
 
#85 := [trans #81 #83]: #84
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    80
 
#90 := [trans #85 #87]: #89
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    81
 
#39 := [asserted]: #22
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    82
 
#91 := [mp #39 #90]: #88
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    83
 
#110 := [mp #91 #109]: #107
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    84
 
#111 := [not-or-elim #110]: #102
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    85
 
#127 := (or #94 #104)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    86
 
#128 := [th-lemma]: #127
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    87
 
#129 := [unit-resolution #128 #111]: #94
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    88
 
#92 := (>= uf_1 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    89
 
#112 := [not-or-elim #110]: #103
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    90
 
#130 := (or #92 #105)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    91
 
#131 := [th-lemma]: #130
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    92
 
#132 := [unit-resolution #131 #112]: #92
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    93
 
#114 := (not #94)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    94
 
#113 := (not #92)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    95
 
#115 := (or #113 #114)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    96
 
#95 := (and #92 #94)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    97
 
#98 := (not #95)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    98
 
#124 := (iff #98 #115)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
    99
 
#116 := (not #115)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   100
 
#119 := (not #116)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   101
 
#122 := (iff #119 #115)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   102
 
#123 := [rewrite]: #122
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   103
 
#120 := (iff #98 #119)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   104
 
#117 := (iff #95 #116)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   105
 
#118 := [rewrite]: #117
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   106
 
#121 := [monotonicity #118]: #120
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   107
 
#125 := [trans #121 #123]: #124
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   108
 
#6 := (= uf_1 0::real)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   109
 
#7 := (not #6)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   110
 
#99 := (iff #7 #98)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   111
 
#96 := (iff #6 #95)
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   112
 
#97 := [rewrite]: #96
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   113
 
#100 := [monotonicity #97]: #99
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   114
 
#38 := [asserted]: #7
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   115
 
#101 := [mp #38 #100]: #98
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   116
 
#126 := [mp #101 #125]: #115
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   117
 
[unit-resolution #126 #132 #129]: false
153a27370a42 handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff changeset 
   118
 
unsat
isabelle