OAI/Computability/MeanPayoff/TreeCopy.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.RegisterBits.rename line 9
  2. def OAI.MeanPayoff.RegisterBits.install line 15
  3. theorem OAI.MeanPayoff.RegisterBits.install_at line 19
  4. theorem OAI.MeanPayoff.RegisterBits.install_off line 27
  5. theorem OAI.MeanPayoff.RegisterBits.install_update line 32
  6. def OAI.MeanPayoff.RegisterBits.renamed line 47
  7. theorem OAI.MeanPayoff.RegisterBits.rename_step line 51
  8. theorem OAI.MeanPayoff.RegisterBits.rename_advance line 63
  9. theorem OAI.MeanPayoff.RegisterBits.halted_step line 72
  10. theorem OAI.MeanPayoff.RegisterBits.advance_halted line 75
  11. theorem OAI.MeanPayoff.RegisterBits.first_termination line 81
  12. structure OAI.MeanPayoff.RegisterBits.Flow.Program line 96
  13. abbrev OAI.MeanPayoff.RegisterBits.Flow.Labels line 103
  14. def OAI.MeanPayoff.RegisterBits.Flow.equiv line 105
  15. def OAI.MeanPayoff.RegisterBits.Flow.inner line 107
  16. def OAI.MeanPayoff.RegisterBits.Flow.boundary line 109
  17. theorem OAI.MeanPayoff.RegisterBits.Flow.dec_inner line 110
  18. theorem OAI.MeanPayoff.RegisterBits.Flow.dec_boundary line 112
  19. def OAI.MeanPayoff.RegisterBits.Flow.compile line 115
  20. def OAI.MeanPayoff.RegisterBits.Flow.embed line 128
  21. def OAI.MeanPayoff.RegisterBits.Flow.state line 132
  22. def OAI.MeanPayoff.RegisterBits.Flow.edge line 136
  23. theorem OAI.MeanPayoff.RegisterBits.Flow.step_inner line 140
  24. theorem OAI.MeanPayoff.RegisterBits.Flow.advance_inner line 156
  25. theorem OAI.MeanPayoff.RegisterBits.Flow.macro_runs line 167
  26. theorem OAI.MeanPayoff.RegisterBits.Flow.step_boundary line 180
  27. inductive OAI.MeanPayoff.BinaryData.Copy.Label line 198
  28. def OAI.MeanPayoff.BinaryData.Copy.equiv line 202
  29. def OAI.MeanPayoff.BinaryData.Copy.enc line 203
  30. theorem OAI.MeanPayoff.BinaryData.Copy.dec line 204
  31. def OAI.MeanPayoff.BinaryData.Copy.program line 206
  32. def OAI.MeanPayoff.BinaryData.Copy.cfg line 224
  33. def OAI.MeanPayoff.BinaryData.Copy.stopped line 226
  34. theorem OAI.MeanPayoff.BinaryData.Copy.config_ext line 229
  35. theorem OAI.MeanPayoff.BinaryData.Copy.advance_front line 233
  36. theorem OAI.MeanPayoff.BinaryData.Copy.advance_add line 242
  37. theorem OAI.MeanPayoff.BinaryData.Copy.start_step line 251
  38. theorem OAI.MeanPayoff.BinaryData.Copy.check_step line 258
  39. theorem OAI.MeanPayoff.BinaryData.Copy.read_step line 265
  40. theorem OAI.MeanPayoff.BinaryData.Copy.put_step line 272
  41. theorem OAI.MeanPayoff.BinaryData.Copy.depth_false line 279
  42. theorem OAI.MeanPayoff.BinaryData.Copy.depth_true line 286
  43. theorem OAI.MeanPayoff.BinaryData.Copy.scan_nil line 293
  44. theorem OAI.MeanPayoff.BinaryData.Copy.scan_pair line 298
  45. theorem OAI.MeanPayoff.BinaryData.Copy.scan line 303
  46. theorem OAI.MeanPayoff.BinaryData.Copy.check_empty line 318
  47. theorem OAI.MeanPayoff.BinaryData.Copy.restore_step line 325
  48. theorem OAI.MeanPayoff.BinaryData.Copy.restore_source line 332
  49. theorem OAI.MeanPayoff.BinaryData.Copy.restore_put line 340
  50. theorem OAI.MeanPayoff.BinaryData.Copy.restore_empty line 347
  51. theorem OAI.MeanPayoff.BinaryData.Copy.restore_all line 351
  52. theorem OAI.MeanPayoff.BinaryData.Copy.copies line 361