Skelet 26 - Revision history

Polygon: Added analysis by int-y1 and meithecatte

2026-03-09T19:02:53Z

Added analysis by int-y1 and meithecatte

Polygon: Removed Template:Stub

2026-03-08T21:43:09Z

Removed Template:Stub

← Older revision		Revision as of 21:43, 8 March 2026
Line 1:		Line 1:
	{{machine\|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---~~}}{{Stub~~}}		{{machine\|1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---}}
	{{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"/>		{{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"/>

Polygon: /* Skelet 15 */ wording

2026-03-07T19:23:00Z

Skelet 15: wording

← Older revision		Revision as of 19:23, 7 March 2026
Line 50:		Line 50:
	== Skelet 15 ==		== 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, ~~starting~~ in configuration D(0, 0, 1) after 21 steps.<ref name="Sligocki2023"/>		{{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 ==		== See also ==

Polygon: Mentioned Skelet 26/15 being adjacent to Skelet 33

2026-03-07T19:22:19Z

Mentioned Skelet 26/15 being adjacent to Skelet 33

← Older revision		Revision as of 19:22, 7 March 2026
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>
Line 53:		Line 53:

	== See also ==		== See also ==
	* [[Skelet 33]]
	* [https://www.sligocki.com/2023/02/02/skelet-34.html Skelet #34 is Infinite]		* [https://www.sligocki.com/2023/02/02/skelet-34.html Skelet #34 is Infinite]

Polygon: Added missing definition of b(n) and see also section

2026-03-07T19:16:56Z

Added missing definition of b(n) and see also section

← Older revision		Revision as of 19:16, 7 March 2026
Line 7:		Line 7:
	https://www.sligocki.com/2023/02/05/shift-overflow.html		https://www.sligocki.com/2023/02/05/shift-overflow.html
	<pre>		<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) = L(k) 0000
	L(2k+1) = L(k) 0001		L(2k+1) = L(k) 0001
Line 49:		Line 51:

	{{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, starting in configuration D(0, 0, 1) after 21 steps.<ref name="Sligocki2023"/>		{{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, starting in configuration D(0, 0, 1) after 21 steps.<ref name="Sligocki2023"/>

			== See also ==
			* [[Skelet 33]]
			* [https://www.sligocki.com/2023/02/02/skelet-34.html Skelet #34 is Infinite]

	== References ==		== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]

Polygon: /* Analysis by Shawn Ligocki */ adjusted heading level (as Skelet 15 doesn't have its own analysis section due to equivalence)

2026-03-07T18:29:39Z

Analysis by Shawn Ligocki: adjusted heading level (as Skelet 15 doesn't have its own analysis section due to equivalence)

← Older revision		Revision as of 18:29, 7 March 2026
Line 4:		Line 4:
	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]] ===		== Analysis by [[User:Sligocki\|Shawn Ligocki]] ==
	https://www.sligocki.com/2023/02/05/shift-overflow.html		https://www.sligocki.com/2023/02/05/shift-overflow.html
	<pre>		<pre>

Polygon: /* Skelet 15 */ expanded section

2026-03-07T18:27:16Z

Skelet 15: expanded section

← Older revision		Revision as of 18:27, 7 March 2026
Line 48:		Line 48:
	== Skelet 15 ==		== Skelet 15 ==

	{{TM\|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet #15''' ~~is equivalent to Skelet 26. It~~ was proven to be non-halting together with Skelet 26 in January 2024 by int-y1 and meithecatte.<ref name="~~Forum2615~~"/>		{{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, starting in configuration D(0, 0, 1) after 21 steps.<ref name="Sligocki2023"/>

	== References ==		== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]

Polygon: Added analysis for Skelet 26

2026-03-07T18:20:44Z

Added analysis for Skelet 26

← Older revision		Revision as of 18:20, 7 March 2026
Line 3:		Line 3:

	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>
			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 ==

Polygon: Mentioned proof of non-halting

2026-03-07T18:17:47Z

Mentioned proof of non-halting

← Older revision		Revision as of 18:17, 7 March 2026
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>		{{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.

			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 15 ==		== Skelet 15 ==

	{{TM\|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet 15''' is equivalent to Skelet 26.		{{TM\|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet #15''' is equivalent to Skelet 26. It was proven to be non-halting together with Skelet 26 in January 2024 by int-y1 and meithecatte.<ref name="Forum2615"/>

	== References ==		== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]

Polygon: /* Skelet 15 */ added a short sentence about equivalence

2026-03-07T18:11:14Z

Skelet 15: added a short sentence about equivalence

← Older revision		Revision as of 18:11, 7 March 2026
Line 3:		Line 3:

	== Skelet 15 ==		== Skelet 15 ==

			{{TM\|1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC}}, also called '''Skelet 15''' is equivalent to Skelet 26.

	== References ==		== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]