OAI/Analysis/MatrixSigning/Machines/Sequential.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W29.Sequential.leftState line 11
  2. def OAI.KS.W29.Sequential.rightState line 14
  3. def OAI.KS.W29.Sequential.liftLeft line 17
  4. def OAI.KS.W29.Sequential.liftRight line 22
  5. def OAI.KS.W29.Sequential.leftInstruction line 25
  6. def OAI.KS.W29.Sequential.rightInstruction line 31
  7. def OAI.KS.W29.Sequential.fetch line 35
  8. def OAI.KS.W29.Sequential.dispatch line 39
  9. def OAI.KS.W29.Sequential.compose line 47
  10. theorem OAI.KS.W29.Sequential.dispatch_left line 50
  11. theorem OAI.KS.W29.Sequential.dispatch_right line 54
  12. theorem OAI.KS.W29.Sequential.step_left line 58
  13. theorem OAI.KS.W29.Sequential.step_right line 68
  14. theorem OAI.KS.W29.Sequential.step_liftRight line 78
  15. theorem OAI.KS.W29.Sequential.run_liftRight line 85
  16. def OAI.KS.W29.Sequential.ActiveFor line 95
  17. def OAI.KS.W29.Sequential.HaltsAfter line 99
  18. theorem OAI.KS.W29.Sequential.step_liftLeft line 102
  19. theorem OAI.KS.W29.Sequential.run_liftLeft line 110
  20. theorem OAI.KS.W29.Sequential.run_compose line 121
  21. theorem OAI.KS.W29.Sequential.exists_halting_prefix line 131
  22. theorem OAI.KS.W29.Sequential.compose_halts line 144
  23. def OAI.KS.W29.Sequential.HaltsFromWithin line 152
  24. theorem OAI.KS.W29.Sequential.haltsFromWithin_mono line 155
  25. theorem OAI.KS.W29.Sequential.compose_haltsFromWithin line 167
  26. theorem OAI.KS.W29.Sequential.polynomialFuel_add_le line 194
  27. theorem OAI.KS.W29.Sequential.compose_polynomial line 205