def AP.State.ReachableVia' (f : State → PointZ) (s s₁ : State) : Prop

Equations

• AP.State.ReachableVia' f s s₁ = ∃ (n : ℕ), AP.sys.simulate f s n = (s₁, 0)

def AP.State.ReachableVia (st : Strat) (s s₁ : State) : Prop

Equations

• AP.State.ReachableVia st s s₁ = AP.State.ReachableVia' st.f s s₁

@[instance_reducible]

instance AP.instDecidableReachableVia {s s₁ : State} {st : Strat} : Decidable (State.ReachableVia st s s₁)

Equations

• AP.instDecidableReachableVia = decidable_of_bool (decide (AP.sys.simulate st.f s (s.diff s₁) = (s₁, 0))) ⋯

def AP.State.moveSim (s : State) (st : Strat) (s₁ : State) : Option (PointZ × State ⊕ PointZ × State)

Equations

• s.moveSim st s₁ = do guard (AP.State.ReachableVia st s s₁) have p : PointZ := st.f s₁ let s₂ ← AP.sys.tr s₁ p pure ((if s₁.aTurn = true then Sum.inr else Sum.inl) (p, s₂))

def AP.State.aMoveSim (s : State) (st : Strat) (s₁ : State) : Option (PointZ × State)

Equations

• s.aMoveSim st s₁ = do let __do_lift ← s.moveSim st s₁ match __do_lift with | Sum.inr r => some r | x => none

def AP.State.dMoveSim (s : State) (st : Strat) (s₁ : State) : Option (PointZ × State)

Equations

• s.dMoveSim st s₁ = do let __do_lift ← s.moveSim st s₁ match __do_lift with | Sum.inl r => some r | x => none

def AP.State.aSimPairs (s : State) (st : Strat) : Set (State × PointZ)

Equations

• s.aSimPairs st = {(s₁, p) : AP.State × PointZ | ∃ (s₂ : AP.State), s.aMoveSim st s₁ = some (p, s₂)}

def AP.State.aSimPts (s : State) (st : Strat) : Set PointZ

Equations

• s.aSimPts st = Prod.snd '' s.aSimPairs st

def AP.State.simStates (s : State) (st : Strat) : Set State

Equations

• s.simStates st = Set.ofPred (AP.State.ReachableVia st s)

def AP.State.simStatesRangeAuxVia (r : ℕ → ℕ → Prop) [hs : DecidableRel r] (st : Strat) (s s₁ : State) : Finset State

Equations

• AP.State.simStatesRangeAuxVia r st s s₁ = if ¬AP.State.ReachableVia st s s₁ then ∅ else {s₂ ∈ Finset.image (fun (n : ℕ) => (AP.sys.simulate st.f s n).1) (Finset.Icc 0 (s.diff s₁)) | r s₂.hist.length s₁.hist.length}

def AP.State.simStatesIccVia (st : Strat) (s s₁ : State) : Finset State

Equations

• AP.State.simStatesIccVia st s s₁ = AP.State.simStatesRangeAuxVia (fun (x1 x2 : ℕ) => x1 ≤ x2) st s s₁

def AP.State.simStatesIcoVia (st : Strat) (s s₁ : State) : Finset State

Equations

• AP.State.simStatesIcoVia st s s₁ = AP.State.simStatesRangeAuxVia (fun (x1 x2 : ℕ) => x1 < x2) st s s₁

def AP.State.aSimStatesIccVia (st : Strat) (s s₁ : State) : Finset State

Equations

• AP.State.aSimStatesIccVia st s s₁ = {x ∈ AP.State.simStatesIccVia st s s₁ | x.aTurn = true}

def AP.State.aSimStatesIcoVia (st : Strat) (s s₁ : State) : Finset State

Equations

• AP.State.aSimStatesIcoVia st s s₁ = {x ∈ AP.State.simStatesIcoVia st s s₁ | x.aTurn = true}

def AP.State.aSimStates (s : State) (st : Strat) : Set State

Equations

• s.aSimStates st = (s.simStates st).filter fun (x : AP.State) => x.aTurn = true

def AP.State.init (s : State) : State

Equations

• s.init = AP.initState s.pw s.aPos₀

def AP.State.prev (s : State) : State

Equations

• s.prev = (AP.sys.trs s.init (s.init.diffTrs s).init).1

def AP.State.lastMove (s : State) : PointZ

Equations

• s.lastMove = (s.prev.diffTrs s).getLast!

def AP.State.IsInit (s : State) : Prop

Equations

• s.IsInit = AP.sys.Initial s

noncomputable def AP.State.aSimPtsNcard (s : State) (st : Strat) (set : Set PointZ) : Option ℕ

Equations

• s.aSimPtsNcard st set = ((s.aSimPairs st).filter fun (x : AP.State × PointZ) => x.2 ∈ set).ncard?

def AP.Strat.ofFn (f : State → Option PointZ) : Strat

Equations

• AP.Strat.ofFn f = { a := AP.AStrat.mk f, d := AP.DStrat.mk f }

def AP.State.diffStrat (s s₁ : State) : Strat

Equations

• s.diffStrat s₁ = AP.Strat.ofFn fun (s' : AP.State) => (s.diffTrs s₁)[s.diff s']?

def AP.State.simStatesIcc (s s₁ : State) : Finset State

Equations

• s.simStatesIcc s₁ = AP.State.simStatesIccVia (s.diffStrat s₁) s s₁

def AP.State.simStatesIco (s s₁ : State) : Finset State

Equations

• s.simStatesIco s₁ = AP.State.simStatesIcoVia (s.diffStrat s₁) s s₁

def AP.State.aSimStatesIcc (s s₁ : State) : Finset State

Equations

• s.aSimStatesIcc s₁ = AP.State.aSimStatesIccVia (s.diffStrat s₁) s s₁

def AP.State.aSimStatesIco (s s₁ : State) : Finset State

Equations

• s.aSimStatesIco s₁ = AP.State.aSimStatesIcoVia (s.diffStrat s₁) s s₁

def AP.State.aVisitedIcc' (s : State) (ps : List PointZ) : Set' PointZ

Equations

• s.aVisitedIcc' [] = ∅
• s.aVisitedIcc' (p :: ps_2) = if s.aTurn = true then ((AP.sys.tr s p).getd.aVisitedIcc' ps_2).insert p else (AP.sys.tr s p).getd.aVisitedIcc' ps_2

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

Equations

• s.aVisitedIcc s₁ = if AP.sys.Reachable s s₁ then (s.aVisitedIcc' (s.diffTrs s₁)).insert s.aPos else ∅

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

Equations

• s.aVisitedIco s₁ = if s = s₁ then ∅ else s.aVisitedIcc s₁.prev

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

Equations

• s.aVisitedIcoPrev s₁ = if s.diff s₁ ≤ 1 then ∅ else s.aVisitedIco s₁.prev

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

Equations

• s.aNbhdsIcoPrev s₁ = (s.aVisitedIcoPrev s₁).bind fun (x : PointZ) => Set'.ofList (Point.nbhd x ↑s.pw)