Comment: A.B.: 2 1 1 1 1 2 1-1 1 3-1 2 3 1 0 2 1 1 0 0 0 1-1 2 2 1 1 Comment: The halting transition has been modified to print a 1 Comment: This TM produces 5600 nonzeros in 29403894 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | B1R | A2R | A1L | 1 | right | B | 2 | right | A | 1 | left | A |
| B | C2L | C0R | B1R | 2 | left | C | 0 | right | C | 1 | right | B |
| C | Z1R | A2L | B1R | 1 | right | Z | 2 | left | A | 1 | right | B |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-macro machine.
Simulation is done as 2-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)A>
1 6 2 01 (11)B>
2 11 -1 01 <A(11) 20
3 14 2 02 (22)A> 20
4 17 -1 02 <A(11) 10
5 24 2 11 (10)C> 10
6 39 -1 11 <A(11) 11
7 42 2 12 (22)A> 11
8 44 4 12 22 (22)A>
9 49 1 12 22 <A(11) 22
10 51 -1 12 <A(11) 11 22
11 56 2 22 (22)A> 11 22
12 58 4 222 (22)A> 22
13 61 1 222 <A(11) 12
14 65 -3 <A(11) 112 12
15 70 0 01 (11)B> 112 12
16 78 4 01 112 (11)B> 12
17 80 6 01 113 (01)B>
18 97 3 01 113 <A(11) 11
19 100 6 01 112 12 (22)A> 11
20 102 8 01 112 12 22 (22)A>
21 107 5 01 112 12 22 <A(11) 22
22 109 3 01 112 12 <A(11) 11 22
23 114 6 01 112 22 (22)A> 11 22
24 116 8 01 112 222 (22)A> 22
25 119 5 01 112 222 <A(11) 12
26 123 1 01 112 <A(11) 112 12
27 126 4 01 11 12 (22)A> 112 12
28 130 8 01 11 12 222 (22)A> 12
29 135 5 01 11 12 222 <A(11) 11
30 139 1 01 11 12 <A(11) 113
31 144 4 01 11 22 (22)A> 113
32 150 10 01 11 224 (22)A>
33 155 7 01 11 224 <A(11) 22
34 163 -1 01 11 <A(11) 114 22
35 166 2 01 12 (22)A> 114 22
36 174 10 01 12 224 (22)A> 22
37 177 7 01 12 224 <A(11) 12
38 185 -1 01 12 <A(11) 114 12
39 190 2 01 22 (22)A> 114 12
40 198 10 01 225 (22)A> 12
41 203 7 01 225 <A(11) 11
42 213 -3 01 <A(11) 116
43 216 0 02 (22)A> 116
44 228 12 02 226 (22)A>
45 233 9 02 226 <A(11) 22
46 245 -3 02 <A(11) 116 22
47 252 0 11 (10)C> 116 22
48 276 12 117 (10)C> 22
49 278 14 117 10 (11)B>
50 283 11 117 10 <A(11) 20
51 288 14 118 (11)B> 20
52 301 11 118 <A(11) 11
53 304 14 117 12 (22)A> 11
54 306 16 117 12 22 (22)A>
55 311 13 117 12 22 <A(11) 22
56 313 11 117 12 <A(11) 11 22
57 318 14 117 22 (22)A> 11 22
58 320 16 117 222 (22)A> 22
59 323 13 117 222 <A(11) 12
60 327 9 117 <A(11) 112 12
61 330 12 116 12 (22)A> 112 12
62 334 16 116 12 222 (22)A> 12
63 339 13 116 12 222 <A(11) 11
64 343 9 116 12 <A(11) 113
65 348 12 116 22 (22)A> 113
66 354 18 116 224 (22)A>
67 359 15 116 224 <A(11) 22
68 367 7 116 <A(11) 114 22
69 370 10 115 12 (22)A> 114 22
70 378 18 115 12 224 (22)A> 22
71 381 15 115 12 224 <A(11) 12
72 389 7 115 12 <A(11) 114 12
73 394 10 115 22 (22)A> 114 12
74 402 18 115 225 (22)A> 12
75 407 15 115 225 <A(11) 11
76 417 5 115 <A(11) 116
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 114+V(1) <A(11) 111+V(2)
1 3 3 113+V(1) 12 (22)A> 111+V(2)
2 5+2*V(2) 5+2*V(2) 113+V(1) 12 221+V(2) (22)A>
3 10+2*V(2) 2+2*V(2) 113+V(1) 12 221+V(2) <A(11) 22
4 12+4*V(2) 0 113+V(1) 12 <A(11) 111+V(2) 22
5 17+4*V(2) 3 113+V(1) 22 (22)A> 111+V(2) 22
6 19+6*V(2) 5+2*V(2) 113+V(1) 222+V(2) (22)A> 22
7 22+6*V(2) 2+2*V(2) 113+V(1) 222+V(2) <A(11) 12
8 26+8*V(2) -2 113+V(1) <A(11) 112+V(2) 12
9 29+8*V(2) 1 112+V(1) 12 (22)A> 112+V(2) 12
10 33+10*V(2) 5+2*V(2) 112+V(1) 12 222+V(2) (22)A> 12
11 38+10*V(2) 2+2*V(2) 112+V(1) 12 222+V(2) <A(11) 11
12 42+12*V(2) -2 112+V(1) 12 <A(11) 113+V(2)
13 47+12*V(2) 1 112+V(1) 22 (22)A> 113+V(2)
14 53+14*V(2) 7+2*V(2) 112+V(1) 224+V(2) (22)A>
15 58+14*V(2) 4+2*V(2) 112+V(1) 224+V(2) <A(11) 22
16 66+16*V(2) -4 112+V(1) <A(11) 114+V(2) 22
17 69+16*V(2) -1 111+V(1) 12 (22)A> 114+V(2) 22
18 77+18*V(2) 7+2*V(2) 111+V(1) 12 224+V(2) (22)A> 22
19 80+18*V(2) 4+2*V(2) 111+V(1) 12 224+V(2) <A(11) 12
20 88+20*V(2) -4 111+V(1) 12 <A(11) 114+V(2) 12
21 93+20*V(2) -1 111+V(1) 22 (22)A> 114+V(2) 12
22 101+22*V(2) 7+2*V(2) 111+V(1) 225+V(2) (22)A> 12
23 106+22*V(2) 4+2*V(2) 111+V(1) 225+V(2) <A(11) 11
24 116+24*V(2) -6 111+V(1) <A(11) 116+V(2)
<< Success! ==> defined new CTR 1 (PA)
76 417 5 115 <A(11) 116
== Executing PA-CTR 1, V(1)=1, V(2)=5, repcount=1, factor=5/3
100 653 -1 112 <A(11) 1111
101 656 2 11 12 (22)A> 1111
102 678 24 11 12 2211 (22)A>
103 683 21 11 12 2211 <A(11) 22
104 705 -1 11 12 <A(11) 1111 22
105 710 2 11 22 (22)A> 1111 22
106 732 24 11 2212 (22)A> 22
107 735 21 11 2212 <A(11) 12
108 759 -3 11 <A(11) 1112 12
109 762 0 12 (22)A> 1112 12
110 786 24 12 2212 (22)A> 12
111 791 21 12 2212 <A(11) 11
112 815 -3 12 <A(11) 1113
113 820 0 22 (22)A> 1113
114 846 26 2214 (22)A>
115 851 23 2214 <A(11) 22
116 879 -5 <A(11) 1114 22
117 884 -2 01 (11)B> 1114 22
118 940 26 01 1114 (11)B> 22
119 942 28 01 1115 (11)B>
120 947 25 01 1115 <A(11) 20
121 950 28 01 1114 12 (22)A> 20
122 953 25 01 1114 12 <A(11) 10
123 958 28 01 1114 22 (22)A> 10
124 960 30 01 1114 222 (21)B>
125 963 27 01 1114 222 <A(12) 20
126 965 25 01 1114 22 <A(11) 12 20
127 967 23 01 1114 <A(11) 11 12 20
128 970 26 01 1113 12 (22)A> 11 12 20
129 972 28 01 1113 12 22 (22)A> 12 20
130 977 25 01 1113 12 22 <A(11) 11 20
131 979 23 01 1113 12 <A(11) 112 20
132 984 26 01 1113 22 (22)A> 112 20
133 988 30 01 1113 223 (22)A> 20
134 991 27 01 1113 223 <A(11) 10
135 997 21 01 1113 <A(11) 113 10
136 1000 24 01 1112 12 (22)A> 113 10
137 1006 30 01 1112 12 223 (22)A> 10
138 1008 32 01 1112 12 224 (21)B>
139 1011 29 01 1112 12 224 <A(12) 20
140 1013 27 01 1112 12 223 <A(11) 12 20
141 1019 21 01 1112 12 <A(11) 113 12 20
142 1024 24 01 1112 22 (22)A> 113 12 20
143 1030 30 01 1112 224 (22)A> 12 20
144 1035 27 01 1112 224 <A(11) 11 20
145 1043 19 01 1112 <A(11) 115 20
146 1046 22 01 1111 12 (22)A> 115 20
147 1056 32 01 1111 12 225 (22)A> 20
148 1059 29 01 1111 12 225 <A(11) 10
149 1069 19 01 1111 12 <A(11) 115 10
150 1074 22 01 1111 22 (22)A> 115 10
151 1084 32 01 1111 226 (22)A> 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 114+V(2) 221+V(1) (22)A> 10
1 2 2 [*]* 114+V(2) 222+V(1) (21)B>
2 5 -1 [*]* 114+V(2) 222+V(1) <A(12) 20
3 7 -3 [*]* 114+V(2) 221+V(1) <A(11) 12 20
4 9+2*V(1) -5+-2*V(1) [*]* 114+V(2) <A(11) 111+V(1) 12 20
5 12+2*V(1) -2+-2*V(1) [*]* 113+V(2) 12 (22)A> 111+V(1) 12 20
6 14+4*V(1) 0 [*]* 113+V(2) 12 221+V(1) (22)A> 12 20
7 19+4*V(1) -3 [*]* 113+V(2) 12 221+V(1) <A(11) 11 20
8 21+6*V(1) -5+-2*V(1) [*]* 113+V(2) 12 <A(11) 112+V(1) 20
9 26+6*V(1) -2+-2*V(1) [*]* 113+V(2) 22 (22)A> 112+V(1) 20
10 30+8*V(1) 2 [*]* 113+V(2) 223+V(1) (22)A> 20
11 33+8*V(1) -1 [*]* 113+V(2) 223+V(1) <A(11) 10
12 39+10*V(1) -7+-2*V(1) [*]* 113+V(2) <A(11) 113+V(1) 10
13 42+10*V(1) -4+-2*V(1) [*]* 112+V(2) 12 (22)A> 113+V(1) 10
14 48+12*V(1) 2 [*]* 112+V(2) 12 223+V(1) (22)A> 10
15 50+12*V(1) 4 [*]* 112+V(2) 12 224+V(1) (21)B>
16 53+12*V(1) 1 [*]* 112+V(2) 12 224+V(1) <A(12) 20
17 55+12*V(1) -1 [*]* 112+V(2) 12 223+V(1) <A(11) 12 20
18 61+14*V(1) -7+-2*V(1) [*]* 112+V(2) 12 <A(11) 113+V(1) 12 20
19 66+14*V(1) -4+-2*V(1) [*]* 112+V(2) 22 (22)A> 113+V(1) 12 20
20 72+16*V(1) 2 [*]* 112+V(2) 224+V(1) (22)A> 12 20
21 77+16*V(1) -1 [*]* 112+V(2) 224+V(1) <A(11) 11 20
22 85+18*V(1) -9+-2*V(1) [*]* 112+V(2) <A(11) 115+V(1) 20
23 88+18*V(1) -6+-2*V(1) [*]* 111+V(2) 12 (22)A> 115+V(1) 20
24 98+20*V(1) 4 [*]* 111+V(2) 12 225+V(1) (22)A> 20
25 101+20*V(1) 1 [*]* 111+V(2) 12 225+V(1) <A(11) 10
26 111+22*V(1) -9+-2*V(1) [*]* 111+V(2) 12 <A(11) 115+V(1) 10
27 116+22*V(1) -6+-2*V(1) [*]* 111+V(2) 22 (22)A> 115+V(1) 10
28 126+24*V(1) 4 [*]* 111+V(2) 226+V(1) (22)A> 10
<< Success! ==> defined new CTR 2 (PA)
151 1084 32 01 1111 226 (22)A> 10
== Executing PA-CTR 2, V(1)=5, V(2)=7, repcount=3, factor=5/3
235 2182 44 01 112 2221 (22)A> 10
236 2184 46 01 112 2222 (21)B>
237 2187 43 01 112 2222 <A(12) 20
238 2189 41 01 112 2221 <A(11) 12 20
239 2231 -1 01 112 <A(11) 1121 12 20
240 2234 2 01 11 12 (22)A> 1121 12 20
241 2276 44 01 11 12 2221 (22)A> 12 20
242 2281 41 01 11 12 2221 <A(11) 11 20
243 2323 -1 01 11 12 <A(11) 1122 20
244 2328 2 01 11 22 (22)A> 1122 20
245 2372 46 01 11 2223 (22)A> 20
246 2375 43 01 11 2223 <A(11) 10
247 2421 -3 01 11 <A(11) 1123 10
248 2424 0 01 12 (22)A> 1123 10
249 2470 46 01 12 2223 (22)A> 10
250 2472 48 01 12 2224 (21)B>
251 2475 45 01 12 2224 <A(12) 20
252 2477 43 01 12 2223 <A(11) 12 20
253 2523 -3 01 12 <A(11) 1123 12 20
254 2528 0 01 22 (22)A> 1123 12 20
255 2574 46 01 2224 (22)A> 12 20
256 2579 43 01 2224 <A(11) 11 20
257 2627 -5 01 <A(11) 1125 20
258 2630 -2 02 (22)A> 1125 20
259 2680 48 02 2225 (22)A> 20
260 2683 45 02 2225 <A(11) 10
261 2733 -5 02 <A(11) 1125 10
262 2740 -2 11 (10)C> 1125 10
263 2840 48 1126 (10)C> 10
264 2855 45 1126 <A(11) 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 112 221+V(1) (22)A> 10
1 2 2 01 112 222+V(1) (21)B>
2 5 -1 01 112 222+V(1) <A(12) 20
3 7 -3 01 112 221+V(1) <A(11) 12 20
4 9+2*V(1) -5+-2*V(1) 01 112 <A(11) 111+V(1) 12 20
5 12+2*V(1) -2+-2*V(1) 01 11 12 (22)A> 111+V(1) 12 20
6 14+4*V(1) 0 01 11 12 221+V(1) (22)A> 12 20
7 19+4*V(1) -3 01 11 12 221+V(1) <A(11) 11 20
8 21+6*V(1) -5+-2*V(1) 01 11 12 <A(11) 112+V(1) 20
9 26+6*V(1) -2+-2*V(1) 01 11 22 (22)A> 112+V(1) 20
10 30+8*V(1) 2 01 11 223+V(1) (22)A> 20
11 33+8*V(1) -1 01 11 223+V(1) <A(11) 10
12 39+10*V(1) -7+-2*V(1) 01 11 <A(11) 113+V(1) 10
13 42+10*V(1) -4+-2*V(1) 01 12 (22)A> 113+V(1) 10
14 48+12*V(1) 2 01 12 223+V(1) (22)A> 10
15 50+12*V(1) 4 01 12 224+V(1) (21)B>
16 53+12*V(1) 1 01 12 224+V(1) <A(12) 20
17 55+12*V(1) -1 01 12 223+V(1) <A(11) 12 20
18 61+14*V(1) -7+-2*V(1) 01 12 <A(11) 113+V(1) 12 20
19 66+14*V(1) -4+-2*V(1) 01 22 (22)A> 113+V(1) 12 20
20 72+16*V(1) 2 01 224+V(1) (22)A> 12 20
21 77+16*V(1) -1 01 224+V(1) <A(11) 11 20
22 85+18*V(1) -9+-2*V(1) 01 <A(11) 115+V(1) 20
23 88+18*V(1) -6+-2*V(1) 02 (22)A> 115+V(1) 20
24 98+20*V(1) 4 02 225+V(1) (22)A> 20
25 101+20*V(1) 1 02 225+V(1) <A(11) 10
26 111+22*V(1) -9+-2*V(1) 02 <A(11) 115+V(1) 10
27 118+22*V(1) -6+-2*V(1) 11 (10)C> 115+V(1) 10
28 138+26*V(1) 4 116+V(1) (10)C> 10
29 153+26*V(1) 1 116+V(1) <A(11) 11
<< Success! ==> defined new CTR 3 (PPA)
264 2855 45 1126 <A(11) 11
== Executing PA-CTR 1, V(1)=22, V(2)=0, repcount=8, factor=5/3
456 7143 -3 112 <A(11) 1141
457 7146 0 11 12 (22)A> 1141
458 7228 82 11 12 2241 (22)A>
459 7233 79 11 12 2241 <A(11) 22
460 7315 -3 11 12 <A(11) 1141 22
461 7320 0 11 22 (22)A> 1141 22
462 7402 82 11 2242 (22)A> 22
463 7405 79 11 2242 <A(11) 12
464 7489 -5 11 <A(11) 1142 12
465 7492 -2 12 (22)A> 1142 12
466 7576 82 12 2242 (22)A> 12
467 7581 79 12 2242 <A(11) 11
468 7665 -5 12 <A(11) 1143
469 7670 -2 22 (22)A> 1143
470 7756 84 2244 (22)A>
471 7761 81 2244 <A(11) 22
472 7849 -7 <A(11) 1144 22
473 7854 -4 01 (11)B> 1144 22
474 8030 84 01 1144 (11)B> 22
475 8032 86 01 1145 (11)B>
476 8037 83 01 1145 <A(11) 20
477 8040 86 01 1144 12 (22)A> 20
478 8043 83 01 1144 12 <A(11) 10
479 8048 86 01 1144 22 (22)A> 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 112 <A(11) 111+V(1)
1 3 3 11 12 (22)A> 111+V(1)
2 5+2*V(1) 5+2*V(1) 11 12 221+V(1) (22)A>
3 10+2*V(1) 2+2*V(1) 11 12 221+V(1) <A(11) 22
4 12+4*V(1) 0 11 12 <A(11) 111+V(1) 22
5 17+4*V(1) 3 11 22 (22)A> 111+V(1) 22
6 19+6*V(1) 5+2*V(1) 11 222+V(1) (22)A> 22
7 22+6*V(1) 2+2*V(1) 11 222+V(1) <A(11) 12
8 26+8*V(1) -2 11 <A(11) 112+V(1) 12
9 29+8*V(1) 1 12 (22)A> 112+V(1) 12
10 33+10*V(1) 5+2*V(1) 12 222+V(1) (22)A> 12
11 38+10*V(1) 2+2*V(1) 12 222+V(1) <A(11) 11
12 42+12*V(1) -2 12 <A(11) 113+V(1)
13 47+12*V(1) 1 22 (22)A> 113+V(1)
14 53+14*V(1) 7+2*V(1) 224+V(1) (22)A>
15 58+14*V(1) 4+2*V(1) 224+V(1) <A(11) 22
16 66+16*V(1) -4 <A(11) 114+V(1) 22
17 71+16*V(1) -1 01 (11)B> 114+V(1) 22
18 87+20*V(1) 7+2*V(1) 01 114+V(1) (11)B> 22
19 89+20*V(1) 9+2*V(1) 01 115+V(1) (11)B>
20 94+20*V(1) 6+2*V(1) 01 115+V(1) <A(11) 20
21 97+20*V(1) 9+2*V(1) 01 114+V(1) 12 (22)A> 20
22 100+20*V(1) 6+2*V(1) 01 114+V(1) 12 <A(11) 10
23 105+20*V(1) 9+2*V(1) 01 114+V(1) 22 (22)A> 10
<< Success! ==> defined new CTR 4 (PPA)
479 8048 86 01 1144 22 (22)A> 10
== Executing PA-CTR 2, V(1)=0, V(2)=40, repcount=14, factor=5/3
871 20732 142 01 112 2271 (22)A> 10
== Executing PPA-CTR 3 (once), V(1)=70
900 22705 143 1176 <A(11) 11
== Executing PA-CTR 1, V(1)=72, V(2)=0, repcount=25, factor=5/3
1500 61605 -7 11 <A(11) 11126
1501 61608 -4 12 (22)A> 11126
1502 61860 248 12 22126 (22)A>
1503 61865 245 12 22126 <A(11) 22
1504 62117 -7 12 <A(11) 11126 22
1505 62122 -4 22 (22)A> 11126 22
1506 62374 248 22127 (22)A> 22
1507 62377 245 22127 <A(11) 12
1508 62631 -9 <A(11) 11127 12
1509 62636 -6 01 (11)B> 11127 12
1510 63144 248 01 11127 (11)B> 12
1511 63146 250 01 11128 (01)B>
1512 63163 247 01 11128 <A(11) 11
1513 63166 250 01 11127 12 (22)A> 11
1514 63168 252 01 11127 12 22 (22)A>
1515 63173 249 01 11127 12 22 <A(11) 22
1516 63175 247 01 11127 12 <A(11) 11 22
1517 63180 250 01 11127 22 (22)A> 11 22
1518 63182 252 01 11127 222 (22)A> 22
1519 63185 249 01 11127 222 <A(11) 12
1520 63189 245 01 11127 <A(11) 112 12
1521 63192 248 01 11126 12 (22)A> 112 12
1522 63196 252 01 11126 12 222 (22)A> 12
1523 63201 249 01 11126 12 222 <A(11) 11
1524 63205 245 01 11126 12 <A(11) 113
1525 63210 248 01 11126 22 (22)A> 113
1526 63216 254 01 11126 224 (22)A>
1527 63221 251 01 11126 224 <A(11) 22
1528 63229 243 01 11126 <A(11) 114 22
1529 63232 246 01 11125 12 (22)A> 114 22
1530 63240 254 01 11125 12 224 (22)A> 22
1531 63243 251 01 11125 12 224 <A(11) 12
1532 63251 243 01 11125 12 <A(11) 114 12
1533 63256 246 01 11125 22 (22)A> 114 12
1534 63264 254 01 11125 225 (22)A> 12
1535 63269 251 01 11125 225 <A(11) 11
1536 63279 241 01 11125 <A(11) 116
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 114+V(1) <A(11) 111+V(2)
1 3 3 [*]* 113+V(1) 12 (22)A> 111+V(2)
2 5+2*V(2) 5+2*V(2) [*]* 113+V(1) 12 221+V(2) (22)A>
3 10+2*V(2) 2+2*V(2) [*]* 113+V(1) 12 221+V(2) <A(11) 22
4 12+4*V(2) 0 [*]* 113+V(1) 12 <A(11) 111+V(2) 22
5 17+4*V(2) 3 [*]* 113+V(1) 22 (22)A> 111+V(2) 22
6 19+6*V(2) 5+2*V(2) [*]* 113+V(1) 222+V(2) (22)A> 22
7 22+6*V(2) 2+2*V(2) [*]* 113+V(1) 222+V(2) <A(11) 12
8 26+8*V(2) -2 [*]* 113+V(1) <A(11) 112+V(2) 12
9 29+8*V(2) 1 [*]* 112+V(1) 12 (22)A> 112+V(2) 12
10 33+10*V(2) 5+2*V(2) [*]* 112+V(1) 12 222+V(2) (22)A> 12
11 38+10*V(2) 2+2*V(2) [*]* 112+V(1) 12 222+V(2) <A(11) 11
12 42+12*V(2) -2 [*]* 112+V(1) 12 <A(11) 113+V(2)
13 47+12*V(2) 1 [*]* 112+V(1) 22 (22)A> 113+V(2)
14 53+14*V(2) 7+2*V(2) [*]* 112+V(1) 224+V(2) (22)A>
15 58+14*V(2) 4+2*V(2) [*]* 112+V(1) 224+V(2) <A(11) 22
16 66+16*V(2) -4 [*]* 112+V(1) <A(11) 114+V(2) 22
17 69+16*V(2) -1 [*]* 111+V(1) 12 (22)A> 114+V(2) 22
18 77+18*V(2) 7+2*V(2) [*]* 111+V(1) 12 224+V(2) (22)A> 22
19 80+18*V(2) 4+2*V(2) [*]* 111+V(1) 12 224+V(2) <A(11) 12
20 88+20*V(2) -4 [*]* 111+V(1) 12 <A(11) 114+V(2) 12
21 93+20*V(2) -1 [*]* 111+V(1) 22 (22)A> 114+V(2) 12
22 101+22*V(2) 7+2*V(2) [*]* 111+V(1) 225+V(2) (22)A> 12
23 106+22*V(2) 4+2*V(2) [*]* 111+V(1) 225+V(2) <A(11) 11
24 116+24*V(2) -6 [*]* 111+V(1) <A(11) 116+V(2)
<< Success! ==> defined new CTR 5 (PA)
1536 63279 241 01 11125 <A(11) 116
== Executing PA-CTR 5, V(1)=121, V(2)=5, repcount=41, factor=5/3
2520 171355 -5 01 112 <A(11) 11211
2521 171358 -2 01 11 12 (22)A> 11211
2522 171780 420 01 11 12 22211 (22)A>
2523 171785 417 01 11 12 22211 <A(11) 22
2524 172207 -5 01 11 12 <A(11) 11211 22
2525 172212 -2 01 11 22 (22)A> 11211 22
2526 172634 420 01 11 22212 (22)A> 22
2527 172637 417 01 11 22212 <A(11) 12
2528 173061 -7 01 11 <A(11) 11212 12
2529 173064 -4 01 12 (22)A> 11212 12
2530 173488 420 01 12 22212 (22)A> 12
2531 173493 417 01 12 22212 <A(11) 11
2532 173917 -7 01 12 <A(11) 11213
2533 173922 -4 01 22 (22)A> 11213
2534 174348 422 01 22214 (22)A>
2535 174353 419 01 22214 <A(11) 22
2536 174781 -9 01 <A(11) 11214 22
2537 174784 -6 02 (22)A> 11214 22
2538 175212 422 02 22214 (22)A> 22
2539 175215 419 02 22214 <A(11) 12
2540 175643 -9 02 <A(11) 11214 12
2541 175650 -6 11 (10)C> 11214 12
2542 176506 422 11215 (10)C> 12
2543 176510 424 11216 (11)B>
2544 176515 421 11216 <A(11) 20
2545 176518 424 11215 12 (22)A> 20
2546 176521 421 11215 12 <A(11) 10
2547 176526 424 11215 22 (22)A> 10
2548 176528 426 11215 222 (21)B>
2549 176531 423 11215 222 <A(12) 20
2550 176533 421 11215 22 <A(11) 12 20
2551 176535 419 11215 <A(11) 11 12 20
2552 176538 422 11214 12 (22)A> 11 12 20
2553 176540 424 11214 12 22 (22)A> 12 20
2554 176545 421 11214 12 22 <A(11) 11 20
2555 176547 419 11214 12 <A(11) 112 20
2556 176552 422 11214 22 (22)A> 112 20
2557 176556 426 11214 223 (22)A> 20
2558 176559 423 11214 223 <A(11) 10
2559 176565 417 11214 <A(11) 113 10
2560 176568 420 11213 12 (22)A> 113 10
2561 176574 426 11213 12 223 (22)A> 10
2562 176576 428 11213 12 224 (21)B>
2563 176579 425 11213 12 224 <A(12) 20
2564 176581 423 11213 12 223 <A(11) 12 20
2565 176587 417 11213 12 <A(11) 113 12 20
2566 176592 420 11213 22 (22)A> 113 12 20
2567 176598 426 11213 224 (22)A> 12 20
2568 176603 423 11213 224 <A(11) 11 20
2569 176611 415 11213 <A(11) 115 20
2570 176614 418 11212 12 (22)A> 115 20
2571 176624 428 11212 12 225 (22)A> 20
2572 176627 425 11212 12 225 <A(11) 10
2573 176637 415 11212 12 <A(11) 115 10
2574 176642 418 11212 22 (22)A> 115 10
2575 176652 428 11212 226 (22)A> 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 114+V(2) 221+V(1) (22)A> 10
1 2 2 114+V(2) 222+V(1) (21)B>
2 5 -1 114+V(2) 222+V(1) <A(12) 20
3 7 -3 114+V(2) 221+V(1) <A(11) 12 20
4 9+2*V(1) -5+-2*V(1) 114+V(2) <A(11) 111+V(1) 12 20
5 12+2*V(1) -2+-2*V(1) 113+V(2) 12 (22)A> 111+V(1) 12 20
6 14+4*V(1) 0 113+V(2) 12 221+V(1) (22)A> 12 20
7 19+4*V(1) -3 113+V(2) 12 221+V(1) <A(11) 11 20
8 21+6*V(1) -5+-2*V(1) 113+V(2) 12 <A(11) 112+V(1) 20
9 26+6*V(1) -2+-2*V(1) 113+V(2) 22 (22)A> 112+V(1) 20
10 30+8*V(1) 2 113+V(2) 223+V(1) (22)A> 20
11 33+8*V(1) -1 113+V(2) 223+V(1) <A(11) 10
12 39+10*V(1) -7+-2*V(1) 113+V(2) <A(11) 113+V(1) 10
13 42+10*V(1) -4+-2*V(1) 112+V(2) 12 (22)A> 113+V(1) 10
14 48+12*V(1) 2 112+V(2) 12 223+V(1) (22)A> 10
15 50+12*V(1) 4 112+V(2) 12 224+V(1) (21)B>
16 53+12*V(1) 1 112+V(2) 12 224+V(1) <A(12) 20
17 55+12*V(1) -1 112+V(2) 12 223+V(1) <A(11) 12 20
18 61+14*V(1) -7+-2*V(1) 112+V(2) 12 <A(11) 113+V(1) 12 20
19 66+14*V(1) -4+-2*V(1) 112+V(2) 22 (22)A> 113+V(1) 12 20
20 72+16*V(1) 2 112+V(2) 224+V(1) (22)A> 12 20
21 77+16*V(1) -1 112+V(2) 224+V(1) <A(11) 11 20
22 85+18*V(1) -9+-2*V(1) 112+V(2) <A(11) 115+V(1) 20
23 88+18*V(1) -6+-2*V(1) 111+V(2) 12 (22)A> 115+V(1) 20
24 98+20*V(1) 4 111+V(2) 12 225+V(1) (22)A> 20
25 101+20*V(1) 1 111+V(2) 12 225+V(1) <A(11) 10
26 111+22*V(1) -9+-2*V(1) 111+V(2) 12 <A(11) 115+V(1) 10
27 116+22*V(1) -6+-2*V(1) 111+V(2) 22 (22)A> 115+V(1) 10
28 126+24*V(1) 4 111+V(2) 226+V(1) (22)A> 10
<< Success! ==> defined new CTR 6 (PA)
2575 176652 428 11212 226 (22)A> 10
== Executing PA-CTR 6, V(1)=5, V(2)=208, repcount=70, factor=5/3
4535 483672 708 112 22356 (22)A> 10
4536 483674 710 112 22357 (21)B>
4537 483677 707 112 22357 <A(12) 20
4538 483679 705 112 22356 <A(11) 12 20
4539 484391 -7 112 <A(11) 11356 12 20
4540 484394 -4 11 12 (22)A> 11356 12 20
4541 485106 708 11 12 22356 (22)A> 12 20
4542 485111 705 11 12 22356 <A(11) 11 20
4543 485823 -7 11 12 <A(11) 11357 20
4544 485828 -4 11 22 (22)A> 11357 20
4545 486542 710 11 22358 (22)A> 20
4546 486545 707 11 22358 <A(11) 10
4547 487261 -9 11 <A(11) 11358 10
4548 487264 -6 12 (22)A> 11358 10
4549 487980 710 12 22358 (22)A> 10
4550 487982 712 12 22359 (21)B>
4551 487985 709 12 22359 <A(12) 20
4552 487987 707 12 22358 <A(11) 12 20
4553 488703 -9 12 <A(11) 11358 12 20
4554 488708 -6 22 (22)A> 11358 12 20
4555 489424 710 22359 (22)A> 12 20
4556 489429 707 22359 <A(11) 11 20
4557 490147 -11 <A(11) 11360 20
4558 490152 -8 01 (11)B> 11360 20
4559 491592 712 01 11360 (11)B> 20
4560 491605 709 01 11360 <A(11) 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 112 221+V(1) (22)A> 10
1 2 2 112 222+V(1) (21)B>
2 5 -1 112 222+V(1) <A(12) 20
3 7 -3 112 221+V(1) <A(11) 12 20
4 9+2*V(1) -5+-2*V(1) 112 <A(11) 111+V(1) 12 20
5 12+2*V(1) -2+-2*V(1) 11 12 (22)A> 111+V(1) 12 20
6 14+4*V(1) 0 11 12 221+V(1) (22)A> 12 20
7 19+4*V(1) -3 11 12 221+V(1) <A(11) 11 20
8 21+6*V(1) -5+-2*V(1) 11 12 <A(11) 112+V(1) 20
9 26+6*V(1) -2+-2*V(1) 11 22 (22)A> 112+V(1) 20
10 30+8*V(1) 2 11 223+V(1) (22)A> 20
11 33+8*V(1) -1 11 223+V(1) <A(11) 10
12 39+10*V(1) -7+-2*V(1) 11 <A(11) 113+V(1) 10
13 42+10*V(1) -4+-2*V(1) 12 (22)A> 113+V(1) 10
14 48+12*V(1) 2 12 223+V(1) (22)A> 10
15 50+12*V(1) 4 12 224+V(1) (21)B>
16 53+12*V(1) 1 12 224+V(1) <A(12) 20
17 55+12*V(1) -1 12 223+V(1) <A(11) 12 20
18 61+14*V(1) -7+-2*V(1) 12 <A(11) 113+V(1) 12 20
19 66+14*V(1) -4+-2*V(1) 22 (22)A> 113+V(1) 12 20
20 72+16*V(1) 2 224+V(1) (22)A> 12 20
21 77+16*V(1) -1 224+V(1) <A(11) 11 20
22 85+18*V(1) -9+-2*V(1) <A(11) 115+V(1) 20
23 90+18*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 20
24 110+22*V(1) 4 01 115+V(1) (11)B> 20
25 123+22*V(1) 1 01 115+V(1) <A(11) 11
<< Success! ==> defined new CTR 7 (PPA)
4560 491605 709 01 11360 <A(11) 11
== Executing PA-CTR 5, V(1)=356, V(2)=0, repcount=119, factor=5/3
7416 1347929 -5 01 113 <A(11) 11596
7417 1347932 -2 01 112 12 (22)A> 11596
7418 1349124 1190 01 112 12 22596 (22)A>
7419 1349129 1187 01 112 12 22596 <A(11) 22
7420 1350321 -5 01 112 12 <A(11) 11596 22
7421 1350326 -2 01 112 22 (22)A> 11596 22
7422 1351518 1190 01 112 22597 (22)A> 22
7423 1351521 1187 01 112 22597 <A(11) 12
7424 1352715 -7 01 112 <A(11) 11597 12
7425 1352718 -4 01 11 12 (22)A> 11597 12
7426 1353912 1190 01 11 12 22597 (22)A> 12
7427 1353917 1187 01 11 12 22597 <A(11) 11
7428 1355111 -7 01 11 12 <A(11) 11598
7429 1355116 -4 01 11 22 (22)A> 11598
7430 1356312 1192 01 11 22599 (22)A>
7431 1356317 1189 01 11 22599 <A(11) 22
7432 1357515 -9 01 11 <A(11) 11599 22
7433 1357518 -6 01 12 (22)A> 11599 22
7434 1358716 1192 01 12 22599 (22)A> 22
7435 1358719 1189 01 12 22599 <A(11) 12
7436 1359917 -9 01 12 <A(11) 11599 12
7437 1359922 -6 01 22 (22)A> 11599 12
7438 1361120 1192 01 22600 (22)A> 12
7439 1361125 1189 01 22600 <A(11) 11
7440 1362325 -11 01 <A(11) 11601
7441 1362328 -8 02 (22)A> 11601
7442 1363530 1194 02 22601 (22)A>
7443 1363535 1191 02 22601 <A(11) 22
7444 1364737 -11 02 <A(11) 11601 22
7445 1364744 -8 11 (10)C> 11601 22
7446 1367148 1194 11602 (10)C> 22
7447 1367150 1196 11602 10 (11)B>
7448 1367155 1193 11602 10 <A(11) 20
7449 1367160 1196 11603 (11)B> 20
7450 1367173 1193 11603 <A(11) 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 113 <A(11) 111+V(1)
1 3 3 01 112 12 (22)A> 111+V(1)
2 5+2*V(1) 5+2*V(1) 01 112 12 221+V(1) (22)A>
3 10+2*V(1) 2+2*V(1) 01 112 12 221+V(1) <A(11) 22
4 12+4*V(1) 0 01 112 12 <A(11) 111+V(1) 22
5 17+4*V(1) 3 01 112 22 (22)A> 111+V(1) 22
6 19+6*V(1) 5+2*V(1) 01 112 222+V(1) (22)A> 22
7 22+6*V(1) 2+2*V(1) 01 112 222+V(1) <A(11) 12
8 26+8*V(1) -2 01 112 <A(11) 112+V(1) 12
9 29+8*V(1) 1 01 11 12 (22)A> 112+V(1) 12
10 33+10*V(1) 5+2*V(1) 01 11 12 222+V(1) (22)A> 12
11 38+10*V(1) 2+2*V(1) 01 11 12 222+V(1) <A(11) 11
12 42+12*V(1) -2 01 11 12 <A(11) 113+V(1)
13 47+12*V(1) 1 01 11 22 (22)A> 113+V(1)
14 53+14*V(1) 7+2*V(1) 01 11 224+V(1) (22)A>
15 58+14*V(1) 4+2*V(1) 01 11 224+V(1) <A(11) 22
16 66+16*V(1) -4 01 11 <A(11) 114+V(1) 22
17 69+16*V(1) -1 01 12 (22)A> 114+V(1) 22
18 77+18*V(1) 7+2*V(1) 01 12 224+V(1) (22)A> 22
19 80+18*V(1) 4+2*V(1) 01 12 224+V(1) <A(11) 12
20 88+20*V(1) -4 01 12 <A(11) 114+V(1) 12
21 93+20*V(1) -1 01 22 (22)A> 114+V(1) 12
22 101+22*V(1) 7+2*V(1) 01 225+V(1) (22)A> 12
23 106+22*V(1) 4+2*V(1) 01 225+V(1) <A(11) 11
24 116+24*V(1) -6 01 <A(11) 116+V(1)
25 119+24*V(1) -3 02 (22)A> 116+V(1)
26 131+26*V(1) 9+2*V(1) 02 226+V(1) (22)A>
27 136+26*V(1) 6+2*V(1) 02 226+V(1) <A(11) 22
28 148+28*V(1) -6 02 <A(11) 116+V(1) 22
29 155+28*V(1) -3 11 (10)C> 116+V(1) 22
30 179+32*V(1) 9+2*V(1) 117+V(1) (10)C> 22
31 181+32*V(1) 11+2*V(1) 117+V(1) 10 (11)B>
32 186+32*V(1) 8+2*V(1) 117+V(1) 10 <A(11) 20
33 191+32*V(1) 11+2*V(1) 118+V(1) (11)B> 20
34 204+32*V(1) 8+2*V(1) 118+V(1) <A(11) 11
<< Success! ==> defined new CTR 8 (PPA)
7450 1367173 1193 11603 <A(11) 11
== Executing PA-CTR 1, V(1)=599, V(2)=0, repcount=200, factor=5/3
12250 3778373 -7 113 <A(11) 111001
12251 3778376 -4 112 12 (22)A> 111001
12252 3780378 1998 112 12 221001 (22)A>
12253 3780383 1995 112 12 221001 <A(11) 22
12254 3782385 -7 112 12 <A(11) 111001 22
12255 3782390 -4 112 22 (22)A> 111001 22
12256 3784392 1998 112 221002 (22)A> 22
12257 3784395 1995 112 221002 <A(11) 12
12258 3786399 -9 112 <A(11) 111002 12
12259 3786402 -6 11 12 (22)A> 111002 12
12260 3788406 1998 11 12 221002 (22)A> 12
12261 3788411 1995 11 12 221002 <A(11) 11
12262 3790415 -9 11 12 <A(11) 111003
12263 3790420 -6 11 22 (22)A> 111003
12264 3792426 2000 11 221004 (22)A>
12265 3792431 1997 11 221004 <A(11) 22
12266 3794439 -11 11 <A(11) 111004 22
12267 3794442 -8 12 (22)A> 111004 22
12268 3796450 2000 12 221004 (22)A> 22
12269 3796453 1997 12 221004 <A(11) 12
12270 3798461 -11 12 <A(11) 111004 12
12271 3798466 -8 22 (22)A> 111004 12
12272 3800474 2000 221005 (22)A> 12
12273 3800479 1997 221005 <A(11) 11
12274 3802489 -13 <A(11) 111006
12275 3802494 -10 01 (11)B> 111006
12276 3806518 2002 01 111006 (11)B>
12277 3806523 1999 01 111006 <A(11) 20
12278 3806526 2002 01 111005 12 (22)A> 20
12279 3806529 1999 01 111005 12 <A(11) 10
12280 3806534 2002 01 111005 22 (22)A> 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 113 <A(11) 111+V(1)
1 3 3 112 12 (22)A> 111+V(1)
2 5+2*V(1) 5+2*V(1) 112 12 221+V(1) (22)A>
3 10+2*V(1) 2+2*V(1) 112 12 221+V(1) <A(11) 22
4 12+4*V(1) 0 112 12 <A(11) 111+V(1) 22
5 17+4*V(1) 3 112 22 (22)A> 111+V(1) 22
6 19+6*V(1) 5+2*V(1) 112 222+V(1) (22)A> 22
7 22+6*V(1) 2+2*V(1) 112 222+V(1) <A(11) 12
8 26+8*V(1) -2 112 <A(11) 112+V(1) 12
9 29+8*V(1) 1 11 12 (22)A> 112+V(1) 12
10 33+10*V(1) 5+2*V(1) 11 12 222+V(1) (22)A> 12
11 38+10*V(1) 2+2*V(1) 11 12 222+V(1) <A(11) 11
12 42+12*V(1) -2 11 12 <A(11) 113+V(1)
13 47+12*V(1) 1 11 22 (22)A> 113+V(1)
14 53+14*V(1) 7+2*V(1) 11 224+V(1) (22)A>
15 58+14*V(1) 4+2*V(1) 11 224+V(1) <A(11) 22
16 66+16*V(1) -4 11 <A(11) 114+V(1) 22
17 69+16*V(1) -1 12 (22)A> 114+V(1) 22
18 77+18*V(1) 7+2*V(1) 12 224+V(1) (22)A> 22
19 80+18*V(1) 4+2*V(1) 12 224+V(1) <A(11) 12
20 88+20*V(1) -4 12 <A(11) 114+V(1) 12
21 93+20*V(1) -1 22 (22)A> 114+V(1) 12
22 101+22*V(1) 7+2*V(1) 225+V(1) (22)A> 12
23 106+22*V(1) 4+2*V(1) 225+V(1) <A(11) 11
24 116+24*V(1) -6 <A(11) 116+V(1)
25 121+24*V(1) -3 01 (11)B> 116+V(1)
26 145+28*V(1) 9+2*V(1) 01 116+V(1) (11)B>
27 150+28*V(1) 6+2*V(1) 01 116+V(1) <A(11) 20
28 153+28*V(1) 9+2*V(1) 01 115+V(1) 12 (22)A> 20
29 156+28*V(1) 6+2*V(1) 01 115+V(1) 12 <A(11) 10
30 161+28*V(1) 9+2*V(1) 01 115+V(1) 22 (22)A> 10
<< Success! ==> defined new CTR 9 (PPA)
12280 3806534 2002 01 111005 22 (22)A> 10
== Executing PA-CTR 2, V(1)=0, V(2)=1001, repcount=334, factor=5/3
21632 10521938 3338 01 113 221671 (22)A> 10
21633 10521940 3340 01 113 221672 (21)B>
21634 10521943 3337 01 113 221672 <A(12) 20
21635 10521945 3335 01 113 221671 <A(11) 12 20
21636 10525287 -7 01 113 <A(11) 111671 12 20
21637 10525290 -4 01 112 12 (22)A> 111671 12 20
21638 10528632 3338 01 112 12 221671 (22)A> 12 20
21639 10528637 3335 01 112 12 221671 <A(11) 11 20
21640 10531979 -7 01 112 12 <A(11) 111672 20
21641 10531984 -4 01 112 22 (22)A> 111672 20
21642 10535328 3340 01 112 221673 (22)A> 20
21643 10535331 3337 01 112 221673 <A(11) 10
21644 10538677 -9 01 112 <A(11) 111673 10
21645 10538680 -6 01 11 12 (22)A> 111673 10
21646 10542026 3340 01 11 12 221673 (22)A> 10
21647 10542028 3342 01 11 12 221674 (21)B>
21648 10542031 3339 01 11 12 221674 <A(12) 20
21649 10542033 3337 01 11 12 221673 <A(11) 12 20
21650 10545379 -9 01 11 12 <A(11) 111673 12 20
21651 10545384 -6 01 11 22 (22)A> 111673 12 20
21652 10548730 3340 01 11 221674 (22)A> 12 20
21653 10548735 3337 01 11 221674 <A(11) 11 20
21654 10552083 -11 01 11 <A(11) 111675 20
21655 10552086 -8 01 12 (22)A> 111675 20
21656 10555436 3342 01 12 221675 (22)A> 20
21657 10555439 3339 01 12 221675 <A(11) 10
21658 10558789 -11 01 12 <A(11) 111675 10
21659 10558794 -8 01 22 (22)A> 111675 10
21660 10562144 3342 01 221676 (22)A> 10
21661 10562146 3344 01 221677 (21)B>
21662 10562149 3341 01 221677 <A(12) 20
21663 10562151 3339 01 221676 <A(11) 12 20
21664 10565503 -13 01 <A(11) 111676 12 20
21665 10565506 -10 02 (22)A> 111676 12 20
21666 10568858 3342 02 221676 (22)A> 12 20
21667 10568863 3339 02 221676 <A(11) 11 20
21668 10572215 -13 02 <A(11) 111677 20
21669 10572222 -10 11 (10)C> 111677 20
21670 10578930 3344 111678 (10)C> 20
21671 10578936 3346 111679 (11)B>
21672 10578941 3343 111679 <A(11) 20
21673 10578944 3346 111678 12 (22)A> 20
21674 10578947 3343 111678 12 <A(11) 10
21675 10578952 3346 111678 22 (22)A> 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 113 221+V(1) (22)A> 10
1 2 2 01 113 222+V(1) (21)B>
2 5 -1 01 113 222+V(1) <A(12) 20
3 7 -3 01 113 221+V(1) <A(11) 12 20
4 9+2*V(1) -5+-2*V(1) 01 113 <A(11) 111+V(1) 12 20
5 12+2*V(1) -2+-2*V(1) 01 112 12 (22)A> 111+V(1) 12 20
6 14+4*V(1) 0 01 112 12 221+V(1) (22)A> 12 20
7 19+4*V(1) -3 01 112 12 221+V(1) <A(11) 11 20
8 21+6*V(1) -5+-2*V(1) 01 112 12 <A(11) 112+V(1) 20
9 26+6*V(1) -2+-2*V(1) 01 112 22 (22)A> 112+V(1) 20
10 30+8*V(1) 2 01 112 223+V(1) (22)A> 20
11 33+8*V(1) -1 01 112 223+V(1) <A(11) 10
12 39+10*V(1) -7+-2*V(1) 01 112 <A(11) 113+V(1) 10
13 42+10*V(1) -4+-2*V(1) 01 11 12 (22)A> 113+V(1) 10
14 48+12*V(1) 2 01 11 12 223+V(1) (22)A> 10
15 50+12*V(1) 4 01 11 12 224+V(1) (21)B>
16 53+12*V(1) 1 01 11 12 224+V(1) <A(12) 20
17 55+12*V(1) -1 01 11 12 223+V(1) <A(11) 12 20
18 61+14*V(1) -7+-2*V(1) 01 11 12 <A(11) 113+V(1) 12 20
19 66+14*V(1) -4+-2*V(1) 01 11 22 (22)A> 113+V(1) 12 20
20 72+16*V(1) 2 01 11 224+V(1) (22)A> 12 20
21 77+16*V(1) -1 01 11 224+V(1) <A(11) 11 20
22 85+18*V(1) -9+-2*V(1) 01 11 <A(11) 115+V(1) 20
23 88+18*V(1) -6+-2*V(1) 01 12 (22)A> 115+V(1) 20
24 98+20*V(1) 4 01 12 225+V(1) (22)A> 20
25 101+20*V(1) 1 01 12 225+V(1) <A(11) 10
26 111+22*V(1) -9+-2*V(1) 01 12 <A(11) 115+V(1) 10
27 116+22*V(1) -6+-2*V(1) 01 22 (22)A> 115+V(1) 10
28 126+24*V(1) 4 01 226+V(1) (22)A> 10
29 128+24*V(1) 6 01 227+V(1) (21)B>
30 131+24*V(1) 3 01 227+V(1) <A(12) 20
31 133+24*V(1) 1 01 226+V(1) <A(11) 12 20
32 145+26*V(1) -11+-2*V(1) 01 <A(11) 116+V(1) 12 20
33 148+26*V(1) -8+-2*V(1) 02 (22)A> 116+V(1) 12 20
34 160+28*V(1) 4 02 226+V(1) (22)A> 12 20
35 165+28*V(1) 1 02 226+V(1) <A(11) 11 20
36 177+30*V(1) -11+-2*V(1) 02 <A(11) 117+V(1) 20
37 184+30*V(1) -8+-2*V(1) 11 (10)C> 117+V(1) 20
38 212+34*V(1) 6 118+V(1) (10)C> 20
39 218+34*V(1) 8 119+V(1) (11)B>
40 223+34*V(1) 5 119+V(1) <A(11) 20
41 226+34*V(1) 8 118+V(1) 12 (22)A> 20
42 229+34*V(1) 5 118+V(1) 12 <A(11) 10
43 234+34*V(1) 8 118+V(1) 22 (22)A> 10
<< Success! ==> defined new CTR 10 (PPA)
21675 10578952 3346 111678 22 (22)A> 10
== Executing PA-CTR 6, V(1)=0, V(2)=1674, repcount=559, factor=5/3
37327 29364706 5582 11 222796 (22)A> 10
37328 29364708 5584 11 222797 (21)B>
37329 29364711 5581 11 222797 <A(12) 20
37330 29364713 5579 11 222796 <A(11) 12 20
37331 29370305 -13 11 <A(11) 112796 12 20
37332 29370308 -10 12 (22)A> 112796 12 20
37333 29375900 5582 12 222796 (22)A> 12 20
37334 29375905 5579 12 222796 <A(11) 11 20
37335 29381497 -13 12 <A(11) 112797 20
37336 29381502 -10 22 (22)A> 112797 20
37337 29387096 5584 222798 (22)A> 20
37338 29387099 5581 222798 <A(11) 10
37339 29392695 -15 <A(11) 112798 10
37340 29392700 -12 01 (11)B> 112798 10
37341 29403892 5584 01 112798 (11)B> 10
37342 29403894 5586 01 112799 (01)Z>
37342 29403894 5586 01 112799 (01)Z> [stop]
Lines: 431
Top steps: 429
Macro steps: 37342
Basic steps: 29403894
Tape index: 5586
nonzeros: 5600
log10(nonzeros): 3.748
log10(steps ): 7.468
Run state: stop
Input to awk program:
gohalt 1
nbs 3
T 3-state 3-symbol champion #18886871 of Allen Brady
C A.B.: 2 1 1 1 1 2 1-1 1 3-1 2 3 1 0 2 1 1 0 0 0 1-1 2 2 1 1
C The halting transition has been modified to print a 1
5T B1R A2R A1L C2L C0R B1R Z1R A2L B1R
: 5600 29403894
L 6
M 600
pref sim
machv AB3Y_b just simple
machv AB3Y_b-r with repetitions reduced
machv AB3Y_b-1 with tape symbol exponents
machv AB3Y_b-m as 2-bck-macro machine
machv AB3Y_b-a as 2-bck-macro machine with pure additive config-TRs
iam AB3Y_b-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:11:37 CEST 2010
edate Tue Jul 6 22:11:38 CEST 2010
bnspeed 1
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:11:37 CEST 2010