OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationLoop.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.MultiplicationLoop.guard line 11
  2. def OAI.KS.W03.MultiplicationLoop.program line 20
  3. def OAI.KS.W03.MultiplicationLoop.cfg line 22
  4. def OAI.KS.W03.MultiplicationLoop.advance line 25
  5. theorem OAI.KS.W03.MultiplicationLoop.advance_length line 29
  6. theorem OAI.KS.W03.MultiplicationLoop.step_empty line 35
  7. theorem OAI.KS.W03.MultiplicationLoop.step_false line 46
  8. theorem OAI.KS.W03.MultiplicationLoop.step_true line 58
  9. theorem OAI.KS.W03.MultiplicationLoop.run_loop line 71
  10. theorem OAI.KS.W03.MultiplicationLoop.loop_spec line 106
  11. theorem OAI.KS.W03.MultiplicationLoop.run_product line 113
  12. theorem OAI.KS.W03.MultiplicationLoop.fixed_state_count line 124