>    restart; read `d:/Aek/Rook/FSRook.txt`;

`Welcome to ShortRook, a Maple package written by`

`Thotsaporn (Aek) Thanatipanonda with help from his`

`brother Thotsaphon. First Version: September, 1st, 2013 `

`It accompanies the article: `

`Rook Endgame Problem in Chess `

` by Thotsaporn (Aek) Thanatipanonda`

`available from authors' website`

>    Help(Part2);

` Function: SymInduction(k);`

` Input: the width of the board `

` Output: the detials proof of the conjectures `

` of standard positions on a k by n board`

` `

` Try  

>    SymInduction(3);

`####For `, f(1,1,1), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 1, `to Column`, 2

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, UpRight

Subcase, 1, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,1)(a,b-1),
Subcase, 1, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,1)(a,b-1),

Subcase, 2, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,1)(a-1,b),
Subcase, 2, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,1)(a-1,b),

Subcase, 3, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,1)(a-2,b+1),
Subcase, 3, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,1)(a-2,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`####For `, f(1,1,2), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`
`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, Up

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-2,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-2,b+1),

`max of these cases is`, a+b-1, moves

`Colclusion black lasts at most`, a+b,

`####For `, f(1,1,3), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 2

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, UpRight

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,2,3)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,2,3)(a,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,3)(a,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,3)(a,b-1),

Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,3)(a-1,b),
Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,3)(a-1,b),

Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,2,3)(a-2,b+1),
Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,2,3)(a-2,b+1),

Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,3)(a-2,b+1),
Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,3)(a-2,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`####For `, f(1,2,2), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move King in direction`, UpRight

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-2,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-2,b+1),

`max of these cases is`, a+b-1, moves

`Colclusion black lasts at most`, a+b,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, UpLeft

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,1,2)(a,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-2,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,1,2)(a-2,b+1),

`max of these cases is`, a+b-1, moves

`Colclusion black lasts at most`, a+b,

`####For `, f(1,2,3), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 1

Subcase, 1, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,1)(a+1,b-1),
Subcase, 1, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,1)(a+1,b-1),

Subcase, 2, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,1)(a,b),
Subcase, 2, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,1)(a,b),

Subcase, 3, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,1)(a-1,b+1),
Subcase, 3, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,1)(a-1,b+1),

`max of these cases is`, a+1+b, moves

`Colclusion black lasts at most`, a+b+2,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, Up

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,2,3)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,2,3)(a,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,3)(a,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(2,2,3)(a,b-1),

Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,3)(a-1,b),
Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(2,2,3)(a-1,b),

Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,2,3)(a-2,b+1),
Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,2,3)(a-2,b+1),

Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,3)(a-2,b+1),
Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(2,2,3)(a-2,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+1+b,

`####For `, f(1,3,2), `####`

`#################`

`Case a is`, 0

`#################`

`White chooses to move Rook from Column`, 2, `to Column`, 1

`Black is checkmated`

`Colclusion black lasts at most`, 1,

`#################`

`Case a is even and a >=`, 1

`#################`

`White chooses to move King in direction`, Up

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-2,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-2,b+1),

`max of these cases is`, a+b-1, moves

`Colclusion black lasts at most`, a+b,

`#################`

`Case a is odd and a>=`, 1

`#################`

`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`
`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+1+b,

`####For `, f(1,3,3), `####`

`#################`

`Case a is`, 0

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 1

`Black is checkmated`

`Colclusion black lasts at most`, 1,

`#################`

`Case a is even and a >=`, 1

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 2

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),

`max of these cases is`, a+1+b, moves

`Colclusion black lasts at most`, a+b+2,

`#################`

`Case a is odd and a>=`, 1

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 2

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(1,3,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),
Subcase, 2, `:black's move is`, Down, `which by induction assumption takes at most`, f_(1,3,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+1+b,

`####For `, f(2,1,1), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 1, `to Column`, 2

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),

Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),
Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),

Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),
Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),

Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),
Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),

`max of these cases is`, a+1+b, moves

`Colclusion black lasts at most`, a+b+2,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move Rook from Column`, 1, `to Column`, 2

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),

Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),
Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),

Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),
Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),

Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),
Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),

`max of these cases is`, a+1+b, moves

`Colclusion black lasts at most`, a+b+2,

`####For `, f(2,1,3), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 3, `to Column`, 2

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,2)(a+1,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,1,2)(a+1,b-1),

Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),
Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,2)(a,b),

Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),
Subcase, 4, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,1,2)(a,b),

Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),
Subcase, 5, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,2)(a-1,b+1),

Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),
Subcase, 6, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,1,2)(a-1,b+1),

`max of these cases is`, a+1+b, moves

`Colclusion black lasts at most`, a+b+2,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, Up

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,3)(a,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,1,3)(a,b-1),

Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,1,3)(a,b-1),
Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,1,3)(a,b-1),

Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,3)(a-1,b),
Subcase, 3, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,1,3)(a-1,b),

Subcase, 4, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,3)(a-2,b+1),
Subcase, 4, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,1,3)(a-2,b+1),

Subcase, 5, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,1,3)(a-2,b+1),
Subcase, 5, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,1,3)(a-2,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+1+b,

`####For `, f(2,2,1), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to move Rook from Column`, 1, `to Column`, 2

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a+1,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a+1,b-1),
Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a+1,b-1),

Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a+1,b-1),
Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a+1,b-1),

Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a,b),
Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a,b),

Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a,b),
Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a,b),

Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b+1),
Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b+1),

Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-1,b+1),
Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-1,b+1),

Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b+1),
Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, UpRight

Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,3,1)(a,b-1),
Subcase, 1, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,3,1)(a,b-1),

Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,3,1)(a,b-1),
Subcase, 2, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,3,1)(a,b-1),

Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,3,1)(a-1,b),
Subcase, 3, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,3,1)(a-1,b),

Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,3,1)(a-2,b+1),
Subcase, 4, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,3,1)(a-2,b+1),

Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,3,1)(a-2,b+1),
Subcase, 5, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,3,1)(a-2,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`####For `, f(2,2,2), `####`

`#################`

`Case a is even and a >=`, 2

`#################`

`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`
`White chooses to do the waiting move by`, `moving his Rook one square up`, `or down the same column`

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a+1,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a+1,b-1),

Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a+1,b-1),
Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a+1,b-1),

Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a+1,b-1),
Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a+1,b-1),

Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a,b),
Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a,b),

Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a,b),
Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a,b),

Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b+1),
Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b+1),

Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-1,b+1),
Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-1,b+1),

Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b+1),
Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b+1),

`max of these cases is`, a+b, moves

`Colclusion black lasts at most`, a+b+1,

`#################`

`Case a is odd and a>=`, 2

`#################`

`White chooses to move King in direction`, Up

Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a,b-1),
Subcase, 1, `:black's move is`, UpLeft, `which by induction assumption takes at most`, f_(1,2,2)(a,b-1),

Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a,b-1),
Subcase, 2, `:black's move is`, Up, `which by induction assumption takes at most`, f_(2,2,2)(a,b-1),

Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a,b-1),
Subcase, 3, `:black's move is`, UpRight, `which by induction assumption takes at most`, f_(3,2,2)(a,b-1),

Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b),
Subcase, 4, `:black's move is`, Left, `which by induction assumption takes at most`, f_(1,2,2)(a-1,b),

Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b),
Subcase, 5, `:black's move is`, Right, `which by induction assumption takes at most`, f_(3,2,2)(a-1,b),

Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-2,b+1),
Subcase, 6, `:black's move is`, DownLeft, `which by induction assumption takes at most`, f_(1,2,2)(a-2,b+1),

Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-2,b+1),
Subcase, 7, `:black's move is`, Down, `which by induction assumption takes at most`, f_(2,2,2)(a-2,b+1),

Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-2,b+1),
Subcase, 8, `:black's move is`, DownRight, `which by induction assumption takes at most`, f_(3,2,2)(a-2,b+1),

`max of these cases is`, a+b-1, moves

`Colclusion black lasts at most`, a+b,

`The proof is done.`

>