OAI/Combinatorics/ParityLifts/Machines.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite-alphabet deterministic multitape model. A transition reads and writes only the currently scanned cell on each tape and moves each head by at most one cell.

  1. inductive OAI.ParityWL.Complexity.Move line 12
  2. instance OAI.ParityWL.Complexity.(instance at line 15) line 15
  3. def OAI.ParityWL.Complexity.Move.offset line 18
  4. structure OAI.ParityWL.Complexity.Machine line 25

    Source documentation

    Blank is 0, input bits are 1 and 2. Every work alphabet, state space and collection of tapes is finite. Tapes are two-way infinite.

    structure Machine where
…
  5. structure OAI.ParityWL.Complexity.Configuration line 35
  6. def OAI.ParityWL.Complexity.inputSymbol line 40
  7. def OAI.ParityWL.Complexity.initialConfiguration line 43
  8. def OAI.ParityWL.Complexity.step line 52
  9. def OAI.ParityWL.Complexity.run line 61
  10. def OAI.ParityWL.Complexity.Emits line 64
  11. structure OAI.ParityWL.Complexity.LocalMachine line 75

    Source documentation

    A finite-control presentation of the very same local multitape model. packed below changes ONLY the names of states, with zero simulation cost.

    structure LocalMachine (Q : Type) (t a : ℕ) where
…
  12. structure OAI.ParityWL.Complexity.LocalConfiguration line 81
  13. def OAI.ParityWL.Complexity.localInputSymbol line 86
  14. def OAI.ParityWL.Complexity.LocalMachine.initialConfiguration line 89
  15. def OAI.ParityWL.Complexity.LocalMachine.step line 99
  16. def OAI.ParityWL.Complexity.LocalMachine.run line 109
  17. def OAI.ParityWL.Complexity.LocalMachine.stateEquiv line 113
  18. def OAI.ParityWL.Complexity.LocalMachine.packed line 118
  19. def OAI.ParityWL.Complexity.LocalMachine.packConfiguration line 128
  20. lemma OAI.ParityWL.Complexity.LocalMachine.pack_initial line 134
  21. lemma OAI.ParityWL.Complexity.LocalMachine.pack_step line 139
  22. lemma OAI.ParityWL.Complexity.LocalMachine.pack_run line 146
  23. lemma OAI.ParityWL.Complexity.LocalMachine.packed_emits line 155