Documentation

Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary

Unary natural numbers #

The encoding and its equation are moved unchanged from the former quantitative primitives.

source
def Turing.MultiTapeTM.encUnary :
ℕ ↪ List Bool

Natural numbers in unary: n is encoded by n ones.

Instances For
    source
    @[simp]
    theorem Turing.MultiTapeTM.encUnary_apply (n : ℕ) :
    encUnary n = List.replicate n true