OAI/Computability/WeisfeilerLeman/Gadgets.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.Pebble.Position.map line 11
  2. theorem OAI.WLTime.Pebble.Position.map_none line 14
  3. theorem OAI.WLTime.Pebble.Position.map_update line 17
  4. theorem OAI.WLTime.Pebble.Position.map_inverse line 26
  5. theorem OAI.WLTime.Pebble.Position.map_apply_eq_some line 31
  6. theorem OAI.WLTime.Pebble.Position.map_apply_eq_none line 40
  7. theorem OAI.WLTime.Pebble.Wins.transport line 45
  8. abbrev OAI.WLTime.Compression.ConsistencyData.Block line 82
  9. abbrev OAI.WLTime.Compression.ConsistencyData.Vertex line 83
  10. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 85) line 85
  11. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 89) line 89
  12. abbrev OAI.WLTime.Compression.ConsistencyData.Vertex.read line 97
  13. theorem OAI.WLTime.Compression.ConsistencyData.Vertex.ext line 99
  14. def OAI.WLTime.Compression.ConsistencyData.valuationGraph line 111
  15. def OAI.WLTime.Compression.ConsistencyData.Maps line 120
  16. theorem OAI.WLTime.Compression.ConsistencyData.atBlock_congr line 123
  17. theorem OAI.WLTime.Compression.ConsistencyData.maps_read line 133
  18. theorem OAI.WLTime.Compression.ConsistencyData.maps_atomic line 139
  19. def OAI.WLTime.Compression.ConsistencyData.rawSet line 172
  20. theorem OAI.WLTime.Compression.ConsistencyData.rawSet_card line 174
  21. theorem OAI.WLTime.Compression.ConsistencyData.rawSet_mono line 178
  22. theorem OAI.WLTime.Compression.ConsistencyData.mem_rawSet line 182
  23. theorem OAI.WLTime.Compression.ConsistencyData.rawSet_valid line 193
  24. def OAI.WLTime.Compression.ConsistencyData.localOffset line 200
  25. def OAI.WLTime.Compression.ConsistencyData.assembleTranslations line 208
  26. theorem OAI.WLTime.Compression.ConsistencyData.assembleTranslations_maps line 213
  27. def OAI.WLTime.Compression.ConsistencyData.valuationSystem line 219
  28. theorem OAI.WLTime.Compression.ConsistencyData.ac_colored_wins line 253
  29. def OAI.WLTime.Compression.ConsistencyData.zeroVertex line 266
  30. theorem OAI.WLTime.Compression.ConsistencyData.zeroVertex_read line 268
  31. def OAI.WLTime.Compression.ConsistencyData.queryPosition line 270
  32. def OAI.WLTime.Compression.ConsistencyData.Queried line 274
  33. theorem OAI.WLTime.Compression.ConsistencyData.queried_color line 278
  34. theorem OAI.WLTime.Compression.ConsistencyData.queried_exists line 282
  35. theorem OAI.WLTime.Compression.ConsistencyData.queried_change_one line 313
  36. theorem OAI.WLTime.Compression.ConsistencyData.queried_transform line 346
  37. theorem OAI.WLTime.Compression.ConsistencyData.queried_legal line 392
  38. theorem OAI.WLTime.Compression.ConsistencyData.queried_shared line 398
  39. def OAI.WLTime.Compression.ConsistencyData.AddressAllowed line 410
  40. abbrev OAI.WLTime.Compression.ConsistencyData.horizontalName line 413
  41. abbrev OAI.WLTime.Compression.ConsistencyData.verticalName line 417
  42. def OAI.WLTime.Compression.ConsistencyData.matchedAddress line 420
  43. def OAI.WLTime.Compression.ConsistencyData.siteRing line 423
  44. def OAI.WLTime.Compression.ConsistencyData.squareRing line 427
  45. theorem OAI.WLTime.Compression.ConsistencyData.leftAddress_allowed line 431
  46. theorem OAI.WLTime.Compression.ConsistencyData.rightAddress_allowed line 435
  47. def OAI.WLTime.Compression.ConsistencyData.horizontalSum line 439
  48. theorem OAI.WLTime.Compression.ConsistencyData.squareRing_injective line 442
  49. theorem OAI.WLTime.Compression.ConsistencyData.squareRing_vertical line 447
  50. theorem OAI.WLTime.Compression.ConsistencyData.squareRing_equation line 458
  51. theorem OAI.WLTime.Compression.ConsistencyData.ring_transfer_left line 482
  52. theorem OAI.WLTime.Compression.ConsistencyData.ring_transfer_right line 507