Pair-encoding validator — proof internals

The finite-state fold is related to unpair?, then the generic scanner correctness theorem supplies the executable machine proof and exact time bound.

theorem Complexity.TM.pairValidateAccept_fold_eq_true_iff_internal (bits : List Bool) : pairValidateAccept (List.foldl pairValidateStep PairValidateState.next bits) = true ↔ (unpair? bits).isSome = true

The pair-validator fold accepts exactly when unpair? succeeds.

theorem Complexity.TM.pairValidateTM_decidesInTime_internal : pairValidateTM.DecidesInTime validPairEncoding fun (n : ℕ) => n + 2

The finite-state pair validator decides all well-formed pair encodings in the generic scanner's exact n + 2 time bound.

theorem Complexity.TM.pairValidateTM_lift_hoareTime_internal (workTapes : ℕ) (bits : List Bool) : (pairValidateTM.liftTM workTapes).HoareTime (fun (inp : Tape) (work : Fin (0 + workTapes) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool bits) ∧ (work = fun (x : Fin (0 + workTapes)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (0 + workTapes) → Tape) (out : Tape) => AllTapesWF inp work out ∧ inp.cells = (Tape.init (List.map Γ.ofBool bits)).cells ∧ inp.head ≤ bits.length + 2 ∧ (∀ (i : Fin (0 + workTapes)), work i = (Tape.init []).move Dir3.right) ∧ out.head ≤ bits.length + 2 ∧ (bits ∈ validPairEncoding → out.cells 1 = Γ.one) ∧ (bits ∉ validPairEncoding → out.cells 1 = Γ.zero)) (bits.length + 2)

Frame-rich initialized specification for the lifted validator.