Dominique Larchey-Wendling

Switch from MM to MMA

12

This is a draft PR for switching from `MM n` to `MMA n` to put `MMA` upfront in place of `MM`. The list of included reduction so far: - `BSM...

Several problems on sequences of nats or Booleans

8

This PR intends to answer a request from Yves Bertot concerning the undecidability of equality testing between (constructive) real numbers. For the moment, the PR implements the following problems, but...

CI launched even if not PR

10

Hi @yforster, I am not sure if this is a bug but in the current configuration under my fork of `coq-8.12`, the `CI` is launched after every push, _even if...

New seed: halting of MM2 starting from the fixed state (1,(0,0))

2

This PR is a first step towards a proof of undecidability of Wang tilings with a fixed origin (ie tiling the North-East part of the plane). The intended reduction chain...

Hi @ole1986, https://github.com/ole1986/centronic-py/blob/0a00870dfe922ca667e380fd919f0acce8e6a838/centronic-stick.py#L349 According to the source code, it seems the increment is common for all channels on a given unit: it is a `unit` dependent notion only. On the...