OAI/Combinatorics/VariableWL/StackSimulation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.OneHead.Related line 10
  2. theorem OAI.VariableWL.OneHead.next_related line 13
  3. theorem OAI.VariableWL.OneHead.run_related line 38
  4. def OAI.VariableWL.OneHead.window line 47
  5. theorem OAI.VariableWL.OneHead.cast_injOn_window line 49
  6. def OAI.VariableWL.OneHead.lineInput line 75
  7. def OAI.VariableWL.OneHead.ringInput line 78
  8. theorem OAI.VariableWL.OneHead.ringInput_cast line 81
  9. def OAI.VariableWL.OneHead.lineInitial line 109
  10. def OAI.VariableWL.OneHead.ringInitial line 112
  11. theorem OAI.VariableWL.OneHead.initial_related line 115
  12. theorem OAI.VariableWL.OneHead.line_ring_related line 122
  13. theorem OAI.VariableWL.OneHead.line_ring_acceptance line 134
  14. def OAI.VariableWL.OneHead.markedInput line 152
  15. def OAI.VariableWL.OneHead.product line 155
  16. theorem OAI.VariableWL.OneHead.finEquiv_val line 163
  17. theorem OAI.VariableWL.OneHead.product_initial line 168
  18. theorem OAI.VariableWL.OneHead.product_state line 184
  19. theorem OAI.VariableWL.OneHead.product_acceptance line 197
  20. theorem OAI.VariableWL.OneHead.line_ring_halt line 221
  21. theorem OAI.VariableWL.OneHead.product_final_acceptance line 235
  22. theorem OAI.VariableWL.OneHead.product_consistent_iff line 250
  23. inductive OAI.VariableWL.BoundedSimulation.Steps line 265
  24. theorem OAI.VariableWL.BoundedSimulation.Steps.trans line 271
  25. theorem OAI.VariableWL.BoundedSimulation.Steps.single line 276
  26. theorem OAI.VariableWL.BoundedSimulation.Steps.tail line 278
  27. theorem OAI.VariableWL.BoundedSimulation.Steps.head line 280
  28. def OAI.VariableWL.BoundedSimulation.evolve line 283
  29. theorem OAI.VariableWL.BoundedSimulation.evolve_add line 287
  30. theorem OAI.VariableWL.BoundedSimulation.Steps.evolve line 296
  31. def OAI.VariableWL.BoundedSimulation.Within line 306
  32. theorem OAI.VariableWL.BoundedSimulation.Within.zero line 311
  33. theorem OAI.VariableWL.BoundedSimulation.Within.mono line 312
  34. theorem OAI.VariableWL.BoundedSimulation.Within.trans line 314
  35. theorem OAI.VariableWL.BoundedSimulation.Within.single line 318
  36. theorem OAI.VariableWL.BoundedSimulation.Within.head line 319
  37. theorem OAI.VariableWL.BoundedSimulation.Within.tail line 321
  38. def OAI.VariableWL.StackSimulation.operations line 330
  39. theorem OAI.VariableWL.StackSimulation.operations_run line 339
  40. theorem OAI.VariableWL.StackSimulation.stWrite_length line 343
  41. theorem OAI.VariableWL.StackSimulation.stepAux_length line 348
  42. theorem OAI.VariableWL.StackSimulation.go_steps line 373
  43. theorem OAI.VariableWL.StackSimulation.return_steps line 387
  44. theorem OAI.VariableWL.StackSimulation.normal_bound line 400