Unary input-length transducer

Public correctness theorem for TM.unaryLengthTM. On input x, the machine emits List.replicate x.length true within the linear bound |x| + 2.

Main result

• TM.unaryLengthTM_computesInTime — unary input-length computation in linear time

theorem Complexity.TM.unaryLengthTM_computesInTime (n : ℕ) : unaryLengthTM.ComputesInTime (fun (x : List Bool) => List.replicate x.length true) fun (m : ℕ) => m + 2

The unary input-length transducer computes List.replicate |x| true within the linear time bound m + 2.