Encoded unconditional-estimator implementations -- proof internals

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.lengthLeFlag_mem_FP_internal {first second : List Bool → List Bool} (hfirst : first ∈ FP) (hsecond : second ∈ FP) : (fun (bits : List Bool) => lengthLeFlag (first bits) (second bits)) ∈ FP

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.decisionString_mem_FP_internal {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) : encodedPlan.decisionString encodedEstimator ∈ FP

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.decisionString_mem_firstBitOne_iff_internal {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) (bits : List Bool) : encodedPlan.decisionString encodedEstimator bits ∈ Language.firstBitOne ↔ bits ∈ estimatorLanguage (plan.components estimate).estimate

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.estimatorLanguage_mem_P_internal {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) : estimatorLanguage (plan.components estimate).estimate ∈ P