author | boehmes |
Tue, 20 Oct 2009 10:11:30 +0200 | |
changeset 33010 | 39f73a59e855 |
permissions | -rw-r--r-- |
33010 | 1 |
(benchmark Isabelle |
2 |
:extrafuns ( |
|
3 |
(uf_1 BitVec[2] Int) |
|
4 |
) |
|
5 |
:assumption (= (uf_1 bv0[2]) 0) |
|
6 |
:assumption (= (uf_1 bv1[2]) 1) |
|
7 |
:assumption (= (uf_1 bv2[2]) 2) |
|
8 |
:assumption (= (uf_1 bv3[2]) 3) |
|
9 |
:assumption (forall (?x1 BitVec[2]) (< 0 (uf_1 ?x1))) |
|
10 |
:assumption (not (forall (?x2 Int) (implies (< ?x2 0) (forall (?x3 BitVec[2]) (< ?x2 (uf_1 ?x3)))))) |
|
11 |
:formula true |
|
12 |
) |