Documentation

LeanPool.GapCVP.Part04E

GapCVP proof, part 04, continuation 05 #

source
theorem GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold_eq_word (input : List Bool) (count : ℕ) (seed : List Bool) (hparse : parseUnaryBoundedFold input = some (count, seed)) :
input = unaryBoundedFoldWord count seed
source
noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldComputable {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) (hbounded : PolynomiallyBoundedFoldStates worker bound = true) :
BitTM (boundedRecordFoldOutput worker)

GapCVP reduction support.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (literal : Literal) :
    List Bool

    GapCVP reduction support.

    Equations
    Instances For
      source
      def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep (input : List Bool) :
      List Bool

      Internal support shared across GapCVP continuation modules.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep_descriptor (literal : Literal) (suffix : List Bool) :
        flatLiteralRecordStep (flatSignedLiteralDescriptor literal ++ suffix) = suffix ++ BinaryEncoding.encodeLiteral literal

        Internal support shared across GapCVP continuation modules.

        source
        def GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptorStream (literals : List Literal) :
        List Bool

        GapCVP reduction support.

        Equations
        Instances For
          source
          theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep_polynomiallyBoundedFoldStates :
          OutputBoundedDependentRecordFold.PolynomiallyBoundedFoldStates flatLiteralRecordStep Polynomial.X = true

          Internal support shared across GapCVP continuation modules.

          source
          structure GapCVP.CNFFlatStructuralRecordWorkerTM.FlatLiteralRecordState :
          Type

          Internal support shared across GapCVP continuation modules.

          • inspected : Option Bool

            The inspected literal bit, when present.

          • sign : Option Bool

            The literal sign bit, when present.

          Instances For
            source
            @[instance_reducible]
            instance GapCVP.CNFFlatStructuralRecordWorkerTM.instFintypeFlatLiteralRecordState :
            Fintype FlatLiteralRecordState
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPrefixStatement :
            Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

            Internal support shared across GapCVP continuation modules.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSignStatement :
              Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

              Internal support shared across GapCVP continuation modules.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPayloadStatement :
                Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                Internal support shared across GapCVP continuation modules.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordRestoreStatement :
                  Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                  Internal support shared across GapCVP continuation modules.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordMarkerStatement :
                    Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                    Internal support shared across GapCVP continuation modules.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixScanStatement :
                      Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                      Internal support shared across GapCVP continuation modules.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixRestoreStatement :
                        Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                        Internal support shared across GapCVP continuation modules.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordInvalidStatement :
                          Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

                          Internal support shared across GapCVP continuation modules.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[reducible, inline]
                            abbrev GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordWorker :
                            Turing.FinTM2

                            Internal support shared across GapCVP continuation modules.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordConfiguration (phase : Fin 8) (sign : Option Bool) (input count reversed markers suffix output : List Bool) :
                              actualFlatLiteralRecordWorker.Cfg

                              Internal support shared across GapCVP continuation modules.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordWorker_init (input : List Bool) :
                                Turing.initList actualFlatLiteralRecordWorker input = flatLiteralRecordConfiguration 0 none input [] [] [] [] []

                                Internal support shared across GapCVP continuation modules.

                                source
                                def GapCVP.CNFFlatStructuralRecordWorkerTM.tacticFlatLiteralRecordStepTac :
                                Lean.ParserDescr

                                Executes the flatLiteralRecordStepTac machine-step simplifier.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_true (sign : Option Bool) (input count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (true :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 0 sign input (true :: count) reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_false (sign : Option Bool) (input count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (false :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 1 sign input count reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_missing (sign : Option Bool) (count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign [] count reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] count reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_step (oldSign : Option Bool) (sign marker : Bool) (input count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 oldSign (sign :: input) (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 (some sign) input count reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_empty (sign : Option Bool) (input reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 sign input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_missing (sign : Option Bool) (marker : Bool) (count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 sign [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_step (sign : Option Bool) (bit marker : Bool) (input count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 sign (bit :: input) (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 sign input count (bit :: reversed) (true :: markers) suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_finish (sign : Bool) (input reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 (some sign) input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 3 (some sign) input [] reversed markers suffix (sign :: output))

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_missing (sign : Option Bool) (marker : Bool) (count reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 sign [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_restore_step (sign : Option Bool) (bit : Bool) (input reversed markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 3 sign input [] (bit :: reversed) markers suffix output) = some (flatLiteralRecordConfiguration 3 sign input [] reversed markers suffix (bit :: output))

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_restore_finish (sign : Option Bool) (input markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 3 sign input [] [] markers suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (false :: output))

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_marker_step (sign : Option Bool) (marker : Bool) (input markers suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 4 sign input [] [] (marker :: markers) suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (true :: output))

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_marker_finish (sign : Option Bool) (input suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 4 sign input [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_scan_step (sign : Option Bool) (bit : Bool) (input suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 5 sign (bit :: input) [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] (bit :: suffix) output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_scan_finish (sign : Option Bool) (suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 5 sign [] [] [] [] suffix output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_restore_step (sign : Option Bool) (bit : Bool) (suffix output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 6 sign [] [] [] [] (bit :: suffix) output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix (bit :: output))

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_restore_finish (sign : Option Bool) (output : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 6 sign [] [] [] [] [] output) = some (Turing.haltList actualFlatLiteralRecordWorker output)

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_count (sign : Option Bool) (bit : Bool) (input count reversed markers : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input (bit :: count) reversed markers [] []) = some (flatLiteralRecordConfiguration 7 sign input count reversed markers [] [])

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_reversed (sign : Option Bool) (bit : Bool) (input reversed markers : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input [] (bit :: reversed) markers [] []) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers [] [])

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_markers (sign : Option Bool) (bit : Bool) (input markers : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input [] [] (bit :: markers) [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] markers [] [])

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_input (sign : Option Bool) (bit : Bool) (input : List Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign (bit :: input) [] [] [] [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] [] [] [])

                                  Internal support shared across GapCVP continuation modules.

                                  source
                                  theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_finish (sign : Option Bool) :
                                  actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign [] [] [] [] [] []) = some (Turing.haltList actualFlatLiteralRecordWorker [])

                                  Internal support shared across GapCVP continuation modules.