OAI/Combinatorics/UniformKServer/StackTape.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A stack is physically stored at a tape head. Padding is literal blank cells, not a unit-cost unbounded register. Each push/pop uses at most two transitions.

  1. def OAI.UniformKServer.StackTape.encode line 15
  2. def OAI.UniformKServer.StackTape.Rep line 20
  3. theorem OAI.UniformKServer.StackTape.head line 22
  4. theorem OAI.UniformKServer.StackTape.blank line 26
  5. def OAI.UniformKServer.StackTape.push line 28
  6. def OAI.UniformKServer.StackTape.pop line 31
  7. theorem OAI.UniformKServer.StackTape.push_rep line 34
  8. theorem OAI.UniformKServer.StackTape.pop_rep line 47