Some proofs of validity using Z3 SMT 2.0 online -

-

lemma: forall x : r, x <> 0 -> (x / x) = 1.

proof:

(declare-const x real) (push) (assert (or (> x 0) (< x 0))) (assert (not (= (/ x x) 1))) (check-sat)

and output : 

unsat

qed.

lemma: forall x y : r, x <> 0, y <> 0 -> (x / x + y / y) = 2.

proof:

(declare-const x real) (declare-const y real) (push) (assert (or (> x 0) (< x 0))) (assert (or (> y 0) (< y 0))) (assert (not (= (+ (/ x x) (/ y y)) 2))) (check-sat)

and output is:

unsat

qed.

lemma: forall x y : r, x <> 0, y <> 0 -> (x / x + x / y) = ((x + y) / y).

proof:

(declare-const x real) (declare-const y real) (push) (assert (or (> x 0) (< x 0))) (assert (or (> y 0) (< y 0))) (assert (not (= (+ (/ x x) (/ x y)) (/ (+ x y) y)))) (check-sat)

and output is:

unsat

qed.

these lemmas proved using coq + maple at

http://coq.inria.fr/v8.2pl1/contribs/maplemode.examples.html

and using z3py online at

some proofs of validity using z3py online , strategy proposed nikolaj bjorner

please let me know if proofs z3 smt 2.0 correct , if know more direct form prove them using z3 smt 2.0. many thanks.

there nothing wrong encodings. may consider following encoding closer lemmas trying prove (also available online here):

(assert (not (forall ((x real)) (=> (not (= x 0)) (= (/ x x) 1))))) (check-sat)  (reset) (assert (not (forall ((x real) (y real)) (=> (and (not (= x 0))                                                   (not (= y 0)))                                              (= (+ (/ x x) (/ y y)) 2))))) (check-sat)  (reset) (assert (not (forall ((x real) (y real)) (=> (and (not (= x 0))                                                   (not (= y 0)))                                              (= (+ (/ x x) (/ x y)) (/ (+ x y) y)))))) (check-sat)

Comments

Post a Comment

Popular posts from this blog

Perl - how to grep a block of text from a file -

-
it can in xml or text format. how in general grep block of text in perl? <track type="ws"> <range> <rangestart>0</rangestart> <rangeend>146.912</rangeend> <locationindex>0</locationindex> <propertyindex>0</propertyindex> </range> </track> <track type="ps" id="1"> <range> <rangestart>0</rangestart> <rangeend>146.912</rangeend> <locationindex>1</locationindex> <propertyindex>1</propertyindex> </range> </track> i want grep type="ps" , till </range> . one solution open file, read line line , match block. open(fh, "file.txt"); foreach $line (<fh>) { if ($line =~ m/type="cc"(.*?)<\/range>/) { print $1; } } but there more optimal solution without reading file line l
Read more

delphi - How to remove all the grips on a coolbar if I have several coolbands? -

-
Image
if set mycoolbar.fixedorder true,only grip on first band hidden. well,if use delphi 7 create vcl forms application,then put coolbar on , create 3 coolbans hold other controls,only grip , top coolbands can hidden setting mycoolbar.fixedorder:=true. i've uploaded picture make things clear. you got fixedorder property wrong. fixed property not allow bands rearranged if set true . setting property of coolbar true keep user changing bands order @ runtime, user can still move , resize bands. can give advice can do, actual solution problem, well, have wait answer. my advice use 3 coolbars in row , setting "fixedorder" property true , bandborderstyle bsnone . way grip hidden on of them. about property, it's not bug of ide, actual preference of property.
Read more

javascript - Animating array of divs; only the final element is modified -

-
this baffling me @ moment. i'm experienced programmer looking throw bit of surprise fiancee on countdown page our wedding. desired effect simulated confetti falling behind main page. setup follows: i have array of divs in javascript. each div absolutely positioned on page. have interval set updates every 50 or milliseconds. on each tick, run loop on array of divs, , calculations , update positions. problem problem having, however, though can see divs created, stored array, , modified (in case, each has slight randomized rotation) during initialization phase, once tick update position starts, div stored in whatever last slot of array gets position updated. tried hard-coding each div index testing purposes, strictly last element update position. upon printing current "left" , "top" style values each div before , after calculations shows value has been changed, no visible change noticeable. here's basic code: javascript var container;
Read more