OAI/Combinatorics/ContingencyTables/Machines/DirectedBFSRuntime.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary execution of the entire materialized BFS

  1. def OAI.ContingencyTables.DirectedBFSRuntime.advance line 12
  2. def OAI.ContingencyTables.DirectedBFSRuntime.advanceRealizer line 13
  3. lemma OAI.ContingencyTables.DirectedBFSRuntime.polynomial_advance line 16
  4. lemma OAI.ContingencyTables.DirectedBFSRuntime.fold_eq line 20
  5. theorem OAI.ContingencyTables.DirectedBFSRuntime.polynomial_fold line 27
  6. def OAI.ContingencyTables.DirectedBFSRuntime.initialRow line 61
  7. def OAI.ContingencyTables.DirectedBFSRuntime.initialRowRealizer line 64
  8. lemma OAI.ContingencyTables.DirectedBFSRuntime.polynomial_initialRow line 71
  9. def OAI.ContingencyTables.DirectedBFSRuntime.initialInput line 78
  10. def OAI.ContingencyTables.DirectedBFSRuntime.initialRealizer line 79
  11. lemma OAI.ContingencyTables.DirectedBFSRuntime.polynomial_initial line 82
  12. def OAI.ContingencyTables.DirectedBFSRuntime.prepare line 87
  13. def OAI.ContingencyTables.DirectedBFSRuntime.prepareRealizer line 89
  14. lemma OAI.ContingencyTables.DirectedBFSRuntime.polynomial_prepare line 93
  15. def OAI.ContingencyTables.DirectedBFSRuntime.runInput line 97
  16. def OAI.ContingencyTables.DirectedBFSRuntime.runRealizer line 98
  17. theorem OAI.ContingencyTables.DirectedBFSRuntime.polynomial_run line 106
  18. def OAI.ContingencyTables.DirectedBFSRuntime.searchInput line 110
  19. def OAI.ContingencyTables.DirectedBFSRuntime.searchRealizer line 111
  20. theorem OAI.ContingencyTables.DirectedBFSRuntime.polynomial_search line 114