Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/SMT/Examples/cert/z3_nat_arith_05
author boehmes
Tue, 20 Oct 2009 10:11:30 +0200
changeset 33006 39f73a59e855
permissions -rw-r--r--
added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML) 
     1 (benchmark Isabelle

     2 :extrasorts ( T1)

     3 :extrafuns (

     4   (uf_1 Int T1)

     5   (uf_2 T1 Int)

     6   (uf_3 T1)

     7  )

     8 :assumption (forall (?x1 T1) (= (uf_1 (uf_2 ?x1)) ?x1))

     9 :assumption (forall (?x2 Int) (implies (<= 0 ?x2) (= (uf_2 (uf_1 ?x2)) ?x2)))

    10 :assumption (forall (?x3 Int) (implies (< ?x3 0) (= (uf_2 (uf_1 ?x3)) 0)))

    11 :assumption (not (distinct (uf_1 (+ (uf_2 uf_3) 1)) (uf_1 (+ (uf_2 (uf_1 (* (uf_2 uf_3) 2))) 3)) (uf_1 (- (uf_2 uf_3) (uf_2 uf_3)))))

    12 :formula true

    13 )
wneuper/isa