OAI/Analysis/MatrixSigning/Arithmetic/RationalSignAction.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W16.RationalSignAction.signedRational line 10
  2. def OAI.KS.W16.RationalSignAction.extend line 12
  3. def OAI.KS.W16.RationalSignAction.corePorts line 15
  4. def OAI.KS.W16.RationalSignAction.inputState line 16
  5. def OAI.KS.W16.RationalSignAction.operandState line 18
  6. def OAI.KS.W16.RationalSignAction.poppedState line 20
  7. def OAI.KS.W16.RationalSignAction.outputState line 22
  8. def OAI.KS.W16.RationalSignAction.chooseSign line 25
  9. def OAI.KS.W16.RationalSignAction.headSign line 28
  10. def OAI.KS.W16.RationalSignAction.toggleDispatch line 32
  11. def OAI.KS.W16.RationalSignAction.toggleMachine line 38
  12. def OAI.KS.W16.RationalSignAction.toggleProgram line 39
  13. theorem OAI.KS.W16.RationalSignAction.toggle_step_start line 41
  14. theorem OAI.KS.W16.RationalSignAction.toggle_step_finish line 58
  15. theorem OAI.KS.W16.RationalSignAction.toggle_spec line 68
  16. theorem OAI.KS.W16.RationalSignAction.encoded_nat_eq_nil line 85
  17. theorem OAI.KS.W16.RationalSignAction.chooseSign_integer line 93
  18. theorem OAI.KS.W16.RationalSignAction.signedRational_num_abs line 106
  19. theorem OAI.KS.W16.RationalSignAction.signedRational_den line 109
  20. theorem OAI.KS.W16.RationalSignAction.chooseSign_rational line 112
  21. def OAI.KS.W16.RationalSignAction.parseProgram line 118
  22. def OAI.KS.W16.RationalSignAction.serializeProgram line 120
  23. def OAI.KS.W16.RationalSignAction.program line 122
  24. def OAI.KS.W16.RationalSignAction.machine line 123
  25. theorem OAI.KS.W16.RationalSignAction.extend_on line 125
  26. theorem OAI.KS.W16.RationalSignAction.extend_off line 130
  27. theorem OAI.KS.W16.RationalSignAction.liftCore_spec line 137
  28. theorem OAI.KS.W16.RationalSignAction.parse_spec line 146
  29. theorem OAI.KS.W16.RationalSignAction.serialize_spec line 154
  30. def OAI.KS.W16.RationalSignAction.ticks line 164
  31. theorem OAI.KS.W16.RationalSignAction.full_spec line 167
  32. theorem OAI.KS.W16.RationalSignAction.ticks_linear line 177
  33. theorem OAI.KS.W16.RationalSignAction.linear_spec line 190
  34. theorem OAI.KS.W16.RationalSignAction.negation_spec line 196