OAI/Analysis/MatrixSigning/Arithmetic/RationalMagnitudeMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W30.RationalMagnitudeMachine.corePorts line 13
  2. def OAI.KS.W30.RationalMagnitudeMachine.numeratorCopyPorts line 15
  3. def OAI.KS.W30.RationalMagnitudeMachine.denominatorCopyPorts line 16
  4. def OAI.KS.W30.RationalMagnitudeMachine.numeratorTrimPorts line 17
  5. def OAI.KS.W30.RationalMagnitudeMachine.denominatorTrimPorts line 18
  6. def OAI.KS.W30.RationalMagnitudeMachine.copyNumerator line 20
  7. def OAI.KS.W30.RationalMagnitudeMachine.reverseNumeratorCopy line 21
  8. def OAI.KS.W30.RationalMagnitudeMachine.copyDenominator line 22
  9. def OAI.KS.W30.RationalMagnitudeMachine.gcd line 23
  10. def OAI.KS.W30.RationalMagnitudeMachine.reverseGCD line 24
  11. def OAI.KS.W30.RationalMagnitudeMachine.placeGCD line 25
  12. def OAI.KS.W30.RationalMagnitudeMachine.takeNumerator line 26
  13. def OAI.KS.W30.RationalMagnitudeMachine.takeDenominator line 27
  14. def OAI.KS.W30.RationalMagnitudeMachine.divide line 28
  15. def OAI.KS.W30.RationalMagnitudeMachine.reverseQuotient line 29
  16. def OAI.KS.W30.RationalMagnitudeMachine.trimNumerator line 30
  17. def OAI.KS.W30.RationalMagnitudeMachine.trimDenominator line 31
  18. def OAI.KS.W30.RationalMagnitudeMachine.clearRemainder line 32
  19. def OAI.KS.W30.RationalMagnitudeMachine.clearGCD line 33
  20. def OAI.KS.W30.RationalMagnitudeMachine.signDispatch line 35
  21. def OAI.KS.W30.RationalMagnitudeMachine.normalizeSign line 41
  22. def OAI.KS.W30.RationalMagnitudeMachine.oneDispatch line 43
  23. def OAI.KS.W30.RationalMagnitudeMachine.insertOne line 45
  24. def OAI.KS.W30.RationalMagnitudeMachine.zeroBranch line 46
  25. def OAI.KS.W30.RationalMagnitudeMachine.prepare line 49
  26. def OAI.KS.W30.RationalMagnitudeMachine.computeGCD line 50
  27. def OAI.KS.W30.RationalMagnitudeMachine.reduceNumerator line 51
  28. def OAI.KS.W30.RationalMagnitudeMachine.reduceDenominator line 53
  29. def OAI.KS.W30.RationalMagnitudeMachine.positiveBranch line 55
  30. def OAI.KS.W30.RationalMagnitudeMachine.selector line 58
  31. def OAI.KS.W30.RationalMagnitudeMachine.program line 60
  32. def OAI.KS.W30.RationalMagnitudeMachine.«stacks» line 62
  33. def OAI.KS.W30.RationalMagnitudeMachine.state line 65
  34. theorem OAI.KS.W30.RationalMagnitudeMachine.branch_table_length line 68
  35. theorem OAI.KS.W30.RationalMagnitudeMachine.program_table_length line 75