OAI/Computability/MeanPayoff/StackMacros.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.RegisterBits.install_self line 7
  2. def OAI.MeanPayoff.RegisterBits.slots line 15
  3. theorem OAI.MeanPayoff.RegisterBits.slots_injective line 21
  4. theorem OAI.MeanPayoff.RegisterBits.renamed_start line 29
  5. theorem OAI.MeanPayoff.RegisterBits.move_tree line 35
  6. theorem OAI.MeanPayoff.RegisterBits.copy_tree line 73
  7. inductive OAI.MeanPayoff.ForestMachine.Instruction line 114
  8. structure OAI.MeanPayoff.ForestMachine.Program line 124
  9. structure OAI.MeanPayoff.ForestMachine.Config line 128
  10. def OAI.MeanPayoff.ForestMachine.encodeForest line 133
  11. theorem OAI.MeanPayoff.ForestMachine.encodeForest_nil line 134
  12. theorem OAI.MeanPayoff.ForestMachine.encodeForest_cons line 135
  13. def OAI.MeanPayoff.ForestMachine.bitStore line 138
  14. theorem OAI.MeanPayoff.ForestMachine.bitStore_at line 140
  15. theorem OAI.MeanPayoff.ForestMachine.bitStore_scratch₀ line 142
  16. theorem OAI.MeanPayoff.ForestMachine.bitStore_scratch₁ line 144
  17. theorem OAI.MeanPayoff.ForestMachine.bitStore_update line 147
  18. def OAI.MeanPayoff.ForestMachine.Valid line 158
  19. def OAI.MeanPayoff.ForestMachine.step line 166
  20. def OAI.MeanPayoff.ForestMachine.skip line 187
  21. def OAI.MeanPayoff.ForestMachine.block line 193
  22. def OAI.MeanPayoff.ForestMachine.read line 198
  23. def OAI.MeanPayoff.ForestMachine.branch line 202
  24. abbrev OAI.MeanPayoff.ForestMachine.flow line 213
  25. def OAI.MeanPayoff.ForestMachine.compile line 220
  26. def OAI.MeanPayoff.ForestMachine.embed line 221
  27. def OAI.MeanPayoff.ForestMachine.ValidOp line 231
  28. def OAI.MeanPayoff.ForestMachine.afterBlock line 237
  29. def OAI.MeanPayoff.ForestMachine.blockBound line 247
  30. theorem OAI.MeanPayoff.ForestMachine.block_contract line 253
  31. theorem OAI.MeanPayoff.ForestMachine.block_deterministic line 276
  32. theorem OAI.MeanPayoff.ForestMachine.step_deterministic line 281
  33. theorem OAI.MeanPayoff.ForestMachine.advance_deterministic line 288
  34. def OAI.MeanPayoff.ForestMachine.duration line 298
  35. theorem OAI.MeanPayoff.ForestMachine.advance_output_irrelevant line 302
  36. theorem OAI.MeanPayoff.ForestMachine.duration_spec line 318
  37. theorem OAI.MeanPayoff.ForestMachine.macro_boundary line 337