OAI/Combinatorics/ParityLifts/TreeRoutines.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.StackMachine.halt line 7
  2. lemma OAI.ParityWL.Complexity.halt_run line 12
  3. def OAI.ParityWL.Complexity.StackMachine.branch line 16

    Source documentation

    Branching tests only the finitely many currently scanned stack symbols.

    def StackMachine.branch {Q R : Type} {t a : ℕ}
    (test : (Fin (t + 1) → Option (StackSymbol a)) → Bool)
    (P : StackMachine Q t a) (T : StackMachine R t a) :
    StackMachine (Unit ⊕ Q ⊕ R) t a where
…

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

  4. lemma OAI.ParityWL.Complexity.Runs.branch_true line 30
  5. lemma OAI.ParityWL.Complexity.Runs.branch_false line 48
  6. def OAI.ParityWL.Complexity.popSymbol line 66
  7. lemma OAI.ParityWL.Complexity.popSymbol_run line 69
  8. def OAI.ParityWL.Complexity.nodeWord line 86

    Source documentation

    Assemble a binary node without changing either operand, even if the store destination aliases an operand. The buffer and temporary are cleared.

    def nodeWord {t : ℕ} (dst left right buf tmp : Fin (t + 1)) :=
…
  9. lemma OAI.ParityWL.Complexity.nodeWord_run line 91
  10. def OAI.ParityWL.Complexity.nilWord line 137
  11. lemma OAI.ParityWL.Complexity.nilWord_run line 140
  12. def OAI.ParityWL.Complexity.DataTree.child line 153
  13. def OAI.ParityWL.Complexity.selectChildTail line 157
  14. def OAI.ParityWL.Complexity.selectChild line 161
  15. lemma OAI.ParityWL.Complexity.selectChild_run line 166
  16. def OAI.ParityWL.Complexity.projectWord line 244

    Source documentation

    Tree projection with untouched operand and clean finite work stacks.

    def projectWord {t : ℕ} (dst src buf tmp out pending : Fin (t + 1)) (right : Bool) :=
…
  17. lemma OAI.ParityWL.Complexity.projectWord_run line 248