OAI/Computability/WeisfeilerLeman/Padding.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.Marking.degree_detect_base line 10
  2. def OAI.WLTime.Marking.basePosition line 41
  3. theorem OAI.WLTime.Marking.basePosition_update line 46
  4. theorem OAI.WLTime.Marking.wins_bases line 55
  5. def OAI.WLTime.Compression.ConsistencyData.baseEquiv line 111
  6. theorem OAI.WLTime.Compression.ConsistencyData.baseEquiv_block line 116
  7. def OAI.WLTime.Compression.ConsistencyData.blockCode line 119
  8. theorem OAI.WLTime.Compression.ConsistencyData.blockCode_injective line 122
  9. theorem OAI.WLTime.Compression.ConsistencyData.blockCode_pos line 128
  10. def OAI.WLTime.Compression.ConsistencyData.markCount line 130
  11. abbrev OAI.WLTime.Compression.ConsistencyData.MarkedVertex line 133
  12. def OAI.WLTime.Compression.ConsistencyData.markedGraph line 136
  13. theorem OAI.WLTime.Compression.ConsistencyData.marked_diameter_two line 140
  14. def OAI.WLTime.Compression.ConsistencyData.markedEquiv line 145
  15. theorem OAI.WLTime.Compression.ConsistencyData.card_marked_eq line 149
  16. theorem OAI.WLTime.Compression.ConsistencyData.two_le_card_base line 153
  17. theorem OAI.WLTime.Compression.ConsistencyData.marked_wins_iff_ac line 168
  18. def OAI.WLTime.Compression.BlockName.equivProduct line 189
  19. theorem OAI.WLTime.Compression.BlockName.card line 200
  20. def OAI.WLTime.Compression.ConsistencyData.blockCoefficient line 211
  21. theorem OAI.WLTime.Compression.ConsistencyData.card_blocks_le line 214
  22. theorem OAI.WLTime.Compression.ConsistencyData.footprint_card_le line 226
  23. theorem OAI.WLTime.Compression.ConsistencyData.card_readValue_le line 237
  24. theorem OAI.WLTime.Compression.ConsistencyData.card_legal_le line 247
  25. theorem OAI.WLTime.Compression.ConsistencyData.card_bases_le line 270
  26. theorem OAI.WLTime.Compression.ConsistencyData.card_blocks_le_bases line 280
  27. theorem OAI.WLTime.Compression.ConsistencyData.marked_order_cubic line 284
  28. theorem OAI.WLTime.Compression.ConsistencyData.marked_order_six line 296
  29. def OAI.WLTime.Graph.ofSimple line 312
  30. def OAI.WLTime.Graph.simple line 317
  31. theorem OAI.WLTime.Graph.ofSimple_adj line 322
  32. theorem OAI.WLTime.Graph.ofSimple_diameter line 327
  33. theorem OAI.WLTime.pebble_iff_wins line 338
  34. theorem OAI.WLTime.wins_ofSimple_iff line 366
  35. theorem OAI.WLTime.Compression.ConsistencyData.marked_padding_order line 389
  36. theorem OAI.WLTime.Compression.ConsistencyData.matrix_compression line 393
  37. theorem OAI.WLTime.Compression.ConsistencyData.matrix_compression_six line 417