GapCVP proof, part 03, continuation 02

def GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput input = match GapCVP.BinaryEncoding.readLengthPrefixedWord input with | some (payload, snd) => true :: payload | none => [false]

@[simp]

theorem GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput_valid (payload suffix : List Bool) : payloadDecodeOutput (BinaryEncoding.lengthPrefixedWord payload ++ suffix) = true :: payload

@[simp]

theorem GapCVP.SourceTotalStructuralDecoder.readUnaryPrefix_missing (count : ℕ) : BinaryEncoding.readUnaryPrefix (List.replicate count true) = none

structure GapCVP.SourceTotalStructuralDecoder.MissingUnaryInput (input : List Bool) : Type

GapCVP reduction support.

• count : ℕ

  GapCVP reduction support.

• shape : input = List.replicate self.count true

structure GapCVP.SourceTotalStructuralDecoder.DelimitedUnaryInput (input : List Bool) : Type

GapCVP reduction support.

• count : ℕ

  GapCVP reduction support.

• tail : List Bool

  GapCVP reduction support.

• shape : input = List.replicate self.count true ++ false :: self.tail

def GapCVP.SourceTotalStructuralDecoder.unaryInputSplit (input : List Bool) : MissingUnaryInput input ⊕ DelimitedUnaryInput input

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceTotalStructuralDecoder.validInput_reconstruct (count : ℕ) (tail : List Bool) (hlen : count ≤ tail.length) : List.replicate count true ++ false :: tail = BinaryEncoding.lengthPrefixedWord (List.take count tail) ++ List.drop count tail

noncomputable def GapCVP.SourceTotalStructuralDecoder.payloadDecoderComputable : BitTM payloadDecodeOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFormulaStructuralDecoder.dropHeadComputable : BitTM List.tail

GapCVP reduction support.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.firstFieldContents (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input = (GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput input).tail

noncomputable def GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable : BitTM firstFieldContents

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.firstFieldContents_valid (payload suffix : List Bool) : firstFieldContents (BinaryEncoding.lengthPrefixedWord payload ++ suffix) = payload

@[reducible, inline]

abbrev GapCVP.SourceFormulaStructuralDecoder.suffixDecoderMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixConfiguration (phase : Fin 6) (input counter reversed output : List Bool) : suffixDecoderMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceFormulaStructuralDecoder.suffixConfiguration phase input counter reversed output = { l := some phase, var := none, stk := ![input, counter, reversed, output] }

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_true (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 (true :: input) counter reversed output) = some (suffixConfiguration 0 input (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_delimiter (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 (false :: input) counter reversed output) = some (suffixConfiguration 1 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_missing_delimiter (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 [] counter reversed output) = some (suffixConfiguration 5 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_copy_step (bit : Bool) (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 (bit :: input) (true :: counter) reversed output) = some (suffixConfiguration 1 input counter (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_insufficient (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 [] (true :: counter) reversed output) = some (suffixConfiguration 5 [] (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_counter_complete (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 input [] reversed output) = some (suffixConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_discard_step (bit : Bool) (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 2 input [] (bit :: reversed) output) = some (suffixConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_discard_complete (input output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 2 input [] [] output) = some (suffixConfiguration 3 input [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_collect_step (bit : Bool) (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 3 (bit :: input) [] reversed output) = some (suffixConfiguration 3 input [] (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_collect_complete (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 3 [] [] reversed output) = some (suffixConfiguration 4 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_restore_step (bit : Bool) (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 4 [] [] (bit :: reversed) output) = some (suffixConfiguration 4 [] [] reversed (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_restore_finish (output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 4 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_input (bit : Bool) (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 (bit :: input) counter reversed output) = some (suffixConfiguration 5 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_counter (bit : Bool) (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] (bit :: counter) reversed output) = some (suffixConfiguration 5 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_reversed (bit : Bool) (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] [] (bit :: reversed) output) = some (suffixConfiguration 5 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_finish (output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output)

Internal support shared across GapCVP continuation modules.