GapCVP proof, part 03, continuation 07

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareMissingFirstTrace (count : ℕ) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid (List.replicate count true) [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (sourcePreservingDelimitedPairComparisonWord (List.replicate count true)))) (24 * ((List.replicate count true).length + 1) + 24)

Reject a first word whose unary length prefix has no delimiter.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareTruncatedFirstTrace (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid (List.replicate count true ++ false :: payload) [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (sourcePreservingDelimitedPairComparisonWord (List.replicate count true ++ false :: payload)))) (24 * ((List.replicate count true ++ false :: payload).length + 1) + 24)

Reject a first word shorter than its declared length.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareMissingSecondTrace (first : List Bool) (count : ℕ) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true) [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (sourcePreservingDelimitedPairComparisonWord (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true)))) (24 * ((BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true).length + 1) + 24)

Reject a second word whose unary length prefix has no delimiter.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareTruncatedSecondTrace (first : List Bool) (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid (BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: payload)) [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (sourcePreservingDelimitedPairComparisonWord (BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: payload))))) (24 * ((BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: payload)).length + 1) + 24)

Reject a second word shorter than its declared length.

Equations

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

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.delimitedCompareTotalTrace (input : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid input [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (sourcePreservingDelimitedPairComparisonWord input))) (24 * (input.length + 1) + 24)

Run the pair comparison machine on every input, valid or malformed.

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