structure AP.WFCnd (s : State) : Prop

• aPos_not_mem_taken : s.aPos ∉ s.taken
• taken_ne_empty_of_aTurn : s.aTurn = true → s.taken ≠ ∅
• size_taken_eq_one_of_aTurn_and_pw_eq_zero : s.aTurn = true → s.pw = 0 → s.taken.size = 1
• exi_aMove_of_not_aTurn_and_taken_ne_empty : s.aTurn = false → s.taken ≠ ∅ → ∃ (p : PointZ), (s.aMove p).isSome = true

@[simp]

theorem AP.State.wfCnd_of_wf {s : State} [hs : sys.WF s] : WFCnd s

theorem AP.WFCnd.pw_ne_zero_of_not_aTurn_and_taken_ne_empty {s : State} (h : WFCnd s) (ht : s.aTurn = false) (h₁ : s.taken ≠ ∅) : s.pw ≠ 0

theorem AP.State.exi_hist_wf_of_not_aTurn_and_taken_eq_empty {s : State} (ht : s.aTurn = false) (h₁ : s.taken = ∅) : ∃ (hist : List PointZ), sys.WF (s.setHist hist)

theorem AP.State.exi_hist_wf_of_exi_p2_aux {s : State} {p₁ p₂ : PointZ} {taken : Set' PointZ} (h₁ : p₁ ≠ p₂) (h₃ : p₁ ∉ taken) (h₄ : p₂ ∉ taken) (h₂ : Point.dist p₁ p₂ ≤ ↑s.pw) (hn : (s.taken.size * 2 - if s.aTurn = true then 1 else 0) = 0) (h₆ : s.aPos = if Odd (s.taken.size + if s.aTurn = true then 0 else 1) then p₁ else p₂) (h₅ : s.taken ⊆ taken) (H : s.aTurn = true → s.taken ≠ ∅) : ∃ (hist : List PointZ), sys.WF (s.setHist hist)

theorem AP.State.exi_hist_wf_of_exi_p2 {s : State} {p₁ p₂ : PointZ} (hpw : s.pw ≠ 0) (h₁ : p₁ ≠ p₂) (h₂ : Point.dist p₁ p₂ ≤ ↑s.pw) (h₃ : p₁ ∉ s.taken) (h₄ : p₂ ∉ s.taken) (ha : s.aPos = p₁) (ht : s.aTurn = false) (h₇ : Even s.taken.size) : ∃ (hist : List PointZ), sys.WF (s.setHist hist)

theorem AP.State.exi_hist_wf_of_wfCnd_and_not_aTurn {s : State} (h : WFCnd s) (ht : s.aTurn = false) : ∃ (hist : List PointZ), sys.WF (s.setHist hist)

theorem AP.State.exi_hist_wf_of_wfCnd {s : State} (h : WFCnd s) : ∃ (hist : List PointZ), sys.WF (s.setHist hist)

theorem AP.State.exi_with_taken_of_wfCnd {s : State} {taken : Set' PointZ} (h : WFCnd { pw := s.pw, taken := taken, aPos := s.aPos, aTurn := s.aTurn, hist := s.hist }) : ∃ (s' : State), sys.WF s' ∧ s'.pw = s.pw ∧ s'.aTurn = s.aTurn ∧ s'.aPos = s.aPos ∧ s'.taken = taken

theorem AP.State.exi_erase_taken {s : State} {p : PointZ} (h : WFCnd { pw := s.pw, taken := s.taken.erase p, aPos := s.aPos, aTurn := s.aTurn, hist := s.hist }) : ∃ (s' : State), sys.WF s' ∧ s'.pw = s.pw ∧ s'.aTurn = s.aTurn ∧ s'.aPos = s.aPos ∧ s'.taken = s.taken.erase p

theorem AP.State.exi_taken_diff {s : State} {ps : Set' PointZ} (h : WFCnd { pw := s.pw, taken := s.taken \ ps, aPos := s.aPos, aTurn := s.aTurn, hist := s.hist }) : ∃ (s' : State), sys.WF s' ∧ s'.pw = s.pw ∧ s'.aTurn = s.aTurn ∧ s'.aPos = s.aPos ∧ s'.taken = s.taken \ ps