OAI/Analysis/MatrixSigning/Machines/BisectionCommands.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W28.BisectionCommands.Call line 13
  2. def OAI.KS.W28.BisectionCommands.Call.program line 21
  3. def OAI.KS.W28.BisectionCommands.Call.eval line 29
  4. def OAI.KS.W28.BisectionCommands.Call.ready line 38
  5. def OAI.KS.W28.BisectionCommands.Call.ticks line 47
  6. theorem OAI.KS.W28.BisectionCommands.Call.spec line 55
  7. def OAI.KS.W28.BisectionCommands.skip line 65
  8. theorem OAI.KS.W28.BisectionCommands.skip_spec line 69
  9. def OAI.KS.W28.BisectionCommands.program line 83
  10. def OAI.KS.W28.BisectionCommands.eval line 87
  11. def OAI.KS.W28.BisectionCommands.ready line 91
  12. def OAI.KS.W28.BisectionCommands.ticks line 95
  13. theorem OAI.KS.W28.BisectionCommands.sequence_spec line 99