Documentation

LeanPool.GapCVP.Part07G

GapCVP proof, part 07, continuation 07 #

source
def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentFixedFamilyStreamWord {α : Type} (indices : List α) (stream : α → List Bool → List Bool) (original : List Bool) :
List Bool

GapCVP reduction support.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAtLeastBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) :
    List Bool → List Bool

    GapCVP reduction support.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAtMostFixedPairWorker (grid : Polynomial ℕ) (alphabet first second : ℕ) :
      List Bool → List Bool

      GapCVP reduction support.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAtMostFixedPairBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (pair : CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm) × CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) :
        List Bool → List Bool

        GapCVP reduction support.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAtMostBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) :
          List Bool → List Bool

          GapCVP reduction support.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentInitialBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) :
            List Bool → List Bool

            GapCVP reduction support.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAcceptanceBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) :
              List Bool

              GapCVP reduction support.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentForbiddenFixedTupleWorker (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (symbols : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) :
                List Bool → List Bool

                GapCVP reduction support.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentForbiddenFixedTupleBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (symbols : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) :
                  List Bool → List Bool

                  GapCVP reduction support.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentForbiddenBundledStreamWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) :
                    List Bool → List Bool

                    GapCVP reduction support.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentActualBundledCatalogueWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) :
                      List Bool

                      GapCVP reduction support.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveFamilyIndependentActualBundledCatalogueComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) :
                        BitTM (fiveIndependentActualBundledCatalogueWord bound machine)

                        GapCVP reduction support.

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