Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. Chapter 34 support. Compact natural-number fields for strict Chapter 34 languages
  4. Chapter 34 support. Fixed-machine interface for compact natural-number fields
Browse chapters
Imports
import CLRSLean.Chapter_34.BinaryNat.Machine.Encoder.Runtime import CLRSLean.Chapter_34.BinaryNat.Machine.Validator import CLRSLean.Chapter_34.BinaryNat.Machine.Adder import CLRSLean.Chapter_34.BinaryNat.Machine.Comparator

Fixed-machine interface for compact natural-number fields

noncomputable sectionnamespace CLRS.Chapter34.Turing.BinaryNat

Encode the length of a Boolean word as a canonical compact natural. The Boolean values are ignored, so callers can first map any finite unary clock alphabet to Bool.

noncomputable def encoderComputableInPolyTime : _root_.Turing.TM2ComputableInPolyTime id id (fun input : List Bool => CLRS.Chapter34.encodeBinaryNat input.length) := Encoder.computableInPolyTime
end CLRS.Chapter34.Turing.BinaryNat