OAI/Analysis/MatrixSigning/Arithmetic/RationalCompareProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W06.RationalCompare.leftMagnitudePorts line 12
  2. def OAI.KS.W06.RationalCompare.rightMagnitudePorts line 13
  3. def OAI.KS.W06.RationalCompare.leftProductPorts line 14
  4. def OAI.KS.W06.RationalCompare.rightProductPorts line 15
  5. def OAI.KS.W06.RationalCompare.resultPorts line 16
  6. def OAI.KS.W06.RationalCompare.workFields line 18
  7. def OAI.KS.W06.RationalCompare.magnitude line 21
  8. def OAI.KS.W06.RationalCompare.product line 22
  9. def OAI.KS.W06.RationalCompare.prepareProgram line 25
  10. theorem OAI.KS.W06.RationalCompare.prepare_spec line 29
  11. def OAI.KS.W06.RationalCompare.productsProgram line 50
  12. def OAI.KS.W06.RationalCompare.productsAfter line 54
  13. theorem OAI.KS.W06.RationalCompare.products_spec line 58
  14. def OAI.KS.W06.RationalCompare.program line 85
  15. def OAI.KS.W06.RationalCompare.machine line 88
  16. def OAI.KS.W06.RationalCompare.totalTicks line 90
  17. def OAI.KS.W06.RationalCompare.finalStacks line 97
  18. theorem OAI.KS.W06.RationalCompare.full_spec line 101
  19. theorem OAI.KS.W06.RationalCompare.final_output line 110
  20. theorem OAI.KS.W06.RationalCompare.machine_stackCount line 120
  21. theorem OAI.KS.W06.RationalCompare.machine_inputStack line 121
  22. theorem OAI.KS.W06.RationalCompare.machine_outputStack line 122
  23. theorem OAI.KS.W06.RationalCompare.init_eq line 124
  24. theorem OAI.KS.W06.RationalCompare.run_input line 130