OAI/Computability/DeterministicSum/Machine.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite deterministic word-RAM states, exact costs and uniform decision specifications.

  1. def OAI.DeterministicThreeSum.ThreeSUM line 9
  2. def OAI.DeterministicThreeSum.InUniverse line 12
  3. def OAI.DeterministicThreeSum.wordWidth line 15
  4. def OAI.DeterministicThreeSum.wordModulus line 18
  5. inductive OAI.DeterministicThreeSum.Operand line 20
  6. inductive OAI.DeterministicThreeSum.BinOp line 25
  7. inductive OAI.DeterministicThreeSum.Test line 29
  8. inductive OAI.DeterministicThreeSum.Instruction line 33
  9. abbrev OAI.DeterministicThreeSum.Program line 43
  10. structure OAI.DeterministicThreeSum.State line 45
  11. def OAI.DeterministicThreeSum.readOperand line 51
  12. def OAI.DeterministicThreeSum.evalBinOp line 55
  13. def OAI.DeterministicThreeSum.evalTest line 69
  14. def OAI.DeterministicThreeSum.putRegister line 74
  15. def OAI.DeterministicThreeSum.step line 77
  16. def OAI.DeterministicThreeSum.encodeWord line 98
  17. def OAI.DeterministicThreeSum.initialState line 101
  18. def OAI.DeterministicThreeSum.run line 110
  19. def OAI.DeterministicThreeSum.registerBound line 114
  20. def OAI.DeterministicThreeSum.setupCost line 126
  21. def OAI.DeterministicThreeSum.ProgramDecidesWithin line 129
  22. def OAI.DeterministicThreeSum.deterministicSaving line 139
  23. def OAI.DeterministicThreeSum.DeterministicCubicStatement line 141
  24. def OAI.DeterministicThreeSum.PolynomialUniverseStatement line 145