OAI/Combinatorics/ContingencyTables/Rooted/RootedBinDrawLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The computed bin program has the analysed independent law

The execution order is the computed free-cell catalog. The mathematical law uses another enumeration. Dependent word equivalences identify their independent Boolean inputs, while preserving each physical cell's draw.

  1. abbrev OAI.ContingencyTables.RootedBinDrawLaw.FreeWords line 28
  2. abbrev OAI.ContingencyTables.RootedBinDrawLaw.Words line 31
  3. def OAI.ContingencyTables.RootedBinDrawLaw.freeWordEquiv line 35
  4. def OAI.ContingencyTables.RootedBinDrawLaw.originalWordEquiv line 40
  5. def OAI.ContingencyTables.RootedBinDrawLaw.reindexWords line 45
  6. def OAI.ContingencyTables.RootedBinDrawLaw.wordBits line 49
  7. def OAI.ContingencyTables.RootedBinDrawLaw.wordEquiv line 53
  8. lemma OAI.ContingencyTables.RootedBinDrawLaw.wordBits_eq line 58
  9. def OAI.ContingencyTables.RootedBinDrawLaw.draw line 66
  10. lemma OAI.ContingencyTables.RootedBinDrawLaw.draw_law line 71
  11. lemma OAI.ContingencyTables.RootedBinDrawLaw.interval_bits_le line 83
  12. lemma OAI.ContingencyTables.RootedBinDrawLaw.coordinate_scalar line 90
  13. lemma OAI.ContingencyTables.RootedBinDrawLaw.original_value line 97
  14. lemma OAI.ContingencyTables.RootedBinDrawLaw.original_free_value line 117
  15. lemma OAI.ContingencyTables.RootedBinDrawLaw.draw_coordinate line 132
  16. def OAI.ContingencyTables.RootedBinDrawLaw.flatDraw line 168
  17. theorem OAI.ContingencyTables.RootedBinDrawLaw.flatDraw_law line 173
  18. theorem OAI.ContingencyTables.RootedBinDrawLaw.program_flatDraw line 181