12 begin |
12 begin |
13 |
13 |
14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] |
14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] |
15 |
15 |
16 primrec rot where |
16 primrec rot where |
17 "rot Nibble0 = Nibble1" | |
17 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | |
18 "rot Nibble1 = Nibble2" | |
18 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" | |
19 "rot Nibble2 = Nibble3" | |
19 "rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" | |
20 "rot Nibble3 = Nibble4" | |
20 "rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" | |
21 "rot Nibble4 = Nibble5" | |
21 "rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" | |
22 "rot Nibble5 = Nibble6" | |
|
23 "rot Nibble6 = Nibble7" | |
|
24 "rot Nibble7 = Nibble8" | |
|
25 "rot Nibble8 = Nibble9" | |
|
26 "rot Nibble9 = NibbleA" | |
|
27 "rot NibbleA = NibbleB" | |
|
28 "rot NibbleB = NibbleC" | |
|
29 "rot NibbleC = NibbleD" | |
|
30 "rot NibbleD = NibbleE" | |
|
31 "rot NibbleE = NibbleF" | |
|
32 "rot NibbleF = Nibble0" |
22 "rot NibbleF = Nibble0" |
33 |
23 |
34 lemma "rot n \<noteq> n" |
24 lemma "rot n \<noteq> n" |
35 nitpick [card = 1\<midarrow>16, expect = none] |
25 nitpick [card = 1\<midarrow>16, expect = none] |
36 sorry |
26 sorry |