theorem AP.AState.aHwsDisj_of_tr {s s₁ : State} {p : PointZ} {fsp : FSP} [hs : AState s] (h₁ : s₁.aHwsDisj fsp.next) (h₂ : sys.tr s p = some s₁) (h₃ : s.aPos ∉ fsp.get 0) : s.aHwsDisj fsp

theorem AP.AState.aHwsDisj_nbhd_pw {s : State} {fsp : FSP} [hs : AState s] (h : s.aHwsDisj fsp) : s.aHwsDisj (fsp.insertSet 3 (Point.nbhd s.aPos ↑s.pw).toSet)

theorem AP.DState.aHwsDisj_nbhd_pw {s : State} {fsp : FSP} [hs : DState s] (h : s.aHwsDisj fsp) : s.aHwsDisj (fsp.insertSet 4 (Point.nbhd s.aPos ↑s.pw).toSet)