OAI/Computability/WeisfeilerLeman/Extension.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.Compression.ConsistencyData.RawBlock line 11
  2. abbrev OAI.WLTime.Compression.ConsistencyData.RawCorner line 12
  3. def OAI.WLTime.Compression.ConsistencyData.drawing line 14
  4. def OAI.WLTime.Compression.ConsistencyData.LabelAllowed line 19
  5. def OAI.WLTime.Compression.ConsistencyData.ValidBlock line 23
  6. theorem OAI.WLTime.Compression.ConsistencyData.linkLeft_allowed line 27
  7. theorem OAI.WLTime.Compression.ConsistencyData.linkRight_allowed line 32
  8. theorem OAI.WLTime.Compression.ConsistencyData.low_allowed line 40
  9. theorem OAI.WLTime.Compression.ConsistencyData.high_allowed line 51
  10. def OAI.WLTime.Compression.ConsistencyData.alignedLabel line 62
  11. theorem OAI.WLTime.Compression.ConsistencyData.alignedLabel_sides line 68
  12. theorem OAI.WLTime.Compression.ConsistencyData.corner_type_reachable line 80
  13. structure OAI.WLTime.Compression.ConsistencyData.WrapData line 96
  14. theorem OAI.WLTime.Compression.ConsistencyData.wrapData_exists line 109
  15. abbrev OAI.WLTime.Compression.ConsistencyData.WrapData.rootType line 122
  16. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.address_unique line 124
  17. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.type_reachable line 129
  18. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.rootfree_allowed line 138
  19. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.type_low_high line 171
  20. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.type_reachable_blocks line 175
  21. def OAI.WLTime.Compression.ConsistencyData.WrapData.changedAddress line 183
  22. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.changedAddress_reads line 190
  23. def OAI.WLTime.Compression.ConsistencyData.WrapData.reframe line 225
  24. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.roots_connected line 237
  25. structure OAI.WLTime.Compression.ConsistencyData.ShiftChoice line 261
  26. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.values line 267
  27. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.AtAddress line 270
  28. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.atAddress line 273
  29. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.atAddress_mem line 277
  30. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.withReal line 281
  31. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.withScalar line 284
  32. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.withReal_mem line 287
  33. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.withScalar_mem line 297
  34. def OAI.WLTime.Compression.ConsistencyData.ShiftChoice.Admissible line 307
  35. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.admissible_of_one line 311
  36. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.admissible_exists line 319
  37. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.changedAddress_both_real line 335
  38. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.changedAddress_neither_real line 343
  39. theorem OAI.WLTime.Compression.ConsistencyData.WrapData.changedAddress_new_real line 351
  40. theorem OAI.WLTime.Compression.ConsistencyData.shifts_eq_on_rootfree_component line 363
  41. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.values_internal line 385
  42. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.values_solves line 394
  43. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.newly_rooted_preimage line 398
  44. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.newly_rooted_image line 427
  45. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.extend_on_wrapping line 449
  46. theorem OAI.WLTime.Compression.ConsistencyData.ShiftChoice.restrict_on_wrapping line 500