SoI accounting for conditional-complexity difference estimators -- internals #
theorem
Complexity.GapMINCKT.DifferenceEstimator.SatisfiesSoIInputs.satisfiesAccounting_internal
{ordinaryTapes conditionalTapes : ℕ}
{components : DifferenceEstimator}
{schedule : SoIAccountingSchedule}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{parameters : Parameters}
{soiClock soiLoss : ℕ → ℕ}
(hinputs : components.SatisfiesSoIInputs schedule ordinaryMachine conditionalMachine parameters soiClock soiLoss)
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss)
(hwidening : parameters.IsWidening)
:
components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters