structure AP.Defense : Type

• cnd : State → Prop
• ps : Set PointZ
• f : State → Option PointZ

theorem AP.Defense.ext_iff {x y : Defense} : x = y ↔ x.cnd = y.cnd ∧ x.ps = y.ps ∧ x.f = y.f

theorem AP.Defense.ext {x y : Defense} (cnd : x.cnd = y.cnd) (ps : x.ps = y.ps) (f : x.f = y.f) : x = y

def AP.Defense.st (dse : Defense) (d : DStrat) : DStrat

Equations

• dse.st d = { f := fun (s : AP.State) => (dse.f s).getD (d.f s) }

def AP.Defense.ValidTr (dse : Defense) : Prop

Equations

• dse.ValidTr = ∀ {s : AP.State} [AP.DState s] {p : PointZ}, dse.f s = some p → AP.sys.validTr s p

class AP.Defense.WF (dse : Defense) : Prop

• valid_tr : dse.ValidTr
• not_mem_ps {s : State} [sys.WF s] : dse.cnd s → ∀ (a : AStrat) [a.WF] (d : DStrat) [d.WF] (n : ℕ), (sys.simulate { a := a, d := dse.st d }.f s n).1.aPos ∉ dse.ps

def AP.Defense.sym (dse : Defense) (sym : sys.Symmetry) : Defense

Equations

• dse.sym sym = { cnd := fun (s : AP.State) => dse.cnd (sym.fs' s), ps := ⇑sym.ft '' dse.ps, f := fun (s : AP.State) => Option.map (⇑sym.ft) (dse.f (sym.fs' s)) }

def AP.Defense.empty : Defense

Equations

• AP.Defense.empty = { cnd := fun (x : AP.State) => True, ps := ∅, f := fun (x : AP.State) => none }

@[instance_reducible]

instance AP.Defense.instEmptyCollection : EmptyCollection Defense

Equations

• AP.Defense.instEmptyCollection = { emptyCollection := AP.Defense.empty }

@[instance_reducible]

instance AP.Defense.instInhabited : Inhabited Defense

Equations

• AP.Defense.instInhabited = { default := ∅ }

def AP.Defense.merge (dse₁ dse₂ : Defense) : Defense

Equations

• dse₁.merge dse₂ = { cnd := fun (s : AP.State) => dse₁.cnd s ∧ dse₂.cnd s, ps := dse₁.ps ∪ dse₂.ps, f := fun (s : AP.State) => dse₁.f s <|> dse₂.f s }

def AP.Defense.ofList (ds : List Defense) : Defense

Equations

• AP.Defense.ofList ds = List.foldr AP.Defense.merge ∅ ds

def AP.Defense.Compatible' (p : State → Prop) (dse₁ dse₂ : Defense) : Prop

Equations

• AP.Defense.Compatible' p dse₁ dse₂ = ∀ {s₀ : AP.State} [AP.sys.WF s₀] {s : AP.State} {p₁ p₂ : PointZ}, p s₀ → dse₁.cnd s₀ → dse₂.cnd s₀ → AP.sys.Reachable s₀ s → dse₁.f s = some p₁ → dse₂.f s = some p₂ → p₁ = p₂

def AP.Defense.Compatible (dse₁ dse₂ : Defense) : Prop

Equations

• dse₁.Compatible dse₂ = AP.Defense.Compatible' (fun (x : AP.State) => True) dse₁ dse₂

def AP.Defense.CompatibleList' (p : State → Prop) (ds : List Defense) : Prop

Equations

• AP.Defense.CompatibleList' p ds = ∀ {s₀ : AP.State} [AP.sys.WF s₀] {s : AP.State} {p₁ p₂ : PointZ} {d₁ d₂ : AP.Defense}, p s₀ → (∀ d ∈ ds, d.cnd s₀) → AP.sys.Reachable s₀ s → d₁ ∈ ds → d₂ ∈ ds → d₁.f s = some p₁ → d₂.f s = some p₂ → p₁ = p₂

def AP.Defense.CompatibleList (ds : List Defense) : Prop

Equations

• AP.Defense.CompatibleList ds = AP.Defense.CompatibleList' (fun (x : AP.State) => True) ds

def AP.Defense.WF' (p : State → Prop) (dse : Defense) : Prop

Equations

• AP.Defense.WF' p dse = ∀ {s : AP.State} [AP.sys.WF s], p s → dse.cnd s → ∀ (a : AP.AStrat) [a.WF] (d : AP.DStrat) [d.WF] (n : ℕ), (AP.sys.simulate { a := a, d := dse.st d }.f s n).1.aPos ∉ dse.ps