def AP.AStrat.Fresh (a : AStrat) (s : State) (fsp : FSP) : Prop

Equations

• a.Fresh s fsp = (a.Fresh1 s fsp ∧ ∀ (d : AP.DStrat), d.WF → ∀ (s₁ s' : AP.State) (p p' : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → s' ∈ AP.State.aSimStatesIcoVia { a := a, d := d } s s₁ → AP.sys.validTr s' p' → p' ≠ a.f s' → p ≠ p')

def AP.aFreshFSP (s s₂ : State) : FSP

Equations

• AP.aFreshFSP s s₂ = (∅.insertSet 0 (s.aNbhdsIcoPrev s₂.prev).toSet).insertSet 2 (Point.nbhd s₂.prev.aPos ↑s.pw).toSet

def AP.AStrat.FreshAux (a : AStrat) (s : State) (fsp : FSP) : Prop

Equations

• a.FreshAux s fsp = AP.AStrat.RespectsFSP AP.aFreshFSP a s fsp

noncomputable def AP.aFresh (s : State) (fsp : FSP) : AStrat

Equations

• AP.aFresh s fsp = AP.aSeek fun (x : AP.State) => AP.AHwsFspCnd AP.aFreshFSP s x fsp

theorem AP.AStrat.Fresh.fresh1 {a : AStrat} {s : State} {fsp : FSP} (h : a.Fresh s fsp) : a.Fresh1 s fsp

theorem AP.AStrat.Fresh.wf {a : AStrat} {s : State} {fsp : FSP} (h : a.Fresh s fsp) : a.WF

theorem AP.AStrat.fresh_iff_alt₁ {a : AStrat} {s : State} {fsp : FSP} [hs : AState s] : a.Fresh s fsp ↔ a.Fresh1 s fsp ∧ ∀ (d : DStrat), d.WF → ∀ (s₁ s' : State) (p p' : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → s' ∈ State.aSimStatesIcoVia { a := a, d := d } s s₁ → sys.validTr s' p' → p ≠ p'

theorem AP.AStrat.fresh_iff_alt₂ {a : AStrat} {s : State} {fsp : FSP} [hs : AState s] : a.Fresh s fsp ↔ a.WF ∧ s.aForallWinsDisj fsp a ∧ ∀ (d : DStrat), d.WF → ∀ (s₁ s' : State) (p p' : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → s' ∈ State.aSimStatesIcoVia { a := a, d := d } s s₁ → Point.dist p' s'.aPos ≤ ↑s.pw → p ≠ p'

theorem AP.AStrat.fresh_iff_alt₃ {a : AStrat} {s : State} {fsp : FSP} [hs : AState s] : a.Fresh s fsp ↔ a.WF ∧ s.aForallWinsDisj fsp a ∧ ∀ (d : DStrat), d.WF → ∀ (s₁ s' : State) (p : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → s' ∈ State.aSimStatesIcoVia { a := a, d := d } s s₁ → p ∉ Point.nbhd s'.aPos ↑s.pw

theorem AP.AStrat.fresh_iff_alt₄ {a : AStrat} {s : State} {fsp : FSP} [hs : AState s] : a.Fresh s fsp ↔ a.WF ∧ s.aForallWinsDisj fsp a ∧ ∀ (d : DStrat), d.WF → ∀ (s₁ : State) (p : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → p ∉ s.aNbhdsIcoPrev s₁

@[simp]

instance AP.instWFAFresh {s : State} {fsp : FSP} : (aFresh s fsp).WF

theorem AP.AState.aForallWinsDisj_of_freshAux {s : State} {fsp : FSP} {a : AStrat} [hs : AState s] (h : a.FreshAux s fsp) : s.aForallWinsDisj fsp a

theorem AP.AState.fresh_of_freshAux {s : State} {fsp : FSP} {a : AStrat} [hs : AState s] (h : a.FreshAux s fsp) : a.Fresh s fsp

theorem AP.AState.exi_fresh_of_aHwsDisj {s : State} {fsp : FSP} [hs : AState s] (h : s.aHwsDisj fsp) : ∃ (a : AStrat), a.Fresh s fsp

theorem AP.State.aSimPairs_state_eq_of_point_eq_of_fresh {s : State} {a : AStrat} {d : DStrat} {s₁ s₂ : State} {p : PointZ} {fsp : FSP} [hs : sys.WF s] [hd : d.WF] (h : a.Fresh s fsp) (h₁ : (s₁, p) ∈ s.aSimPairs { a := a, d := d }) (h₂ : (s₂, p) ∈ s.aSimPairs { a := a, d := d }) : s₁ = s₂

theorem AP.State.aSimPtsNcard_spec_of_fresh {s : State} {fsp : FSP} {a : AStrat} [hs : sys.WF s] (h : a.Fresh s fsp) (set : Set' PointZ) (d : DStrat) [d.WF] : ∃ (n : ℕ), s.aSimPtsNcard { a := a, d := d } set.toSet = some n ∧ n ≤ set.size