OAI/Combinatorics/IndependentSets/Encoding/BinaryNameTables.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.BinaryNames.raw line 10
  2. lemma OAI.LargeIndependentSets.BinaryNames.raw_out line 12
  3. lemma OAI.LargeIndependentSets.BinaryNames.end_exists line 15
  4. def OAI.LargeIndependentSets.BinaryNames.nameLength line 18
  5. lemma OAI.LargeIndependentSets.BinaryNames.nameLength_le line 20
  6. lemma OAI.LargeIndependentSets.BinaryNames.nameLength_end line 22
  7. lemma OAI.LargeIndependentSets.BinaryNames.nameLength_before line 24
  8. def OAI.LargeIndependentSets.BinaryNames.payload line 29
  9. lemma OAI.LargeIndependentSets.BinaryNames.payload_eq_iff line 32
  10. lemma OAI.LargeIndependentSets.BinaryNames.key_exists line 49
  11. def OAI.LargeIndependentSets.BinaryNames.key line 53
  12. lemma OAI.LargeIndependentSets.BinaryNames.key_le line 54
  13. lemma OAI.LargeIndependentSets.BinaryNames.key_payload line 55
  14. lemma OAI.LargeIndependentSets.BinaryNames.key_eq line 58
  15. def OAI.LargeIndependentSets.BinaryNames.next line 66
  16. lemma OAI.LargeIndependentSets.BinaryNames.raw_middle line 68
  17. lemma OAI.LargeIndependentSets.BinaryNames.frame_eq line 76
  18. lemma OAI.LargeIndependentSets.BinaryNames.literal_marker line 81
  19. lemma OAI.LargeIndependentSets.BinaryNames.literal_payload line 87
  20. lemma OAI.LargeIndependentSets.BinaryNames.nameLength_literal line 94
  21. lemma OAI.LargeIndependentSets.BinaryNames.payload_literal line 108
  22. lemma OAI.LargeIndependentSets.BinaryNames.next_literal line 122
  23. def OAI.LargeIndependentSets.BinaryNames.rawExpr line 128
  24. lemma OAI.LargeIndependentSets.BinaryNames.rawExpr_eval line 131
  25. def OAI.LargeIndependentSets.BinaryNames.nameLengthExpr line 137
  26. lemma OAI.LargeIndependentSets.BinaryNames.nameLengthExpr_eval line 140
  27. def OAI.LargeIndependentSets.BinaryNames.payloadEqExpr line 149
  28. lemma OAI.LargeIndependentSets.BinaryNames.payloadEqExpr_eval line 154
  29. def OAI.LargeIndependentSets.BinaryNames.minExpr line 173
  30. lemma OAI.LargeIndependentSets.BinaryNames.minExpr_eval line 174
  31. def OAI.LargeIndependentSets.BinaryNames.keyExpr line 178
  32. lemma OAI.LargeIndependentSets.BinaryNames.keyExpr_eval line 181
  33. def OAI.LargeIndependentSets.BinaryNames.nextExpr line 198
  34. lemma OAI.LargeIndependentSets.BinaryNames.nextExpr_eval line 199