OAI/Analysis/MatrixSigning/Arithmetic/FloorRationalMachine.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KS.W20.FloorRationalMachine.Registers line 12
  2. def OAI.KS.W20.FloorRationalMachine.state line 14
  3. def OAI.KS.W20.FloorRationalMachine.clearDivisor line 17
  4. def OAI.KS.W20.FloorRationalMachine.clearRemainder line 18
  5. def OAI.KS.W20.FloorRationalMachine.clearScratch line 20
  6. theorem OAI.KS.W20.FloorRationalMachine.clearScratch_spec line 22
  7. def OAI.KS.W20.FloorRationalMachine.appendDenominator line 40
  8. theorem OAI.KS.W20.FloorRationalMachine.appendDenominator_spec line 45
  9. def OAI.KS.W20.FloorRationalMachine.program line 69
  10. def OAI.KS.W20.FloorRationalMachine.machine line 70
  11. def OAI.KS.W20.FloorRationalMachine.ticks line 72
  12. theorem OAI.KS.W20.FloorRationalMachine.encodeRat_intCast line 77
  13. theorem OAI.KS.W20.FloorRationalMachine.full_spec line 81
  14. theorem OAI.KS.W20.FloorRationalMachine.onPorts_spec line 91
  15. theorem OAI.KS.W20.FloorRationalMachine.ticks_le_polynomial line 100
  16. theorem OAI.KS.W20.FloorRationalMachine.polynomial_spec line 117
  17. theorem OAI.KS.W20.FloorRationalMachine.init_eq line 122
  18. theorem OAI.KS.W20.FloorRationalMachine.output_floor_rational line 129
  19. theorem OAI.KS.W20.FloorRationalMachine.halts_polynomial line 139