Direct-unrolling next-atom generator -- proof internals

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.advanceAvailableValues (values : BinaryValues WorkCount) (amount : ℕ) : BinaryValues WorkCount

Advances the generator's available-wire register by amount.

Equations

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue_sound_internal (stateIndex : ℕ) : (emitOldStateValue stateIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldHeadValue_sound_internal (stateCount tapeIndex : ℕ) : (emitOldHeadValue stateCount tapeIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldCellValue_sound_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) : (emitOldCellValue stateCount tapeCount tapeIndex symbolIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue_requires_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hemit : values Work.emitCounter = 0) : (emitOldStateValue stateIndex).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldHeadValue_requires_internal (stateCount tapeIndex : ℕ) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitOldHeadValue stateCount tapeIndex).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldCellValue_requires_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitOldCellValue stateCount tapeCount tapeIndex symbolIndex).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue_effect_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : (emitOldStateValue stateIndex).effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldHeadValue_effect_internal (stateCount tapeIndex : ℕ) (values : BinaryValues WorkCount) (htape : values Work.tapeIndex = 0) (htemporary : values Work.temporary₀ = 0) (hreference : values Work.reference₀ = 0) : (emitOldHeadValue stateCount tapeIndex).effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldCellValue_effect_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (htape : values Work.tapeIndex = 0) (hsymbol : values Work.symbolIndex = 0) (htemporary₀ : values Work.temporary₀ = 0) (htemporary₁ : values Work.temporary₁ = 0) (htemporary₂ : values Work.temporary₂ = 0) (hreference : values Work.reference₀ = 0) : (emitOldCellValue stateCount tapeCount tapeIndex symbolIndex).effect values = Function.update values Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue_emitted_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) : (emitOldStateValue stateIndex).emitted values = (CircuitCode.RawGate.copy (transitionStateRef (values Work.configBase) stateIndex)).encode

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldHeadValue_emitted_internal (stateCount tapeIndex : ℕ) (values : BinaryValues WorkCount) : (emitOldHeadValue stateCount tapeIndex).emitted values = (CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) tapeIndex (values Work.position))).encode

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldCellValue_emitted_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) : (emitOldCellValue stateCount tapeCount tapeIndex symbolIndex).emitted values = (CircuitCode.RawGate.copy (transitionCellRef stateCount tapeCount (values Work.horizon) (values Work.configBase) tapeIndex (values Work.position) symbolIndex)).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_sound_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_requires_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_effect_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (htape : values Work.tapeIndex = 0) (hsymbol : values Work.symbolIndex = 0) (htemporary₀ : values Work.temporary₀ = 0) (htemporary₁ : values Work.temporary₁ = 0) (htemporary₂ : values Work.temporary₂ = 0) (hreference : values Work.reference₀ = 0) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_emitted_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).emitted values = List.flatMap CircuitCode.RawGate.encode (nextCellCopySchedule stateCount tapeCount (values Work.horizon) (values Work.configBase) tapeIndex (values Work.position) symbolIndex)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_spaceBoundByWidth_internal (stateCount tapeCount tapeIndex symbolIndex : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex (values inputLength Work.position) symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + values inputLength Work.position) + (values inputLength Work.horizon + 2) + tapeCount + tapeIndex + 4 ≤ width inputLength) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHaltedOrFormula_sound_internal (haltStateIndex : ℕ) (childSize : Polynomial ℕ) (oldValue nextValue : BinaryRoutine WorkCount) (hold : oldValue.Sound) (hnext : nextValue.Sound) : (emitHaltedOrFormula haltStateIndex childSize oldValue nextValue).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHaltedOrFormula_requires_internal (haltStateIndex : ℕ) (childSize : Polynomial ℕ) (oldValue nextValue : BinaryRoutine WorkCount) (values : BinaryValues WorkCount) (hclean : HaltedOrFormulaClean values) (holdRequires : oldValue.requires (advanceAvailableValues values 1)) (holdEffect : oldValue.effect (advanceAvailableValues values 1) = advanceAvailableValues values 2) (hnextRequires : nextValue.requires (advanceAvailableValues values 5)) (hnextEffect : nextValue.effect (advanceAvailableValues values 5) = advanceAvailableValues values (5 + Polynomial.eval (values Work.horizon) childSize)) : (emitHaltedOrFormula haltStateIndex childSize oldValue nextValue).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHaltedOrFormula_effect_internal (haltStateIndex : ℕ) (childSize : Polynomial ℕ) (oldValue nextValue : BinaryRoutine WorkCount) (values : BinaryValues WorkCount) (hclean : HaltedOrFormulaClean values) (holdEffect : oldValue.effect (advanceAvailableValues values 1) = advanceAvailableValues values 2) (hnextEffect : nextValue.effect (advanceAvailableValues values 5) = advanceAvailableValues values (5 + Polynomial.eval (values Work.horizon) childSize)) : (emitHaltedOrFormula haltStateIndex childSize oldValue nextValue).effect values = advanceAvailableValues values (Polynomial.eval (values Work.horizon) childSize + 7)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHaltedOrFormula_emitted_internal (haltStateIndex : ℕ) (childSize : Polynomial ℕ) (oldValue nextValue : BinaryRoutine WorkCount) (oldWire : ℕ) (nextSchedule : CircuitCode.RawCircuit) (values : BinaryValues WorkCount) (hclean : HaltedOrFormulaClean values) (holdEffect : oldValue.effect (advanceAvailableValues values 1) = advanceAvailableValues values 2) (hnextEffect : nextValue.effect (advanceAvailableValues values 5) = advanceAvailableValues values (5 + Polynomial.eval (values Work.horizon) childSize)) (holdEmitted : oldValue.emitted (advanceAvailableValues values 1) = (CircuitCode.RawGate.copy oldWire).encode) (hnextEmitted : nextValue.emitted (advanceAvailableValues values 5) = List.flatMap CircuitCode.RawGate.encode nextSchedule) (hsize : List.length nextSchedule = Polynomial.eval (values Work.horizon) childSize) : (emitHaltedOrFormula haltStateIndex childSize oldValue nextValue).emitted values = List.flatMap CircuitCode.RawGate.encode (nextHaltedOrSchedule (transitionStateRef (values Work.configBase) haltStateIndex) (values Work.available) oldWire nextSchedule)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_sound_internal {k : ℕ} (tm : NTM k) (state : tm.Q) : (emitNextStateFormula tm state).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_requires_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_effect_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).effect values = Function.update values Work.available (values Work.available + nextStateFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_emitted_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).emitted values = List.flatMap CircuitCode.RawGate.encode (nextStateFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (stateIndex tm state) (stateIndex tm tm.qhalt) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (state : tm.Q) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), CaseFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon → values inputLength Work.available + nextStateFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon + 2 * TM.binaryPolynomialValueCap (stateNextChildPolynomial tm state) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextStateFormula tm state).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitNextHeadFormula tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_requires_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitNextHeadFormula tm tape).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitNextHeadFormula tm tape).effect values = Function.update values Work.available (values Work.available + nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitNextHeadFormula tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (nextHeadFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.index) (values Work.position) (stateIndex tm tm.qhalt) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), MovedHeadFormulaClean (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) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon + 1 → values inputLength Work.available + nextHeadFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + 2 * TM.binaryPolynomialValueCap predecessorHeadSchedulePolynomial (values inputLength Work.horizon) + 2 * (values inputLength Work.horizon + 2) + values inputLength Work.horizon + 2 * TM.binaryPolynomialValueCap (headNextChildPolynomial tm tape) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextHeadFormula tm tape).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_sound_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : (emitNextWrittenCellFormula tm tape symbol).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_requires_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitNextWrittenCellFormula tm tape symbol).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_effect_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) : (emitNextWrittenCellFormula tm tape symbol).effect values = Function.update values Work.available (values Work.available + nextWrittenCellFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_emitted_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitNextWrittenCellFormula tm tape symbol).emitted values = List.flatMap CircuitCode.RawGate.encode (nextWrittenCellFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.toTapeSlot.index) (values Work.position) (↑(symbolIndex symbol)) (stateIndex tm tm.qhalt) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), WrittenCellFormulaClean (values inputLength)) (hposition : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon + 1) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon + 1 → values inputLength Work.available + nextWrittenCellFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon + 2 * TM.binaryPolynomialValueCap (writtenNextChildPolynomial tm tape symbol) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextWrittenCellFormula tm tape symbol).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextChildPolynomial_eval_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : Polynomial.eval T (stateNextChildPolynomial tm state) = effectFormulaScheduleSize (transitionCases tm).length k T (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextFormulaPolynomial_eval_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : Polynomial.eval T (stateNextFormulaPolynomial tm state) = nextStateFormulaScheduleSize (transitionCases tm).length k T (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextChildPolynomial_eval_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : Polynomial.eval T (headNextChildPolynomial tm tape) = movedHeadFormulaScheduleSize (transitionCases tm).length k T (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial_eval_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : Polynomial.eval T (headNextFormulaPolynomial tm tape) = nextHeadFormulaScheduleSize (transitionCases tm).length k T (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextChildPolynomial_eval_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : Polynomial.eval T (writtenNextChildPolynomial tm tape symbol) = writtenCellScheduleSize (transitionCases tm).length k T (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextFormulaPolynomial_eval_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : Polynomial.eval T (writtenNextFormulaPolynomial tm tape symbol) = nextWrittenCellFormulaScheduleSize (transitionCases tm).length k T (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextFormulaPolynomial_eval_pos_internal {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : 0 < Polynomial.eval T (stateNextFormulaPolynomial tm state)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial_eval_pos_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : 0 < Polynomial.eval T (headNextFormulaPolynomial tm tape)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextFormulaPolynomial_eval_pos_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : 0 < Polynomial.eval T (writtenNextFormulaPolynomial tm tape symbol)