Sync bouncer counter - Revision history

Int-y1: coq -> rocq

2025-08-25T09:05:55Z

coq -> rocq

← Older revision		Revision as of 09:05, 25 August 2025
Line 5:		Line 5:
	* Increment: the counter is increased by one, and the bouncer finishes a period.		* Increment: the counter is increased by one, and the bouncer finishes a period.
	* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).		* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).
	[https://github.com/ccz181078/busycoq/blob/BB6/verify/SBCv1.v A ~~Coq~~ proof of a kind of typical behavior doesn't halt.]		[https://github.com/ccz181078/busycoq/blob/BB6/verify/SBCv1.v A Rocq proof of a kind of typical behavior doesn't halt.]

	== Examples ==		== Examples ==

Polygon: Used Template:Stub

2025-08-10T22:40:24Z

Used Template:Stub

← Older revision		Revision as of 22:40, 10 August 2025
Line 1:		Line 1:
			{{Stub}}
	A '''sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:		A '''sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:

Line 11:		Line 12:
	{{TM\|1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA}} (complex)		{{TM\|1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA}} (complex)

	~~[[Category:Stub]]~~
	[[Category:Zoology]]		[[Category:Zoology]]

Int-y1 at 02:10, 9 July 2025

2025-07-09T02:10:21Z

← Older revision		Revision as of 02:10, 9 July 2025
Line 1:		Line 1:
	'''~~Sync~~ bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:		A '''sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:

	* It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.		* It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.
Line 7:		Line 7:

	== Examples ==		== Examples ==
	~~[https://bbchallenge.org/~~1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB ~~1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB]~~ (most common)		{{TM\|1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB}} (most common)

	~~[https://bbchallenge.org/~~1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA ~~1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA]~~ (complex)		{{TM\|1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA}} (complex)

	[[Category:Stub]]		[[Category:Stub]]
	[[Category:Zoology]]		[[Category:Zoology]]

Bt2901 at 10:31, 25 August 2024

2024-08-25T10:31:47Z

← Older revision		Revision as of 10:31, 25 August 2024
Line 10:		Line 10:

	[https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA] (complex)		[https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA] (complex)

			[[Category:Stub]]
			[[Category:Zoology]]

Mxdys: add link to Coq proof

2024-08-01T06:24:58Z

add link to Coq proof

← Older revision		Revision as of 06:24, 1 August 2024
Line 4:		Line 4:
	* Increment: the counter is increased by one, and the bouncer finishes a period.		* Increment: the counter is increased by one, and the bouncer finishes a period.
	* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).		* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).
			[https://github.com/ccz181078/busycoq/blob/BB6/verify/SBCv1.v A Coq proof of a kind of typical behavior doesn't halt.]

	== Examples ==		== Examples ==

Int-y1: bold name

2024-07-24T03:18:50Z

bold name

← Older revision		Revision as of 03:18, 24 July 2024
Line 1:		Line 1:
	~~== Definition ==~~		'''Sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:
	Sync bouncer counter is a informal class of Turing machines. A typical Turing machine in this class has the following behavior:

	* It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.		* It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.
	* Increment: the counter is increased by one, and the bouncer ~~finish~~ a period.		* Increment: the counter is increased by one, and the bouncer finishes a period.
	* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).		* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).

Mxdys: init, add definition and examples

2024-05-30T09:51:13Z

init, add definition and examples

New page

== Definition ==
Sync bouncer counter is a informal class of Turing machines. A typical Turing machine in this class has the following behavior:

* It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.
* Increment: the counter is increased by one, and the bouncer finish a period.
* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).

== Examples ==
[https://bbchallenge.org/1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB 1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB] (most common)

[https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA] (complex)