OAI/Combinatorics/ContingencyTables/Machines/FiniteGraphCutProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Executing the selected root-away cut

Deletion filters the stored adjacency rows. The endpoint and cut side are then computed by the bounded reachability program.

  1. abbrev OAI.ContingencyTables.FiniteGraphCutProgram.EdgeInput line 16
  2. abbrev OAI.ContingencyTables.FiniteGraphCutProgram.KeepInput line 17
  3. def OAI.ContingencyTables.FiniteGraphCutProgram.keep line 19
  4. def OAI.ContingencyTables.FiniteGraphCutProgram.keepRealizer line 23
  5. lemma OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_keep line 34
  6. def OAI.ContingencyTables.FiniteGraphCutProgram.deleteRow line 52
  7. def OAI.ContingencyTables.FiniteGraphCutProgram.deleteRowRealizer line 55
  8. lemma OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_deleteRow line 63
  9. def OAI.ContingencyTables.FiniteGraphCutProgram.deleteGraph line 70
  10. def OAI.ContingencyTables.FiniteGraphCutProgram.deleteGraphRealizer line 73
  11. theorem OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_deleteGraph line 76
  12. def OAI.ContingencyTables.FiniteGraphCutProgram.reachableCode line 81
  13. def OAI.ContingencyTables.FiniteGraphCutProgram.reachableCodeRealizer line 83
  14. lemma OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_reachableCode line 86
  15. abbrev OAI.ContingencyTables.FiniteGraphCutProgram.CutInput line 91
  16. def OAI.ContingencyTables.FiniteGraphCutProgram.awayCode line 93
  17. def OAI.ContingencyTables.FiniteGraphCutProgram.awayTestRealizer line 96
  18. lemma OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_awayTest line 101
  19. def OAI.ContingencyTables.FiniteGraphCutProgram.awayCodeRealizer line 107
  20. lemma OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_awayCode line 111
  21. def OAI.ContingencyTables.FiniteGraphCutProgram.cutCode line 118
  22. def OAI.ContingencyTables.FiniteGraphCutProgram.cutCodeRealizer line 121
  23. theorem OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_cutCode line 126
  24. def OAI.ContingencyTables.FiniteGraphCutProgram.canonicalCutCode line 133
  25. def OAI.ContingencyTables.FiniteGraphCutProgram.canonicalCutCodeRealizer line 136
  26. theorem OAI.ContingencyTables.FiniteGraphCutProgram.polynomial_canonicalCutCode line 142