OAI/Combinatorics/PolynomialVacuum/Cylinder/NetworkFromFlow.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumCylinder.edgeOf_reverse line 9
  2. theorem OAI.PolynomialVacuumCylinder.dartSign_reverse line 13
  3. theorem OAI.PolynomialVacuumCylinder.orientedFlow_reverse line 17
  4. def OAI.PolynomialVacuumCylinder.LocalIce line 23
  5. def OAI.PolynomialVacuumCylinder.activeSites line 28
  6. theorem OAI.PolynomialVacuumCylinder.mem_activeSites line 31
  7. theorem OAI.PolynomialVacuumCylinder.IceNetwork.occupied line 42
  8. def OAI.PolynomialVacuumCylinder.IceNetwork.enter line 49
  9. def OAI.PolynomialVacuumCylinder.IceNetwork.exit line 50
  10. theorem OAI.PolynomialVacuumCylinder.IceNetwork.distinct line 52
  11. theorem OAI.PolynomialVacuumCylinder.IceNetwork.at_slot line 55
  12. theorem OAI.PolynomialVacuumCylinder.IceNetwork.at_enter line 59
  13. theorem OAI.PolynomialVacuumCylinder.IceNetwork.at_exit line 61
  14. theorem OAI.PolynomialVacuumCylinder.IceNetwork.enter_of_neg line 64
  15. theorem OAI.PolynomialVacuumCylinder.IceNetwork.exit_of_pos line 69
  16. def OAI.PolynomialVacuumCylinder.IceNetwork.next line 74
  17. def OAI.PolynomialVacuumCylinder.IceNetwork.prev line 80
  18. theorem OAI.PolynomialVacuumCylinder.IceNetwork.enter_next line 86
  19. theorem OAI.PolynomialVacuumCylinder.IceNetwork.exit_prev line 91
  20. theorem OAI.PolynomialVacuumCylinder.IceNetwork.prev_next line 96
  21. theorem OAI.PolynomialVacuumCylinder.IceNetwork.next_prev line 101
  22. def OAI.PolynomialVacuumCylinder.IceNetwork.permutation line 106
  23. def OAI.PolynomialVacuumCylinder.IceNetwork.network line 109