GapCVP proof, part 04

def GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords {α : Type} [Encodable α] [DecidableEq α] (records : List α) : List α

GapCVP reduction support.

Equations

• GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords records = GapCVP.ThreeCNFReduction.sortedElements records.toFinset

@[simp]

theorem GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords_sortedElements {α : Type} [Encodable α] [DecidableEq α] (records : Finset α) : sourceOrderedDistinctRecords (ThreeCNFReduction.sortedElements records) = ThreeCNFReduction.sortedElements records

theorem GapCVP.CNFInputDependentRecordSort.sourceOrderedDistinctRecords_eq_of_nodup_pairwise {α : Type} [Encodable α] [DecidableEq α] (source candidate : List α) (hmembership : ∀ (record : α), record ∈ candidate ↔ record ∈ source) (hnodup : candidate.Nodup) (hpairwise : List.Pairwise (fun (first second : α) => Encodable.encode first ≤ Encodable.encode second) candidate) : CNFFiniteRecordSort.sourceOrderedDistinctRecords source = candidate

def GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue : List Bool → ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue [] = 0
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue (false :: remaining) = 2 * GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue remaining
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue (true :: remaining) = 2 * GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue remaining + 1

@[simp]

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue_encodeNat (number : ℕ) : littleEndianNaturalValue (Computability.encodeNat number) = number

def GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering (first second : List Bool) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering_eq_value_order (first second : List Bool) : littleEndianNaturalOrdering first second = if littleEndianNaturalValue first < littleEndianNaturalValue second then CNFEncodedClauseSort.EncodedWordOrdering.less else if littleEndianNaturalValue second < littleEndianNaturalValue first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

@[simp]

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering_encodeNat (first second : ℕ) : littleEndianNaturalOrdering (Computability.encodeNat first) (Computability.encodeNat second) = if first < second then CNFEncodedClauseSort.EncodedWordOrdering.less else if second < first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

def GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering (input : List Bool) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

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

def GapCVP.CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering_valid (first second suffix : List Bool) : delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = littleEndianNaturalOrdering first second

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering_encodeNat (first second : ℕ) (suffix : List Bool) : delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord (Computability.encodeNat first) ++ BinaryEncoding.lengthPrefixedWord (Computability.encodeNat second) ++ suffix) = if first < second then CNFEncodedClauseSort.EncodedWordOrdering.less else if second < first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

def GapCVP.CNFNaturalOrderComparator.naturalCompareWordsStatement : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) CNFEncodedClauseSort.DelimitedPairComparisonState

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.CNFNaturalOrderComparator.delimitedNaturalComparisonMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFNaturalOrderComparator.naturalCompareConfiguration (phase : Fin 12) (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalComparisonMachine_init (input : List Bool) : Turing.initList delimitedNaturalComparisonMachine input = naturalCompareConfiguration 0 CNFEncodedClauseSort.EncodedWordOrdering.invalid input [] [] [] [] [] [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFNaturalOrderComparator.tacticNaturalCompareStepTac : Lean.ParserDescr

Executes the naturalCompareStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.CNFNaturalOrderComparator.naturalCompareWordsTraceInitial (first second input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.invalid input firstCounter firstReversed secondCounter secondReversed first second source sourcePrefix output) (some (naturalCompareConfiguration 7 (littleEndianNaturalOrdering first second) input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)) (first.length + second.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_missingFirst (count : ℕ) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (List.replicate count true) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_shortFirst (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (List.replicate count true ++ false :: payload) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_missingSecond (first : List Bool) (count : ℕ) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

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

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderTotalComparator.sourcePreservingNaturalComparison_valid (first second suffix : List Bool) : CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = BinaryEncoding.lengthPrefixedWord (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) ++ CNFEncodedClauseSort.encodedWordOrderingWord (CNFNaturalOrderComparator.littleEndianNaturalOrdering first second)

theorem GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNatural_step_eq_old (configuration : CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.Cfg) (hphase : configuration.l ≠ some 6) : CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step configuration = CNFEncodedClauseSort.delimitedPairComparisonMachine.step configuration

Internal support shared across GapCVP continuation modules.