OAI/Computability/WeisfeilerLeman/Wrapping.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.Compression.walkWeight_ne_zero_edge line 11
  2. theorem OAI.WLTime.Compression.closed_row_weights_eq line 22
  3. theorem OAI.WLTime.Compression.wrapping_all_rows line 37
  4. theorem OAI.WLTime.Compression.wrapping_card_lower line 51
  5. theorem OAI.WLTime.Compression.unique_block_per_row line 68
  6. theorem OAI.WLTime.Compression.boundary_label_recovery line 89
  7. theorem OAI.WLTime.Compression.difference_card_le_one line 105
  8. theorem OAI.WLTime.Compression.recovered_addresses_agree line 113
  9. theorem OAI.WLTime.Compression.rotate_castSucc line 154
  10. theorem OAI.WLTime.Compression.rotate_ne_self line 157
  11. theorem OAI.WLTime.Compression.rotate_no_two_cycle line 168
  12. structure OAI.WLTime.Compression.BlockDrawing line 178
  13. def OAI.WLTime.Compression.BlockDrawing.Edge line 190
  14. def OAI.WLTime.Compression.BlockDrawing.graph line 195
  15. def OAI.WLTime.Compression.BlockDrawing.rowMark line 202
  16. theorem OAI.WLTime.Compression.BlockDrawing.rowMark_symm line 206
  17. theorem OAI.WLTime.Compression.BlockDrawing.rowMark_horizontal line 210
  18. theorem OAI.WLTime.Compression.BlockDrawing.rowMark_zero_of_boundary_eq line 219
  19. def OAI.WLTime.Compression.BlockDrawing.boundaryMark line 226
  20. theorem OAI.WLTime.Compression.BlockDrawing.row_balance_horizontal line 229
  21. theorem OAI.WLTime.Compression.BlockDrawing.row_balance_vertical line 239
  22. theorem OAI.WLTime.Compression.BlockDrawing.row_balance_edge line 248
  23. theorem OAI.WLTime.Compression.BlockDrawing.row_balance line 257
  24. theorem OAI.WLTime.Compression.BlockDrawing.row_support_edge line 266
  25. theorem OAI.WLTime.Compression.BlockDrawing.row_support line 277
  26. def OAI.WLTime.Compression.BlockDrawing.Wraps line 283
  27. theorem OAI.WLTime.Compression.BlockDrawing.wraps_card line 286
  28. theorem OAI.WLTime.Compression.BlockDrawing.wraps_unique_row line 292
  29. theorem OAI.WLTime.Compression.BlockDrawing.edge_reachable line 307
  30. theorem OAI.WLTime.Compression.BlockDrawing.low_reachable line 313
  31. theorem OAI.WLTime.Compression.BlockDrawing.high_reachable line 319
  32. theorem OAI.WLTime.Compression.BlockDrawing.edge_left_reachable line 323
  33. theorem OAI.WLTime.Compression.BlockDrawing.edge_right_reachable line 330
  34. theorem OAI.WLTime.Compression.BlockDrawing.row_weight_nonzero_has_block line 334
  35. theorem OAI.WLTime.Compression.BlockDrawing.wraps_connected line 351
  36. def OAI.WLTime.Compression.BlockDrawing.labeledBoundary line 369
  37. theorem OAI.WLTime.Compression.BlockDrawing.side_label_low line 373
  38. theorem OAI.WLTime.Compression.BlockDrawing.side_label_high line 378
  39. theorem OAI.WLTime.Compression.BlockDrawing.labeled_balance_horizontal line 382
  40. theorem OAI.WLTime.Compression.BlockDrawing.labeled_balance_vertical line 403
  41. theorem OAI.WLTime.Compression.BlockDrawing.labeled_balance_edge line 414
  42. theorem OAI.WLTime.Compression.BlockDrawing.labeled_balance line 433
  43. theorem OAI.WLTime.Compression.BlockDrawing.wrapping_labels_join line 447