OAI/Computability/WeisfeilerLeman/Stacks.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLTime.StackMachine.Command line 9
  2. structure OAI.WLTime.StackMachine.Machine line 15
  3. structure OAI.WLTime.StackMachine.Machine.Config line 28
  4. def OAI.WLTime.StackMachine.Machine.inputLetter line 32
  5. def OAI.WLTime.StackMachine.Machine.initialConfig line 34
  6. def OAI.WLTime.StackMachine.Machine.perform line 38
  7. def OAI.WLTime.StackMachine.Machine.step line 44
  8. def OAI.WLTime.StackMachine.Machine.run line 48
  9. def OAI.WLTime.StackMachine.Machine.encodeLetter line 50
  10. def OAI.WLTime.StackMachine.Machine.decodeLetter line 54
  11. theorem OAI.WLTime.StackMachine.Machine.decode_encode line 57
  12. def OAI.WLTime.StackMachine.Machine.contents line 60
  13. theorem OAI.WLTime.StackMachine.Machine.contents_empty line 63
  14. theorem OAI.WLTime.StackMachine.Machine.contents_head line 66
  15. theorem OAI.WLTime.StackMachine.Machine.contents_push line 71
  16. theorem OAI.WLTime.StackMachine.Machine.contents_pop line 85
  17. abbrev OAI.WLTime.StackMachine.Machine.Micro line 99
  18. def OAI.WLTime.StackMachine.Machine.microEquiv line 101
  19. theorem OAI.WLTime.StackMachine.Machine.micro_left line 105
  20. theorem OAI.WLTime.StackMachine.Machine.micro_right_ge line 107
  21. def OAI.WLTime.StackMachine.Machine.microTransition line 112
  22. abbrev OAI.WLTime.StackMachine.Machine.compile line 122
  23. def OAI.WLTime.StackMachine.Machine.stateCode line 132
  24. def OAI.WLTime.StackMachine.Machine.embed line 136
  25. theorem OAI.WLTime.StackMachine.Machine.embed_halted line 141
  26. def OAI.WLTime.StackMachine.Machine.cost line 151
  27. def OAI.WLTime.StackMachine.Machine.moveHeads line 155
  28. theorem OAI.WLTime.StackMachine.Machine.write_same line 160
  29. theorem OAI.WLTime.StackMachine.Machine.write_one line 167
  30. theorem OAI.WLTime.StackMachine.Machine.step_micro line 180
  31. theorem OAI.WLTime.StackMachine.Machine.heads_one line 191
  32. theorem OAI.WLTime.StackMachine.Machine.tame_right line 199
  33. theorem OAI.WLTime.StackMachine.Machine.simulate_action line 204
  34. theorem OAI.WLTime.StackMachine.Machine.initial_tape line 255
  35. theorem OAI.WLTime.StackMachine.Machine.initial_step line 274
  36. theorem OAI.WLTime.StackMachine.Machine.simulate_step line 287
  37. theorem OAI.WLTime.StackMachine.Machine.simulate_iterate line 295
  38. theorem OAI.WLTime.StackMachine.Machine.simulate_run line 305
  39. theorem OAI.WLTime.StackMachine.Machine.compile_correct line 312
  40. abbrev OAI.WLTime.TypedTape.State line 329
  41. abbrev OAI.WLTime.TypedTape.Symbol line 330
  42. structure OAI.WLTime.TypedTape.Machine line 332
  43. structure OAI.WLTime.TypedTape.Config line 335
  44. def OAI.WLTime.TypedTape.Machine.halted line 343
  45. instance OAI.WLTime.TypedTape.Machine.(instance at line 345) line 345
  46. def OAI.WLTime.TypedTape.Machine.action line 350
  47. def OAI.WLTime.TypedTape.Machine.step line 353
  48. def OAI.WLTime.TypedTape.Machine.initial line 359
  49. def OAI.WLTime.TypedTape.Machine.run line 365
  50. theorem OAI.WLTime.TypedTape.Machine.step_live line 367
  51. theorem OAI.WLTime.TypedTape.Machine.step_keep line 373
  52. theorem OAI.WLTime.TypedTape.Machine.path_iterate line 381
  53. theorem OAI.WLTime.TypedTape.Machine.concat line 389
  54. def OAI.WLTime.TypedTape.Machine.stateEquiv line 395
  55. def OAI.WLTime.TypedTape.Machine.symbolEquiv line 398
  56. theorem OAI.WLTime.TypedTape.Machine.state_left line 402
  57. theorem OAI.WLTime.TypedTape.Machine.symbol_left line 404
  58. theorem OAI.WLTime.TypedTape.Machine.state_halted line 407
  59. abbrev OAI.WLTime.TypedTape.Machine.compile line 418
  60. def OAI.WLTime.TypedTape.Machine.embed line 426
  61. theorem OAI.WLTime.TypedTape.Machine.compile_action line 431
  62. theorem OAI.WLTime.TypedTape.Machine.embed_step line 437
  63. theorem OAI.WLTime.TypedTape.Machine.embed_initial line 445
  64. theorem OAI.WLTime.TypedTape.Machine.embed_run line 456