Theorem: ############################# Let , f[1], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], B, T $ a[4], B, T $ a[5], F] ############################# Then we have: f[1](0, 0, 0, 0, 0) = [-4] f[1](a[1], 0, 0, 0, 0) = [3 a[1] - 3], 1 <= a[1] f[1](0, 1, 0, 0, 0) = [-1/2] f[1](a[1], 1, 0, 0, 0) = [3 a[1] - 1/4], 1 <= a[1] f[1](a[1], a[2], 0, 0, 0) = [{[3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 2]}], 2 <= a[2], 0 <= a[1] f[1](0, 0, 1, 0, 0) = [-1] f[1](a[1], 0, 1, 0, 0) = [3 a[1] - 1/2], 1 <= a[1] f[1](a[1], a[2], 1, 0, 0) = [3 a[1] + 2 a[2]], 1 <= a[2], 0 <= a[1] f[1](a[1], a[2], a[3], 0, 0) = [3 a[1] + 2 a[2] + a[3] - 1], 2 <= a[3], 0 <= a[1], 0 <= a[2] f[1](0, 0, 0, 1, 0) = [-2] f[1](a[1], 0, 0, 1, 0) = [3 a[1] - 1], 1 <= a[1] f[1](a[1], a[2], 0, 1, 0) = [3 a[1] + 2 a[2] - 1], 1 <= a[2], 0 <= a[1] f[1](0, 0, 1, 1, 0) = [1/2] f[1](a[1], 0, 1, 1, 0) = [3 a[1] + 3/4], 1 <= a[1] f[1](a[1], a[2], 1, 1, 0) = [{[3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}], 1 <= a[2], 0 <= a[1] f[1](a[1], a[2], a[3], 1, 0) = [{[3 a[1] + 2 a[2] + a[3]]}, {[3 a[1] + 2 a[2] + a[3]]}], 2 <= a[3], 0 <= a[1], 0 <= a[2] f[1](0, 0, 0, 2, 0) = [{[{[0]}, {[0]}]}, {[0]}] f[1](a[1], 0, 0, 2, 0) = [{[{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1]]}], 1 <= a[1] f[1](a[1], a[2], 0, 2, 0) = [{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}], 1 <= a[2], 0 <= a[1] f[1](a[1], a[2], a[3], 2, 0) = [ {[{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]}, {[3 a[1] + 2 a[2] + a[3]]}], 1 <= a[3], 0 <= a[1], 0 <= a[2] f[1](a[1], a[2], a[3], a[4], 0) = [ {[{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 2]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]} , {[3 a[1] + 2 a[2] + a[3]]}], 3 <= a[4], 0 <= a[1], 0 <= a[2], 0 <= a[3] f[1](0, 0, 0, 0, 1) = [-3] f[1](a[1], 0, 0, 0, 1) = [3 a[1] - 2], 1 <= a[1] f[1](0, 1, 0, 0, 1) = [1/2] f[1](a[1], 1, 0, 0, 1) = [3 a[1] + 3/4], 1 <= a[1] f[1](a[1], a[2], 0, 0, 1) = [{[3 a[1] + 2 a[2] - 1]}, {[3 a[1] + 2 a[2] - 1]}], 2 <= a[2], 0 <= a[1] f[1](0, 0, 1, 0, 1) = [0] f[1](a[1], 0, 1, 0, 1) = [3 a[1] + 1/2], 1 <= a[1] f[1](a[1], a[2], a[3], 0, 1) = [3 a[1] + 2 a[2] + a[3]], 2 <= a[3], 0 <= a[1], 0 <= a[2] f[1](a[1], a[2], 1, 0, 1) = [3 a[1] + 2 a[2] + 1], 1 <= a[2], 0 <= a[1] f[1](0, 0, 0, 1, 1) = [{[0]}, {[0]}] f[1](a[1], 0, 0, 1, 1) = [{[4 a[1]]}, {[3 a[1] + 1/2]}], 1 <= a[1] f[1](a[1], a[2], a[3], 1, 1) = [{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}], 1 <= a[3], 0 <= a[1], 0 <= a[2] f[1](a[1], a[2], 0, 1, 1) = [{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}], 1 <= a[2], 0 <= a[1] f[1](a[1], a[2], a[3], a[4], 1) = [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 1]}, {[3 a[1] + 2 a[2] + a[3] + 1]}], 2 <= a[4], 0 <= a[1], 0 <= a[2], 0 <= a[3] f[1](a[1], a[2], a[3], a[4], a[5]) = [4 a[1] + 3 a[2] + 2 a[3] + a[4]], 2 <= a[5], 0 <= a[1], 0 <= a[2], 0 <= a[3], 0 <= a[4] Theorem: ############################# Let , f[2], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], B, T $ a[4], F, B] ############################# Then we have: f[2](0, 0, 0, 0) = [-3] f[2](a[1], 0, 0, 0) = [3 a[1] - 5/2], 1 <= a[1] f[2](a[1], a[2], 0, 0) = [3 a[1] + 2 a[2] - 2], 1 <= a[2], 0 <= a[1] f[2](0, 0, 1, 0) = [-1/2] f[2](a[1], 0, 1, 0) = [3 a[1] - 1/4], 1 <= a[1] f[2](a[1], a[2], 1, 0) = [{[3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2]]}], 1 <= a[2], 0 <= a[1] f[2](a[1], a[2], a[3], 0) = [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[3 a[1] + 2 a[2] + a[3] - 1]}], 2 <= a[3], 0 <= a[1], 0 <= a[2] f[2](0, 0, 0, 1) = [-1] f[2](a[1], 0, 0, 1) = [3 a[1] - 1/2], 1 <= a[1] f[2](a[1], a[2], a[3], 1) = [3 a[1] + 2 a[2] + a[3]], 1 <= a[3], 0 <= a[1], 0 <= a[2] f[2](a[1], a[2], 0, 1) = [3 a[1] + 2 a[2]], 1 <= a[2], 0 <= a[1] f[2](a[1], a[2], a[3], a[4]) = [3 a[1] + 2 a[2] + a[3]], 2 <= a[4], 0 <= a[1], 0 <= a[2], 0 <= a[3] Theorem: ############################# Let , f[3], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], F, B, B] ############################# Then we have: f[3](a[1], 0, 0) = [3 a[1] - 2], 0 <= a[1] f[3](a[1], a[2], 0) = [3 a[1] + 2 a[2] - 3/2], 1 <= a[2], 0 <= a[1] f[3](a[1], a[2], a[3]) = [3 a[1] + 2 a[2] + a[3] - 1], 1 <= a[3], 0 <= a[1], 0 <= a[2] Theorem: ############################# Let , f[4], be the value of , [T $ a[1], B, T $ a[2], F, B, B, B] ############################# Then we have: f[4](a[1], a[2]) = [3 a[1] + 2 a[2] - 1], 0 <= a[1], 0 <= a[2] Theorem: ############################# Let , f[5], be the value of , [T $ a[1], F, B, B, B, B] ############################# Then we have: f[5](a[1]) = [3 a[1]], 0 <= a[1] Now we will prove by applying induction to each of the above conjectures one by one. If everything is true, we get the complete proofs. ############### ##Begin to prove## ############### ########## #, f[1], # ########## For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 0, 0, 0) + [0]}] = , [{}, {[-3]}] = , [-4] For the domain, {a[1] = 1, a[5] = 0, a[2] = 0, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 1, 0, 0, 0)}, {f[2](1, 0, 0, 0) + [0]}] = , [{[-1/2]}, {[1/2]}] = , [0] For the domain, {a[5] = 0, a[2] = 0, 2 <= a[1], a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, 0, 0, 0)}, {f[2](a[1], 0, 0, 0) + [0]}] = , [{[3 a[1] - 13/4]}, {[3 a[1] - 5/2]}] = , [3 a[1] - 3] For the domain, {a[1] = 0, a[5] = 0, a[2] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 0, 0)}, {f[2](0, 1, 0, 0) + [0]}] = , [{[-1]}, {[0]}] = , [-1/2] For the domain, {a[5] = 0, a[2] = 1, a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 1, 0, 0), f[1](a[1] - 1, 2, 0, 0, 0)}, {f[2](a[1], 1, 0, 0) + [0]}] = , [{[3 a[1] - 1/2], [{[3 a[1] - 1]}, {[3 a[1] - 1]}]}, {[3 a[1]]}] = , [3 a[1] - 1/4] For the domain, {a[5] = 0, 2 <= a[2], a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 0, 0, 0), f[1](a[1], a[2] - 1, 1, 0, 0)}, {f[2](a[1], a[2], 0, 0) + [0]}] = , [ {[{[3 a[1] - 3 + 2 a[2]]}, {[3 a[1] - 3 + 2 a[2]]}], [3 a[1] + 2 a[2] - 2]} , {[3 a[1] + 2 a[2] - 2]}] = , [{[3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 2]}] For the domain, {a[1] = 0, a[5] = 0, 2 <= a[2], a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, 1, 0, 0)}, {f[2](0, a[2], 0, 0) + [0]}] = , [{[-2 + 2 a[2]]}, {[-2 + 2 a[2]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 1, 0)}, {f[2](0, 0, 1, 0) + [0]}] = , [{[-2]}, {[-1/2]}] = , [-1] For the domain, {a[5] = 0, a[2] = 0, a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 0, 1, 0), f[1](a[1] - 1, 1, 1, 0, 0)}, {f[2](a[1], 0, 1, 0) + [0]}] = , [{[3 a[1] - 1]}, {[3 a[1] - 1/4]}] = , [3 a[1] - 1/2] For the domain, {a[5] = 0, 1 <= a[2], a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, 1, 0), f[1](a[1], a[2] - 1, 2, 0, 0), f[1](a[1] - 1, a[2] + 1, 1, 0, 0)}, {f[2](a[1], a[2], 1, 0) + [0]}] = , [{[3 a[1] + 2 a[2] - 1]}, {[{[3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2]]}]}] = , [3 a[1] + 2 a[2]] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 2, 0, 0), f[1](0, a[2], 0, 1, 0)}, {f[2](0, a[2], 1, 0) + [0]}] = , [{[-1 + 2 a[2]]}, {[{[2 a[2]]}, {[2 a[2]]}]}] = , [2 a[2]] For the domain, {a[5] = 0, 1 <= a[2], a[4] = 0, a[3] = 2, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 2, 0, 0), f[1](a[1], a[2] - 1, 3, 0, 0), f[1](a[1], a[2], 1, 1, 0)}, {f[2](a[1], a[2], 2, 0) + [0]}] = , [{[%1, %1], [3 a[1] + 2 a[2]]}, {[%1, %1]}] %1 := {[3 a[1] + 2 a[2] + 1]} = , [3 a[1] + 2 a[2] + 1] For the domain, {a[5] = 0, 3 <= a[3], 1 <= a[2], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, a[3], 0, 0), f[1](a[1], a[2] - 1, a[3] + 1, 0, 0), f[1](a[1], a[2], a[3] - 1, 1, 0)}, {f[2](a[1], a[2], a[3], 0) + [0]}] = , [{[3 a[1] - 2 + 2 a[2] + a[3]], [%1, %1]}, {[%1, %1]}] %1 := {[3 a[1] + 2 a[2] + a[3] - 1]} = , [3 a[1] + 2 a[2] + a[3] - 1] For the domain, {a[5] = 0, a[2] = 0, a[4] = 0, a[3] = 2, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, 2, 0, 0), f[1](a[1], 0, 1, 1, 0)}, {f[2](a[1], 0, 2, 0) + [0]}] = , [{[3 a[1] + 3/4], [3 a[1]]}, {[{[3 a[1] + 1]}, {[3 a[1] + 1]}]}] = , [3 a[1] + 1] For the domain, {a[5] = 0, a[2] = 0, 3 <= a[3], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, a[3] - 1, 1, 0), f[1](a[1] - 1, 1, a[3], 0, 0)}, {f[2](a[1], 0, a[3], 0) + [0]}] = , [{[%1, %1], [3 a[1] - 2 + a[3]]}, {[%1, %1]}] %1 := {[3 a[1] - 1 + a[3]]} = , [3 a[1] - 1 + a[3]] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], a[4] = 0, a[3] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 3, 0, 0), f[1](0, a[2], 1, 1, 0)}, {f[2](0, a[2], 2, 0) + [0]}] = , [{[%1, %1], [2 a[2]]}, {[%1, %1]}] %1 := {[1 + 2 a[2]]} = , [1 + 2 a[2]] For the domain, {a[1] = 0, a[5] = 0, 3 <= a[3], 1 <= a[2], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, a[3] + 1, 0, 0), f[1](0, a[2], a[3] - 1, 1, 0)}, {f[2](0, a[2], a[3], 0) + [0]}] = , [{[%1, %1], [-2 + 2 a[2] + a[3]]}, {[%1, %1]}] %1 := {[-1 + 2 a[2] + a[3]]} = , [-1 + 2 a[2] + a[3]] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[4] = 0, a[3] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 1, 0)}, {f[2](0, 0, 2, 0) + [0]}] = , [{[1/2]}, {[{[1]}, {[1]}]}] = , [1] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, 3 <= a[3], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, 1, 0)}, {f[2](0, 0, a[3], 0) + [0]}] = , [{[{[a[3] - 1]}, {[a[3] - 1]}]}, {[{[a[3] - 1]}, {[a[3] - 1]}]}] = , [a[3] - 1] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 0, 1)}, {f[2](0, 0, 0, 1) + [0]}] = , [{[-3]}, {[-1]}] = , [-2] For the domain, {a[5] = 0, a[2] = 0, a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 0, 0, 1), f[1](a[1] - 1, 1, 0, 1, 0)}, {f[2](a[1], 0, 0, 1) + [0]}] = , [{[3 a[1] - 2]}, {[3 a[1] - 1/2]}] = , [3 a[1] - 1] For the domain, {a[5] = 0, a[2] = 1, a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](a[1], 0, 1, 1, 0), f[1](a[1], 1, 0, 0, 1), f[1](a[1] - 1, 2, 0, 1, 0)} , {f[2](a[1], 1, 0, 1) + [0]}] = , [{[3 a[1] + 3/4], [3 a[1]]}, {[3 a[1] + 2]}] = , [3 a[1] + 1] For the domain, {a[5] = 0, 2 <= a[2], a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 0, 1, 0), f[1](a[1], a[2] - 1, 1, 1, 0), f[1](a[1], a[2], 0, 0, 1)}, {f[2](a[1], a[2], 0, 1) + [0]}] = , [ {[{[3 a[1] + 2 a[2] - 1]}, {[3 a[1] + 2 a[2] - 1]}], [3 a[1] + 2 a[2] - 2]} , {[3 a[1] + 2 a[2]]}] = , [3 a[1] + 2 a[2] - 1] For the domain, {a[1] = 0, a[5] = 0, a[2] = 1, a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 1, 0), f[1](0, 1, 0, 0, 1)}, {f[2](0, 1, 0, 1) + [0]}] = , [{[1/2]}, {[2]}] = , [1] For the domain, {a[1] = 0, a[5] = 0, 2 <= a[2], a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2], 0, 0, 1), f[1](0, a[2] - 1, 1, 1, 0)}, {f[2](0, a[2], 0, 1) + [0]}] = , [{[{[-1 + 2 a[2]]}, {[-1 + 2 a[2]]}]}, {[2 a[2]]}] = , [-1 + 2 a[2]] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[3] = 1, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 0, 1), f[1](0, 0, 0, 2, 0)}, {f[2](0, 0, 1, 1) + [0]}] = , [{[0], [{[{[0]}, {[0]}]}, {[0]}]}, {[1]}] = , [1/2] For the domain, {a[5] = 0, a[2] = 0, a[3] = 1, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](a[1] - 1, 1, 1, 1, 0), f[1](a[1], 0, 0, 2, 0), f[1](a[1], 0, 1, 0, 1)} , {f[2](a[1], 0, 1, 1) + [0]}] = , [{[{[3 a[1]]}, {[3 a[1]]}], [{[{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1]]}], [3 a[1] + 1/2]}, {[3 a[1] + 1]}] = , [3 a[1] + 3/4] For the domain, {a[5] = 0, 1 <= a[2], a[3] = 1, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 1, 0, 1), f[1](a[1], a[2] - 1, 2, 1, 0), f[1](a[1] - 1, a[2] + 1, 1, 1, 0), f[1](a[1], a[2], 0, 2, 0)}, {f[2](a[1], a[2], 1, 1) + [0]}] = , [{[{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}], [{[3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2]]}], [3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}] = , [{[3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], a[3] = 1, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](0, a[2], 0, 2, 0), f[1](0, a[2] - 1, 2, 1, 0), f[1](0, a[2], 1, 0, 1)} , {f[2](0, a[2], 1, 1) + [0]}] = , [{[{[{[3 a[2]]}, {[2 a[2] + 1]}]}, {[2 a[2]]}], [2 a[2] + 1], [{[2 a[2]]}, {[2 a[2]]}]}, {[2 a[2] + 1]}] = , [{[2 a[2] + 1]}, {[2 a[2] + 1]}] For the domain, {a[5] = 0, 1 <= a[2], 2 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], a[3], 0, 1), f[1](a[1], a[2], a[3] - 1, 2, 0), f[1](a[1], a[2] - 1, a[3] + 1, 1, 0), f[1](a[1] - 1, a[2] + 1, a[3], 1, 0)}, {f[2](a[1], a[2], a[3], 1) + [0]}] = , [{[{[{[4 a[1] + 3 a[2] + 2 a[3] - 2]}, {[3 a[1] + 2 a[2] + a[3]]}]}, %1], [3 a[1] + 2 a[2] + a[3]], [%1, %1]}, {[3 a[1] + 2 a[2] + a[3]]}] %1 := {[3 a[1] + 2 a[2] + a[3] - 1]} = , [{[3 a[1] + 2 a[2] + a[3]]}, {[3 a[1] + 2 a[2] + a[3]]}] For the domain, {a[5] = 0, a[2] = 0, 2 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, a[3], 1, 0), f[1](a[1], 0, a[3] - 1, 2, 0), f[1](a[1], 0, a[3], 0, 1)}, {f[2](a[1], 0, a[3], 1) + [0]}] = , [{[{[{[4 a[1] - 2 + 2 a[3]]}, {[3 a[1] + a[3]]}]}, {[3 a[1] - 1 + a[3]]}], [{[3 a[1] - 1 + a[3]]}, {[3 a[1] - 1 + a[3]]}], [3 a[1] + a[3]]}, {[3 a[1] + a[3]]}] = , [{[3 a[1] + a[3]]}, {[3 a[1] + a[3]]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], 2 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3] - 1, 2, 0), f[1](0, a[2] - 1, a[3] + 1, 1, 0), f[1](0, a[2], a[3], 0, 1)}, {f[2](0, a[2], a[3], 1) + [0]}] = , [{[2 a[2] + a[3]], [{[{[-2 + 3 a[2] + 2 a[3]]}, {[2 a[2] + a[3]]}]}, {[-1 + 2 a[2] + a[3]]}], [{[-1 + 2 a[2] + a[3]]}, {[-1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}] = , [{[2 a[2] + a[3]]}, {[2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, 2 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3], 0, 1), f[1](0, 0, a[3] - 1, 2, 0)}, {f[2](0, 0, a[3], 1) + [0]}] = , [{[a[3]], [{[{[-2 + 2 a[3]]}, {[a[3]]}]}, {[a[3] - 1]}]}, {[a[3]]}] = , [{[a[3]]}, {[a[3]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[4] = 2, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 1, 1)}, {f[2](0, 0, 0, 2) + [0]}] = , [{[{[0]}, {[0]}]}, {[0]}] For the domain, {a[5] = 0, a[2] = 0, a[4] = 2, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 0, 1, 1), f[1](a[1] - 1, 1, 0, 2, 0)}, {f[2](a[1], 0, 0, 2) + [0]}] = , [{[{[{[4 a[1] - 1]}, {[3 a[1]]}]}, {[3 a[1] - 1]}], [{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1]]}] = , [{[{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1]]}] For the domain, {a[5] = 0, 1 <= a[2], a[4] = 2, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 0, 2, 0), f[1](a[1], a[2], 0, 1, 1), f[1](a[1], a[2] - 1, 1, 2, 0)}, {f[2](a[1], a[2], 0, 2) + [0]}] = , [{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}], [{[{[4 a[1] - 1 + 3 a[2]]}, {[3 a[1] + 2 a[2]]}]}, {[3 a[1] + 2 a[2] - 1]}] }, {[3 a[1] + 2 a[2]]}] = , [{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], a[4] = 2, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 1, 2, 0), f[1](0, a[2], 0, 1, 1)}, {f[2](0, a[2], 0, 2) + [0]}] = , [{[{[{[-1 + 3 a[2]]}, {[2 a[2]]}]}, {[-1 + 2 a[2]]}], [{[3 a[2]]}, {[1 + 2 a[2]]}]}, {[2 a[2]]}] = , [{[{[3 a[2]]}, {[1 + 2 a[2]]}]}, {[2 a[2]]}] For the domain, {a[5] = 0, 1 <= a[2], a[4] = 2, 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, a[3], 2, 0), f[1](a[1], a[2] - 1, a[3] + 1, 2, 0), f[1](a[1], a[2], a[3] - 1, 3, 0), f[1](a[1], a[2], a[3], 1, 1)}, {f[2](a[1], a[2], a[3], 2) + [0]}] = , [{[{[{[4 a[1] - 1 + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3]]}]}, {[3 a[1] + 2 a[2] + a[3] - 1]}], [{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]}, {[3 a[1] + 2 a[2] + a[3]]}] = , [{[{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]}, {[3 a[1] + 2 a[2] + a[3]]}] For the domain, {a[5] = 0, a[2] = 0, a[4] = 2, 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], 1, 1), f[1](a[1], 0, a[3] - 1, 3, 0), f[1](a[1] - 1, 1, a[3], 2, 0)}, {f[2](a[1], 0, a[3], 2) + [0]}] = , [{[{[4 a[1] + 2 a[3]]}, {[3 a[1] + 1 + a[3]]}], [{[{[4 a[1] - 1 + 2 a[3]]}, {[3 a[1] + a[3]]}]}, {[3 a[1] - 1 + a[3]]}]}, {[3 a[1] + a[3]]}] = , [{[{[4 a[1] + 2 a[3]]}, {[3 a[1] + 1 + a[3]]}]}, {[3 a[1] + a[3]]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], a[4] = 2, 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], 1, 1), f[1](0, a[2], a[3] - 1, 3, 0), f[1](0, a[2] - 1, a[3] + 1, 2, 0)}, {f[2](0, a[2], a[3], 2) + [0]}] = , [{[{[3 a[2] + 2 a[3]]}, {[1 + 2 a[2] + a[3]]}], [{[{[-1 + 3 a[2] + 2 a[3]]}, {[2 a[2] + a[3]]}]}, {[-1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}] = , [{[{[3 a[2] + 2 a[3]]}, {[1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, a[4] = 2, 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3], 1, 1), f[1](0, 0, a[3] - 1, 3, 0)}, {f[2](0, 0, a[3], 2) + [0]}] = , [ {[{[2 a[3]]}, {[a[3] + 1]}], [{[{[-1 + 2 a[3]]}, {[a[3]]}]}, {[a[3] - 1]}]} , {[a[3]]}] = , [{[{[2 a[3]]}, {[a[3] + 1]}]}, {[a[3]]}] For the domain, {a[5] = 0, 1 <= a[2], 3 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, a[3] + 1, a[4], 0), f[1](a[1] - 1, a[2] + 1, a[3], a[4], 0), f[1](a[1], a[2], a[3] - 1, a[4] + 1, 0), f[1](a[1], a[2], a[3], a[4] - 1, 1)}, {f[2](a[1], a[2], a[3], a[4]) + [0]}] = , [{[ {[{[4 a[1] - 3 + 3 a[2] + 2 a[3] + a[4]]}, {[3 a[1] + 2 a[2] + a[3]]}]}, {[3 a[1] + 2 a[2] + a[3] - 1]}], [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 2]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]}, {[3 a[1] + 2 a[2] + a[3]]}] = , [ {[{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 2]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]} , {[3 a[1] + 2 a[2] + a[3]]}] For the domain, {a[5] = 0, 1 <= a[2], 3 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, 1, a[4], 0), f[1](a[1], a[2], 0, a[4] - 1, 1), f[1](a[1] - 1, a[2] + 1, 0, a[4], 0)}, {f[2](a[1], a[2], 0, a[4]) + [0]}] = , [{[{[{[4 a[1] - 3 + 3 a[2] + a[4]]}, {[3 a[1] + 2 a[2]]}]}, {[3 a[1] + 2 a[2] - 1]}], [{[4 a[1] + 3 a[2] - 2 + a[4]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}] = , [{[{[4 a[1] + 3 a[2] - 2 + a[4]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}] For the domain, {a[5] = 0, a[2] = 0, 3 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], a[4] - 1, 1), f[1](a[1], 0, a[3] - 1, a[4] + 1, 0), f[1](a[1] - 1, 1, a[3], a[4], 0)}, {f[2](a[1], 0, a[3], a[4]) + [0]}] = , [{[{[4 a[1] - 2 + 2 a[3] + a[4]]}, {[3 a[1] + 1 + a[3]]}], [ {[{[4 a[1] - 3 + 2 a[3] + a[4]]}, {[3 a[1] + a[3]]}]}, {[3 a[1] - 1 + a[3]]}]}, {[3 a[1] + a[3]]}] = , [{[{[4 a[1] - 2 + 2 a[3] + a[4]]}, {[3 a[1] + 1 + a[3]]}]}, {[3 a[1] + a[3]]}] For the domain, {a[5] = 0, a[2] = 0, 3 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, 0, a[4], 0), f[1](a[1], 0, 0, a[4] - 1, 1)}, {f[2](a[1], 0, 0, a[4]) + [0]}] = , [{[{[4 a[1] - 2 + a[4]]}, {[3 a[1] + 1]}], [{[{[4 a[1] - 3 + a[4]]}, {[3 a[1]]}]}, {[3 a[1] - 1]}]}, {[3 a[1]]}] = , [{[{[4 a[1] - 2 + a[4]]}, {[3 a[1] + 1]}]}, {[3 a[1]]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], 3 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3] - 1, a[4] + 1, 0), f[1](0, a[2], a[3], a[4] - 1, 1), f[1](0, a[2] - 1, a[3] + 1, a[4], 0)}, {f[2](0, a[2], a[3], a[4]) + [0]}] = , [{[{[{[-3 + 3 a[2] + 2 a[3] + a[4]]}, {[2 a[2] + a[3]]}]}, {[-1 + 2 a[2] + a[3]]}], [{[-2 + 3 a[2] + 2 a[3] + a[4]]}, {[1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}] = , [{[{[-2 + 3 a[2] + 2 a[3] + a[4]]}, {[1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[5] = 0, 1 <= a[2], 3 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2], 0, a[4] - 1, 1), f[1](0, a[2] - 1, 1, a[4], 0)}, {f[2](0, a[2], 0, a[4]) + [0]}] = , [{[{[-2 + 3 a[2] + a[4]]}, {[1 + 2 a[2]]}], [{[{[-3 + 3 a[2] + a[4]]}, {[2 a[2]]}]}, {[-1 + 2 a[2]]}]}, {[2 a[2]]}] = , [{[{[-2 + 3 a[2] + a[4]]}, {[1 + 2 a[2]]}]}, {[2 a[2]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, 3 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3] - 1, a[4] + 1, 0), f[1](0, 0, a[3], a[4] - 1, 1)}, {f[2](0, 0, a[3], a[4]) + [0]}] = , [{[{[{[-3 + 2 a[3] + a[4]]}, {[a[3]]}]}, {[a[3] - 1]}], [{[-2 + 2 a[3] + a[4]]}, {[a[3] + 1]}]}, {[a[3]]}] = , [{[{[-2 + 2 a[3] + a[4]]}, {[a[3] + 1]}]}, {[a[3]]}] For the domain, {a[1] = 0, a[5] = 0, a[2] = 0, 3 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, a[4] - 1, 1)}, {f[2](0, 0, 0, a[4]) + [0]}] = , [{[{[-2 + a[4]]}, {[1]}]}, {[0]}] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 0, 0, 0) + [1]}] = , [{}, {[-2]}] = , [-3] For the domain, {a[2] = 0, a[5] = 1, a[1] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 1, 0, 0, 1)}, {f[2](1, 0, 0, 0) + [1]}] = , [{[1/2]}, {[3/2]}] = , [1] For the domain, {2 <= a[1], a[2] = 0, a[5] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, 0, 0, 1)}, {f[2](a[1], 0, 0, 0) + [1]}] = , [{[3 a[1] - 9/4]}, {[3 a[1] - 3/2]}] = , [3 a[1] - 2] For the domain, {a[1] = 0, a[2] = 1, a[5] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 0, 1)}, {f[2](0, 1, 0, 0) + [1]}] = , [{[0]}, {[1]}] = , [1/2] For the domain, {a[2] = 1, a[5] = 1, a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 1, 0, 1), f[1](a[1] - 1, 2, 0, 0, 1)}, {f[2](a[1], 1, 0, 0) + [1]}] = , [{[{[3 a[1]]}, {[3 a[1]]}], [3 a[1] + 1/2]}, {[3 a[1] + 1]}] = , [3 a[1] + 3/4] For the domain, {2 <= a[2], a[5] = 1, a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 0, 0, 1), f[1](a[1], a[2] - 1, 1, 0, 1)}, {f[2](a[1], a[2], 0, 0) + [1]}] = , [ {[3 a[1] + 2 a[2] - 1], [{[3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 2]}]} , {[3 a[1] + 2 a[2] - 1]}] = , [{[3 a[1] + 2 a[2] - 1]}, {[3 a[1] + 2 a[2] - 1]}] For the domain, {a[1] = 0, 2 <= a[2], a[5] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, 1, 0, 1)}, {f[2](0, a[2], 0, 0) + [1]}] = , [{[-1 + 2 a[2]]}, {[-1 + 2 a[2]]}] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 1, 1)}, {f[2](0, 0, 1, 0) + [1]}] = , [{[{[0]}, {[0]}]}, {[1/2]}] = , [0] For the domain, {a[2] = 0, a[5] = 1, a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 0, 1, 1), f[1](a[1] - 1, 1, 1, 0, 1)}, {f[2](a[1], 0, 1, 0) + [1]}] = , [{[3 a[1]], [{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1] + 3/4]}] = , [3 a[1] + 1/2] For the domain, {a[5] = 1, 1 <= a[2], 2 <= a[3], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, a[3] + 1, 0, 1), f[1](a[1] - 1, a[2] + 1, a[3], 0, 1), f[1](a[1], a[2], a[3] - 1, 1, 1)}, {f[2](a[1], a[2], a[3], 0) + [1]}] = , [{[{[4 a[1] + 3 a[2] + 2 a[3] - 2]}, %1], [3 a[1] + 2 a[2] + a[3] - 1]}, {[%1, %1]}] %1 := {[3 a[1] + 2 a[2] + a[3]]} = , [3 a[1] + 2 a[2] + a[3]] For the domain, {a[2] = 0, a[5] = 1, 2 <= a[3], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, a[3] - 1, 1, 1), f[1](a[1] - 1, 1, a[3], 0, 1)}, {f[2](a[1], 0, a[3], 0) + [1]}] = , [{[{[4 a[1] - 2 + 2 a[3]]}, {[3 a[1] + a[3]]}], [3 a[1] - 1 + a[3]]}, {[{[3 a[1] + a[3]]}, {[3 a[1] + a[3]]}]}] = , [3 a[1] + a[3]] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], 2 <= a[3], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, a[3] + 1, 0, 1), f[1](0, a[2], a[3] - 1, 1, 1)}, {f[2](0, a[2], a[3], 0) + [1]}] = , [{[{[-2 + 3 a[2] + 2 a[3]]}, {[2 a[2] + a[3]]}], [-1 + 2 a[2] + a[3]]}, {[{[2 a[2] + a[3]]}, {[2 a[2] + a[3]]}]}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, 2 <= a[3], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, 1, 1)}, {f[2](0, 0, a[3], 0) + [1]}] = , [{[{[-2 + 2 a[3]]}, {[a[3]]}]}, {[{[a[3]]}, {[a[3]]}]}] = , [a[3]] For the domain, {a[5] = 1, 1 <= a[2], a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 1, 0, 1), f[1](a[1], a[2] - 1, 2, 0, 1), f[1](a[1], a[2], 0, 1, 1)}, {f[2](a[1], a[2], 1, 0) + [1]}] = , [{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}], [3 a[1] + 2 a[2]]}, {[{[3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}]}] = , [3 a[1] + 2 a[2] + 1] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 2, 0, 1), f[1](0, a[2], 0, 1, 1)}, {f[2](0, a[2], 1, 0) + [1]}] = , [{[2 a[2]], [{[3 a[2]]}, {[2 a[2] + 1]}]}, {[{[2 a[2] + 1]}, {[2 a[2] + 1]}]}] = , [2 a[2] + 1] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 0, 2)}, {f[2](0, 0, 0, 1) + [1]}] = , [{[0]}, {[0]}] For the domain, {a[2] = 0, a[5] = 1, a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], 0, 0, 0, 2), f[1](a[1] - 1, 1, 0, 1, 1)}, {f[2](a[1], 0, 0, 1) + [1]}] = , [{[{[4 a[1] - 1]}, {[3 a[1]]}], [4 a[1]]}, {[3 a[1] + 1/2]}] = , [{[4 a[1]]}, {[3 a[1] + 1/2]}] For the domain, {a[5] = 1, 1 <= a[2], 1 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], a[3], 0, 2), f[1](a[1], a[2], a[3] - 1, 2, 1), f[1](a[1], a[2] - 1, a[3] + 1, 1, 1), f[1](a[1] - 1, a[2] + 1, a[3], 1, 1)}, {f[2](a[1], a[2], a[3], 1) + [1]}] = , [{[{[4 a[1] - 1 + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3]]}], [4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}] = , [{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}] For the domain, {a[2] = 0, a[5] = 1, 1 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, a[3], 1, 1), f[1](a[1], 0, a[3], 0, 2), f[1](a[1], 0, a[3] - 1, 2, 1)}, {f[2](a[1], 0, a[3], 1) + [1]}] = , [{[{[4 a[1] - 1 + 2 a[3]]}, {[3 a[1] + a[3]]}], [4 a[1] + 2 a[3]]}, {[3 a[1] + 1 + a[3]]}] = , [{[4 a[1] + 2 a[3]]}, {[3 a[1] + 1 + a[3]]}] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], 1 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, a[3] + 1, 1, 1), f[1](0, a[2], a[3], 0, 2), f[1](0, a[2], a[3] - 1, 2, 1)}, {f[2](0, a[2], a[3], 1) + [1]}] = , [{[{[-1 + 3 a[2] + 2 a[3]]}, {[2 a[2] + a[3]]}], [3 a[2] + 2 a[3]]}, {[1 + 2 a[2] + a[3]]}] = , [{[3 a[2] + 2 a[3]]}, {[1 + 2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, 1 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3] - 1, 2, 1), f[1](0, 0, a[3], 0, 2)}, {f[2](0, 0, a[3], 1) + [1]}] = , [{[{[-1 + 2 a[3]]}, {[a[3]]}], [2 a[3]]}, {[a[3] + 1]}] = , [{[2 a[3]]}, {[a[3] + 1]}] For the domain, {a[5] = 1, 1 <= a[2], a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 0, 1, 1), f[1](a[1], a[2] - 1, 1, 1, 1), f[1](a[1], a[2], 0, 0, 2)}, {f[2](a[1], a[2], 0, 1) + [1]}] = , [{[{[4 a[1] - 1 + 3 a[2]]}, {[3 a[1] + 2 a[2]]}], [4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}] = , [{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 1, 1, 1), f[1](0, a[2], 0, 0, 2)}, {f[2](0, a[2], 0, 1) + [1]}] = , [{[{[-1 + 3 a[2]]}, {[2 a[2]]}], [3 a[2]]}, {[1 + 2 a[2]]}] = , [{[3 a[2]]}, {[1 + 2 a[2]]}] For the domain, {a[5] = 1, 1 <= a[2], 2 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], a[3] - 1, a[4] + 1, 1), f[1](a[1], a[2] - 1, a[3] + 1, a[4], 1), f[1](a[1] - 1, a[2] + 1, a[3], a[4], 1), f[1](a[1], a[2], a[3], a[4] - 1, 2)}, {f[2](a[1], a[2], a[3], a[4]) + [1]}] = , [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 1], [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 2]}, {[3 a[1] + 2 a[2] + a[3]]}]}, {[3 a[1] + 2 a[2] + a[3] + 1]}] = , [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 1]}, {[3 a[1] + 2 a[2] + a[3] + 1]}] For the domain, {a[5] = 1, 1 <= a[2], 2 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, 0, a[4], 1), f[1](a[1], a[2], 0, a[4] - 1, 2), f[1](a[1], a[2] - 1, 1, a[4], 1)}, {f[2](a[1], a[2], 0, a[4]) + [1]}] = , [{[{[4 a[1] + 3 a[2] - 2 + a[4]]}, {[3 a[1] + 2 a[2]]}], [4 a[1] + 3 a[2] - 1 + a[4]]}, {[3 a[1] + 2 a[2] + 1]}] = , [{[4 a[1] + 3 a[2] - 1 + a[4]]}, {[3 a[1] + 2 a[2] + 1]}] For the domain, {a[2] = 0, a[5] = 1, 2 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3] - 1, a[4] + 1, 1), f[1](a[1] - 1, 1, a[3], a[4], 1), f[1](a[1], 0, a[3], a[4] - 1, 2)}, {f[2](a[1], 0, a[3], a[4]) + [1]}] = , [{[4 a[1] - 1 + 2 a[3] + a[4]], [{[4 a[1] - 2 + 2 a[3] + a[4]]}, {[3 a[1] + a[3]]}]}, {[3 a[1] + 1 + a[3]]} ] = , [{[4 a[1] - 1 + 2 a[3] + a[4]]}, {[3 a[1] + 1 + a[3]]}] For the domain, {a[2] = 0, a[5] = 1, 2 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, 0, a[4], 1), f[1](a[1], 0, 0, a[4] - 1, 2)}, {f[2](a[1], 0, 0, a[4]) + [1]}] = , [ {[4 a[1] - 1 + a[4]], [{[4 a[1] - 2 + a[4]]}, {[3 a[1]]}]}, {[3 a[1] + 1]}] = , [{[4 a[1] - 1 + a[4]]}, {[3 a[1] + 1]}] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], 2 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], a[4] - 1, 2), f[1](0, a[2] - 1, a[3] + 1, a[4], 1), f[1](0, a[2], a[3] - 1, a[4] + 1, 1)} , {f[2](0, a[2], a[3], a[4]) + [1]}] = , [{[{[-2 + 3 a[2] + 2 a[3] + a[4]]}, {[2 a[2] + a[3]]}], [-1 + 3 a[2] + 2 a[3] + a[4]]}, {[1 + 2 a[2] + a[3]]}] = , [{[-1 + 3 a[2] + 2 a[3] + a[4]]}, {[1 + 2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[5] = 1, 1 <= a[2], 2 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 1, a[4], 1), f[1](0, a[2], 0, a[4] - 1, 2)}, {f[2](0, a[2], 0, a[4]) + [1]}] = , [{[-1 + 3 a[2] + a[4]], [{[-2 + 3 a[2] + a[4]]}, {[2 a[2]]}]}, {[1 + 2 a[2]]}] = , [{[-1 + 3 a[2] + a[4]]}, {[1 + 2 a[2]]}] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, 2 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3] - 1, a[4] + 1, 1), f[1](0, 0, a[3], a[4] - 1, 2)}, {f[2](0, 0, a[3], a[4]) + [1]}] = , [{[{[-2 + 2 a[3] + a[4]]}, {[a[3]]}], [-1 + 2 a[3] + a[4]]}, {[a[3] + 1]}] = , [{[-1 + 2 a[3] + a[4]]}, {[a[3] + 1]}] For the domain, {a[1] = 0, a[2] = 0, a[5] = 1, 2 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, a[4] - 1, 2)}, {f[2](0, 0, 0, a[4]) + [1]}] = , [{[a[4] - 1]}, {[1]}] For the domain, {1 <= a[4], 1 <= a[2], 2 <= a[5], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, a[2] + 1, a[3], a[4], a[5]), f[1](a[1], a[2] - 1, a[3] + 1, a[4], a[5]), f[1](a[1], a[2], a[3] - 1, a[4] + 1, a[5]), f[1](a[1], a[2], a[3], a[4] - 1, a[5] + 1)}, {}] = , [{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 1]}, {}] = , [4 a[1] + 3 a[2] + 2 a[3] + a[4]] For the domain, {1 <= a[2], 2 <= a[5], a[4] = 0, 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, a[3] + 1, 0, a[5]), f[1](a[1], a[2], a[3] - 1, 1, a[5]), f[1](a[1] - 1, a[2] + 1, a[3], 0, a[5])}, {}] = , [{[4 a[1] + 3 a[2] + 2 a[3] - 1]}, {}] = , [4 a[1] + 3 a[2] + 2 a[3]] For the domain, {1 <= a[4], 1 <= a[2], 2 <= a[5], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, a[4] - 1, a[5] + 1), f[1](a[1], a[2] - 1, 1, a[4], a[5]), f[1](a[1] - 1, a[2] + 1, 0, a[4], a[5])}, {}] = , [{[4 a[1] + 3 a[2] - 1 + a[4]]}, {}] = , [4 a[1] + 3 a[2] + a[4]] For the domain, {1 <= a[2], 2 <= a[5], a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 0, 0, a[5]), f[1](a[1], a[2] - 1, 1, 0, a[5])}, {}] = , [{[4 a[1] + 3 a[2] - 1]}, {}] = , [4 a[1] + 3 a[2]] For the domain, {a[2] = 0, 1 <= a[4], 2 <= a[5], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, a[3], a[4], a[5]), f[1](a[1], 0, a[3] - 1, a[4] + 1, a[5]), f[1](a[1], 0, a[3], a[4] - 1, a[5] + 1)}, {}] = , [{[4 a[1] - 1 + 2 a[3] + a[4]]}, {}] = , [4 a[1] + 2 a[3] + a[4]] For the domain, {a[2] = 0, 2 <= a[5], a[4] = 0, 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3] - 1, 1, a[5]), f[1](a[1] - 1, 1, a[3], 0, a[5])}, {}] = , [{[4 a[1] - 1 + 2 a[3]]}, {}] = , [4 a[1] + 2 a[3]] For the domain, {a[2] = 0, 1 <= a[4], 2 <= a[5], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, 0, a[4], a[5]), f[1](a[1], 0, 0, a[4] - 1, a[5] + 1)}, {}] = , [{[4 a[1] - 1 + a[4]]}, {}] = , [4 a[1] + a[4]] For the domain, {a[2] = 0, 2 <= a[5], a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, 0, 0, a[5])}, {}] = , [{[4 a[1] - 1]}, {}] = , [4 a[1]] For the domain, {a[1] = 0, 1 <= a[4], 1 <= a[2], 2 <= a[5], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, a[3] + 1, a[4], a[5]), f[1](0, a[2], a[3] - 1, a[4] + 1, a[5]), f[1](0, a[2], a[3], a[4] - 1, a[5] + 1)}, {}] = , [{[-1 + 3 a[2] + 2 a[3] + a[4]]}, {}] = , [3 a[2] + 2 a[3] + a[4]] For the domain, {a[1] = 0, 1 <= a[2], 2 <= a[5], a[4] = 0, 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, a[3] + 1, 0, a[5]), f[1](0, a[2], a[3] - 1, 1, a[5])}, {}] = , [{[-1 + 3 a[2] + 2 a[3]]}, {}] = , [3 a[2] + 2 a[3]] For the domain, {a[1] = 0, 1 <= a[4], 1 <= a[2], 2 <= a[5], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, 1, a[4], a[5]), f[1](0, a[2], 0, a[4] - 1, a[5] + 1)}, {}] = , [{[-1 + 3 a[2] + a[4]]}, {}] = , [3 a[2] + a[4]] For the domain, {a[1] = 0, 1 <= a[2], 2 <= a[5], a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, 1, 0, a[5])}, {}] = , [{[-1 + 3 a[2]]}, {}] = , [3 a[2]] For the domain, {a[1] = 0, a[2] = 0, 1 <= a[4], 2 <= a[5], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](0, 0, a[3], a[4] - 1, a[5] + 1), f[1](0, 0, a[3] - 1, a[4] + 1, a[5])} , {}] = , [{[-1 + 2 a[3] + a[4]]}, {}] = , [2 a[3] + a[4]] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[5], a[4] = 0, 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, 1, a[5])}, {}] = , [{[-1 + 2 a[3]]}, {}] = , [2 a[3]] For the domain, {a[1] = 0, a[2] = 0, 1 <= a[4], 2 <= a[5], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, a[4] - 1, a[5] + 1)}, {}] = , [{[a[4] - 1]}, {}] = , [a[4]] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[5], a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] ########## #, f[2], # ########## For the domain, {a[1] = 0, a[2] = 0, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[3](0, 0, 0) + [0]}] = , [{}, {[-2]}] = , [-3] For the domain, {a[2] = 0, a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, 1, 0, 0)}, {f[3](a[1], 0, 0) + [0]}] = , [{[3 a[1] - 3]}, {[3 a[1] - 2]}] = , [3 a[1] - 5/2] For the domain, {a[2] = 1, a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], 0, 1, 0), f[2](a[1] - 1, 2, 0, 0)}, {f[3](a[1], 1, 0) + [0]}] = , [{[3 a[1] - 1/4], [3 a[1] - 1]}, {[3 a[1] + 1/2]}] = , [3 a[1]] For the domain, {2 <= a[2], a[4] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[2](a[1] - 1, a[2] + 1, 0, 0), f[2](a[1], a[2] - 1, 1, 0)}, {f[3](a[1], a[2], 0) + [0]}] = , [ {[{[3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 2]}], [3 a[1] - 3 + 2 a[2]]} , {[3 a[1] + 2 a[2] - 3/2]}] = , [3 a[1] + 2 a[2] - 2] For the domain, {a[1] = 0, a[2] = 1, a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 1, 0)}, {f[3](0, 1, 0) + [0]}] = , [{[-1/2]}, {[1/2]}] = , [0] For the domain, {a[1] = 0, 2 <= a[2], a[4] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2] - 1, 1, 0)}, {f[3](0, a[2], 0) + [0]}] = , [{[{[-2 + 2 a[2]]}, {[-2 + 2 a[2]]}]}, {[- 3/2 + 2 a[2]]}] = , [-2 + 2 a[2]] For the domain, {a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 0, 1)}, {f[3](0, 0, 1) + [0]}] = , [{[-1]}, {[0]}] = , [-1/2] For the domain, {a[2] = 0, a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, 1, 1, 0), f[2](a[1], 0, 0, 1)}, {f[3](a[1], 0, 1) + [0]}] = , [{[3 a[1] - 1/2], [{[3 a[1] - 1]}, {[3 a[1] - 1]}]}, {[3 a[1]]}] = , [3 a[1] - 1/4] For the domain, {1 <= a[2], a[3] = 1, a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], a[2] - 1, 2, 0), f[2](a[1] - 1, a[2] + 1, 1, 0), f[2](a[1], a[2], 0, 1)}, {f[3](a[1], a[2], 1) + [0]}] = , [{[{[3 a[1] + 2 a[2] - 1]}, {[3 a[1] + 2 a[2] - 1]}], [3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2]]}] = , [{[3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2]]}] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 1, a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2] - 1, 2, 0), f[2](0, a[2], 0, 1)}, {f[3](0, a[2], 1) + [0]}] = , [{[{[-1 + 2 a[2]]}, {[-1 + 2 a[2]]}], [2 a[2]]}, {[2 a[2]]}] = , [{[2 a[2]]}, {[2 a[2]]}] For the domain, {1 <= a[2], 2 <= a[3], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, a[3], 0), f[2](a[1], a[2] - 1, a[3] + 1, 0), f[2](a[1], a[2], a[3] - 1, 1)}, {f[3](a[1], a[2], a[3]) + [0]}] = , [{[{[3 a[1] - 2 + 2 a[2] + a[3]]}, {[3 a[1] - 2 + 2 a[2] + a[3]]}], [3 a[1] + 2 a[2] + a[3] - 1]}, {[3 a[1] + 2 a[2] + a[3] - 1]}] = , [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[3 a[1] + 2 a[2] + a[3] - 1]}] For the domain, {a[2] = 0, 2 <= a[3], a[4] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[2](a[1] - 1, 1, a[3], 0), f[2](a[1], 0, a[3] - 1, 1)}, {f[3](a[1], 0, a[3]) + [0]}] = , [{[3 a[1] - 1 + a[3]], [{[3 a[1] - 2 + a[3]]}, {[3 a[1] - 2 + a[3]]}]}, {[3 a[1] - 1 + a[3]]}] = , [{[3 a[1] - 1 + a[3]]}, {[3 a[1] - 1 + a[3]]}] For the domain, {a[1] = 0, 1 <= a[2], 2 <= a[3], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[2](0, a[2] - 1, a[3] + 1, 0), f[2](0, a[2], a[3] - 1, 1)}, {f[3](0, a[2], a[3]) + [0]}] = , [{[-1 + 2 a[2] + a[3]], [{[-2 + 2 a[2] + a[3]]}, {[-2 + 2 a[2] + a[3]]}]}, {[-1 + 2 a[2] + a[3]]}] = , [{[-1 + 2 a[2] + a[3]]}, {[-1 + 2 a[2] + a[3]]}] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[3], a[4] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, a[3] - 1, 1)}, {f[3](0, 0, a[3]) + [0]}] = , [{[a[3] - 1]}, {[a[3] - 1]}] For the domain, {a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 0, 0) + [0]}, {f[3](0, 0, 0) + [2]}] = , [{[-4]}, {[0]}] = , [-1] For the domain, {a[2] = 0, a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[2](a[1] - 1, 1, 0, 1), f[1](a[1], 0, 0, 0, 0) + [0]}, {f[3](a[1], 0, 0) + [2]}] = , [{[3 a[1] - 3], [3 a[1] - 1]}, {[3 a[1]]}] = , [3 a[1] - 1/2] For the domain, {1 <= a[2], a[3] = 1, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 1, 0, 0) + [0], f[2](a[1], a[2], 0, 2), f[2](a[1] - 1, a[2] + 1, 1, 1), f[2](a[1], a[2] - 1, 2, 1)}, {f[3](a[1], a[2], 1) + [2]}] = , [{[3 a[1] + 2 a[2]]}, {[3 a[1] + 2 a[2] + 2]}] = , [3 a[1] + 2 a[2] + 1] For the domain, {1 <= a[2], 2 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, a[3], 1), f[2](a[1], a[2], a[3] - 1, 2), f[2](a[1], a[2] - 1, a[3] + 1, 1), f[1](a[1], a[2], a[3], 0, 0) + [0]}, {f[3](a[1], a[2], a[3]) + [2]}] = , [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[3 a[1] + 2 a[2] + a[3] + 1]}] = , [3 a[1] + 2 a[2] + a[3]] For the domain, {a[2] = 0, a[3] = 1, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[2](a[1], 0, 0, 2), f[1](a[1], 0, 1, 0, 0) + [0], f[2](a[1] - 1, 1, 1, 1)} , {f[3](a[1], 0, 1) + [2]}] = , [{[3 a[1] - 1/2], [3 a[1]]}, {[3 a[1] + 2]}] = , [3 a[1] + 1] For the domain, {a[2] = 0, 2 <= a[3], a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], 0, 0) + [0], f[2](a[1], 0, a[3] - 1, 2), f[2](a[1] - 1, 1, a[3], 1)}, {f[3](a[1], 0, a[3]) + [2]}] = , [{[3 a[1] - 1 + a[3]]}, {[3 a[1] + 1 + a[3]]}] = , [3 a[1] + a[3]] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 1, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[2](0, a[2], 0, 2), f[1](0, a[2], 1, 0, 0) + [0], f[2](0, a[2] - 1, 2, 1)} , {f[3](0, a[2], 1) + [2]}] = , [{[2 a[2]]}, {[2 a[2] + 2]}] = , [2 a[2] + 1] For the domain, {a[1] = 0, 1 <= a[2], 2 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], 0, 0) + [0], f[2](0, a[2], a[3] - 1, 2), f[2](0, a[2] - 1, a[3] + 1, 1)}, {f[3](0, a[2], a[3]) + [2]}] = , [{[-1 + 2 a[2] + a[3]]}, {[1 + 2 a[2] + a[3]]}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 0, 2), f[1](0, 0, 1, 0, 0) + [0]}, {f[3](0, 0, 1) + [2]}] = , [{[0], [-1]}, {[2]}] = , [1] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[3], a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, 0, a[3], 0, 0) + [0], f[2](0, 0, a[3] - 1, 2)}, {f[3](0, 0, a[3]) + [2]}] = , [{[a[3] - 1]}, {[a[3] + 1]}] = , [a[3]] For the domain, {a[2] = 1, a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[2](a[1], 0, 1, 1), f[1](a[1], 1, 0, 0, 0) + [0], f[2](a[1] - 1, 2, 0, 1)} , {f[3](a[1], 1, 0) + [2]}] = , [{[3 a[1] - 1/4], [3 a[1] + 1]}, {[3 a[1] + 5/2]}] = , [3 a[1] + 2] For the domain, {2 <= a[2], a[3] = 0, a[4] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, 0, 0) + [0], f[2](a[1] - 1, a[2] + 1, 0, 1), f[2](a[1], a[2] - 1, 1, 1)}, {f[3](a[1], a[2], 0) + [2]}] = , [ {[3 a[1] + 2 a[2] - 1], [{[3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 2]}]} , {[3 a[1] + 2 a[2] + 1/2]}] = , [3 a[1] + 2 a[2]] For the domain, {a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 1, 1), f[1](0, 1, 0, 0, 0) + [0]}, {f[3](0, 1, 0) + [2]}] = , [{[-1/2], [1]}, {[5/2]}] = , [2] For the domain, {a[1] = 0, 2 <= a[2], a[3] = 0, a[4] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2], 0, 0, 0) + [0], f[2](0, a[2] - 1, 1, 1)}, {f[3](0, a[2], 0) + [2]}] = , [{[{[-2 + 2 a[2]]}, {[-2 + 2 a[2]]}], [-1 + 2 a[2]]}, {[1/2 + 2 a[2]]}] = , [2 a[2]] For the domain, {1 <= a[2], a[3] = 1, a[4] = 2, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 1, 1, 0) + [0], f[2](a[1] - 1, a[2] + 1, 1, 2), f[2](a[1], a[2] - 1, 2, 2), f[2](a[1], a[2], 0, 3)}, {}] = , [ {[{[3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}], [3 a[1] + 2 a[2]]}, {} ] = , [3 a[1] + 2 a[2] + 1] For the domain, {1 <= a[2], a[4] = 2, 2 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], a[3], 1, 0) + [0], f[2](a[1], a[2], a[3] - 1, 3), f[2](a[1], a[2] - 1, a[3] + 1, 2), f[2](a[1] - 1, a[2] + 1, a[3], 2)}, {}] = , [{[{[3 a[1] + 2 a[2] + a[3]]}, {[3 a[1] + 2 a[2] + a[3]]}], [3 a[1] + 2 a[2] + a[3] - 1]}, {}] = , [3 a[1] + 2 a[2] + a[3]] For the domain, {1 <= a[2], 1 <= a[3], a[4] = 3, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], a[3], 2, 0) + [0], f[2](a[1], a[2] - 1, a[3] + 1, 3), f[2](a[1], a[2], a[3] - 1, 4), f[2](a[1] - 1, a[2] + 1, a[3], 3)}, {}] = , [{[3 a[1] + 2 a[2] + a[3] - 1], [ {[{[4 a[1] + 3 a[2] + 2 a[3]]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]}, {[3 a[1] + 2 a[2] + a[3]]}]}, {}] = , [3 a[1] + 2 a[2] + a[3]] For the domain, {1 <= a[2], 4 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, a[3], a[4]), f[2](a[1], a[2] - 1, a[3] + 1, a[4]), f[2](a[1], a[2], a[3] - 1, a[4] + 1), f[1](a[1], a[2], a[3], a[4] - 1, 0) + [0]}, {}] = , [{[3 a[1] + 2 a[2] + a[3] - 1], [ {[{[4 a[1] + 3 a[2] + 2 a[3] + a[4] - 3]}, {[3 a[1] + 2 a[2] + a[3] + 1]}]} , {[3 a[1] + 2 a[2] + a[3]]}]}, {}] = , [3 a[1] + 2 a[2] + a[3]] For the domain, {1 <= a[2], a[4] = 2, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, 1, 0) + [0], f[2](a[1], a[2] - 1, 1, 2), f[2](a[1] - 1, a[2] + 1, 0, 2)}, {}] = , [{[3 a[1] + 2 a[2] - 1]}, {}] = , [3 a[1] + 2 a[2]] For the domain, {1 <= a[2], a[3] = 0, a[4] = 3, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, 2, 0) + [0], f[2](a[1] - 1, a[2] + 1, 0, 3), f[2](a[1], a[2] - 1, 1, 3)}, {}] = , [{[3 a[1] + 2 a[2] - 1], [{[{[4 a[1] + 3 a[2]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}]}, {}] = , [3 a[1] + 2 a[2]] For the domain, {1 <= a[2], 4 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2], 0, a[4] - 1, 0) + [0], f[2](a[1], a[2] - 1, 1, a[4]), f[2](a[1] - 1, a[2] + 1, 0, a[4])}, {}] = , [{[3 a[1] + 2 a[2] - 1], [ {[{[4 a[1] + 3 a[2] - 3 + a[4]]}, {[3 a[1] + 2 a[2] + 1]}]}, {[3 a[1] + 2 a[2]]}]}, {}] = , [3 a[1] + 2 a[2]] For the domain, {a[2] = 0, a[3] = 1, a[4] = 2, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](a[1], 0, 1, 1, 0) + [0], f[2](a[1], 0, 0, 3), f[2](a[1] - 1, 1, 1, 2)} , {}] = , [{[3 a[1] + 3/4], [3 a[1]]}, {}] = , [3 a[1] + 1] For the domain, {a[2] = 0, a[4] = 2, 2 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], 1, 0) + [0], f[2](a[1] - 1, 1, a[3], 2), f[2](a[1], 0, a[3] - 1, 3)}, {}] = , [{[3 a[1] - 1 + a[3]], [{[3 a[1] + a[3]]}, {[3 a[1] + a[3]]}]}, {}] = , [3 a[1] + a[3]] For the domain, {a[2] = 0, 1 <= a[3], a[4] = 3, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], 2, 0) + [0], f[2](a[1], 0, a[3] - 1, 4), f[2](a[1] - 1, 1, a[3], 3)}, {}] = , [{[3 a[1] - 1 + a[3]], [{[{[4 a[1] + 2 a[3]]}, {[3 a[1] + 1 + a[3]]}]}, {[3 a[1] + a[3]]}]}, {}] = , [3 a[1] + a[3]] For the domain, {a[2] = 0, 4 <= a[4], 1 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, a[3], a[4] - 1, 0) + [0], f[2](a[1], 0, a[3] - 1, a[4] + 1), f[2](a[1] - 1, 1, a[3], a[4])}, {}] = , [{[{[{[4 a[1] - 3 + 2 a[3] + a[4]]}, {[3 a[1] + 1 + a[3]]}]}, {[3 a[1] + a[3]]}], [3 a[1] - 1 + a[3]]}, {}] = , [3 a[1] + a[3]] For the domain, {a[2] = 0, a[4] = 2, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 0, 1, 0) + [0], f[2](a[1] - 1, 1, 0, 2)}, {}] = , [{[3 a[1] - 1]}, {}] = , [3 a[1]] For the domain, {a[2] = 0, a[3] = 0, a[4] = 3, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 0, 2, 0) + [0], f[2](a[1] - 1, 1, 0, 3)}, {}] = , [{[3 a[1] - 1], [{[{[4 a[1]]}, {[3 a[1] + 1/2]}]}, {[3 a[1]]}]}, {}] = , [3 a[1]] For the domain, {a[2] = 0, 4 <= a[4], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 0, a[4] - 1, 0) + [0], f[2](a[1] - 1, 1, 0, a[4])}, {}] = , [ {[3 a[1] - 1], [{[{[4 a[1] - 3 + a[4]]}, {[3 a[1] + 1]}]}, {[3 a[1]]}]}, {} ] = , [3 a[1]] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 1, a[4] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{ f[1](0, a[2], 1, 1, 0) + [0], f[2](0, a[2] - 1, 2, 2), f[2](0, a[2], 0, 3)} , {}] = , [{[{[2 a[2] + 1]}, {[2 a[2] + 1]}], [2 a[2]]}, {}] = , [2 a[2] + 1] For the domain, {a[1] = 0, 1 <= a[2], a[4] = 2, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], 1, 0) + [0], f[2](0, a[2], a[3] - 1, 3), f[2](0, a[2] - 1, a[3] + 1, 2)}, {}] = , [{[-1 + 2 a[2] + a[3]], [{[2 a[2] + a[3]]}, {[2 a[2] + a[3]]}]}, {}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, 1 <= a[2], 1 <= a[3], a[4] = 3} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], 2, 0) + [0], f[2](0, a[2] - 1, a[3] + 1, 3), f[2](0, a[2], a[3] - 1, 4)}, {}] = , [{[-1 + 2 a[2] + a[3]], [{[{[3 a[2] + 2 a[3]]}, {[1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}]}, {}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, 1 <= a[2], 4 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], a[3], a[4] - 1, 0) + [0], f[2](0, a[2], a[3] - 1, a[4] + 1), f[2](0, a[2] - 1, a[3] + 1, a[4])}, {}] = , [{[-1 + 2 a[2] + a[3]], [ {[{[-3 + 3 a[2] + 2 a[3] + a[4]]}, {[1 + 2 a[2] + a[3]]}]}, {[2 a[2] + a[3]]}]}, {}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, 1 <= a[2], a[4] = 2, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], 0, 1, 0) + [0], f[2](0, a[2] - 1, 1, 2)}, {}] = , [{[-1 + 2 a[2]]}, {}] = , [2 a[2]] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 0, a[4] = 3} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], 0, 2, 0) + [0], f[2](0, a[2] - 1, 1, 3)}, {}] = , [{[-1 + 2 a[2]], [{[{[3 a[2]]}, {[1 + 2 a[2]]}]}, {[2 a[2]]}]}, {}] = , [2 a[2]] For the domain, {a[1] = 0, 1 <= a[2], 4 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], 0, a[4] - 1, 0) + [0], f[2](0, a[2] - 1, 1, a[4])}, {}] = , [ {[{[{[-3 + 3 a[2] + a[4]]}, {[1 + 2 a[2]]}]}, {[2 a[2]]}], [-1 + 2 a[2]]}, {}] = , [2 a[2]] For the domain, {a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 1, 0) + [0], f[2](0, 0, 0, 3)}, {}] = , [{[0], [1/2]}, {}] = , [1] For the domain, {a[1] = 0, a[2] = 0, a[4] = 2, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3], 1, 0) + [0], f[2](0, 0, a[3] - 1, 3)}, {}] = , [{[a[3] - 1], [{[a[3]]}, {[a[3]]}]}, {}] = , [a[3]] For the domain, {a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 3} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3], 2, 0) + [0], f[2](0, 0, a[3] - 1, 4)}, {}] = , [{[a[3] - 1], [{[{[2 a[3]]}, {[a[3] + 1]}]}, {[a[3]]}]}, {}] = , [a[3]] For the domain, {a[1] = 0, a[2] = 0, 4 <= a[4], 1 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, a[3] - 1, a[4] + 1), f[1](0, 0, a[3], a[4] - 1, 0) + [0]}, {}] = , [{[a[3] - 1], [{[{[-3 + 2 a[3] + a[4]]}, {[a[3] + 1]}]}, {[a[3]]}]}, {}] = , [a[3]] For the domain, {a[1] = 0, a[2] = 0, a[4] = 2, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 1, 0) + [0]}, {}] = , [{[-2]}, {}] = , [0] For the domain, {a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 3} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 2, 0) + [0]}, {}] = , [{[{[{[0]}, {[0]}]}, {[0]}]}, {}] = , [0] For the domain, {a[1] = 0, a[2] = 0, 4 <= a[4], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, a[4] - 1, 0) + [0]}, {}] = , [{[{[{[a[4] - 3]}, {[1]}]}, {[0]}]}, {}] = , [0] ########## #, f[3], # ########## For the domain, {a[2] = 0, a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](a[1] - 1, 1, 0)}, {f[4](a[1], 0) + [0]}] = , [{[3 a[1] - 5/2]}, {[3 a[1] - 1]}] = , [3 a[1] - 2] For the domain, {a[1] = 0, a[2] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[4](0, 0) + [0]}] = , [{}, {[-1]}] = , [-2] For the domain, {1 <= a[2], a[3] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[3](a[1], a[2] - 1, 1), f[3](a[1] - 1, a[2] + 1, 0)}, {f[4](a[1], a[2]) + [0]}] = , [{[3 a[1] - 5/2 + 2 a[2]], [3 a[1] + 2 a[2] - 2]}, {[3 a[1] + 2 a[2] - 1]}] = , [3 a[1] + 2 a[2] - 3/2] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](0, a[2] - 1, 1)}, {f[4](0, a[2]) + [0]}] = , [{[-2 + 2 a[2]]}, {[-1 + 2 a[2]]}] = , [- 3/2 + 2 a[2]] For the domain, {1 <= a[2], a[3] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], a[2], 0, 0) + [1], f[3](a[1] - 1, a[2] + 1, 1), f[3](a[1], a[2] - 1, 2)}, {f[4](a[1], a[2]) + [3]}] = , [{[3 a[1] + 2 a[2] - 1]}, {[3 a[1] + 2 a[2] + 2]}] = , [3 a[1] + 2 a[2]] For the domain, {a[2] = 0, a[3] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], 0, 0, 0) + [1], f[3](a[1] - 1, 1, 1)}, {f[4](a[1], 0) + [3]}] = , [{[3 a[1] - 1], [3 a[1] - 3/2]}, {[3 a[1] + 2]}] = , [3 a[1]] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2], 0, 0) + [1], f[3](0, a[2] - 1, 2)}, {f[4](0, a[2]) + [3]}] = , [{[-1 + 2 a[2]]}, {[2 + 2 a[2]]}] = , [2 a[2]] For the domain, {a[1] = 0, a[2] = 0, a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 0, 0) + [1]}, {f[4](0, 0) + [3]}] = , [{[-2]}, {[2]}] = , [0] For the domain, {a[3] = 2, 1 <= a[2], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], a[2], 1, 0) + [1], f[3](a[1], a[2] - 1, 3), f[3](a[1] - 1, a[2] + 1, 2)}, {}] = , [ {[{[3 a[1] + 2 a[2] + 1]}, {[3 a[1] + 2 a[2] + 1]}], [3 a[1] + 2 a[2]]}, {} ] = , [3 a[1] + 2 a[2] + 1] For the domain, {3 <= a[3], 1 <= a[2], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], a[2], a[3] - 1, 0) + [1], f[3](a[1] - 1, a[2] + 1, a[3]), f[3](a[1], a[2] - 1, a[3] + 1)}, {}] = , [{[3 a[1] - 2 + 2 a[2] + a[3]], [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[3 a[1] + 2 a[2] + a[3] - 1]}]}, {}] = , [3 a[1] + 2 a[2] + a[3] - 1] For the domain, {a[3] = 2, a[2] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], 0, 1, 0) + [1], f[3](a[1] - 1, 1, 2)}, {}] = , [{[3 a[1] + 3/4], [3 a[1]]}, {}] = , [3 a[1] + 1] For the domain, {a[2] = 0, 3 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], 0, a[3] - 1, 0) + [1], f[3](a[1] - 1, 1, a[3])}, {}] = , [{[{[3 a[1] - 1 + a[3]]}, {[3 a[1] - 1 + a[3]]}], [3 a[1] - 2 + a[3]]}, {}] = , [3 a[1] - 1 + a[3]] For the domain, {a[1] = 0, a[3] = 2, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2], 1, 0) + [1], f[3](0, a[2] - 1, 3)}, {}] = , [{[2 a[2]], [{[1 + 2 a[2]]}, {[1 + 2 a[2]]}]}, {}] = , [1 + 2 a[2]] For the domain, {a[1] = 0, 3 <= a[3], 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2], a[3] - 1, 0) + [1], f[3](0, a[2] - 1, a[3] + 1)}, {}] = , [{[{[-1 + 2 a[2] + a[3]]}, {[-1 + 2 a[2] + a[3]]}], [-2 + 2 a[2] + a[3]]}, {}] = , [-1 + 2 a[2] + a[3]] For the domain, {a[1] = 0, a[3] = 2, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 1, 0) + [1]}, {}] = , [{[1/2]}, {}] = , [1] For the domain, {a[1] = 0, a[2] = 0, 3 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, a[3] - 1, 0) + [1]}, {}] = , [{[{[a[3] - 1]}, {[a[3] - 1]}]}, {}] = , [a[3] - 1] ########## #, f[4], # ########## For the domain, {a[2] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](a[1], 0, 0) + [2], f[4](a[1] - 1, 2)}, {f[5](a[1]) + [4]}] = , [{[3 a[1]]}, {[3 a[1] + 4]}] = , [3 a[1] + 1] For the domain, {a[2] = 0, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[4](a[1] - 1, 1)}, {f[5](a[1]) + [0]}] = , [{[3 a[1] - 2]}, {[3 a[1]]}] = , [3 a[1] - 1] For the domain, {a[1] = 0, a[2] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](0, 0, 0) + [2]}, {f[5](0) + [4]}] = , [{[0]}, {[4]}] = , [1] For the domain, {a[1] = 0, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[5](0) + [0]}] = , [{}, {[0]}] = , [-1] For the domain, {2 <= a[2], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](a[1], a[2] - 1, 0) + [2], f[4](a[1] - 1, a[2] + 1)}, {}] = , [{[3 a[1] + 2 a[2] - 2], [3 a[1] + 2 a[2] - 3/2]}, {}] = , [3 a[1] + 2 a[2] - 1] For the domain, {a[1] = 0, 2 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](0, a[2] - 1, 0) + [2]}, {}] = , [{[- 3/2 + 2 a[2]]}, {}] = , [-1 + 2 a[2]] ########## #, f[5], # ########## For the domain, {1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[4](a[1] - 1, 0) + [3]}, {}] = , [{[3 a[1] - 1]}, {}] = , [3 a[1]] For the domain, {a[1] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] ### The theorems are proved! ### This took, 431.407, seconds of CPU time