> #restart; read `d:/Ake/tf/ToadsAndFrogs.txt`;
> Prove(1,1,a);

                           ##Conjectures##





                    #############################


       Let, f[1], be the value of , [T $ a[1], B, T $ a[2], F]


                    #############################


                          f[1](0, 0) = [-1]


     f[1](a[1], 0) = [{[{[a[1] - 2]}, {[1]}]}, {[0]}], 1 <= a[1]


           f[1](a[1], 1) = [{[a[1] - 1]}, {[1]}], 0 <= a[1]


           f[1](a[1], a[2]) = [a[1]], 2 <= a[2], 0 <= a[1]





                    #############################


            Let, f[2], be the value of , [T $ a[1], F, B]


                    #############################


                     f[2](a[1]) = [0], 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}


           The value of the game = , [{}, {f[2](0) + [0]}]


                            = , [{}, {[0]}]


                               = , [-1]





                For the domain, {a[2] = 0, 1 <= a[1]}


 The value of the game = , [{f[1](a[1] - 1, 1)}, {f[2](a[1]) + [0]}]


                 = , [{[{[a[1] - 2]}, {[1]}]}, {[0]}]





                For the domain, {a[2] = 1, 1 <= a[1]}


 The value of the game = , [{f[1](a[1] - 1, 2)}, {f[2](a[1]) + [1]}]


                       = , [{[a[1] - 1]}, {[1]}]





                 For the domain, {a[1] = 0, a[2] = 1}


           The value of the game = , [{}, {f[2](0) + [1]}]


                            = , [{}, {[1]}]


                                = , [0]





                For the domain, {2 <= a[2], 1 <= a[1]}


      The value of the game = , [{f[1](a[1] - 1, a[2] + 1)}, {}]


                        = , [{[a[1] - 1]}, {}]


                              = , [a[1]]





                For the domain, {a[1] = 0, 2 <= a[2]}


                  The value of the game = , [{}, {}]


                             = , [{}, {}]


                                = , [0]





                              ##########


                              #, f[2], #


                              ##########





                      For the domain, {a[1] = 1}


          The value of the game = , [{f[1](0, 0) + [0]}, {}]


                           = , [{[-1]}, {}]


                                = , [0]





                     For the domain, {2 <= a[1]}


      The value of the game = , [{f[1](a[1] - 1, 0) + [0]}, {}]


             = , [{[{[{[a[1] - 3]}, {[1]}]}, {[0]}]}, {}]


                                = , [0]





                      For the domain, {a[1] = 0}


                  The value of the game = , [{}, {}]


                             = , [{}, {}]


                                = , [0]





                   ###The conjectures is proved###

>