OAI/Computability/Scheduling/TreeData.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ThreeMachine.StackCompiler.Data line 9
  2. def OAI.ThreeMachine.StackCompiler.Data.encode line 16
  3. def OAI.ThreeMachine.StackCompiler.Data.size line 20
  4. theorem OAI.ThreeMachine.StackCompiler.Data.encode_nil line 22
  5. theorem OAI.ThreeMachine.StackCompiler.Data.encode_pair line 23
  6. theorem OAI.ThreeMachine.StackCompiler.Data.size_nil line 24
  7. theorem OAI.ThreeMachine.StackCompiler.Data.size_pair line 25
  8. def OAI.ThreeMachine.StackCompiler.Data.head line 28
  9. def OAI.ThreeMachine.StackCompiler.Data.tail line 29
  10. def OAI.ThreeMachine.StackCompiler.Program.scanActions line 36
  11. def OAI.ThreeMachine.StackCompiler.Program.scan line 40
  12. def OAI.ThreeMachine.StackCompiler.Program.scanned line 43
  13. def OAI.ThreeMachine.StackCompiler.Program.scanOnce line 47
  14. theorem OAI.ThreeMachine.StackCompiler.Program.scan_instruction line 51
  15. theorem OAI.ThreeMachine.StackCompiler.Program.scanned_scanned line 66
  16. theorem OAI.ThreeMachine.StackCompiler.Program.scan_tree_continue line 79
  17. theorem OAI.ThreeMachine.StackCompiler.Program.scan_tree line 126
  18. def OAI.ThreeMachine.StackCompiler.Program.Runs line 143
  19. theorem OAI.ThreeMachine.StackCompiler.Program.Exec.runs line 146
  20. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.mono line 149
  21. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.computes line 154
  22. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.seq line 163
  23. def OAI.ThreeMachine.StackCompiler.Program.branch line 169
  24. theorem OAI.ThreeMachine.StackCompiler.Program.branch_left_exec line 177
  25. theorem OAI.ThreeMachine.StackCompiler.Program.branch_right_exec line 193
  26. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.branch_left line 209
  27. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.branch_right line 217
  28. def OAI.ThreeMachine.StackCompiler.Program.move line 225
  29. theorem OAI.ThreeMachine.StackCompiler.Program.move_exec line 228
  30. def OAI.ThreeMachine.StackCompiler.Program.push line 257
  31. theorem OAI.ThreeMachine.StackCompiler.Program.push_exec line 260
  32. def OAI.ThreeMachine.StackCompiler.Program.setNil line 268
  33. theorem OAI.ThreeMachine.StackCompiler.Program.setNil_runs line 270
  34. def OAI.ThreeMachine.StackCompiler.Program.setPair line 275
  35. theorem OAI.ThreeMachine.StackCompiler.Program.setPair_runs line 279