OAI/Computability/WeisfeilerLeman/Programs.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLTime.TypedStack.Command line 9
  2. structure OAI.WLTime.TypedStack.Machine line 15
  3. structure OAI.WLTime.TypedStack.Config line 21
  4. def OAI.WLTime.TypedStack.Machine.perform line 28
  5. def OAI.WLTime.TypedStack.Machine.step line 33
  6. def OAI.WLTime.TypedStack.Machine.initialConfig line 36
  7. def OAI.WLTime.TypedStack.Machine.run line 38
  8. def OAI.WLTime.TypedStack.Machine.registerEquiv line 42
  9. theorem OAI.WLTime.TypedStack.Machine.register_input line 46
  10. def OAI.WLTime.TypedStack.Machine.decodeSymbol line 49
  11. def OAI.WLTime.TypedStack.Machine.encodeSymbol line 54
  12. theorem OAI.WLTime.TypedStack.Machine.decode_encode line 58
  13. def OAI.WLTime.TypedStack.Machine.encodeCommand line 61
  14. abbrev OAI.WLTime.TypedStack.Machine.compile line 68
  15. def OAI.WLTime.TypedStack.Machine.project line 78
  16. theorem OAI.WLTime.TypedStack.Machine.project_perform line 82
  17. theorem OAI.WLTime.TypedStack.Machine.project_step line 109
  18. theorem OAI.WLTime.TypedStack.Machine.project_initial line 118
  19. theorem OAI.WLTime.TypedStack.Machine.project_run line 133
  20. theorem OAI.WLTime.TypedStack.Machine.compile_halt line 140
  21. theorem OAI.WLTime.TypedStack.Machine.oneTape_correct line 147
  22. def OAI.WLTime.TypedStack.Command.rename line 160
  23. def OAI.WLTime.TypedStack.Command.redirect line 165
  24. abbrev OAI.WLTime.TypedStack.Stacks line 173
  25. abbrev OAI.WLTime.TypedStack.Tops line 174
  26. def OAI.WLTime.TypedStack.tops line 175
  27. inductive OAI.WLTime.TypedStack.Execution line 177
  28. theorem OAI.WLTime.TypedStack.Execution.iterate line 190
  29. theorem OAI.WLTime.TypedStack.Execution.rename line 213
  30. theorem OAI.WLTime.TypedStack.Execution.plug line 222
  31. inductive OAI.WLTime.TypedStack.Code line 237
  32. def OAI.WLTime.TypedStack.Code.State line 247
  33. instance OAI.WLTime.TypedStack.Code.stateFintype line 256
  34. def OAI.WLTime.TypedStack.Code.entry line 266
  35. def OAI.WLTime.TypedStack.Code.transition line 275
  36. def OAI.WLTime.TypedStack.Code.machine line 288
  37. inductive OAI.WLTime.TypedStack.Code.Exec line 291
  38. theorem OAI.WLTime.TypedStack.Code.exec_finite line 307
  39. theorem OAI.WLTime.TypedStack.Code.exec_iterate line 328
  40. def OAI.WLTime.TypedStack.Code.nonempty line 338
  41. def OAI.WLTime.TypedStack.Code.clear line 339
  42. def OAI.WLTime.TypedStack.Code.transfer line 340
  43. theorem OAI.WLTime.TypedStack.Code.clear_exec line 343
  44. theorem OAI.WLTime.TypedStack.Code.transfer_exec line 361
  45. def OAI.WLTime.TypedStack.Code.distribute line 400
  46. theorem OAI.WLTime.TypedStack.Code.distribute_exec line 404