OAI/Analysis/MatrixSigning/Machines/LittleEndianCompare.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W28.LittleEndianCompare.encode line 11
  2. def OAI.KS.W28.LittleEndianCompare.decode line 16
  3. theorem OAI.KS.W28.LittleEndianCompare.decode_encode line 19
  4. def OAI.KS.W28.LittleEndianCompare.merge line 22
  5. def OAI.KS.W28.LittleEndianCompare.update line 27
  6. def OAI.KS.W28.LittleEndianCompare.result line 28
  7. def OAI.KS.W28.LittleEndianCompare.dispatch line 30
  8. def OAI.KS.W28.LittleEndianCompare.machine line 36
  9. def OAI.KS.W28.LittleEndianCompare.cfg line 38
  10. theorem OAI.KS.W28.LittleEndianCompare.table_length line 41
  11. theorem OAI.KS.W28.LittleEndianCompare.table_lookup line 44
  12. theorem OAI.KS.W28.LittleEndianCompare.step_left line 60
  13. theorem OAI.KS.W28.LittleEndianCompare.step_right line 78
  14. theorem OAI.KS.W28.LittleEndianCompare.step_done line 89
  15. def OAI.KS.W28.LittleEndianCompare.scan line 100
  16. theorem OAI.KS.W28.LittleEndianCompare.scan_eq line 108
  17. theorem OAI.KS.W28.LittleEndianCompare.run_scan line 129
  18. theorem OAI.KS.W28.LittleEndianCompare.result_correct line 182
  19. theorem OAI.KS.W28.LittleEndianCompare.run_correct line 197
  20. theorem OAI.KS.W28.LittleEndianCompare.haltsFromWithin line 203