OAI/Combinatorics/ParityLifts/StackMachine.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.StackSymbol line 7
  2. def OAI.ParityWL.Complexity.encodeTop line 9
  3. def OAI.ParityWL.Complexity.decodeTop line 13
  4. lemma OAI.ParityWL.Complexity.decode_encodeTop line 16
  5. lemma OAI.ParityWL.Complexity.encode_decodeTop line 19
  6. lemma OAI.ParityWL.Complexity.encodeTop_zero_iff line 23
  7. def OAI.ParityWL.Complexity.wordCell line 29
  8. lemma OAI.ParityWL.Complexity.wordCell_zero line 32
  9. lemma OAI.ParityWL.Complexity.wordCell_nil line 35
  10. lemma OAI.ParityWL.Complexity.wordCell_neg line 38
  11. lemma OAI.ParityWL.Complexity.wordCell_cons line 41
  12. lemma OAI.ParityWL.Complexity.wordCell_pop line 53
  13. inductive OAI.ParityWL.Complexity.StackOp line 60
  14. def OAI.ParityWL.Complexity.StackOp.apply line 66
  15. def OAI.ParityWL.Complexity.StackOp.action line 71
  16. def OAI.ParityWL.Complexity.StackOp.pending line 76
  17. def OAI.ParityWL.Complexity.finishWrite line 80
  18. lemma OAI.ParityWL.Complexity.tape_operation line 83
  19. structure OAI.ParityWL.Complexity.StackMachine line 139
  20. structure OAI.ParityWL.Complexity.StackConfiguration line 144
  21. def OAI.ParityWL.Complexity.StackMachine.step line 148
  22. abbrev OAI.ParityWL.Complexity.StackControl line 156
  23. def OAI.ParityWL.Complexity.StackMachine.lower line 158
  24. def OAI.ParityWL.Complexity.StackMachine.Represents line 168
  25. lemma OAI.ParityWL.Complexity.StackMachine.lower_two_steps line 172
  26. def OAI.ParityWL.Complexity.stackInputSymbol line 196
  27. lemma OAI.ParityWL.Complexity.encodeTop_input line 199
  28. def OAI.ParityWL.Complexity.StackMachine.initialConfiguration line 203
  29. def OAI.ParityWL.Complexity.StackMachine.run line 208
  30. lemma OAI.ParityWL.Complexity.StackMachine.lower_initial line 212
  31. lemma OAI.ParityWL.Complexity.StackMachine.lower_iterate line 234
  32. lemma OAI.ParityWL.Complexity.StackMachine.lower_run line 246
  33. def OAI.ParityWL.Complexity.StackMachine.compiled line 254

    Source documentation

    Every machine with finite control and finitely many finite-alphabet stacks is realized by the multitape Machine, at exactly two local steps per stack step. This includes input preparation and halting semantics.

    noncomputable def StackMachine.compiled {Q : Type} [Fintype Q] {t a : ℕ}
    (P : StackMachine Q t a) : Machine := P.lower.packed

    Mentions: OAI.ParityWL.Complexity.StackMachine, OAI.ParityWL.Complexity.Machine

  34. lemma OAI.ParityWL.Complexity.StackMachine.compiled_emits line 257