OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PrefixListPrograms.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Actual conversion of the source's counted prefix list to quoted machine list registers. Each field is parsed by its literal splitter; the loop count and all temporary word lengths are bounded by the input.

  1. abbrev OAI.ContinuumCoulomb.PrefixListPrograms.State line 14
  2. def OAI.ContinuumCoulomb.PrefixListPrograms.stateView line 16
  3. def OAI.ContinuumCoulomb.PrefixListPrograms.stateCode line 19
  4. def OAI.ContinuumCoulomb.PrefixListPrograms.step line 22
  5. theorem OAI.ContinuumCoulomb.PrefixListPrograms.step_iterate line 27
  6. theorem OAI.ContinuumCoulomb.PrefixListPrograms.flat_length line 37
  7. theorem OAI.ContinuumCoulomb.PrefixListPrograms.quoted_length line 46
  8. theorem OAI.ContinuumCoulomb.PrefixListPrograms.stateCode_length line 54
  9. theorem OAI.ContinuumCoulomb.PrefixListPrograms.state_growth line 60
  10. def OAI.ContinuumCoulomb.PrefixListPrograms.listOutput line 77
  11. def OAI.ContinuumCoulomb.PrefixListPrograms.countProgram line 89
  12. def OAI.ContinuumCoulomb.PrefixListPrograms.streamProgram line 92
  13. def OAI.ContinuumCoulomb.PrefixListPrograms.accProgram line 97
  14. abbrev OAI.ContinuumCoulomb.PrefixListPrograms.NonemptyState line 101
  15. def OAI.ContinuumCoulomb.PrefixListPrograms.headerProgram line 103
  16. def OAI.ContinuumCoulomb.PrefixListPrograms.nonemptyStep line 117
  17. def OAI.ContinuumCoulomb.PrefixListPrograms.stepProgram line 137
  18. def OAI.ContinuumCoulomb.PrefixListPrograms.iterationProgram line 148
  19. def OAI.ContinuumCoulomb.PrefixListPrograms.inputCount line 157
  20. def OAI.ContinuumCoulomb.PrefixListPrograms.inputStream line 166
  21. def OAI.ContinuumCoulomb.PrefixListPrograms.startProgram line 175
  22. theorem OAI.ContinuumCoulomb.PrefixListPrograms.input_length line 181
  23. def OAI.ContinuumCoulomb.PrefixListPrograms.parseProgram line 188
  24. def OAI.ContinuumCoulomb.PrefixListPrograms.parsedList line 200
  25. def OAI.ContinuumCoulomb.PrefixListPrograms.parsedTail line 205
  26. def OAI.ContinuumCoulomb.PrefixListPrograms.listSplitter line 209
  27. def OAI.ContinuumCoulomb.PrefixListPrograms.listInput line 214

    Source documentation

    Actual quoted-list conversion for a complete source field, with no postulated record-decoding primitive.

    noncomputable def listInput (hc : ∀ a, 0 < (c.encode a).length) :
    Procedure (BinaryEncoding.list c).encode (listCode c.encode) id :=
…

    Mentions: OAI.ContinuumCoulomb.BinaryEncoding.list