Repeated Word List - Revision history

Polygon: /* RWLAcc */ underscore in Quick_Sim

2026-04-26T18:51:21Z

RWLAcc: underscore in Quick_Sim

← Older revision		Revision as of 18:51, 26 April 2026
Line 9:		Line 9:

	=== RWLAcc ===		=== RWLAcc ===
	RWLAcc is a block-based [[accelerated simulator]] similar to [[~~Quick Sim~~]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v		RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick_Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

	== History ==		== History ==

Polygon: Undo revision 6975 by Polygon (talk) using headings makes it easier to link to these variants later

2026-04-02T14:37:41Z

Undo revision 6975 by Polygon (talk) using headings makes it easier to link to these variants later

← Older revision		Revision as of 14:37, 2 April 2026
Line 8:		Line 8:
	== Variants ==		== Variants ==

	~~'''~~RWLAcc~~''':~~		=== RWLAcc ===

	RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v		RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

Polygon: /* Variants */ used the format from the NGram CPS page

2026-04-02T14:31:37Z

Variants: used the format from the NGram CPS page

← Older revision		Revision as of 14:31, 2 April 2026
Line 8:		Line 8:
	== Variants ==		== Variants ==

	~~===~~ RWLAcc ~~===~~		'''RWLAcc''':

	RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v		RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

Polygon: added RepWL_ES as a synonym

2026-04-01T10:40:12Z

added RepWL_ES as a synonym

← Older revision		Revision as of 10:40, 1 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]		[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]
	'''Repeated Word List''' (short '''RepWL''') is a [[decider]] first introduced as part of [[Coq-BB5]]. It is a subset of the general [[CTL]] method and works by generating a graph of TM configurations, if the graph is shown to be closed, the TM is proven non-halting.		'''Repeated Word List''' (short '''RepWL''', also called '''RepWL_ES''' where ES means ExecState) is a [[decider]] first introduced as part of [[Coq-BB5]]. It is a subset of the general [[CTL]] method and works by generating a graph of TM configurations, if the graph is shown to be closed, the TM is proven non-halting.

	== Method ==		== Method ==

Polygon: /* RWLAcc */ similar to Quick Sim

2026-03-31T21:31:53Z

RWLAcc: similar to Quick Sim

← Older revision		Revision as of 21:31, 31 March 2026
Line 9:		Line 9:

	=== RWLAcc ===		=== RWLAcc ===
	RWLAcc is a block-based [[accelerated simulator]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v		RWLAcc is a block-based [[accelerated simulator]] similar to [[Quick Sim]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

	== History ==		== History ==

Polygon: /* Method */ referencing

2026-03-31T21:30:49Z

Method: referencing

← Older revision		Revision as of 21:30, 31 March 2026
Line 4:		Line 4:

	== Method ==		== Method ==
	It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.		It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref>

	== Variants ==		== Variants ==

Polygon: /* RWLAcc */ linked accelerated simulator

2026-03-31T21:26:26Z

RWLAcc: linked accelerated simulator

← Older revision		Revision as of 21:26, 31 March 2026
Line 9:		Line 9:

	=== RWLAcc ===		=== RWLAcc ===
	RWLAcc is a block-based accelerated simulator capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v		RWLAcc is a block-based [[accelerated simulator]] capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

	== History ==		== History ==

Polygon: Added RWLAcc section (currently lacking details)

2026-03-31T21:20:59Z

Added RWLAcc section (currently lacking details)

← Older revision		Revision as of 21:20, 31 March 2026
Line 5:		Line 5:
	== Method ==		== Method ==
	It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.		It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.

			== Variants ==

			=== RWLAcc ===
			RWLAcc is a block-based accelerated simulator capable of supporting L0 and L1 [[Inductive Proof System\|inductive rules]].<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1333106708117196941</ref> It is part of mxdys's [[BB(6)]] Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

	== History ==		== History ==

Polygon: Added general description to the lead

2026-03-31T20:16:29Z

Added general description to the lead

← Older revision		Revision as of 20:16, 31 March 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]		[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]
	'''Repeated Word List''' (short '''RepWL''') is a [[decider]] first introduced as part of [[Coq-BB5]]. It is a subset of the general [[CTL]] method.		'''Repeated Word List''' (short '''RepWL''') is a [[decider]] first introduced as part of [[Coq-BB5]]. It is a subset of the general [[CTL]] method and works by generating a graph of TM configurations, if the graph is shown to be closed, the TM is proven non-halting.

	== Method ==		== Method ==

Polygon: Splitting the description into a separate paragraph

2026-03-31T19:18:55Z

Splitting the description into a separate paragraph

← Older revision		Revision as of 19:18, 31 March 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]		[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png\|thumb\|500px\|RepWL graph for non-halting TM {{TM\|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]]
	'''Repeated Word List''' (short '''RepWL''') is a [[decider]]. It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.		'''Repeated Word List''' (short '''RepWL''') is a [[decider]] first introduced as part of [[Coq-BB5]]. It is a subset of the general [[CTL]] method.

			== Method ==
			It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit <math>B</math>. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a <math>+</math> in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to <math>T-1</math> and one where it stays at <math>T+</math>. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.

	== History ==		== History ==