OAI/Computability/WeisfeilerLeman/Interpreter.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.Universal.motionLeft line 10
  2. def OAI.WLTime.Universal.motion line 15
  3. def OAI.WLTime.Universal.shiftTape line 20
  4. def OAI.WLTime.Universal.movedDir line 25
  5. theorem OAI.WLTime.Universal.motionLeft_exec line 28
  6. theorem OAI.WLTime.Universal.motion_exec line 52
  7. def OAI.WLTime.Universal.haltFlag line 103
  8. def OAI.WLTime.Universal.flagTest line 105
  9. def OAI.WLTime.Universal.flagState line 111
  10. theorem OAI.WLTime.Universal.flagTest_exec line 114
  11. theorem OAI.WLTime.Universal.flagState_exec line 163
  12. def OAI.WLTime.Universal.zeroSymbol line 185
  13. def OAI.WLTime.Universal.store line 187
  14. theorem OAI.WLTime.Universal.map_head_val line 198
  15. theorem OAI.WLTime.Universal.map_head_zero line 201
  16. theorem OAI.WLTime.Universal.table_lookup line 205
  17. def OAI.WLTime.Universal.activeStep line 216
  18. def OAI.WLTime.Universal.step line 224
  19. def OAI.WLTime.Universal.stepBound line 226
  20. def OAI.WLTime.Universal.nextState line 230
  21. def OAI.WLTime.Universal.nextTape line 233
  22. theorem OAI.WLTime.Universal.activeStep_exec line 238
  23. theorem OAI.WLTime.Universal.step_exec line 316
  24. theorem OAI.WLTime.UnaryPrograms.countdown_lift line 337
  25. theorem OAI.WLTime.UnaryPrograms.repeat_lift line 359
  26. theorem OAI.WLTime.TypedStack.Program.repeat_lift line 384
  27. abbrev OAI.WLTime.Universal.Config line 406
  28. def OAI.WLTime.Universal.next line 408
  29. def OAI.WLTime.Universal.encode line 410
  30. def OAI.WLTime.Universal.steps line 412
  31. theorem OAI.WLTime.Universal.steps_exec line 416