OAI/Analysis/MatrixSigning/Arithmetic/DivisionMachine.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.DivisionMachine.trialPorts line 18
  2. def OAI.KS.W19.DivisionMachine.divisorPorts line 19
  3. def OAI.KS.W19.DivisionMachine.subtractPorts line 20
  4. def OAI.KS.W19.DivisionMachine.trimPorts line 21
  5. def OAI.KS.W19.DivisionMachine.copyTrial line 23
  6. def OAI.KS.W19.DivisionMachine.copyDivisor line 24
  7. def OAI.KS.W19.DivisionMachine.subtract line 25
  8. def OAI.KS.W19.DivisionMachine.prepareTail line 26
  9. def OAI.KS.W19.DivisionMachine.prepare line 27
  10. def OAI.KS.W19.DivisionMachine.keepTrial line 29
  11. def OAI.KS.W19.DivisionMachine.trimCandidate line 30
  12. def OAI.KS.W19.DivisionMachine.useCandidate line 31
  13. def OAI.KS.W19.DivisionMachine.select line 33
  14. def OAI.KS.W19.DivisionMachine.choose line 38
  15. def OAI.KS.W19.DivisionMachine.body line 39
  16. def OAI.KS.W19.DivisionMachine.guard line 41
  17. def OAI.KS.W19.DivisionMachine.loop line 46
  18. def OAI.KS.W19.DivisionMachine.«stacks» line 48
  19. theorem OAI.KS.W19.DivisionMachine.copyTrial_run line 51
  20. theorem OAI.KS.W19.DivisionMachine.copyTrial_halts line 63
  21. theorem OAI.KS.W19.DivisionMachine.copyDivisor_run line 67
  22. theorem OAI.KS.W19.DivisionMachine.copyDivisor_halts line 79
  23. theorem OAI.KS.W19.DivisionMachine.subtract_start line 83
  24. theorem OAI.KS.W19.DivisionMachine.subtract_run line 92
  25. theorem OAI.KS.W19.DivisionMachine.prepare_run line 105
  26. theorem OAI.KS.W19.DivisionMachine.choose_step_borrowed line 121
  27. theorem OAI.KS.W19.DivisionMachine.choose_step_candidate line 133
  28. theorem OAI.KS.W19.DivisionMachine.keepTrial_run line 145
  29. theorem OAI.KS.W19.DivisionMachine.clearRemainder_run line 158
  30. theorem OAI.KS.W19.DivisionMachine.trim_start line 172
  31. theorem OAI.KS.W19.DivisionMachine.trim_run line 181
  32. theorem OAI.KS.W19.DivisionMachine.useCandidate_run line 195
  33. theorem OAI.KS.W19.DivisionMachine.choose_run_borrowed line 208
  34. theorem OAI.KS.W19.DivisionMachine.choose_run_candidate line 217
  35. theorem OAI.KS.W19.DivisionMachine.subtract_halts line 228
  36. theorem OAI.KS.W19.DivisionMachine.prepare_halts line 235
  37. theorem OAI.KS.W19.DivisionMachine.body_run_borrowed line 248
  38. theorem OAI.KS.W19.DivisionMachine.body_run_candidate line 263