OAI/Computability/WeisfeilerLeman/TapeCompiler.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.StackMachine.Machine.inputStacks line 9
  2. def OAI.WLTime.StackMachine.Machine.rawTape line 10
  3. def OAI.WLTime.StackMachine.Machine.mixed line 11
  4. theorem OAI.WLTime.StackMachine.Machine.rawTape_nil line 14
  5. theorem OAI.WLTime.StackMachine.Machine.rawTape_bit line 16
  6. theorem OAI.WLTime.StackMachine.Machine.rawTape_beyond line 20
  7. theorem OAI.WLTime.StackMachine.Machine.mixed_nonneg line 24
  8. theorem OAI.WLTime.StackMachine.Machine.mixed_neg line 26
  9. theorem OAI.WLTime.StackMachine.Machine.mixed_bottom line 28
  10. theorem OAI.WLTime.StackMachine.Machine.inputStacks_zero line 36
  11. theorem OAI.WLTime.StackMachine.Machine.inputStacks_cons line 39
  12. theorem OAI.WLTime.StackMachine.Machine.storage_nonneg line 47
  13. theorem OAI.WLTime.StackMachine.Machine.mixed_nil line 52
  14. theorem OAI.WLTime.StackMachine.Machine.rawTape_erase line 57
  15. theorem OAI.WLTime.StackMachine.Machine.mixed_erase line 71
  16. theorem OAI.WLTime.StackMachine.Machine.mixed_push line 81
  17. theorem OAI.WLTime.StackMachine.Machine.seekEnd_run line 98
  18. theorem OAI.WLTime.StackMachine.Machine.reverse_path line 110
  19. theorem OAI.WLTime.StackMachine.Machine.mixed_return line 126
  20. theorem OAI.WLTime.StackMachine.Machine.append_run line 142
  21. theorem OAI.WLTime.StackMachine.Machine.seekEnd_finish line 160
  22. theorem OAI.WLTime.StackMachine.Machine.take_run line 174
  23. theorem OAI.WLTime.StackMachine.Machine.bring_run line 188
  24. theorem OAI.WLTime.StackMachine.Machine.append_finish line 208
  25. theorem OAI.WLTime.StackMachine.Machine.back_run line 234
  26. theorem OAI.WLTime.StackMachine.Machine.init_cycle line 251
  27. theorem OAI.WLTime.StackMachine.Machine.init_empty line 265
  28. theorem OAI.WLTime.StackMachine.Machine.init_process line 279
  29. theorem OAI.WLTime.StackMachine.Machine.storage_empty line 302
  30. theorem OAI.WLTime.StackMachine.Machine.mixed_initial line 315
  31. theorem OAI.WLTime.StackMachine.Machine.init_mark line 327
  32. theorem OAI.WLTime.StackMachine.Machine.sweep_initial line 342
  33. theorem OAI.WLTime.StackMachine.Machine.step_length line 348
  34. theorem OAI.WLTime.StackMachine.Machine.iterate_length line 371
  35. theorem OAI.WLTime.StackMachine.Machine.sweep_iterate line 379
  36. theorem OAI.WLTime.StackMachine.Machine.sweep_run line 391
  37. abbrev OAI.WLTime.StackMachine.Machine.oneTape line 405
  38. theorem OAI.WLTime.StackMachine.Machine.oneTape_simulate line 407
  39. theorem OAI.WLTime.StackMachine.Machine.oneTape_correct line 414