> #restart; read `d:/Ake/tf/ToadsAndFrogs.txt`; > Prove(1,2,a,A12); ##Conjectures## ############################# Let, f[1], be the value of , [T $ a[1], B, T $ a[2], F, T $ a[3], F] ############################# 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[1], 0 <= a[3] f[1](a[1], a[2], a[3]) = [a[1]], 2 <= a[2], 0 <= a[1], 0 <= a[3] ############################# Let, f[2], be the value of , [T $ a[1], F, T $ a[2], B, T $ a[3], F] ############################# 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) = [{[{[a[2] - 2]}, {[1]}]}, {[0]}], 0 <= a[1], 1 <= a[2] f[2](a[1], a[2], 1) = [{[a[2] - 1]}, {[1]}], 0 <= a[2], 0 <= a[1] f[2](a[1], a[2], a[3]) = [a[2]], 0 <= a[2], 2 <= a[3], 0 <= a[1] ############################# Let, f[3], be the value of , [T $ a[1], F, T $ a[2], F, B] ############################# f[3](a[1], a[2]) = [0], 0 <= a[2], 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[2] = 0, a[3] = 0} The value of the game = , [{}, {f[2](0, 0, 0)}] = , [{}, {[-1]}] = , [-2] For the domain, {a[3] = 1, a[1] = 0, a[2] = 0} The value of the game = , [{}, {f[2](0, 0, 1)}] = , [{}, {[{[-1]}, {[1]}]}] = , [-1] For the domain, {2 <= a[3], a[1] = 0, a[2] = 0} 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} 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[3] = 1, a[2] = 0, a[1] = 1} 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, {2 <= a[3], a[2] = 0, a[1] = 1} 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]} 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[3] = 1, a[2] = 0, 2 <= a[1]} 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, {2 <= a[3], a[2] = 0, 2 <= a[1]} 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]} 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[3] = 1, a[2] = 1, 1 <= a[1]} 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, {2 <= a[3], a[2] = 1, 1 <= a[1]} 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} The value of the game = , [{}, {f[2](0, 1, 0)}] = , [{}, {[{[{[-1]}, {[1]}]}, {[0]}]}] = , [0] For the domain, {a[3] = 1, a[1] = 0, a[2] = 1} The value of the game = , [{}, {f[2](0, 1, 1)}] = , [{}, {[{[0]}, {[1]}]}] = , [0] For the domain, {2 <= a[3], a[1] = 0, a[2] = 1} The value of the game = , [{}, {f[2](0, 1, a[3])}] = , [{}, {[1]}] = , [0] For the domain, {2 <= a[2], 0 <= a[3], 1 <= a[1]} The value of the game = , [{f[1](a[1] - 1, a[2] + 1, a[3])}, {}] = , [{[a[1] - 1]}, {}] = , [a[1]] For the domain, {2 <= a[2], a[1] = 0, 0 <= a[3]} The value of the game = , [{}, {}] = , [{}, {}] = , [0] ########## #, f[2], # ########## For the domain, {a[1] = 0, a[2] = 0, a[3] = 0} The value of the game = , [{}, {f[3](0, 0) + [0]}] = , [{}, {[0]}] = , [-1] For the domain, {a[2] = 0, a[3] = 0, a[1] = 1} 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} 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]} 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]} The value of the game = , [{f[2](a[1], a[2] - 1, 1)}, {f[3](a[1], a[2]) + [0]}] = , [{[{[a[2] - 2]}, {[1]}]}, {[0]}] For the domain, {a[3] = 1, a[2] = 0, a[1] = 1} The value of the game = , [{f[1](0, 0, 2)}, {f[3](1, 0) + [1]}] = , [{[-1]}, {[1]}] = , [0] For the domain, {a[3] = 1, a[2] = 0, a[1] = 2} The value of the game = , [{f[1](1, 0, 2)}, {f[3](2, 0) + [1]}] = , [{[{[0]}, {[0]}]}, {[1]}] = , [0] For the domain, {a[3] = 1, a[2] = 0, 3 <= a[1]} 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[3] = 1, a[1] = 0, a[2] = 0} The value of the game = , [{}, {f[3](0, 0) + [1]}] = , [{}, {[1]}] = , [0] For the domain, {a[3] = 1, 0 <= a[1], 1 <= a[2]} The value of the game = , [{f[2](a[1], a[2] - 1, 2)}, {f[3](a[1], a[2]) + [1]}] = , [{[a[2] - 1]}, {[1]}] For the domain, {2 <= a[3], a[2] = 0, a[1] = 1} The value of the game = , [{f[1](0, 0, a[3] + 1)}, {}] = , [{[-1]}, {}] = , [0] For the domain, {2 <= a[3], a[2] = 0, a[1] = 2} The value of the game = , [{f[1](1, 0, a[3] + 1)}, {}] = , [{[{[0]}, {[0]}]}, {}] = , [0] For the domain, {2 <= a[3], 3 <= a[1], a[2] = 0} 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, {2 <= a[3], a[1] = 0, a[2] = 0} The value of the game = , [{}, {}] = , [{}, {}] = , [0] For the domain, {2 <= a[3], 0 <= a[1], 1 <= a[2]} The value of the game = , [{f[2](a[1], a[2] - 1, a[3] + 1)}, {}] = , [{[a[2] - 1]}, {}] = , [a[2]] ########## #, f[3], # ########## For the domain, {a[1] = 0, a[2] = 1} The value of the game = , [{f[2](0, 0, 0) + [0]}, {}] = , [{[-1]}, {}] = , [0] For the domain, {a[1] = 1, a[2] = 1} The value of the game = , [{f[2](1, 0, 0) + [0]}, {}] = , [{[-1/2]}, {}] = , [0] For the domain, {2 <= a[1], a[2] = 1} The value of the game = , [{f[2](a[1], 0, 0) + [0]}, {}] = , [{[{[{[{[a[1] - 3]}, {[1/2]}]}, {[0]}]}, {[0]}]}, {}] = , [0] For the domain, {2 <= a[2], 0 <= a[1]} The value of the game = , [{f[2](a[1], a[2] - 1, 0) + [0]}, {}] = , [{[{[{[a[2] - 3]}, {[1]}]}, {[0]}]}, {}] = , [0] For the domain, {a[2] = 0, 0 <= a[1]} The value of the game = , [{}, {}] = , [{}, {}] = , [0] ###The conjectures is proved### >