OAI/Analysis/MatrixSigning/Arithmetic/DivisionInput.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.DivisionInput.firstPorts line 12
  2. def OAI.KS.W19.DivisionInput.secondPorts line 13
  3. def OAI.KS.W19.DivisionInput.parseFirst line 14
  4. def OAI.KS.W19.DivisionInput.parseSecond line 15
  5. def OAI.KS.W19.DivisionInput.reverseInput line 16
  6. def OAI.KS.W19.DivisionInput.loopStage line 18
  7. def OAI.KS.W19.DivisionInput.secondStage line 19
  8. def OAI.KS.W19.DivisionInput.program line 20
  9. def OAI.KS.W19.DivisionInput.machine line 21
  10. def OAI.KS.W19.DivisionInput.«stacks» line 23
  11. theorem OAI.KS.W19.DivisionInput.first_init line 26
  12. theorem OAI.KS.W19.DivisionInput.first_run line 35
  13. theorem OAI.KS.W19.DivisionInput.first_halts line 48
  14. theorem OAI.KS.W19.DivisionInput.second_start line 55
  15. theorem OAI.KS.W19.DivisionInput.second_run line 64
  16. theorem OAI.KS.W19.DivisionInput.second_halts line 77
  17. theorem OAI.KS.W19.DivisionInput.reverse_run line 84
  18. theorem OAI.KS.W19.DivisionInput.reverse_halts line 98
  19. theorem OAI.KS.W19.DivisionInput.run_input line 102
  20. def OAI.KS.W19.DivisionInput.inputFuel line 129
  21. theorem OAI.KS.W19.DivisionInput.run_input_tape line 133
  22. theorem OAI.KS.W19.DivisionInput.inputFuel_quadratic line 143
  23. theorem OAI.KS.W19.DivisionInput.run_input_polynomial line 148
  24. theorem OAI.KS.W19.DivisionInput.run_naturals line 160
  25. theorem OAI.KS.W19.DivisionInput.haltsWithin_polynomial line 174