OAI/Combinatorics/VariableWL/Stack.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Program.evolve line 12
  2. theorem OAI.VariableWL.Computation.Program.evolve_add line 16
  3. theorem OAI.VariableWL.Computation.Program.evolve_run line 25
  4. theorem OAI.VariableWL.Computation.Program.evolve_one line 31
  5. theorem OAI.VariableWL.Computation.state_ext line 36
  6. inductive OAI.VariableWL.Computation.Stack.Control line 44
  7. def OAI.VariableWL.Computation.Stack.readBit line 53
  8. theorem OAI.VariableWL.Computation.Stack.readBit_bit line 57
  9. theorem OAI.VariableWL.Computation.Stack.readBit_none line 58
  10. theorem OAI.VariableWL.Computation.Stack.readBit_bind line 59
  11. def OAI.VariableWL.Computation.Stack.marker line 62
  12. def OAI.VariableWL.Computation.Stack.instruction line 64
  13. def OAI.VariableWL.Computation.Stack.Machine.program line 69
  14. def OAI.VariableWL.Computation.Stack.Machine.execState line 105
  15. def OAI.VariableWL.Computation.Stack.intermediate line 111
  16. theorem OAI.VariableWL.Computation.Stack.step_eq_intermediate line 117
  17. theorem OAI.VariableWL.Computation.Stack.Machine.execute_two line 125
  18. theorem OAI.VariableWL.Computation.typedWordCells_snoc line 177
  19. def OAI.VariableWL.Computation.Stack.tapeState line 191
  20. def OAI.VariableWL.Computation.Stack.firstData line 197
  21. def OAI.VariableWL.Computation.Stack.secondData line 201
  22. theorem OAI.VariableWL.Computation.Stack.twoTapeUpdates line 206
  23. def OAI.VariableWL.Computation.Stack.inputTapes line 235
  24. def OAI.VariableWL.Computation.Stack.pushInput line 236
  25. theorem OAI.VariableWL.Computation.Stack.pushInput_apply line 238
  26. def OAI.VariableWL.Computation.Stack.inputCells line 244
  27. theorem OAI.VariableWL.Computation.Stack.inputCells_scan line 247
  28. theorem OAI.VariableWL.Computation.Stack.inputCells_zero line 253
  29. theorem OAI.VariableWL.Computation.Stack.inputCells_blank line 256
  30. theorem OAI.VariableWL.Computation.Stack.inputCells_next line 260
  31. def OAI.VariableWL.Computation.Stack.Machine.loading line 280
  32. theorem OAI.VariableWL.Computation.Stack.Machine.loading_two line 284
  33. theorem OAI.VariableWL.Computation.Stack.initial_tapeState line 330
  34. theorem OAI.VariableWL.Computation.Stack.Machine.initial_two line 347
  35. theorem OAI.VariableWL.Computation.Stack.Machine.loading_all line 387
  36. def OAI.VariableWL.Computation.Stack.Machine.backState line 397
  37. theorem OAI.VariableWL.Computation.Stack.Machine.back_zero line 401
  38. theorem OAI.VariableWL.Computation.Stack.Machine.back_succ line 423
  39. theorem OAI.VariableWL.Computation.Stack.Machine.back_all line 448
  40. theorem OAI.VariableWL.Computation.Stack.Machine.loading_end line 456
  41. theorem OAI.VariableWL.Computation.Stack.Machine.initial_empty line 482
  42. theorem OAI.VariableWL.Computation.Stack.Machine.initialize line 506