GapCVP proof, part 04, continuation 07

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairFirstTrace (count : ℕ) (tail first second matchedFirst matchedSecond base outer output scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 0 (List.replicate count true ++ false :: tail) first second matchedFirst matchedSecond base outer output scratch) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 1 tail (List.replicate count true ++ first) second matchedFirst matchedSecond base outer output scratch)) (count + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairSecondTrace (count : ℕ) (tail first second matchedFirst matchedSecond base outer output scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 1 (List.replicate count true ++ false :: tail) first second matchedFirst matchedSecond base outer output scratch) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 2 tail first (List.replicate count true ++ second) matchedFirst matchedSecond base outer output scratch)) (count + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairSquareCopyTrace (count : ℕ) (outer output scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 8 [] [] [] [] [] (List.replicate count true) outer output scratch) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 9 [] [] [] [] [] [] outer (List.replicate count true ++ output) (List.replicate count true ++ scratch))) (count + 1)

Copy the unary base to both output and scratch during a squaring iteration.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairSquareRestoreTrace (count : ℕ) (base outer output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 9 [] [] [] [] [] base outer output (List.replicate count true)) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 7 [] [] [] [] [] (List.replicate count true ++ base) outer output [])) (count + 1)

Restore the unary base from scratch and return to the squaring loop.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairSquareCleanupTrace (count : ℕ) (output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 10 [] [] [] [] [] (List.replicate count true) [] output []) (some (Turing.haltList CNFUnaryPairIndexTM.actualUnaryPairIndexMachine output)) (count + 1)

Clear the unary base after the squaring loop and halt with the accumulated output.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairSquareTrace (baseCount outerCount : ℕ) (output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 7 [] [] [] [] [] (List.replicate baseCount true) (List.replicate outerCount true) output []) (some (Turing.haltList CNFUnaryPairIndexTM.actualUnaryPairIndexMachine (List.replicate (baseCount * outerCount) true ++ output))) (outerCount * (2 * baseCount + 3) + baseCount + 2)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairComparedConfiguration (first second matched : ℕ) : CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.Cfg

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairCompareTrace (first second matched : ℕ) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 2 [] (List.replicate first true) (List.replicate second true) (List.replicate matched true) (List.replicate matched true) [] [] [] []) (some (unaryPairComparedConfiguration first second matched)) (min first second + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairGreaterBaseTrace (first matchedFirst matchedSecond : ℕ) (base outer output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 3 [] (List.replicate first true) [] (List.replicate matchedFirst true) (List.replicate matchedSecond true) base outer output []) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 4 [] [] [] [] (List.replicate matchedSecond true) (List.replicate (first + matchedFirst) true ++ base) (List.replicate (first + matchedFirst) true ++ outer) (List.replicate (first + matchedFirst) true ++ output) [])) (first + matchedFirst + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairGreaterOffsetTrace (count : ℕ) (base outer output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 4 [] [] [] [] (List.replicate count true) base outer output []) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 7 [] [] [] [] [] base outer (List.replicate count true ++ output) [])) (count + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairLessBaseTrace (second matchedFirst matchedSecond : ℕ) (base outer output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 5 [] [] (List.replicate second true) (List.replicate matchedFirst true) (List.replicate matchedSecond true) base outer output []) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 6 [] [] [] (List.replicate matchedFirst true) [] (List.replicate (second + matchedSecond) true ++ base) (List.replicate (second + matchedSecond) true ++ outer) output [])) (second + matchedSecond + 1)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalCert.unaryPairLessOffsetTrace (count : ℕ) (base outer output : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 6 [] [] [] (List.replicate count true) [] base outer output []) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 7 [] [] [] [] [] base outer (List.replicate count true ++ output) [])) (count + 1)

GapCVP reduction support.

Equations

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