OAI/Combinatorics/ParityLifts/TreeWords.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.StackConfiguration.ext line 7
  2. inductive OAI.ParityWL.Complexity.StackTrace line 12
  3. lemma OAI.ParityWL.Complexity.StackTrace.exec line 18
  4. lemma OAI.ParityWL.Complexity.StackTrace.trans line 29
  5. lemma OAI.ParityWL.Complexity.StackTrace.one line 40
  6. def OAI.ParityWL.Complexity.copyWord line 45

    Source documentation

    Prepending a copy preserves the source and clears the temporary stack.

    def copyWord {t a : ℕ} (src dst tmp : Fin (t + 1)) :=
…
  7. lemma OAI.ParityWL.Complexity.copyWord_run line 48
  8. def OAI.ParityWL.Complexity.pushSymbol line 77

    Source documentation

    A fixed one-cell insertion.

    def pushSymbol {t a : ℕ} (dst : Fin (t + 1)) (c : StackSymbol a) :=
…

    Mentions: OAI.ParityWL.Complexity.StackSymbol

  9. lemma OAI.ParityWL.Complexity.pushSymbol_run line 80
  10. inductive OAI.ParityWL.Complexity.DataTree line 93

    Source documentation

    A prefix-encoded finite binary tree; every code is nonempty and uniquely self-delimiting. Working trees need no infinite-alphabet cells.

    inductive DataTree where
…
  11. def OAI.ParityWL.Complexity.DataTree.code line 98
  12. def OAI.ParityWL.Complexity.DataTree.size line 102
  13. lemma OAI.ParityWL.Complexity.DataTree.length_code line 106
  14. lemma OAI.ParityWL.Complexity.DataTree.size_pos line 111
  15. def OAI.ParityWL.Complexity.treeScan line 116

    Source documentation

    Sweep one prefix tree into dst in reverse order, tracking unvisited child slots on a unary stack. A null pending stack terminates; all transitions are constant-size finite-table operations.

    def treeScan {t : ℕ} (src dst pending : Fin (t + 1)) : StackMachine Bool t 0 where
…

    Mentions: OAI.ParityWL.Complexity.StackMachine

  16. def OAI.ParityWL.Complexity.scanUpdate line 125
  17. def OAI.ParityWL.Complexity.scanResult line 130
  18. lemma OAI.ParityWL.Complexity.treeScan_nil_step line 134
  19. lemma OAI.ParityWL.Complexity.scanUpdate_comp line 162
  20. lemma OAI.ParityWL.Complexity.treeScan_node_step line 177
  21. lemma OAI.ParityWL.Complexity.treeScan_trace line 200
  22. lemma OAI.ParityWL.Complexity.treeScan_run line 236
  23. def OAI.ParityWL.Complexity.moveTree line 253
  24. lemma OAI.ParityWL.Complexity.moveTree_run line 256