OAI/Analysis/MatrixSigning/Arithmetic/RationalSubtractProgram.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W13.RationalSubtract.firstPorts line 11
  2. def OAI.KS.W13.RationalSubtract.extend line 14
  3. theorem OAI.KS.W13.RationalSubtract.first_spec line 17
  4. def OAI.KS.W13.RationalSubtract.registers line 33
  5. def OAI.KS.W13.RationalSubtract.inputState line 36
  6. def OAI.KS.W13.RationalSubtract.outputState line 37
  7. def OAI.KS.W13.RationalSubtract.parseProgram line 39
  8. def OAI.KS.W13.RationalSubtract.serializeProgram line 41
  9. def OAI.KS.W13.RationalSubtract.negateProgram line 43
  10. def OAI.KS.W13.RationalSubtract.addProgram line 45
  11. def OAI.KS.W13.RationalSubtract.parsed line 48
  12. def OAI.KS.W13.RationalSubtract.saved line 50
  13. def OAI.KS.W13.RationalSubtract.emitted line 52
  14. def OAI.KS.W13.RationalSubtract.paired line 53
  15. def OAI.KS.W13.RationalSubtract.prepared line 54
  16. def OAI.KS.W13.RationalSubtract.marked line 55
  17. def OAI.KS.W13.RationalSubtract.negated line 56
  18. def OAI.KS.W13.RationalSubtract.cleared line 57
  19. def OAI.KS.W13.RationalSubtract.withRight line 58
  20. theorem OAI.KS.W13.RationalSubtract.parse_spec line 60
  21. theorem OAI.KS.W13.RationalSubtract.saveR_spec line 67
  22. def OAI.KS.W13.RationalSubtract.serializeTicks line 73
  23. theorem OAI.KS.W13.RationalSubtract.serialize_spec line 76
  24. theorem OAI.KS.W13.RationalSubtract.saveQ_spec line 83
  25. theorem OAI.KS.W13.RationalSubtract.takeR_spec line 89
  26. def OAI.KS.W13.RationalSubtract.markDispatch line 95
  27. def OAI.KS.W13.RationalSubtract.markProgram line 97
  28. theorem OAI.KS.W13.RationalSubtract.mark_spec line 99
  29. theorem OAI.KS.W13.RationalSubtract.negate_spec line 115
  30. theorem OAI.KS.W13.RationalSubtract.clearMark_spec line 122
  31. theorem OAI.KS.W13.RationalSubtract.placeRight_spec line 127
  32. theorem OAI.KS.W13.RationalSubtract.prependLeft_spec line 133
  33. theorem OAI.KS.W13.RationalSubtract.addition_spec line 139
  34. def OAI.KS.W13.RationalSubtract.prepareProgram line 148
  35. def OAI.KS.W13.RationalSubtract.changeSignProgram line 151
  36. def OAI.KS.W13.RationalSubtract.program line 154
  37. def OAI.KS.W13.RationalSubtract.machine line 155
  38. def OAI.KS.W13.RationalSubtract.prepareTicks line 157
  39. def OAI.KS.W13.RationalSubtract.changeSignTicks line 159
  40. def OAI.KS.W13.RationalSubtract.totalTicks line 161
  41. theorem OAI.KS.W13.RationalSubtract.full_spec line 164