Boolean-formula codec internals

This module proves the stack-machine, round-trip, injectivity, and length properties of the canonical postfix formula encoding.

theorem Complexity.FormulaCode.Token.length_encode_internal (token : Token) : token.encode.length = token.codeLength

Internal exact length of one encoded token.

theorem Complexity.FormulaCode.Token.decodePrefix?_encode_append_internal (token : Token) (suffix : List Bool) : decodePrefix? (token.encode ++ suffix) = some (token, suffix)

Internal token-prefix round trip.

theorem Complexity.FormulaCode.run?_append_internal (first second : List Token) (stack : List BoolFormula) : run? (first ++ second) stack = (run? first stack).bind (run? second)

Internal composition law for the postfix stack machine.

theorem Complexity.FormulaCode.run?_tokens_internal (formula : BoolFormula) (stack : List BoolFormula) : run? (tokens formula) stack = some (formula :: stack)

Internal stack specification for the postfix tokens of a formula.

theorem Complexity.FormulaCode.build?_tokens_internal (formula : BoolFormula) : build? (tokens formula) = some formula

Internal reconstruction of a formula from its own postfix tokens.

theorem Complexity.FormulaCode.length_tokens_internal (formula : BoolFormula) : (tokens formula).length = formula.size

Internal exact token-count theorem.

theorem Complexity.FormulaCode.decodeTokens?_flatMap_encode_append_internal (stream : List Token) (suffix : List Bool) : decodeTokens? stream.length (List.flatMap Token.encode stream ++ suffix) = some (stream, suffix)

Internal fixed-count token-list round trip.

theorem Complexity.FormulaCode.decodePrefix?_encode_append_internal (formula : BoolFormula) (suffix : List Bool) : decodePrefix? (encode formula ++ suffix) = some (formula, suffix)

Internal formula-prefix round trip.

theorem Complexity.FormulaCode.decode?_encode_internal (formula : BoolFormula) : decode? (encode formula) = some formula

Internal exact-decoder round trip.

theorem Complexity.FormulaCode.encode_injective_internal : Function.Injective encode

Internal injectivity of canonical formula serialization.

theorem Complexity.FormulaCode.decode?_encode_append_eq_none_internal (formula : BoolFormula) {suffix : List Bool} (hsuffix : suffix ≠ []) : decode? (encode formula ++ suffix) = none

Internal rejection of nonempty trailing data by exact decoding.

theorem Complexity.FormulaCode.length_encode_internal (formula : BoolFormula) : (encode formula).length = formula.size + 1 + (List.map Token.codeLength (tokens formula)).sum

Internal exact formula-code length.