Conversions between bit-string encodings

TheoremNumber normalizer restores its work stacks and prepends its answer#✓fully proved

The canonical normalizer restores both work stacks and prepends its answer to an arbitrary output suffix, within a linear bit bound.

theorem normalizeNat_run_frame (x out : List Bool) (v : Bool) :
    ∃ v', RunLe prog (2 * x.length + 3)
      ⟨some (.read none), v, st x [] out⟩
      ⟨some .done, v', st [] [] (normalizeNat x ++ out)⟩

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .read last =>
    .peek .input (fun _ o => o.isSome) <| .branch id
      (.pop .input (fun _ o => o.getD false) <|
        .push .buffer id <| .goto fun b => .read (some b))
      (if last = some false then
        .push .buffer (fun _ => true) (.goto fun _ => .copy)
       else .goto fun _ => .copy)
  | .copy => moveB .buffer .output some id .copy .done
  | .done => .halt

CSLibExt/Computability/Complexity/FramedCNF/NormalizeMachine.lean:46

def st (input buffer output : List Bool) : K → List Bool
  | .input => input
  | .buffer => buffer
  | .output => output

CSLibExt/Computability/Complexity/FramedCNF/NormalizeMachine.lean:58

def normalizeNat (bits : List Bool) : List Bool :=
  if bits.getLast? = some false then bits ++ [true] else bits

CSLibExt/Computability/Complexity/FramedCNF/Normalize.lean:27

Uses 11 · Used by 2

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stack contents for the payload normalizer invariant · Normalization of a raw binary natural-number payload · Runs within a step budget

Proof usesRead phase of the payload normalizer consumes each bit once · Payload normalization adds at most one bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · Running the bit-moving loop

Used byList canonicalizer normalizes one element · Number-pair projector normalizes both fields of a raw pair frame

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.