Theorem: ############################# Let , f[1], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], B, T $ a[4], F] ############################# Then we have: f[1](0, 0, 0, 0) = [-3] f[1](a[1], 0, 0, 0) = [{[2 a[1] - 2]}, {[2 a[1] - 2]}], 1 <= a[1] f[1](a[1], a[2], 0, 0) = [2 a[1] + a[2] - 1], 0 <= a[1], 1 <= a[2] f[1](a[1], 0, 1, 0) = [2 a[1] - 1], 0 <= a[1] f[1](a[1], a[2], 1, 0) = [{[2 a[1] + a[2]]}, {[2 a[1] + a[2]]}], 0 <= a[1], 1 <= a[2] f[1](a[1], a[2], a[3], 0) = [ {[{[3 a[1] + 2 a[2] + a[3] - 2]}, {[2 a[1] + a[2] + 1]}]}, {[2 a[1] + a[2]]}], 0 <= a[2], 0 <= a[1], 2 <= a[3] f[1](0, 0, 0, 1) = [-2] f[1](a[1], 0, 0, 1) = [{[2 a[1] - 1]}, {[2 a[1] - 1]}], 1 <= a[1] f[1](a[1], a[2], 0, 1) = [2 a[1] + a[2]], 0 <= a[1], 1 <= a[2] f[1](a[1], a[2], a[3], 1) = [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[2 a[1] + a[2] + 1]}], 0 <= a[2], 0 <= a[1], 1 <= a[3] f[1](a[1], a[2], a[3], a[4]) = [3 a[1] + 2 a[2] + a[3]], 0 <= a[3], 0 <= a[2], 0 <= a[1], 2 <= a[4] Theorem: ############################# Let , f[2], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], F, B] ############################# Then we have: f[2](a[1], 0, 0) = [2 a[1] - 2], 0 <= a[1] f[2](a[1], a[2], 0) = [{[2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] - 1]}], 0 <= a[1], 1 <= a[2] f[2](a[1], a[2], a[3]) = [2 a[1] + a[2]], 0 <= a[2], 0 <= a[1], 1 <= a[3] Theorem: ############################# Let , f[3], be the value of , [T $ a[1], B, T $ a[2], F, B, B] ############################# Then we have: f[3](a[1], a[2]) = [2 a[1] + a[2] - 1], 0 <= a[2], 0 <= a[1] Theorem: ############################# Let , f[4], be the value of , [T $ a[1], F, B, B, B] ############################# Then we have: f[4](a[1]) = [2 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[4] = 0, a[2] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 0, 0) + [0]}] = , [{}, {[-2]}] = , [-3] For the domain, {a[4] = 0, 1 <= a[1], a[2] = 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)}, {f[2](a[1], 0, 0) + [0]}] = , [{[2 a[1] - 2]}, {[2 a[1] - 2]}] For the domain, {a[2] = 1, a[4] = 0, 1 <= a[1], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 2, 0, 0), f[1](a[1], 0, 1, 0)}, {f[2](a[1], 1, 0) + [0]}] = , [{[2 a[1] - 1]}, {[{[2 a[1]]}, {[2 a[1]]}]}] = , [2 a[1]] For the domain, {2 <= a[2], a[4] = 0, 1 <= a[1], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 0, 0), f[1](a[1], a[2] - 1, 1, 0)}, {f[2](a[1], a[2], 0) + [0]}] = , [{[2 a[1] - 2 + a[2]], [%1, %1]}, {[%1, %1]}] %1 := {[2 a[1] + a[2] - 1]} = , [2 a[1] + a[2] - 1] For the domain, {a[2] = 1, a[1] = 0, 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)}, {f[2](0, 1, 0) + [0]}] = , [{[-1]}, {[{[0]}, {[0]}]}] = , [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[1](0, a[2] - 1, 1, 0)}, {f[2](0, a[2], 0) + [0]}] = , [{[{[a[2] - 1]}, {[a[2] - 1]}]}, {[{[a[2] - 1]}, {[a[2] - 1]}]}] = , [a[2] - 1] For the domain, {a[4] = 0, 1 <= a[1], a[3] = 1, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 0, 1), f[1](a[1] - 1, 1, 1, 0)}, {f[2](a[1], 0, 1) + [0]}] = , [{[{[2 a[1] - 1]}, {[2 a[1] - 1]}]}, {[2 a[1]]}] = , [2 a[1] - 1] For the domain, {a[1] = 0, a[4] = 0, a[3] = 1, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 1)}, {f[2](0, 0, 1) + [0]}] = , [{[-2]}, {[0]}] = , [-1] For the domain, {a[4] = 0, 1 <= a[1], a[3] = 1, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, 2, 0), f[1](a[1] - 1, a[2] + 1, 1, 0), f[1](a[1], a[2], 0, 1)}, {f[2](a[1], a[2], 1) + [0]}] = , [{[{[{[3 a[1] + 2 a[2] - 2]}, {[2 a[1] + a[2]]}]}, {[2 a[1] + a[2] - 1]}], [2 a[1] + a[2]], [{[2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] - 1]}]}, {[2 a[1] + a[2]]}] = , [{[2 a[1] + a[2]]}, {[2 a[1] + a[2]]}] For the domain, {a[1] = 0, a[4] = 0, a[3] = 1, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2] - 1, 2, 0), f[1](0, a[2], 0, 1)}, {f[2](0, a[2], 1) + [0]}] = , [{[a[2]], [{[{[-2 + 2 a[2]]}, {[a[2]]}]}, {[a[2] - 1]}]}, {[a[2]]}] = , [{[a[2]]}, {[a[2]]}] For the domain, {a[4] = 0, 1 <= a[1], 2 <= a[3], 1 <= a[2]} 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), f[1](a[1], a[2], a[3] - 1, 1), f[1](a[1], a[2] - 1, a[3] + 1, 0)}, {f[2](a[1], a[2], a[3]) + [0]}] = , [{[{[{[3 a[1] - 3 + 2 a[2] + a[3]]}, {[2 a[1] + a[2]]}]}, {[2 a[1] + a[2] - 1]}], [{[3 a[1] + 2 a[2] + a[3] - 2]}, {[2 a[1] + a[2] + 1]}]}, {[2 a[1] + a[2]]} ] = , [{[{[3 a[1] + 2 a[2] + a[3] - 2]}, {[2 a[1] + a[2] + 1]}]}, {[2 a[1] + a[2]]}] For the domain, {a[4] = 0, 1 <= a[1], 2 <= a[3], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, a[3], 0), f[1](a[1], 0, a[3] - 1, 1)}, {f[2](a[1], 0, a[3]) + [0]}] = , [{[{[{[3 a[1] - 3 + a[3]]}, {[2 a[1]]}]}, {[2 a[1] - 1]}], [{[3 a[1] - 2 + a[3]]}, {[2 a[1] + 1]}]}, {[2 a[1]]}] = , [{[{[3 a[1] - 2 + a[3]]}, {[2 a[1] + 1]}]}, {[2 a[1]]}] For the domain, {a[1] = 0, a[4] = 0, 2 <= a[3], 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, a[3] + 1, 0), f[1](0, a[2], a[3] - 1, 1)}, {f[2](0, a[2], a[3]) + [0]}] = , [{[{[-2 + 2 a[2] + a[3]]}, {[a[2] + 1]}], [{[{[-3 + 2 a[2] + a[3]]}, {[a[2]]}]}, {[a[2] - 1]}]}, {[a[2]]}] = , [{[{[-2 + 2 a[2] + a[3]]}, {[a[2] + 1]}]}, {[a[2]]}] For the domain, {a[1] = 0, a[4] = 0, 2 <= a[3], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, 1)}, {f[2](0, 0, a[3]) + [0]}] = , [{[{[a[3] - 2]}, {[1]}]}, {[0]}] For the domain, {a[4] = 1, a[1] = 0, a[2] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 0, 0) + [1]}] = , [{}, {[-1]}] = , [-2] For the domain, {a[4] = 1, 1 <= a[1], a[2] = 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, 1)}, {f[2](a[1], 0, 0) + [1]}] = , [{[2 a[1] - 1]}, {[2 a[1] - 1]}] For the domain, {a[4] = 1, 1 <= a[1], 1 <= a[2], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1], a[2] - 1, 1, 1), f[1](a[1] - 1, a[2] + 1, 0, 1)}, {f[2](a[1], a[2], 0) + [1]}] = , [{[2 a[1] + a[2] - 1], [{[3 a[1] + 2 a[2] - 2]}, {[2 a[1] + a[2]]}]}, {[{[2 a[1] + a[2]]}, {[2 a[1] + a[2]]}]}] = , [2 a[1] + a[2]] For the domain, {a[4] = 1, a[1] = 0, 1 <= a[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, 1)}, {f[2](0, a[2], 0) + [1]}] = , [{[{[-2 + 2 a[2]]}, {[a[2]]}]}, {[{[a[2]]}, {[a[2]]}]}] = , [a[2]] For the domain, {a[4] = 1, 1 <= a[1], 1 <= a[3], 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, a[3] + 1, 1), f[1](a[1] - 1, a[2] + 1, a[3], 1), f[1](a[1], a[2], a[3] - 1, 2)}, {f[2](a[1], a[2], a[3]) + [1]}] = , [{[3 a[1] + 2 a[2] + a[3] - 1], [{[3 a[1] + 2 a[2] + a[3] - 2]}, {[2 a[1] + a[2]]}]}, {[2 a[1] + a[2] + 1]} ] = , [{[3 a[1] + 2 a[2] + a[3] - 1]}, {[2 a[1] + a[2] + 1]}] For the domain, {a[4] = 1, 1 <= a[1], 1 <= a[3], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](a[1] - 1, 1, a[3], 1), f[1](a[1], 0, a[3] - 1, 2)}, {f[2](a[1], 0, a[3]) + [1]}] = , [ {[{[3 a[1] - 2 + a[3]]}, {[2 a[1]]}], [3 a[1] - 1 + a[3]]}, {[2 a[1] + 1]}] = , [{[3 a[1] - 1 + a[3]]}, {[2 a[1] + 1]}] For the domain, {a[4] = 1, a[1] = 0, 1 <= a[3], 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[1](0, a[2] - 1, a[3] + 1, 1), f[1](0, a[2], a[3] - 1, 2)}, {f[2](0, a[2], a[3]) + [1]}] = , [{[{[-2 + 2 a[2] + a[3]]}, {[a[2]]}], [-1 + 2 a[2] + a[3]]}, {[a[2] + 1]}] = , [{[-1 + 2 a[2] + a[3]]}, {[a[2] + 1]}] For the domain, {a[4] = 1, a[1] = 0, 1 <= a[3], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, 2)}, {f[2](0, 0, a[3]) + [1]}] = , [{[a[3] - 1]}, {[1]}] For the domain, {1 <= a[1], 1 <= a[3], 2 <= a[4], 1 <= a[2]} 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]), f[1](a[1], a[2], a[3] - 1, a[4] + 1), f[1](a[1], a[2] - 1, a[3] + 1, a[4])} , {}] = , [{[3 a[1] + 2 a[2] + a[3] - 1]}, {}] = , [3 a[1] + 2 a[2] + a[3]] For the domain, {1 <= a[1], 2 <= a[4], 1 <= a[2], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], a[2] - 1, 1, a[4]), f[1](a[1] - 1, a[2] + 1, 0, a[4])}, {}] = , [{[3 a[1] + 2 a[2] - 1]}, {}] = , [3 a[1] + 2 a[2]] For the domain, {1 <= a[1], 1 <= a[3], 2 <= a[4], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, a[3], a[4]), f[1](a[1], 0, a[3] - 1, a[4] + 1)}, {}] = , [{[3 a[1] - 1 + a[3]]}, {}] = , [3 a[1] + a[3]] For the domain, {1 <= a[1], 2 <= a[4], a[2] = 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, a[4])}, {}] = , [{[3 a[1] - 1]}, {}] = , [3 a[1]] For the domain, {a[1] = 0, 1 <= a[3], 2 <= a[4], 1 <= a[2]} 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]), f[1](0, a[2], a[3] - 1, a[4] + 1)}, {}] = , [{[-1 + 2 a[2] + a[3]]}, {}] = , [2 a[2] + a[3]] For the domain, {a[1] = 0, 2 <= a[4], 1 <= a[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, a[4])}, {}] = , [{[-1 + 2 a[2]]}, {}] = , [2 a[2]] For the domain, {a[1] = 0, 1 <= a[3], 2 <= a[4], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] - 1, a[4] + 1)}, {}] = , [{[a[3] - 1]}, {}] = , [a[3]] For the domain, {a[1] = 0, 2 <= a[4], a[2] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] ########## #, f[2], # ########## For the domain, {1 <= a[1], a[2] = 0, a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, 1, 0)}, {f[3](a[1], 0) + [0]}] = , [{[{[2 a[1] - 2]}, {[2 a[1] - 2]}]}, {[2 a[1] - 1]}] = , [2 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[3](0, 0) + [0]}] = , [{}, {[-1]}] = , [-2] For the domain, {1 <= a[1], 1 <= a[2], a[3] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [ {f[2](a[1], a[2] - 1, 1), f[2](a[1] - 1, a[2] + 1, 0)}, {f[3](a[1], a[2]) + [0]}] = , [{[{[2 a[1] - 2 + a[2]]}, {[2 a[1] - 2 + a[2]]}], [2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] - 1]}] = , [{[2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] - 1]}] 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[2](0, a[2] - 1, 1)}, {f[3](0, a[2]) + [0]}] = , [{[a[2] - 1]}, {[a[2] - 1]}] For the domain, {1 <= a[1], a[3] = 1, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, 1), f[2](a[1], a[2] - 1, 2), f[1](a[1], a[2], 0, 0) + [0]}, {f[3](a[1], a[2]) + [2]}] = , [{[2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] + 1]}] = , [2 a[1] + a[2]] For the domain, {1 <= a[1], a[3] = 1, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 0, 0) + [0], f[2](a[1] - 1, 1, 1)}, {f[3](a[1], 0) + [2]}] = , [{[{[2 a[1] - 2]}, {[2 a[1] - 2]}], [2 a[1] - 1]}, {[2 a[1] + 1]}] = , [2 a[1]] For the domain, {a[1] = 0, a[3] = 1, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, a[2], 0, 0) + [0], f[2](0, a[2] - 1, 2)}, {f[3](0, a[2]) + [2]}] = , [{[a[2] - 1]}, {[a[2] + 1]}] = , [a[2]] For the domain, {a[1] = 0, a[3] = 1, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 0, 0) + [0]}, {f[3](0, 0) + [2]}] = , [{[-3]}, {[1]}] = , [0] For the domain, {a[3] = 2, 1 <= a[1], 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, 2), f[2](a[1], a[2] - 1, 3), f[1](a[1], a[2], 1, 0) + [0]}, {}] = , [{[{[2 a[1] + a[2]]}, {[2 a[1] + a[2]]}], [2 a[1] + a[2] - 1]}, {}] = , [2 a[1] + a[2]] For the domain, {1 <= a[1], 1 <= a[2], 3 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1] - 1, a[2] + 1, a[3]), f[1](a[1], a[2], a[3] - 1, 0) + [0], f[2](a[1], a[2] - 1, a[3] + 1)}, {}] = , [{[{[{[3 a[1] + 2 a[2] + a[3] - 3]}, {[2 a[1] + a[2] + 1]}]}, {[2 a[1] + a[2]]}], [2 a[1] + a[2] - 1]}, {}] = , [2 a[1] + a[2]] For the domain, {a[3] = 2, 1 <= a[1], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1], 0, 1, 0) + [0], f[2](a[1] - 1, 1, 2)}, {}] = , [{[2 a[1] - 1]}, {}] = , [2 a[1]] For the domain, {1 <= a[1], a[2] = 0, 3 <= a[3]} 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 a[1] - 1], [{[{[3 a[1] - 3 + a[3]]}, {[2 a[1] + 1]}]}, {[2 a[1]]}]}, {} ] = , [2 a[1]] For the domain, {a[3] = 2, a[1] = 0, 1 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2] - 1, 3), f[1](0, a[2], 1, 0) + [0]}, {}] = , [{[{[a[2]]}, {[a[2]]}], [a[2] - 1]}, {}] = , [a[2]] For the domain, {a[1] = 0, 1 <= a[2], 3 <= 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] - 1, a[3] + 1)}, {}] = , [{[{[{[-3 + 2 a[2] + a[3]]}, {[a[2] + 1]}]}, {[a[2]]}], [a[2] - 1]}, {}] = , [a[2]] For the domain, {a[3] = 2, a[1] = 0, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1, 0) + [0]}, {}] = , [{[-1]}, {}] = , [0] 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[1](0, 0, a[3] - 1, 0) + [0]}, {}] = , [{[{[{[a[3] - 3]}, {[1]}]}, {[0]}]}, {}] = , [0] ########## #, f[3], # ########## 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] - 1, 2), f[2](a[1], 0, 0) + [1]}, {f[4](a[1]) + [3]}] = , [{[2 a[1] - 1]}, {[2 a[1] + 3]}] = , [2 a[1]] For the domain, {1 <= a[1], a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](a[1] - 1, 1)}, {f[4](a[1]) + [0]}] = , [{[2 a[1] - 2]}, {[2 a[1]]}] = , [2 a[1] - 1] For the domain, {a[2] = 1, a[1] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 0) + [1]}, {f[4](0) + [3]}] = , [{[-1]}, {[3]}] = , [0] For the domain, {a[1] = 0, a[2] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[4](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[2](a[1], a[2] - 1, 0) + [1], f[3](a[1] - 1, a[2] + 1)}, {}] = , [{[2 a[1] - 2 + a[2]], [{[2 a[1] + a[2] - 1]}, {[2 a[1] + a[2] - 1]}]}, {}] = , [2 a[1] + a[2] - 1] For the domain, {2 <= a[2], a[1] = 0} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, a[2] - 1, 0) + [1]}, {}] = , [{[{[a[2] - 1]}, {[a[2] - 1]}]}, {}] = , [a[2] - 1] ########## #, f[4], # ########## For the domain, {1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[3](a[1] - 1, 0) + [2]}, {}] = , [{[2 a[1] - 1]}, {}] = , [2 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, 23.609, seconds of CPU time