OAI/Combinatorics/ContingencyTables/Machines/DirectedBFSProgram.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary programs for one stored BFS round

  1. abbrev OAI.ContingencyTables.DirectedBFSProgram.Context line 15
  2. abbrev OAI.ContingencyTables.DirectedBFSProgram.Query line 16
  3. abbrev OAI.ContingencyTables.DirectedBFSProgram.Candidate line 17
  4. def OAI.ContingencyTables.DirectedBFSProgram.indices line 19
  5. def OAI.ContingencyTables.DirectedBFSProgram.indicesRealizer line 20
  6. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_indices line 22
  7. def OAI.ContingencyTables.DirectedBFSProgram.pathSomeRealizer line 27
  8. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_pathSome line 33
  9. def OAI.ContingencyTables.DirectedBFSProgram.lookupPath line 38
  10. def OAI.ContingencyTables.DirectedBFSProgram.lookupRealizer line 39
  11. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_lookup line 40
  12. def OAI.ContingencyTables.DirectedBFSProgram.readEdge line 42
  13. def OAI.ContingencyTables.DirectedBFSProgram.readEdgeRealizer line 43
  14. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_readEdge line 46
  15. def OAI.ContingencyTables.DirectedBFSProgram.candidate line 51
  16. def OAI.ContingencyTables.DirectedBFSProgram.candidateRealizer line 54
  17. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_candidate line 65
  18. def OAI.ContingencyTables.DirectedBFSProgram.headOptionRealizer line 80
  19. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_headOption line 83
  20. def OAI.ContingencyTables.DirectedBFSProgram.predecessorInput line 87
  21. def OAI.ContingencyTables.DirectedBFSProgram.predecessorRealizer line 89
  22. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_predecessor line 97
  23. def OAI.ContingencyTables.DirectedBFSProgram.appendPath line 103
  24. def OAI.ContingencyTables.DirectedBFSProgram.appendPathRealizer line 105
  25. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_appendPath line 109
  26. def OAI.ContingencyTables.DirectedBFSProgram.fromPredecessor line 115
  27. def OAI.ContingencyTables.DirectedBFSProgram.fromPredecessorRealizer line 118
  28. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_fromPredecessor line 126
  29. def OAI.ContingencyTables.DirectedBFSProgram.missing line 133
  30. def OAI.ContingencyTables.DirectedBFSProgram.missingRealizer line 136
  31. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_missing line 143
  32. def OAI.ContingencyTables.DirectedBFSProgram.rowInput line 148
  33. def OAI.ContingencyTables.DirectedBFSProgram.rowRealizer line 150
  34. lemma OAI.ContingencyTables.DirectedBFSProgram.polynomial_row line 158
  35. def OAI.ContingencyTables.DirectedBFSProgram.roundInput line 166
  36. def OAI.ContingencyTables.DirectedBFSProgram.roundRealizer line 167
  37. theorem OAI.ContingencyTables.DirectedBFSProgram.polynomial_round line 170