OAI/Combinatorics/ParityLifts/TreeMachine.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ParityWL.Complexity.FinStack line 7
  2. def OAI.ParityWL.Complexity.FinStack.of line 14
  3. def OAI.ParityWL.Complexity.dataReg line 17
  4. def OAI.ParityWL.Complexity.workReg line 19
  5. lemma OAI.ParityWL.Complexity.dataReg_ne_workReg line 21
  6. lemma OAI.ParityWL.Complexity.workReg_injective line 27
  7. def OAI.ParityWL.Complexity.dataWords line 34
  8. lemma OAI.ParityWL.Complexity.dataWords_data line 37
  9. lemma OAI.ParityWL.Complexity.dataWords_work line 40
  10. lemma OAI.ParityWL.Complexity.dataWords_update line 43
  11. def OAI.ParityWL.Complexity.dataMass line 62
  12. lemma OAI.ParityWL.Complexity.dataSize_le_mass line 64
  13. inductive OAI.ParityWL.Complexity.TreeOp line 68
  14. def OAI.ParityWL.Complexity.TreeOp.eval line 75
  15. def OAI.ParityWL.Complexity.testNil line 83
  16. lemma OAI.ParityWL.Complexity.testNil_run line 86
  17. def OAI.ParityWL.Complexity.TreeOp.routine line 97
  18. lemma OAI.ParityWL.Complexity.TreeOp.routine_run line 106
  19. structure OAI.ParityWL.Complexity.TreeMachine line 148

    Source documentation

    Finite code over unbounded but explicitly serialized binary trees.

    structure TreeMachine (Q : Type) (r : ℕ) where
…
  20. def OAI.ParityWL.Complexity.TreeMachine.lower line 154
  21. instance OAI.ParityWL.Complexity.(instance at line 161) line 161
  22. inductive OAI.ParityWL.Complexity.TreeExec line 166

    Source documentation

    Work is the sum of one plus the size of all live data before each step. The compiler bound below is linear in this actual execution measure.

    inductive TreeExec {Q : Type} {r : ℕ} (P : TreeMachine Q r) :
    Q → (Fin r → DataTree) → ℕ → (Fin r → DataTree) → Bool → Prop
  | halt (q d b) (h : P.output q = some b) : TreeExec P q d 0 d b
  | next (q d) {m z c} (h : P.output q = none)
      (tail : TreeExec P (P.next q ((P.instruction q).eval d).2)
        ((P.instruction q).eval d).1 m z c) :
      TreeExec P q d (dataMass d + 1 + m) z c

    Mentions: OAI.ParityWL.Complexity.TreeMachine, OAI.ParityWL.Complexity.DataTree, OAI.ParityWL.Complexity.dataMass

  23. lemma OAI.ParityWL.Complexity.TreeExec.lower line 174
  24. structure OAI.ParityWL.Complexity.FinTree line 188
  25. def OAI.ParityWL.Complexity.FinTree.of line 195
  26. def OAI.ParityWL.Complexity.TreeRuns line 198
  27. def OAI.ParityWL.Complexity.TreeMachine.halt line 201
  28. lemma OAI.ParityWL.Complexity.treeHalt_run line 207
  29. def OAI.ParityWL.Complexity.TreeMachine.atomic line 210
  30. lemma OAI.ParityWL.Complexity.treeAtomic_run line 216
  31. lemma OAI.ParityWL.Complexity.TreeExec.map line 222
  32. def OAI.ParityWL.Complexity.TreeMachine.andThen line 234
  33. lemma OAI.ParityWL.Complexity.TreeExec.andThen_right line 245
  34. lemma OAI.ParityWL.Complexity.TreeExec.andThen line 251
  35. lemma OAI.ParityWL.Complexity.TreeRuns.andThen line 274
  36. def OAI.ParityWL.Complexity.TreeMachine.branch line 280
  37. lemma OAI.ParityWL.Complexity.TreeRuns.branch_true line 296
  38. lemma OAI.ParityWL.Complexity.TreeRuns.branch_false line 306
  39. def OAI.ParityWL.Complexity.TreeMachine.repeat line 316
  40. lemma OAI.ParityWL.Complexity.TreeExec.repeat_true line 322
  41. lemma OAI.ParityWL.Complexity.TreeExec.repeat_false line 332