OAI/Computability/Scheduling/RoutineCompiler.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Tree.Code.rename line 10
  2. def OAI.ThreeMachine.StackCompiler.Tree.overlay line 20
  3. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_apply line 24
  4. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_out line 28
  5. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_update line 31
  6. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_of_agree line 42
  7. theorem OAI.ThreeMachine.StackCompiler.Tree.Eval.rename line 53
  8. def OAI.ThreeMachine.StackCompiler.Tree.Bounded line 73
  9. theorem OAI.ThreeMachine.StackCompiler.Tree.Eval.bounded line 76
  10. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.mono line 79
  11. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.seq line 84
  12. def OAI.ThreeMachine.StackCompiler.Tree.join line 90
  13. theorem OAI.ThreeMachine.StackCompiler.Tree.join_inl line 93
  14. theorem OAI.ThreeMachine.StackCompiler.Tree.join_inr line 95
  15. theorem OAI.ThreeMachine.StackCompiler.Tree.join_update_left line 97
  16. theorem OAI.ThreeMachine.StackCompiler.Tree.join_update_right line 104
  17. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_left line 112
  18. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_right line 119
  19. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.left line 125
  20. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.right line 131
  21. def OAI.ThreeMachine.StackCompiler.zeroStore line 142
  22. def OAI.ThreeMachine.StackCompiler.start line 144
  23. def OAI.ThreeMachine.StackCompiler.finish line 147
  24. structure OAI.ThreeMachine.StackCompiler.Routine line 150
  25. def OAI.ThreeMachine.StackCompiler.Routine.mono line 165
  26. def OAI.ThreeMachine.StackCompiler.Routine.identity line 168
  27. def OAI.ThreeMachine.StackCompiler.Routine.nil line 179
  28. def OAI.ThreeMachine.StackCompiler.Routine.select line 190
  29. theorem OAI.ThreeMachine.StackCompiler.start_input line 208
  30. theorem OAI.ThreeMachine.StackCompiler.start_other line 209
  31. theorem OAI.ThreeMachine.StackCompiler.finish_output line 210
  32. theorem OAI.ThreeMachine.StackCompiler.finish_input line 211
  33. theorem OAI.ThreeMachine.StackCompiler.start_left line 213
  34. theorem OAI.ThreeMachine.StackCompiler.start_right line 220
  35. theorem OAI.ThreeMachine.StackCompiler.finish_lr line 227
  36. theorem OAI.ThreeMachine.StackCompiler.reset_output line 232
  37. theorem OAI.ThreeMachine.StackCompiler.reset_input line 237
  38. def OAI.ThreeMachine.StackCompiler.Routine.compCode line 249
  39. def OAI.ThreeMachine.StackCompiler.Routine.comp line 255
  40. theorem OAI.ThreeMachine.StackCompiler.reset_start line 295
  41. def OAI.ThreeMachine.StackCompiler.Routine.pairCode line 303
  42. def OAI.ThreeMachine.StackCompiler.Routine.pair line 311
  43. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.loop_stop line 363
  44. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.loop_step line 367