OAI/Computability/WeisfeilerLeman/Readouts.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.Compression.BlockDrawing.seam_potential_exists line 12
  2. inductive OAI.WLTime.Compression.ReadoutName line 31
  3. abbrev OAI.WLTime.Compression.RawName line 36
  4. abbrev OAI.WLTime.Compression.ConsistencyData.ReadValue line 42
  5. abbrev OAI.WLTime.Compression.ConsistencyData.Readouts line 46
  6. abbrev OAI.WLTime.Compression.ConsistencyData.Potentials line 47
  7. def OAI.WLTime.Compression.ConsistencyData.seam line 49
  8. def OAI.WLTime.Compression.ConsistencyData.footprint line 51
  9. def OAI.WLTime.Compression.ConsistencyData.AgreeOn line 63
  10. theorem OAI.WLTime.Compression.ConsistencyData.AgreeOn.refl line 70
  11. theorem OAI.WLTime.Compression.ConsistencyData.AgreeOn.symm line 71
  12. theorem OAI.WLTime.Compression.ConsistencyData.AgreeOn.trans line 72
  13. theorem OAI.WLTime.Compression.ConsistencyData.AgreeOn.mono line 74
  14. def OAI.WLTime.Compression.ConsistencyData.fromPotentials line 78
  15. def OAI.WLTime.Compression.ConsistencyData.adjustPotentials line 85
  16. theorem OAI.WLTime.Compression.ConsistencyData.adjust_horizontal line 90
  17. theorem OAI.WLTime.Compression.ConsistencyData.adjust_vertical line 99
  18. theorem OAI.WLTime.Compression.ConsistencyData.adjust_nonwrapping line 114
  19. theorem OAI.WLTime.Compression.ConsistencyData.fromPotentials_agree line 154
  20. def OAI.WLTime.Compression.ConsistencyData.OffsetFamily line 180
  21. theorem OAI.WLTime.Compression.ConsistencyData.offset_nonempty line 185
  22. theorem OAI.WLTime.Compression.ConsistencyData.offset_extend line 193
  23. theorem OAI.WLTime.Compression.ConsistencyData.offset_restrict line 227
  24. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 266) line 266
  25. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 268) line 268
  26. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 270) line 270
  27. def OAI.WLTime.Compression.ConsistencyData.blockForm line 273
  28. def OAI.WLTime.Compression.ConsistencyData.blockBias line 286
  29. def OAI.WLTime.Compression.ConsistencyData.blockSpace line 290
  30. def OAI.WLTime.Compression.ConsistencyData.atBlock line 297
  31. theorem OAI.WLTime.Compression.ConsistencyData.atBlock_apply line 303
  32. theorem OAI.WLTime.Compression.ConsistencyData.blockForm_congr line 310
  33. theorem OAI.WLTime.Compression.ConsistencyData.blockForm_atBlock line 326
  34. abbrev OAI.WLTime.Compression.ConsistencyData.Legal line 331
  35. def OAI.WLTime.Compression.ConsistencyData.zeroValuation line 335
  36. def OAI.WLTime.Compression.ConsistencyData.translate line 339
  37. theorem OAI.WLTime.Compression.ConsistencyData.fromPotentials_legal line 349
  38. theorem OAI.WLTime.Compression.ConsistencyData.offset_legal line 360
  39. theorem OAI.WLTime.Compression.ConsistencyData.legal_nonempty line 371