Theorem: ############################# Let , f[1], be the value of , [T $ a[1], B, T $ a[2], F, T $ a[3], F] ############################# Then we have: f[1](0, 0, 0) = [-2] f[1](0, 0, a[3]) = [-1], 1 <= a[3] f[1](1, 0, 0) = [{[0]}, {[-1/2]}] f[1](1, 0, a[3]) = [{[0]}, {[0]}], 1 <= a[3] f[1](a[1], 0, a[3]) = [{[{[a[1] - 2]}, {[{[0]}, {[a[3]]}]}]}, {[0]}], 2 <= a[1], 0 <= a[3] f[1](a[1], 1, a[3]) = [{[a[1] - 1]}, {[{[0]}, {[a[3]]}]}], 0 <= a[3], 0 <= a[1] f[1](a[1], a[2], a[3]) = [a[1]], 0 <= a[3], 0 <= a[1], 2 <= a[2] Theorem: ############################# Let , f[2], be the value of , [T $ a[1], F, T $ a[2], B, T $ a[3], F] ############################# Then we have: f[2](0, 0, 0) = [-1] f[2](1, 0, 0) = [-1/2] f[2](a[1], 0, 0) = [{[{[{[a[1] - 3]}, {[1/2]}]}, {[0]}]}, {[0]}], 2 <= a[1] f[2](a[1], a[2], 0) = [{[{[-2 + a[2]]}, {[1]}]}, {[0]}], 0 <= a[1], 1 <= a[2] f[2](a[1], a[2], 1) = [{[-1 + a[2]]}, {[1]}], 0 <= a[1], 0 <= a[2] f[2](a[1], a[2], a[3]) = [a[2]], 0 <= a[1], 0 <= a[2], 2 <= a[3] Theorem: ############################# Let , f[3], be the value of , [T $ a[1], F, T $ a[2], F, B] ############################# Then we have: f[3](a[1], a[2]) = [0], 0 <= a[1], 0 <= a[2] 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], # ########## " in beginning Rec", [B, F, F], a, [B, F] " in the end Rec", [[[[[B, F, F], [a[1] - 1, a[2] + 1, a[3]]]], [[[F, B, F], [a[1], a[2], a[3]]]], [0 <= a[1], 0 <= a[2], a[2] <= 1, 0 <= a[3]]], [ [[[B, F, F], [a[1] - 1, a[2] + 1, a[3]]]], [], [0 <= a[1], 2 <= a[2], 0 <= a[3]]]] 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[2](0, 0, 0)}] = , [{}, {[-1]}] = , [-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, 1)}] = , [{}, {[{[-1]}, {[1]}]}] = , [-1] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 0, a[3])}] = , [{}, {[0]}] = , [-1] For the domain, {a[2] = 0, a[3] = 0, a[1] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 1, 0)}, {f[2](1, 0, 0)}] = , [{[{[-1]}, {[{[0]}, {[0]}]}]}, {[-1/2]}] = , [{[0]}, {[-1/2]}] For the domain, {a[2] = 0, a[1] = 1, a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 1, 1)}, {f[2](1, 0, 1)}] = , [{[{[-1]}, {[{[0]}, {[1]}]}]}, {[{[-1]}, {[1]}]}] = , [{[0]}, {[0]}] For the domain, {a[2] = 0, a[1] = 1, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 1, a[3])}, {f[2](1, 0, a[3])}] = , [{[{[-1]}, {[{[0]}, {[a[3]]}]}]}, {[0]}] = , [{[0]}, {[0]}] For the domain, {a[2] = 0, a[3] = 0, 2 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, 0)}, {f[2](a[1], 0, 0)}] = , [{[{[a[1] - 2]}, {[{[0]}, {[0]}]}]}, {[{[{[{[a[1] - 3]}, {[1/2]}]}, {[0]}]}, {[0]}]}] = , [{[0]}, {[0]}] For the domain, {a[2] = 0, 2 <= a[1], a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, 1)}, {f[2](a[1], 0, 1)}] = , [{[{[a[1] - 2]}, {[{[0]}, {[1]}]}]}, {[{[-1]}, {[1]}]}] = , [{[{[a[1] - 2]}, {[1/2]}]}, {[0]}] For the domain, {a[2] = 0, 2 <= a[1], 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 1, a[3])}, {f[2](a[1], 0, a[3])}] = , [{[{[a[1] - 2]}, {[{[0]}, {[a[3]]}]}]}, {[0]}] = , [{[{[a[1] - 2]}, {[1]}]}, {[0]}] For the domain, {a[3] = 0, a[2] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 2, 0)}, {f[2](a[1], 1, 0)}] = , [{[a[1] - 1]}, {[{[{[-1]}, {[1]}]}, {[0]}]}] = , [{[a[1] - 1]}, {[{[0]}, {[0]}]}] For the domain, {a[2] = 1, a[3] = 1, 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 2, 1)}, {f[2](a[1], 1, 1)}] = , [{[a[1] - 1]}, {[{[0]}, {[1]}]}] = , [{[a[1] - 1]}, {[1/2]}] For the domain, {a[2] = 1, 2 <= a[3], 1 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 2, a[3])}, {f[2](a[1], 1, a[3])}] = , [{[a[1] - 1]}, {[1]}] For the domain, {a[1] = 0, a[3] = 0, a[2] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 1, 0)}] = , [{}, {[{[{[-1]}, {[1]}]}, {[0]}]}] = , [0] For the domain, {a[1] = 0, a[2] = 1, a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 1, 1)}] = , [{}, {[{[0]}, {[1]}]}] = , [0] For the domain, {a[1] = 0, a[2] = 1, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {f[2](0, 1, a[3])}] = , [{}, {[1]}] = , [0] For the domain, {0 <= a[3], 2 <= a[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, a[3])}, {}] = , [{[a[1] - 1]}, {}] = , [a[1]] For the domain, {a[1] = 0, 0 <= a[3], 2 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] ########## #, f[2], # ########## " in beginning Rec", [F, B, F], a, [B, F] " in the end Rec", [[[[[B, F, F], [a[1] - 1, 0, a[3] + 1]]], [[[F, F, B], [a[1], a[2]], a[3]]], [0 <= a[1], a[2] = 0, 0 <= a[3], a[3] <= 1]], [ [[[B, F, F], [a[1] - 1, 0, a[3] + 1]]], [], [0 <= a[1], a[2] = 0, 2 <= a[3]]], [ [[[F, B, F], [a[1], -1 + a[2], a[3] + 1]]], [[[F, F, B], [a[1], a[2]], a[3]]], [0 <= a[1], 1 <= a[2], 0 <= a[3], a[3] <= 1]], [ [[[F, B, F], [a[1], -1 + a[2], a[3] + 1]]], [], [0 <= a[1], 1 <= a[2], 2 <= a[3]]]] 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]}] = , [{}, {[0]}] = , [-1] For the domain, {a[2] = 0, a[3] = 0, a[1] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 1)}, {f[3](1, 0) + [0]}] = , [{[-1]}, {[0]}] = , [-1/2] For the domain, {a[2] = 0, a[3] = 0, a[1] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](1, 0, 1)}, {f[3](2, 0) + [0]}] = , [{[{[0]}, {[0]}]}, {[0]}] For the domain, {a[2] = 0, a[3] = 0, 3 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 0, 1)}, {f[3](a[1], 0) + [0]}] = , [{[{[{[a[1] - 3]}, {[{[0]}, {[1]}]}]}, {[0]}]}, {[0]}] = , [{[{[{[a[1] - 3]}, {[1/2]}]}, {[0]}]}, {[0]}] For the domain, {a[3] = 0, 0 <= 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)}, {f[3](a[1], a[2]) + [0]}] = , [{[{[-2 + a[2]]}, {[1]}]}, {[0]}] For the domain, {a[2] = 0, a[1] = 1, a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, 2)}, {f[3](1, 0) + [1]}] = , [{[-1]}, {[1]}] = , [0] For the domain, {a[2] = 0, a[3] = 1, a[1] = 2} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](1, 0, 2)}, {f[3](2, 0) + [1]}] = , [{[{[0]}, {[0]}]}, {[1]}] = , [0] For the domain, {3 <= a[1], a[2] = 0, a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 0, 2)}, {f[3](a[1], 0) + [1]}] = , [{[{[{[a[1] - 3]}, {[{[0]}, {[2]}]}]}, {[0]}]}, {[1]}] = , [0] 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[3](0, 0) + [1]}] = , [{}, {[1]}] = , [0] For the domain, {0 <= a[1], 1 <= a[2], a[3] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], -1 + a[2], 2)}, {f[3](a[1], a[2]) + [1]}] = , [{[-1 + a[2]]}, {[1]}] For the domain, {a[2] = 0, a[1] = 1, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](0, 0, a[3] + 1)}, {}] = , [{[-1]}, {}] = , [0] For the domain, {a[1] = 2, a[2] = 0, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](1, 0, a[3] + 1)}, {}] = , [{[{[0]}, {[0]}]}, {}] = , [0] For the domain, {3 <= a[1], a[2] = 0, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[1](a[1] - 1, 0, a[3] + 1)}, {}] = , [{[{[{[a[1] - 3]}, {[{[0]}, {[a[3] + 1]}]}]}, {[0]}]}, {}] = , [0] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] For the domain, {0 <= a[1], 1 <= a[2], 2 <= a[3]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], -1 + a[2], a[3] + 1)}, {}] = , [{[-1 + a[2]]}, {}] = , [a[2]] ########## #, f[3], # ########## " in beginning Rec", [F, F, B], a, [B, F] " in the end Rec", [[[[[F, B, F], [a[1], -1 + a[2], 0], 0]], [], [0 <= a[1], 0 <= a[2], a[3] = 0]]] For the domain, {a[1] = 0, a[2] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](0, 0, 0) + [0]}, {}] = , [{[-1]}, {}] = , [0] For the domain, {a[1] = 1, a[2] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](1, 0, 0) + [0]}, {}] = , [{[-1/2]}, {}] = , [0] For the domain, {2 <= a[1], a[2] = 1} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], 0, 0) + [0]}, {}] = , [{[{[{[{[a[1] - 3]}, {[1/2]}]}, {[0]}]}, {[0]}]}, {}] = , [0] For the domain, {0 <= a[1], 2 <= a[2]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{f[2](a[1], -1 + a[2], 0) + [0]}, {}] = , [{[{[{[-3 + a[2]]}, {[1]}]}, {[0]}]}, {}] = , [0] For the domain, {a[2] = 0, 0 <= a[1]} using the inductive hypothesis, and then simplifying, we get: The value of the game = , [{}, {}] = , [{}, {}] = , [0] ### The theorems are proved! ### This took, 3.944, seconds of CPU time