def AP.aMimic (st : Strat) (s s' : State) : AStrat

Equations

• AP.aMimic st s s' = AP.AStrat.mk fun (sa : AP.State) => some (have n := sa.hist.length - s'.hist.length; have r := AP.sys.simulate st.f s n; st.a.f r.1)

def AP.dMimic (st : Strat) (s s' : State) : DStrat

Equations

• AP.dMimic st s s' = AP.DStrat.mk fun (sd : AP.State) => some (have n := sd.hist.length - s'.hist.length; have r := AP.sys.simulate st.f s n; st.d.f r.1)

instance AP.instWFAMimic {st : Strat} {s s' : State} : (aMimic st s s').WF

instance AP.instWFDMimic {st : Strat} {s s' : State} : (dMimic st s s').WF

theorem AP.aMimic_apply_eq_of {st st' : Strat} {s₀ s₁ s₂ : State} {n : ℕ} [hs₀ : sys.WF s₀] (h₁ : sys.simulate st.f s₀ n = (s₁, 0)) (h₂ : sys.simulate st'.f s₀ n = (s₂, 0)) (h₃ : sys.validTr s₂ (st.a.f s₁)) : (aMimic st s₀ s₀).f s₂ = st.a.f s₁

theorem AP.dMimic_apply_eq_of {st st' : Strat} {s₀ s₁ s₂ : State} {n : ℕ} [hs₀ : sys.WF s₀] (h₁ : sys.simulate st.f s₀ n = (s₁, 0)) (h₂ : sys.simulate st'.f s₀ n = (s₂, 0)) (h₃ : sys.validTr s₂ (st.d.f s₁)) : (dMimic st s₀ s₀).f s₂ = st.d.f s₁

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

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

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

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