GapCVP proof, part 07, continuation 05

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceMinimumWord (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceMaximumWord (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowSlotWord (grid : Polynomial ℕ) (coordinate : CNFFiveFamilyForbiddenWindowCoordinateTM.FiveFamilyForbiddenWindowCoordinate) (symbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowFirstLowWord (grid : Polynomial ℕ) (leftSymbol centerSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowFirstHighWord (grid : Polynomial ℕ) (leftSymbol centerSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowSecondLowWord (grid : Polynomial ℕ) (rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowSecondHighWord (grid : Polynomial ℕ) (rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowOuterLowWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowMiddleLeftWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowMiddleRightWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowOuterHighWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowMiddleLowWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawWindowMiddleHighWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveForbiddenRawDistinctPayloadWord (first second third fourth payload : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveForbiddenExactWindowDistinctPayloadWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) (payload : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveForbiddenExactWindowWholeClauseRecordWord (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveFamilyForbiddenExactWindowWholeClauseRecordComputable (grid : Polynomial ℕ) (leftSymbol centerSymbol rightSymbol nextSymbol : ℕ) : BitTM (fiveForbiddenExactWindowWholeClauseRecordWord grid leftSymbol centerSymbol rightSymbol nextSymbol)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveForbiddenRawSourceMinimumWord_valid {α : Type} [Encodable α] (first second : List Bool → List Bool) (input : List Bool) (firstAtom secondAtom : α) (hfirst : first input = List.replicate (Encodable.encode firstAtom) true) (hsecond : second input = List.replicate (Encodable.encode secondAtom) true) : CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceMinimumWord first second input = List.replicate (Encodable.encode (CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMinimum firstAtom secondAtom)) true

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveForbiddenRawSourceMaximumWord_valid {α : Type} [Encodable α] (first second : List Bool → List Bool) (input : List Bool) (firstAtom secondAtom : α) (hfirst : first input = List.replicate (Encodable.encode firstAtom) true) (hsecond : second input = List.replicate (Encodable.encode secondAtom) true) : CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceMaximumWord first second input = List.replicate (Encodable.encode (CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMaximum firstAtom secondAtom)) true

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM.fiveFamilyForbiddenRawDistinctPayloadWord_valid {α : Type} [Encodable α] [DecidableEq α] (first second third fourth payload : List Bool → List Bool) (input : List Bool) (firstAtom secondAtom thirdAtom fourthAtom : α) (output : α → List Bool) (hfirst : first input = List.replicate (Encodable.encode firstAtom) true) (hsecond : second input = List.replicate (Encodable.encode secondAtom) true) (hthird : third input = List.replicate (Encodable.encode thirdAtom) true) (hfourth : fourth input = List.replicate (Encodable.encode fourthAtom) true) (hpayload : ∀ (atom : α), payload (List.replicate (Encodable.encode atom) true) = output atom) (hordered : List.Pairwise (fun (left right : α) => Encodable.encode left ≤ Encodable.encode right) [firstAtom, secondAtom, thirdAtom, fourthAtom]) : fiveForbiddenRawDistinctPayloadWord first second third fourth payload input = List.flatMap output [firstAtom, secondAtom, thirdAtom, fourthAtom].dedup