def AP.State.HasDReenter (s : State) (fsp : FSP) : Prop

Equations

• s.HasDReenter fsp = ∀ (a : AP.AStrat), a.WF → s.aForallWinsDisj fsp a → ∃ (d : AP.DStrat), d.WF ∧ ∃ (n : ℕ) (sd : AP.State), AP.DState sd ∧ AP.sys.simulate { a := a, d := d }.f s n = (sd, 0) ∧ sd.aPos = s.aPos

theorem AP.AState.hasDReenter_of_not_aHwsDisj_insert_aPos {s : State} {fsp : FSP} [hs : AState s] (h₁ : ¬s.aHwsDisj (fsp.insert 1 s.aPos)) : s.HasDReenter fsp

theorem AP.AState.not_aHwsDisj_insert_aPos_of_hasDReenter {s : State} {fsp : FSP} [hs : AState s] (h : s.HasDReenter fsp) : ¬s.aHwsDisj (fsp.insert 1 s.aPos)

theorem AP.AState.hasDReenter_iff_not_aHwsDisj_insert_aPos {s : State} {fsp : FSP} [hs : AState s] : s.HasDReenter fsp ↔ ¬s.aHwsDisj (fsp.insert 1 s.aPos)

theorem AP.AState.hasDReenter_of_taken_subset {fsp : FSP} {s s' : State} [hs : AState s] [hs' : AState s'] (h : s.HasDReenter fsp) (hpw : s'.pw = s.pw) (ht : s'.aTurn = s.aTurn) (hpa : s'.aPos = s.aPos) (h₁ : s.taken ⊆ s'.taken) : s'.HasDReenter fsp

theorem AP.AState.aHwsDisj_insert_one_aPos {s : State} {fsp : FSP} [hs : AState s] (h : s.aHwsDisj fsp) : s.aHwsDisj (fsp.insert 1 s.aPos)

theorem AP.DState.forall_tr_of_aHwsDisj {s : State} {fsp : FSP} [hs : DState s] (h : s.aHwsDisj fsp) (p : PointZ) (s' : State) : sys.tr s p = some s' → s'.aHwsDisj fsp.next

theorem AP.DState.forall_tr_exi_aForallWinsDisj_of_aHwsDisj {s : State} {fsp : FSP} [hs : DState s] (h : s.aHwsDisj fsp) (p : PointZ) : ∃ (a : AStrat), a.WF ∧ ∀ (s' : State), sys.tr s p = some s' → s'.aForallWinsDisj fsp.next a

theorem AP.DState.aHwsDisj_iff_forall_tr_exi_aForallWinsDisj {s : State} {fsp : FSP} [hs : DState s] : s.aHwsDisj fsp ↔ ∀ (p : PointZ), ∃ (a : AStrat), a.WF ∧ ∀ (s' : State), sys.tr s p = some s' → s'.aForallWinsDisj fsp.next a

theorem AP.DState.aHwsDisj_iff_forall_tr {s : State} {fsp : FSP} [hs : DState s] : s.aHwsDisj fsp ↔ ∀ (p : PointZ) (s' : State), sys.tr s p = some s' → s'.aHwsDisj fsp.next

theorem AP.DState.aHwsDisj_insert_two_aPos {s : State} {fsp : FSP} [hs : DState s] (h : s.aHwsDisj fsp) : s.aHwsDisj (fsp.insert 2 s.aPos)

theorem AP.State.aHwsDisj_insert_two_aPos {s : State} {fsp : FSP} [hs : sys.WF s] (h : s.aHwsDisj fsp) : s.aHwsDisj (fsp.insert 2 s.aPos)