Hi, I am now struggling with structural induction, this cannot be proved so I needed to prove with stronger property but I am stuck... please help with proving..
so, this is based on Haskell property (tree structure)
so 'Haskell' definition of binary tree is
data Tree a = Nul
| Node a (Tree a) (Tree a)
so basically, if the tree has no node then it is Nul or otherwise tree a has node a and left to it another tree that has less number than a and another tree on the right with the number greater than Node a.
so the problem has this property.
mult Nul = 1 ------ (M1)
mult (Node a t1 t2) = a * mult t1 * mult t2 ------ (M2)
multa t = multb t 1 ------ (MA)
multb Nul acc = acc --------- (MB1)
multb (Node a t1 t2) acc = multb t1 (a * (multb t2 acc)) ---- (MB2)
and I need to prove
mult t = multa t
certain two cannot be equal hence must prove with stronger property...
it seems that multb is acc times multiplication all nodes but I don't know how to prove from this point..
help me thank you very much for your support always..