def AP.Alt₁.Point.toAlt : Point → PointZ

Equations

• { x := x_1, y := y }.toAlt = { x := x_1, y := y }

def AP.Alt₁.Point.ofAlt : PointZ → Point

Equations

• AP.Alt₁.Point.ofAlt { x := x_1, y := y } = { x := x_1, y := y }

def AP.Alt₁.State.aTurn (s : State) : Bool

Equations

• s.aTurn = decide (Odd s.history.length)

def AP.Alt₁.Board.ofAlt (s : AP.State) : Board

Equations

• AP.Alt₁.Board.ofAlt s = { squares := Set.univ \ AP.Alt₁.Point.ofAlt '' s.taken.toSet, A := AP.Alt₁.Point.ofAlt s.aPos }

noncomputable def AP.Alt₁.Board.toAlt (b : Board) (pw : ℕ) (aTurn : Bool) (hist : List PointZ) : AP.State

Equations

• b.toAlt pw aTurn hist = { pw := pw, taken := Set'.ofSet ((fun (x : AP.Alt₁.Point) => x.toAlt) '' (Set.univ \ b.squares)), aPos := b.A.toAlt, aTurn := aTurn, hist := hist }

noncomputable def AP.Alt₁.State.toAlt (s : State) (pw : ℕ) (hist : List PointZ) : AP.State

Equations

• s.toAlt pw hist = s.board.toAlt pw s.aTurn hist

def AP.Alt₁.State.ofAlt (s : AP.State) (act : Prop) (hist : List Board) : State

Equations

• AP.Alt₁.State.ofAlt s act hist = { board := AP.Alt₁.Board.ofAlt s, history := hist, act := act }

noncomputable def AP.Alt₁.Board.toAltH? (b : Board) (pw : ℕ) (aTurn : Bool) : Option AP.State

Equations

• b.toAltH? pw aTurn = choose? fun (s' : AP.State) => AP.sys.WF s' ∧ b.toAlt pw aTurn s'.hist = s'

noncomputable def AP.Alt₁.State.toAltH? (s : State) (pw : ℕ) : Option AP.State

Equations

• s.toAltH? pw = s.board.toAltH? pw s.aTurn

noncomputable def AP.Alt₁.Board.toAltH (b : Board) (pw : ℕ) (aTurn : Bool) : AP.State

Equations

• b.toAltH pw aTurn = (b.toAltH? pw aTurn).getd

noncomputable def AP.Alt₁.State.toAltH (s : State) (pw : ℕ) : AP.State

Equations

• s.toAltH pw = (s.toAltH? pw).getd

def AP.Alt₁.State.setHist (s : State) (hist : List Board) : State

Equations

• s.setHist hist = { board := s.board, history := hist, act := s.act }

def AP.Alt₁.State.FinSq (s : State) : Prop

Equations

• s.FinSq = (Set.univ \ s.board.squares).Finite

def AP.Alt₁.ASeekCnd (pw : ℕ) (r : State → State → Prop) (s : State) (m : ValidAMove pw s.board) : Prop

Equations

• AP.Alt₁.ASeekCnd pw r s m = r s (AP.Alt₁.applyAMove s m.m)

def AP.Alt₁.DSeekCnd (r : State → State → Prop) (s : State) (m : ValidDMove s.board) : Prop

Equations

• AP.Alt₁.DSeekCnd r s m = r s (AP.Alt₁.applyDMove s m.m)

noncomputable def AP.Alt₁.aSeek (pw : ℕ) (r : State → State → Prop) : Option (A pw)

Equations

• AP.Alt₁.aSeek pw r = choose? fun (a : AP.Alt₁.A pw) => ∀ (s : AP.Alt₁.State) (h₁ : s.act) (h₂ : AP.Alt₁.AHasValidMove pw s.board), (∃ (m : AP.Alt₁.ValidAMove pw s.board), AP.Alt₁.ASeekCnd pw r s m) → AP.Alt₁.ASeekCnd pw r s (a.f s h₁ h₂)

noncomputable def AP.Alt₁.dSeek (r : State → State → Prop) : Option D

Equations

• AP.Alt₁.dSeek r = choose? fun (d : AP.Alt₁.D) => ∀ (s : AP.Alt₁.State) (h₁ : s.act), (∃ (m : AP.Alt₁.ValidDMove s.board), AP.Alt₁.DSeekCnd r s m) → AP.Alt₁.DSeekCnd r s (d.f s h₁)

def AP.Alt₁.Board.aHws (b : Board) (pw : ℕ) (aTurn : Bool) : Prop

Equations

• b.aHws pw aTurn = (b.toAltH pw aTurn).aHws

def AP.Alt₁.Board.dHws (b : Board) (pw : ℕ) (aTurn : Bool) : Prop

Equations

• b.dHws pw aTurn = (b.toAltH pw aTurn).dHws

def AP.Alt₁.State.aHws (s : State) (pw : ℕ) : Prop

Equations

• s.aHws pw = s.board.aHws pw s.aTurn

def AP.Alt₁.State.dHws (s : State) (pw : ℕ) : Prop

Equations

• s.dHws pw = s.board.dHws pw s.aTurn

noncomputable def AP.Alt₁.Board.dwn (b : Board) (pw : ℕ) (aTurn : Bool) : ℕ

Equations

• b.dwn pw aTurn = (b.toAltH pw aTurn).dwn

noncomputable def AP.Alt₁.State.dwn (s : State) (pw : ℕ) : ℕ

Equations

• s.dwn pw = s.board.dwn pw s.aTurn

noncomputable def AP.Alt₁.aOptimal (pw : ℕ) : Option (A pw)

Equations

• AP.Alt₁.aOptimal pw = AP.Alt₁.aSeek pw fun (x s' : AP.Alt₁.State) => s'.aHws pw

noncomputable def AP.Alt₁.dOptimal (pw : ℕ) : Option D

Equations

• AP.Alt₁.dOptimal pw = AP.Alt₁.dSeek fun (s s' : AP.Alt₁.State) => s'.dHws pw ∧ s'.dwn pw < s.dwn pw

class AP.Alt₁.State.WF (pw : outParam ℕ) (s : State) : Prop

• wf : ∃ (a : A pw) (d : D) (n : ℕ) (g : Game pw), (initGame a d state₀).play n = g ∧ (g.s = s ∨ ∃ (h : g.s.act), (playDMoveAt g h).s = s)

class AP.Alt₁.AState (pw : outParam ℕ) (s : State) extends AP.Alt₁.State.WF pw s : Prop

• wf : ∃ (a : A pw) (d : D) (n : ℕ) (g : Game pw), (initGame a d state₀).play n = g ∧ (g.s = s ∨ ∃ (h : g.s.act), (playDMoveAt g h).s = s)
• ht : s.aTurn = true

class AP.Alt₁.DState (pw : outParam ℕ) (s : State) extends AP.Alt₁.State.WF pw s : Prop

• wf : ∃ (a : A pw) (d : D) (n : ℕ) (g : Game pw), (initGame a d state₀).play n = g ∧ (g.s = s ∨ ∃ (h : g.s.act), (playDMoveAt g h).s = s)
• ht : s.aTurn = false

noncomputable def AP.Alt₁.A.set {pw : ℕ} (a : A pw) (s : State) (ref : A pw) : A pw

Equations

• a.set s ref = { f := fun (s₁ : AP.Alt₁.State) (h₁ : s₁.act) (h₂ : AP.Alt₁.AHasValidMove pw s₁.board) => if s₁ = s then ref.f s₁ h₁ h₂ else a.f s₁ h₁ h₂ }

noncomputable def AP.Alt₁.D.set (d : D) (s : State) (ref : D) : D

Equations

• d.set s ref = { f := fun (s₁ : AP.Alt₁.State) (h : s₁.act) => if s₁ = s then ref.f s₁ h else d.f s₁ h }