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

Equations

• a.Fresh1 s fsp = (a.WF ∧ s.aForallWinsDisj fsp a ∧ ∀ (d : AP.DStrat), d.WF → ∀ (s₁ : AP.State) (p : PointZ), (s₁, p) ∈ s.aSimPairs { a := a, d := d } → p ∉ s.aVisitedIcc s₁)

def AP.AHwsFspCnd (f : State → State → FSP) (s s₂ : State) (fsp : FSP) : Prop

Equations

• AP.AHwsFspCnd f s s₂ fsp = s₂.aHwsDisj (fsp.offset (s.diff s₂) ∪ f s s₂)

def AP.AStrat.RespectsFSP (f : State → State → FSP) (a : AStrat) (s : State) (fsp : FSP) : Prop

Equations

• AP.AStrat.RespectsFSP f a s fsp = (a.WF ∧ s.aPos ∉ fsp.get 0 ∧ ∀ (d : AP.DStrat), d.WF → ∀ (n : ℕ), ∃ (s₁ : AP.State) (s₂ : AP.State), AP.sys.simulate { a := a, d := d }.f s (n * 2) = (s₁, 0) ∧ AP.sys.tr s₁ (a.f s₁) = some s₂ ∧ AP.AHwsFspCnd f s s₂ fsp)

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

Equations

• AP.aFresh1FSP s s₂ = ∅.insertSet 0 (s.aVisitedIcc s₂.prev).toSet

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

Equations

• a.Fresh1Aux s fsp = AP.AStrat.RespectsFSP AP.aFresh1FSP a s fsp

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

Equations

• AP.aFresh1 s fsp = AP.aSeek fun (x : AP.State) => AP.AHwsFspCnd AP.aFresh1FSP s x fsp

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

theorem AP.State.aPos_notMem_of_aWinsDisj {s : State} {fsp : FSP} {a : AStrat} {d : DStrat} (h : s.aWinsDisj fsp { a := a, d := d }) : s.aPos ∉ fsp.get 0

theorem AP.State.aPos_notMem_of_aForallWinsDisj {s : State} {fsp : FSP} {a : AStrat} (h : s.aForallWinsDisj fsp a) : s.aPos ∉ fsp.get 0

theorem AP.State.aPos_notMem_of_aHwsDisj {s : State} {fsp : FSP} (h : s.aHwsDisj fsp) : s.aPos ∉ fsp.get 0

theorem AP.State.hasTr_of_aWinsDisj {s : State} {fsp : FSP} {a : AStrat} {d : DStrat} [hs : sys.WF s] (h : s.aWinsDisj fsp { a := a, d := d }) : sys.hasTr s

theorem AP.State.hasTr_of_aForallWinsDisj {s : State} {fsp : FSP} {a : AStrat} [hs : sys.WF s] (h : s.aForallWinsDisj fsp a) : sys.hasTr s

theorem AP.State.hasTr_of_aHwsDisj {s : State} {fsp : FSP} [hs : sys.WF s] (h : s.aHwsDisj fsp) : sys.hasTr s

@[simp]

instance AP.instWFAFresh1 {s : State} {fsp : FSP} : (aFresh1 s fsp).WF

theorem AP.AState.aForallWinsDisj_of_respectsFSP {s : State} {fsp : FSP} {f : State → State → FSP} {a : AStrat} [hs : AState s] (h : AStrat.RespectsFSP f a s fsp) : s.aForallWinsDisj fsp a

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

theorem AP.AState.fresh1_of_fresh1Aux {s : State} {fsp : FSP} {a : AStrat} [hs : AState s] (h : a.Fresh1Aux s fsp) : a.Fresh1 s fsp

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

theorem AP.State.aSimPairs_state_eq_of_point_eq_of_fresh1 {s : State} {a : AStrat} {d : DStrat} {s₁ s₂ : State} {p : PointZ} {fsp : FSP} [hs : sys.WF s] [hd : d.WF] (h : a.Fresh1 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_fresh1 {s : State} {fsp : FSP} {a : AStrat} [hs : sys.WF s] (h : a.Fresh1 s fsp) (set : Set' PointZ) (d : DStrat) [d.WF] : ∃ (n : ℕ), s.aSimPtsNcard { a := a, d := d } set.toSet = some n ∧ n ≤ set.size