GapCVP proof, part 03, continuation 07

def GapCVP.CNFEncodedClauseSort.lengthPrefixedPairCases {motive : List Bool → Sort u_1} (missingFirst : (count : ℕ) → motive (List.replicate count true)) (truncatedFirst : (count : ℕ) → (tail : List Bool) → tail.length < count → motive (List.replicate count true ++ false :: tail)) (missingSecond : (first : List Bool) → (count : ℕ) → motive (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true)) (truncatedSecond : (first : List Bool) → (count : ℕ) → (tail : List Bool) → tail.length < count → motive (BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: tail))) (valid : (first second suffix : List Bool) → motive (BinaryEncoding.lengthPrefixedWord first ++ (BinaryEncoding.lengthPrefixedWord second ++ suffix))) (input : List Bool) : motive input

Exhaust the five shapes of two length-prefixed fields, including missing delimiters and truncated payloads. The motive may carry a computation trace, not just a proposition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CNFEncodedClauseSort.sourcePreservingDelimitedPairComparisonComputable : BitTM sourcePreservingDelimitedPairComparisonWord

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering_eq_equal_iff (first second : List Bool) : lexicographicEncodedWordOrdering first second = EncodedWordOrdering.equal ↔ first = second