noncomputable def AP.State.aProx (s s₁ : State) : Set' PointZ

Equations

• s.aProx s₁ = Set'.ofSet {p : PointZ | AP.sys.WF s ∧ AP.sys.Reachable s s₁ ∧ (∃ (ps : List PointZ) (s₂ : AP.State), ps <+: s₁.diffTrs s ∧ AP.sys.trs s ps = (s₂, []) ∧ s₂.aPos = p) ∧ ∃ (ps : List PointZ) (p₁ : PointZ) (s₂ : AP.State), AP.AState s₂ ∧ ps ++ [p₁] <+: s₁.diffTrs s ∧ AP.sys.trs s ps = (s₂, []) ∧ AP.sys.validTr s₂ p ∧ p ≠ p₁}

def AP.State.aProx' (s s₁ : State) : Set' PointZ

Equations

• s.aProx' s₁ = s.aNbhdsIcoPrev s₁