OAI/Combinatorics/IndependentSets/Reduction/FloydLoop.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LargeIndependentSets.StoredFloyd.Input line 13
  2. def OAI.LargeIndependentSets.StoredFloyd.Input.initial line 17
  3. def OAI.LargeIndependentSets.StoredFloyd.Input.bits line 18
  4. def OAI.LargeIndependentSets.StoredFloyd.Input.output line 21
  5. lemma OAI.LargeIndependentSets.StoredFloyd.run_append line 23
  6. lemma OAI.LargeIndependentSets.StoredFloyd.iterate_initial line 29
  7. lemma OAI.LargeIndependentSets.StoredFloyd.iterate_output line 42
  8. lemma OAI.LargeIndependentSets.StoredFloyd.entry_le line 47
  9. lemma OAI.LargeIndependentSets.StoredFloyd.value_le line 55
  10. lemma OAI.LargeIndependentSets.StoredFloyd.bits_length_le line 63
  11. def OAI.LargeIndependentSets.StoredFloyd.lengthPolynomial line 75
  12. lemma OAI.LargeIndependentSets.StoredFloyd.lengthPolynomial_eval line 78
  13. lemma OAI.LargeIndependentSets.StoredFloyd.intermediate_bound line 81
  14. def OAI.LargeIndependentSets.StoredFloyd.rawCertificate line 90
  15. def OAI.LargeIndependentSets.StoredFloyd.certificate line 96
  16. lemma OAI.LargeIndependentSets.StoredFloyd.certificate_finiteAlphabet line 105
  17. lemma OAI.LargeIndependentSets.StoredFloyd.output_threshold line 110
  18. structure OAI.LargeIndependentSets.FloydCarry.State line 122
  19. def OAI.LargeIndependentSets.FloydCarry.State.value line 126
  20. def OAI.LargeIndependentSets.FloydCarry.State.count line 131
  21. def OAI.LargeIndependentSets.FloydCarry.State.bits line 132
  22. def OAI.LargeIndependentSets.FloydCarry.State.step line 134
  23. lemma OAI.LargeIndependentSets.FloydCarry.read_core line 136
  24. lemma OAI.LargeIndependentSets.FloydCarry.read_n line 140
  25. lemma OAI.LargeIndependentSets.FloydCarry.read_k line 142
  26. lemma OAI.LargeIndependentSets.FloydCarry.read_count line 144
  27. lemma OAI.LargeIndependentSets.FloydCarry.read_payload line 148
  28. lemma OAI.LargeIndependentSets.FloydCarry.read_cell line 155
  29. lemma OAI.LargeIndependentSets.FloydCarry.sizeExpr_eval line 165
  30. lemma OAI.LargeIndependentSets.FloydCarry.pivotExpr_eval line 167
  31. lemma OAI.LargeIndependentSets.FloydCarry.coreCount_eval line 169
  32. def OAI.LargeIndependentSets.FloydCarry.payloadCountExpr line 172
  33. def OAI.LargeIndependentSets.FloydCarry.countExpr line 174
  34. def OAI.LargeIndependentSets.FloydCarry.valueExpr line 176
  35. lemma OAI.LargeIndependentSets.FloydCarry.coreValue_eval line 179
  36. lemma OAI.LargeIndependentSets.FloydCarry.payloadCount_eval line 206
  37. lemma OAI.LargeIndependentSets.FloydCarry.countExpr_eval line 208
  38. lemma OAI.LargeIndependentSets.FloydCarry.valueExpr_eval line 211
  39. lemma OAI.LargeIndependentSets.FloydCarry.body_spec line 221
  40. def OAI.LargeIndependentSets.FloydCarry.body line 227
  41. lemma OAI.LargeIndependentSets.FloydCarry.body_finiteAlphabet line 229
  42. structure OAI.LargeIndependentSets.FloydCarry.Input line 232
  43. def OAI.LargeIndependentSets.FloydCarry.Input.initial line 236
  44. def OAI.LargeIndependentSets.FloydCarry.Input.count line 237
  45. def OAI.LargeIndependentSets.FloydCarry.Input.bits line 238
  46. def OAI.LargeIndependentSets.FloydCarry.Input.output line 241
  47. lemma OAI.LargeIndependentSets.FloydCarry.iterate_pair line 243
  48. lemma OAI.LargeIndependentSets.FloydCarry.iterate_output line 249
  49. lemma OAI.LargeIndependentSets.FloydCarry.wordValue_le_length line 254
  50. lemma OAI.LargeIndependentSets.FloydCarry.initial_length_le line 264
  51. lemma OAI.LargeIndependentSets.FloydCarry.payload_length_le line 267
  52. lemma OAI.LargeIndependentSets.FloydCarry.payload_value_le line 272
  53. lemma OAI.LargeIndependentSets.FloydCarry.bits_length_le line 281
  54. def OAI.LargeIndependentSets.FloydCarry.lengthPolynomial line 302
  55. lemma OAI.LargeIndependentSets.FloydCarry.lengthPolynomial_eval line 305
  56. lemma OAI.LargeIndependentSets.FloydCarry.intermediate_bound line 309
  57. def OAI.LargeIndependentSets.FloydCarry.rawCertificate line 322
  58. def OAI.LargeIndependentSets.FloydCarry.certificate line 328
  59. lemma OAI.LargeIndependentSets.FloydCarry.certificate_finiteAlphabet line 336