OAI/Analysis/MatrixSigning/Arithmetic/CleanRationalCompare.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W04.CleanRationalCompare.haltProgram line 12
  2. def OAI.KS.W04.CleanRationalCompare.clearState line 15
  3. def OAI.KS.W04.CleanRationalCompare.clearListProgram line 18
  4. def OAI.KS.W04.CleanRationalCompare.clearListState line 22
  5. def OAI.KS.W04.CleanRationalCompare.clearListTicks line 26
  6. theorem OAI.KS.W04.CleanRationalCompare.halt_spec line 30
  7. theorem OAI.KS.W04.CleanRationalCompare.clear_spec line 41
  8. theorem OAI.KS.W04.CleanRationalCompare.clearList_spec line 47
  9. theorem OAI.KS.W04.CleanRationalCompare.clearListState_apply line 54
  10. theorem OAI.KS.W04.CleanRationalCompare.clearListTicks_le line 62
  11. def OAI.KS.W04.CleanRationalCompare.scratchPorts line 76
  12. def OAI.KS.W04.CleanRationalCompare.cleanupProgram line 77
  13. def OAI.KS.W04.CleanRationalCompare.flagState line 79
  14. def OAI.KS.W04.CleanRationalCompare.canonicalFinal line 81
  15. def OAI.KS.W04.CleanRationalCompare.inputState line 87
  16. def OAI.KS.W04.CleanRationalCompare.comparisonTicks line 90
  17. theorem OAI.KS.W04.CleanRationalCompare.canonical_spec line 93
  18. theorem OAI.KS.W04.CleanRationalCompare.canonicalFinal_length line 109
  19. theorem OAI.KS.W04.CleanRationalCompare.clear_canonicalFinal line 121
  20. def OAI.KS.W04.CleanRationalCompare.cleanedComparator line 128
  21. def OAI.KS.W04.CleanRationalCompare.totalTicks line 130
  22. theorem OAI.KS.W04.CleanRationalCompare.cleaned_spec line 133
  23. theorem OAI.KS.W04.CleanRationalCompare.totalTicks_le_polynomial line 139
  24. theorem OAI.KS.W04.CleanRationalCompare.cleaned_polynomial_spec line 150
  25. theorem OAI.KS.W04.CleanRationalCompare.cleaned_output line 155