OAI/Combinatorics/ContingencyTables/Transport/DirectedBFSCode.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Materialized breadth-first path tables

Every round reads the preceding path table and writes one table of the same size. Consequently evaluation does not recursively recompute old rounds when different vertices ask for their predecessors.

  1. abbrev OAI.ContingencyTables.DirectedBFSCode.Graph line 15
  2. abbrev OAI.ContingencyTables.DirectedBFSCode.Store line 16
  3. def OAI.ContingencyTables.DirectedBFSCode.adjacent line 18
  4. def OAI.ContingencyTables.DirectedBFSCode.lookup line 19
  5. def OAI.ContingencyTables.DirectedBFSCode.predecessor line 21
  6. def OAI.ContingencyTables.DirectedBFSCode.roundRow line 24
  7. def OAI.ContingencyTables.DirectedBFSCode.round line 29
  8. def OAI.ContingencyTables.DirectedBFSCode.initial line 32
  9. def OAI.ContingencyTables.DirectedBFSCode.run line 35
  10. def OAI.ContingencyTables.DirectedBFSCode.search line 38
  11. def OAI.ContingencyTables.DirectedBFSCode.graphCode line 40
  12. def OAI.ContingencyTables.DirectedBFSCode.storeCode line 43
  13. lemma OAI.ContingencyTables.DirectedBFSCode.range_eq_map line 46
  14. lemma OAI.ContingencyTables.DirectedBFSCode.adjacent_graphCode line 49
  15. lemma OAI.ContingencyTables.DirectedBFSCode.lookup_storeCode line 53
  16. lemma OAI.ContingencyTables.DirectedBFSCode.predecessor_code line 57
  17. lemma OAI.ContingencyTables.DirectedBFSCode.roundRow_code line 68
  18. lemma OAI.ContingencyTables.DirectedBFSCode.round_code line 82
  19. lemma OAI.ContingencyTables.DirectedBFSCode.initial_code line 91
  20. lemma OAI.ContingencyTables.DirectedBFSCode.fold_round_code line 103
  21. theorem OAI.ContingencyTables.DirectedBFSCode.run_code line 112
  22. theorem OAI.ContingencyTables.DirectedBFSCode.search_code line 116