Bell eats counter - Revision history

Int-y1: coq -> rocq

2025-08-25T09:06:41Z

coq -> rocq

← Older revision		Revision as of 09:06, 25 August 2025
Line 5:		Line 5:
	* Increment: when the bouncer in the bell finishes a period, the counter is increased by one.		* Increment: when the bouncer in the bell finishes a period, the counter is increased by one.
	* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.		* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.
	[https://github.com/ccz181078/busycoq/blob/BB6/verify/BECv1.v A ~~Coq~~ proof of a kind of typical behavior doesn't halt.]		[https://github.com/ccz181078/busycoq/blob/BB6/verify/BECv1.v A Rocq proof of a kind of typical behavior doesn't halt.]

	== Examples ==		== Examples ==

Polygon: Used Template:Stub

2025-08-10T22:28:49Z

Used Template:Stub

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

Line 15:		Line 16:
	[https://bbchallenge.org/1RB3LB---3RA0LA_2LA3LB4RB1RB2RA 1RB3LB---3RA0LA_2LA3LB4RB1RB2RA]		[https://bbchallenge.org/1RB3LB---3RA0LA_2LA3LB4RB1RB2RA 1RB3LB---3RA0LA_2LA3LB4RB1RB2RA]

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

Bt2901 at 10:30, 25 August 2024

2024-08-25T10:30:54Z

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

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

Mxdys: link to Coq proof

2024-08-01T06:23:04Z

link to Coq proof

← Older revision		Revision as of 06:23, 1 August 2024
Line 4:		Line 4:
	* Increment: when the bouncer in the bell finishes a period, the counter is increased by one.		* Increment: when the bouncer in the bell finishes a period, the counter is increased by one.
	* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.		* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.
			[https://github.com/ccz181078/busycoq/blob/BB6/verify/BECv1.v A Coq proof of a kind of typical behavior doesn't halt.]

	== Examples ==		== Examples ==

Int-y1: improve style

2024-07-24T02:25:47Z

improve style

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

	* It has both a bell and a counter on the tape.		* It has both a bell and a counter on the tape.
	* Increment: when the bouncer in the bell ~~finish~~ a period, the counter is increased by one.		* Increment: when the bouncer in the bell finishes a period, the counter is increased by one.
	* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.		* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.

Line 14:		Line 13:

	[https://bbchallenge.org/1RB3LB---3RA0LA_2LA3LB4RB1RB2RA 1RB3LB---3RA0LA_2LA3LB4RB1RB2RA]		[https://bbchallenge.org/1RB3LB---3RA0LA_2LA3LB4RB1RB2RA 1RB3LB---3RA0LA_2LA3LB4RB1RB2RA]

			[[Category:Stub]]

Mxdys: /* Examples */

2024-05-29T14:19:27Z

Examples

← Older revision		Revision as of 14:19, 29 May 2024
Line 12:		Line 12:

	[https://bbchallenge.org/1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF 1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF] (more complex than typical ones)		[https://bbchallenge.org/1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF 1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF] (more complex than typical ones)

			[https://bbchallenge.org/1RB3LB---3RA0LA_2LA3LB4RB1RB2RA 1RB3LB---3RA0LA_2LA3LB4RB1RB2RA]

Mxdys: init, add definition and examples

2024-05-28T20:21:14Z

init, add definition and examples

New page

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

* It has both a bell and a counter on the tape.
* Increment: when the bouncer in the bell finish a period, the counter is increased by one.
* Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.

== Examples ==
[https://bbchallenge.org/1RB1RE_0RC1RD_1LA1RC_1LC---_1LF0RE_0LF0LA 1RB1RE_0RC1RD_1LA1RC_1LC---_1LF0RE_0LF0LA]

[https://bbchallenge.org/1RB---_1RC0RA_1LD1RA_1LE0LD_0RE1RF_0RB0LF 1RB---_1RC0RA_1LD1RA_1LE0LD_0RE1RF_0RB0LF]

[https://bbchallenge.org/1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF 1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF] (more complex than typical ones)