OAI/Analysis/MatrixSigning/Encoding/ReusableArrayLookup.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W04.ReusableArrayLookup.reoutput line 14
  2. theorem OAI.KS.W04.ReusableArrayLookup.step_reoutput line 17
  3. theorem OAI.KS.W04.ReusableArrayLookup.run_reoutput line 23
  4. theorem OAI.KS.W04.ReusableArrayLookup.run_halted_of_length_ge line 32
  5. theorem OAI.KS.W04.ReusableArrayLookup.run_compose_bounded line 41
  6. def OAI.KS.W04.ReusableArrayLookup.arrayStacks line 54
  7. theorem OAI.KS.W04.ReusableArrayLookup.config_ext line 58
  8. def OAI.KS.W04.ReusableArrayLookup.copyPorts line 64
  9. def OAI.KS.W04.ReusableArrayLookup.lookupPorts line 70
  10. def OAI.KS.W04.ReusableArrayLookup.copyProgram line 71
  11. def OAI.KS.W04.ReusableArrayLookup.lookupProgram line 72
  12. def OAI.KS.W04.ReusableArrayLookup.cleanupProgram line 73
  13. def OAI.KS.W04.ReusableArrayLookup.lookupAndCleanup line 74
  14. def OAI.KS.W04.ReusableArrayLookup.program line 76
  15. theorem OAI.KS.W04.ReusableArrayLookup.program_states line 78
  16. theorem OAI.KS.W04.ReusableArrayLookup.composed_table_length line 80
  17. theorem OAI.KS.W04.ReusableArrayLookup.program_table_length line 84
  18. theorem OAI.KS.W04.ReusableArrayLookup.program_input line 87
  19. theorem OAI.KS.W04.ReusableArrayLookup.program_output line 88
  20. theorem OAI.KS.W04.ReusableArrayLookup.arrayStacks_copy_update line 90
  21. theorem OAI.KS.W04.ReusableArrayLookup.run_copy line 96
  22. theorem OAI.KS.W04.ReusableArrayLookup.run_lookup line 110
  23. theorem OAI.KS.W04.ReusableArrayLookup.run_cleanup line 141
  24. theorem OAI.KS.W04.ReusableArrayLookup.suffix_length_le line 158
  25. theorem OAI.KS.W04.ReusableArrayLookup.run_program line 166
  26. theorem OAI.KS.W04.ReusableArrayLookup.linear_time line 197
  27. def OAI.KS.W04.ReusableArrayLookup.liftedProgram line 205
  28. theorem OAI.KS.W04.ReusableArrayLookup.run_program_ports line 207