OAI/NumberTheory/Ostmann/Tree/PreorderNodePaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit preorder indices for internal nodes and their ancestors

  1. def OAI.Ostmann.nodePathIndex line 11

    Source documentation

    false descends left, true descends right.

    def nodePathIndex : ℕ → List Bool → ℕ
  | 0, _ => 0
  | _ + 1, [] => 0
  | n + 1, b :: p => (if b then 2 ^ n else 1) + nodePathIndex n p
  2. theorem OAI.Ostmann.nodePathIndex_lt line 16
  3. def OAI.Ostmann.preorderNodePath line 34
  4. theorem OAI.Ostmann.preorderNodePath_length line 48
  5. theorem OAI.Ostmann.nodePathIndex_preorderNodePath line 59
  6. theorem OAI.Ostmann.preorderNodePath_nodePathIndex line 72
  7. theorem OAI.Ostmann.nodePathIndex_nonempty_pos line 96
  8. theorem OAI.Ostmann.nodePathIndex_proper_prefix line 107