OAI/Combinatorics/ContingencyTables/Counting/CountingPositiveProgram.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

One executed positive-label counting run

The supplied word is partitioned into equally padded phase words. The phase count only truncates a supplied list, so malformed scalar inputs do not create an unbounded loop.

  1. abbrev OAI.ContingencyTables.CountingPositiveProgram.Request line 16
  2. abbrev OAI.ContingencyTables.CountingPositiveProgram.Input line 17
  3. abbrev OAI.ContingencyTables.CountingPositiveProgram.Prepared line 18
  4. def OAI.ContingencyTables.CountingPositiveProgram.prepared line 20
  5. def OAI.ContingencyTables.CountingPositiveProgram.preparedRealizer line 21
  6. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_prepared line 24
  7. def OAI.ContingencyTables.CountingPositiveProgram.phaseCount line 27
  8. def OAI.ContingencyTables.CountingPositiveProgram.phaseCountRealizer line 29
  9. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_phaseCount line 34
  10. def OAI.ContingencyTables.CountingPositiveProgram.phaseWidth line 38
  11. def OAI.ContingencyTables.CountingPositiveProgram.phaseWidthRealizer line 39
  12. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_phaseWidth line 42
  13. def OAI.ContingencyTables.CountingPositiveProgram.bitCount line 45
  14. def OAI.ContingencyTables.CountingPositiveProgram.bitCountRealizer line 46
  15. theorem OAI.ContingencyTables.CountingPositiveProgram.polynomial_bitCount line 49
  16. def OAI.ContingencyTables.CountingPositiveProgram.words line 52
  17. def OAI.ContingencyTables.CountingPositiveProgram.wordsRealizer line 54
  18. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_words line 61
  19. def OAI.ContingencyTables.CountingPositiveProgram.start line 68
  20. def OAI.ContingencyTables.CountingPositiveProgram.startRealizer line 70
  21. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_start line 73
  22. def OAI.ContingencyTables.CountingPositiveProgram.historyInput line 76
  23. def OAI.ContingencyTables.CountingPositiveProgram.historyInputRealizer line 77
  24. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_historyInput line 78
  25. def OAI.ContingencyTables.CountingPositiveProgram.finalStored line 83
  26. def OAI.ContingencyTables.CountingPositiveProgram.finalStoredRealizer line 85
  27. lemma OAI.ContingencyTables.CountingPositiveProgram.polynomial_finalStored line 88
  28. def OAI.ContingencyTables.CountingPositiveProgram.output line 91
  29. def OAI.ContingencyTables.CountingPositiveProgram.outputRealizer line 92
  30. theorem OAI.ContingencyTables.CountingPositiveProgram.polynomial_output line 94
  31. theorem OAI.ContingencyTables.CountingPositiveProgram.phaseWidth_pos line 97
  32. theorem OAI.ContingencyTables.CountingPositiveProgram.words_ofFn line 100