noncomputable def AP.aSeek (p : State → Prop) : AStrat

Equations

• AP.aSeek p = AP.AStrat.mk fun (sa : AP.State) => choose? fun (pa : PointZ) => ∃ (sd : AP.State), AP.sys.tr sa pa = some sd ∧ p sd

def AP.aStratChooseCnd (p : State → Prop) (sa : State) (pa : PointZ) : Prop

Equations

• AP.aStratChooseCnd p sa pa = ∃ (sd : AP.State), AP.sys.tr sa pa = some sd ∧ ∀ (pd : PointZ) (sa' : AP.State), AP.sys.tr sd pd = some sa' → p sa'

noncomputable def AP.aStratChoose (p : State → Prop) : AStrat

Equations

• AP.aStratChoose p = AP.AStrat.mk fun (sa : AP.State) => choose? (AP.aStratChooseCnd p sa)

def AP.getMoveFromHist (s_target s : State) : List PointZ → Option PointZ

Equations

• AP.getMoveFromHist s_target s [] = none
• AP.getMoveFromHist s_target s (p :: ps) = if s = s_target then some p else do let s' ← AP.sys.tr s p AP.getMoveFromHist s_target s' ps

def AP.State.getMoveAt (s s_target : State) : Option PointZ

Equations

• s.getMoveAt s_target = AP.getMoveFromHist s_target (AP.initState s.pw s.aPos₀) s.hist.reverse.tail

noncomputable def AP.dStratOfDWins (sa : State) : DStrat

Equations

• AP.dStratOfDWins sa = AP.DStrat.mk fun (sd : AP.State) => do let pa ← sd.getMoveAt sa let sd' ← AP.sys.tr sa pa let pd ← choose? fun (pd : PointZ) => ∃ (sa' : AP.State), AP.sys.tr sd' pd = some sa' ∧ ∃ (d : AP.DStrat), d.WF ∧ ∀ (a : AP.AStrat), a.WF → sa'.dWins { a := a, d := d } if sd' = sd then some pd else do let sa' ← AP.sys.tr sd' pd let d ← choose? fun (d : AP.DStrat) => d.WF ∧ ∀ (a : AP.AStrat), a.WF → sa'.dWins { a := a, d := d } pure (d.f sd)

def AP.AStrat.set (a : AStrat) (s : State) (p : PointZ) : AStrat

Equations

• a.set s p = { f := fn_set s p a.f }

def AP.DStrat.set (d : DStrat) (s : State) (p : PointZ) : DStrat

Equations

• d.set s p = { f := fn_set s p d.f }

noncomputable def AP.aStratOfAHws (sd : State) : AStrat

Equations

• AP.aStratOfAHws sd = AP.AStrat.mk fun (sa : AP.State) => do let pd ← sa.getMoveAt sd let sa' ← AP.sys.tr sd pd let a ← choose? fun (a : AP.AStrat) => a.WF ∧ ∀ (d : AP.DStrat), d.WF → sa'.aWins { a := a, d := d } pure (a.f sa)

theorem AP.State.not_aHws_of_dHws {s : State} (h : s.dHws) : ¬s.aHws

theorem AP.AState.of_simulate_mul_two {sa : State} [ha : AState sa] {st : Strat} [hst : st.WF] {n : ℕ} : AState (sys.simulate st.f sa (n * 2)).1

@[simp]

instance AP.instAStateFstStateNatSimulatePointZSysFHMulOfNat {sa : State} [ha : AState sa] {st : Strat} [hst : st.WF] {n : ℕ} : AState (sys.simulate st.f sa (n * 2)).1

theorem AP.AState.of_simulate_mul_two_eq' {sa s₁ : State} {r : ℕ} [ha : AState sa] {st : Strat} [hst : st.WF] {n : ℕ} (h : sys.simulate st.f sa (n * 2) = (s₁, r)) : AState s₁

theorem AP.AState.of_simulate_mul_two_eq_full {sa s₁ : State} {f : State → PointZ} [ha : AState sa] {n : ℕ} (h : sys.simulate f sa (n * 2) = (s₁, 0)) : AState s₁

theorem AP.DState.of_simulate_mul_two_eq_full {sd s₁ : State} {f : State → PointZ} [hd : DState sd] {n : ℕ} (h : sys.simulate f sd (n * 2) = (s₁, 0)) : DState s₁

theorem AP.AState.aWins_of_ind_two' {sa₀ : State} [ha₀ : AState sa₀] {st : Strat} [hst : st.WF] {p : State → Prop} (hp : p sa₀) (h : ∀ {sa : State} [AState sa], sys.Reachable sa₀ sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ ∀ (sa' : State), sys.tr sd (st.d.f sd) = some sa' → p sa') : sa₀.aWins st ∧ p sa₀

theorem AP.AState.aWins_of_ind_two {sa₀ : State} [ha₀ : AState sa₀] {st : Strat} [hst : st.WF] {p : State → Prop} (hp : p sa₀) (h : ∀ {sa : State} [AState sa], sys.Reachable sa₀ sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ ∀ (sa' : State), sys.tr sd (st.d.f sd) = some sa' → p sa') : sa₀.aWins st

theorem AP.AState.ind_two {sa sa' : State} [ha : AState sa] [ha' : AState sa'] {p : State → Prop} (h₁ : p sa) (h₂ : ∀ (sa : State) [AState sa] (pa : PointZ) (sd : State) (pd : PointZ) (sa' : State), sys.tr sa pa = some sd → sys.tr sd pd = some sa' → p sa') (h₃ : sys.Reachable sa sa') : p sa'

theorem AP.wf_aStratChoose {p : State → Prop} : (aStratChoose p).WF

@[simp]

instance AP.instWFAStratChoose {p : State → Prop} : (aStratChoose p).WF

theorem AP.AState.aHws_of_ind_two' {sa₀ : State} [ha₀ : AState sa₀] {p : State → Prop} (h₁ : p sa₀) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable sa₀ sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ ∀ (pd : PointZ) (sa' : State), sys.tr sd pd = some sa' → p sa') : sa₀.aHws ∧ p sa₀

theorem AP.AState.aHws_of_ind_two {sa₀ : State} [ha₀ : AState sa₀] {p : State → Prop} (h₁ : p sa₀) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable sa₀ sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ ∀ (pd : PointZ) (sa' : State), sys.tr sd pd = some sa' → p sa') : sa₀.aHws

@[simp]

instance AP.instTreeStatePointZSysOfWF {s : State} [hs : sys.WF s] : sys.Tree s

theorem AP.getMoveFromHist_append_eq_some_of {s acc : State} {ps ps₁ : List PointZ} {p : PointZ} (h : getMoveFromHist s acc ps = some p) : getMoveFromHist s acc (ps ++ ps₁) = some p

theorem AP.getMoveAt_eq_getMoveAt_eq_some_and_tr {s₁ s₂ : State} {p₁ : PointZ} {s : State} {p : PointZ} [hs : sys.WF s₁] (h₁ : s₁.getMoveAt s = some p) (h₂ : sys.tr s₁ p₁ = some s₂) : s₂.getMoveAt s = some p

theorem AP.getMoveFromHist_eq_some_iff_exi_trs {s acc : State} {p : PointZ} {ps : List PointZ} [hs : sys.WF acc] : getMoveFromHist s acc ps = some p ↔ sys.WF s ∧ ∃ (ps' : List PointZ), ps' ++ [p] <+: ps ∧ sys.trs acc ps' = (s, [])

theorem AP.getMoveAt_eq_some_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') : s'.getMoveAt s = some p

theorem AP.getMoveAt_eq_some_of_tr_and_reachable {s s₁ s₂ : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s₁) (h₂ : sys.Reachable s₁ s₂) : s₂.getMoveAt s = some p

theorem AP.getMoveAt_eq_some_iff_exi_trs {s₀ s : State} {p : PointZ} [sys.WF s] : s.getMoveAt s₀ = some p ↔ ∃ (ps' : List PointZ), ps' ++ [p] <+: s.hist.reverse.tail ∧ sys.trs (initState s.pw s.aPos₀) ps' = (s₀, [])

instance AP.instWFDStratOfDWins {sa : State} : (dStratOfDWins sa).WF

@[simp]

theorem AP.AStrat.f_set {a : AStrat} {s : State} {p : PointZ} : (a.set s p).f = fn_set s p a.f

@[simp]

theorem AP.DStrat.f_set {d : DStrat} {s : State} {p : PointZ} : (d.set s p).f = fn_set s p d.f

theorem AP.AStrat.wf_set_of_validTr {a : AStrat} {s : State} {p : PointZ} [ha : a.WF] (h : sys.validTr s p) : (a.set s p).WF

theorem AP.DStrat.wf_set_of_validTr {d : DStrat} {s : State} {p : PointZ} [hd : d.WF] (h : sys.validTr s p) : (d.set s p).WF

theorem AP.AStrat.wf_set_of_tr {a : AStrat} {s s' : State} {p : PointZ} [ha : a.WF] (h : sys.tr s p = some s') : (a.set s p).WF

theorem AP.DStrat.wf_set_of_tr {d : DStrat} {s s' : State} {p : PointZ} [hd : d.WF] (h : sys.tr s p = some s') : (d.set s p).WF

theorem AP.simulate_congr {s : State} [hs : sys.WF s] {st₁ st₂ : Strat} [hst₁ : st₁.WF] [hst₂ : st₂.WF] {n : ℕ} (h₁ : ∀ k < n, ∀ (sa : State) [AState sa], sys.simulate st₁.f s k = (sa, 0) → sys.simulate st₂.f s k = (sa, 0) → sys.hasTr sa → st₁.a.f sa = st₂.a.f sa) (h₂ : ∀ k < n, ∀ (sd : State) [DState sd], sys.simulate st₁.f s k = (sd, 0) → sys.simulate st₂.f s k = (sd, 0) → sys.hasTr sd → st₁.d.f sd = st₂.d.f sd) : sys.simulate st₁.f s n = sys.simulate st₂.f s n

theorem AP.AState.aHws_of_not_dHws {sa : State} [ha : AState sa] (h : ¬sa.dHws) : sa.aHws

instance AP.instWFAStratOfAHws {s : State} : (aStratOfAHws s).WF

theorem AP.AState.dHws_of_tr' {sd sa : State} {pd : PointZ} [hd : DState sd] (h₁ : sys.tr sd pd = some sa) (h₂ : sa.dHws) : sd.dHws

theorem AP.DState.aHws_of_tr' {sa sd : State} {pa : PointZ} [ha : AState sa] (h₁ : sys.tr sa pa = some sd) (h₂ : sd.aHws) : sa.aHws

theorem AP.State.aHws_of_not_dHws {s : State} [hs : sys.WF s] (h : ¬s.dHws) : s.aHws

@[simp]

theorem AP.State.not_aHws_iff {s : State} [hs : sys.WF s] : ¬s.aHws ↔ s.dHws

@[simp]

theorem AP.State.not_dHws_iff {s : State} [hs : sys.WF s] : ¬s.dHws ↔ s.aHws

theorem AP.State.hasTr_of_aHws {s : State} (h : s.aHws) : sys.hasTr s

theorem AP.AState.aHws_iff_tr {sa : State} [hs : AState sa] : sa.aHws ↔ ∃ (p : PointZ) (sd : State), sys.tr sa p = some sd ∧ sd.aHws

theorem AP.AState.dHws_iff_tr {sa : State} [hs : AState sa] : sa.dHws ↔ ∀ (p : PointZ) (sd : State), sys.tr sa p = some sd → sd.dHws

theorem AP.DState.dHws_iff_tr {sd : State} [hs : DState sd] : sd.dHws ↔ ∃ (p : PointZ) (sa : State), sys.tr sd p = some sa ∧ sa.dHws

theorem AP.DState.aHws_iff_tr {sd : State} [hs : DState sd] : sd.aHws ↔ ∀ (p : PointZ) (sa : State), sys.tr sd p = some sa → sa.aHws

theorem AP.AState.aHws_of_ind' {s : State} [ha : AState s] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (pd : PointZ) (sa : State), sys.Reachable s sd → p sd → sys.tr sd pd = some sa → p sa) : s.aHws ∧ p s

theorem AP.AState.aHws_of_ind {s : State} [ha : AState s] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (pd : PointZ) (sa : State), sys.Reachable s sd → p sd → sys.tr sd pd = some sa → p sa) : s.aHws

theorem AP.AState.aWins_of_ind' {s : State} [ha : AState s] {st : Strat} [hst : st.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), sys.Reachable s sd → p sd → sys.tr sd (st.d.f sd) = some sa → p sa) : s.aWins st ∧ p s

theorem AP.AState.aWins_of_ind {s : State} [ha : AState s] {st : Strat} [hst : st.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), sys.Reachable s sd → p sd → sys.tr sd (st.d.f sd) = some sa → p sa) : s.aWins st

theorem AP.State.aWins_of_ind' {s : State} [hs : sys.WF s] {st : Strat} [hst : st.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), sys.Reachable s sd → p sd → sys.tr sd (st.d.f sd) = some sa → p sa) : s.aWins st ∧ p s

theorem AP.State.aWins_of_ind {s : State} [hs : sys.WF s] {st : Strat} [hst : st.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (sd : State), sys.tr sa (st.a.f sa) = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), sys.Reachable s sd → p sd → sys.tr sd (st.d.f sd) = some sa → p sa) : s.aWins st

theorem AP.State.aHws_of_ind' {s : State} [hs : sys.WF s] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (pd : PointZ) (sa : State), sys.Reachable s sd → p sd → sys.tr sd pd = some sa → p sa) : s.aHws ∧ p s

theorem AP.State.aHws_of_ind {s : State} [hs : sys.WF s] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], sys.Reachable s sa → p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (pd : PointZ) (sa : State), sys.Reachable s sd → p sd → sys.tr sd pd = some sa → p sa) : s.aHws

instance AP.instWFASeek {p : State → Prop} : (aSeek p).WF

theorem AP.State.exi_aWins_of_ind' {s : State} [hs : sys.WF s] {d : DStrat} [Hd : d.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), p sd → sys.tr sd (d.f sd) = some sa → p sa) : (∃ (a : AStrat), a.WF ∧ s.aWins { a := a, d := d }) ∧ p s

theorem AP.State.exi_aWins_of_ind {s : State} [hs : sys.WF s] {d : DStrat} [Hd : d.WF] {p : State → Prop} (h₁ : p s) (h₂ : ∀ (sa : State) [AState sa], p sa → ∃ (pa : PointZ) (sd : State), sys.tr sa pa = some sd ∧ p sd) (h₃ : ∀ (sd : State) [DState sd] (sa : State), p sd → sys.tr sd (d.f sd) = some sa → p sa) : ∃ (a : AStrat), a.WF ∧ s.aWins { a := a, d := d }

theorem AP.State.aWins_iff_add {s : State} {st : Strat} (k : ℕ) : s.aWins st ↔ ∀ (n : ℕ), (sys.simulate st.f s (k + n)).2 = 0

theorem AP.State.dWins_iff_add {s : State} {st : Strat} (k : ℕ) : s.dWins st ↔ ∃ (n : ℕ), (sys.simulate st.f s (k + n)).2 ≠ 0

theorem AP.State.length_hist_lt_of_tr {s s' : State} {p : PointZ} (h : sys.tr s p = some s') : s.hist.length < s'.hist.length

theorem AP.length_hist_sub_eq_of_simulate {s₀ s : State} {n : ℕ} {f : State → PointZ} [hs : sys.WF s₀] (h : sys.simulate f s₀ n = (s, 0)) : s.hist.length - s₀.hist.length = n

theorem AP.AState.dHws_of_tr {sa sd : State} {p : PointZ} [ha : AState sa] (h₁ : sys.tr sa p = some sd) (h₂ : sa.dHws) : sd.dHws

theorem AP.DState.aHws_of_tr {sd sa : State} {p : PointZ} [hd : DState sd] (h₁ : sys.tr sd p = some sa) (h₂ : sd.aHws) : sa.aHws

theorem AP.State.dWins_of_lt_lt {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {p : State → Prop} {f : State → ℕ} (h₁ : p s) (h₂ : ∀ (sa sd : State) [AState sa] [DState sd], p sa → sys.tr sa (a.f sa) = some sd → p sd ∧ f sd < f sa) (h₃ : ∀ (sd sa : State) [DState sd] [AState sa], p sd → sys.tr sd (d.f sd) = some sa → p sa ∧ f sa < f sd) : s.dWins { a := a, d := d }

theorem AP.State.dWins_of_le_lt {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {p : State → Prop} {f : State → ℕ} (h₁ : p s) (h₂ : ∀ (sa sd : State) [AState sa] [DState sd], p sa → sys.tr sa (a.f sa) = some sd → p sd ∧ f sd ≤ f sa) (h₃ : ∀ (sd sa : State) [DState sd] [AState sa], p sd → sys.tr sd (d.f sd) = some sa → p sa ∧ f sa < f sd) : s.dWins { a := a, d := d }

theorem AP.State.dWins_of_lt_le {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {p : State → Prop} {f : State → ℕ} (h₁ : p s) (h₂ : ∀ (sa sd : State) [AState sa] [DState sd], p sa → sys.tr sa (a.f sa) = some sd → p sd ∧ f sd < f sa) (h₃ : ∀ (sd sa : State) [DState sd] [AState sa], p sd → sys.tr sd (d.f sd) = some sa → p sa ∧ f sa ≤ f sd) : s.dWins { a := a, d := d }

theorem AP.State.dWins_of_lt_lt_uncond {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {f : State → ℕ} (h₁ : ∀ (sa sd : State) [AState sa] [DState sd], sys.tr sa (a.f sa) = some sd → f sd < f sa) (h₂ : ∀ (sd sa : State) [DState sd] [AState sa], sys.tr sd (d.f sd) = some sa → f sa < f sd) : s.dWins { a := a, d := d }

theorem AP.State.dWins_of_le_lt_uncond {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {f : State → ℕ} (h₁ : ∀ (sa sd : State) [AState sa] [DState sd], sys.tr sa (a.f sa) = some sd → f sd ≤ f sa) (h₂ : ∀ (sd sa : State) [DState sd] [AState sa], sys.tr sd (d.f sd) = some sa → f sa < f sd) : s.dWins { a := a, d := d }

theorem AP.State.dWins_of_lt_le_uncond {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] {f : State → ℕ} (h₁ : ∀ (sa sd : State) [AState sa] [DState sd], sys.tr sa (a.f sa) = some sd → f sd < f sa) (h₂ : ∀ (sd sa : State) [DState sd] [AState sa], sys.tr sd (d.f sd) = some sa → f sa ≤ f sd) : s.dWins { a := a, d := d }

theorem AP.State.simulate_set_a_eq_of_length_hist_lt {s s₁ : State} {p₁ : PointZ} {n : ℕ} {a : AStrat} {d : DStrat} [hs : sys.WF s] [hs₁ : sys.WF s₁] [ha : a.WF] [hd : d.WF] (h₁ : sys.validTr s₁ p₁) (h₂ : s₁.hist.length < s.hist.length) : sys.simulate { a := a.set s₁ p₁, d := d }.f s n = sys.simulate { a := a, d := d }.f s n

theorem AP.State.simulate_set_d_eq_of_length_hist_lt {s s₁ : State} {p₁ : PointZ} {n : ℕ} {a : AStrat} {d : DStrat} [hs : sys.WF s] [hs₁ : sys.WF s₁] [ha : a.WF] [hd : d.WF] (h₁ : sys.validTr s₁ p₁) (h₂ : s₁.hist.length < s.hist.length) : sys.simulate { a := a, d := d.set s₁ p₁ }.f s n = sys.simulate { a := a, d := d }.f s n

theorem AP.State.simulate_set_a_eq_of_le_length_hist_sub {s s₁ : State} {p₁ : PointZ} {n : ℕ} {a : AStrat} {d : DStrat} [hs : sys.WF s] [hs₁ : sys.WF s₁] [ha : a.WF] [hd : d.WF] (h₁ : sys.validTr s₁ p₁) (h₂ : n ≤ s₁.hist.length - s.hist.length) : sys.simulate { a := a.set s₁ p₁, d := d }.f s n = sys.simulate { a := a, d := d }.f s n

theorem AP.State.simulate_set_d_eq_of_le_length_hist_sub {s s₁ : State} {p₁ : PointZ} {n : ℕ} {a : AStrat} {d : DStrat} [hs : sys.WF s] [hs₁ : sys.WF s₁] [ha : a.WF] [hd : d.WF] (h₁ : sys.validTr s₁ p₁) (h₂ : n ≤ s₁.hist.length - s.hist.length) : sys.simulate { a := a, d := d.set s₁ p₁ }.f s n = sys.simulate { a := a, d := d }.f s n