OAI/Combinatorics/UniformKServer/HiddenHistory.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal optimal labeled histories yield the public-prefix hidden law used in the finite-law construction. After a word ends its chosen label stays put; no future request is supplied to the online process.

  1. def OAI.UniformKServer.HiddenHistory.next line 18
  2. def OAI.UniformKServer.HiddenHistory.location line 21
  3. theorem OAI.UniformKServer.HiddenHistory.finish_append line 25
  4. theorem OAI.UniformKServer.HiddenHistory.update line 31
  5. def OAI.UniformKServer.HiddenHistory.trace line 43
  6. theorem OAI.UniformKServer.HiddenHistory.trace_snoc line 46
  7. theorem OAI.UniformKServer.HiddenHistory.trace_length line 50
  8. theorem OAI.UniformKServer.HiddenHistory.trace_take line 53
  9. theorem OAI.UniformKServer.HiddenHistory.trace_full line 62
  10. theorem OAI.UniformKServer.HiddenHistory.trace_prefix line 66
  11. def OAI.UniformKServer.HiddenHistory.data line 80
  12. theorem OAI.UniformKServer.HiddenHistory.is_public line 102
  13. theorem OAI.UniformKServer.HiddenHistory.paid_step line 107
  14. theorem OAI.UniformKServer.HiddenHistory.paid_sum line 118