theorem AP.Defense.empty_def : ∅ = empty

theorem AP.Defense.default_def : default = ∅

@[simp]

theorem AP.Defense.cnd_empty : ∅.cnd = fun (x : State) => True

@[simp]

theorem AP.Defense.ps_empty : ∅.ps = ∅

@[simp]

theorem AP.Defense.f_empty : ∅.f = fun (x : State) => none

@[simp]

instance AP.Defense.instWFEmptyCollection : ∅.WF

@[simp]

instance AP.Defense.instWFDefault : default.WF

theorem AP.Defense.valid_tr {dse : Defense} [H : dse.WF] {s : State} [DState s] {p : PointZ} : dse.f s = some p → sys.validTr s p

@[simp]

instance AP.Defense.instWFStOfWF {dse : Defense} {d : DStrat} [H : dse.WF] [Hd : d.WF] : (dse.st d).WF

theorem AP.Defense.st_comm {dse₁ dse₂ : Defense} {d : DStrat} (h : ∀ {s : State} {p₁ p₂ : PointZ}, dse₁.f s = some p₁ → dse₂.f s = some p₂ → p₁ = p₂) : dse₁.st (dse₂.st d) = dse₂.st (dse₁.st d)

theorem AP.Defense.simulate_st_comm {dse₁ dse₂ : Defense} {s₀ : State} {n : ℕ} {a : AStrat} {d : DStrat} [hs₀ : sys.WF s₀] [Ha : a.WF] [Hd : d.WF] [H₁ : dse₁.WF] [H₂ : dse₂.WF] (h : ∀ {s : State}, sys.Reachable s₀ s → ∀ {p₁ p₂ : PointZ}, dse₁.f s = some p₁ → dse₂.f s = some p₂ → p₁ = p₂) : sys.simulate { a := a, d := dse₁.st (dse₂.st d) }.f s₀ n = sys.simulate { a := a, d := dse₂.st (dse₁.st d) }.f s₀ n

@[simp]

theorem AP.Defense.sym_one {dse : Defense} : dse.sym 1 = dse

@[simp]

theorem AP.Defense.sym_sym {dse : Defense} {sym₁ sym₂ : sys.Symmetry} : (dse.sym sym₁).sym sym₂ = dse.sym (sym₂ * sym₁)

@[simp]

theorem AP.Defense.ps_sym {dse : Defense} {sym : sys.Symmetry} : (dse.sym sym).ps = ⇑sym.ft '' dse.ps

theorem AP.Defense.wf_sym_of_basicSym {dse : Defense} {sym : sys.Symmetry} [H₁ : dse.WF] [H₂ : BasicSym sym] : (dse.sym sym).WF

instance AP.Defense.instWFSymOfBasicSym {dse : Defense} {sym : sys.Symmetry} [H₁ : dse.WF] [H₂ : BasicSym sym] : (dse.sym sym).WF

@[simp]

theorem AP.Defense.wf_sym_iff_of_basicSym {dse : Defense} {sym : sys.Symmetry} [H₂ : BasicSym sym] : (dse.sym sym).WF ↔ dse.WF

@[simp]

theorem AP.Defense.merge_empty_left {dse : Defense} : ∅.merge dse = dse

@[simp]

theorem AP.Defense.merge_empty_right {dse : Defense} : dse.merge ∅ = dse

@[simp]

theorem AP.Defense.ofList_nil : ofList [] = ∅

@[simp]

theorem AP.Defense.ofList_cons {d : Defense} {ds : List Defense} : ofList (d :: ds) = d.merge (ofList ds)

@[simp]

theorem AP.Defense.cnd_merge {dse₁ dse₂ : Defense} : (dse₁.merge dse₂).cnd = fun (s : State) => dse₁.cnd s ∧ dse₂.cnd s

@[simp]

theorem AP.Defense.ps_merge {dse₁ dse₂ : Defense} : (dse₁.merge dse₂).ps = dse₁.ps ∪ dse₂.ps

@[simp]

theorem AP.Defense.f_merge {dse₁ dse₂ : Defense} : (dse₁.merge dse₂).f = fun (s : State) => dse₁.f s <|> dse₂.f s

@[simp]

theorem AP.Defense.st_merge {dse₁ dse₂ : Defense} : (dse₁.merge dse₂).st = fun (d : DStrat) => dse₁.st (dse₂.st d)

theorem AP.Defense.st_merge_ext {dse₁ dse₂ : Defense} {d : DStrat} : (dse₁.merge dse₂).st d = dse₁.st (dse₂.st d)

@[simp]

theorem AP.Defense.validTr_merge_of_wf {dse₁ dse₂ : Defense} [H₁ : dse₁.WF] [H₂ : dse₂.WF] : (dse₁.merge dse₂).ValidTr

@[simp]

theorem AP.Defense.Compatible.refl {dse : Defense} : dse.Compatible dse

theorem AP.Defense.Compatible.symm {dse₁ dse₂ : Defense} (h : dse₁.Compatible dse₂) : dse₂.Compatible dse₁

@[simp]

theorem AP.Defense.compatible_empty_left {dse : Defense} : ∅.Compatible dse

@[simp]

theorem AP.Defense.compatible_empty_right {dse : Defense} : dse.Compatible ∅

theorem AP.Defense.compatible_merge_left_of {a b c : Defense} (h₁ : a.Compatible c) (h₂ : b.Compatible c) : (a.merge b).Compatible c

theorem AP.Defense.compatible_merge_right_of {a b c : Defense} (h₁ : a.Compatible b) (h₂ : a.Compatible c) : a.Compatible (b.merge c)

theorem AP.Defense.compatible_ofList_of_forall_compatible {e : Defense} {ds : List Defense} (h : ∀ e₁ ∈ ds, e.Compatible e₁) : e.Compatible (ofList ds)

@[simp]

theorem AP.Defense.compatibleList_nil : CompatibleList []

@[simp]

theorem AP.Defense.validTr_empty : ∅.ValidTr

theorem AP.Defense.validTr_merge_of {dse₁ dse₂ : Defense} (h₁ : dse₁.ValidTr) (h₂ : dse₂.ValidTr) : (dse₁.merge dse₂).ValidTr

theorem AP.Defense.validTr_ofList' {ds : List Defense} (H : ∀ d ∈ ds, d.ValidTr) : (ofList ds).ValidTr

theorem AP.Defense.validTr_ofList {ds : List Defense} (H : ∀ d ∈ ds, d.WF) : (ofList ds).ValidTr

@[simp]

theorem AP.Defense.merge_self {d : Defense} : d.merge d = d

theorem AP.Defense.merge_assoc {a b c : Defense} : (a.merge b).merge c = a.merge (b.merge c)

@[simp]

theorem AP.Defense.ofList_append {ds₁ ds₂ : List Defense} : ofList (ds₁ ++ ds₂) = (ofList ds₁).merge (ofList ds₂)

@[simp]

theorem AP.Defense.cnd_ofList {ds : List Defense} {s : State} : (ofList ds).cnd s ↔ ∀ d ∈ ds, d.cnd s

@[simp]

theorem AP.Defense.ps_ofList {ds : List Defense} : (ofList ds).ps = ⋃ d ∈ ds, d.ps

@[simp]

theorem AP.Defense.st_empty : ∅.st = id

theorem AP.Defense.compatibleList'_of_perm {p : State → Prop} {ds₁ ds₂ : List Defense} (h₁ : CompatibleList' p ds₁) (h₂ : ds₁.Perm ds₂) : CompatibleList' p ds₂

theorem AP.Defense.compatibleList_of_perm {ds₁ ds₂ : List Defense} (h₁ : CompatibleList ds₁) (h₂ : ds₁.Perm ds₂) : CompatibleList ds₂

theorem AP.Defense.compatibleList'_iff_of_perm {p : State → Prop} {ds₁ ds₂ : List Defense} (h : ds₁.Perm ds₂) : CompatibleList' p ds₁ ↔ CompatibleList' p ds₂

theorem AP.Defense.compatibleList_iff_of_perm {ds₁ ds₂ : List Defense} (h : ds₁.Perm ds₂) : CompatibleList ds₁ ↔ CompatibleList ds₂

theorem AP.Defense.of_compatibleList'_cons {p : State → Prop} {d : Defense} {ds : List Defense} (h : CompatibleList' p (d :: ds)) : CompatibleList' (fun (s : State) => d.cnd s ∧ p s) ds

theorem AP.Defense.of_compatibleList_cons {d : Defense} {ds : List Defense} (h : CompatibleList (d :: ds)) : CompatibleList' d.cnd ds

theorem AP.Defense.of_f_ofList_eq_some {ds : List Defense} {s : State} {p : PointZ} (h : (ofList ds).f s = some p) : ∃ d ∈ ds, d.f s = some p

theorem AP.Defense.wf_merge {e₁ e₂ : Defense} [He₁ : e₁.WF] [He₂ : e₂.WF] (h₀ : e₁.Compatible e₂) : (e₁.merge e₂).WF

theorem AP.Defense.wf_iff_validTr_and_wf' {d : Defense} : d.WF ↔ d.ValidTr ∧ WF' (fun (x : State) => True) d

theorem AP.Defense.wf_dStrat_of_validTr {dse : Defense} {d : DStrat} [Hd : d.WF] (h : dse.ValidTr) : (dse.st d).WF

@[simp]

theorem AP.Defense.compatibleList'_nil {p : State → Prop} : CompatibleList' p []

theorem AP.Defense.compatibleList'_append_comm {p : State → Prop} {ds₁ ds₂ : List Defense} : CompatibleList' p (ds₁ ++ ds₂) ↔ CompatibleList' p (ds₂ ++ ds₁)

theorem AP.Defense.right_of_compatibleList'_append {p : State → Prop} {ds₁ ds₂ : List Defense} (h : CompatibleList' p (ds₁ ++ ds₂)) : CompatibleList' (fun (s : State) => (∀ d ∈ ds₁, d.cnd s) ∧ p s) ds₂

theorem AP.Defense.left_of_compatibleList'_append {p : State → Prop} {ds₁ ds₂ : List Defense} (h : CompatibleList' p (ds₁ ++ ds₂)) : CompatibleList' (fun (s : State) => (∀ d ∈ ds₂, d.cnd s) ∧ p s) ds₁

theorem AP.Defense.wf'_of_imp {d : Defense} {p₁ p₂ : State → Prop} (h₁ : WF' p₁ d) (h₂ : ∀ (s : State), p₂ s → p₁ s) : WF' p₂ d

theorem AP.Defense.simulate_st_comm' {dse₁ dse₂ : Defense} {s₀ : State} {n : ℕ} {a : AStrat} {d : DStrat} [hs₀ : sys.WF s₀] [Ha : a.WF] [Hd : d.WF] (hv₁ : dse₁.ValidTr) (hv₂ : dse₂.ValidTr) (h : ∀ (s : State), sys.Reachable s₀ s → ∀ {p₁ p₂ : PointZ}, dse₁.f s = some p₁ → dse₂.f s = some p₂ → p₁ = p₂) : sys.simulate { a := a, d := dse₁.st (dse₂.st d) }.f s₀ n = sys.simulate { a := a, d := dse₂.st (dse₁.st d) }.f s₀ n

theorem AP.Defense.wf_ofList {ds : List Defense} (H : ∀ d ∈ ds, d.WF) (h₀ : CompatibleList ds) : (ofList ds).WF

theorem AP.Defense.compatible'_of_compatible {d₁ d₂ : Defense} {p : State → Prop} (h : d₁.Compatible d₂) : Compatible' p d₁ d₂

theorem AP.Defense.compatible'_of_compatibleList' {p : State → Prop} {ds : List Defense} {d₁ d₂ : Defense} (h : CompatibleList' p ds) (h₁ : d₁ ∈ ds) (h₂ : d₂ ∈ ds) : Compatible' (fun (s : State) => (∀ d ∈ ds, d.cnd s) ∧ p s) d₁ d₂

theorem AP.Defense.compatible'_of_compatibleList {ds : List Defense} {d₁ d₂ : Defense} (h : CompatibleList ds) (h₁ : d₁ ∈ ds) (h₂ : d₂ ∈ ds) : Compatible' (fun (s : State) => ∀ d ∈ ds, d.cnd s) d₁ d₂

theorem AP.Defense.compatibleList_iff_getElem {ds : List Defense} : CompatibleList ds ↔ ∀ (i j : ℕ) (h₁ : i < j) (h₂ : j < ds.length), Compatible' (fun (s : State) => ∀ d ∈ ds, d.cnd s) ds[i] ds[j]

theorem AP.Defense.compatibleList_iff_getElem! {ds : List Defense} : CompatibleList ds ↔ ∀ (i j : ℕ), i < j → j < ds.length → Compatible' (fun (s : State) => ∀ d ∈ ds, d.cnd s) ds[i]! ds[j]!

theorem AP.Defense.f_st_eq_of_f_eq_none {dse : Defense} {s : State} {d : DStrat} (h : dse.f s = none) : (dse.st d).f s = d.f s

theorem AP.Defense.f_st_eq_of_f_eq_some {dse : Defense} {s : State} {d : DStrat} {p : PointZ} (h : dse.f s = some p) : (dse.st d).f s = p

@[simp]

theorem AP.Defense.f_ofList_eq_none_iff {ds : List Defense} {s : State} : (ofList ds).f s = none ↔ ∀ d ∈ ds, d.f s = none