| No. |
Conjecture |
File |
Proved |
Time |
| 0 |
(!!x y z.
bin_distrib.times x (bin_distrib.plus y z) =
bin_distrib.plus (bin_distrib.times x y) (bin_distrib.times x z))
==> (!!x y z.
bin_distrib.times x (bin_distrib.plus y z) =
bin_distrib.plus (bin_distrib.times x y) (bin_distrib.times x z)) |
bin_distrib.thy |
✗ |
70.620187 |
| 1 |
(!!x y. toNat (bin_plus.plus x y) = plus2 (toNat x) (toNat y))
==> (!!x y. toNat (bin_plus.plus x y) = plus2 (toNat x) (toNat y)) |
bin_plus.thy |
✗ |
71.056965 |
| 2 |
(!!x y z.
bin_plus_assoc.plus x (bin_plus_assoc.plus y z) =
bin_plus_assoc.plus (bin_plus_assoc.plus x y) z)
==> (!!x y z.
bin_plus_assoc.plus x (bin_plus_assoc.plus y z) =
bin_plus_assoc.plus (bin_plus_assoc.plus x y) z) |
bin_plus_assoc.thy |
✗ |
70.355378 |
| 3 |
(!!x y. bin_plus_comm.plus x y = bin_plus_comm.plus y x)
==> (!!x y. bin_plus_comm.plus x y = bin_plus_comm.plus y x) |
bin_plus_comm.thy |
✓ |
13.407736 |
| 4 |
(!!n. toNat (s n) = S (toNat n)) ==> (!!n. toNat (s n) = S (toNat n)) |
bin_s.thy |
✗ |
70.432041 |
| 5 |
(!!x y. toNat (bin_times.times x y) = mult (toNat x) (toNat y))
==> (!!x y. toNat (bin_times.times x y) = mult (toNat x) (toNat y)) |
bin_times.thy |
✗ |
71.212275 |
| 6 |
(!!x y z.
bin_times_assoc.times x (bin_times_assoc.times y z) =
bin_times_assoc.times (bin_times_assoc.times x y) z)
==> (!!x y z.
bin_times_assoc.times x (bin_times_assoc.times y z) =
bin_times_assoc.times (bin_times_assoc.times x y) z) |
bin_times_assoc.thy |
✗ |
70.20727 |
| 7 |
(!!x y. bin_times_comm.times x y = bin_times_comm.times y x)
==> (!!x y. bin_times_comm.times x y = bin_times_comm.times y x) |
bin_times_comm.thy |
✗ |
70.367421 |
| 8 |
(!!xs ys. escape xs = escape ys ==> xs = ys)
==> (!!xs ys. escape xs = escape ys ==> xs = ys) |
escape_Injective.thy |
✗ |
11.337252 |
| 9 |
(!!xs. all (λxa. ok xa) (escape xs))
==> (!!xs. all (λxa. ok xa) (escape xs)) |
escape_NoSpecial.thy |
✓ |
10.200143 |
| 10 |
(!!n x y z.
fermat_last.plus (pow (S x) (S (S (S n)))) (pow (S y) (S (S (S n)))) ≠
pow (S z) (S (S (S n))))
==> (!!n x y z.
fermat_last.plus (pow (S x) (S (S (S n))))
(pow (S y) (S (S (S n)))) ≠
pow (S z) (S (S (S n)))) |
fermat_last.thy |
✗ |
8.443014 |
| 11 |
(!!h. heap h
==> listDeleteMinimum (toList2 h) = maybeToList (deleteMinimum h))
==> (!!h. heap h
==> listDeleteMinimum (toList2 h) = maybeToList (deleteMinimum h)) |
heap_deleteMinimum.thy |
✗ |
71.986352 |
| 12 |
(!!x h. heap h ==> toList2 (insert2 x h) = listInsert x (toList2 h))
==> (!!x h. heap h ==> toList2 (insert2 x h) = listInsert x (toList2 h)) |
heap_insert.thy |
✗ |
71.240061 |
| 13 |
(!!x y.
[| heap x; heap y |]
==> toList2 (merge x y) = mergeLists (toList2 x) (toList2 y))
==> (!!x y.
[| heap x; heap y |]
==> toList2 (merge x y) = mergeLists (toList2 x) (toList2 y)) |
heap_merge.thy |
✗ |
71.822258 |
| 14 |
(!!h. heap h ==> listMinimum (toList2 h) = minimum h)
==> (!!h. heap h ==> listMinimum (toList2 h) = minimum h) |
heap_minimum.thy |
✓ |
12.599195 |
| 15 |
(!!x y. count x (hsort y) = count x y)
==> (!!x y. count x (hsort y) = count x y) |
heap_SortPermutes.thy |
✗ |
71.734746 |
| 16 |
(!!x. ordered (hsort x)) ==> (!!x. ordered (hsort x)) |
heap_SortSorts.thy |
✗ |
71.17349 |
| 17 |
(!!x y z.
int_add_assoc.plus x (int_add_assoc.plus y z) =
int_add_assoc.plus (int_add_assoc.plus x y) z)
==> (!!x y z.
int_add_assoc.plus x (int_add_assoc.plus y z) =
int_add_assoc.plus (int_add_assoc.plus x y) z) |
int_add_assoc.thy |
✗ |
69.228879 |
| 18 |
(!!x y. int_add_comm.plus x y = int_add_comm.plus y x)
==> (!!x y. int_add_comm.plus x y = int_add_comm.plus y x) |
int_add_comm.thy |
✗ |
69.209178 |
| 19 |
(!!x. x = int_add_ident_left.plus zero x)
==> (!!x. x = int_add_ident_left.plus zero x) |
int_add_ident_left.thy |
✓ |
9.072363 |
| 20 |
(!!x. x = int_add_ident_right.plus x zero)
==> (!!x. x = int_add_ident_right.plus x zero) |
int_add_ident_right.thy |
✓ |
9.124087 |
| 21 |
(!!x. int_add_inv_left.plus (neg x) x = zero)
==> (!!x. int_add_inv_left.plus (neg x) x = zero) |
int_add_inv_left.thy |
✓ |
12.38298 |
| 22 |
(!!x. int_add_inv_right.plus x (neg x) = zero)
==> (!!x. int_add_inv_right.plus x (neg x) = zero) |
int_add_inv_right.thy |
✓ |
12.325678 |
| 23 |
(!!x y z.
int_left_distrib.times x (int_left_distrib.plus y z) =
int_left_distrib.plus (int_left_distrib.times x y)
(int_left_distrib.times x z))
==> (!!x y z.
int_left_distrib.times x (int_left_distrib.plus y z) =
int_left_distrib.plus (int_left_distrib.times x y)
(int_left_distrib.times x z)) |
int_left_distrib.thy |
✗ |
70.154126 |
| 24 |
(!!x y z.
int_mul_assoc.times x (int_mul_assoc.times y z) =
int_mul_assoc.times (int_mul_assoc.times x y) z)
==> (!!x y z.
int_mul_assoc.times x (int_mul_assoc.times y z) =
int_mul_assoc.times (int_mul_assoc.times x y) z) |
int_mul_assoc.thy |
✗ |
69.83637 |
| 25 |
(!!x y. int_mul_comm.times x y = int_mul_comm.times y x)
==> (!!x y. int_mul_comm.times x y = int_mul_comm.times y x) |
int_mul_comm.thy |
✗ |
69.786701 |
| 26 |
(!!x. x = int_mul_ident_left.times one x)
==> (!!x. x = int_mul_ident_left.times one x) |
int_mul_ident_left.thy |
✓ |
9.97141 |
| 27 |
(!!x. x = int_mul_ident_right.times x one)
==> (!!x. x = int_mul_ident_right.times x one) |
int_mul_ident_right.thy |
✓ |
10.077942 |
| 28 |
(!!x y z.
int_right_distrib.times (int_right_distrib.plus x y) z =
int_right_distrib.plus (int_right_distrib.times x z)
(int_right_distrib.times y z))
==> (!!x y z.
int_right_distrib.times (int_right_distrib.plus x y) z =
int_right_distrib.plus (int_right_distrib.times x z)
(int_right_distrib.times y z)) |
int_right_distrib.thy |
✗ |
70.178103 |
| 29 |
(!!xs ys zs.
list_append_inj_1.append xs zs = list_append_inj_1.append ys zs
==> xs = ys)
==> (!!xs ys zs.
list_append_inj_1.append xs zs = list_append_inj_1.append ys zs
==> xs = ys) |
list_append_inj_1.thy |
✗ |
8.683961 |
| 30 |
(!!xs ys zs.
list_append_inj_2.append xs ys = list_append_inj_2.append xs zs
==> ys = zs)
==> (!!xs ys zs.
list_append_inj_2.append xs ys = list_append_inj_2.append xs zs
==> ys = zs) |
list_append_inj_2.thy |
✗ |
8.692828 |
| 31 |
(!!m f g. bind (bind m f) g = bind m (λxa. bind (f xa) g))
==> (!!m f g. bind (bind m f) g = bind m (λxa. bind (f xa) g)) |
list_assoc.thy |
✗ |
68.507862 |
| 32 |
(!!f xs. concat2 (map2 f xs) = bind xs f)
==> (!!f xs. concat2 (map2 f xs) = bind xs f) |
list_concat_map_bind.thy |
✓ |
9.293828 |
| 33 |
(!!x xs. elem x xs ==> count x (nub xs) = S Z)
==> (!!x xs. elem x xs ==> count x (nub xs) = S Z) |
list_count_nub.thy |
✗ |
11.727907 |
| 34 |
(!!x xs. deleteAll x xs = delete x xs ==> le (count x xs) (S Z))
==> (!!x xs. deleteAll x xs = delete x xs ==> le (count x xs) (S Z)) |
list_deleteAll_count.thy |
✗ |
9.815629 |
| 35 |
(!!x xs. elem x xs ==> elem x (nub xs))
==> (!!x xs. elem x xs ==> elem x (nub xs)) |
list_elem_nub_l.thy |
✗ |
9.462946 |
| 36 |
(!!x xs. elem x (nub xs) ==> elem x xs)
==> (!!x xs. elem x (nub xs) ==> elem x xs) |
list_elem_nub_r.thy |
✗ |
9.447416 |
| 37 |
(!!xs. interleave (evens xs) (odds xs) = xs)
==> (!!xs. interleave (evens xs) (odds xs) = xs) |
list_Interleave.thy |
✓ |
8.765551 |
| 38 |
(!!xs. nub (nub xs) = nub xs) ==> (!!xs. nub (nub xs) = nub xs) |
list_nub_nub.thy |
✗ |
69.325228 |
| 39 |
(!!xs. list_PairEvens.even (list_PairEvens.length xs)
==> map2 (λxa. list_PairEvens.fst xa) (pairs xs) = evens xs)
==> (!!xs. list_PairEvens.even (list_PairEvens.length xs)
==> map2 (λxa. list_PairEvens.fst xa) (pairs xs) = evens xs) |
list_PairEvens.thy |
✓ |
10.689935 |
| 40 |
(!!xs. map2 (λxa. list_PairOdds.snd xa) (pairs xs) = odds xs)
==> (!!xs. map2 (λxa. list_PairOdds.snd xa) (pairs xs) = odds xs) |
list_PairOdds.thy |
✓ |
9.858202 |
| 41 |
(!!xs. list_PairUnpair.even (list_PairUnpair.length xs)
==> unpair (pairs xs) = xs)
==> (!!xs. list_PairUnpair.even (list_PairUnpair.length xs)
==> unpair (pairs xs) = xs) |
list_PairUnpair.thy |
✗ |
10.892624 |
| 42 |
(!!x xs ys. [| elem x xs; isPermutation xs ys |] ==> elem x ys)
==> (!!x xs ys. [| elem x xs; isPermutation xs ys |] ==> elem x ys) |
list_perm_elem.thy |
✗ |
9.586743 |
| 43 |
(!!xs. isPermutation xs xs) ==> (!!xs. isPermutation xs xs) |
list_perm_refl.thy |
✗ |
69.568857 |
| 44 |
(!!xs ys. isPermutation xs ys ==> isPermutation ys xs)
==> (!!xs ys. isPermutation xs ys ==> isPermutation ys xs) |
list_perm_symm.thy |
✗ |
69.605929 |
| 45 |
(!!xs ys zs.
[| isPermutation xs ys; isPermutation ys zs |] ==> isPermutation xs zs)
==> (!!xs ys zs.
[| isPermutation xs ys; isPermutation ys zs |]
==> isPermutation xs zs) |
list_perm_trans.thy |
✗ |
69.543859 |
| 46 |
(!!x f. bind (return x) f = f x) ==> (!!x f. bind (return x) f = f x) |
list_return_1.thy |
✗ |
8.778336 |
| 47 |
(!!xs. bind xs (λxa. return xa) = xs)
==> (!!xs. bind xs (λxa. return xa) = xs) |
list_return_2.thy |
✓ |
8.720329 |
| 48 |
(!!xs. map2 (λxa. list_Select.fst xa) (select2 xs) = xs)
==> (!!xs. map2 (λxa. list_Select.fst xa) (select2 xs) = xs) |
list_Select.thy |
✓ |
9.742031 |
| 49 |
(!!xs. all (λxa. zisPermutation xa xs)
(propSelectPermutations (select2 xs)))
==> (!!xs. all (λxa. zisPermutation xa xs)
(propSelectPermutations (select2 xs))) |
list_SelectPermutations.thy |
✓ |
10.492546 |
| 50 |
(!!f xs. weirdconcat (map2 f xs) = bind xs f)
==> (!!f xs. weirdconcat (map2 f xs) = bind xs f) |
list_weird_concat_map_bind.thy |
✗ |
69.309976 |
| 51 |
(!!x. concat2 x = weirdconcat x) ==> (!!x. concat2 x = weirdconcat x) |
list_weird_is_normal.thy |
✓ |
9.131987 |
| 52 |
(!!x xs. zelem x xs ==> zcount x (znub xs) = S Z)
==> (!!x xs. zelem x xs ==> zcount x (znub xs) = S Z) |
list_z_count_nub.thy |
✗ |
69.536755 |
| 53 |
(!!x xs. zdeleteAll x xs = zdelete x xs ==> le (zcount x xs) (S Z))
==> (!!x xs. zdeleteAll x xs = zdelete x xs ==> le (zcount x xs) (S Z)) |
list_z_deleteAll_count.thy |
✗ |
69.494176 |
| 54 |
(!!x xs. zelem x xs ==> zelem x (znub xs))
==> (!!x xs. zelem x xs ==> zelem x (znub xs)) |
list_z_elem_nub_l.thy |
✗ |
52.480422 |
| 55 |
(!!x xs. zelem x (znub xs) ==> zelem x xs)
==> (!!x xs. zelem x (znub xs) ==> zelem x xs) |
list_z_elem_nub_r.thy |
✗ |
11.829751 |
| 56 |
(!!xs. znub (znub xs) = znub xs) ==> (!!xs. znub (znub xs) = znub xs) |
list_z_nub_nub.thy |
✗ |
68.748424 |
| 57 |
(!!x xs ys. [| zelem x xs; zisPermutation xs ys |] ==> zelem x ys)
==> (!!x xs ys. [| zelem x xs; zisPermutation xs ys |] ==> zelem x ys) |
list_z_perm_elem.thy |
✗ |
12.325247 |
| 58 |
(!!xs. zisPermutation xs xs) ==> (!!xs. zisPermutation xs xs) |
list_z_perm_refl.thy |
✓ |
9.072856 |
| 59 |
(!!xs ys. zisPermutation xs ys ==> zisPermutation ys xs)
==> (!!xs ys. zisPermutation xs ys ==> zisPermutation ys xs) |
list_z_perm_symm.thy |
✗ |
69.047113 |
| 60 |
(!!xs ys zs.
[| zisPermutation xs ys; zisPermutation ys zs |]
==> zisPermutation xs zs)
==> (!!xs ys zs.
[| zisPermutation xs ys; zisPermutation ys zs |]
==> zisPermutation xs zs) |
list_z_perm_trans.thy |
✗ |
68.870038 |
| 61 |
(!!n. [| m_dom n; n ≤ 100 |] ==> m n = 91)
==> (!!n. [| m_dom n; n ≤ 100 |] ==> m n = 91) |
mccarthy91_M1.thy |
✗ |
7.330986 |
| 62 |
(!!n. [| m_dom n; 101 ≤ n |] ==> m n = n - 10)
==> (!!n. [| m_dom n; 101 ≤ n |] ==> m n = n - 10) |
mccarthy91_M2.thy |
✗ |
7.339755 |
| 63 |
(!!m n. mod2_dom (m, n) ==> mod2 m n = modstructural m n)
==> (!!m n. mod2_dom (m, n) ==> mod2 m n = modstructural m n) |
mod_same.thy |
✗ |
27.959979 |
| 64 |
(!!x y z. accaltmul x (accaltmul y z) = accaltmul (accaltmul x y) z)
==> (!!x y z. accaltmul x (accaltmul y z) = accaltmul (accaltmul x y) z) |
nat_acc_alt_mul_assoc.thy |
✗ |
68.084091 |
| 65 |
(!!x y. accaltmul x y = accaltmul y x)
==> (!!x y. accaltmul x y = accaltmul y x) |
nat_acc_alt_mul_comm.thy |
✗ |
68.126302 |
| 66 |
(!!x y. accaltmul x y = mult x y) ==> (!!x y. accaltmul x y = mult x y) |
nat_acc_alt_mul_same.thy |
✗ |
68.397341 |
| 67 |
(!!x y z. accplus x (accplus y z) = accplus (accplus x y) z)
==> (!!x y z. accplus x (accplus y z) = accplus (accplus x y) z) |
nat_acc_plus_assoc.thy |
✗ |
67.978796 |
| 68 |
(!!x y. accplus x y = accplus y x) ==> (!!x y. accplus x y = accplus y x) |
nat_acc_plus_comm.thy |
✗ |
67.893249 |
| 69 |
(!!x y. nat_acc_plus_same.plus x y = accplus x y)
==> (!!x y. nat_acc_plus_same.plus x y = accplus x y) |
nat_acc_plus_same.thy |
✓ |
8.297949 |
| 70 |
(!!x y z. altmul x (altmul y z) = altmul (altmul x y) z)
==> (!!x y z. altmul x (altmul y z) = altmul (altmul x y) z) |
nat_alt_mul_assoc.thy |
✗ |
68.024493 |
| 71 |
(!!x y. altmul x y = altmul y x) ==> (!!x y. altmul x y = altmul y x) |
nat_alt_mul_comm.thy |
✗ |
68.020639 |
| 72 |
(!!x y. altmul x y = mult x y) ==> (!!x y. altmul x y = mult x y) |
nat_alt_mul_same.thy |
✗ |
68.077371 |
| 73 |
(!!x y. [| ge x y; ge y x |] ==> x = y)
==> (!!x y. [| ge x y; ge y x |] ==> x = y) |
nat_boring_ge_antisym.thy |
✗ |
7.934434 |
| 74 |
(!!x. ge x x) ==> (!!x. ge x x) |
nat_boring_ge_reflexive.thy |
✓ |
7.934319 |
| 75 |
(!!x y z. [| ge x y; ge y z |] ==> ge x z)
==> (!!x y z. [| ge x y; ge y z |] ==> ge x z) |
nat_boring_ge_trans.thy |
✗ |
7.945294 |
| 76 |
(!!x y. gt x y ==> ¬ gt y x) ==> (!!x y. gt x y ==> ¬ gt y x) |
nat_boring_gt_asymmetric.thy |
✗ |
7.873347 |
| 77 |
(!!x. ¬ gt x x) ==> (!!x. ¬ gt x x) |
nat_boring_gt_irreflexive.thy |
✓ |
7.960158 |
| 78 |
(!!x y z. [| gt x y; gt y z |] ==> gt x z)
==> (!!x y z. [| gt x y; gt y z |] ==> gt x z) |
nat_boring_gt_trans.thy |
✗ |
7.917797 |
| 79 |
(!!x y. max2 x (min2 x y) = x) ==> (!!x y. max2 x (min2 x y) = x) |
nat_boring_max_min_abs.thy |
✓ |
8.023902 |
| 80 |
(!!x y z. min2 x (max2 y z) = max2 (min2 x y) (min2 x z))
==> (!!x y z. min2 x (max2 y z) = max2 (min2 x y) (min2 x z)) |
nat_boring_max_min_distrib.thy |
✗ |
68.059366 |
| 81 |
(!!x y z. min2 x (min2 y z) = min2 (min2 x y) z)
==> (!!x y z. min2 x (min2 y z) = min2 (min2 x y) z) |
nat_boring_min_assoc.thy |
✗ |
67.901125 |
| 82 |
(!!x y. min2 x y = min2 y x) ==> (!!x y. min2 x y = min2 y x) |
nat_boring_min_comm.thy |
✓ |
8.176305 |
| 83 |
(!!x. min2 x x = x) ==> (!!x. min2 x x = x) |
nat_boring_min_idem.thy |
✓ |
8.198159 |
| 84 |
(!!x. equal2 x x) ==> (!!x. equal2 x x) |
nat_eq_refl.thy |
✓ |
7.901538 |
| 85 |
(!!x y. equal2 x y ==> equal2 y x) ==> (!!x y. equal2 x y ==> equal2 y x) |
nat_eq_sym.thy |
✗ |
7.889388 |
| 86 |
(!!x y z. [| equal2 x y; equal2 y z |] ==> equal2 x z)
==> (!!x y z. [| equal2 x y; equal2 y z |] ==> equal2 x z) |
nat_eq_trans.thy |
✗ |
7.846504 |
| 87 |
(!!x y. [| le x y; le y x |] ==> x = y)
==> (!!x y. [| le x y; le y x |] ==> x = y) |
nat_le_antisym.thy |
✗ |
7.927613 |
| 88 |
(!!x y. [| ge x y; le x y |] ==> equal2 x y)
==> (!!x y. [| ge x y; le x y |] ==> equal2 x y) |
nat_le_ge_eq.thy |
✗ |
8.250954 |
| 89 |
(!!x y. [| le x y; unequal x y |] ==> lt x y)
==> (!!x y. [| le x y; unequal x y |] ==> lt x y) |
nat_le_ne_lt.thy |
✗ |
8.601857 |
| 90 |
(!!x. le x x) ==> (!!x. le x x) |
nat_le_reflexive.thy |
✓ |
7.922905 |
| 91 |
(!!x y z. [| le x y; le y z |] ==> le x z)
==> (!!x y z. [| le x y; le y z |] ==> le x z) |
nat_le_trans.thy |
✗ |
7.903054 |
| 92 |
(!!x y. lt x y ==> ¬ lt y x) ==> (!!x y. lt x y ==> ¬ lt y x) |
nat_lt_asymmetric.thy |
✗ |
7.8529 |
| 93 |
(!!x. ¬ lt x x) ==> (!!x. ¬ lt x x) |
nat_lt_irreflexive.thy |
✓ |
7.896736 |
| 94 |
(!!x y. lt y x ==> unequal x y) ==> (!!x y. lt y x ==> unequal x y) |
nat_lt_ne.thy |
✗ |
8.141907 |
| 95 |
(!!x y z. [| lt x y; lt y z |] ==> lt x z)
==> (!!x y z. [| lt x y; lt y z |] ==> lt x z) |
nat_lt_trans.thy |
✗ |
7.907236 |
| 96 |
(!!x y z. max2 x (max2 y z) = max2 (max2 x y) z)
==> (!!x y z. max2 x (max2 y z) = max2 (max2 x y) z) |
nat_max_assoc.thy |
✗ |
67.89223 |
| 97 |
(!!x y. max2 x y = max2 y x) ==> (!!x y. max2 x y = max2 y x) |
nat_max_comm.thy |
✓ |
7.981254 |
| 98 |
(!!x. max2 x x = x) ==> (!!x. max2 x x = x) |
nat_max_idem.thy |
✓ |
7.782576 |
| 99 |
(!!x y. min2 x (max2 x y) = x) ==> (!!x y. min2 x (max2 x y) = x) |
nat_min_max_abs.thy |
✓ |
8.434682 |
| 100 |
(!!x y z. max2 x (min2 y z) = min2 (max2 x y) (max2 x z))
==> (!!x y z. max2 x (min2 y z) = min2 (max2 x y) (max2 x z)) |
nat_min_max_distrib.thy |
✗ |
68.021566 |
| 101 |
(!!n. lt (pow (S (S Z)) (S (S (S (S n))))) (factorial (S (S (S (S n))))))
==> (!!n. lt (pow (S (S Z)) (S (S (S (S n)))))
(factorial (S (S (S (S n)))))) |
nat_pow_le_factorial.thy |
✗ |
68.369217 |
| 102 |
(!!x. pow (S Z) x = S Z) ==> (!!x. pow (S Z) x = S Z) |
nat_pow_one.thy |
✓ |
7.971004 |
| 103 |
(!!x y z. pow x (mult y z) = pow (pow x y) z)
==> (!!x y z. pow x (mult y z) = pow (pow x y) z) |
nat_pow_pow.thy |
✗ |
68.019903 |
| 104 |
(!!x y z. pow x (nat_pow_times.plus y z) = mult (pow x y) (pow x z))
==> (!!x y z. pow x (nat_pow_times.plus y z) = mult (pow x y) (pow x z)) |
nat_pow_times.thy |
✗ |
68.083406 |
| 105 |
(!!n. cubes n = mult (sum n) (sum n))
==> (!!n. cubes n = mult (sum n) (sum n)) |
nicomachus_theorem.thy |
✗ |
68.187348 |
| 106 |
(!!u v. linS u = linS v ==> u = v) ==> (!!u v. linS u = linS v ==> u = v) |
packrat_unambigPackrat.thy |
✗ |
11.689671 |
| 107 |
(!!n xs. prop_01.append (prop_01.take n xs) (prop_01.drop n xs) = xs)
==> (!!n xs. prop_01.append (prop_01.take n xs) (prop_01.drop n xs) = xs) |
prop_01.thy |
✓ |
9.289484 |
| 108 |
(!!x y.
prop_02.length (prop_02.append x y) =
prop_02.length (prop_02.append y x))
==> (!!x y.
prop_02.length (prop_02.append x y) =
prop_02.length (prop_02.append y x)) |
prop_02.thy |
✓ |
10.247044 |
| 109 |
(!!x y.
prop_03.length (prop_03.append x y) =
prop_03.plus (prop_03.length y) (prop_03.length x))
==> (!!x y.
prop_03.length (prop_03.append x y) =
prop_03.plus (prop_03.length y) (prop_03.length x)) |
prop_03.thy |
✓ |
10.971601 |
| 110 |
(!!x. prop_04.length (prop_04.append x x) = double (prop_04.length x))
==> (!!x. prop_04.length (prop_04.append x x) = double (prop_04.length x)) |
prop_04.thy |
✗ |
69.051087 |
| 111 |
(!!x. prop_05.length (prop_05.rev x) = prop_05.length x)
==> (!!x. prop_05.length (prop_05.rev x) = prop_05.length x) |
prop_05.thy |
✗ |
69.227024 |
| 112 |
(!!x y.
prop_06.length (prop_06.rev (prop_06.append x y)) =
prop_06.plus (prop_06.length x) (prop_06.length y))
==> (!!x y.
prop_06.length (prop_06.rev (prop_06.append x y)) =
prop_06.plus (prop_06.length x) (prop_06.length y)) |
prop_06.thy |
✗ |
69.235099 |
| 113 |
(!!x y.
prop_07.length (qrev x y) =
prop_07.plus (prop_07.length x) (prop_07.length y))
==> (!!x y.
prop_07.length (qrev x y) =
prop_07.plus (prop_07.length x) (prop_07.length y)) |
prop_07.thy |
✓ |
10.841273 |
| 114 |
(!!x y z.
prop_08.drop x (prop_08.drop y z) = prop_08.drop y (prop_08.drop x z))
==> (!!x y z.
prop_08.drop x (prop_08.drop y z) =
prop_08.drop y (prop_08.drop x z)) |
prop_08.thy |
✗ |
68.968932 |
| 115 |
(!!x y z w.
prop_09.drop w (prop_09.drop x (prop_09.drop y z)) =
prop_09.drop y (prop_09.drop x (prop_09.drop w z)))
==> (!!x y z w.
prop_09.drop w (prop_09.drop x (prop_09.drop y z)) =
prop_09.drop y (prop_09.drop x (prop_09.drop w z))) |
prop_09.thy |
✗ |
68.942085 |
| 116 |
(!!x. prop_10.rev (prop_10.rev x) = x)
==> (!!x. prop_10.rev (prop_10.rev x) = x) |
prop_10.thy |
✗ |
68.498543 |
| 117 |
(!!x y.
prop_11.rev (prop_11.append (prop_11.rev x) (prop_11.rev y)) =
prop_11.append y x)
==> (!!x y.
prop_11.rev (prop_11.append (prop_11.rev x) (prop_11.rev y)) =
prop_11.append y x) |
prop_11.thy |
✗ |
68.396319 |
| 118 |
(!!x y. qrev x y = prop_12.append (prop_12.rev x) y)
==> (!!x y. qrev x y = prop_12.append (prop_12.rev x) y) |
prop_12.thy |
✗ |
68.608521 |
| 119 |
(!!x. half (prop_13.plus x x) = x) ==> (!!x. half (prop_13.plus x x) = x) |
prop_13.thy |
✗ |
67.961629 |
| 120 |
(!!x. prop_14.sorted (isort x)) ==> (!!x. prop_14.sorted (isort x)) |
prop_14.thy |
✗ |
69.287165 |
| 121 |
(!!x. prop_15.plus x (S x) = S (prop_15.plus x x))
==> (!!x. prop_15.plus x (S x) = S (prop_15.plus x x)) |
prop_15.thy |
✗ |
67.895212 |
| 122 |
(!!x. prop_16.even (prop_16.plus x x))
==> (!!x. prop_16.even (prop_16.plus x x)) |
prop_16.thy |
✗ |
67.941648 |
| 123 |
(!!x y.
prop_17.rev (prop_17.rev (prop_17.append x y)) =
prop_17.append (prop_17.rev (prop_17.rev x))
(prop_17.rev (prop_17.rev y)))
==> (!!x y.
prop_17.rev (prop_17.rev (prop_17.append x y)) =
prop_17.append (prop_17.rev (prop_17.rev x))
(prop_17.rev (prop_17.rev y))) |
prop_17.thy |
✗ |
68.465462 |
| 124 |
(!!x y.
prop_18.rev (prop_18.append (prop_18.rev x) y) =
prop_18.append (prop_18.rev y) x)
==> (!!x y.
prop_18.rev (prop_18.append (prop_18.rev x) y) =
prop_18.append (prop_18.rev y) x) |
prop_18.thy |
✗ |
68.426053 |
| 125 |
(!!x y.
prop_19.append (prop_19.rev (prop_19.rev x)) y =
prop_19.rev (prop_19.rev (prop_19.append x y)))
==> (!!x y.
prop_19.append (prop_19.rev (prop_19.rev x)) y =
prop_19.rev (prop_19.rev (prop_19.append x y))) |
prop_19.thy |
✗ |
68.450846 |
| 126 |
(!!x. prop_20.even (prop_20.length (prop_20.append x x)))
==> (!!x. prop_20.even (prop_20.length (prop_20.append x x))) |
prop_20.thy |
✗ |
69.101568 |
| 127 |
(!!x y.
prop_21.rotate (prop_21.length x) (prop_21.append x y) =
prop_21.append y x)
==> (!!x y.
prop_21.rotate (prop_21.length x) (prop_21.append x y) =
prop_21.append y x) |
prop_21.thy |
✗ |
69.21474 |
| 128 |
(!!x y.
prop_22.even (prop_22.length (prop_22.append x y)) =
prop_22.even (prop_22.length (prop_22.append y x)))
==> (!!x y.
prop_22.even (prop_22.length (prop_22.append x y)) =
prop_22.even (prop_22.length (prop_22.append y x))) |
prop_22.thy |
✗ |
69.181752 |
| 129 |
(!!x y.
half (prop_23.length (prop_23.append x y)) =
half (prop_23.length (prop_23.append y x)))
==> (!!x y.
half (prop_23.length (prop_23.append x y)) =
half (prop_23.length (prop_23.append y x))) |
prop_23.thy |
✗ |
69.203588 |
| 130 |
(!!x y. prop_24.even (prop_24.plus x y) = prop_24.even (prop_24.plus y x))
==> (!!x y.
prop_24.even (prop_24.plus x y) = prop_24.even (prop_24.plus y x)) |
prop_24.thy |
✗ |
68.042863 |
| 131 |
(!!x y.
prop_25.even (prop_25.length (prop_25.append x y)) =
prop_25.even (prop_25.plus (prop_25.length y) (prop_25.length x)))
==> (!!x y.
prop_25.even (prop_25.length (prop_25.append x y)) =
prop_25.even (prop_25.plus (prop_25.length y) (prop_25.length x))) |
prop_25.thy |
✗ |
69.296705 |
| 132 |
(!!x y. half (prop_26.plus x y) = half (prop_26.plus y x))
==> (!!x y. half (prop_26.plus x y) = half (prop_26.plus y x)) |
prop_26.thy |
✗ |
67.989569 |
| 133 |
(!!x. prop_27.rev x = qrev x nil2) ==> (!!x. prop_27.rev x = qrev x nil2) |
prop_27.thy |
✗ |
68.616078 |
| 134 |
(!!x. revflat x = qrevflat x nil2) ==> (!!x. revflat x = qrevflat x nil2) |
prop_28.thy |
✗ |
68.745544 |
| 135 |
(!!x. prop_29.rev (qrev x nil2) = x)
==> (!!x. prop_29.rev (qrev x nil2) = x) |
prop_29.thy |
✗ |
68.596944 |
| 136 |
(!!x. prop_30.rev (prop_30.append (prop_30.rev x) nil2) = x)
==> (!!x. prop_30.rev (prop_30.append (prop_30.rev x) nil2) = x) |
prop_30.thy |
✗ |
68.386551 |
| 137 |
(!!x. qrev (qrev x nil2) nil2 = x) ==> (!!x. qrev (qrev x nil2) nil2 = x) |
prop_31.thy |
✗ |
68.267778 |
| 138 |
(!!x. prop_32.rotate (prop_32.length x) x = x)
==> (!!x. prop_32.rotate (prop_32.length x) x = x) |
prop_32.thy |
✗ |
69.17261 |
| 139 |
(!!x. fac x = qfac x one) ==> (!!x. fac x = qfac x one) |
prop_33.thy |
✗ |
68.141077 |
| 140 |
(!!x y. mult x y = mult2 x y Z) ==> (!!x y. mult x y = mult2 x y Z) |
prop_34.thy |
✗ |
68.029303 |
| 141 |
(!!x y. prop_35.exp x y = qexp x y one)
==> (!!x y. prop_35.exp x y = qexp x y one) |
prop_35.thy |
✗ |
68.1074 |
| 142 |
(!!x y z. elem x y ==> elem x (prop_36.append y z))
==> (!!x y z. elem x y ==> elem x (prop_36.append y z)) |
prop_36.thy |
✗ |
11.695822 |
| 143 |
(!!x y z. elem x z ==> elem x (prop_37.append y z))
==> (!!x y z. elem x z ==> elem x (prop_37.append y z)) |
prop_37.thy |
✓ |
9.23722 |
| 144 |
(!!x y z. [| elem x y; elem x z |] ==> elem x (prop_38.append y z))
==> (!!x y z. [| elem x y; elem x z |] ==> elem x (prop_38.append y z)) |
prop_38.thy |
✓ |
9.235734 |
| 145 |
(!!x y z. elem x (prop_39.drop y z) ==> elem x z)
==> (!!x y z. elem x (prop_39.drop y z) ==> elem x z) |
prop_39.thy |
✗ |
9.240559 |
| 146 |
(!!x y. subset2 x y ==> union2 x y = y)
==> (!!x y. subset2 x y ==> union2 x y = y) |
prop_40.thy |
✗ |
9.700314 |
| 147 |
(!!x y. subset2 x y ==> intersect2 x y = x)
==> (!!x y. subset2 x y ==> intersect2 x y = x) |
prop_41.thy |
✗ |
9.749594 |
| 148 |
(!!x y z. elem x y ==> elem x (union2 y z))
==> (!!x y z. elem x y ==> elem x (union2 y z)) |
prop_42.thy |
✗ |
11.824833 |
| 149 |
(!!x y z. elem x y ==> elem x (union2 z y))
==> (!!x y z. elem x y ==> elem x (union2 z y)) |
prop_43.thy |
✓ |
9.203883 |
| 150 |
(!!x y z. [| elem x y; elem x z |] ==> elem x (intersect2 y z))
==> (!!x y z. [| elem x y; elem x z |] ==> elem x (intersect2 y z)) |
prop_44.thy |
✗ |
9.231152 |
| 151 |
(!!x y. elem x (insert2 x y)) ==> (!!x y. elem x (insert2 x y)) |
prop_45.thy |
✗ |
11.026447 |
| 152 |
(!!x y z. x = y ==> elem x (insert2 y z))
==> (!!x y z. x = y ==> elem x (insert2 y z)) |
prop_46.thy |
✗ |
24.010158 |
| 153 |
(!!x y z. unequal x y ==> elem x (insert2 y z) = elem x z)
==> (!!x y z. unequal x y ==> elem x (insert2 y z) = elem x z) |
prop_47.thy |
✓ |
9.436047 |
| 154 |
(!!x. prop_48.length (isort x) = prop_48.length x)
==> (!!x. prop_48.length (isort x) = prop_48.length x) |
prop_48.thy |
✗ |
69.185693 |
| 155 |
(!!x y. elem x (isort y) ==> elem x y)
==> (!!x y. elem x (isort y) ==> elem x y) |
prop_49.thy |
✗ |
9.321643 |
| 156 |
(!!x y. count x (isort y) = count x y)
==> (!!x y. count x (isort y) = count x y) |
prop_50.thy |
✗ |
69.270736 |
| 157 |
(!!xs x. prop_51.butlast (prop_51.append xs (cons2 x nil2)) = xs)
==> (!!xs x. prop_51.butlast (prop_51.append xs (cons2 x nil2)) = xs) |
prop_51.thy |
✓ |
8.401105 |
| 158 |
(!!n xs. count n xs = count n (prop_52.rev xs))
==> (!!n xs. count n xs = count n (prop_52.rev xs)) |
prop_52.thy |
✗ |
69.243424 |
| 159 |
(!!n xs. count n xs = count n (prop_53.sort xs))
==> (!!n xs. count n xs = count n (prop_53.sort xs)) |
prop_53.thy |
✗ |
69.277786 |
| 160 |
(!!n m. prop_54.minus (prop_54.plus m n) n = m)
==> (!!n m. prop_54.minus (prop_54.plus m n) n = m) |
prop_54.thy |
✗ |
67.888591 |
| 161 |
(!!n xs ys.
prop_55.drop n (prop_55.append xs ys) =
prop_55.append (prop_55.drop n xs)
(prop_55.drop (prop_55.minus n (len xs)) ys))
==> (!!n xs ys.
prop_55.drop n (prop_55.append xs ys) =
prop_55.append (prop_55.drop n xs)
(prop_55.drop (prop_55.minus n (len xs)) ys)) |
prop_55.thy |
✓ |
9.49764 |
| 162 |
(!!n m xs.
prop_56.drop n (prop_56.drop m xs) = prop_56.drop (prop_56.plus n m) xs)
==> (!!n m xs.
prop_56.drop n (prop_56.drop m xs) =
prop_56.drop (prop_56.plus n m) xs) |
prop_56.thy |
✗ |
69.014319 |
| 163 |
(!!n m xs.
prop_57.drop n (prop_57.take m xs) =
prop_57.take (prop_57.minus m n) (prop_57.drop n xs))
==> (!!n m xs.
prop_57.drop n (prop_57.take m xs) =
prop_57.take (prop_57.minus m n) (prop_57.drop n xs)) |
prop_57.thy |
✗ |
69.187645 |
| 164 |
(!!n xs ys.
prop_58.drop n (prop_58.zip xs ys) =
prop_58.zip (prop_58.drop n xs) (prop_58.drop n ys))
==> (!!n xs ys.
prop_58.drop n (prop_58.zip xs ys) =
prop_58.zip (prop_58.drop n xs) (prop_58.drop n ys)) |
prop_58.thy |
✗ |
69.970374 |
| 165 |
(!!xs ys.
ys = nil2 ==> prop_59.last (prop_59.append xs ys) = prop_59.last xs)
==> (!!xs ys.
ys = nil2 ==> prop_59.last (prop_59.append xs ys) = prop_59.last xs) |
prop_59.thy |
✓ |
9.069762 |
| 166 |
(!!xs ys.
¬ null ys ==> prop_60.last (prop_60.append xs ys) = prop_60.last ys)
==> (!!xs ys.
¬ null ys ==> prop_60.last (prop_60.append xs ys) = prop_60.last ys) |
prop_60.thy |
✗ |
69.056249 |
| 167 |
(!!xs ys. prop_61.last (prop_61.append xs ys) = lastOfTwo xs ys)
==> (!!xs ys. prop_61.last (prop_61.append xs ys) = lastOfTwo xs ys) |
prop_61.thy |
✗ |
69.266978 |
| 168 |
(!!xs x. ¬ null xs ==> prop_62.last (cons2 x xs) = prop_62.last xs)
==> (!!xs x. ¬ null xs ==> prop_62.last (cons2 x xs) = prop_62.last xs) |
prop_62.thy |
✗ |
8.998722 |
| 169 |
(!!n xs.
lt n (len xs) ==> prop_63.last (prop_63.drop n xs) = prop_63.last xs)
==> (!!n xs.
lt n (len xs)
==> prop_63.last (prop_63.drop n xs) = prop_63.last xs) |
prop_63.thy |
✗ |
69.194899 |
| 170 |
(!!x xs. prop_64.last (prop_64.append xs (cons2 x nil2)) = x)
==> (!!x xs. prop_64.last (prop_64.append xs (cons2 x nil2)) = x) |
prop_64.thy |
✗ |
68.975457 |
| 171 |
(!!i m. lt i (S (prop_65.plus m i)))
==> (!!i m. lt i (S (prop_65.plus m i))) |
prop_65.thy |
✗ |
68.011283 |
| 172 |
(!!q xs. le (len (prop_66.filter q xs)) (len xs))
==> (!!q xs. le (len (prop_66.filter q xs)) (len xs)) |
prop_66.thy |
✗ |
69.160426 |
| 173 |
(!!xs. len (prop_67.butlast xs) = prop_67.minus (len xs) (S Z))
==> (!!xs. len (prop_67.butlast xs) = prop_67.minus (len xs) (S Z)) |
prop_67.thy |
✓ |
9.241709 |
| 174 |
(!!n xs. le (len (delete n xs)) (len xs))
==> (!!n xs. le (len (delete n xs)) (len xs)) |
prop_68.thy |
✗ |
69.30053 |
| 175 |
(!!n m. le n (prop_69.plus m n)) ==> (!!n m. le n (prop_69.plus m n)) |
prop_69.thy |
✗ |
67.991654 |
| 176 |
(!!m n. le m n ==> le m (S n)) ==> (!!m n. le m n ==> le m (S n)) |
prop_70.thy |
✗ |
8.038062 |
| 177 |
(!!x y xs. ¬ equal2 x y ==> elem x (ins y xs) = elem x xs)
==> (!!x y xs. ¬ equal2 x y ==> elem x (ins y xs) = elem x xs) |
prop_71.thy |
✓ |
9.525973 |
| 178 |
(!!i xs.
prop_72.rev (prop_72.drop i xs) =
prop_72.take (prop_72.minus (len xs) i) (prop_72.rev xs))
==> (!!i xs.
prop_72.rev (prop_72.drop i xs) =
prop_72.take (prop_72.minus (len xs) i) (prop_72.rev xs)) |
prop_72.thy |
✗ |
69.506906 |
| 179 |
(!!p xs.
prop_73.rev (prop_73.filter p xs) = prop_73.filter p (prop_73.rev xs))
==> (!!p xs.
prop_73.rev (prop_73.filter p xs) =
prop_73.filter p (prop_73.rev xs)) |
prop_73.thy |
✗ |
68.632123 |
| 180 |
(!!i xs.
prop_74.rev (prop_74.take i xs) =
prop_74.drop (prop_74.minus (len xs) i) (prop_74.rev xs))
==> (!!i xs.
prop_74.rev (prop_74.take i xs) =
prop_74.drop (prop_74.minus (len xs) i) (prop_74.rev xs)) |
prop_74.thy |
✗ |
69.539922 |
| 181 |
(!!n m xs.
prop_75.plus (count n xs) (count n (cons2 m nil2)) =
count n (cons2 m xs))
==> (!!n m xs.
prop_75.plus (count n xs) (count n (cons2 m nil2)) =
count n (cons2 m xs)) |
prop_75.thy |
✓ |
9.380522 |
| 182 |
(!!n m xs.
¬ equal2 n m
==> count n (prop_76.append xs (cons2 m nil2)) = count n xs)
==> (!!n m xs.
¬ equal2 n m
==> count n (prop_76.append xs (cons2 m nil2)) = count n xs) |
prop_76.thy |
✓ |
9.233988 |
| 183 |
(!!x xs. prop_77.sorted xs ==> prop_77.sorted (prop_77.insort x xs))
==> (!!x xs. prop_77.sorted xs ==> prop_77.sorted (prop_77.insort x xs)) |
prop_77.thy |
✗ |
69.169566 |
| 184 |
(!!xs. prop_78.sorted (prop_78.sort xs))
==> (!!xs. prop_78.sorted (prop_78.sort xs)) |
prop_78.thy |
✗ |
69.311313 |
| 185 |
(!!m n k.
prop_79.minus (prop_79.minus (S m) n) (S k) =
prop_79.minus (prop_79.minus m n) k)
==> (!!m n k.
prop_79.minus (prop_79.minus (S m) n) (S k) =
prop_79.minus (prop_79.minus m n) k) |
prop_79.thy |
✓ |
15.166993 |
| 186 |
(!!n xs ys.
prop_80.take n (prop_80.append xs ys) =
prop_80.append (prop_80.take n xs)
(prop_80.take (prop_80.minus n (len xs)) ys))
==> (!!n xs ys.
prop_80.take n (prop_80.append xs ys) =
prop_80.append (prop_80.take n xs)
(prop_80.take (prop_80.minus n (len xs)) ys)) |
prop_80.thy |
✓ |
9.394922 |
| 187 |
(!!n m xs.
prop_81.take n (prop_81.drop m xs) =
prop_81.drop m (prop_81.take (prop_81.plus n m) xs))
==> (!!n m xs.
prop_81.take n (prop_81.drop m xs) =
prop_81.drop m (prop_81.take (prop_81.plus n m) xs)) |
prop_81.thy |
✗ |
69.20161 |
| 188 |
(!!n xs ys.
prop_82.take n (prop_82.zip xs ys) =
prop_82.zip (prop_82.take n xs) (prop_82.take n ys))
==> (!!n xs ys.
prop_82.take n (prop_82.zip xs ys) =
prop_82.zip (prop_82.take n xs) (prop_82.take n ys)) |
prop_82.thy |
✗ |
70.086745 |
| 189 |
(!!xs ys zs.
prop_83.zip (prop_83.append xs ys) zs =
prop_83.append (prop_83.zip xs (prop_83.take (len xs) zs))
(prop_83.zip ys (prop_83.drop (len xs) zs)))
==> (!!xs ys zs.
prop_83.zip (prop_83.append xs ys) zs =
prop_83.append (prop_83.zip xs (prop_83.take (len xs) zs))
(prop_83.zip ys (prop_83.drop (len xs) zs))) |
prop_83.thy |
✗ |
70.390512 |
| 190 |
(!!xs ys zs.
prop_84.zip xs (prop_84.append ys zs) =
prop_84.append (prop_84.zip (prop_84.take (len ys) xs) ys)
(prop_84.zip (prop_84.drop (len ys) xs) zs))
==> (!!xs ys zs.
prop_84.zip xs (prop_84.append ys zs) =
prop_84.append (prop_84.zip (prop_84.take (len ys) xs) ys)
(prop_84.zip (prop_84.drop (len ys) xs) zs)) |
prop_84.thy |
✗ |
70.585719 |
| 191 |
(!!xs ys.
len xs = len ys
==> prop_85.zip (prop_85.rev xs) (prop_85.rev ys) =
prop_85.rev (prop_85.zip xs ys))
==> (!!xs ys.
len xs = len ys
==> prop_85.zip (prop_85.rev xs) (prop_85.rev ys) =
prop_85.rev (prop_85.zip xs ys)) |
prop_85.thy |
✗ |
70.390209 |
| 192 |
(!!x y xs. lt x y ==> elem x (ins y xs) = elem x xs)
==> (!!x y xs. lt x y ==> elem x (ins y xs) = elem x xs) |
prop_86.thy |
✗ |
69.407964 |
| 193 |
(!!p s. recognise (Star p) s = recognise (Star (deeps p)) s)
==> (!!p s. recognise (Star p) s = recognise (Star (deeps p)) s) |
regexp_Deeps.thy |
✗ |
72.51526 |
| 194 |
(!!p q r s.
recognise (Plus p (Plus q r)) s = recognise (Plus (Plus p q) r) s)
==> (!!p q r s.
recognise (Plus p (Plus q r)) s = recognise (Plus (Plus p q) r) s) |
regexp_PlusAssociative.thy |
✗ |
72.558854 |
| 195 |
(!!p q s. recognise (Plus p q) s = recognise (Plus q p) s)
==> (!!p q s. recognise (Plus p q) s = recognise (Plus q p) s) |
regexp_PlusCommutative.thy |
✗ |
72.634871 |
| 196 |
(!!p s. recognise (Plus p p) s = recognise p s)
==> (!!p s. recognise (Plus p p) s = recognise p s) |
regexp_PlusIdempotent.thy |
✗ |
72.880255 |
| 197 |
(!!a s. recognise (Atom a) s = eqList s (cons2 a nil2))
==> (!!a s. recognise (Atom a) s = eqList s (cons2 a nil2)) |
regexp_RecAtom.thy |
✗ |
72.807583 |
| 198 |
(!!s. recognise R.Eps s = null s) ==> (!!s. recognise R.Eps s = null s) |
regexp_RecEps.thy |
✗ |
13.083918 |
| 199 |
(!!s. ¬ recognise Nil2 s) ==> (!!s. ¬ recognise Nil2 s) |
regexp_RecNil.thy |
✓ |
12.922417 |
| 200 |
(!!p q s. recognise (Plus p q) s = (recognise p s ∨ recognise q s))
==> (!!p q s. recognise (Plus p q) s = (recognise p s ∨ recognise q s)) |
regexp_RecPlus.thy |
✗ |
72.959011 |
| 201 |
(!!p q s.
recognise (Seq p q) s = or2 (propRecSeq p q (regexp_RecSeq.split s)))
==> (!!p q s.
recognise (Seq p q) s =
or2 (propRecSeq p q (regexp_RecSeq.split s))) |
regexp_RecSeq.thy |
✗ |
74.418307 |
| 202 |
(!!p s. recognise (Star p) s = (null s ∨ recognise (Seq p (Star p)) s))
==> (!!p s. recognise (Star p) s = (null s ∨ recognise (Seq p (Star p)) s)) |
regexp_RecStar.thy |
✗ |
73.202396 |
| 203 |
(!!r s. recognise (regexp_Reverse.rev r) s = recognise r (reverse s))
==> (!!r s. recognise (regexp_Reverse.rev r) s = recognise r (reverse s)) |
regexp_Reverse.thy |
✗ |
73.208955 |
| 204 |
(!!p q r s. recognise (Seq p (Seq q r)) s = recognise (Seq (Seq p q) r) s)
==> (!!p q r s.
recognise (Seq p (Seq q r)) s = recognise (Seq (Seq p q) r) s) |
regexp_SeqAssociative.thy |
✗ |
72.910936 |
| 205 |
(!!p q r s.
recognise (Seq p (Plus q r)) s = recognise (Plus (Seq p q) (Seq p r)) s)
==> (!!p q r s.
recognise (Seq p (Plus q r)) s =
recognise (Plus (Seq p q) (Seq p r)) s) |
regexp_SeqDistrPlus.thy |
✗ |
73.412353 |
| 206 |
(!!p s. recognise (Star p) s = recognise (Plus R.Eps (Seq p (Star p))) s)
==> (!!p s.
recognise (Star p) s = recognise (Plus R.Eps (Seq p (Star p))) s) |
regexp_Star.thy |
✗ |
73.743609 |
| 207 |
(!!xs ys. isRelaxedPrefix xs ys = spec xs ys)
==> (!!xs ys. isRelaxedPrefix xs ys = spec xs ys) |
relaxedprefix_correct.thy |
✗ |
71.102908 |
| 208 |
(!!xs ys. isRelaxedPrefix xs (relaxedprefix_is_prefix_1.append xs ys))
==> (!!xs ys. isRelaxedPrefix xs (relaxedprefix_is_prefix_1.append xs ys)) |
relaxedprefix_is_prefix_1.thy |
✗ |
70.397262 |
| 209 |
(!!x xs ys zs.
isRelaxedPrefix
(relaxedprefix_is_prefix_2.append
(relaxedprefix_is_prefix_2.append xs (cons2 x nil2)) ys)
(relaxedprefix_is_prefix_2.append
(relaxedprefix_is_prefix_2.append xs ys) zs))
==> (!!x xs ys zs.
isRelaxedPrefix
(relaxedprefix_is_prefix_2.append
(relaxedprefix_is_prefix_2.append xs (cons2 x nil2)) ys)
(relaxedprefix_is_prefix_2.append
(relaxedprefix_is_prefix_2.append xs ys) zs)) |
relaxedprefix_is_prefix_2.thy |
✗ |
70.277739 |
| 210 |
(!!x xs ys.
isRelaxedPrefix (relaxedprefix_is_prefix_3.append xs (cons2 x nil2))
(relaxedprefix_is_prefix_3.append xs ys))
==> (!!x xs ys.
isRelaxedPrefix (relaxedprefix_is_prefix_3.append xs (cons2 x nil2))
(relaxedprefix_is_prefix_3.append xs ys)) |
relaxedprefix_is_prefix_3.thy |
✗ |
70.23452 |
| 211 |
(!!x xs ys.
isRelaxedPrefix (cons2 x xs) (relaxedprefix_is_prefix_4.append xs ys))
==> (!!x xs ys.
isRelaxedPrefix (cons2 x xs)
(relaxedprefix_is_prefix_4.append xs ys)) |
relaxedprefix_is_prefix_4.thy |
✗ |
70.19854 |
| 212 |
(!!n xs.
mod2_dom (n, rotate_mod.length xs)
==> rotate_mod.rotate n xs =
rotate_mod.append
(rotate_mod.drop (mod2 n (rotate_mod.length xs)) xs)
(rotate_mod.take (mod2 n (rotate_mod.length xs)) xs))
==> (!!n xs.
mod2_dom (n, rotate_mod.length xs)
==> rotate_mod.rotate n xs =
rotate_mod.append
(rotate_mod.drop (mod2 n (rotate_mod.length xs)) xs)
(rotate_mod.take (mod2 n (rotate_mod.length xs)) xs)) |
rotate_mod.thy |
✗ |
70.470309 |
| 213 |
(!!n xs.
rotate_self.rotate n (rotate_self.append xs xs) =
rotate_self.append (rotate_self.rotate n xs) (rotate_self.rotate n xs))
==> (!!n xs.
rotate_self.rotate n (rotate_self.append xs xs) =
rotate_self.append (rotate_self.rotate n xs)
(rotate_self.rotate n xs)) |
rotate_self.thy |
✗ |
69.776196 |
| 214 |
(!!xs. rotate_snoc.rotate (rotate_snoc.length xs) xs = xs)
==> (!!xs. rotate_snoc.rotate (rotate_snoc.length xs) xs = xs) |
rotate_snoc.thy |
✗ |
69.507846 |
| 215 |
(!!n xs.
rotate_snoc_self.rotate n (rotate_snoc_self.append xs xs) =
rotate_snoc_self.append (rotate_snoc_self.rotate n xs)
(rotate_snoc_self.rotate n xs))
==> (!!n xs.
rotate_snoc_self.rotate n (rotate_snoc_self.append xs xs) =
rotate_snoc_self.append (rotate_snoc_self.rotate n xs)
(rotate_snoc_self.rotate n xs)) |
rotate_snoc_self.thy |
✗ |
69.647239 |
| 216 |
(!!n xs.
rotate_structural_mod.rotate n xs =
rotate_structural_mod.append
(rotate_structural_mod.drop
(modstructural n (rotate_structural_mod.length xs)) xs)
(rotate_structural_mod.take
(modstructural n (rotate_structural_mod.length xs)) xs))
==> (!!n xs.
rotate_structural_mod.rotate n xs =
rotate_structural_mod.append
(rotate_structural_mod.drop
(modstructural n (rotate_structural_mod.length xs)) xs)
(rotate_structural_mod.take
(modstructural n (rotate_structural_mod.length xs)) xs)) |
rotate_structural_mod.thy |
✗ |
70.451897 |
| 217 |
(!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) |
simp_expr_unambig1.thy |
✗ |
10.572635 |
| 218 |
(!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) |
simp_expr_unambig2.thy |
✗ |
10.602825 |
| 219 |
(!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) |
simp_expr_unambig3.thy |
✗ |
10.668774 |
| 220 |
(!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) |
simp_expr_unambig4.thy |
✗ |
10.632997 |
| 221 |
(!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) |
simp_expr_unambig5.thy |
✗ |
11.647516 |
| 222 |
(!!x y. zcount x (isort y) = zcount x y)
==> (!!x y. zcount x (isort y) = zcount x y) |
sort_ISortCount.thy |
✗ |
69.603022 |
| 223 |
(!!x. zisPermutation (isort x) x) ==> (!!x. zisPermutation (isort x) x) |
sort_ISortPermutes.thy |
✗ |
69.354619 |
| 224 |
(!!x. zordered (isort x)) ==> (!!x. zordered (isort x)) |
sort_ISortSorts.thy |
✗ |
68.924567 |
| 225 |
(!!x y. zcount x (nstoogesort2 y) = zcount x y)
==> (!!x y. zcount x (nstoogesort2 y) = zcount x y) |
sort_NStoogeSort2Count.thy |
✗ |
71.762378 |
| 226 |
(!!x. nstoogesort2 x = isort x) ==> (!!x. nstoogesort2 x = isort x) |
sort_NStoogeSort2IsSort.thy |
✗ |
11.855424 |
| 227 |
(!!x. zisPermutation (nstoogesort2 x) x)
==> (!!x. zisPermutation (nstoogesort2 x) x) |
sort_NStoogeSort2Permutes.thy |
✗ |
72.121381 |
| 228 |
(!!x. zordered (nstoogesort2 x)) ==> (!!x. zordered (nstoogesort2 x)) |
sort_NStoogeSort2Sorts.thy |
✗ |
71.725171 |
| 229 |
(!!x y. zcount x (nstoogesort y) = zcount x y)
==> (!!x y. zcount x (nstoogesort y) = zcount x y) |
sort_NStoogeSortCount.thy |
✗ |
71.791066 |
| 230 |
(!!x. nstoogesort x = isort x) ==> (!!x. nstoogesort x = isort x) |
sort_NStoogeSortIsSort.thy |
✗ |
11.89711 |
| 231 |
(!!x. zisPermutation (nstoogesort x) x)
==> (!!x. zisPermutation (nstoogesort x) x) |
sort_NStoogeSortPermutes.thy |
✗ |
72.05802 |
| 232 |
(!!x. zordered (nstoogesort x)) ==> (!!x. zordered (nstoogesort x)) |
sort_NStoogeSortSorts.thy |
✗ |
71.706379 |
| 233 |
(!!x y. zcount x (stoogesort2 y) = zcount x y)
==> (!!x y. zcount x (stoogesort2 y) = zcount x y) |
sort_StoogeSort2Count.thy |
✗ |
71.70904 |
| 234 |
(!!x. stoogesort2 x = isort x) ==> (!!x. stoogesort2 x = isort x) |
sort_StoogeSort2IsSort.thy |
✗ |
11.208312 |
| 235 |
(!!x. zisPermutation (stoogesort2 x) x)
==> (!!x. zisPermutation (stoogesort2 x) x) |
sort_StoogeSort2Permutes.thy |
✗ |
71.3558 |
| 236 |
(!!x. zordered (stoogesort2 x)) ==> (!!x. zordered (stoogesort2 x)) |
sort_StoogeSort2Sorts.thy |
✗ |
71.011346 |
| 237 |
(!!x y. zcount x (stoogesort y) = zcount x y)
==> (!!x y. zcount x (stoogesort y) = zcount x y) |
sort_StoogeSortCount.thy |
✗ |
71.689783 |
| 238 |
(!!x. stoogesort x = isort x) ==> (!!x. stoogesort x = isort x) |
sort_StoogeSortIsSort.thy |
✗ |
11.379635 |
| 239 |
(!!x. zisPermutation (stoogesort x) x)
==> (!!x. zisPermutation (stoogesort x) x) |
sort_StoogeSortPermutes.thy |
✗ |
71.507972 |
| 240 |
(!!x. zordered (stoogesort x)) ==> (!!x. zordered (stoogesort x)) |
sort_StoogeSortSorts.thy |
✗ |
71.034318 |
| 241 |
(!!x y. zcount x (tsort y) = zcount x y)
==> (!!x y. zcount x (tsort y) = zcount x y) |
sort_TSortCount.thy |
✗ |
70.923388 |
| 242 |
(!!x. tsort x = isort x) ==> (!!x. tsort x = isort x) |
sort_TSortIsSort.thy |
✗ |
70.427277 |
| 243 |
(!!x. zisPermutation (tsort x) x) ==> (!!x. zisPermutation (tsort x) x) |
sort_TSortPermutes.thy |
✗ |
70.75927 |
| 244 |
(!!x. zordered (tsort x)) ==> (!!x. zordered (tsort x)) |
sort_TSortSorts.thy |
✗ |
70.372144 |
| 245 |
(!!p. flatten2 p nil2 = flatten0 p) ==> (!!p. flatten2 p nil2 = flatten0 p) |
tree_Flatten2.thy |
✗ |
70.15765 |
| 246 |
(!!x y t.
¬ equal2 x y
==> count y (flatten (add x t) nil2) = count y (flatten t nil2))
==> (!!x y t.
¬ equal2 x y
==> count y (flatten (add x t) nil2) = count y (flatten t nil2)) |
tree_sort_AddDifferent.thy |
✗ |
58.247859 |
| 247 |
(!!x t. count x (flatten (add x t) nil2) = S (count x (flatten t nil2)))
==> (!!x t. count x (flatten (add x t) nil2) = S (count x (flatten t nil2))) |
tree_sort_AddSame.thy |
✗ |
71.110769 |
| 248 |
(!!x y. count x (tsort y) = count x y)
==> (!!x y. count x (tsort y) = count x y) |
tree_sort_SortPermutes.thy |
✗ |
71.298702 |
| 249 |
(!!x. ordered (tsort x)) ==> (!!x. ordered (tsort x)) |
tree_sort_SortSorts.thy |
✗ |
71.107968 |
| 250 |
(!!p a b.
[| zelem a (flatten0 p); zelem b (flatten0 p) |]
==> zelem a (flatten0 (swap a b p)) ∧ zelem b (flatten0 (swap a b p)))
==> (!!p a b.
[| zelem a (flatten0 p); zelem b (flatten0 p) |]
==> zelem a (flatten0 (swap a b p)) ∧
zelem b (flatten0 (swap a b p))) |
tree_SwapAB.thy |
✗ |
70.433401 |
| 251 |
(!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 x2 (add3 x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
add3 (add3 x1 x2 x3) x4 x5 = add3 x1 x2 (add3 x3 x4 x5)) |
weird_nat_add3_assoc1.thy |
✓ |
8.345732 |
| 252 |
(!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 (add3 x2 x3 x4) x5)
==> (!!x1 x2 x3 x4 x5.
add3 (add3 x1 x2 x3) x4 x5 = add3 x1 (add3 x2 x3 x4) x5) |
weird_nat_add3_assoc2.thy |
✓ |
32.84501 |
| 253 |
(!!x1 x2 x3 x4 x5. add3 x1 (add3 x2 x3 x4) x5 = add3 x1 x2 (add3 x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
add3 x1 (add3 x2 x3 x4) x5 = add3 x1 x2 (add3 x3 x4 x5)) |
weird_nat_add3_assoc3.thy |
✓ |
49.001601 |
| 254 |
(!!x y z. add3 x y z = add3 y x z) ==> (!!x y z. add3 x y z = add3 y x z) |
weird_nat_add3_comm12.thy |
✓ |
9.450155 |
| 255 |
(!!x y z. add3 x y z = add3 z y x) ==> (!!x y z. add3 x y z = add3 z y x) |
weird_nat_add3_comm13.thy |
✓ |
10.955537 |
| 256 |
(!!x y z. add3 x y z = add3 x z y) ==> (!!x y z. add3 x y z = add3 x z y) |
weird_nat_add3_comm23.thy |
✓ |
9.264705 |
| 257 |
(!!x y z. add3 x y z = add3 y x z) ==> (!!x y z. add3 x y z = add3 y x z) |
weird_nat_add3_rot.thy |
✓ |
9.317288 |
| 258 |
(!!x y z. add3 x y z = add3 z x y) ==> (!!x y z. add3 x y z = add3 z x y) |
weird_nat_add3_rrot.thy |
✓ |
10.0389 |
| 259 |
(!!x y z. add3 x y z = add3acc x y z)
==> (!!x y z. add3 x y z = add3acc x y z) |
weird_nat_add3_same.thy |
✗ |
68.393321 |
| 260 |
(!!x y z.
add3 x y z = weird_nat_add3_spec.plus x (weird_nat_add3_spec.plus y z))
==> (!!x y z.
add3 x y z =
weird_nat_add3_spec.plus x (weird_nat_add3_spec.plus y z)) |
weird_nat_add3_spec.thy |
✓ |
8.261464 |
| 261 |
(!!x1 x2 x3 x4 x5.
add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 x2 (add3acc x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 x2 (add3acc x3 x4 x5)) |
weird_nat_add3acc_assoc1.thy |
✓ |
25.403472 |
| 262 |
(!!x1 x2 x3 x4 x5.
add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 (add3acc x2 x3 x4) x5)
==> (!!x1 x2 x3 x4 x5.
add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 (add3acc x2 x3 x4) x5) |
weird_nat_add3acc_assoc2.thy |
✓ |
36.638099 |
| 263 |
(!!x1 x2 x3 x4 x5.
add3acc x1 (add3acc x2 x3 x4) x5 = add3acc x1 x2 (add3acc x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
add3acc x1 (add3acc x2 x3 x4) x5 = add3acc x1 x2 (add3acc x3 x4 x5)) |
weird_nat_add3acc_assoc3.thy |
✗ |
68.205264 |
| 264 |
(!!x y z. add3acc x y z = add3acc y x z)
==> (!!x y z. add3acc x y z = add3acc y x z) |
weird_nat_add3acc_comm12.thy |
✗ |
68.191903 |
| 265 |
(!!x y z. add3acc x y z = add3acc z y x)
==> (!!x y z. add3acc x y z = add3acc z y x) |
weird_nat_add3acc_comm13.thy |
✗ |
68.329493 |
| 266 |
(!!x y z. add3acc x y z = add3acc x z y)
==> (!!x y z. add3acc x y z = add3acc x z y) |
weird_nat_add3acc_comm23.thy |
✗ |
68.274878 |
| 267 |
(!!x y z. add3acc x y z = add3acc y x z)
==> (!!x y z. add3acc x y z = add3acc y x z) |
weird_nat_add3acc_rot.thy |
✗ |
68.253045 |
| 268 |
(!!x y z. add3acc x y z = add3acc z x y)
==> (!!x y z. add3acc x y z = add3acc z x y) |
weird_nat_add3acc_rrot.thy |
✗ |
68.283508 |
| 269 |
(!!x y z.
add3acc x y z =
weird_nat_add3acc_spec.plus x (weird_nat_add3acc_spec.plus y z))
==> (!!x y z.
add3acc x y z =
weird_nat_add3acc_spec.plus x (weird_nat_add3acc_spec.plus y z)) |
weird_nat_add3acc_spec.thy |
✓ |
10.813298 |
| 270 |
(!!x y z. mul2 x (mul2 y z) = mul2 (mul2 x y) z)
==> (!!x y z. mul2 x (mul2 y z) = mul2 (mul2 x y) z) |
weird_nat_mul2_assoc.thy |
✗ |
68.348566 |
| 271 |
(!!x y. mul2 x y = mul2 y x) ==> (!!x y. mul2 x y = mul2 y x) |
weird_nat_mul2_comm.thy |
✗ |
68.351782 |
| 272 |
(!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 x2 (mul3 x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 x2 (mul3 x3 x4 x5)) |
weird_nat_mul3_assoc1.thy |
✗ |
68.97589 |
| 273 |
(!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 (mul3 x2 x3 x4) x5)
==> (!!x1 x2 x3 x4 x5.
mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 (mul3 x2 x3 x4) x5) |
weird_nat_mul3_assoc2.thy |
✗ |
69.011361 |
| 274 |
(!!x1 x2 x3 x4 x5. mul3 x1 (mul3 x2 x3 x4) x5 = mul3 x1 x2 (mul3 x3 x4 x5))
==> (!!x1 x2 x3 x4 x5.
mul3 x1 (mul3 x2 x3 x4) x5 = mul3 x1 x2 (mul3 x3 x4 x5)) |
weird_nat_mul3_assoc3.thy |
✗ |
69.392498 |
| 275 |
(!!x y z. mul3 x y z = mul3 y x z) ==> (!!x y z. mul3 x y z = mul3 y x z) |
weird_nat_mul3_comm12.thy |
✗ |
69.011996 |
| 276 |
(!!x y z. mul3 x y z = mul3 z y x) ==> (!!x y z. mul3 x y z = mul3 z y x) |
weird_nat_mul3_comm13.thy |
✗ |
68.963751 |
| 277 |
(!!x y z. mul3 x y z = mul3 x z y) ==> (!!x y z. mul3 x y z = mul3 x z y) |
weird_nat_mul3_comm23.thy |
✗ |
69.07085 |
| 278 |
(!!x y z. mul3 x y z = mul3 y x z) ==> (!!x y z. mul3 x y z = mul3 y x z) |
weird_nat_mul3_rot.thy |
✗ |
68.964568 |
| 279 |
(!!x y z. mul3 x y z = mul3 z x y) ==> (!!x y z. mul3 x y z = mul3 z x y) |
weird_nat_mul3_rrot.thy |
✗ |
68.994129 |
| 280 |
(!!x y z. mul3 x y z = mul3acc x y z)
==> (!!x y z. mul3 x y z = mul3acc x y z) |
weird_nat_mul3_same.thy |
✗ |
69.717675 |
| 281 |
(!!x y z. mul3 x y z = mult (mult x y) z)
==> (!!x y z. mul3 x y z = mult (mult x y) z) |
weird_nat_mul3_spec.thy |
✗ |
69.291949 |
| 282 |
(!!x1 x2 x3acc x4 x5.
mul3acc (mul3acc x1 x2 x3acc) x4 x5 =
mul3acc x1 x2 (mul3acc x3acc x4 x5))
==> (!!x1 x2 x3acc x4 x5.
mul3acc (mul3acc x1 x2 x3acc) x4 x5 =
mul3acc x1 x2 (mul3acc x3acc x4 x5)) |
weird_nat_mul3acc_assoc1.thy |
✗ |
69.151581 |
| 283 |
(!!x1 x2 x3acc x4 x5.
mul3acc (mul3acc x1 x2 x3acc) x4 x5 =
mul3acc x1 (mul3acc x2 x3acc x4) x5)
==> (!!x1 x2 x3acc x4 x5.
mul3acc (mul3acc x1 x2 x3acc) x4 x5 =
mul3acc x1 (mul3acc x2 x3acc x4) x5) |
weird_nat_mul3acc_assoc2.thy |
✗ |
69.033559 |
| 284 |
(!!x1 x2 x3acc x4 x5.
mul3acc x1 (mul3acc x2 x3acc x4) x5 =
mul3acc x1 x2 (mul3acc x3acc x4 x5))
==> (!!x1 x2 x3acc x4 x5.
mul3acc x1 (mul3acc x2 x3acc x4) x5 =
mul3acc x1 x2 (mul3acc x3acc x4 x5)) |
weird_nat_mul3acc_assoc3.thy |
✗ |
69.123922 |
| 285 |
(!!x y z. mul3acc x y z = mul3acc y x z)
==> (!!x y z. mul3acc x y z = mul3acc y x z) |
weird_nat_mul3acc_comm12.thy |
✗ |
69.021613 |
| 286 |
(!!x y z. mul3acc x y z = mul3acc z y x)
==> (!!x y z. mul3acc x y z = mul3acc z y x) |
weird_nat_mul3acc_comm13.thy |
✗ |
69.065365 |
| 287 |
(!!x y z. mul3acc x y z = mul3acc x z y)
==> (!!x y z. mul3acc x y z = mul3acc x z y) |
weird_nat_mul3acc_comm23.thy |
✗ |
69.086191 |
| 288 |
(!!x y z. mul3acc x y z = mul3acc y x z)
==> (!!x y z. mul3acc x y z = mul3acc y x z) |
weird_nat_mul3acc_rot.thy |
✗ |
69.103617 |
| 289 |
(!!x y z. mul3acc x y z = mul3acc z x y)
==> (!!x y z. mul3acc x y z = mul3acc z x y) |
weird_nat_mul3acc_rrot.thy |
✗ |
69.095496 |
| 290 |
(!!x y z. mul3acc x y z = mult (mult x y) z)
==> (!!x y z. mul3acc x y z = mult (mult x y) z) |
weird_nat_mul3acc_spec.thy |
✗ |
69.162028 |
| 291 |
(!!a b c d e. opp (opp a b Z Z) c d e = opp a (opp b c Z Z) d e)
==> (!!a b c d e. opp (opp a b Z Z) c d e = opp a (opp b c Z Z) d e) |
weird_nat_op_assoc.thy |
✗ |
68.300298 |
| 292 |
(!!x a b c d. opp (opp x a a a) b c d = opp a (opp b x b b) c d)
==> (!!x a b c d. opp (opp x a a a) b c d = opp a (opp b x b b) c d) |
weird_nat_op_assoc2.thy |
✗ |
68.250017 |
| 293 |
(!!a b c d. opp a b c d = opp b a d c)
==> (!!a b c d. opp a b c d = opp b a d c) |
weird_nat_op_comm_comm.thy |
✗ |
68.224757 |
| 294 |
(!!a b c d.
opp a b c d =
weird_nat_op_spec.plus (weird_nat_op_spec.plus (mult a b) c) d)
==> (!!a b c d.
opp a b c d =
weird_nat_op_spec.plus (weird_nat_op_spec.plus (mult a b) c) d) |
weird_nat_op_spec.thy |
✗ |
68.630564 |