GapCVP proof, part 03, continuation 06

@[reducible, inline]

abbrev GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.NonComparisonStepLift (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) : Type

Lifts each old-machine step outside the specialized comparison phase.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.cleanup (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] source sourcePrefix output)) (firstCounter.length + firstReversed.length + secondCounter.length + secondReversed.length + firstForward.length + secondForward.length + 1)

Clears the six comparison work tapes using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.trailing (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (input source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] source sourcePrefix output) (some (delimitedCompareConfiguration 9 outcome [] [] [] [] [] [] [] (input.reverse ++ source) (List.replicate input.length true ++ sourcePrefix) output)) (input.length + 1)

Restores the trailing input using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.source (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] source sourcePrefix output) (some (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix (false :: (source.reverse ++ output)))) (source.length + 1)

Restores the saved source using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.prefix (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix output) (some (Turing.haltList delimitedPairComparisonMachine (List.replicate sourcePrefix.length true ++ output))) (sourcePrefix.length + 1)

Restores prefix markers and halts using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.delimitedCompareRestoredWord (outcome : EncodedWordOrdering) (input source sourcePrefix output : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.finish (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (Turing.haltList delimitedPairComparisonMachine (delimitedCompareRestoredWord outcome input source sourcePrefix output))) (firstCounter.length + firstReversed.length + secondCounter.length + secondReversed.length + firstForward.length + secondForward.length + 3 * input.length + source.length + sourcePrefix.length + 5)

Restores every saved tape and halts using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareFinishTrace (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (Turing.haltList delimitedPairComparisonMachine (delimitedCompareRestoredWord outcome input source sourcePrefix output))) (firstCounter.length + firstReversed.length + secondCounter.length + secondReversed.length + firstForward.length + secondForward.length + 3 * input.length + source.length + sourcePrefix.length + 5)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.firstPrefix (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 0 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 1 outcome tail (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Reads the first unary prefix using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstPrefixTrace (outcome : EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 1 outcome tail (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.firstMissingPrefix (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 0 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Detects a missing first delimiter using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstMissingPrefixTrace (outcome : EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.firstPayload (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload tail firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 1 outcome (payload ++ tail) (List.replicate payload.length true) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 2 outcome tail [] (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) (payload.length + 1)

Reads the first payload using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.firstPartialPayload (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload remainingCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 1 outcome payload (List.replicate payload.length true ++ remainingCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 1 outcome [] remainingCounter (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Reads an incomplete first payload using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstPartialPayloadTrace (outcome : EncodedWordOrdering) (payload remainingCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 1 outcome payload (List.replicate payload.length true ++ remainingCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 1 outcome [] remainingCounter (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.secondPrefix (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 2 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 3 outcome tail firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Reads the second unary prefix using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareSecondPrefixTrace (outcome : EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 2 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 3 outcome tail firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.secondMissingPrefix (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 2 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Detects a missing second delimiter using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareSecondMissingPrefixTrace (outcome : EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 2 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.secondPayload (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload tail firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 3 outcome (payload ++ tail) firstCounter firstReversed (List.replicate payload.length true) secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 4 outcome tail firstCounter firstReversed [] (payload.reverse ++ secondReversed) firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) (payload.length + 1)

Reads the second payload using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.secondPartialPayload (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload remainingCounter firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 3 outcome payload firstCounter firstReversed (List.replicate payload.length true ++ remainingCounter) secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 3 outcome [] firstCounter firstReversed remainingCounter (payload.reverse ++ secondReversed) firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Reads an incomplete second payload using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareSecondPartialPayloadTrace (outcome : EncodedWordOrdering) (payload remainingCounter firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 3 outcome payload firstCounter firstReversed (List.replicate payload.length true ++ remainingCounter) secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 3 outcome [] firstCounter firstReversed remainingCounter (payload.reverse ++ secondReversed) firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.firstRecord (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload tail firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 0 outcome (BinaryEncoding.lengthPrefixedWord payload ++ tail) [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 2 outcome tail [] (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward ((BinaryEncoding.lengthPrefixedWord payload).reverse ++ source) (List.replicate (BinaryEncoding.lengthPrefixedWord payload).length true ++ sourcePrefix) output)) (2 * payload.length + 2)

Reads the first length-prefixed record using any compatible machine step.

Equations

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

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstRecordTrace (outcome : EncodedWordOrdering) (payload tail firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome (BinaryEncoding.lengthPrefixedWord payload ++ tail) [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 2 outcome tail [] (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward ((BinaryEncoding.lengthPrefixedWord payload).reverse ++ source) (List.replicate (BinaryEncoding.lengthPrefixedWord payload).length true ++ sourcePrefix) output)) (2 * payload.length + 2)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.secondRecord (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (payload tail firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 2 outcome (BinaryEncoding.lengthPrefixedWord payload ++ tail) firstCounter firstReversed [] secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 4 outcome tail firstCounter firstReversed [] (payload.reverse ++ secondReversed) firstForward secondForward ((BinaryEncoding.lengthPrefixedWord payload).reverse ++ source) (List.replicate (BinaryEncoding.lengthPrefixedWord payload).length true ++ sourcePrefix) output)) (2 * payload.length + 2)

Reads the second length-prefixed record using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.reverseFirst (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 4 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 5 outcome input firstCounter [] secondCounter secondReversed (firstReversed.reverse ++ firstForward) secondForward source sourcePrefix output)) (firstReversed.length + 1)

Reverses the first payload using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.reverseSecond (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 5 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter [] firstForward (secondReversed.reverse ++ secondForward) source sourcePrefix output)) (secondReversed.length + 1)

Reverses the second payload using any compatible machine step.

Equations

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

def GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals : List Bool → List Bool → List Bool × List Bool

Drop matching leading bits, leaving both words at their first difference.

Equations

• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals [] x✝ = ([], x✝)
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals (bit :: left) [] = (bit :: left, [])
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals (false :: left) (true :: right) = (false :: left, true :: right)
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals (true :: left) (false :: right) = (true :: left, false :: right)
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals (false :: left) (false :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals left right
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals (true :: left) (true :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResiduals left right

noncomputable def GapCVP.CNFEncodedClauseSort.delimitedCompareWordsTrace (outcome : EncodedWordOrdering) (first second input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed first second source sourcePrefix output) (some (delimitedCompareConfiguration 7 (lexicographicEncodedWordOrdering first second) input firstCounter firstReversed secondCounter secondReversed (lexicographicEncodedWordResiduals first second).1 (lexicographicEncodedWordResiduals first second).2 source sourcePrefix output)) (first.length + 1)

Compare two encoded words and leave their unmatched suffixes in the machine state.

Equations

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

theorem GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResidualsFirstLengthLe (first second : List Bool) : (lexicographicEncodedWordResiduals first second).1.length ≤ first.length

theorem GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordResidualsSecondLengthLe (first second : List Bool) : (lexicographicEncodedWordResiduals first second).2.length ≤ second.length

noncomputable def GapCVP.CNFEncodedClauseSort.DelimitedCompareTrace.validAssembly (chosenStep : delimitedPairComparisonMachine.Cfg → Option delimitedPairComparisonMachine.Cfg) (lift : NonComparisonStepLift chosenStep) (first second suffix firstResidual secondResidual : List Bool) (comparisonOutcome : EncodedWordOrdering) (comparisonTime : ℕ) (comparisonTrace : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 6 EncodedWordOrdering.invalid suffix [] [] [] [] first second ((BinaryEncoding.lengthPrefixedWord second).reverse ++ (BinaryEncoding.lengthPrefixedWord first).reverse) (List.replicate (BinaryEncoding.lengthPrefixedWord second).length true ++ List.replicate (BinaryEncoding.lengthPrefixedWord first).length true) []) (some (delimitedCompareConfiguration 7 comparisonOutcome suffix [] [] [] [] firstResidual secondResidual ((BinaryEncoding.lengthPrefixedWord second).reverse ++ (BinaryEncoding.lengthPrefixedWord first).reverse) (List.replicate (BinaryEncoding.lengthPrefixedWord second).length true ++ List.replicate (BinaryEncoding.lengthPrefixedWord first).length true) [])) comparisonTime) : StateTransition.EvalsToInTime chosenStep (delimitedCompareConfiguration 0 EncodedWordOrdering.invalid (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) [] [] [] [] [] [] [] [] []) (some (Turing.haltList delimitedPairComparisonMachine (delimitedCompareRestoredWord comparisonOutcome suffix ((BinaryEncoding.lengthPrefixedWord second).reverse ++ (BinaryEncoding.lengthPrefixedWord first).reverse) (List.replicate (BinaryEncoding.lengthPrefixedWord second).length true ++ List.replicate (BinaryEncoding.lengthPrefixedWord first).length true) []))) (2 * first.length + 2 + (2 * second.length + 2) + (first.length + 1) + (second.length + 1) + comparisonTime + (firstResidual.length + secondResidual.length + 3 * suffix.length + ((BinaryEncoding.lengthPrefixedWord second).reverse ++ (BinaryEncoding.lengthPrefixedWord first).reverse).length + (List.replicate (BinaryEncoding.lengthPrefixedWord second).length true ++ List.replicate (BinaryEncoding.lengthPrefixedWord first).length true).length + 5))

Parses both records, runs a supplied phase-six comparison, and restores the input.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_missingFirst (count : ℕ) : delimitedPairWordOrdering (List.replicate count true) = EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_shortFirst (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : delimitedPairWordOrdering (List.replicate count true ++ false :: payload) = EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_missingSecond (first : List Bool) (count : ℕ) : delimitedPairWordOrdering (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true) = EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_shortSecond (first : List Bool) (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : delimitedPairWordOrdering (BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: payload)) = EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.