def AP.AStrat.mkFold' {α : Type u_1} (s : State) (z : α) (fa : State → α → PointZ × α) (fd : State → PointZ → α → α) : List PointZ → Option PointZ

Equations

• AP.AStrat.mkFold' s z fa fd [] = some (fa s z).1
• AP.AStrat.mkFold' s z fa fd (p :: ps) = do let s₁ ← AP.sys.tr s p AP.AStrat.mkFold' s₁ (if s.aTurn = true then (fa s z).2 else fd s p z) fa fd ps

def AP.AStrat.mkFold {α : Type u_1} (s₀ : State) (z : α) (fa : State → α → PointZ × α) (fd : State → PointZ → α → α) : AStrat

Equations

• AP.AStrat.mkFold s₀ z fa fd = AP.AStrat.mk fun (s : AP.State) => AP.AStrat.mkFold' s₀ z fa fd (List.drop s₀.hist.length s.hist.reverse)

def AP.DStrat.mkFold' {α : Type u_1} (s : State) (z : α) (fa : State → PointZ → α → α) (fd : State → α → PointZ × α) : List PointZ → Option PointZ

Equations

• AP.DStrat.mkFold' s z fa fd [] = some (fd s z).1
• AP.DStrat.mkFold' s z fa fd (p :: ps) = do let s₁ ← AP.sys.tr s p AP.DStrat.mkFold' s₁ (if s.aTurn = true then fa s p z else (fd s z).2) fa fd ps

def AP.DStrat.mkFold {α : Type u_1} (s₀ : State) (z : α) (fa : State → PointZ → α → α) (fd : State → α → PointZ × α) : DStrat

Equations

• AP.DStrat.mkFold s₀ z fa fd = AP.DStrat.mk fun (s : AP.State) => AP.DStrat.mkFold' s₀ z fa fd (List.drop s₀.hist.length s.hist.reverse)

@[simp]

instance AP.instWFMkFold {α : Type u_1} {z : α} {s₀ : State} {fa : State → α → PointZ × α} {fd : State → PointZ → α → α} : (AStrat.mkFold s₀ z fa fd).WF

@[simp]

instance AP.instWFMkFold_1 {α : Type u_1} {z : α} {s₀ : State} {fa : State → PointZ → α → α} {fd : State → α → PointZ × α} : (DStrat.mkFold s₀ z fa fd).WF

theorem AP.aStrat_mkFold_apply_a {α : Type u_1} {s : State} {z : α} {fa : State → α → PointZ × α} {fd : State → PointZ → α → α} (h : sys.validTr s (fa s z).1) : (AStrat.mkFold s z fa fd).f s = (fa s z).1

theorem AP.AState.aStrat_mkFold_eq_of_tr {α : Type u_1} {s s' s₁ : State} {z : α} {fa : State → α → PointZ × α} {fd : State → PointZ → α → α} [hs : AState s] (h₁ : sys.tr s (fa s z).1 = some s') (h₂ : sys.Reachable s' s₁) : (AStrat.mkFold s' (fa s z).2 fa fd).f s₁ = (AStrat.mkFold s z fa fd).f s₁

theorem AP.DState.aStrat_mkFold_eq_of_tr {α : Type u_1} {s s' s₁ : State} {p : PointZ} {z : α} {fa : State → α → PointZ × α} {fd : State → PointZ → α → α} [hs : DState s] (h₁ : sys.tr s p = some s') (h₂ : sys.Reachable s' s₁) : (AStrat.mkFold s' (fd s p z) fa fd).f s₁ = (AStrat.mkFold s z fa fd).f s₁

theorem AP.AStrat.mkFold_ind {α : Type u_1} {s : State} {z : α} {fa : State → α → PointZ × α} {fd : State → PointZ → α → α} {n : ℕ} {d : DStrat} {p : State → α → Prop} [hs : sys.WF s] [hd : d.WF] (h₀ : p s z) (h₁ : ∀ (sa : State) [AState sa] (acc : α), sys.Reachable s sa → p sa acc → ∃ (sd : State), sys.tr sa (fa sa acc).1 = some sd ∧ p sd (fa sa acc).2) (h₂ : ∀ (sd : State) [DState sd] (sa : State) [AState sa] (p₁ : PointZ) (acc : α), sys.Reachable s sd → sys.tr sd p₁ = some sa → p sd acc → p sa (fd sd p₁ acc)) : ∃ (s₁ : State) (acc : α), sys.simulate { a := mkFold s z fa fd, d := d }.f s n = (s₁, 0) ∧ p s₁ acc