OAI/Combinatorics/ContingencyTables/Counting/CompanionRepeatedReturnProgram.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Bounded iteration of the executed capped-return routine

The numeric repetition count only truncates chunks of the supplied word. The stored profile is clipped to the fixed initial dimension, which is redundant on every actual encoded state.

  1. abbrev OAI.ContingencyTables.CompanionRepeatedReturnProgram.Fixed line 16
  2. abbrev OAI.ContingencyTables.CompanionRepeatedReturnProgram.State line 17
  3. abbrev OAI.ContingencyTables.CompanionRepeatedReturnProgram.Input line 18
  4. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.returnInput line 20
  5. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.returnInputRealizer line 22
  6. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_returnInput line 30
  7. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.candidate line 40
  8. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.candidateRealizer line 41
  9. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_candidate line 44
  10. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.bound line 47
  11. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.boundRealizer line 48
  12. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_bound line 50
  13. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.next line 58
  14. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.nextRealizer line 59
  15. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_next line 63
  16. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.advance line 67
  17. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.advanceRealizer line 68
  18. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_advance line 69
  19. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.advance_weight line 72
  20. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.walk line 83
  21. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.walkRealizer line 85
  22. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.fold_fixed line 87
  23. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.fold_weight line 93
  24. theorem OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_walk line 104
  25. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.widthInput line 111
  26. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.widthInputRealizer line 113
  27. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_widthInput line 115
  28. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.blockWidth line 120
  29. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.blockWidthRealizer line 122
  30. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_blockWidth line 128
  31. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.words line 132
  32. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.wordsRealizer line 134
  33. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_words line 141
  34. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.output line 148
  35. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.outputRealizer line 149
  36. theorem OAI.ContingencyTables.CompanionRepeatedReturnProgram.polynomial_output line 153