OAI/Analysis/MatrixSigning/Machines/FixedLoop.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W29.FixedLoop.Choice line 12
  2. structure OAI.KS.W29.FixedLoop.GuardInstruction line 18
  3. def OAI.KS.W29.FixedLoop.guardState line 22
  4. def OAI.KS.W29.FixedLoop.bodyState line 24
  5. def OAI.KS.W29.FixedLoop.guardInstruction line 27
  6. def OAI.KS.W29.FixedLoop.bodyInstruction line 34
  7. def OAI.KS.W29.FixedLoop.dispatch line 40
  8. def OAI.KS.W29.FixedLoop.loop line 47
  9. theorem OAI.KS.W29.FixedLoop.loop_states line 51
  10. theorem OAI.KS.W29.FixedLoop.loop_input line 54
  11. theorem OAI.KS.W29.FixedLoop.loop_output line 57
  12. theorem OAI.KS.W29.FixedLoop.loop_table_length line 60
  13. theorem OAI.KS.W29.FixedLoop.loop_initial line 66
  14. theorem OAI.KS.W29.FixedLoop.loop_toMachine line 69
  15. theorem OAI.KS.W29.FixedLoop.dispatch_guard line 74
  16. theorem OAI.KS.W29.FixedLoop.dispatch_body line 78
  17. def OAI.KS.W29.FixedLoop.liftBody line 82
  18. theorem OAI.KS.W29.FixedLoop.step_guard line 87
  19. theorem OAI.KS.W29.FixedLoop.step_body line 99
  20. theorem OAI.KS.W29.FixedLoop.step_liftBody line 110
  21. theorem OAI.KS.W29.FixedLoop.run_body line 119
  22. theorem OAI.KS.W29.FixedLoop.run_body_then line 132
  23. theorem OAI.KS.W29.FixedLoop.run_body_within line 144