Skelet 26: Difference between revisions
Jump to navigation
Jump to search
Mentioned proof of non-halting |
→Skelet 15: wording |
||
| (5 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{machine|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---}}{{Stub}} | {{machine|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---}}{{Stub}} | ||
{{TM|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---}}, called '''Skelet #26''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is a [[Shift overflow counter]] and has an individual proof of non-halting in [[Coq-BB5]].<ref>https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v</ref> It is equivalent to Skelet 15. | {{TM|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---}}, called '''Skelet #26''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is a [[Shift overflow counter]] and has an individual proof of non-halting in [[Coq-BB5]].<ref>https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v</ref> It is equivalent to Skelet 15. Both Skelet 26 and Skelet 15 are [[adjacent]] to [[Skelet 33]].<ref name="Sligocki2023"/> | ||
Skelet 26 was proven to be non-halting in January 2024 by int-y1 and meithecatte.<ref name="Forum2615">https://discuss.bbchallenge.org/t/skelet-26-and-15-do-not-halt-coq-proof/183</ref> | Skelet 26 was proven to be non-halting in January 2024 by int-y1 and meithecatte.<ref name="Forum2615">https://discuss.bbchallenge.org/t/skelet-26-and-15-do-not-halt-coq-proof/183</ref> | ||
== Analysis by [[User:Sligocki|Shawn Ligocki]] == | |||
https://www.sligocki.com/2023/02/05/shift-overflow.html | |||
<pre> | |||
b(n) is the number we have to add to n to reach the “next” power of 2 (strictly greater than n) or the smallest number which when added to n “expands” the binary representation to a larger length. | |||
L(2k) = L(k) 0000 | |||
L(2k+1) = L(k) 0001 | |||
D(n, a, m) = L(n) 000 <C 101a R(m) | |||
E(n, a, m) = L(n) 00 <C 101a R(m) | |||
F(n, a, m) = L(n) 0 <C 101a R(m) | |||
G(n, a, m) = L(n) <C 101a R(m) | |||
D(n, a, m) -> D(n+1, a, m+1) (if b(m) > 1) | |||
L(n) 000 <C -> L(n+1) 000 B> | |||
1000 <C -> <C 1111 | |||
0000 <C -> 1000 B> | |||
E> R(n) -> <C R(n+1) | |||
E> 11 -> 11 E> | |||
E> 10 -> <C 11 | |||
11 <C -> <C 10 | |||
B> 1010 -> 1111 E> | |||
1111 <C -> <C 1010 | |||
B> 1011 -> 0111 E> | |||
0111 <C -> <C 1011 | |||
D(n-1, 0, 2^k - 1) -> E(n, 1, 2^k) | |||
0 1111 E> 11^k 0 -> <C 1011 10^k 11 | |||
E(n, a, m) -> E(n', 1, m') (if b(m) > n) (n' < n) | |||
0100 0000^k <C 101a R(m) -> 0100 1000^k <C 101a R(m + 2^k - 1) | |||
0100 1000^k <C 101a R(m + 2^k - 1) -> <C 1011 10^2k 11 1a R(m + 2^k - 1) | |||
D(n-1, 1, 2^k - 1) -> G(2n, 0, 2^{k-1}) | |||
1000 0000^n 0111 E> 11^m+1 0 -> 01 0000^n+1 <C 1010 10^m 11 | |||
G(n, a, m) -> E(n', a', m') (if b(m) > n) (n' < n) | |||
01 0000^k <C 101a R(m) -> <C 10 10^2k 11 1a R(m + 2^k - 1) | |||
Start -> D(0, 0, 11) @ Step 85 | |||
</pre> | |||
== Skelet 15 == | == Skelet 15 == | ||
{{TM|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet #15''' | {{TM|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet #15''', was proven to be non-halting together with Skelet 26 in January 2024 by int-y1 and meithecatte<ref name="Forum2615"/> and has an individual proof of non-halting in Coq-BB5.<ref>https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v</ref> It is a [[permutation]] of Skelet 26, achieved by starting Skelet 26 in state E and then normalizing to [[TNF]].<ref name="Sligocki2023">https://www.sligocki.com/2023/02/05/shift-overflow.html</ref> Its analysis is equivalent to that of Skelet 26, except that it starts in configuration D(0, 0, 1) after 21 steps.<ref name="Sligocki2023"/> | ||
== See also == | |||
* [https://www.sligocki.com/2023/02/02/skelet-34.html Skelet #34 is Infinite] | |||
== References == | == References == | ||
[[Category:BB(5)]] | [[Category:BB(5)]] | ||
Latest revision as of 19:23, 7 March 2026
1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- (bbch), called Skelet #26, was one of Skelet's 43 holdouts and one of the last holdouts in BB(5). It is a Shift overflow counter and has an individual proof of non-halting in Coq-BB5.[1] It is equivalent to Skelet 15. Both Skelet 26 and Skelet 15 are adjacent to Skelet 33.[2]
Skelet 26 was proven to be non-halting in January 2024 by int-y1 and meithecatte.[3]
Analysis by Shawn Ligocki
https://www.sligocki.com/2023/02/05/shift-overflow.html
b(n) is the number we have to add to n to reach the “next” power of 2 (strictly greater than n) or the smallest number which when added to n “expands” the binary representation to a larger length.
L(2k) = L(k) 0000
L(2k+1) = L(k) 0001
D(n, a, m) = L(n) 000 <C 101a R(m)
E(n, a, m) = L(n) 00 <C 101a R(m)
F(n, a, m) = L(n) 0 <C 101a R(m)
G(n, a, m) = L(n) <C 101a R(m)
D(n, a, m) -> D(n+1, a, m+1) (if b(m) > 1)
L(n) 000 <C -> L(n+1) 000 B>
1000 <C -> <C 1111
0000 <C -> 1000 B>
E> R(n) -> <C R(n+1)
E> 11 -> 11 E>
E> 10 -> <C 11
11 <C -> <C 10
B> 1010 -> 1111 E>
1111 <C -> <C 1010
B> 1011 -> 0111 E>
0111 <C -> <C 1011
D(n-1, 0, 2^k - 1) -> E(n, 1, 2^k)
0 1111 E> 11^k 0 -> <C 1011 10^k 11
E(n, a, m) -> E(n', 1, m') (if b(m) > n) (n' < n)
0100 0000^k <C 101a R(m) -> 0100 1000^k <C 101a R(m + 2^k - 1)
0100 1000^k <C 101a R(m + 2^k - 1) -> <C 1011 10^2k 11 1a R(m + 2^k - 1)
D(n-1, 1, 2^k - 1) -> G(2n, 0, 2^{k-1})
1000 0000^n 0111 E> 11^m+1 0 -> 01 0000^n+1 <C 1010 10^m 11
G(n, a, m) -> E(n', a', m') (if b(m) > n) (n' < n)
01 0000^k <C 101a R(m) -> <C 10 10^2k 11 1a R(m + 2^k - 1)
Start -> D(0, 0, 11) @ Step 85
Skelet 15
1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC (bbch), also called Skelet #15, was proven to be non-halting together with Skelet 26 in January 2024 by int-y1 and meithecatte[3] and has an individual proof of non-halting in Coq-BB5.[4] It is a permutation of Skelet 26, achieved by starting Skelet 26 in state E and then normalizing to TNF.[2] Its analysis is equivalent to that of Skelet 26, except that it starts in configuration D(0, 0, 1) after 21 steps.[2]