OAI/Computability/MaxCut/Encoding/Encoding2.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

An occurrence-preserving E3LIN table codec. The word stream contains its declared variable count and equation count, followed by four words per equation. Parsing checks all three indices, the Boolean right-hand side, the exact count, absence of trailing words, and nonemptiness. Length theorems below concern the actual serialized output; they make no running-time claim.

  1. structure OAI.MaxCutGames.Reduction.SourceEncoding.Input line 16
  2. abbrev OAI.MaxCutGames.Reduction.SourceEncoding.Table line 21
  3. def OAI.MaxCutGames.Reduction.SourceEncoding.equationWords line 23
  4. def OAI.MaxCutGames.Reduction.SourceEncoding.inputWords line 26
  5. def OAI.MaxCutGames.Reduction.SourceEncoding.inputBits line 29
  6. def OAI.MaxCutGames.Reduction.SourceEncoding.parseEquation line 31
  7. theorem OAI.MaxCutGames.Reduction.SourceEncoding.parseEquation_encoded line 47
  8. def OAI.MaxCutGames.Reduction.SourceEncoding.parseEquations line 54
  9. theorem OAI.MaxCutGames.Reduction.SourceEncoding.parseEquations_encoded line 63

    Source documentation

    Parsing preserves the entire ordered list, including all equal entries.

    @[simp] theorem parseEquations_encoded {n : Nat}
    (equations : List (CloneGap.Equation (Fin n))) (rest : List Nat) :
    parseEquations n equations.length (equations.flatMap equationWords ++ rest) =
      some (equations, rest) := by
…

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.SourceEncoding.parseEquations, OAI.MaxCutGames.Reduction.SourceEncoding.equationWords

  10. def OAI.MaxCutGames.Reduction.SourceEncoding.decodeInputWords line 72
  11. theorem OAI.MaxCutGames.Reduction.SourceEncoding.decodeInputWords_encoded line 82
  12. def OAI.MaxCutGames.Reduction.SourceEncoding.decodeInputBits line 91
  13. theorem OAI.MaxCutGames.Reduction.SourceEncoding.decodeInputBits_encoded line 94
  14. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputWords_injective line 98
  15. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputBits_injective line 103
  16. theorem OAI.MaxCutGames.Reduction.SourceEncoding.equationWords_length line 108
  17. theorem OAI.MaxCutGames.Reduction.SourceEncoding.equationsWords_length line 111
  18. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputWords_length line 120
  19. theorem OAI.MaxCutGames.Reduction.SourceEncoding.equationBits_length_le line 125
  20. theorem OAI.MaxCutGames.Reduction.SourceEncoding.equationsBits_length_le line 132
  21. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputBits_length line 143
  22. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputBits_length_le line 150
  23. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputBits_length_ge_variables line 156
  24. theorem OAI.MaxCutGames.Reduction.SourceEncoding.inputBits_length_ge_equations line 159