OAI/Combinatorics/IndependentSets/Reduction/StoredFloyd.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.wordValue_words line 8
  2. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.words_congr line 14
  3. structure OAI.LargeIndependentSets.StoredFloyd.State line 26
  4. def OAI.LargeIndependentSets.StoredFloyd.entry line 31
  5. lemma OAI.LargeIndependentSets.StoredFloyd.entry_fin line 34
  6. def OAI.LargeIndependentSets.StoredFloyd.State.value line 37
  7. def OAI.LargeIndependentSets.StoredFloyd.State.bits line 41
  8. def OAI.LargeIndependentSets.StoredFloyd.State.step line 44
  9. lemma OAI.LargeIndependentSets.StoredFloyd.read_n line 49
  10. lemma OAI.LargeIndependentSets.StoredFloyd.read_k line 52
  11. lemma OAI.LargeIndependentSets.StoredFloyd.read_cell line 56
  12. def OAI.LargeIndependentSets.StoredFloyd.sizeExpr line 71
  13. def OAI.LargeIndependentSets.StoredFloyd.pivotExpr line 72
  14. def OAI.LargeIndependentSets.StoredFloyd.cellExpr line 73
  15. def OAI.LargeIndependentSets.StoredFloyd.minExpr line 75
  16. def OAI.LargeIndependentSets.StoredFloyd.countExpr line 76
  17. def OAI.LargeIndependentSets.StoredFloyd.rowExpr line 77
  18. def OAI.LargeIndependentSets.StoredFloyd.colExpr line 78
  19. def OAI.LargeIndependentSets.StoredFloyd.valueExpr line 80
  20. lemma OAI.LargeIndependentSets.StoredFloyd.sizeExpr_eval line 88
  21. lemma OAI.LargeIndependentSets.StoredFloyd.pivotExpr_eval line 90
  22. lemma OAI.LargeIndependentSets.StoredFloyd.cellExpr_eval line 92
  23. lemma OAI.LargeIndependentSets.StoredFloyd.minExpr_eval line 96
  24. lemma OAI.LargeIndependentSets.StoredFloyd.countExpr_eval line 99
  25. lemma OAI.LargeIndependentSets.StoredFloyd.valueExpr_eval line 102
  26. lemma OAI.LargeIndependentSets.StoredFloyd.body_spec line 134
  27. def OAI.LargeIndependentSets.StoredFloyd.body line 141
  28. lemma OAI.LargeIndependentSets.StoredFloyd.body_finiteAlphabet line 145