OAI/Combinatorics/IndependentSets/Reduction/FiniteScan.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LargeIndependentSets.FiniteScan.State line 13
  2. def OAI.LargeIndependentSets.FiniteScan.State.value line 18
  3. def OAI.LargeIndependentSets.FiniteScan.State.bits line 23
  4. def OAI.LargeIndependentSets.FiniteScan.initial line 26
  5. def OAI.LargeIndependentSets.FiniteScan.step line 28
  6. lemma OAI.LargeIndependentSets.FiniteScan.read_n line 34
  7. lemma OAI.LargeIndependentSets.FiniteScan.read_k line 37
  8. lemma OAI.LargeIndependentSets.FiniteScan.read_input line 41
  9. lemma OAI.LargeIndependentSets.FiniteScan.read_history line 46
  10. def OAI.LargeIndependentSets.FiniteScan.nExpr line 52
  11. def OAI.LargeIndependentSets.FiniteScan.kExpr line 53
  12. def OAI.LargeIndependentSets.FiniteScan.inputExpr line 54
  13. def OAI.LargeIndependentSets.FiniteScan.historyExpr line 55
  14. def OAI.LargeIndependentSets.FiniteScan.transitionExpr line 57
  15. lemma OAI.LargeIndependentSets.FiniteScan.transitionExpr_eval line 61
  16. lemma OAI.LargeIndependentSets.FiniteScan.nExpr_eval line 72
  17. lemma OAI.LargeIndependentSets.FiniteScan.kExpr_eval line 74
  18. lemma OAI.LargeIndependentSets.FiniteScan.inputExpr_eval line 77
  19. lemma OAI.LargeIndependentSets.FiniteScan.historyExpr_eval line 79
  20. def OAI.LargeIndependentSets.FiniteScan.countExpr line 83
  21. def OAI.LargeIndependentSets.FiniteScan.valueExpr line 84
  22. lemma OAI.LargeIndependentSets.FiniteScan.valueExpr_eval line 90
  23. lemma OAI.LargeIndependentSets.FiniteScan.body_spec line 120
  24. def OAI.LargeIndependentSets.FiniteScan.body line 128
  25. lemma OAI.LargeIndependentSets.FiniteScan.body_finiteAlphabet line 132
  26. lemma OAI.LargeIndependentSets.FiniteScan.iterate_input line 136
  27. lemma OAI.LargeIndependentSets.FiniteScan.iterate_k line 142
  28. lemma OAI.LargeIndependentSets.FiniteScan.history_prefix line 148
  29. def OAI.LargeIndependentSets.FiniteScan.output line 168
  30. lemma OAI.LargeIndependentSets.FiniteScan.output_history line 171
  31. lemma OAI.LargeIndependentSets.FiniteScan.value_le line 175
  32. lemma OAI.LargeIndependentSets.FiniteScan.bits_length_le line 185
  33. def OAI.LargeIndependentSets.FiniteScan.lengthPolynomial line 197
  34. lemma OAI.LargeIndependentSets.FiniteScan.lengthPolynomial_eval line 200
  35. def OAI.LargeIndependentSets.FiniteScan.countedInput line 204
  36. lemma OAI.LargeIndependentSets.FiniteScan.intermediate_bound line 207
  37. def OAI.LargeIndependentSets.FiniteScan.countedCertificate line 217
  38. lemma OAI.LargeIndependentSets.FiniteScan.countedCertificate_finiteAlphabet line 222
  39. lemma OAI.LargeIndependentSets.FiniteScan.words_cons line 226
  40. def OAI.LargeIndependentSets.FiniteScan.initialCount line 231
  41. def OAI.LargeIndependentSets.FiniteScan.initialValue line 232
  42. lemma OAI.LargeIndependentSets.FiniteScan.initialValue_zero line 238
  43. lemma OAI.LargeIndependentSets.FiniteScan.initialValue_succ line 241
  44. lemma OAI.LargeIndependentSets.FiniteScan.initial_spec line 256
  45. def OAI.LargeIndependentSets.FiniteScan.initialCertificate line 266
  46. lemma OAI.LargeIndependentSets.FiniteScan.initialCertificate_finiteAlphabet line 270
  47. def OAI.LargeIndependentSets.FiniteScan.certificate line 274
  48. lemma OAI.LargeIndependentSets.FiniteScan.finiteAlphabet line 278