OAI/Computability/MeanPayoff/Registers.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MeanPayoff.RegisterBits.Act line 11
  2. structure OAI.MeanPayoff.RegisterBits.Program line 15
  3. structure OAI.MeanPayoff.RegisterBits.Config line 20
  4. def OAI.MeanPayoff.RegisterBits.step line 25
  5. def OAI.MeanPayoff.RegisterBits.encode line 34
  6. def OAI.MeanPayoff.RegisterBits.encodeAll line 38
  7. theorem OAI.MeanPayoff.RegisterBits.encode_length line 42
  8. theorem OAI.MeanPayoff.RegisterBits.encodeAll_append line 47
  9. theorem OAI.MeanPayoff.RegisterBits.encodeAll_length line 53
  10. inductive OAI.MeanPayoff.RegisterBits.Compile.Label line 61
  11. def OAI.MeanPayoff.RegisterBits.Compile.equiv line 76
  12. def OAI.MeanPayoff.RegisterBits.Compile.enc line 77
  13. theorem OAI.MeanPayoff.RegisterBits.Compile.decode line 78
  14. def OAI.MeanPayoff.RegisterBits.Compile.dispatch line 81
  15. def OAI.MeanPayoff.RegisterBits.Compile.program line 94
  16. def OAI.MeanPayoff.RegisterBits.Compile.cfg line 146
  17. theorem OAI.MeanPayoff.RegisterBits.Compile.advance_add line 150
  18. theorem OAI.MeanPayoff.RegisterBits.Compile.step_skip line 161
  19. theorem OAI.MeanPayoff.RegisterBits.Compile.step_seek_tag line 170
  20. theorem OAI.MeanPayoff.RegisterBits.Compile.step_seek_delim line 179
  21. theorem OAI.MeanPayoff.RegisterBits.Compile.seek_one line 188
  22. theorem OAI.MeanPayoff.RegisterBits.Compile.seek_prefix line 203
  23. theorem OAI.MeanPayoff.RegisterBits.Compile.step_restore_some line 222
  24. def OAI.MeanPayoff.RegisterBits.Compile.sourceCfg line 231
  25. theorem OAI.MeanPayoff.RegisterBits.Compile.step_restore_nil line 235
  26. theorem OAI.MeanPayoff.RegisterBits.Compile.restore_all line 244
  27. def OAI.MeanPayoff.RegisterBits.Compile.localOp line 259
  28. def OAI.MeanPayoff.RegisterBits.Compile.localDest line 262
  29. def OAI.MeanPayoff.RegisterBits.Compile.localEmit line 265
  30. theorem OAI.MeanPayoff.RegisterBits.Compile.local_update line 268