Andrej Dudenhefner

I annotated my comments above only once. Of course, they hold for other files in this PR. Ideally, the new proofs should compile with ``` Set Default Goal Selector "!"....

Would it possibly help to have a slightly different compiler to FRACTRAN instead? E.g. split each state MMA `p` into two and have a fractran transition `p |-> p'`. So...

FYI, I am currently writing an `MMA` which evaluates a closed `L` term such that, if the result is an encoded natural number, then this number is extracted into a...

> The hope is to remove the heavy TM machinery from the proof of `L_computable -> TM_computable`. (FYI) I have now written fast, compact, alternative proofs of `L_computable -> MMA_computable`...

> @mrhaandi Does this comprises the input-output relation as well as the termination predicate ? It follows exactly the definitions of @yforster, so it is about the input/output relations on...

> What is `MM 2` ? Is this the instance of `MM n` with `n := 2`? Yes. > problematic because it described and used in the CPP'19 paper. Isn't...

> Do you suggest completely suppressing the semantics of `MM` where the conditional jump occurs on the `0` case (as opposed to the `1+n` case) ? Yes. Currently, I see...

Also, I am looking to fully replace `CM2` by `MM2` in proofs, to logically deduplicate the library.

> Also, I am looking to fully replace `CM2` by `MM2` in proofs, to logically deduplicate the library. I put in the effort to replace `CM2` by `MM2` in reductions...

> I think it makes sense to let `MMA` be the central, exposed notion (maybe renamed into something entirely new like `MCM` (Minsky Counter Machines, unfortunately just `CM` is already...