author | boehmes |
Tue, 26 Oct 2010 11:46:19 +0200 | |
changeset 40163 | a462d5207aa6 |
parent 37489 | 44e42d392c6e |
child 40333 | 12a06ad29681 |
permissions | -rw-r--r-- |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1 |
19e9a49723add29f06290682aca290aa2ab968ea 238 0 |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
2 |
#2 := false |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
3 |
#48 := 0::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
4 |
decl f19 :: (-> S3 S10 real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
5 |
decl f20 :: S10 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
6 |
#43 := f20 |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
7 |
decl f4 :: S3 |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
8 |
#8 := f4 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
9 |
#58 := (f19 f4 f20) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
10 |
#109 := -1::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
11 |
#153 := (* -1::real #58) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
12 |
decl f5 :: (-> S4 S5 real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
13 |
decl f8 :: S5 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
14 |
#13 := f8 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
15 |
decl f22 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
16 |
#54 := f22 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
17 |
#55 := (f5 f22 f8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
18 |
#154 := (+ #55 #153) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
19 |
#137 := (* -1::real #55) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
20 |
#144 := (+ #137 #58) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
21 |
#188 := (<= #154 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
22 |
#195 := (ite #188 #144 #154) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
23 |
#451 := (* -1::real #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
24 |
#452 := (+ #144 #451) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
25 |
#453 := (<= #452 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
26 |
#435 := (= #144 #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
27 |
decl f21 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
28 |
#45 := f21 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
29 |
#46 := (f5 f21 f8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
30 |
decl f9 :: S3 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
31 |
#17 := f9 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
32 |
#44 := (f19 f9 f20) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
33 |
#120 := (* -1::real #44) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
34 |
#121 := (+ #120 #46) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
35 |
#110 := (* -1::real #46) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
36 |
#111 := (+ #44 #110) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
37 |
#216 := (>= #111 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
38 |
#223 := (ite #216 #111 #121) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
39 |
#447 := (* -1::real #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
40 |
#450 := (+ #121 #447) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
41 |
#454 := (<= #450 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
42 |
#442 := (= #121 #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
43 |
#217 := (not #216) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
44 |
#455 := [hypothesis]: #216 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
45 |
#184 := (+ #44 #153) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
46 |
#185 := (<= #184 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
47 |
#206 := -3::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
48 |
#234 := (* -3::real #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
49 |
#235 := (+ #137 #234) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
50 |
#236 := (+ #46 #235) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
51 |
#237 := (<= #236 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
52 |
#238 := (not #237) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
53 |
#207 := (* -3::real #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
54 |
#208 := (+ #137 #207) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
55 |
#209 := (+ #46 #208) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
56 |
#210 := (<= #209 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
57 |
#211 := (not #210) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
58 |
#249 := (and #185 #211 #238) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
59 |
#65 := (<= #44 #58) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
60 |
#56 := (- #46 #55) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
61 |
#52 := 3::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
62 |
#59 := (- #58 #55) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
63 |
#61 := (- #59) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
64 |
#60 := (< #59 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
65 |
#62 := (ite #60 #61 #59) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
66 |
#63 := (* #62 3::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
67 |
#64 := (< #63 #56) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
68 |
#66 := (and #64 #65) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
69 |
#47 := (- #44 #46) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
70 |
#50 := (- #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
71 |
#49 := (< #47 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
72 |
#51 := (ite #49 #50 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
73 |
#53 := (* #51 3::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
74 |
#57 := (< #53 #56) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
75 |
#67 := (and #57 #66) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
76 |
#254 := (iff #67 #249) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
77 |
#138 := (+ #46 #137) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
78 |
#147 := (< #144 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
79 |
#159 := (ite #147 #154 #144) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
80 |
#165 := (* 3::real #159) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
81 |
#170 := (< #165 #138) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
82 |
#176 := (and #65 #170) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
83 |
#114 := (< #111 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
84 |
#126 := (ite #114 #121 #111) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
85 |
#132 := (* 3::real #126) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
86 |
#141 := (< #132 #138) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
87 |
#181 := (and #141 #176) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
88 |
#252 := (iff #181 #249) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
89 |
#243 := (and #185 #211) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
90 |
#246 := (and #238 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
91 |
#250 := (iff #246 #249) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
92 |
#251 := [rewrite]: #250 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
93 |
#247 := (iff #181 #246) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
94 |
#244 := (iff #176 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
95 |
#214 := (iff #170 #211) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
96 |
#200 := (* 3::real #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
97 |
#203 := (< #200 #138) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
98 |
#212 := (iff #203 #211) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
99 |
#213 := [rewrite]: #212 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
100 |
#204 := (iff #170 #203) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
101 |
#201 := (= #165 #200) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
102 |
#198 := (= #159 #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
103 |
#189 := (not #188) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
104 |
#192 := (ite #189 #154 #144) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
105 |
#196 := (= #192 #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
106 |
#197 := [rewrite]: #196 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
107 |
#193 := (= #159 #192) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
108 |
#190 := (iff #147 #189) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
109 |
#191 := [rewrite]: #190 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
110 |
#194 := [monotonicity #191]: #193 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
111 |
#199 := [trans #194 #197]: #198 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
112 |
#202 := [monotonicity #199]: #201 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
113 |
#205 := [monotonicity #202]: #204 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
114 |
#215 := [trans #205 #213]: #214 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
115 |
#186 := (iff #65 #185) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
116 |
#187 := [rewrite]: #186 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
117 |
#245 := [monotonicity #187 #215]: #244 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
118 |
#241 := (iff #141 #238) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
119 |
#228 := (* 3::real #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
120 |
#231 := (< #228 #138) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
121 |
#239 := (iff #231 #238) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
122 |
#240 := [rewrite]: #239 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
123 |
#232 := (iff #141 #231) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
124 |
#229 := (= #132 #228) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
125 |
#226 := (= #126 #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
126 |
#220 := (ite #217 #121 #111) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
127 |
#224 := (= #220 #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
128 |
#225 := [rewrite]: #224 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
129 |
#221 := (= #126 #220) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
130 |
#218 := (iff #114 #217) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
131 |
#219 := [rewrite]: #218 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
132 |
#222 := [monotonicity #219]: #221 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
133 |
#227 := [trans #222 #225]: #226 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
134 |
#230 := [monotonicity #227]: #229 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
135 |
#233 := [monotonicity #230]: #232 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
136 |
#242 := [trans #233 #240]: #241 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
137 |
#248 := [monotonicity #242 #245]: #247 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
138 |
#253 := [trans #248 #251]: #252 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
139 |
#182 := (iff #67 #181) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
140 |
#179 := (iff #66 #176) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
141 |
#173 := (and #170 #65) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
142 |
#177 := (iff #173 #176) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
143 |
#178 := [rewrite]: #177 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
144 |
#174 := (iff #66 #173) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
145 |
#171 := (iff #64 #170) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
146 |
#139 := (= #56 #138) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
147 |
#140 := [rewrite]: #139 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
148 |
#168 := (= #63 #165) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
149 |
#162 := (* #159 3::real) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
150 |
#166 := (= #162 #165) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
151 |
#167 := [rewrite]: #166 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
152 |
#163 := (= #63 #162) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
153 |
#160 := (= #62 #159) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
154 |
#145 := (= #59 #144) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
155 |
#146 := [rewrite]: #145 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
156 |
#157 := (= #61 #154) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
157 |
#150 := (- #144) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
158 |
#155 := (= #150 #154) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
159 |
#156 := [rewrite]: #155 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
160 |
#151 := (= #61 #150) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
161 |
#152 := [monotonicity #146]: #151 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
162 |
#158 := [trans #152 #156]: #157 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
163 |
#148 := (iff #60 #147) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
164 |
#149 := [monotonicity #146]: #148 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
165 |
#161 := [monotonicity #149 #158 #146]: #160 |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
166 |
#164 := [monotonicity #161]: #163 |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
167 |
#169 := [trans #164 #167]: #168 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
168 |
#172 := [monotonicity #169 #140]: #171 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
169 |
#175 := [monotonicity #172]: #174 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
170 |
#180 := [trans #175 #178]: #179 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
171 |
#142 := (iff #57 #141) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
172 |
#135 := (= #53 #132) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
173 |
#129 := (* #126 3::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
174 |
#133 := (= #129 #132) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
175 |
#134 := [rewrite]: #133 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
176 |
#130 := (= #53 #129) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
177 |
#127 := (= #51 #126) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
178 |
#112 := (= #47 #111) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
179 |
#113 := [rewrite]: #112 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
180 |
#124 := (= #50 #121) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
181 |
#117 := (- #111) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
182 |
#122 := (= #117 #121) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
183 |
#123 := [rewrite]: #122 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
184 |
#118 := (= #50 #117) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
185 |
#119 := [monotonicity #113]: #118 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
186 |
#125 := [trans #119 #123]: #124 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
187 |
#115 := (iff #49 #114) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
188 |
#116 := [monotonicity #113]: #115 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
189 |
#128 := [monotonicity #116 #125 #113]: #127 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
190 |
#131 := [monotonicity #128]: #130 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
191 |
#136 := [trans #131 #134]: #135 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
192 |
#143 := [monotonicity #136 #140]: #142 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
193 |
#183 := [monotonicity #143 #180]: #182 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
194 |
#255 := [trans #183 #253]: #254 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
195 |
#108 := [asserted]: #67 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
196 |
#256 := [mp #108 #255]: #249 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
197 |
#257 := [and-elim #256]: #185 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
198 |
#259 := [and-elim #256]: #238 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
199 |
#448 := (+ #111 #447) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
200 |
#449 := (<= #448 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
201 |
#441 := (= #111 #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
202 |
#443 := (or #217 #441) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
203 |
#444 := [def-axiom]: #443 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
204 |
#467 := [unit-resolution #444 #455]: #441 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
205 |
#468 := (not #441) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
206 |
#469 := (or #468 #449) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
207 |
#470 := [th-lemma]: #469 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
208 |
#471 := [unit-resolution #470 #467]: #449 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
209 |
#463 := (or #189 #217) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
210 |
#456 := [hypothesis]: #188 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
211 |
#258 := [and-elim #256]: #211 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
212 |
#437 := (or #189 #435) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
213 |
#438 := [def-axiom]: #437 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
214 |
#457 := [unit-resolution #438 #456]: #435 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
215 |
#458 := (not #435) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
216 |
#459 := (or #458 #453) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
217 |
#460 := [th-lemma]: #459 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
218 |
#461 := [unit-resolution #460 #457]: #453 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
219 |
#462 := [th-lemma #257 #461 #258 #456 #455]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
220 |
#464 := [lemma #462]: #463 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
221 |
#472 := [unit-resolution #464 #455]: #189 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
222 |
#473 := [th-lemma #472 #471 #259 #257 #455]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
223 |
#474 := [lemma #473]: #217 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
224 |
#445 := (or #216 #442) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
225 |
#446 := [def-axiom]: #445 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
226 |
#475 := [unit-resolution #446 #474]: #442 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
227 |
#476 := (not #442) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
228 |
#477 := (or #476 #454) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
229 |
#478 := [th-lemma]: #477 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
230 |
#479 := [unit-resolution #478 #475]: #454 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
231 |
#481 := (not #185) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
232 |
#480 := (not #454) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
233 |
#482 := (or #188 #480 #237 #481 #216) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
234 |
#483 := [th-lemma]: #482 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
235 |
#484 := [unit-resolution #483 #257 #474 #259 #479]: #188 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
236 |
#485 := [unit-resolution #438 #484]: #435 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
237 |
#486 := [unit-resolution #460 #485]: #453 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
238 |
[th-lemma #479 #259 #257 #474 #258 #486]: false |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
239 |
unsat |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
240 |
96c3a1d2dea133da23272bb1832adcfffc19c650 333 0 |
36900 | 241 |
#2 := false |
242 |
#11 := 0::real |
|
243 |
decl ?v2!1 :: real |
|
244 |
#225 := ?v2!1 |
|
245 |
decl ?v1!2 :: real |
|
246 |
#223 := ?v1!2 |
|
247 |
#45 := -1::real |
|
248 |
#238 := (* -1::real ?v1!2) |
|
249 |
#260 := (+ #238 ?v2!1) |
|
250 |
#240 := (* -1::real ?v2!1) |
|
251 |
#266 := (+ ?v1!2 #240) |
|
252 |
#267 := (>= #266 0::real) |
|
253 |
#274 := (ite #267 #266 #260) |
|
254 |
#277 := (* -1::real #274) |
|
255 |
#74 := -1/3::real |
|
256 |
#233 := (* -1/3::real ?v2!1) |
|
257 |
#280 := (+ #233 #277) |
|
258 |
decl ?v3!0 :: real |
|
259 |
#224 := ?v3!0 |
|
260 |
#72 := 1/3::real |
|
261 |
#235 := (* 1/3::real ?v3!0) |
|
262 |
#283 := (+ #235 #280) |
|
263 |
#286 := (<= #283 0::real) |
|
264 |
#302 := (not #286) |
|
265 |
decl ?v0!3 :: real |
|
266 |
#221 := ?v0!3 |
|
267 |
#248 := (+ ?v0!3 #238) |
|
268 |
#249 := (<= #248 0::real) |
|
269 |
#250 := (not #249) |
|
270 |
#226 := (* -1::real ?v0!3) |
|
271 |
#227 := (+ #226 ?v3!0) |
|
272 |
#228 := (* -1::real ?v3!0) |
|
273 |
#229 := (+ ?v0!3 #228) |
|
274 |
#230 := (>= #229 0::real) |
|
275 |
#231 := (ite #230 #229 #227) |
|
276 |
#232 := (* -1::real #231) |
|
277 |
#234 := (+ #233 #232) |
|
278 |
#236 := (+ #235 #234) |
|
279 |
#237 := (<= #236 0::real) |
|
280 |
#292 := (or #237 #250 #286) |
|
281 |
#297 := (not #292) |
|
282 |
#239 := (+ ?v2!1 #238) |
|
283 |
#241 := (+ #240 ?v1!2) |
|
284 |
#242 := (<= #239 0::real) |
|
285 |
#243 := (ite #242 #241 #239) |
|
286 |
#244 := (* -1::real #243) |
|
287 |
#245 := (+ #233 #244) |
|
288 |
#246 := (+ #235 #245) |
|
289 |
#247 := (<= #246 0::real) |
|
290 |
#251 := (or #250 #247 #237) |
|
291 |
#252 := (not #251) |
|
292 |
#298 := (iff #252 #297) |
|
293 |
#295 := (iff #251 #292) |
|
294 |
#289 := (or #250 #286 #237) |
|
295 |
#293 := (iff #289 #292) |
|
296 |
#294 := [rewrite]: #293 |
|
297 |
#290 := (iff #251 #289) |
|
298 |
#287 := (iff #247 #286) |
|
299 |
#284 := (= #246 #283) |
|
300 |
#281 := (= #245 #280) |
|
301 |
#278 := (= #244 #277) |
|
302 |
#275 := (= #243 #274) |
|
303 |
#261 := (= #239 #260) |
|
304 |
#262 := [rewrite]: #261 |
|
305 |
#272 := (= #241 #266) |
|
306 |
#273 := [rewrite]: #272 |
|
307 |
#270 := (iff #242 #267) |
|
308 |
#263 := (<= #260 0::real) |
|
309 |
#268 := (iff #263 #267) |
|
310 |
#269 := [rewrite]: #268 |
|
311 |
#264 := (iff #242 #263) |
|
312 |
#265 := [monotonicity #262]: #264 |
|
313 |
#271 := [trans #265 #269]: #270 |
|
314 |
#276 := [monotonicity #271 #273 #262]: #275 |
|
315 |
#279 := [monotonicity #276]: #278 |
|
316 |
#282 := [monotonicity #279]: #281 |
|
317 |
#285 := [monotonicity #282]: #284 |
|
318 |
#288 := [monotonicity #285]: #287 |
|
319 |
#291 := [monotonicity #288]: #290 |
|
320 |
#296 := [trans #291 #294]: #295 |
|
321 |
#299 := [monotonicity #296]: #298 |
|
322 |
#9 := (:var 0 real) |
|
323 |
#8 := (:var 3 real) |
|
324 |
#56 := (* -1::real #8) |
|
325 |
#57 := (+ #56 #9) |
|
326 |
#46 := (* -1::real #9) |
|
327 |
#47 := (+ #8 #46) |
|
328 |
#170 := (>= #47 0::real) |
|
329 |
#177 := (ite #170 #47 #57) |
|
330 |
#185 := (* -1::real #177) |
|
331 |
#15 := (:var 1 real) |
|
332 |
#75 := (* -1/3::real #15) |
|
333 |
#186 := (+ #75 #185) |
|
334 |
#73 := (* 1/3::real #9) |
|
335 |
#187 := (+ #73 #186) |
|
336 |
#188 := (<= #187 0::real) |
|
337 |
#20 := (:var 2 real) |
|
338 |
#93 := (* -1::real #20) |
|
339 |
#94 := (+ #15 #93) |
|
340 |
#65 := (* -1::real #15) |
|
341 |
#84 := (+ #65 #20) |
|
342 |
#139 := (<= #94 0::real) |
|
343 |
#146 := (ite #139 #84 #94) |
|
344 |
#154 := (* -1::real #146) |
|
345 |
#155 := (+ #75 #154) |
|
346 |
#156 := (+ #73 #155) |
|
347 |
#157 := (<= #156 0::real) |
|
348 |
#132 := (+ #8 #93) |
|
349 |
#133 := (<= #132 0::real) |
|
350 |
#136 := (not #133) |
|
351 |
#207 := (or #136 #157 #188) |
|
352 |
#212 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #207) |
|
353 |
#215 := (not #212) |
|
354 |
#253 := (~ #215 #252) |
|
355 |
#254 := [sk]: #253 |
|
356 |
#26 := (<= #8 #20) |
|
357 |
#27 := (implies #26 false) |
|
358 |
#17 := 3::real |
|
359 |
#16 := (- #9 #15) |
|
360 |
#18 := (/ #16 3::real) |
|
361 |
#21 := (- #20 #15) |
|
362 |
#23 := (- #21) |
|
363 |
#22 := (< #21 0::real) |
|
364 |
#24 := (ite #22 #23 #21) |
|
365 |
#25 := (< #24 #18) |
|
366 |
#28 := (implies #25 #27) |
|
367 |
#10 := (- #8 #9) |
|
368 |
#13 := (- #10) |
|
369 |
#12 := (< #10 0::real) |
|
370 |
#14 := (ite #12 #13 #10) |
|
371 |
#19 := (< #14 #18) |
|
372 |
#29 := (implies #19 #28) |
|
373 |
#30 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #29) |
|
374 |
#31 := (not #30) |
|
375 |
#218 := (iff #31 #215) |
|
376 |
#76 := (+ #73 #75) |
|
377 |
#87 := (< #84 0::real) |
|
378 |
#99 := (ite #87 #94 #84) |
|
379 |
#102 := (< #99 #76) |
|
380 |
#111 := (not #102) |
|
381 |
#105 := (not #26) |
|
382 |
#112 := (or #105 #111) |
|
383 |
#50 := (< #47 0::real) |
|
384 |
#62 := (ite #50 #57 #47) |
|
385 |
#81 := (< #62 #76) |
|
386 |
#120 := (not #81) |
|
387 |
#121 := (or #120 #112) |
|
388 |
#126 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #121) |
|
389 |
#129 := (not #126) |
|
390 |
#216 := (iff #129 #215) |
|
391 |
#213 := (iff #126 #212) |
|
392 |
#210 := (iff #121 #207) |
|
393 |
#201 := (or #136 #157) |
|
394 |
#204 := (or #188 #201) |
|
395 |
#208 := (iff #204 #207) |
|
396 |
#209 := [rewrite]: #208 |
|
397 |
#205 := (iff #121 #204) |
|
398 |
#202 := (iff #112 #201) |
|
399 |
#168 := (iff #111 #157) |
|
400 |
#158 := (not #157) |
|
401 |
#163 := (not #158) |
|
402 |
#166 := (iff #163 #157) |
|
403 |
#167 := [rewrite]: #166 |
|
404 |
#164 := (iff #111 #163) |
|
405 |
#161 := (iff #102 #158) |
|
406 |
#151 := (< #146 #76) |
|
407 |
#159 := (iff #151 #158) |
|
408 |
#160 := [rewrite]: #159 |
|
409 |
#152 := (iff #102 #151) |
|
410 |
#149 := (= #99 #146) |
|
411 |
#140 := (not #139) |
|
412 |
#143 := (ite #140 #94 #84) |
|
413 |
#147 := (= #143 #146) |
|
414 |
#148 := [rewrite]: #147 |
|
415 |
#144 := (= #99 #143) |
|
416 |
#141 := (iff #87 #140) |
|
417 |
#142 := [rewrite]: #141 |
|
418 |
#145 := [monotonicity #142]: #144 |
|
419 |
#150 := [trans #145 #148]: #149 |
|
420 |
#153 := [monotonicity #150]: #152 |
|
421 |
#162 := [trans #153 #160]: #161 |
|
422 |
#165 := [monotonicity #162]: #164 |
|
423 |
#169 := [trans #165 #167]: #168 |
|
424 |
#137 := (iff #105 #136) |
|
425 |
#134 := (iff #26 #133) |
|
426 |
#135 := [rewrite]: #134 |
|
427 |
#138 := [monotonicity #135]: #137 |
|
428 |
#203 := [monotonicity #138 #169]: #202 |
|
429 |
#199 := (iff #120 #188) |
|
430 |
#189 := (not #188) |
|
431 |
#194 := (not #189) |
|
432 |
#197 := (iff #194 #188) |
|
433 |
#198 := [rewrite]: #197 |
|
434 |
#195 := (iff #120 #194) |
|
435 |
#192 := (iff #81 #189) |
|
436 |
#182 := (< #177 #76) |
|
437 |
#190 := (iff #182 #189) |
|
438 |
#191 := [rewrite]: #190 |
|
439 |
#183 := (iff #81 #182) |
|
440 |
#180 := (= #62 #177) |
|
441 |
#171 := (not #170) |
|
442 |
#174 := (ite #171 #57 #47) |
|
443 |
#178 := (= #174 #177) |
|
444 |
#179 := [rewrite]: #178 |
|
445 |
#175 := (= #62 #174) |
|
446 |
#172 := (iff #50 #171) |
|
447 |
#173 := [rewrite]: #172 |
|
448 |
#176 := [monotonicity #173]: #175 |
|
449 |
#181 := [trans #176 #179]: #180 |
|
450 |
#184 := [monotonicity #181]: #183 |
|
451 |
#193 := [trans #184 #191]: #192 |
|
452 |
#196 := [monotonicity #193]: #195 |
|
453 |
#200 := [trans #196 #198]: #199 |
|
454 |
#206 := [monotonicity #200 #203]: #205 |
|
455 |
#211 := [trans #206 #209]: #210 |
|
456 |
#214 := [quant-intro #211]: #213 |
|
457 |
#217 := [monotonicity #214]: #216 |
|
458 |
#130 := (iff #31 #129) |
|
459 |
#127 := (iff #30 #126) |
|
460 |
#124 := (iff #29 #121) |
|
461 |
#117 := (implies #81 #112) |
|
462 |
#122 := (iff #117 #121) |
|
463 |
#123 := [rewrite]: #122 |
|
464 |
#118 := (iff #29 #117) |
|
465 |
#115 := (iff #28 #112) |
|
466 |
#108 := (implies #102 #105) |
|
467 |
#113 := (iff #108 #112) |
|
468 |
#114 := [rewrite]: #113 |
|
469 |
#109 := (iff #28 #108) |
|
470 |
#106 := (iff #27 #105) |
|
471 |
#107 := [rewrite]: #106 |
|
472 |
#103 := (iff #25 #102) |
|
473 |
#79 := (= #18 #76) |
|
474 |
#66 := (+ #9 #65) |
|
475 |
#69 := (/ #66 3::real) |
|
476 |
#77 := (= #69 #76) |
|
477 |
#78 := [rewrite]: #77 |
|
478 |
#70 := (= #18 #69) |
|
479 |
#67 := (= #16 #66) |
|
480 |
#68 := [rewrite]: #67 |
|
481 |
#71 := [monotonicity #68]: #70 |
|
482 |
#80 := [trans #71 #78]: #79 |
|
483 |
#100 := (= #24 #99) |
|
484 |
#85 := (= #21 #84) |
|
485 |
#86 := [rewrite]: #85 |
|
486 |
#97 := (= #23 #94) |
|
487 |
#90 := (- #84) |
|
488 |
#95 := (= #90 #94) |
|
489 |
#96 := [rewrite]: #95 |
|
490 |
#91 := (= #23 #90) |
|
491 |
#92 := [monotonicity #86]: #91 |
|
492 |
#98 := [trans #92 #96]: #97 |
|
493 |
#88 := (iff #22 #87) |
|
494 |
#89 := [monotonicity #86]: #88 |
|
495 |
#101 := [monotonicity #89 #98 #86]: #100 |
|
496 |
#104 := [monotonicity #101 #80]: #103 |
|
497 |
#110 := [monotonicity #104 #107]: #109 |
|
498 |
#116 := [trans #110 #114]: #115 |
|
499 |
#82 := (iff #19 #81) |
|
500 |
#63 := (= #14 #62) |
|
501 |
#48 := (= #10 #47) |
|
502 |
#49 := [rewrite]: #48 |
|
503 |
#60 := (= #13 #57) |
|
504 |
#53 := (- #47) |
|
505 |
#58 := (= #53 #57) |
|
506 |
#59 := [rewrite]: #58 |
|
507 |
#54 := (= #13 #53) |
|
508 |
#55 := [monotonicity #49]: #54 |
|
509 |
#61 := [trans #55 #59]: #60 |
|
510 |
#51 := (iff #12 #50) |
|
511 |
#52 := [monotonicity #49]: #51 |
|
512 |
#64 := [monotonicity #52 #61 #49]: #63 |
|
513 |
#83 := [monotonicity #64 #80]: #82 |
|
514 |
#119 := [monotonicity #83 #116]: #118 |
|
515 |
#125 := [trans #119 #123]: #124 |
|
516 |
#128 := [quant-intro #125]: #127 |
|
517 |
#131 := [monotonicity #128]: #130 |
|
518 |
#219 := [trans #131 #217]: #218 |
|
519 |
#44 := [asserted]: #31 |
|
520 |
#220 := [mp #44 #219]: #215 |
|
521 |
#257 := [mp~ #220 #254]: #252 |
|
522 |
#258 := [mp #257 #299]: #297 |
|
523 |
#303 := [not-or-elim #258]: #302 |
|
524 |
#301 := [not-or-elim #258]: #249 |
|
525 |
#259 := (not #237) |
|
526 |
#300 := [not-or-elim #258]: #259 |
|
527 |
#376 := (+ #227 #232) |
|
528 |
#377 := (<= #376 0::real) |
|
529 |
#360 := (= #227 #231) |
|
530 |
#361 := (not #230) |
|
531 |
#368 := (not #267) |
|
532 |
#379 := [hypothesis]: #368 |
|
533 |
#387 := (or #361 #267) |
|
534 |
#373 := (+ #260 #277) |
|
535 |
#374 := (<= #373 0::real) |
|
536 |
#367 := (= #260 #274) |
|
537 |
#371 := (or #267 #367) |
|
538 |
#372 := [def-axiom]: #371 |
|
539 |
#380 := [unit-resolution #372 #379]: #367 |
|
540 |
#381 := (not #367) |
|
541 |
#382 := (or #381 #374) |
|
542 |
#383 := [th-lemma]: #382 |
|
543 |
#384 := [unit-resolution #383 #380]: #374 |
|
544 |
#385 := [hypothesis]: #230 |
|
545 |
#386 := [th-lemma #385 #384 #303 #379 #301]: false |
|
546 |
#388 := [lemma #386]: #387 |
|
547 |
#389 := [unit-resolution #388 #379]: #361 |
|
548 |
#364 := (or #230 #360) |
|
549 |
#365 := [def-axiom]: #364 |
|
550 |
#390 := [unit-resolution #365 #389]: #360 |
|
551 |
#391 := (not #360) |
|
552 |
#392 := (or #391 #377) |
|
553 |
#393 := [th-lemma]: #392 |
|
554 |
#394 := [unit-resolution #393 #390]: #377 |
|
555 |
#395 := [th-lemma #384 #303 #379 #394 #300 #301]: false |
|
556 |
#396 := [lemma #395]: #267 |
|
557 |
#399 := [hypothesis]: #361 |
|
558 |
#400 := [unit-resolution #365 #399]: #360 |
|
559 |
#401 := [unit-resolution #393 #400]: #377 |
|
560 |
#375 := (+ #266 #277) |
|
561 |
#378 := (<= #375 0::real) |
|
562 |
#366 := (= #266 #274) |
|
563 |
#369 := (or #368 #366) |
|
564 |
#370 := [def-axiom]: #369 |
|
565 |
#402 := [unit-resolution #370 #396]: #366 |
|
566 |
#403 := (not #366) |
|
567 |
#404 := (or #403 #378) |
|
568 |
#405 := [th-lemma]: #404 |
|
569 |
#406 := [unit-resolution #405 #402]: #378 |
|
570 |
#407 := [th-lemma #406 #301 #401 #300 #399 #303]: false |
|
571 |
#408 := [lemma #407]: #230 |
|
572 |
[th-lemma #406 #301 #408 #396 #303]: false |
|
573 |
unsat |
|
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
574 |
d083434592d4f729dd1c100279aa204b663fa35c 57 0 |
36900 | 575 |
#2 := false |
576 |
decl f13 :: (-> S4 S4 S5) |
|
577 |
#44 := (:var 0 S4) |
|
578 |
#43 := (:var 1 S4) |
|
579 |
#45 := (f13 #43 #44) |
|
580 |
#252 := (pattern #45) |
|
581 |
#39 := 0::real |
|
582 |
decl f12 :: (-> S5 real) |
|
583 |
#46 := (f12 #45) |
|
584 |
#133 := (>= #46 0::real) |
|
585 |
#253 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #252) #133) |
|
586 |
#135 := (forall (vars (?v0 S4) (?v1 S4)) #133) |
|
587 |
#256 := (iff #135 #253) |
|
588 |
#254 := (iff #133 #133) |
|
589 |
#255 := [refl]: #254 |
|
590 |
#257 := [quant-intro #255]: #256 |
|
591 |
#150 := (~ #135 #135) |
|
592 |
#139 := (~ #133 #133) |
|
593 |
#130 := [refl]: #139 |
|
594 |
#151 := [nnf-pos #130]: #150 |
|
595 |
#47 := (<= 0::real #46) |
|
596 |
#48 := (forall (vars (?v0 S4) (?v1 S4)) #47) |
|
597 |
#136 := (iff #48 #135) |
|
598 |
#132 := (iff #47 #133) |
|
599 |
#134 := [rewrite]: #132 |
|
600 |
#137 := [quant-intro #134]: #136 |
|
601 |
#129 := [asserted]: #48 |
|
602 |
#138 := [mp #129 #137]: #135 |
|
603 |
#152 := [mp~ #138 #151]: #135 |
|
604 |
#258 := [mp #152 #257]: #253 |
|
605 |
decl f14 :: (-> S3 S4) |
|
606 |
decl f4 :: S3 |
|
607 |
#8 := f4 |
|
608 |
#36 := (f14 f4) |
|
609 |
decl f10 :: S3 |
|
610 |
#24 := f10 |
|
611 |
#35 := (f14 f10) |
|
612 |
#37 := (f13 #35 #36) |
|
613 |
#38 := (f12 #37) |
|
614 |
#259 := (>= #38 0::real) |
|
615 |
#261 := (not #259) |
|
616 |
#41 := (= #38 0::real) |
|
617 |
#42 := (not #41) |
|
618 |
#128 := [asserted]: #42 |
|
619 |
#267 := (or #41 #261) |
|
620 |
#40 := (<= #38 0::real) |
|
621 |
#127 := [asserted]: #40 |
|
622 |
#260 := (not #40) |
|
623 |
#265 := (or #41 #260 #261) |
|
624 |
#266 := [th-lemma]: #265 |
|
625 |
#268 := [unit-resolution #266 #127]: #267 |
|
626 |
#269 := [unit-resolution #268 #128]: #261 |
|
627 |
#262 := (not #253) |
|
628 |
#263 := (or #262 #259) |
|
629 |
#264 := [quant-inst]: #263 |
|
630 |
[unit-resolution #264 #269 #258]: false |
|
631 |
unsat |
|
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
632 |
93a3d21a7f84dc839f14b9a0cfcafdfff6c6b0f1 318 0 |
36900 | 633 |
#2 := false |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
634 |
#25 := 0::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
635 |
decl f8 :: (-> S4 S2 real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
636 |
decl f11 :: S2 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
637 |
#40 := f11 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
638 |
decl f9 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
639 |
#32 := f9 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
640 |
#47 := (f8 f9 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
641 |
decl f12 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
642 |
#44 := f12 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
643 |
#45 := (f8 f12 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
644 |
#192 := -1::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
645 |
#232 := (* -1::real #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
646 |
#233 := (+ #232 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
647 |
decl f5 :: real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
648 |
#26 := f5 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
649 |
#268 := (* -1::real #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
650 |
#271 := (+ #45 #268) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
651 |
#274 := (+ f5 #271) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
652 |
#275 := (<= #274 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
653 |
#278 := (ite #275 f5 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
654 |
#593 := (* -1::real #278) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
655 |
#594 := (+ f5 #593) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
656 |
#595 := (<= #594 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
657 |
#603 := (not #595) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
658 |
#223 := 1/2::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
659 |
#281 := (* 1/2::real #278) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
660 |
#457 := (<= #281 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
661 |
#292 := (= #281 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
662 |
#306 := (<= #271 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
663 |
decl f10 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
664 |
#34 := f10 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
665 |
#43 := (f8 f10 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
666 |
#302 := (+ #43 #232) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
667 |
#303 := (<= #302 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
668 |
#309 := (and #303 #306) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
669 |
#13 := 0::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
670 |
decl f4 :: (-> S2 int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
671 |
#41 := (f4 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
672 |
#178 := -1::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
673 |
#213 := (* -1::int #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
674 |
decl f6 :: (-> S3 S2) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
675 |
decl f7 :: S3 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
676 |
#28 := f7 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
677 |
#29 := (f6 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
678 |
#30 := (f4 #29) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
679 |
#214 := (+ #30 #213) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
680 |
#215 := (<= #214 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
681 |
#312 := (or #215 #309) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
682 |
#225 := (* 1/2::real #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
683 |
#272 := (+ #232 #225) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
684 |
#224 := (* 1/2::real #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
685 |
#273 := (+ #224 #272) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
686 |
#270 := (>= #273 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
687 |
#321 := (and #270 #292 #312) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
688 |
#52 := 2::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
689 |
#55 := (- #47 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
690 |
#56 := (<= f5 #55) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
691 |
#57 := (ite #56 f5 #55) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
692 |
#58 := (/ #57 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
693 |
#59 := (+ #45 #58) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
694 |
#60 := (= #59 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
695 |
#51 := (+ #43 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
696 |
#53 := (/ #51 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
697 |
#54 := (<= #45 #53) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
698 |
#61 := (and #54 #60) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
699 |
#48 := (<= #45 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
700 |
#46 := (<= #43 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
701 |
#49 := (and #46 #48) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
702 |
#42 := (< #41 #30) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
703 |
#50 := (implies #42 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
704 |
#62 := (and #50 #61) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
705 |
#326 := (iff #62 #321) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
706 |
#236 := (<= f5 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
707 |
#239 := (ite #236 f5 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
708 |
#245 := (* 1/2::real #239) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
709 |
#250 := (+ #45 #245) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
710 |
#256 := (= #45 #250) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
711 |
#226 := (+ #224 #225) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
712 |
#229 := (<= #45 #226) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
713 |
#261 := (and #229 #256) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
714 |
#212 := (not #42) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
715 |
#220 := (or #212 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
716 |
#264 := (and #220 #261) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
717 |
#324 := (iff #264 #321) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
718 |
#315 := (and #270 #292) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
719 |
#318 := (and #312 #315) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
720 |
#322 := (iff #318 #321) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
721 |
#323 := [rewrite]: #322 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
722 |
#319 := (iff #264 #318) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
723 |
#316 := (iff #261 #315) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
724 |
#293 := (iff #256 #292) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
725 |
#284 := (+ #45 #281) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
726 |
#287 := (= #45 #284) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
727 |
#290 := (iff #287 #292) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
728 |
#291 := [rewrite]: #290 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
729 |
#288 := (iff #256 #287) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
730 |
#285 := (= #250 #284) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
731 |
#282 := (= #245 #281) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
732 |
#279 := (= #239 #278) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
733 |
#276 := (iff #236 #275) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
734 |
#277 := [rewrite]: #276 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
735 |
#280 := [monotonicity #277]: #279 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
736 |
#283 := [monotonicity #280]: #282 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
737 |
#286 := [monotonicity #283]: #285 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
738 |
#289 := [monotonicity #286]: #288 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
739 |
#294 := [trans #289 #291]: #293 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
740 |
#267 := (iff #229 #270) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
741 |
#269 := [rewrite]: #267 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
742 |
#317 := [monotonicity #269 #294]: #316 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
743 |
#313 := (iff #220 #312) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
744 |
#310 := (iff #49 #309) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
745 |
#307 := (iff #48 #306) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
746 |
#308 := [rewrite]: #307 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
747 |
#304 := (iff #46 #303) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
748 |
#305 := [rewrite]: #304 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
749 |
#311 := [monotonicity #305 #308]: #310 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
750 |
#300 := (iff #212 #215) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
751 |
#216 := (not #215) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
752 |
#295 := (not #216) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
753 |
#298 := (iff #295 #215) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
754 |
#299 := [rewrite]: #298 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
755 |
#296 := (iff #212 #295) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
756 |
#217 := (iff #42 #216) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
757 |
#218 := [rewrite]: #217 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
758 |
#297 := [monotonicity #218]: #296 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
759 |
#301 := [trans #297 #299]: #300 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
760 |
#314 := [monotonicity #301 #311]: #313 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
761 |
#320 := [monotonicity #314 #317]: #319 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
762 |
#325 := [trans #320 #323]: #324 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
763 |
#265 := (iff #62 #264) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
764 |
#262 := (iff #61 #261) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
765 |
#259 := (iff #60 #256) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
766 |
#253 := (= #250 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
767 |
#257 := (iff #253 #256) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
768 |
#258 := [rewrite]: #257 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
769 |
#254 := (iff #60 #253) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
770 |
#251 := (= #59 #250) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
771 |
#248 := (= #58 #245) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
772 |
#242 := (/ #239 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
773 |
#246 := (= #242 #245) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
774 |
#247 := [rewrite]: #246 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
775 |
#243 := (= #58 #242) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
776 |
#240 := (= #57 #239) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
777 |
#234 := (= #55 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
778 |
#235 := [rewrite]: #234 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
779 |
#237 := (iff #56 #236) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
780 |
#238 := [monotonicity #235]: #237 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
781 |
#241 := [monotonicity #238 #235]: #240 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
782 |
#244 := [monotonicity #241]: #243 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
783 |
#249 := [trans #244 #247]: #248 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
784 |
#252 := [monotonicity #249]: #251 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
785 |
#255 := [monotonicity #252]: #254 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
786 |
#260 := [trans #255 #258]: #259 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
787 |
#230 := (iff #54 #229) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
788 |
#227 := (= #53 #226) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
789 |
#228 := [rewrite]: #227 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
790 |
#231 := [monotonicity #228]: #230 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
791 |
#263 := [monotonicity #231 #260]: #262 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
792 |
#221 := (iff #50 #220) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
793 |
#222 := [rewrite]: #221 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
794 |
#266 := [monotonicity #222 #263]: #265 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
795 |
#327 := [trans #266 #325]: #326 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
796 |
#211 := [asserted]: #62 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
797 |
#328 := [mp #211 #327]: #321 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
798 |
#330 := [and-elim #328]: #292 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
799 |
#597 := (not #292) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
800 |
#598 := (or #597 #457) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
801 |
#599 := [th-lemma]: #598 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
802 |
#600 := [unit-resolution #599 #330]: #457 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
803 |
#601 := [hypothesis]: #595 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
804 |
#167 := (<= f5 0::real) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
37156
diff
changeset
|
805 |
#168 := (not #167) |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
806 |
#27 := (< 0::real f5) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
807 |
#169 := (iff #27 #168) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
808 |
#170 := [rewrite]: #169 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
809 |
#164 := [asserted]: #27 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
810 |
#171 := [mp #164 #170]: #168 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
811 |
#602 := [th-lemma #171 #601 #600]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
812 |
#604 := [lemma #602]: #603 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
813 |
#450 := (= f5 #278) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
814 |
#451 := (= #233 #278) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
815 |
#613 := (not #451) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
816 |
#596 := (+ #233 #593) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
817 |
#605 := (<= #596 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
818 |
#610 := (not #605) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
819 |
#532 := (+ #43 #268) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
820 |
#533 := (>= #532 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
821 |
#538 := (not #533) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
822 |
#210 := [asserted]: #42 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
823 |
#219 := [mp #210 #218]: #216 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
824 |
#8 := (:var 0 S2) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
825 |
#35 := (f8 f10 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
826 |
#443 := (pattern #35) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
827 |
#33 := (f8 f9 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
828 |
#442 := (pattern #33) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
829 |
#9 := (f4 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
830 |
#422 := (pattern #9) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
831 |
#193 := (* -1::real #35) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
832 |
#194 := (+ #33 #193) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
833 |
#195 := (<= #194 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
834 |
#198 := (not #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
835 |
#181 := (* -1::int #30) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
836 |
#182 := (+ #9 #181) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
837 |
#180 := (>= #182 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
838 |
#201 := (or #180 #198) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
839 |
#444 := (forall (vars (?v0 S2)) (:pat #422 #442 #443) #201) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
840 |
#204 := (forall (vars (?v0 S2)) #201) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
841 |
#447 := (iff #204 #444) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
842 |
#445 := (iff #201 #201) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
843 |
#446 := [refl]: #445 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
844 |
#448 := [quant-intro #446]: #447 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
845 |
#362 := (~ #204 #204) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
846 |
#332 := (~ #201 #201) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
847 |
#361 := [refl]: #332 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
848 |
#363 := [nnf-pos #361]: #362 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
849 |
#36 := (<= #33 #35) |
36900 | 850 |
#37 := (not #36) |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
851 |
#31 := (< #9 #30) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
852 |
#38 := (implies #31 #37) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
853 |
#39 := (forall (vars (?v0 S2)) #38) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
854 |
#207 := (iff #39 #204) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
855 |
#166 := (not #31) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
856 |
#172 := (or #166 #37) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
857 |
#175 := (forall (vars (?v0 S2)) #172) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
858 |
#205 := (iff #175 #204) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
859 |
#202 := (iff #172 #201) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
860 |
#199 := (iff #37 #198) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
861 |
#196 := (iff #36 #195) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
862 |
#197 := [rewrite]: #196 |
36900 | 863 |
#200 := [monotonicity #197]: #199 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
864 |
#190 := (iff #166 #180) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
865 |
#179 := (not #180) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
866 |
#185 := (not #179) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
867 |
#188 := (iff #185 #180) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
868 |
#189 := [rewrite]: #188 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
869 |
#186 := (iff #166 #185) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
870 |
#183 := (iff #31 #179) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
871 |
#184 := [rewrite]: #183 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
872 |
#187 := [monotonicity #184]: #186 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
873 |
#191 := [trans #187 #189]: #190 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
874 |
#203 := [monotonicity #191 #200]: #202 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
875 |
#206 := [quant-intro #203]: #205 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
876 |
#176 := (iff #39 #175) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
877 |
#173 := (iff #38 #172) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
878 |
#174 := [rewrite]: #173 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
879 |
#177 := [quant-intro #174]: #176 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
880 |
#208 := [trans #177 #206]: #207 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
881 |
#165 := [asserted]: #39 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
882 |
#209 := [mp #165 #208]: #204 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
883 |
#364 := [mp~ #209 #363]: #204 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
884 |
#449 := [mp #364 #448]: #444 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
885 |
#544 := (not #444) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
886 |
#545 := (or #544 #215 #538) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
887 |
#507 := (* -1::real #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
888 |
#508 := (+ #47 #507) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
889 |
#511 := (<= #508 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
890 |
#512 := (not #511) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
891 |
#513 := (+ #41 #181) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
892 |
#514 := (>= #513 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
893 |
#515 := (or #514 #512) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
894 |
#546 := (or #544 #515) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
895 |
#553 := (iff #546 #545) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
896 |
#541 := (or #215 #538) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
897 |
#548 := (or #544 #541) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
898 |
#551 := (iff #548 #545) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
899 |
#552 := [rewrite]: #551 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
900 |
#549 := (iff #546 #548) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
901 |
#542 := (iff #515 #541) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
902 |
#539 := (iff #512 #538) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
903 |
#536 := (iff #511 #533) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
904 |
#526 := (+ #507 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
905 |
#529 := (<= #526 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
906 |
#534 := (iff #529 #533) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
907 |
#535 := [rewrite]: #534 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
908 |
#530 := (iff #511 #529) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
909 |
#527 := (= #508 #526) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
910 |
#528 := [rewrite]: #527 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
911 |
#531 := [monotonicity #528]: #530 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
912 |
#537 := [trans #531 #535]: #536 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
913 |
#540 := [monotonicity #537]: #539 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
914 |
#524 := (iff #514 #215) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
915 |
#516 := (+ #181 #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
916 |
#519 := (>= #516 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
917 |
#522 := (iff #519 #215) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
918 |
#523 := [rewrite]: #522 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
919 |
#520 := (iff #514 #519) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
920 |
#517 := (= #513 #516) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
921 |
#518 := [rewrite]: #517 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
922 |
#521 := [monotonicity #518]: #520 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
923 |
#525 := [trans #521 #523]: #524 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
924 |
#543 := [monotonicity #525 #540]: #542 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
925 |
#550 := [monotonicity #543]: #549 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
926 |
#554 := [trans #550 #552]: #553 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
927 |
#547 := [quant-inst]: #546 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
928 |
#555 := [mp #547 #554]: #545 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
929 |
#607 := [unit-resolution #555 #449 #219]: #538 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
930 |
#329 := [and-elim #328]: #270 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
931 |
#608 := [hypothesis]: #605 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
932 |
#609 := [th-lemma #608 #329 #607 #600]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
933 |
#611 := [lemma #609]: #610 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
934 |
#612 := [hypothesis]: #451 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
935 |
#614 := (or #613 #605) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
936 |
#615 := [th-lemma]: #614 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
937 |
#616 := [unit-resolution #615 #612 #611]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
938 |
#617 := [lemma #616]: #613 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
939 |
#455 := (or #275 #451) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
940 |
#456 := [def-axiom]: #455 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
941 |
#618 := [unit-resolution #456 #617]: #275 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
942 |
#452 := (not #275) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
943 |
#453 := (or #452 #450) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
944 |
#454 := [def-axiom]: #453 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
945 |
#619 := [unit-resolution #454 #618]: #450 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
946 |
#620 := (not #450) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
947 |
#621 := (or #620 #595) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
948 |
#622 := [th-lemma]: #621 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
949 |
[unit-resolution #622 #619 #604]: false |
36900 | 950 |
unsat |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
951 |
26bfbe5c6decad8b4a2114b85a11ff3552d6b060 295 0 |
36900 | 952 |
#2 := false |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
953 |
#25 := 0::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
954 |
decl f8 :: (-> S4 S2 real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
955 |
decl f11 :: S2 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
956 |
#40 := f11 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
957 |
decl f12 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
958 |
#44 := f12 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
959 |
#45 := (f8 f12 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
960 |
decl f10 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
961 |
#34 := f10 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
962 |
#43 := (f8 f10 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
963 |
#199 := -1::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
964 |
#263 := (* -1::real #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
965 |
#264 := (+ #263 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
966 |
decl f5 :: real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
967 |
#26 := f5 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
968 |
#242 := (* -1::real #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
969 |
#331 := (+ #43 #242) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
970 |
#332 := (+ f5 #331) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
971 |
#333 := (<= #332 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
972 |
#336 := (ite #333 f5 #264) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
973 |
#666 := (* -1::real #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
974 |
#667 := (+ f5 #666) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
975 |
#668 := (<= #667 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
976 |
#676 := (not #668) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
977 |
#230 := 1/2::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
978 |
#414 := (* 1/2::real #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
979 |
#531 := (<= #414 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
980 |
#415 := (= #414 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
981 |
#284 := -1/2::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
982 |
#339 := (* -1/2::real #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
983 |
#342 := (+ #45 #339) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
984 |
decl f9 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
985 |
#32 := f9 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
986 |
#47 := (f8 f9 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
987 |
#243 := (+ #242 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
988 |
#316 := (* -1::real #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
989 |
#317 := (+ #45 #316) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
990 |
#318 := (+ f5 #317) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
991 |
#319 := (<= #318 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
992 |
#322 := (ite #319 f5 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
993 |
#325 := (* 1/2::real #322) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
994 |
#328 := (+ #45 #325) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
995 |
#232 := (* 1/2::real #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
996 |
#312 := (+ #242 #232) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
997 |
#231 := (* 1/2::real #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
998 |
#313 := (+ #231 #312) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
999 |
#310 := (>= #313 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1000 |
#345 := (ite #310 #328 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1001 |
#348 := (= #45 #345) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1002 |
#418 := (iff #348 #415) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1003 |
#411 := (= #45 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1004 |
#416 := (iff #411 #415) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1005 |
#417 := [rewrite]: #416 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1006 |
#412 := (iff #348 #411) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1007 |
#409 := (= #345 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1008 |
#404 := (ite false #328 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1009 |
#407 := (= #404 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1010 |
#408 := [rewrite]: #407 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1011 |
#405 := (= #345 #404) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1012 |
#402 := (iff #310 false) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1013 |
#309 := (not #310) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1014 |
#361 := (<= #317 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1015 |
#358 := (<= #331 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1016 |
#364 := (and #358 #361) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1017 |
#13 := 0::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1018 |
decl f4 :: (-> S2 int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1019 |
#41 := (f4 f11) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1020 |
#185 := -1::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1021 |
#220 := (* -1::int #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1022 |
decl f6 :: (-> S3 S2) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1023 |
decl f7 :: S3 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1024 |
#28 := f7 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1025 |
#29 := (f6 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1026 |
#30 := (f4 #29) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1027 |
#221 := (+ #30 #220) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1028 |
#222 := (<= #221 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1029 |
#367 := (or #222 #364) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1030 |
#376 := (and #309 #348 #367) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1031 |
#52 := 2::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1032 |
#61 := (- #45 #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1033 |
#62 := (<= f5 #61) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1034 |
#63 := (ite #62 f5 #61) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1035 |
#64 := (/ #63 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1036 |
#65 := (- #45 #64) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1037 |
#56 := (- #47 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1038 |
#57 := (<= f5 #56) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1039 |
#58 := (ite #57 f5 #56) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1040 |
#59 := (/ #58 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1041 |
#60 := (+ #45 #59) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1042 |
#51 := (+ #43 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1043 |
#53 := (/ #51 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1044 |
#55 := (<= #45 #53) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1045 |
#66 := (ite #55 #60 #65) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1046 |
#67 := (= #66 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1047 |
#54 := (< #53 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1048 |
#68 := (and #54 #67) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1049 |
#48 := (<= #45 #47) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1050 |
#46 := (<= #43 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1051 |
#49 := (and #46 #48) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1052 |
#42 := (< #41 #30) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1053 |
#50 := (implies #42 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1054 |
#69 := (and #50 #68) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1055 |
#381 := (iff #69 #376) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1056 |
#267 := (<= f5 #264) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1057 |
#270 := (ite #267 f5 #264) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1058 |
#285 := (* -1/2::real #270) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1059 |
#286 := (+ #45 #285) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1060 |
#246 := (<= f5 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1061 |
#249 := (ite #246 f5 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1062 |
#255 := (* 1/2::real #249) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1063 |
#260 := (+ #45 #255) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1064 |
#233 := (+ #231 #232) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1065 |
#239 := (<= #45 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1066 |
#291 := (ite #239 #260 #286) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1067 |
#297 := (= #45 #291) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1068 |
#236 := (< #233 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1069 |
#302 := (and #236 #297) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1070 |
#219 := (not #42) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1071 |
#227 := (or #219 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1072 |
#305 := (and #227 #302) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1073 |
#379 := (iff #305 #376) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1074 |
#370 := (and #309 #348) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1075 |
#373 := (and #367 #370) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1076 |
#377 := (iff #373 #376) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1077 |
#378 := [rewrite]: #377 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1078 |
#374 := (iff #305 #373) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1079 |
#371 := (iff #302 #370) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1080 |
#349 := (iff #297 #348) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1081 |
#346 := (= #291 #345) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1082 |
#343 := (= #286 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1083 |
#340 := (= #285 #339) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1084 |
#337 := (= #270 #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1085 |
#334 := (iff #267 #333) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1086 |
#335 := [rewrite]: #334 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1087 |
#338 := [monotonicity #335]: #337 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1088 |
#341 := [monotonicity #338]: #340 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1089 |
#344 := [monotonicity #341]: #343 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1090 |
#329 := (= #260 #328) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1091 |
#326 := (= #255 #325) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1092 |
#323 := (= #249 #322) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1093 |
#320 := (iff #246 #319) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1094 |
#321 := [rewrite]: #320 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1095 |
#324 := [monotonicity #321]: #323 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1096 |
#327 := [monotonicity #324]: #326 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1097 |
#330 := [monotonicity #327]: #329 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1098 |
#315 := (iff #239 #310) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1099 |
#314 := [rewrite]: #315 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1100 |
#347 := [monotonicity #314 #330 #344]: #346 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1101 |
#350 := [monotonicity #347]: #349 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1102 |
#308 := (iff #236 #309) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1103 |
#311 := [rewrite]: #308 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1104 |
#372 := [monotonicity #311 #350]: #371 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1105 |
#368 := (iff #227 #367) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1106 |
#365 := (iff #49 #364) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1107 |
#362 := (iff #48 #361) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1108 |
#363 := [rewrite]: #362 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1109 |
#359 := (iff #46 #358) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1110 |
#360 := [rewrite]: #359 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1111 |
#366 := [monotonicity #360 #363]: #365 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1112 |
#356 := (iff #219 #222) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1113 |
#223 := (not #222) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1114 |
#351 := (not #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1115 |
#354 := (iff #351 #222) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1116 |
#355 := [rewrite]: #354 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1117 |
#352 := (iff #219 #351) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1118 |
#224 := (iff #42 #223) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1119 |
#225 := [rewrite]: #224 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1120 |
#353 := [monotonicity #225]: #352 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1121 |
#357 := [trans #353 #355]: #356 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1122 |
#369 := [monotonicity #357 #366]: #368 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1123 |
#375 := [monotonicity #369 #372]: #374 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1124 |
#380 := [trans #375 #378]: #379 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1125 |
#306 := (iff #69 #305) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1126 |
#303 := (iff #68 #302) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1127 |
#300 := (iff #67 #297) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1128 |
#294 := (= #291 #45) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1129 |
#298 := (iff #294 #297) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1130 |
#299 := [rewrite]: #298 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1131 |
#295 := (iff #67 #294) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1132 |
#292 := (= #66 #291) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1133 |
#289 := (= #65 #286) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1134 |
#276 := (* 1/2::real #270) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1135 |
#281 := (- #45 #276) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1136 |
#287 := (= #281 #286) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1137 |
#288 := [rewrite]: #287 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1138 |
#282 := (= #65 #281) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1139 |
#279 := (= #64 #276) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1140 |
#273 := (/ #270 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1141 |
#277 := (= #273 #276) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1142 |
#278 := [rewrite]: #277 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1143 |
#274 := (= #64 #273) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1144 |
#271 := (= #63 #270) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1145 |
#265 := (= #61 #264) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1146 |
#266 := [rewrite]: #265 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1147 |
#268 := (iff #62 #267) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1148 |
#269 := [monotonicity #266]: #268 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1149 |
#272 := [monotonicity #269 #266]: #271 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1150 |
#275 := [monotonicity #272]: #274 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1151 |
#280 := [trans #275 #278]: #279 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1152 |
#283 := [monotonicity #280]: #282 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1153 |
#290 := [trans #283 #288]: #289 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1154 |
#261 := (= #60 #260) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1155 |
#258 := (= #59 #255) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1156 |
#252 := (/ #249 2::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1157 |
#256 := (= #252 #255) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1158 |
#257 := [rewrite]: #256 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1159 |
#253 := (= #59 #252) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1160 |
#250 := (= #58 #249) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1161 |
#244 := (= #56 #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1162 |
#245 := [rewrite]: #244 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1163 |
#247 := (iff #57 #246) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1164 |
#248 := [monotonicity #245]: #247 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1165 |
#251 := [monotonicity #248 #245]: #250 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1166 |
#254 := [monotonicity #251]: #253 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1167 |
#259 := [trans #254 #257]: #258 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1168 |
#262 := [monotonicity #259]: #261 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1169 |
#240 := (iff #55 #239) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1170 |
#234 := (= #53 #233) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1171 |
#235 := [rewrite]: #234 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1172 |
#241 := [monotonicity #235]: #240 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1173 |
#293 := [monotonicity #241 #262 #290]: #292 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1174 |
#296 := [monotonicity #293]: #295 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1175 |
#301 := [trans #296 #299]: #300 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1176 |
#237 := (iff #54 #236) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1177 |
#238 := [monotonicity #235]: #237 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1178 |
#304 := [monotonicity #238 #301]: #303 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1179 |
#228 := (iff #50 #227) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1180 |
#229 := [rewrite]: #228 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1181 |
#307 := [monotonicity #229 #304]: #306 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1182 |
#382 := [trans #307 #380]: #381 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1183 |
#218 := [asserted]: #69 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1184 |
#383 := [mp #218 #382]: #376 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1185 |
#384 := [and-elim #383]: #309 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1186 |
#403 := [iff-false #384]: #402 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1187 |
#406 := [monotonicity #403]: #405 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1188 |
#410 := [trans #406 #408]: #409 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1189 |
#413 := [monotonicity #410]: #412 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1190 |
#419 := [trans #413 #417]: #418 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1191 |
#385 := [and-elim #383]: #348 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1192 |
#420 := [mp #385 #419]: #415 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1193 |
#670 := (not #415) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1194 |
#671 := (or #670 #531) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1195 |
#672 := [th-lemma]: #671 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1196 |
#673 := [unit-resolution #672 #420]: #531 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1197 |
#674 := [hypothesis]: #668 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1198 |
#174 := (<= f5 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1199 |
#175 := (not #174) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1200 |
#27 := (< 0::real f5) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1201 |
#176 := (iff #27 #175) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1202 |
#177 := [rewrite]: #176 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1203 |
#171 := [asserted]: #27 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1204 |
#178 := [mp #171 #177]: #175 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1205 |
#675 := [th-lemma #178 #674 #673]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1206 |
#677 := [lemma #675]: #676 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1207 |
#524 := (= f5 #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1208 |
#525 := (= #264 #336) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1209 |
#685 := (not #525) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1210 |
#669 := (+ #264 #666) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1211 |
#678 := (<= #669 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1212 |
#682 := (not #678) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1213 |
#428 := (iff #367 #364) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1214 |
#423 := (or false #364) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1215 |
#426 := (iff #423 #364) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1216 |
#427 := [rewrite]: #426 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1217 |
#424 := (iff #367 #423) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1218 |
#400 := (iff #222 false) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1219 |
#217 := [asserted]: #42 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1220 |
#226 := [mp #217 #225]: #223 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1221 |
#401 := [iff-false #226]: #400 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1222 |
#425 := [monotonicity #401]: #424 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1223 |
#429 := [trans #425 #427]: #428 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1224 |
#386 := [and-elim #383]: #367 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1225 |
#430 := [mp #386 #429]: #364 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1226 |
#422 := [and-elim #430]: #361 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1227 |
#680 := [hypothesis]: #678 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1228 |
#681 := [th-lemma #680 #422 #384 #673]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1229 |
#683 := [lemma #681]: #682 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1230 |
#684 := [hypothesis]: #525 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1231 |
#686 := (or #685 #678) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1232 |
#687 := [th-lemma]: #686 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1233 |
#688 := [unit-resolution #687 #684 #683]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1234 |
#689 := [lemma #688]: #685 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1235 |
#529 := (or #333 #525) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1236 |
#530 := [def-axiom]: #529 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1237 |
#690 := [unit-resolution #530 #689]: #333 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1238 |
#526 := (not #333) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1239 |
#527 := (or #526 #524) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1240 |
#528 := [def-axiom]: #527 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1241 |
#691 := [unit-resolution #528 #690]: #524 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1242 |
#692 := (not #524) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1243 |
#693 := (or #692 #668) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1244 |
#694 := [th-lemma]: #693 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1245 |
[unit-resolution #694 #691 #677]: false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1246 |
unsat |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1247 |
5d75e298a98eb55cd39dacd22665bd3062cf5345 204 0 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1248 |
#2 := false |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1249 |
#46 := 0::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1250 |
decl f5 :: (-> S3 S2 real) |
36900 | 1251 |
decl f7 :: S2 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1252 |
#26 := f7 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1253 |
decl f11 :: S3 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1254 |
#38 := f11 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1255 |
#49 := (f5 f11 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1256 |
#183 := -1::real |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1257 |
#349 := (* -1::real #49) |
36900 | 1258 |
decl f8 :: S3 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1259 |
#28 := f8 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1260 |
#29 := (f5 f8 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1261 |
#362 := (+ #29 #349) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1262 |
#363 := (>= #362 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1263 |
#368 := (not #363) |
36900 | 1264 |
decl f6 :: S3 |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1265 |
#25 := f6 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1266 |
#27 := (f5 f6 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1267 |
#350 := (+ #27 #349) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1268 |
#351 := (<= #350 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1269 |
#352 := (not #351) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1270 |
#371 := (or #352 #368) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1271 |
#374 := (not #371) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1272 |
#8 := (:var 0 S2) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1273 |
#41 := (f5 f8 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1274 |
#333 := (pattern #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1275 |
#39 := (f5 f11 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1276 |
#332 := (pattern #39) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1277 |
#37 := (f5 f6 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1278 |
#331 := (pattern #37) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1279 |
decl f4 :: (-> S2 int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1280 |
#9 := (f4 #8) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1281 |
#311 := (pattern #9) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1282 |
#189 := (* -1::real #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1283 |
#190 := (+ #39 #189) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1284 |
#191 := (<= #190 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1285 |
#242 := (not #191) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1286 |
#184 := (* -1::real #39) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1287 |
#185 := (+ #37 #184) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1288 |
#186 := (<= #185 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1289 |
#241 := (not #186) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1290 |
#243 := (or #241 #242) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1291 |
#244 := (not #243) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1292 |
#13 := 0::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1293 |
decl f9 :: (-> S4 S2) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1294 |
decl f10 :: S4 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1295 |
#32 := f10 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1296 |
#33 := (f9 f10) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1297 |
#34 := (f4 #33) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1298 |
#157 := -1::int |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1299 |
#160 := (* -1::int #34) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1300 |
#173 := (+ #9 #160) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1301 |
#172 := (>= #173 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1302 |
#247 := (or #172 #244) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1303 |
#334 := (forall (vars (?v0 S2)) (:pat #311 #331 #332 #333) #247) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1304 |
#250 := (forall (vars (?v0 S2)) #247) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1305 |
#337 := (iff #250 #334) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1306 |
#335 := (iff #247 #247) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1307 |
#336 := [refl]: #335 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1308 |
#338 := [quant-intro #336]: #337 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1309 |
#194 := (and #186 #191) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1310 |
#197 := (or #172 #194) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1311 |
#200 := (forall (vars (?v0 S2)) #197) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1312 |
#251 := (iff #200 #250) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1313 |
#248 := (iff #197 #247) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1314 |
#245 := (iff #194 #244) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1315 |
#246 := [rewrite]: #245 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1316 |
#249 := [monotonicity #246]: #248 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1317 |
#252 := [quant-intro #249]: #251 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1318 |
#219 := (~ #200 #200) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1319 |
#224 := (~ #197 #197) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1320 |
#222 := [refl]: #224 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1321 |
#239 := [nnf-pos #222]: #219 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1322 |
#42 := (<= #39 #41) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1323 |
#40 := (<= #37 #39) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1324 |
#43 := (and #40 #42) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1325 |
#36 := (< #9 #34) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1326 |
#44 := (implies #36 #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1327 |
#45 := (forall (vars (?v0 S2)) #44) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1328 |
#203 := (iff #45 #200) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1329 |
#156 := (not #36) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1330 |
#165 := (or #156 #43) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1331 |
#168 := (forall (vars (?v0 S2)) #165) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1332 |
#201 := (iff #168 #200) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1333 |
#198 := (iff #165 #197) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1334 |
#195 := (iff #43 #194) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1335 |
#192 := (iff #42 #191) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1336 |
#193 := [rewrite]: #192 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1337 |
#187 := (iff #40 #186) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1338 |
#188 := [rewrite]: #187 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1339 |
#196 := [monotonicity #188 #193]: #195 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1340 |
#181 := (iff #156 #172) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1341 |
#171 := (not #172) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1342 |
#176 := (not #171) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1343 |
#179 := (iff #176 #172) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1344 |
#180 := [rewrite]: #179 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1345 |
#177 := (iff #156 #176) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1346 |
#174 := (iff #36 #171) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1347 |
#175 := [rewrite]: #174 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1348 |
#178 := [monotonicity #175]: #177 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1349 |
#182 := [trans #178 #180]: #181 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1350 |
#199 := [monotonicity #182 #196]: #198 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1351 |
#202 := [quant-intro #199]: #201 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1352 |
#169 := (iff #45 #168) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1353 |
#166 := (iff #44 #165) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1354 |
#167 := [rewrite]: #166 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1355 |
#170 := [quant-intro #167]: #169 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1356 |
#204 := [trans #170 #202]: #203 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1357 |
#155 := [asserted]: #45 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1358 |
#205 := [mp #155 #204]: #200 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1359 |
#240 := [mp~ #205 #239]: #200 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1360 |
#253 := [mp #240 #252]: #250 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1361 |
#339 := [mp #253 #338]: #334 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1362 |
#31 := (f4 f7) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1363 |
#161 := (+ #31 #160) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1364 |
#159 := (>= #161 0::int) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1365 |
#158 := (not #159) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1366 |
#35 := (< #31 #34) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1367 |
#162 := (iff #35 #158) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1368 |
#163 := [rewrite]: #162 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1369 |
#154 := [asserted]: #35 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1370 |
#164 := [mp #154 #163]: #158 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1371 |
#380 := (not #334) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1372 |
#381 := (or #380 #159 #374) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1373 |
#342 := (* -1::real #29) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1374 |
#343 := (+ #49 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1375 |
#347 := (<= #343 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1376 |
#348 := (not #347) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1377 |
#353 := (or #352 #348) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1378 |
#354 := (not #353) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1379 |
#355 := (or #159 #354) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1380 |
#382 := (or #380 #355) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1381 |
#389 := (iff #382 #381) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1382 |
#377 := (or #159 #374) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1383 |
#384 := (or #380 #377) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1384 |
#387 := (iff #384 #381) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1385 |
#388 := [rewrite]: #387 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1386 |
#385 := (iff #382 #384) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1387 |
#378 := (iff #355 #377) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1388 |
#375 := (iff #354 #374) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1389 |
#372 := (iff #353 #371) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1390 |
#369 := (iff #348 #368) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1391 |
#366 := (iff #347 #363) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1392 |
#356 := (+ #342 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1393 |
#359 := (<= #356 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1394 |
#364 := (iff #359 #363) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1395 |
#365 := [rewrite]: #364 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1396 |
#360 := (iff #347 #359) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1397 |
#357 := (= #343 #356) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1398 |
#358 := [rewrite]: #357 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1399 |
#361 := [monotonicity #358]: #360 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1400 |
#367 := [trans #361 #365]: #366 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1401 |
#370 := [monotonicity #367]: #369 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1402 |
#373 := [monotonicity #370]: #372 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1403 |
#376 := [monotonicity #373]: #375 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1404 |
#379 := [monotonicity #376]: #378 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1405 |
#386 := [monotonicity #379]: #385 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1406 |
#390 := [trans #386 #388]: #389 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1407 |
#383 := [quant-inst]: #382 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1408 |
#391 := [mp #383 #390]: #381 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1409 |
#513 := [unit-resolution #391 #164 #339]: #374 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1410 |
#394 := (or #371 #363) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1411 |
#395 := [def-axiom]: #394 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1412 |
#514 := [unit-resolution #395 #513]: #363 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1413 |
#475 := (>= #350 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1414 |
#524 := (not #475) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1415 |
#474 := (= #27 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1416 |
#519 := (not #474) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1417 |
#208 := (= #29 #49) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1418 |
#216 := (not #208) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1419 |
#520 := (iff #216 #519) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1420 |
#517 := (iff #208 #474) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1421 |
#515 := (iff #474 #208) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1422 |
#30 := (= #27 #29) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1423 |
#153 := [asserted]: #30 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1424 |
#516 := [monotonicity #153]: #515 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1425 |
#518 := [symm #516]: #517 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1426 |
#521 := [monotonicity #518]: #520 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1427 |
#50 := (= #49 #29) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1428 |
#51 := (not #50) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1429 |
#217 := (iff #51 #216) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1430 |
#214 := (iff #50 #208) |
36900 | 1431 |
#215 := [rewrite]: #214 |
1432 |
#218 := [monotonicity #215]: #217 |
|
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1433 |
#207 := [asserted]: #51 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1434 |
#221 := [mp #207 #218]: #216 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1435 |
#522 := [mp #221 #521]: #519 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1436 |
#527 := (or #474 #524) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1437 |
#392 := (or #371 #351) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1438 |
#393 := [def-axiom]: #392 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1439 |
#523 := [unit-resolution #393 #513]: #351 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1440 |
#525 := (or #474 #352 #524) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1441 |
#526 := [th-lemma]: #525 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1442 |
#528 := [unit-resolution #526 #523]: #527 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1443 |
#529 := [unit-resolution #528 #522]: #524 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1444 |
#471 := (+ #27 #342) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1445 |
#473 := (>= #471 0::real) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1446 |
#530 := (not #30) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1447 |
#531 := (or #530 #473) |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1448 |
#532 := [th-lemma]: #531 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1449 |
#533 := [unit-resolution #532 #153]: #473 |
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1450 |
[th-lemma #533 #529 #514]: false |
36900 | 1451 |
unsat |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
37489
diff
changeset
|
1452 |
7b235442f6856a575f67cb04d6eaa03042f5336e 870 0 |
36900 | 1453 |
#2 := false |
1454 |
#11 := 0::real |
|
1455 |
decl f5 :: real |
|
1456 |
#26 := f5 |
|
1457 |
decl f3 :: real |
|
1458 |
#9 := f3 |
|
1459 |
#76 := -1::real |
|
1460 |
#77 := (* -1::real f3) |
|
1461 |
#176 := (+ #77 f5) |
|
1462 |
#124 := (* -1::real f5) |
|
1463 |
#167 := (+ f3 #124) |
|
1464 |
#260 := (>= #167 0::real) |
|
1465 |
#267 := (ite #260 #167 #176) |
|
1466 |
#275 := (* -1::real #267) |
|
1467 |
decl f4 :: real |
|
1468 |
#15 := f4 |
|
1469 |
#96 := 1/3::real |
|
1470 |
#97 := (* 1/3::real f4) |
|
1471 |
#276 := (+ #97 #275) |
|
1472 |
#277 := (<= #276 0::real) |
|
1473 |
#278 := (not #277) |
|
1474 |
decl ?v0!5 :: real |
|
1475 |
#448 := ?v0!5 |
|
1476 |
#459 := (* -1::real ?v0!5) |
|
1477 |
#573 := (+ f3 #459) |
|
1478 |
#567 := (+ #77 ?v0!5) |
|
1479 |
#574 := (<= #573 0::real) |
|
1480 |
#581 := (ite #574 #567 #573) |
|
1481 |
#584 := (* -1::real #581) |
|
1482 |
#587 := (+ #97 #584) |
|
1483 |
#590 := (<= #587 0::real) |
|
1484 |
#593 := (not #590) |
|
1485 |
decl ?v2!3 :: real |
|
1486 |
#442 := ?v2!3 |
|
1487 |
#477 := (* -1::real ?v2!3) |
|
1488 |
#544 := (+ f5 #477) |
|
1489 |
#538 := (+ #124 ?v2!3) |
|
1490 |
#545 := (<= #544 0::real) |
|
1491 |
#552 := (ite #545 #538 #544) |
|
1492 |
#555 := (* -1::real #552) |
|
1493 |
#558 := (+ #97 #555) |
|
1494 |
#561 := (<= #558 0::real) |
|
1495 |
#564 := (not #561) |
|
1496 |
decl ?v4!1 :: real |
|
1497 |
#446 := ?v4!1 |
|
1498 |
#532 := (+ ?v4!1 #459) |
|
1499 |
#533 := (>= #532 0::real) |
|
1500 |
decl ?v1!4 :: real |
|
1501 |
#447 := ?v1!4 |
|
1502 |
#468 := (* -1::real ?v1!4) |
|
1503 |
decl ?v5!0 :: real |
|
1504 |
#445 := ?v5!0 |
|
1505 |
#520 := (+ ?v5!0 #468) |
|
1506 |
#521 := (>= #520 0::real) |
|
1507 |
#451 := (* -1::real ?v5!0) |
|
1508 |
decl ?v3!2 :: real |
|
1509 |
#444 := ?v3!2 |
|
1510 |
#499 := (+ ?v3!2 #451) |
|
1511 |
#500 := (>= #499 0::real) |
|
1512 |
#449 := (* -1::real ?v4!1) |
|
1513 |
#497 := (+ ?v2!3 #449) |
|
1514 |
#498 := (>= #497 0::real) |
|
1515 |
#486 := (* -1::real ?v3!2) |
|
1516 |
#487 := (+ f5 #486) |
|
1517 |
#488 := (+ #124 ?v3!2) |
|
1518 |
#489 := (<= #487 0::real) |
|
1519 |
#490 := (ite #489 #488 #487) |
|
1520 |
#491 := (* -1::real #490) |
|
1521 |
#492 := (+ #97 #491) |
|
1522 |
#493 := (<= #492 0::real) |
|
1523 |
#494 := (not #493) |
|
1524 |
#469 := (+ f3 #468) |
|
1525 |
#470 := (+ #77 ?v1!4) |
|
1526 |
#471 := (<= #469 0::real) |
|
1527 |
#472 := (ite #471 #470 #469) |
|
1528 |
#473 := (* -1::real #472) |
|
1529 |
#474 := (+ #97 #473) |
|
1530 |
#475 := (<= #474 0::real) |
|
1531 |
#476 := (not #475) |
|
1532 |
#599 := (and #278 #476 #494 #498 #500 #521 #533 #564 #593) |
|
1533 |
#613 := (+ ?v5!0 #449) |
|
1534 |
#607 := (+ #451 ?v4!1) |
|
1535 |
#614 := (<= #613 0::real) |
|
1536 |
#621 := (ite #614 #607 #613) |
|
1537 |
#624 := (* -1::real #621) |
|
1538 |
#627 := (+ f4 #624) |
|
1539 |
#630 := (<= #627 0::real) |
|
1540 |
#633 := (not #630) |
|
1541 |
#604 := (not #599) |
|
1542 |
#636 := (or #604 #633) |
|
1543 |
#639 := (not #636) |
|
1544 |
#450 := (+ #449 ?v5!0) |
|
1545 |
#452 := (+ ?v4!1 #451) |
|
1546 |
#453 := (>= #452 0::real) |
|
1547 |
#454 := (ite #453 #452 #450) |
|
1548 |
#455 := (* -1::real #454) |
|
1549 |
#456 := (+ f4 #455) |
|
1550 |
#457 := (<= #456 0::real) |
|
1551 |
#458 := (not #457) |
|
1552 |
#460 := (+ #459 f3) |
|
1553 |
#461 := (+ ?v0!5 #77) |
|
1554 |
#462 := (>= #461 0::real) |
|
1555 |
#463 := (ite #462 #461 #460) |
|
1556 |
#464 := (* -1::real #463) |
|
1557 |
#465 := (+ #97 #464) |
|
1558 |
#466 := (<= #465 0::real) |
|
1559 |
#467 := (not #466) |
|
1560 |
#478 := (+ #477 f5) |
|
1561 |
#479 := (+ ?v2!3 #124) |
|
1562 |
#480 := (>= #479 0::real) |
|
1563 |
#481 := (ite #480 #479 #478) |
|
1564 |
#482 := (* -1::real #481) |
|
1565 |
#483 := (+ #97 #482) |
|
1566 |
#484 := (<= #483 0::real) |
|
1567 |
#485 := (not #484) |
|
1568 |
#495 := (+ ?v0!5 #449) |
|
1569 |
#496 := (<= #495 0::real) |
|
1570 |
#501 := (+ ?v1!4 #451) |
|
1571 |
#502 := (<= #501 0::real) |
|
1572 |
#503 := (and #502 #500 #498 #496 #278 #494 #485 #476 #467) |
|
1573 |
#504 := (not #503) |
|
1574 |
#505 := (or #504 #458) |
|
1575 |
#506 := (not #505) |
|
1576 |
#640 := (iff #506 #639) |
|
1577 |
#637 := (iff #505 #636) |
|
1578 |
#634 := (iff #458 #633) |
|
1579 |
#631 := (iff #457 #630) |
|
1580 |
#628 := (= #456 #627) |
|
1581 |
#625 := (= #455 #624) |
|
1582 |
#622 := (= #454 #621) |
|
1583 |
#619 := (= #450 #613) |
|
1584 |
#620 := [rewrite]: #619 |
|
1585 |
#608 := (= #452 #607) |
|
1586 |
#609 := [rewrite]: #608 |
|
1587 |
#617 := (iff #453 #614) |
|
1588 |
#610 := (>= #607 0::real) |
|
1589 |
#615 := (iff #610 #614) |
|
1590 |
#616 := [rewrite]: #615 |
|
1591 |
#611 := (iff #453 #610) |
|
1592 |
#612 := [monotonicity #609]: #611 |
|
1593 |
#618 := [trans #612 #616]: #617 |
|
1594 |
#623 := [monotonicity #618 #609 #620]: #622 |
|
1595 |
#626 := [monotonicity #623]: #625 |
|
1596 |
#629 := [monotonicity #626]: #628 |
|
1597 |
#632 := [monotonicity #629]: #631 |
|
1598 |
#635 := [monotonicity #632]: #634 |
|
1599 |
#605 := (iff #504 #604) |
|
1600 |
#602 := (iff #503 #599) |
|
1601 |
#596 := (and #521 #500 #498 #533 #278 #494 #564 #476 #593) |
|
1602 |
#600 := (iff #596 #599) |
|
1603 |
#601 := [rewrite]: #600 |
|
1604 |
#597 := (iff #503 #596) |
|
1605 |
#594 := (iff #467 #593) |
|
1606 |
#591 := (iff #466 #590) |
|
1607 |
#588 := (= #465 #587) |
|
1608 |
#585 := (= #464 #584) |
|
1609 |
#582 := (= #463 #581) |
|
1610 |
#579 := (= #460 #573) |
|
1611 |
#580 := [rewrite]: #579 |
|
1612 |
#568 := (= #461 #567) |
|
1613 |
#569 := [rewrite]: #568 |
|
1614 |
#577 := (iff #462 #574) |
|
1615 |
#570 := (>= #567 0::real) |
|
1616 |
#575 := (iff #570 #574) |
|
1617 |
#576 := [rewrite]: #575 |
|
1618 |
#571 := (iff #462 #570) |
|
1619 |
#572 := [monotonicity #569]: #571 |
|
1620 |
#578 := [trans #572 #576]: #577 |
|
1621 |
#583 := [monotonicity #578 #569 #580]: #582 |
|
1622 |
#586 := [monotonicity #583]: #585 |
|
1623 |
#589 := [monotonicity #586]: #588 |
|
1624 |
#592 := [monotonicity #589]: #591 |
|
1625 |
#595 := [monotonicity #592]: #594 |
|
1626 |
#565 := (iff #485 #564) |
|
1627 |
#562 := (iff #484 #561) |
|
1628 |
#559 := (= #483 #558) |
|
1629 |
#556 := (= #482 #555) |
|
1630 |
#553 := (= #481 #552) |
|
1631 |
#550 := (= #478 #544) |
|
1632 |
#551 := [rewrite]: #550 |
|
1633 |
#539 := (= #479 #538) |
|
1634 |
#540 := [rewrite]: #539 |
|
1635 |
#548 := (iff #480 #545) |
|
1636 |
#541 := (>= #538 0::real) |
|
1637 |
#546 := (iff #541 #545) |
|
1638 |
#547 := [rewrite]: #546 |
|
1639 |
#542 := (iff #480 #541) |
|
1640 |
#543 := [monotonicity #540]: #542 |
|
1641 |
#549 := [trans #543 #547]: #548 |
|
1642 |
#554 := [monotonicity #549 #540 #551]: #553 |
|
1643 |
#557 := [monotonicity #554]: #556 |
|
1644 |
#560 := [monotonicity #557]: #559 |
|
1645 |
#563 := [monotonicity #560]: #562 |
|
1646 |
#566 := [monotonicity #563]: #565 |
|
1647 |
#536 := (iff #496 #533) |
|
1648 |
#526 := (+ #449 ?v0!5) |
|
1649 |
#529 := (<= #526 0::real) |
|
1650 |
#534 := (iff #529 #533) |
|
1651 |
#535 := [rewrite]: #534 |
|
1652 |
#530 := (iff #496 #529) |
|
1653 |
#527 := (= #495 #526) |
|
1654 |
#528 := [rewrite]: #527 |
|
1655 |
#531 := [monotonicity #528]: #530 |
|
1656 |
#537 := [trans #531 #535]: #536 |
|
1657 |
#524 := (iff #502 #521) |
|
1658 |
#514 := (+ #451 ?v1!4) |
|
1659 |
#517 := (<= #514 0::real) |
|
1660 |
#522 := (iff #517 #521) |
|
1661 |
#523 := [rewrite]: #522 |
|
1662 |
#518 := (iff #502 #517) |
|
1663 |
#515 := (= #501 #514) |
|
1664 |
#516 := [rewrite]: #515 |
|
1665 |
#519 := [monotonicity #516]: #518 |
|
1666 |
#525 := [trans #519 #523]: #524 |
|
1667 |
#598 := [monotonicity #525 #537 #566 #595]: #597 |
|
1668 |
#603 := [trans #598 #601]: #602 |
|
1669 |
#606 := [monotonicity #603]: #605 |
|
1670 |
#638 := [monotonicity #606 #635]: #637 |
|
1671 |
#641 := [monotonicity #638]: #640 |
|
1672 |
#46 := (:var 0 real) |
|
1673 |
#43 := (:var 1 real) |
|
1674 |
#217 := (* -1::real #43) |
|
1675 |
#218 := (+ #217 #46) |
|
1676 |
#207 := (* -1::real #46) |
|
1677 |
#208 := (+ #43 #207) |
|
1678 |
#407 := (>= #208 0::real) |
|
1679 |
#414 := (ite #407 #208 #218) |
|
1680 |
#422 := (* -1::real #414) |
|
1681 |
#423 := (+ f4 #422) |
|
1682 |
#424 := (<= #423 0::real) |
|
1683 |
#425 := (not #424) |
|
1684 |
#8 := (:var 5 real) |
|
1685 |
#87 := (* -1::real #8) |
|
1686 |
#88 := (+ #87 f3) |
|
1687 |
#78 := (+ #8 #77) |
|
1688 |
#352 := (>= #78 0::real) |
|
1689 |
#359 := (ite #352 #78 #88) |
|
1690 |
#367 := (* -1::real #359) |
|
1691 |
#368 := (+ #97 #367) |
|
1692 |
#369 := (<= #368 0::real) |
|
1693 |
#370 := (not #369) |
|
1694 |
#19 := (:var 4 real) |
|
1695 |
#112 := (* -1::real #19) |
|
1696 |
#113 := (+ f3 #112) |
|
1697 |
#103 := (+ #77 #19) |
|
1698 |
#329 := (<= #113 0::real) |
|
1699 |
#336 := (ite #329 #103 #113) |
|
1700 |
#344 := (* -1::real #336) |
|
1701 |
#345 := (+ #97 #344) |
|
1702 |
#346 := (<= #345 0::real) |
|
1703 |
#347 := (not #346) |
|
1704 |
#25 := (:var 3 real) |
|
1705 |
#134 := (* -1::real #25) |
|
1706 |
#135 := (+ #134 f5) |
|
1707 |
#125 := (+ #25 #124) |
|
1708 |
#306 := (>= #125 0::real) |
|
1709 |
#313 := (ite #306 #125 #135) |
|
1710 |
#321 := (* -1::real #313) |
|
1711 |
#322 := (+ #97 #321) |
|
1712 |
#323 := (<= #322 0::real) |
|
1713 |
#324 := (not #323) |
|
1714 |
#32 := (:var 2 real) |
|
1715 |
#155 := (* -1::real #32) |
|
1716 |
#156 := (+ f5 #155) |
|
1717 |
#146 := (+ #124 #32) |
|
1718 |
#283 := (<= #156 0::real) |
|
1719 |
#290 := (ite #283 #146 #156) |
|
1720 |
#298 := (* -1::real #290) |
|
1721 |
#299 := (+ #97 #298) |
|
1722 |
#300 := (<= #299 0::real) |
|
1723 |
#301 := (not #300) |
|
1724 |
#256 := (+ #8 #217) |
|
1725 |
#257 := (<= #256 0::real) |
|
1726 |
#253 := (+ #25 #217) |
|
1727 |
#252 := (>= #253 0::real) |
|
1728 |
#249 := (+ #32 #207) |
|
1729 |
#248 := (>= #249 0::real) |
|
1730 |
#244 := (+ #19 #207) |
|
1731 |
#245 := (<= #244 0::real) |
|
1732 |
#399 := (and #245 #248 #252 #257 #278 #301 #324 #347 #370) |
|
1733 |
#404 := (not #399) |
|
1734 |
#430 := (or #404 #425) |
|
1735 |
#433 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #430) |
|
1736 |
#436 := (not #433) |
|
1737 |
#507 := (~ #436 #506) |
|
1738 |
#508 := [sk]: #507 |
|
1739 |
#57 := (- #43 #46) |
|
1740 |
#59 := (- #57) |
|
1741 |
#58 := (< #57 0::real) |
|
1742 |
#60 := (ite #58 #59 #57) |
|
1743 |
#61 := (< #60 f4) |
|
1744 |
#48 := (<= #46 #32) |
|
1745 |
#47 := (<= #19 #46) |
|
1746 |
#49 := (and #47 #48) |
|
1747 |
#45 := (<= #43 #25) |
|
1748 |
#50 := (and #45 #49) |
|
1749 |
#44 := (<= #8 #43) |
|
1750 |
#51 := (and #44 #50) |
|
1751 |
#16 := 3::real |
|
1752 |
#17 := (/ f4 3::real) |
|
1753 |
#38 := (- f3 f5) |
|
1754 |
#40 := (- #38) |
|
1755 |
#39 := (< #38 0::real) |
|
1756 |
#41 := (ite #39 #40 #38) |
|
1757 |
#42 := (< #41 #17) |
|
1758 |
#52 := (and #42 #51) |
|
1759 |
#33 := (- #32 f5) |
|
1760 |
#35 := (- #33) |
|
1761 |
#34 := (< #33 0::real) |
|
1762 |
#36 := (ite #34 #35 #33) |
|
1763 |
#37 := (< #36 #17) |
|
1764 |
#53 := (and #37 #52) |
|
1765 |
#27 := (- #25 f5) |
|
1766 |
#29 := (- #27) |
|
1767 |
#28 := (< #27 0::real) |
|
1768 |
#30 := (ite #28 #29 #27) |
|
1769 |
#31 := (< #30 #17) |
|
1770 |
#54 := (and #31 #53) |
|
1771 |
#20 := (- #19 f3) |
|
1772 |
#22 := (- #20) |
|
1773 |
#21 := (< #20 0::real) |
|
1774 |
#23 := (ite #21 #22 #20) |
|
1775 |
#24 := (< #23 #17) |
|
1776 |
#55 := (and #24 #54) |
|
1777 |
#10 := (- #8 f3) |
|
1778 |
#13 := (- #10) |
|
1779 |
#12 := (< #10 0::real) |
|
1780 |
#14 := (ite #12 #13 #10) |
|
1781 |
#18 := (< #14 #17) |
|
1782 |
#56 := (and #18 #55) |
|
1783 |
#62 := (implies #56 #61) |
|
1784 |
#63 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #62) |
|
1785 |
#64 := (not #63) |
|
1786 |
#439 := (iff #64 #436) |
|
1787 |
#211 := (< #208 0::real) |
|
1788 |
#223 := (ite #211 #218 #208) |
|
1789 |
#226 := (< #223 f4) |
|
1790 |
#170 := (< #167 0::real) |
|
1791 |
#181 := (ite #170 #176 #167) |
|
1792 |
#184 := (< #181 #97) |
|
1793 |
#190 := (and #51 #184) |
|
1794 |
#149 := (< #146 0::real) |
|
1795 |
#161 := (ite #149 #156 #146) |
|
1796 |
#164 := (< #161 #97) |
|
1797 |
#195 := (and #164 #190) |
|
1798 |
#128 := (< #125 0::real) |
|
1799 |
#140 := (ite #128 #135 #125) |
|
1800 |
#143 := (< #140 #97) |
|
1801 |
#198 := (and #143 #195) |
|
1802 |
#106 := (< #103 0::real) |
|
1803 |
#118 := (ite #106 #113 #103) |
|
1804 |
#121 := (< #118 #97) |
|
1805 |
#201 := (and #121 #198) |
|
1806 |
#81 := (< #78 0::real) |
|
1807 |
#93 := (ite #81 #88 #78) |
|
1808 |
#100 := (< #93 #97) |
|
1809 |
#204 := (and #100 #201) |
|
1810 |
#232 := (not #204) |
|
1811 |
#233 := (or #232 #226) |
|
1812 |
#238 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #233) |
|
1813 |
#241 := (not #238) |
|
1814 |
#437 := (iff #241 #436) |
|
1815 |
#434 := (iff #238 #433) |
|
1816 |
#431 := (iff #233 #430) |
|
1817 |
#428 := (iff #226 #425) |
|
1818 |
#419 := (< #414 f4) |
|
1819 |
#426 := (iff #419 #425) |
|
1820 |
#427 := [rewrite]: #426 |
|
1821 |
#420 := (iff #226 #419) |
|
1822 |
#417 := (= #223 #414) |
|
1823 |
#408 := (not #407) |
|
1824 |
#411 := (ite #408 #218 #208) |
|
1825 |
#415 := (= #411 #414) |
|
1826 |
#416 := [rewrite]: #415 |
|
1827 |
#412 := (= #223 #411) |
|
1828 |
#409 := (iff #211 #408) |
|
1829 |
#410 := [rewrite]: #409 |
|
1830 |
#413 := [monotonicity #410]: #412 |
|
1831 |
#418 := [trans #413 #416]: #417 |
|
1832 |
#421 := [monotonicity #418]: #420 |
|
1833 |
#429 := [trans #421 #427]: #428 |
|
1834 |
#405 := (iff #232 #404) |
|
1835 |
#402 := (iff #204 #399) |
|
1836 |
#375 := (and #245 #248) |
|
1837 |
#378 := (and #252 #375) |
|
1838 |
#381 := (and #257 #378) |
|
1839 |
#384 := (and #381 #278) |
|
1840 |
#387 := (and #301 #384) |
|
1841 |
#390 := (and #324 #387) |
|
1842 |
#393 := (and #347 #390) |
|
1843 |
#396 := (and #370 #393) |
|
1844 |
#400 := (iff #396 #399) |
|
1845 |
#401 := [rewrite]: #400 |
|
1846 |
#397 := (iff #204 #396) |
|
1847 |
#394 := (iff #201 #393) |
|
1848 |
#391 := (iff #198 #390) |
|
1849 |
#388 := (iff #195 #387) |
|
1850 |
#385 := (iff #190 #384) |
|
1851 |
#281 := (iff #184 #278) |
|
1852 |
#272 := (< #267 #97) |
|
1853 |
#279 := (iff #272 #278) |
|
1854 |
#280 := [rewrite]: #279 |
|
1855 |
#273 := (iff #184 #272) |
|
1856 |
#270 := (= #181 #267) |
|
1857 |
#261 := (not #260) |
|
1858 |
#264 := (ite #261 #176 #167) |
|
1859 |
#268 := (= #264 #267) |
|
1860 |
#269 := [rewrite]: #268 |
|
1861 |
#265 := (= #181 #264) |
|
1862 |
#262 := (iff #170 #261) |
|
1863 |
#263 := [rewrite]: #262 |
|
1864 |
#266 := [monotonicity #263]: #265 |
|
1865 |
#271 := [trans #266 #269]: #270 |
|
1866 |
#274 := [monotonicity #271]: #273 |
|
1867 |
#282 := [trans #274 #280]: #281 |
|
1868 |
#382 := (iff #51 #381) |
|
1869 |
#379 := (iff #50 #378) |
|
1870 |
#376 := (iff #49 #375) |
|
1871 |
#250 := (iff #48 #248) |
|
1872 |
#251 := [rewrite]: #250 |
|
1873 |
#246 := (iff #47 #245) |
|
1874 |
#247 := [rewrite]: #246 |
|
1875 |
#377 := [monotonicity #247 #251]: #376 |
|
1876 |
#254 := (iff #45 #252) |
|
1877 |
#255 := [rewrite]: #254 |
|
1878 |
#380 := [monotonicity #255 #377]: #379 |
|
1879 |
#258 := (iff #44 #257) |
|
1880 |
#259 := [rewrite]: #258 |
|
1881 |
#383 := [monotonicity #259 #380]: #382 |
|
1882 |
#386 := [monotonicity #383 #282]: #385 |
|
1883 |
#304 := (iff #164 #301) |
|
1884 |
#295 := (< #290 #97) |
|
1885 |
#302 := (iff #295 #301) |
|
1886 |
#303 := [rewrite]: #302 |
|
1887 |
#296 := (iff #164 #295) |
|
1888 |
#293 := (= #161 #290) |
|
1889 |
#284 := (not #283) |
|
1890 |
#287 := (ite #284 #156 #146) |
|
1891 |
#291 := (= #287 #290) |
|
1892 |
#292 := [rewrite]: #291 |
|
1893 |
#288 := (= #161 #287) |
|
1894 |
#285 := (iff #149 #284) |
|
1895 |
#286 := [rewrite]: #285 |
|
1896 |
#289 := [monotonicity #286]: #288 |
|
1897 |
#294 := [trans #289 #292]: #293 |
|
1898 |
#297 := [monotonicity #294]: #296 |
|
1899 |
#305 := [trans #297 #303]: #304 |
|
1900 |
#389 := [monotonicity #305 #386]: #388 |
|
1901 |
#327 := (iff #143 #324) |
|
1902 |
#318 := (< #313 #97) |
|
1903 |
#325 := (iff #318 #324) |
|
1904 |
#326 := [rewrite]: #325 |
|
1905 |
#319 := (iff #143 #318) |
|
1906 |
#316 := (= #140 #313) |
|
1907 |
#307 := (not #306) |
|
1908 |
#310 := (ite #307 #135 #125) |
|
1909 |
#314 := (= #310 #313) |
|
1910 |
#315 := [rewrite]: #314 |
|
1911 |
#311 := (= #140 #310) |
|
1912 |
#308 := (iff #128 #307) |
|
1913 |
#309 := [rewrite]: #308 |
|
1914 |
#312 := [monotonicity #309]: #311 |
|
1915 |
#317 := [trans #312 #315]: #316 |
|
1916 |
#320 := [monotonicity #317]: #319 |
|
1917 |
#328 := [trans #320 #326]: #327 |
|
1918 |
#392 := [monotonicity #328 #389]: #391 |
|
1919 |
#350 := (iff #121 #347) |
|
1920 |
#341 := (< #336 #97) |
|
1921 |
#348 := (iff #341 #347) |
|
1922 |
#349 := [rewrite]: #348 |
|
1923 |
#342 := (iff #121 #341) |
|
1924 |
#339 := (= #118 #336) |
|
1925 |
#330 := (not #329) |
|
1926 |
#333 := (ite #330 #113 #103) |
|
1927 |
#337 := (= #333 #336) |
|
1928 |
#338 := [rewrite]: #337 |
|
1929 |
#334 := (= #118 #333) |
|
1930 |
#331 := (iff #106 #330) |
|
1931 |
#332 := [rewrite]: #331 |
|
1932 |
#335 := [monotonicity #332]: #334 |
|
1933 |
#340 := [trans #335 #338]: #339 |
|
1934 |
#343 := [monotonicity #340]: #342 |
|
1935 |
#351 := [trans #343 #349]: #350 |
|
1936 |
#395 := [monotonicity #351 #392]: #394 |
|
1937 |
#373 := (iff #100 #370) |
|
1938 |
#364 := (< #359 #97) |
|
1939 |
#371 := (iff #364 #370) |
|
1940 |
#372 := [rewrite]: #371 |
|
1941 |
#365 := (iff #100 #364) |
|
1942 |
#362 := (= #93 #359) |
|
1943 |
#353 := (not #352) |
|
1944 |
#356 := (ite #353 #88 #78) |
|
1945 |
#360 := (= #356 #359) |
|
1946 |
#361 := [rewrite]: #360 |
|
1947 |
#357 := (= #93 #356) |
|
1948 |
#354 := (iff #81 #353) |
|
1949 |
#355 := [rewrite]: #354 |
|
1950 |
#358 := [monotonicity #355]: #357 |
|
1951 |
#363 := [trans #358 #361]: #362 |
|
1952 |
#366 := [monotonicity #363]: #365 |
|
1953 |
#374 := [trans #366 #372]: #373 |
|
1954 |
#398 := [monotonicity #374 #395]: #397 |
|
1955 |
#403 := [trans #398 #401]: #402 |
|
1956 |
#406 := [monotonicity #403]: #405 |
|
1957 |
#432 := [monotonicity #406 #429]: #431 |
|
1958 |
#435 := [quant-intro #432]: #434 |
|
1959 |
#438 := [monotonicity #435]: #437 |
|
1960 |
#242 := (iff #64 #241) |
|
1961 |
#239 := (iff #63 #238) |
|
1962 |
#236 := (iff #62 #233) |
|
1963 |
#229 := (implies #204 #226) |
|
1964 |
#234 := (iff #229 #233) |
|
1965 |
#235 := [rewrite]: #234 |
|
1966 |
#230 := (iff #62 #229) |
|
1967 |
#227 := (iff #61 #226) |
|
1968 |
#224 := (= #60 #223) |
|
1969 |
#209 := (= #57 #208) |
|
1970 |
#210 := [rewrite]: #209 |
|
1971 |
#221 := (= #59 #218) |
|
1972 |
#214 := (- #208) |
|
1973 |
#219 := (= #214 #218) |
|
1974 |
#220 := [rewrite]: #219 |
|
1975 |
#215 := (= #59 #214) |
|
1976 |
#216 := [monotonicity #210]: #215 |
|
1977 |
#222 := [trans #216 #220]: #221 |
|
1978 |
#212 := (iff #58 #211) |
|
1979 |
#213 := [monotonicity #210]: #212 |
|
1980 |
#225 := [monotonicity #213 #222 #210]: #224 |
|
1981 |
#228 := [monotonicity #225]: #227 |
|
1982 |
#205 := (iff #56 #204) |
|
1983 |
#202 := (iff #55 #201) |
|
1984 |
#199 := (iff #54 #198) |
|
1985 |
#196 := (iff #53 #195) |
|
1986 |
#193 := (iff #52 #190) |
|
1987 |
#187 := (and #184 #51) |
|
1988 |
#191 := (iff #187 #190) |
|
1989 |
#192 := [rewrite]: #191 |
|
1990 |
#188 := (iff #52 #187) |
|
1991 |
#185 := (iff #42 #184) |
|
1992 |
#98 := (= #17 #97) |
|
1993 |
#99 := [rewrite]: #98 |
|
1994 |
#182 := (= #41 #181) |
|
1995 |
#168 := (= #38 #167) |
|
1996 |
#169 := [rewrite]: #168 |
|
1997 |
#179 := (= #40 #176) |
|
1998 |
#173 := (- #167) |
|
1999 |
#177 := (= #173 #176) |
|
2000 |
#178 := [rewrite]: #177 |
|
2001 |
#174 := (= #40 #173) |
|
2002 |
#175 := [monotonicity #169]: #174 |
|
2003 |
#180 := [trans #175 #178]: #179 |
|
2004 |
#171 := (iff #39 #170) |
|
2005 |
#172 := [monotonicity #169]: #171 |
|
2006 |
#183 := [monotonicity #172 #180 #169]: #182 |
|
2007 |
#186 := [monotonicity #183 #99]: #185 |
|
2008 |
#189 := [monotonicity #186]: #188 |
|
2009 |
#194 := [trans #189 #192]: #193 |
|
2010 |
#165 := (iff #37 #164) |
|
2011 |
#162 := (= #36 #161) |
|
2012 |
#147 := (= #33 #146) |
|
2013 |
#148 := [rewrite]: #147 |
|
2014 |
#159 := (= #35 #156) |
|
2015 |
#152 := (- #146) |
|
2016 |
#157 := (= #152 #156) |
|
2017 |
#158 := [rewrite]: #157 |
|
2018 |
#153 := (= #35 #152) |
|
2019 |
#154 := [monotonicity #148]: #153 |
|
2020 |
#160 := [trans #154 #158]: #159 |
|
2021 |
#150 := (iff #34 #149) |
|
2022 |
#151 := [monotonicity #148]: #150 |
|
2023 |
#163 := [monotonicity #151 #160 #148]: #162 |
|
2024 |
#166 := [monotonicity #163 #99]: #165 |
|
2025 |
#197 := [monotonicity #166 #194]: #196 |
|
2026 |
#144 := (iff #31 #143) |
|
2027 |
#141 := (= #30 #140) |
|
2028 |
#126 := (= #27 #125) |
|
2029 |
#127 := [rewrite]: #126 |
|
2030 |
#138 := (= #29 #135) |
|
2031 |
#131 := (- #125) |
|
2032 |
#136 := (= #131 #135) |
|
2033 |
#137 := [rewrite]: #136 |
|
2034 |
#132 := (= #29 #131) |
|
2035 |
#133 := [monotonicity #127]: #132 |
|
2036 |
#139 := [trans #133 #137]: #138 |
|
2037 |
#129 := (iff #28 #128) |
|
2038 |
#130 := [monotonicity #127]: #129 |
|
2039 |
#142 := [monotonicity #130 #139 #127]: #141 |
|
2040 |
#145 := [monotonicity #142 #99]: #144 |
|
2041 |
#200 := [monotonicity #145 #197]: #199 |
|
2042 |
#122 := (iff #24 #121) |
|
2043 |
#119 := (= #23 #118) |
|
2044 |
#104 := (= #20 #103) |
|
2045 |
#105 := [rewrite]: #104 |
|
2046 |
#116 := (= #22 #113) |
|
2047 |
#109 := (- #103) |
|
2048 |
#114 := (= #109 #113) |
|
2049 |
#115 := [rewrite]: #114 |
|
2050 |
#110 := (= #22 #109) |
|
2051 |
#111 := [monotonicity #105]: #110 |
|
2052 |
#117 := [trans #111 #115]: #116 |
|
2053 |
#107 := (iff #21 #106) |
|
2054 |
#108 := [monotonicity #105]: #107 |
|
2055 |
#120 := [monotonicity #108 #117 #105]: #119 |
|
2056 |
#123 := [monotonicity #120 #99]: #122 |
|
2057 |
#203 := [monotonicity #123 #200]: #202 |
|
2058 |
#101 := (iff #18 #100) |
|
2059 |
#94 := (= #14 #93) |
|
2060 |
#79 := (= #10 #78) |
|
2061 |
#80 := [rewrite]: #79 |
|
2062 |
#91 := (= #13 #88) |
|
2063 |
#84 := (- #78) |
|
2064 |
#89 := (= #84 #88) |
|
2065 |
#90 := [rewrite]: #89 |
|
2066 |
#85 := (= #13 #84) |
|
2067 |
#86 := [monotonicity #80]: #85 |
|
2068 |
#92 := [trans #86 #90]: #91 |
|
2069 |
#82 := (iff #12 #81) |
|
2070 |
#83 := [monotonicity #80]: #82 |
|
2071 |
#95 := [monotonicity #83 #92 #80]: #94 |
|
2072 |
#102 := [monotonicity #95 #99]: #101 |
|
2073 |
#206 := [monotonicity #102 #203]: #205 |
|
2074 |
#231 := [monotonicity #206 #228]: #230 |
|
2075 |
#237 := [trans #231 #235]: #236 |
|
2076 |
#240 := [quant-intro #237]: #239 |
|
2077 |
#243 := [monotonicity #240]: #242 |
|
2078 |
#440 := [trans #243 #438]: #439 |
|
2079 |
#75 := [asserted]: #64 |
|
2080 |
#441 := [mp #75 #440]: #436 |
|
2081 |
#511 := [mp~ #441 #508]: #506 |
|
2082 |
#512 := [mp #511 #641]: #639 |
|
2083 |
#513 := [not-or-elim #512]: #599 |
|
2084 |
#642 := [and-elim #513]: #278 |
|
2085 |
#644 := [and-elim #513]: #494 |
|
2086 |
#891 := (+ #488 #491) |
|
2087 |
#892 := (<= #891 0::real) |
|
2088 |
#720 := (= #488 #490) |
|
2089 |
#743 := (not #614) |
|
2090 |
#741 := (= #607 #621) |
|
2091 |
#884 := (not #741) |
|
2092 |
#748 := (+ #607 #624) |
|
2093 |
#750 := (>= #748 0::real) |
|
2094 |
#778 := (not #750) |
|
2095 |
#754 := (+ #538 #555) |
|
2096 |
#755 := (<= #754 0::real) |
|
2097 |
#777 := (not #755) |
|
2098 |
#753 := (+ #573 #584) |
|
2099 |
#756 := (<= #753 0::real) |
|
2100 |
#735 := (= #573 #581) |
|
2101 |
#736 := (not #574) |
|
2102 |
#773 := [hypothesis]: #750 |
|
2103 |
#837 := (or #736 #778) |
|
2104 |
#648 := [and-elim #513]: #533 |
|
2105 |
#645 := [and-elim #513]: #498 |
|
2106 |
#729 := (not #545) |
|
2107 |
#727 := (= #538 #552) |
|
2108 |
#814 := (not #727) |
|
2109 |
#767 := [hypothesis]: #574 |
|
2110 |
#802 := (or #777 #778 #736) |
|
2111 |
#763 := (+ #176 #275) |
|
2112 |
#764 := (<= #763 0::real) |
|
2113 |
#708 := (= #176 #267) |
|
2114 |
#757 := (+ #469 #473) |
|
2115 |
#758 := (<= #757 0::real) |
|
2116 |
#714 := (= #469 #472) |
|
2117 |
#715 := (not #471) |
|
2118 |
#774 := [hypothesis]: #755 |
|
2119 |
#788 := (or #715 #777 #778 #736) |
|
2120 |
#766 := [hypothesis]: #471 |
|
2121 |
#779 := (or #261 #736 #777 #778 #715) |
|
2122 |
#649 := [and-elim #513]: #564 |
|
2123 |
#650 := [and-elim #513]: #593 |
|
2124 |
#751 := (+ #567 #584) |
|
2125 |
#752 := (<= #751 0::real) |
|
2126 |
#734 := (= #567 #581) |
|
2127 |
#737 := (or #736 #734) |
|
2128 |
#738 := [def-axiom]: #737 |
|
2129 |
#768 := [unit-resolution #738 #767]: #734 |
|
2130 |
#769 := (not #734) |
|
2131 |
#770 := (or #769 #752) |
|
2132 |
#771 := [th-lemma]: #770 |
|
2133 |
#772 := [unit-resolution #771 #768]: #752 |
|
2134 |
#651 := [not-or-elim #512]: #630 |
|
2135 |
#775 := [hypothesis]: #260 |
|
2136 |
#647 := [and-elim #513]: #521 |
|
2137 |
#776 := [th-lemma #767 #647 #775 #774 #645 #773 #651 #772 #650 #649 #766]: false |
|
2138 |
#780 := [lemma #776]: #779 |
|
2139 |
#781 := [unit-resolution #780 #766 #774 #773 #767]: #261 |
|
2140 |
#711 := (or #260 #708) |
|
2141 |
#712 := [def-axiom]: #711 |
|
2142 |
#782 := [unit-resolution #712 #781]: #708 |
|
2143 |
#783 := (not #708) |
|
2144 |
#784 := (or #783 #764) |
|
2145 |
#785 := [th-lemma]: #784 |
|
2146 |
#786 := [unit-resolution #785 #782]: #764 |
|
2147 |
#787 := [th-lemma #647 #774 #645 #773 #651 #649 #786 #642 #781 #766]: false |
|
2148 |
#789 := [lemma #787]: #788 |
|
2149 |
#761 := [unit-resolution #789 #774 #773 #767]: #715 |
|
2150 |
#718 := (or #471 #714) |
|
2151 |
#719 := [def-axiom]: #718 |
|
2152 |
#762 := [unit-resolution #719 #761]: #714 |
|
2153 |
#765 := (not #714) |
|
2154 |
#790 := (or #765 #758) |
|
2155 |
#791 := [th-lemma]: #790 |
|
2156 |
#792 := [unit-resolution #791 #762]: #758 |
|
2157 |
#643 := [and-elim #513]: #476 |
|
2158 |
#795 := (not #758) |
|
2159 |
#794 := (not #498) |
|
2160 |
#793 := (not #521) |
|
2161 |
#796 := (or #261 #471 #793 #777 #794 #778 #633 #561 #795 #475) |
|
2162 |
#797 := [th-lemma]: #796 |
|
2163 |
#798 := [unit-resolution #797 #761 #643 #645 #647 #649 #651 #773 #774 #792]: #261 |
|
2164 |
#799 := [unit-resolution #712 #798]: #708 |
|
2165 |
#800 := [unit-resolution #785 #799]: #764 |
|
2166 |
#801 := [th-lemma #647 #774 #645 #773 #651 #649 #792 #643 #642 #800]: false |
|
2167 |
#803 := [lemma #801]: #802 |
|
2168 |
#826 := [unit-resolution #803 #767 #773]: #777 |
|
2169 |
#815 := (or #814 #755) |
|
2170 |
#804 := [hypothesis]: #777 |
|
2171 |
#805 := [hypothesis]: #727 |
|
2172 |
#816 := [th-lemma]: #815 |
|
2173 |
#817 := [unit-resolution #816 #805 #804]: false |
|
2174 |
#818 := [lemma #817]: #815 |
|
2175 |
#833 := [unit-resolution #818 #826]: #814 |
|
2176 |
#730 := (or #729 #727) |
|
2177 |
#731 := [def-axiom]: #730 |
|
2178 |
#834 := [unit-resolution #731 #833]: #729 |
|
2179 |
#831 := (or #260 #545 #778) |
|
2180 |
#806 := [hypothesis]: #261 |
|
2181 |
#810 := [hypothesis]: #729 |
|
2182 |
#812 := (or #545 #795 #778 #260) |
|
2183 |
#807 := [unit-resolution #712 #806]: #708 |
|
2184 |
#808 := [unit-resolution #785 #807]: #764 |
|
2185 |
#809 := [hypothesis]: #758 |
|
2186 |
#811 := [th-lemma #810 #645 #809 #643 #647 #773 #651 #808 #642 #806]: false |
|
2187 |
#813 := [lemma #811]: #812 |
|
2188 |
#827 := [unit-resolution #813 #806 #773 #810]: #795 |
|
2189 |
#821 := [hypothesis]: #795 |
|
2190 |
#822 := [hypothesis]: #714 |
|
2191 |
#823 := [unit-resolution #791 #822 #821]: false |
|
2192 |
#824 := [lemma #823]: #790 |
|
2193 |
#828 := [unit-resolution #824 #827]: #765 |
|
2194 |
#829 := [unit-resolution #719 #828]: #471 |
|
2195 |
#830 := [th-lemma #808 #642 #829 #810 #645 #647 #773 #651 #806]: false |
|
2196 |
#832 := [lemma #830]: #831 |
|
2197 |
#835 := [unit-resolution #832 #834 #773]: #260 |
|
2198 |
#836 := [th-lemma #767 #835 #834 #645 #648]: false |
|
2199 |
#838 := [lemma #836]: #837 |
|
2200 |
#863 := [unit-resolution #838 #773]: #736 |
|
2201 |
#739 := (or #574 #735) |
|
2202 |
#740 := [def-axiom]: #739 |
|
2203 |
#864 := [unit-resolution #740 #863]: #735 |
|
2204 |
#865 := (not #735) |
|
2205 |
#866 := (or #865 #756) |
|
2206 |
#867 := [th-lemma]: #866 |
|
2207 |
#868 := [unit-resolution #867 #864]: #756 |
|
2208 |
#852 := (or #260 #778) |
|
2209 |
#845 := [unit-resolution #832 #806 #773]: #545 |
|
2210 |
#846 := [unit-resolution #731 #845]: #727 |
|
2211 |
#847 := [unit-resolution #818 #846]: #755 |
|
2212 |
#840 := (not #764) |
|
2213 |
#841 := (or #795 #777 #778 #840) |
|
2214 |
#825 := [hypothesis]: #764 |
|
2215 |
#839 := [th-lemma #774 #645 #647 #773 #651 #809 #643 #825 #642 #649]: false |
|
2216 |
#842 := [lemma #839]: #841 |
|
2217 |
#848 := [unit-resolution #842 #847 #773 #808]: #795 |
|
2218 |
#849 := [unit-resolution #824 #848]: #765 |
|
2219 |
#850 := [unit-resolution #719 #849]: #471 |
|
2220 |
#851 := [th-lemma #847 #649 #645 #647 #773 #651 #808 #850 #806 #642]: false |
|
2221 |
#853 := [lemma #851]: #852 |
|
2222 |
#859 := [unit-resolution #853 #773]: #260 |
|
2223 |
#870 := (or #471 #778) |
|
2224 |
#856 := [hypothesis]: #715 |
|
2225 |
#857 := [unit-resolution #719 #856]: #714 |
|
2226 |
#858 := [unit-resolution #824 #857]: #758 |
|
2227 |
#860 := [unit-resolution #797 #858 #643 #645 #647 #649 #651 #773 #859 #856]: #777 |
|
2228 |
#861 := [unit-resolution #818 #860]: #814 |
|
2229 |
#862 := [unit-resolution #731 #861]: #729 |
|
2230 |
#869 := [th-lemma #643 #650 #863 #868 #859 #862 #645 #647 #773 #651 #858]: false |
|
2231 |
#871 := [lemma #869]: #870 |
|
2232 |
#855 := [unit-resolution #871 #773]: #471 |
|
2233 |
#872 := (not #756) |
|
2234 |
#873 := (or #777 #590 #574 #872 #561 #261 #794 #793 #778 #633 #715) |
|
2235 |
#874 := [th-lemma]: #873 |
|
2236 |
#875 := [unit-resolution #874 #855 #645 #647 #649 #863 #650 #651 #773 #859 #868]: #777 |
|
2237 |
#876 := (or #545 #261 #794 #793 #778 #633 #715 #590 #574 #872) |
|
2238 |
#877 := [th-lemma]: #876 |
|
2239 |
#878 := [unit-resolution #877 #855 #645 #647 #859 #863 #650 #651 #773 #868]: #545 |
|
2240 |
#879 := [unit-resolution #731 #878]: #727 |
|
2241 |
#880 := [unit-resolution #818 #879 #875]: false |
|
2242 |
#881 := [lemma #880]: #778 |
|
2243 |
#883 := [hypothesis]: #741 |
|
2244 |
#885 := (or #884 #750) |
|
2245 |
#886 := [th-lemma]: #885 |
|
2246 |
#887 := [unit-resolution #886 #883 #881]: false |
|
2247 |
#888 := [lemma #887]: #884 |
|
2248 |
#744 := (or #743 #741) |
|
2249 |
#745 := [def-axiom]: #744 |
|
2250 |
#894 := [unit-resolution #745 #888]: #743 |
|
2251 |
#930 := [hypothesis]: #736 |
|
2252 |
#935 := (or #489 #574) |
|
2253 |
#931 := [unit-resolution #740 #930]: #735 |
|
2254 |
#893 := [hypothesis]: #872 |
|
2255 |
#915 := [hypothesis]: #735 |
|
2256 |
#916 := [unit-resolution #867 #915 #893]: false |
|
2257 |
#917 := [lemma #916]: #866 |
|
2258 |
#932 := [unit-resolution #917 #931]: #756 |
|
2259 |
#749 := (+ #613 #624) |
|
2260 |
#844 := (>= #749 0::real) |
|
2261 |
#742 := (= #613 #621) |
|
2262 |
#746 := (or #614 #742) |
|
2263 |
#747 := [def-axiom]: #746 |
|
2264 |
#895 := [unit-resolution #747 #894]: #742 |
|
2265 |
#896 := (not #742) |
|
2266 |
#897 := (or #896 #844) |
|
2267 |
#898 := [th-lemma]: #897 |
|
2268 |
#899 := [unit-resolution #898 #895]: #844 |
|
2269 |
#913 := (or #872 #260) |
|
2270 |
#900 := [hypothesis]: #756 |
|
2271 |
#646 := [and-elim #513]: #500 |
|
2272 |
#903 := (not #844) |
|
2273 |
#902 := (not #533) |
|
2274 |
#901 := (not #500) |
|
2275 |
#904 := (or #489 #901 #260 #872 #840 #277 #590 #902 #903 #633) |
|
2276 |
#905 := [th-lemma]: #904 |
|
2277 |
#906 := [unit-resolution #905 #900 #806 #646 #648 #650 #651 #808 #642 #899]: #489 |
|
2278 |
#722 := (not #489) |
|
2279 |
#723 := (or #722 #720) |
|
2280 |
#724 := [def-axiom]: #723 |
|
2281 |
#907 := [unit-resolution #724 #906]: #720 |
|
2282 |
#908 := (not #720) |
|
2283 |
#909 := (or #908 #892) |
|
2284 |
#910 := [th-lemma]: #909 |
|
2285 |
#911 := [unit-resolution #910 #907]: #892 |
|
2286 |
#912 := [th-lemma #911 #646 #900 #808 #650 #648 #899 #651 #644 #642]: false |
|
2287 |
#914 := [lemma #912]: #913 |
|
2288 |
#890 := [unit-resolution #914 #806]: #872 |
|
2289 |
#918 := [unit-resolution #917 #890]: #865 |
|
2290 |
#919 := [unit-resolution #740 #918]: #574 |
|
2291 |
#920 := (or #489 #901 #260 #902 #903 #633 #840 #277 #736) |
|
2292 |
#921 := [th-lemma]: #920 |
|
2293 |
#922 := [unit-resolution #921 #806 #642 #646 #648 #919 #651 #808 #899]: #489 |
|
2294 |
#923 := [unit-resolution #724 #922]: #720 |
|
2295 |
#924 := [unit-resolution #910 #923]: #892 |
|
2296 |
#925 := [th-lemma #924 #646 #806 #648 #899 #651 #808 #919 #644 #642]: false |
|
2297 |
#926 := [lemma #925]: #260 |
|
2298 |
#933 := [hypothesis]: #722 |
|
2299 |
#934 := [th-lemma #646 #933 #926 #648 #899 #651 #932 #650 #930]: false |
|
2300 |
#936 := [lemma #934]: #935 |
|
2301 |
#927 := [unit-resolution #936 #930]: #489 |
|
2302 |
#928 := [unit-resolution #724 #927]: #720 |
|
2303 |
#929 := [unit-resolution #910 #928]: #892 |
|
2304 |
#937 := [th-lemma #929 #644 #926 #932 #650 #646 #648 #899 #651 #927]: false |
|
2305 |
#938 := [lemma #937]: #574 |
|
2306 |
#940 := (or #489 #261 #614 #901 #902 #736) |
|
2307 |
#941 := [th-lemma]: #940 |
|
2308 |
#942 := [unit-resolution #941 #926 #646 #648 #938 #894]: #489 |
|
2309 |
#943 := [unit-resolution #724 #942]: #720 |
|
2310 |
#944 := [unit-resolution #910 #943]: #892 |
|
2311 |
#760 := (+ #167 #275) |
|
2312 |
#819 := (<= #760 0::real) |
|
2313 |
#707 := (= #167 #267) |
|
2314 |
#709 := (or #261 #707) |
|
2315 |
#710 := [def-axiom]: #709 |
|
2316 |
#945 := [unit-resolution #710 #926]: #707 |
|
2317 |
#946 := (not #707) |
|
2318 |
#947 := (or #946 #819) |
|
2319 |
#948 := [th-lemma]: #947 |
|
2320 |
#949 := [unit-resolution #948 #945]: #819 |
|
2321 |
[th-lemma #926 #949 #646 #648 #899 #651 #938 #944 #644 #642]: false |
|
2322 |
unsat |