OAI/Analysis/MatrixSigning/Arithmetic/SingleRationalParser.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KS.W06.SingleRationalParser.magnitude_result_canonical line 12
  2. theorem OAI.KS.W06.SingleRationalParser.magnitude_constructor_eq line 33
  3. def OAI.KS.W06.SingleRationalParser.numeratorPorts line 43
  4. def OAI.KS.W06.SingleRationalParser.denominatorPorts line 44
  5. def OAI.KS.W06.SingleRationalParser.magnitudePorts line 45
  6. def OAI.KS.W06.SingleRationalParser.baseState line 47
  7. def OAI.KS.W06.SingleRationalParser.baseProgram line 50
  8. def OAI.KS.W06.SingleRationalParser.baseTicks line 54
  9. theorem OAI.KS.W06.SingleRationalParser.base_spec line 56
  10. theorem OAI.KS.W06.SingleRationalParser.singleBits_encodeRat line 90
  11. theorem OAI.KS.W06.SingleRationalParser.canonical_base_spec line 98
  12. theorem OAI.KS.W06.SingleRationalParser.canonical_ticks_le line 107
  13. def OAI.KS.W06.SingleRationalParser.onPorts line 116
  14. theorem OAI.KS.W06.SingleRationalParser.onPorts_spec line 119
  15. def OAI.KS.W06.SingleRationalParser.normalizerPorts line 130
  16. def OAI.KS.W06.SingleRationalParser.program line 131
  17. def OAI.KS.W06.SingleRationalParser.machine line 132
  18. def OAI.KS.W06.SingleRationalParser.state line 134
  19. def OAI.KS.W06.SingleRationalParser.inputState line 137
  20. def OAI.KS.W06.SingleRationalParser.canonicalState line 140
  21. theorem OAI.KS.W06.SingleRationalParser.canonical_spec line 144
  22. theorem OAI.KS.W06.SingleRationalParser.init_eq line 151
  23. theorem OAI.KS.W06.SingleRationalParser.run_input line 156
  24. theorem OAI.KS.W06.SingleRationalParser.halts_input line 163