OAI/Combinatorics/VariableWL/MachineSimulation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.MultiStack.found line 11
  2. def OAI.VariableWL.MultiStack.drainVars line 13
  3. def OAI.VariableWL.MultiStack.drainLabel line 18
  4. theorem OAI.VariableWL.MultiStack.drain_stage line 20
  5. theorem OAI.VariableWL.MultiStack.drain_both line 57
  6. theorem OAI.VariableWL.MultiStack.exists_getI_two line 79
  7. theorem OAI.VariableWL.MultiStack.tape_two_iff line 95
  8. theorem OAI.VariableWL.MultiStack.symbol_zero_ne_two line 111
  9. theorem OAI.VariableWL.MultiStack.symbol_one_ne_two line 118
  10. theorem OAI.VariableWL.MultiStack.word_two_iff line 125
  11. theorem OAI.VariableWL.MultiStack.related_output line 140
  12. instance OAI.VariableWL.MultiStack.(instance at line 156) line 156
  13. instance OAI.VariableWL.MultiStack.(instance at line 158) line 158
  14. def OAI.VariableWL.MultiStack.operationsBound line 162
  15. theorem OAI.VariableWL.MultiStack.operations_le line 164
  16. theorem OAI.VariableWL.MultiStack.outputs_simulated line 167
  17. abbrev OAI.VariableWL.TM0Adapter.Control line 198
  18. def OAI.VariableWL.TM0Adapter.action line 200
  19. def OAI.VariableWL.TM0Adapter.program line 205
  20. def OAI.VariableWL.TM0Adapter.Related line 212
  21. theorem OAI.VariableWL.TM0Adapter.program_none line 218
  22. theorem OAI.VariableWL.TM0Adapter.program_some line 224
  23. theorem OAI.VariableWL.TM0Adapter.next_related line 237
  24. theorem OAI.VariableWL.TM0Adapter.steps_related line 261
  25. theorem OAI.VariableWL.TM0Adapter.halt_related line 271
  26. theorem OAI.VariableWL.TM0Adapter.acceptance_related line 279
  27. theorem OAI.VariableWL.TM0Adapter.initial_related line 287
  28. abbrev OAI.VariableWL.MachineOneHead.Alphabet line 315
  29. abbrev OAI.VariableWL.MachineOneHead.Label1 line 316
  30. def OAI.VariableWL.MachineOneHead.program1 line 318
  31. def OAI.VariableWL.MachineOneHead.support1 line 319
  32. theorem OAI.VariableWL.MachineOneHead.supported2 line 321
  33. theorem OAI.VariableWL.MachineOneHead.supported1 line 326
  34. abbrev OAI.VariableWL.MachineOneHead.Label0 line 329
  35. def OAI.VariableWL.MachineOneHead.program0 line 330
  36. def OAI.VariableWL.MachineOneHead.support0 line 331
  37. theorem OAI.VariableWL.MachineOneHead.supported0 line 332
  38. abbrev OAI.VariableWL.MachineOneHead.Control line 335
  39. instance OAI.VariableWL.MachineOneHead.(instance at line 336) line 336
  40. def OAI.VariableWL.MachineOneHead.instructionsBound line 338
  41. theorem OAI.VariableWL.MachineOneHead.instructions_le line 339
  42. def OAI.VariableWL.MachineOneHead.oneHead line 343
  43. def OAI.VariableWL.MachineOneHead.input line 346
  44. theorem OAI.VariableWL.MachineOneHead.input_pos line 349
  45. theorem OAI.VariableWL.MachineOneHead.input_length line 351
  46. def OAI.VariableWL.MachineOneHead.stackTime line 357
  47. def OAI.VariableWL.MachineOneHead.time line 358
  48. theorem OAI.VariableWL.MachineOneHead.outputs_oneHead line 362