OAI/Analysis/MatrixSigning/Machines/FixedSequential.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KS.W29.FixedSequential.Program line 10
  2. def OAI.KS.W29.FixedSequential.Program.toMachine line 17
  3. def OAI.KS.W29.FixedSequential.ofMachine line 20
  4. theorem OAI.KS.W29.FixedSequential.toMachine_ofMachine line 23
  5. theorem OAI.KS.W29.FixedSequential.ofMachine_toMachine line 27
  6. def OAI.KS.W29.FixedSequential.leftState line 31
  7. def OAI.KS.W29.FixedSequential.rightState line 34
  8. def OAI.KS.W29.FixedSequential.liftLeft line 37
  9. def OAI.KS.W29.FixedSequential.liftRight line 43
  10. def OAI.KS.W29.FixedSequential.leftInstruction line 47
  11. def OAI.KS.W29.FixedSequential.rightInstruction line 53
  12. def OAI.KS.W29.FixedSequential.fetch line 57
  13. def OAI.KS.W29.FixedSequential.dispatch line 61
  14. def OAI.KS.W29.FixedSequential.compose line 69
  15. theorem OAI.KS.W29.FixedSequential.compose_toMachine line 72
  16. theorem OAI.KS.W29.FixedSequential.compose_input line 77
  17. theorem OAI.KS.W29.FixedSequential.compose_output line 78
  18. theorem OAI.KS.W29.FixedSequential.dispatch_left line 80
  19. theorem OAI.KS.W29.FixedSequential.dispatch_right line 85
  20. theorem OAI.KS.W29.FixedSequential.step_left line 90
  21. theorem OAI.KS.W29.FixedSequential.step_right line 101
  22. theorem OAI.KS.W29.FixedSequential.step_liftRight line 112
  23. theorem OAI.KS.W29.FixedSequential.run_liftRight line 120
  24. def OAI.KS.W29.FixedSequential.ActiveFor line 132
  25. theorem OAI.KS.W29.FixedSequential.activeFor_append line 136
  26. def OAI.KS.W29.FixedSequential.HaltsAfter line 145
  27. theorem OAI.KS.W29.FixedSequential.step_liftLeft line 148
  28. theorem OAI.KS.W29.FixedSequential.run_liftLeft line 157
  29. theorem OAI.KS.W29.FixedSequential.run_compose line 169
  30. theorem OAI.KS.W29.FixedSequential.activeFor_liftLeft line 180
  31. theorem OAI.KS.W29.FixedSequential.activeFor_liftRight line 190
  32. theorem OAI.KS.W29.FixedSequential.compose_haltsAfter line 207
  33. def OAI.KS.W29.FixedSequential.HaltsFromWithin line 226
  34. theorem OAI.KS.W29.FixedSequential.exists_halting_prefix line 230
  35. theorem OAI.KS.W29.FixedSequential.run_compose_within line 243
  36. theorem OAI.KS.W29.FixedSequential.haltsFromWithin_mono line 271
  37. theorem OAI.KS.W29.FixedSequential.compose_haltsFromWithin line 283
  38. theorem OAI.KS.W29.FixedSequential.polynomialFuel_add_le line 311
  39. theorem OAI.KS.W29.FixedSequential.compose_polynomial line 322