> #restart; read `d:/Ake/tf/ToadsAndFrogs.txt`; > Prove(2,1,a); ##Conjectures## ############################# Let, f[1], be the value of , [T $ a[1], B, T $ a[2], B, T $ a[3], F] ############################# f[1](0, 0, 0) = [-2] f[1](a[1], 0, 0) = [a[1] - 1], 1 <= a[1] f[1](0, 1, 0) = [-1/2] f[1](a[1], 1, 0) = [{[a[1]]}, {[a[1]]}], 1 <= a[1] f[1](a[1], a[2], 0) = [{[{[2 a[1] + a[2] - 2]}, {[a[1] + 1]}]}, {[a[1]]}], 2 <= a[2], 0 <= a[1] f[1](0, 0, 1) = [-1] f[1](a[1], 0, 1) = [a[1]], 1 <= a[1] f[1](a[1], a[2], 1) = [{[2 a[1] + a[2] - 1]}, {[a[1] + 1]}], 1 <= a[2], 0 <= a[1] f[1](a[1], a[2], a[3]) = [2 a[1] + a[2]], 2 <= a[3], 0 <= a[1], 0 <= a[2] ############################# Let, f[2], be the value of , [T $ a[1], B, T $ a[2], F, B] ############################# f[2](0, 0) = [-1] f[2](a[1], 0) = [- 1/2 + a[1]], 1 <= a[1] f[2](a[1], a[2]) = [a[1]], 1 <= a[2], 0 <= a[1] ############################# Let, f[3], be the value of , [T $ a[1], F, B, B] ############################# f[3](a[1]) = [a[1]], 0 <= a[1] Now we will prove by applying induction to each of the above conjectures one by one. If everythings are true, we get the proofs. ############### ##Begin to prove## ############### ########## #, f[1], # ########## For the domain, {a[1] = 0, a[3] = 0, a[2] = 0} The value of the game = , [{}, {f[2](0, 0) + [0]}] = , [{}, {[-1]}] = , [-2] For the domain, {a[3] = 0, a[2] = 0, a[1] = 1} The value of the game = , [{f[1](0, 1, 0)}, {f[2](1, 0) + [0]}] = , [{[-1/2]}, {[1/2]}] = , [0] For the domain, {a[3] = 0, a[2] = 0, 2 <= a[1]} The value of the game = , [{f[1](a[1] - 1, 1, 0)}, {f[2](a[1], 0) + [0]}] = , [{[{[a[1] - 1]}, {[a[1] - 1]}]}, {[- 1/2 + a[1]]}] = , [a[1] - 1] For the domain, {a[1] = 0, a[3] = 0, a[2] = 1} The value of the game = , [{f[1](0, 0, 1)}, {f[2](0, 1) + [0]}] = , [{[-1]}, {[0]}] = , [-1/2] For the domain, {a[3] = 0, a[2] = 1, 1 <= a[1]} The value of the game = , [ {f[1](a[1] - 1, 2, 0), f[1](a[1], 0, 1)}, {f[2](a[1], 1) + [0]}] = , [{[a[1]], [{[{[2 a[1] - 2]}, {[a[1]]}]}, {[a[1] - 1]}]}, {[a[1]]}] = , [{[a[1]]}, {[a[1]]}] For the domain, {a[3] = 0, 2 <= a[2], 1 <= a[1]} The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 0), f[1](a[1], a[2] - 1, 1)}, {f[2](a[1], a[2]) + [0]}] = , [{[{[2 a[1] + a[2] - 2]}, {[a[1] + 1]}], [{[{[2 a[1] - 3 + a[2]]}, {[a[1]]}]}, {[a[1] - 1]}]}, {[a[1]]}] = , [{[{[2 a[1] + a[2] - 2]}, {[a[1] + 1]}]}, {[a[1]]}] For the domain, {a[1] = 0, a[3] = 0, 2 <= a[2]} The value of the game = , [{f[1](0, a[2] - 1, 1)}, {f[2](0, a[2]) + [0]}] = , [{[{[a[2] - 2]}, {[1]}]}, {[0]}] For the domain, {a[1] = 0, a[2] = 0, a[3] = 1} The value of the game = , [{}, {f[2](0, 0) + [1]}] = , [{}, {[0]}] = , [-1] For the domain, {a[2] = 0, a[3] = 1, 1 <= a[1]} The value of the game = , [{f[1](a[1] - 1, 1, 1)}, {f[2](a[1], 0) + [1]}] = , [{[{[2 a[1] - 2]}, {[a[1]]}]}, {[1/2 + a[1]]}] = , [a[1]] For the domain, {1 <= a[2], a[3] = 1, 1 <= a[1]} The value of the game = , [ {f[1](a[1] - 1, a[2] + 1, 1), f[1](a[1], a[2] - 1, 2)}, {f[2](a[1], a[2]) + [1]}] = , [{[{[2 a[1] + a[2] - 2]}, {[a[1]]}], [2 a[1] + a[2] - 1]}, {[a[1] + 1]}] = , [{[2 a[1] + a[2] - 1]}, {[a[1] + 1]}] For the domain, {a[1] = 0, 1 <= a[2], a[3] = 1} The value of the game = , [{f[1](0, a[2] - 1, 2)}, {f[2](0, a[2]) + [1]}] = , [{[a[2] - 1]}, {[1]}] For the domain, {1 <= a[2], 2 <= a[3], 1 <= a[1]} The value of the game = , [{f[1](a[1] - 1, a[2] + 1, a[3]), f[1](a[1], a[2] - 1, a[3] + 1)}, {}] = , [{[2 a[1] + a[2] - 1]}, {}] = , [2 a[1] + a[2]] For the domain, {a[2] = 0, 2 <= a[3], 1 <= a[1]} The value of the game = , [{f[1](a[1] - 1, 1, a[3])}, {}] = , [{[2 a[1] - 1]}, {}] = , [2 a[1]] For the domain, {a[1] = 0, 1 <= a[2], 2 <= a[3]} The value of the game = , [{f[1](0, a[2] - 1, a[3] + 1)}, {}] = , [{[a[2] - 1]}, {}] = , [a[2]] For the domain, {a[1] = 0, a[2] = 0, 2 <= a[3]} The value of the game = , [{}, {}] = , [{}, {}] = , [0] ########## #, f[2], # ########## For the domain, {a[1] = 0, a[2] = 0} The value of the game = , [{}, {f[3](0) + [0]}] = , [{}, {[0]}] = , [-1] For the domain, {a[2] = 0, 1 <= a[1]} The value of the game = , [{f[2](a[1] - 1, 1)}, {f[3](a[1]) + [0]}] = , [{[a[1] - 1]}, {[a[1]]}] = , [- 1/2 + a[1]] For the domain, {a[2] = 1, 1 <= a[1]} The value of the game = , [ {f[1](a[1], 0, 0) + [0], f[2](a[1] - 1, 2)}, {f[3](a[1]) + [2]}] = , [{[a[1] - 1]}, {[a[1] + 2]}] = , [a[1]] For the domain, {a[1] = 0, a[2] = 1} The value of the game = , [{f[1](0, 0, 0) + [0]}, {f[3](0) + [2]}] = , [{[-2]}, {[2]}] = , [0] For the domain, {1 <= a[1], a[2] = 2} The value of the game = , [{f[1](a[1], 1, 0) + [0], f[2](a[1] - 1, 3)}, {}] = , [{[a[1] - 1], [{[a[1]]}, {[a[1]]}]}, {}] = , [a[1]] For the domain, {1 <= a[1], 3 <= a[2]} The value of the game = , [ {f[1](a[1], a[2] - 1, 0) + [0], f[2](a[1] - 1, a[2] + 1)}, {} ] = , [{[a[1] - 1], [{[{[2 a[1] - 3 + a[2]]}, {[a[1] + 1]}]}, {[a[1]]}]}, {}] = , [a[1]] For the domain, {a[1] = 0, a[2] = 2} The value of the game = , [{f[1](0, 1, 0) + [0]}, {}] = , [{[-1/2]}, {}] = , [0] For the domain, {a[1] = 0, 3 <= a[2]} The value of the game = , [{f[1](0, a[2] - 1, 0) + [0]}, {}] = , [{[{[{[a[2] - 3]}, {[1]}]}, {[0]}]}, {}] = , [0] ########## #, f[3], # ########## For the domain, {a[1] = 1} The value of the game = , [{f[2](0, 0) + [1]}, {}] = , [{[0]}, {}] = , [1] For the domain, {2 <= a[1]} The value of the game = , [{f[2](a[1] - 1, 0) + [1]}, {}] = , [{[- 1/2 + a[1]]}, {}] = , [a[1]] For the domain, {a[1] = 0} The value of the game = , [{}, {}] = , [{}, {}] = , [0] ###The conjectures is proved### >