OAI/Analysis/MatrixSigning/Arithmetic/RationalReciprocalMachine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W30.RationalReciprocal.program line 10
  2. def OAI.KS.W30.RationalReciprocal.machine line 11
  3. def OAI.KS.W30.RationalReciprocal.inputState line 13
  4. def OAI.KS.W30.RationalReciprocal.outputState line 16
  5. theorem OAI.KS.W30.RationalReciprocal.program_spec line 19
  6. theorem OAI.KS.W30.RationalReciprocal.init_eq line 33
  7. theorem OAI.KS.W30.RationalReciprocal.run_polynomial line 40
  8. theorem OAI.KS.W30.RationalReciprocal.haltsWithin_polynomial line 48
  9. theorem OAI.KS.W30.RationalReciprocal.output_polynomial line 56
  10. theorem OAI.KS.W30.RationalReciprocal.output_of_sufficient_length line 63
  11. theorem OAI.KS.W30.RationalReciprocal.uniform_rational_reciprocal line 71
  12. def OAI.KS.W30.RationalReciprocal.onPorts line 83
  13. theorem OAI.KS.W30.RationalReciprocal.onPorts_spec line 86