OAI/Computability/Scheduling/MachineBridge.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Packed.halt line 10
  2. theorem OAI.ThreeMachine.StackCompiler.Packed.halt_runs line 12
  3. def OAI.ThreeMachine.StackCompiler.Packed.pushWord line 15
  4. theorem OAI.ThreeMachine.StackCompiler.Packed.pushWord_runs line 19
  5. def OAI.ThreeMachine.StackCompiler.Packed.pop line 32
  6. theorem OAI.ThreeMachine.StackCompiler.Packed.pop_runs line 34
  7. def OAI.ThreeMachine.StackCompiler.Packed.popN line 38
  8. theorem OAI.ThreeMachine.StackCompiler.Packed.popN_runs line 42
  9. def OAI.ThreeMachine.StackCompiler.Raw.boolChunk line 57
  10. theorem OAI.ThreeMachine.StackCompiler.Raw.encoded_cons line 59
  11. def OAI.ThreeMachine.StackCompiler.Raw.encodeBody line 62
  12. theorem OAI.ThreeMachine.StackCompiler.Raw.encodeBody_runs line 67
  13. def OAI.ThreeMachine.StackCompiler.Raw.encodeLoop line 80
  14. theorem OAI.ThreeMachine.StackCompiler.Raw.encodeLoop_runs line 83
  15. def OAI.ThreeMachine.StackCompiler.Raw.decodeAfterTag line 115
  16. def OAI.ThreeMachine.StackCompiler.Raw.decodeBody line 120
  17. theorem OAI.ThreeMachine.StackCompiler.Raw.decodeAfterTag_runs line 123
  18. theorem OAI.ThreeMachine.StackCompiler.Raw.decodeBody_runs line 143
  19. def OAI.ThreeMachine.StackCompiler.Raw.decodeLoop line 152
  20. theorem OAI.ThreeMachine.StackCompiler.Raw.decodeLoop_runs line 155
  21. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_zero line 186
  22. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_start line 189
  23. theorem OAI.ThreeMachine.StackCompiler.Tree.overlay_finish line 194
  24. def OAI.ThreeMachine.StackCompiler.Routine.number line 206
  25. theorem OAI.ThreeMachine.StackCompiler.Routine.number_injective line 209
  26. theorem OAI.ThreeMachine.StackCompiler.Routine.number_ne_zero line 212
  27. def OAI.ThreeMachine.StackCompiler.Routine.numberedCode line 214
  28. theorem OAI.ThreeMachine.StackCompiler.Routine.numberedCode_runs line 216
  29. def OAI.ThreeMachine.StackCompiler.Routine.initRegs line 224
  30. theorem OAI.ThreeMachine.StackCompiler.Routine.initRegs_runs line 228
  31. def OAI.ThreeMachine.StackCompiler.Routine.inputProgram line 238
  32. theorem OAI.ThreeMachine.StackCompiler.Routine.temp_ne_zero line 242
  33. theorem OAI.ThreeMachine.StackCompiler.Routine.reg_number_ne_zero line 246
  34. theorem OAI.ThreeMachine.StackCompiler.Routine.inputProgram_runs line 250
  35. def OAI.ThreeMachine.StackCompiler.Routine.outputProgram line 298
  36. def OAI.ThreeMachine.StackCompiler.Routine.rawProgram line 302
  37. theorem OAI.ThreeMachine.StackCompiler.Routine.outputProgram_runs line 305
  38. theorem OAI.ThreeMachine.StackCompiler.Routine.rawProgram_runs line 336
  39. theorem OAI.ThreeMachine.StackCompiler.Routine.exists_rawMachine line 346