OAI/Combinatorics/ContingencyTables/Counting/CompanionOuterHistoryProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Chronological execution of all counting phases

  1. abbrev OAI.ContingencyTables.CompanionOuterHistoryProgram.Prepared line 8
  2. abbrev OAI.ContingencyTables.CompanionOuterHistoryProgram.Stored line 9
  3. abbrev OAI.ContingencyTables.CompanionOuterHistoryProgram.Fixed line 10
  4. abbrev OAI.ContingencyTables.CompanionOuterHistoryProgram.State line 11
  5. abbrev OAI.ContingencyTables.CompanionOuterHistoryProgram.Input line 12
  6. def OAI.ContingencyTables.CompanionOuterHistoryProgram.phaseInput line 17
  7. def OAI.ContingencyTables.CompanionOuterHistoryProgram.phaseInputRealizer line 18
  8. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_phaseInput line 19
  9. def OAI.ContingencyTables.CompanionOuterHistoryProgram.next line 22
  10. def OAI.ContingencyTables.CompanionOuterHistoryProgram.nextRealizer line 23
  11. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_next line 26
  12. def OAI.ContingencyTables.CompanionOuterHistoryProgram.advance line 29
  13. def OAI.ContingencyTables.CompanionOuterHistoryProgram.advanceRealizer line 30
  14. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_advance line 34
  15. def OAI.ContingencyTables.CompanionOuterHistoryProgram.run line 40
  16. def OAI.ContingencyTables.CompanionOuterHistoryProgram.runRealizer line 41
  17. def OAI.ContingencyTables.CompanionOuterHistoryProgram.storedHistory line 44
  18. def OAI.ContingencyTables.CompanionOuterHistoryProgram.storedHistoryRealizer line 45
  19. def OAI.ContingencyTables.CompanionOuterHistoryProgram.output line 48
  20. def OAI.ContingencyTables.CompanionOuterHistoryProgram.outputRealizer line 50
  21. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.advance_fixed line 55
  22. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.run_fixed line 56