OAI/Computability/WeisfeilerLeman/Predicates.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.NatCode.Expr.bind line 11
  2. theorem OAI.WLTime.NatCode.Expr.bind_eval line 17
  3. theorem OAI.WLTime.NatCode.Expr.bounded_mono line 24
  4. inductive OAI.WLTime.NatCode.Predicate line 32
  5. def OAI.WLTime.NatCode.Predicate.Holds line 43
  6. instance OAI.WLTime.NatCode.Predicate.decidableHolds line 51
  7. def OAI.WLTime.NatCode.Predicate.code line 56
  8. theorem OAI.WLTime.NatCode.Predicate.code_eval line 64
  9. theorem OAI.WLTime.NatCode.Predicate.code_le_one line 82
  10. def OAI.WLTime.NatCode.Predicate.Bounded line 85
  11. theorem OAI.WLTime.NatCode.Predicate.code_bounded line 92
  12. def OAI.WLTime.NatCode.Predicate.disj line 115
  13. theorem OAI.WLTime.NatCode.Predicate.holds_disj line 116
  14. def OAI.WLTime.NatCode.Predicate.all line 120
  15. def OAI.WLTime.NatCode.Predicate.any line 121
  16. theorem OAI.WLTime.NatCode.Predicate.holds_all line 123
  17. theorem OAI.WLTime.NatCode.Predicate.holds_any line 131
  18. def OAI.WLTime.Compression.ReadoutName.encode line 148
  19. theorem OAI.WLTime.Compression.ReadoutName.encode_injective line 152
  20. structure OAI.WLTime.Compression.FormalName line 162
  21. def OAI.WLTime.Compression.FormalName.eval line 169
  22. def OAI.WLTime.Compression.FormalName.equal line 171
  23. theorem OAI.WLTime.Compression.FormalName.equal_holds line 176
  24. abbrev OAI.WLTime.Compression.ConsistencyData.BlockTag line 184
  25. def OAI.WLTime.Compression.ConsistencyData.makeBlock line 186
  26. def OAI.WLTime.Compression.ConsistencyData.fixedTags line 191
  27. def OAI.WLTime.Compression.ConsistencyData.footprintList line 196
  28. theorem OAI.WLTime.Compression.ConsistencyData.mem_footprintList line 205
  29. theorem OAI.WLTime.Compression.ConsistencyData.footprintList_tags line 212
  30. theorem OAI.WLTime.Compression.ConsistencyData.tagSupported_iff_fixed line 216
  31. def OAI.WLTime.Compression.ConsistencyData.fixedForm line 226
  32. def OAI.WLTime.Compression.ConsistencyData.fixedBias line 232
  33. theorem OAI.WLTime.Compression.ConsistencyData.blockForm_fixed line 236
  34. theorem OAI.WLTime.Compression.ConsistencyData.blockBias_fixed line 241
  35. def OAI.WLTime.Compression.ConsistencyData.FixedLegal line 245
  36. theorem OAI.WLTime.Compression.ConsistencyData.descriptorValid_fixed line 248
  37. def OAI.WLTime.Compression.ConsistencyData.labelPredicate line 265
  38. def OAI.WLTime.Compression.ConsistencyData.blockPredicate line 269
  39. def OAI.WLTime.Compression.ConsistencyData.validPredicate line 274
  40. theorem OAI.WLTime.Compression.ConsistencyData.blockPredicate_holds line 279
  41. theorem OAI.WLTime.Compression.ConsistencyData.validPredicate_holds line 290
  42. def OAI.WLTime.Compression.ConsistencyData.matchCode line 299
  43. theorem OAI.WLTime.Compression.ConsistencyData.matchCode_eval line 302
  44. def OAI.WLTime.Compression.ConsistencyData.formalFootprint line 314
  45. theorem OAI.WLTime.Compression.ConsistencyData.formalFootprint_correct line 322
  46. def OAI.WLTime.Compression.ConsistencyData.valueCode line 337
  47. theorem OAI.WLTime.Compression.ConsistencyData.valueCode_eq_iff line 340
  48. def OAI.WLTime.Compression.ConsistencyData.overlapPredicate line 346
  49. def OAI.WLTime.Compression.ConsistencyData.agreePredicate line 350
  50. theorem OAI.WLTime.Compression.ConsistencyData.overlapPredicate_holds line 356
  51. theorem OAI.WLTime.Compression.ConsistencyData.agreePredicate_holds line 369
  52. theorem OAI.WLTime.Compression.ReadoutName.encode_tag line 393
  53. theorem OAI.WLTime.Compression.ConsistencyData.overlapPredicate_correct line 399
  54. theorem OAI.WLTime.Compression.ConsistencyData.agreePredicate_correct line 425
  55. theorem OAI.WLTime.Compression.ConsistencyData.makeBlock_eq_iff line 459
  56. def OAI.WLTime.Compression.ConsistencyData.sameBlockPredicate line 465
  57. theorem OAI.WLTime.Compression.ConsistencyData.sameBlockPredicate_holds line 470
  58. def OAI.WLTime.Compression.ConsistencyData.RawAdjacent line 478
  59. theorem OAI.WLTime.Compression.ConsistencyData.descriptor_adjacent line 482
  60. def OAI.WLTime.Compression.ConsistencyData.adjacencyPredicate line 506
  61. theorem OAI.WLTime.Compression.ConsistencyData.adjacencyPredicate_correct line 513