OAI/Computability/WeisfeilerLeman/Pebbles.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.Pebble.Position line 9
  2. def OAI.WLTime.Pebble.Position.Sub line 11
  3. def OAI.WLTime.Pebble.Position.PartialIso line 14
  4. structure OAI.WLTime.Pebble.Invariant line 20
  5. def OAI.WLTime.Pebble.Wins line 28
  6. theorem OAI.WLTime.Pebble.Position.Sub.refl line 35
  7. theorem OAI.WLTime.Pebble.Position.Sub.trans line 37
  8. theorem OAI.WLTime.Pebble.Position.Sub.mark line 45
  9. theorem OAI.WLTime.Pebble.Position.erase_sub line 51
  10. theorem OAI.WLTime.Pebble.Wins.forget line 63
  11. theorem OAI.WLTime.Pebble.Wins.atomic line 67
  12. theorem OAI.WLTime.Pebble.Wins.extend line 71
  13. theorem OAI.WLTime.Pebble.Wins.erase line 77
  14. theorem OAI.WLTime.Pebble.Wins.rename line 80
  15. def OAI.WLTime.Pebble.active line 114
  16. theorem OAI.WLTime.Pebble.mem_active line 122
  17. theorem OAI.WLTime.Pebble.active_mono line 136
  18. theorem OAI.WLTime.Pebble.active_card_le line 142
  19. theorem OAI.WLTime.Pebble.active_card line 170
  20. theorem OAI.WLTime.Pebble.active_card_free line 174
  21. theorem OAI.WLTime.Pebble.active_update line 186
  22. structure OAI.WLTime.Pebble.ExactLocalSystem line 208
  23. def OAI.WLTime.Pebble.ExactLocalSystem.Safe line 232
  24. def OAI.WLTime.Pebble.ExactLocalSystem.invariant line 235
  25. theorem OAI.WLTime.Pebble.ExactLocalSystem.wins_empty line 287
  26. theorem OAI.WLTime.Pebble.Wins.replace line 306
  27. theorem OAI.WLTime.Pebble.Wins.realize line 328
  28. def OAI.WLTime.Pebble.degree line 364
  29. theorem OAI.WLTime.Pebble.Wins.neighborhood_bijection line 367
  30. theorem OAI.WLTime.Pebble.Wins.degree_eq line 393