OAI/Combinatorics/VariableWL/OneHead.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Computation.stackCells_pop line 11
  2. def OAI.VariableWL.Computation.Stack.Machine.outputState line 24
  3. theorem OAI.VariableWL.Computation.Stack.Machine.output_step line 28
  4. theorem OAI.VariableWL.Computation.Stack.Machine.output_all line 66
  5. theorem OAI.VariableWL.Computation.Stack.Machine.output_halt line 76
  6. theorem OAI.VariableWL.Computation.Stack.Machine.execute_halt line 83
  7. theorem OAI.VariableWL.Computation.Stack.Machine.execute_run line 111
  8. theorem OAI.VariableWL.Computation.Stack.Machine.compile_outputs line 129
  9. def OAI.VariableWL.Computation.Stack.Machine.compile line 171
  10. theorem OAI.VariableWL.Computation.Stack.Machine.outputs_compile line 174
  11. structure OAI.VariableWL.OneHead.Program line 186
  12. structure OAI.VariableWL.OneHead.State line 191
  13. abbrev OAI.VariableWL.OneHead.Cell line 196
  14. def OAI.VariableWL.OneHead.Program.action line 198
  15. def OAI.VariableWL.OneHead.move line 201
  16. def OAI.VariableWL.OneHead.Program.next line 206
  17. def OAI.VariableWL.OneHead.encode line 210
  18. def OAI.VariableWL.OneHead.Program.incoming line 213
  19. def OAI.VariableWL.OneHead.Program.rule line 216
  20. theorem OAI.VariableWL.OneHead.incoming_encode line 220
  21. theorem OAI.VariableWL.OneHead.rule_encode line 230
  22. def OAI.VariableWL.OneHead.Program.run line 249
  23. def OAI.VariableWL.OneHead.evolution line 253
  24. theorem OAI.VariableWL.OneHead.evolution_encode line 259
  25. def OAI.VariableWL.OneHead.Program.acceptingCell line 269
  26. theorem OAI.VariableWL.OneHead.accepting_encode line 272
  27. theorem OAI.VariableWL.OneHead.next_of_halt line 285
  28. theorem OAI.VariableWL.OneHead.run_of_halt line 290
  29. theorem OAI.VariableWL.OneHead.run_add line 296
  30. theorem OAI.VariableWL.OneHead.run_freeze line 304
  31. theorem OAI.VariableWL.OneHead.head_bounds line 310