Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT/Examples/cert/z3_mono_01
author blanchet
Mon, 26 Oct 2009 14:57:49 +0100
changeset 33204 79bd3fbf5d61
parent 33010 39f73a59e855
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     1
 
(benchmark Isabelle
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     2
 
:extrasorts ( T2 T13 T12 T11 T10 T9 T8 T7 T6 T5 T4 T1 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     3
 
:extrafuns (
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     4
 
  (uf_37 T13)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     5
 
  (uf_34 T12)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     6
 
  (uf_31 T11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     7
 
  (uf_28 T10)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     8
 
  (uf_25 T9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     9
 
  (uf_22 T8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    10
 
  (uf_19 T7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    11
 
  (uf_16 T6)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    12
 
  (uf_13 T5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    13
 
  (uf_10 T4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    14
 
  (uf_7 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    15
 
  (uf_4 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    16
 
  (uf_36 Int T13 T13)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    17
 
  (uf_33 T13 T12 T12)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    18
 
  (uf_30 T12 T11 T11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    19
 
  (uf_27 T11 T10 T10)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    20
 
  (uf_24 T10 T9 T9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    21
 
  (uf_21 T9 T8 T8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    22
 
  (uf_18 T8 T7 T7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    23
 
  (uf_15 T7 T6 T6)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    24
 
  (uf_12 T6 T5 T5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    25
 
  (uf_9 T5 T4 T4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    26
 
  (uf_6 T4 T1 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    27
 
  (uf_3 T1 T3 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    28
 
 )
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    29
 
:extrapreds (
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    30
 
  (up_35 Int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    31
 
  (up_32 T13)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    32
 
  (up_29 T12)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    33
 
  (up_26 T11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    34
 
  (up_23 T10)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    35
 
  (up_20 T9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    36
 
  (up_17 T8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    37
 
  (up_14 T7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    38
 
  (up_11 T6)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    39
 
  (up_8 T5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    40
 
  (up_5 T4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    41
 
  (up_1 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    42
 
  (up_2 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    43
 
 )
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    44
 
:assumption (forall (?x1 T1) (and (up_1 ?x1) (or (up_2 (uf_3 ?x1 uf_4)) (not (up_2 (uf_3 ?x1 uf_4))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    45
 
:assumption (forall (?x2 T4) (and (up_5 ?x2) (or (up_1 (uf_6 ?x2 uf_7)) (not (up_1 (uf_6 ?x2 uf_7))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    46
 
:assumption (forall (?x3 T5) (and (up_8 ?x3) (or (up_5 (uf_9 ?x3 uf_10)) (not (up_5 (uf_9 ?x3 uf_10))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    47
 
:assumption (forall (?x4 T6) (and (up_11 ?x4) (or (up_8 (uf_12 ?x4 uf_13)) (not (up_8 (uf_12 ?x4 uf_13))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    48
 
:assumption (forall (?x5 T7) (and (up_14 ?x5) (or (up_11 (uf_15 ?x5 uf_16)) (not (up_11 (uf_15 ?x5 uf_16))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    49
 
:assumption (forall (?x6 T8) (and (up_17 ?x6) (or (up_14 (uf_18 ?x6 uf_19)) (not (up_14 (uf_18 ?x6 uf_19))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    50
 
:assumption (forall (?x7 T9) (and (up_20 ?x7) (or (up_17 (uf_21 ?x7 uf_22)) (not (up_17 (uf_21 ?x7 uf_22))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    51
 
:assumption (forall (?x8 T10) (and (up_23 ?x8) (or (up_20 (uf_24 ?x8 uf_25)) (not (up_20 (uf_24 ?x8 uf_25))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    52
 
:assumption (forall (?x9 T11) (and (up_26 ?x9) (or (up_23 (uf_27 ?x9 uf_28)) (not (up_23 (uf_27 ?x9 uf_28))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    53
 
:assumption (forall (?x10 T12) (and (up_29 ?x10) (or (up_26 (uf_30 ?x10 uf_31)) (not (up_26 (uf_30 ?x10 uf_31))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    54
 
:assumption (forall (?x11 T13) (and (up_32 ?x11) (or (up_29 (uf_33 ?x11 uf_34)) (not (up_29 (uf_33 ?x11 uf_34))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    55
 
:assumption (forall (?x12 Int) (and (up_35 ?x12) (or (up_32 (uf_36 ?x12 uf_37)) (not (up_32 (uf_36 ?x12 uf_37))))))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    56
 
:assumption (not (up_35 1))
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    57
 
:formula true
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    58
 
)
isabelle