OAI/Combinatorics/PolynomialVacuum/Cylinder/OpenIce.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumCylinder.activeInside line 9
  2. theorem OAI.PolynomialVacuumCylinder.OpenIce.occupied line 16
  3. def OAI.PolynomialVacuumCylinder.OpenIce.enter line 24
  4. def OAI.PolynomialVacuumCylinder.OpenIce.exit line 25
  5. theorem OAI.PolynomialVacuumCylinder.OpenIce.distinct line 27
  6. theorem OAI.PolynomialVacuumCylinder.OpenIce.at_slot line 30
  7. theorem OAI.PolynomialVacuumCylinder.OpenIce.at_enter line 34
  8. theorem OAI.PolynomialVacuumCylinder.OpenIce.at_exit line 36
  9. theorem OAI.PolynomialVacuumCylinder.OpenIce.matching line 39
  10. def OAI.PolynomialVacuumCylinder.OpenIce.network line 47
  11. theorem OAI.PolynomialVacuumCylinder.OpenIce.exit_outside_domain line 56
  12. theorem OAI.PolynomialVacuumCylinder.OpenIce.enter_outside_domain line 70