Polynomial-time unary input length

Main result

• unaryLength_mem_FP — x ↦ 1^|x| is polynomial-time computable

theorem Complexity.unaryLength_mem_FP : (fun (x : List Bool) => List.replicate x.length true) ∈ FP

Writing one unary mark per input bit is a polynomial-time string function.