Direct predecessor-head formula generation -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setPredecessorHorizonLimit_sound_internal : setPredecessorHorizonLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorFalseRange_sound_internal : emitPredecessorFalseRange.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStayPredecessorMembers_sound_internal (stateCount : ℕ) : (emitStayPredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightZeroPredecessorMembers_sound_internal : emitRightZeroPredecessorMembers.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPositivePredecessorMembers_sound_internal (stateCount : ℕ) : (emitRightPositivePredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPredecessorMembers_sound_internal (stateCount : ℕ) : (emitRightPredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftZeroPredecessorMembers_sound_internal (stateCount : ℕ) : (emitLeftZeroPredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePredecessorHorizonGap_sound_internal : preparePredecessorHorizonGap.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorTail_sound_internal (stateCount : ℕ) : (emitLeftPositivePredecessorTail stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorMembers_sound_internal (stateCount : ℕ) : (emitLeftPositivePredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPredecessorMembers_sound_internal (stateCount : ℕ) : (emitLeftPredecessorMembers stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadMembers_sound_internal (stateCount directionCode : ℕ) : (emitPredecessorHeadMembers stateCount directionCode).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnector_sound_internal : emitPredecessorHeadConnector.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setPredecessorHorizonLimit_effect_internal (values : BinaryValues WorkCount) : setPredecessorHorizonLimit.effect values = Function.update values Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setPredecessorHorizonLimit_emitted_internal (values : BinaryValues WorkCount) : setPredecessorHorizonLimit.emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorFalseRange_effect_internal (values : BinaryValues WorkCount) : emitPredecessorFalseRange.effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.limit₀ - values Work.loop₀))) Work.loop₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorFalseRange_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitPredecessorFalseRange.emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (values Work.limit₀ - values Work.loop₀) fun (x : ℕ) => [directInitConstant false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStayPredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitStayPredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightZeroPredecessorMembers_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) : emitRightZeroPredecessorMembers.effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePredecessorHorizonGap_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) : preparePredecessorHorizonGap.effect values = Function.update (Function.update values Work.temporary₃ (values Work.horizon - values Work.position)) Work.loop₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePredecessorHorizonGap_emitted_internal (values : BinaryValues WorkCount) : preparePredecessorHorizonGap.emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorTail_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) (htemporary : values Work.temporary₀ = 0) (hreference : values Work.reference₀ = 0) : (emitLeftPositivePredecessorTail stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + values Work.temporary₃)) Work.temporary₃ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPositivePredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hpositive : 0 < values Work.position) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPositivePredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftZeroPredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) : (emitLeftZeroPredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPositivePredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPredecessorMembers_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPredecessorMembers stateCount).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadMembers_effect_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadMembers stateCount directionCode).effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStayPredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitStayPredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode ((indexedGateBlocks (values Work.position) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false]) ++ [CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position))] ++ indexedGateBlocks (values Work.horizon - values Work.position) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightZeroPredecessorMembers_emitted_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) (hreference : values Work.reference₀ = 0) : emitRightZeroPredecessorMembers.emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (values Work.horizon + 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPositivePredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hpositive : 0 < values Work.position) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPositivePredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode ((indexedGateBlocks (values Work.position - 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false]) ++ [CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position - 1))] ++ indexedGateBlocks (values Work.horizon + 1 - values Work.position) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftZeroPredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (_hclean : PredecessorHeadClean values) (hposition : values Work.position = 0) (hhorizon : 0 < values Work.horizon) : (emitLeftZeroPredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode ([CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) 0), CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) 1)] ++ indexedGateBlocks (values Work.horizon - 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorTail_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) : (emitLeftPositivePredecessorTail stateCount).emitted values = if values Work.temporary₃ = 0 then [] else List.flatMap CircuitCode.RawGate.encode ([CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position + 1))] ++ indexedGateBlocks (values Work.temporary₃ - 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPositivePredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode ((indexedGateBlocks (values Work.position + 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false]) ++ if values Work.horizon - values Work.position = 0 then [] else [CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position + 1))] ++ indexedGateBlocks (values Work.horizon - values Work.position - 1) fun (x : ℕ) => [CircuitCode.RawGate.constant 0 false])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode (predecessorHeadMemberGates stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPredecessorMembers_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPredecessorMembers stateCount).emitted values = List.flatMap CircuitCode.RawGate.encode (predecessorHeadMemberGates stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) 0)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadMembers_emitted_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadMembers stateCount directionCode).emitted values = List.flatMap CircuitCode.RawGate.encode (predecessorHeadMemberGates stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) directionCode)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnector_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₁ = 0) : emitPredecessorHeadConnector.effect values = Function.update (Function.update (Function.update (Function.update (Function.update values Work.loop₁ 0) Work.available (values Work.available + 1)) Work.reference₀ 0) Work.reference₁ 0) Work.temporary₃ (values Work.temporary₃ + 2)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnector_emitted_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₁ = 0) : emitPredecessorHeadConnector.emitted values = { op := AndOrOp.or, input₀ := values Work.available - values Work.temporary₃, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnectors_effect_internal (values : BinaryValues WorkCount) (hloop₁ : values Work.loop₁ = 0) (hreference₀ : values Work.reference₀ = 0) (hreference₁ : values Work.reference₁ = 0) : (emitPredecessorHeadConnector.binaryFor Work.loop₀ Work.limit₀).effect values = Function.update (Function.update (Function.update values Work.available (values Work.available + (values Work.limit₀ - values Work.loop₀))) Work.temporary₃ (values Work.temporary₃ + 2 * (values Work.limit₀ - values Work.loop₀))) Work.loop₀ (values Work.loop₀ + (values Work.limit₀ - values Work.loop₀))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnectors_emitted_internal (values : BinaryValues WorkCount) (available count : ℕ) (hloop₀ : values Work.loop₀ = 0) (hlimit : values Work.limit₀ = count) (hloop₁ : values Work.loop₁ = 0) (hreference₀ : values Work.reference₀ = 0) (hreference₁ : values Work.reference₁ = 0) (havailable : values Work.available = available + count + 1) (htemporary : values Work.temporary₃ = 2) : (emitPredecessorHeadConnector.binaryFor Work.loop₀ Work.limit₀).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedRightFoldConnectors AndOrOp.or available count (fixedWidthSizeAt count 1))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_effect_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadFormula stateCount directionCode).effect values = Function.update values Work.available (values Work.available + movedHeadPredecessorSize (values Work.horizon))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_emitted_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadFormula stateCount directionCode).emitted values = List.flatMap CircuitCode.RawGate.encode (predecessorHeadFormulaSchedule stateCount (values Work.horizon) (values Work.configBase) (values Work.available) (values Work.tapeIndex) (values Work.position) directionCode)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setPredecessorHorizonLimit_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) : setPredecessorHorizonLimit.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorFalseRange_requires_internal (values : BinaryValues WorkCount) (hle : values Work.loop₀ ≤ values Work.limit₀) (hemit : values Work.emitCounter = 0) : emitPredecessorFalseRange.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnector_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hloop₁ : values Work.loop₁ = 0) (hoffset : values Work.temporary₃ ≤ values Work.available) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) : emitPredecessorHeadConnector.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStayPredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitStayPredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightZeroPredecessorMembers_requires_internal (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) : emitRightZeroPredecessorMembers.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPositivePredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hpositive : 0 < values Work.position) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPositivePredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitRightPredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePredecessorHorizonGap_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hloop : values Work.loop₀ = 0) (htarget : values Work.position ≤ values Work.horizon) : preparePredecessorHorizonGap.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftZeroPredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hposition : values Work.position = 0) (hhorizon : 0 < values Work.horizon) : (emitLeftZeroPredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorTail_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitLeftPositivePredecessorTail stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPositivePredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPredecessorMembers_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitLeftPredecessorMembers stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadMembers_requires_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadMembers stateCount directionCode).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_requires_internal (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) : (emitPredecessorHeadFormula stateCount directionCode).requires values ↔ PredecessorHeadClean values ∧ 0 < values Work.horizon ∧ values Work.position ≤ values Work.horizon

Pointwise all-prefix width certificates

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_spaceBoundByWidth_internal (stateCount directionCode : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), PredecessorHeadClean (values inputLength)) (hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon) (htarget : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.available + movedHeadPredecessorSize (values inputLength Work.horizon) ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.horizon + 1) + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 + 2 * (values inputLength Work.horizon + 2) ≤ width inputLength) : (emitPredecessorHeadFormula stateCount directionCode).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_sound_internal (stateCount directionCode : ℕ) : (emitPredecessorHeadFormula stateCount directionCode).Sound