OAI/Computability/MeanPayoff/Instructions.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.RegisterBits.Compile.step_source line 10
  2. theorem OAI.MeanPayoff.RegisterBits.Compile.instruction line 19
  3. theorem OAI.MeanPayoff.RegisterBits.Config.ext line 48
  4. def OAI.MeanPayoff.RegisterBits.storeSize line 52
  5. def OAI.MeanPayoff.RegisterBits.advance line 54
  6. theorem OAI.MeanPayoff.RegisterBits.advance_front line 58
  7. def OAI.MeanPayoff.RegisterBits.Compile.embed line 68
  8. theorem OAI.MeanPayoff.RegisterBits.Compile.ofFn_split line 71
  9. theorem OAI.MeanPayoff.RegisterBits.Compile.ofFn_update line 78
  10. theorem OAI.MeanPayoff.RegisterBits.Compile.encode_split line 85
  11. theorem OAI.MeanPayoff.RegisterBits.Compile.encode_update line 91
  12. theorem OAI.MeanPayoff.RegisterBits.Compile.encoded_size line 97
  13. theorem OAI.MeanPayoff.RegisterBits.Compile.step_simulation line 101
  14. theorem OAI.MeanPayoff.RegisterBits.update_size line 143
  15. theorem OAI.MeanPayoff.RegisterBits.op_size line 156
  16. theorem OAI.MeanPayoff.RegisterBits.step_size line 160
  17. theorem OAI.MeanPayoff.RegisterBits.advance_size line 174
  18. theorem OAI.MeanPayoff.RegisterBits.Compile.step_simulation_all line 185
  19. def OAI.MeanPayoff.RegisterBits.Compile.clock line 198
  20. theorem OAI.MeanPayoff.RegisterBits.Compile.clock_pos line 201
  21. theorem OAI.MeanPayoff.RegisterBits.Compile.clock_bound line 204
  22. theorem OAI.MeanPayoff.RegisterBits.Compile.clock_simulation line 208
  23. def OAI.MeanPayoff.RegisterBits.initial line 216
  24. def OAI.MeanPayoff.RegisterBits.Compile.escape line 222
  25. theorem OAI.MeanPayoff.RegisterBits.Compile.escape_append line 226
  26. theorem OAI.MeanPayoff.RegisterBits.Compile.encode_escape line 231
  27. theorem OAI.MeanPayoff.RegisterBits.Compile.encodeAll_replicate_nil line 236
  28. theorem OAI.MeanPayoff.RegisterBits.Compile.encode_initial line 242
  29. theorem OAI.MeanPayoff.RegisterBits.Compile.init_move_step line 254
  30. theorem OAI.MeanPayoff.RegisterBits.Compile.init_move_all line 262
  31. theorem OAI.MeanPayoff.RegisterBits.Compile.init_move_empty line 271
  32. theorem OAI.MeanPayoff.RegisterBits.Compile.init_pad_zero line 279
  33. theorem OAI.MeanPayoff.RegisterBits.Compile.init_pad_succ line 287
  34. theorem OAI.MeanPayoff.RegisterBits.Compile.init_pad_all line 296
  35. theorem OAI.MeanPayoff.RegisterBits.Compile.init_restore_step line 307
  36. theorem OAI.MeanPayoff.RegisterBits.Compile.init_tag_step line 315
  37. theorem OAI.MeanPayoff.RegisterBits.Compile.init_restore_empty line 323
  38. theorem OAI.MeanPayoff.RegisterBits.Compile.init_restore_all line 331
  39. theorem OAI.MeanPayoff.RegisterBits.Compile.initial_cfg line 341
  40. theorem OAI.MeanPayoff.RegisterBits.Compile.initialize_correct line 348