OAI/Analysis/PeriodicLattice/Compiler.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Compilation of finite machines into planar velocity data.

  1. def OAI.PeriodicLattice.CompilerPlanar.radix line 19
  2. theorem OAI.PeriodicLattice.CompilerPlanar.radix_ge_two line 21
  3. theorem OAI.PeriodicLattice.CompilerPlanar.states_le_radix line 22
  4. theorem OAI.PeriodicLattice.CompilerPlanar.symbols_le_radix line 24
  5. def OAI.PeriodicLattice.CompilerPlanar.loadingCode line 27
  6. def OAI.PeriodicLattice.CompilerPlanar.nextTable line 29
  7. def OAI.PeriodicLattice.CompilerPlanar.haltTable line 30
  8. def OAI.PeriodicLattice.CompilerPlanar.velocity line 32
  9. def OAI.PeriodicLattice.CompilerPlanar.path line 35
  10. theorem OAI.PeriodicLattice.CompilerPlanar.loadingCode_bound line 38
  11. theorem OAI.PeriodicLattice.CompilerPlanar.nextTable_bound line 42
  12. theorem OAI.PeriodicLattice.CompilerPlanar.nextTable_periodic line 46
  13. theorem OAI.PeriodicLattice.CompilerPlanar.haltTable_periodic line 50
  14. theorem OAI.PeriodicLattice.CompilerPlanar.velocity_contDiff line 54
  15. theorem OAI.PeriodicLattice.CompilerPlanar.velocity_start line 57
  16. theorem OAI.PeriodicLattice.CompilerPlanar.velocity_periodic line 59
  17. theorem OAI.PeriodicLattice.CompilerPlanar.path_contDiff line 66
  18. theorem OAI.PeriodicLattice.CompilerPlanar.path_start line 68
  19. theorem OAI.PeriodicLattice.CompilerPlanar.path_solves line 70
  20. theorem OAI.PeriodicLattice.CompilerPlanar.path_unique line 75
  21. theorem OAI.PeriodicLattice.CompilerPlanar.path_event_iff line 82