OAI/Algebra/FormulaHitting/Program.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.dimensionExpr line 10
  2. def OAI.NCHitting.entryProgram line 13
  3. def OAI.NCHitting.rowProgram line 21
  4. def OAI.NCHitting.variableProgram line 23
  5. def OAI.NCHitting.generatorProgram line 25
  6. def OAI.NCHitting.encodedEntry line 30
  7. def OAI.NCHitting.encodedOutput line 34
  8. def OAI.NCHitting.generate line 40
  9. theorem OAI.NCHitting.entryProgram_output line 42
  10. theorem OAI.NCHitting.rowProgram_output line 47
  11. theorem OAI.NCHitting.variableProgram_output line 53
  12. theorem OAI.NCHitting.generate_output line 60
  13. theorem OAI.NCHitting.encodedEntry_denominator_pos line 65
  14. def OAI.NCHitting.decode line 74
  15. theorem OAI.NCHitting.decode_encodedEntry line 77
  16. theorem OAI.NCHitting.encodedEntry_bits_le line 88