Documentation

LeanPool.GapCVP.Part03E

GapCVP proof, part 03, continuation 05 #

source
structure GapCVP.CNFEncodedClauseSort.DelimitedPairComparisonState :
Type

GapCVP reduction support.

Instances For
    source
    @[instance_reducible]
    noncomputable instance GapCVP.CNFEncodedClauseSort.instFintypeDelimitedPairComparisonState :
    Fintype DelimitedPairComparisonState
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def GapCVP.CNFEncodedClauseSort.delimitedComparePeekFirst (stack : Fin 10) (present absent : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState) :
    Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

    GapCVP reduction support.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def GapCVP.CNFEncodedClauseSort.delimitedComparePeekSecond (stack : Fin 10) (present absent : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState) :
      Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

      GapCVP reduction support.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def GapCVP.CNFEncodedClauseSort.delimitedComparePop (stack : Fin 10) (continuation : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState) :
        Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

        GapCVP reduction support.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def GapCVP.CNFEncodedClauseSort.delimitedComparePushFirst (stack : Fin 10) (continuation : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState) :
          Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

          GapCVP reduction support.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def GapCVP.CNFEncodedClauseSort.delimitedComparePushConstant (stack : Fin 10) (bit : Bool) (continuation : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState) :
            Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

            GapCVP reduction support.

            Equations
            Instances For
              source
              def GapCVP.CNFEncodedClauseSort.delimitedCompareGoto (phase : Fin 12) :
              Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

              GapCVP reduction support.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def GapCVP.CNFEncodedClauseSort.delimitedCompareSetOutcome (outcome : EncodedWordOrdering) (phase : Fin 12) :
                Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                GapCVP reduction support.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstPrefixStatement :
                  Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                  GapCVP reduction support.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def GapCVP.CNFEncodedClauseSort.delimitedCompareFirstPayloadStatement :
                    Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                    GapCVP reduction support.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def GapCVP.CNFEncodedClauseSort.delimitedCompareSecondPrefixStatement :
                      Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                      GapCVP reduction support.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def GapCVP.CNFEncodedClauseSort.delimitedCompareSecondPayloadStatement :
                        Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                        GapCVP reduction support.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def GapCVP.CNFEncodedClauseSort.delimitedCompareReverseFirstStatement :
                          Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                          GapCVP reduction support.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def GapCVP.CNFEncodedClauseSort.delimitedCompareReverseSecondStatement :
                            Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                            GapCVP reduction support.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def GapCVP.CNFEncodedClauseSort.delimitedCompareWordsStatement :
                              Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                              GapCVP reduction support.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def GapCVP.CNFEncodedClauseSort.delimitedCompareCleanupStatement :
                                Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                                GapCVP reduction support.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def GapCVP.CNFEncodedClauseSort.delimitedCompareTrailingStatement :
                                  Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                                  GapCVP reduction support.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    def GapCVP.CNFEncodedClauseSort.delimitedCompareOutcomeStatement :
                                    Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                                    GapCVP reduction support.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      def GapCVP.CNFEncodedClauseSort.delimitedCompareSourceStatement :
                                      Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                                      GapCVP reduction support.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        def GapCVP.CNFEncodedClauseSort.delimitedComparePrefixStatement :
                                        Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) DelimitedPairComparisonState

                                        GapCVP reduction support.

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

                                          GapCVP reduction support.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def GapCVP.CNFEncodedClauseSort.delimitedCompareConfiguration (phase : Fin 12) (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                            delimitedPairComparisonMachine.Cfg

                                            GapCVP reduction support.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              theorem GapCVP.CNFEncodedClauseSort.delimitedPairComparisonMachine_init (input : List Bool) :
                                              Turing.initList delimitedPairComparisonMachine input = delimitedCompareConfiguration 0 EncodedWordOrdering.invalid input [] [] [] [] [] [] [] [] []
                                              source
                                              def GapCVP.CNFEncodedClauseSort.tacticDelimitedCompareStepTac :
                                              Lean.ParserDescr

                                              Executes the delimitedCompareStepTac machine-step simplifier.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPrefix_true (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome (true :: input) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 0 outcome input (true :: firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (true :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPrefix_delimiter (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome (false :: input) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 1 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward (false :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPrefix_missing (outcome : EncodedWordOrdering) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 0 outcome [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPayload_step (outcome : EncodedWordOrdering) (bit marker : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 1 outcome (bit :: input) (marker :: firstCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 1 outcome input firstCounter (bit :: firstReversed) secondCounter secondReversed firstForward secondForward (bit :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPayload_finish (outcome : EncodedWordOrdering) (input firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 1 outcome input [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 2 outcome input [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_firstPayload_missing (outcome : EncodedWordOrdering) (marker : Bool) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 1 outcome [] (marker :: firstCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPrefix_true (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 2 outcome (true :: input) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 2 outcome input firstCounter firstReversed (true :: secondCounter) secondReversed firstForward secondForward (true :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPrefix_delimiter (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 2 outcome (false :: input) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 3 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward (false :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPrefix_missing (outcome : EncodedWordOrdering) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 2 outcome [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPayload_step (outcome : EncodedWordOrdering) (bit marker : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 3 outcome (bit :: input) firstCounter firstReversed (marker :: secondCounter) secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 3 outcome input firstCounter firstReversed secondCounter (bit :: secondReversed) firstForward secondForward (bit :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPayload_finish (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 3 outcome input firstCounter firstReversed [] secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 4 outcome input firstCounter firstReversed [] secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_secondPayload_missing (outcome : EncodedWordOrdering) (marker : Bool) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 3 outcome [] firstCounter firstReversed (marker :: secondCounter) secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.invalid [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_reverseFirst_step (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 4 outcome input firstCounter (bit :: firstReversed) secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 4 outcome input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_reverseFirst_finish (outcome : EncodedWordOrdering) (input firstCounter secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 4 outcome input firstCounter [] secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 5 outcome input firstCounter [] secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_reverseSecond_step (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 5 outcome input firstCounter firstReversed secondCounter (bit :: secondReversed) firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 5 outcome input firstCounter firstReversed secondCounter secondReversed firstForward (bit :: secondForward) source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_reverseSecond_finish (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 5 outcome input firstCounter firstReversed secondCounter [] firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter [] firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_equalBit (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) (bit :: secondForward) source sourcePrefix output) = some (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_lessBit (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (false :: firstForward) (true :: secondForward) source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.less input firstCounter firstReversed secondCounter secondReversed (false :: firstForward) (true :: secondForward) source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_greaterBit (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (true :: firstForward) (false :: secondForward) source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.greater input firstCounter firstReversed secondCounter secondReversed (true :: firstForward) (false :: secondForward) source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_firstEmpty (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] (bit :: secondForward) source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.less input firstCounter firstReversed secondCounter secondReversed [] (bit :: secondForward) source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_secondEmpty (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) [] source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.greater input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) [] source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_words_bothEmpty (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 7 EncodedWordOrdering.equal input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)

                                                Internal support shared across GapCVP continuation modules.

                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_firstCounter (outcome : EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input (bit :: firstCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_firstReversed (outcome : EncodedWordOrdering) (bit : Bool) (input firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] (bit :: firstReversed) secondCounter secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_secondCounter (outcome : EncodedWordOrdering) (bit : Bool) (input secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] [] (bit :: secondCounter) secondReversed firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input [] [] secondCounter secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_secondReversed (outcome : EncodedWordOrdering) (bit : Bool) (input secondReversed firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] [] [] (bit :: secondReversed) firstForward secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input [] [] [] secondReversed firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_firstForward (outcome : EncodedWordOrdering) (bit : Bool) (input firstForward secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] [] [] [] (bit :: firstForward) secondForward source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input [] [] [] [] firstForward secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_secondForward (outcome : EncodedWordOrdering) (bit : Bool) (input secondForward source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] [] [] [] [] (bit :: secondForward) source sourcePrefix output) = some (delimitedCompareConfiguration 7 outcome input [] [] [] [] [] secondForward source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_cleanup_finish (outcome : EncodedWordOrdering) (input source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 7 outcome input [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_trailing_step (outcome : EncodedWordOrdering) (bit : Bool) (input source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 8 outcome (bit :: input) [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] (bit :: source) (true :: sourcePrefix) output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_trailing_finish (outcome : EncodedWordOrdering) (source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 8 outcome [] [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 9 outcome [] [] [] [] [] [] [] source sourcePrefix output)
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_outcome_step (outcome : EncodedWordOrdering) (source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 9 outcome [] [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] source sourcePrefix (encodedWordOrderingWord outcome ++ output))
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_source_step (outcome : EncodedWordOrdering) (bit : Bool) (source sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] (bit :: source) sourcePrefix output) = some (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] source sourcePrefix (bit :: output))
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_source_finish (outcome : EncodedWordOrdering) (sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] [] sourcePrefix output) = some (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix (false :: output))
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_prefix_step (outcome : EncodedWordOrdering) (bit : Bool) (sourcePrefix output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] (bit :: sourcePrefix) output) = some (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix (true :: output))
                                                source
                                                theorem GapCVP.CNFEncodedClauseSort.delimitedCompare_prefix_finish (outcome : EncodedWordOrdering) (output : List Bool) :
                                                delimitedPairComparisonMachine.step (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] [] output) = some (Turing.haltList delimitedPairComparisonMachine output)