OAI/Computability/WeisfeilerLeman/BoundedRun.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.TypedStack.Program.reverseInto line 10
  2. theorem OAI.WLTime.TypedStack.Program.reverseInto_exec line 12
  3. def OAI.WLTime.TypedStack.Program.shift line 17
  4. theorem OAI.WLTime.TypedStack.Program.shift_exec line 20
  5. def OAI.WLTime.Universal.shiftPair line 32
  6. theorem OAI.WLTime.Universal.shiftPair_prefix line 34
  7. def OAI.WLTime.Universal.takeDescription line 44
  8. theorem OAI.WLTime.Universal.takeDescription_exec line 47
  9. def OAI.WLTime.Universal.bitValue line 80
  10. theorem OAI.WLTime.Universal.fields_append line 82
  11. def OAI.WLTime.Universal.tapeBody line 85
  12. def OAI.WLTime.Universal.tapeLoop line 91
  13. theorem OAI.WLTime.Universal.tapeBody_exec line 93
  14. theorem OAI.WLTime.Universal.tapeLoop_exec line 122
  15. def OAI.WLTime.Universal.inputPrep line 146
  16. def OAI.WLTime.Universal.inputStore line 150
  17. def OAI.WLTime.Universal.prepared line 152
  18. theorem OAI.WLTime.Universal.inputPrep_exec line 158
  19. def OAI.WLTime.Universal.initialConfig line 181
  20. theorem OAI.WLTime.Universal.symbol_val line 184
  21. theorem OAI.WLTime.Universal.map_symbols_val line 187
  22. def OAI.WLTime.Universal.parseProgram line 191
  23. def OAI.WLTime.Universal.initProgram line 198
  24. theorem OAI.WLTime.Universal.parseProgram_exec line 200
  25. theorem OAI.WLTime.Universal.initProgram_exec line 239
  26. def OAI.WLTime.Universal.Relative line 257
  27. theorem OAI.WLTime.Universal.initial_relative line 260
  28. theorem OAI.WLTime.Universal.next_relative line 279
  29. theorem OAI.WLTime.Universal.iterate_relative line 303
  30. theorem OAI.WLTime.Universal.simulated_state line 311
  31. def OAI.WLTime.TypedStack.Program.inputStacks line 322
  32. abbrev OAI.WLTime.TypedStack.Program.FinalState line 324
  33. def OAI.WLTime.TypedStack.Program.finalTransition line 326
  34. def OAI.WLTime.TypedStack.Program.machine line 331
  35. theorem OAI.WLTime.TypedStack.Program.machine_initial line 338
  36. theorem OAI.WLTime.TypedStack.Program.machine_run line 347
  37. theorem OAI.WLTime.TypedStack.Program.oneTape_correct line 357
  38. def OAI.WLTime.Universal.boundedProgram line 372
  39. def OAI.WLTime.Universal.answer line 373
  40. def OAI.WLTime.Universal.machine line 375
  41. theorem OAI.WLTime.Universal.haltFlag_answer line 377
  42. theorem OAI.WLTime.Universal.boundedProgram_exec line 382
  43. def OAI.WLTime.Universal.timeBound line 393
  44. theorem OAI.WLTime.Universal.machine_correct line 397