I have completed the problem but I would like to know whether I did it correctly so please check my work to see whether everything went ok.

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)

Prove mult t = multa t

By induction on t,

Base Case P(Nul)

mult Nul = multa Nul

RHS = multb Nul 1 ---by (MA)

= 1 --- by (MB1)

LHS = 1 --- by (M1)

= RHS

Step Case∀a.∀t1.∀t2. P(t1)^P(t2)→P(Node a t1 t2)

Assume, P(u1)^ P(u2)

mult u1 = multa u1 --- (IH1)

mult u2 = multa u2 --- (IH2)

Prove P(Node x u1 u2), that is,

mult (Node x u1 u2) = multa (Node x u1 u2)

LHS= x * mult u1 * mult u2 ---by (M2)

= x * multa u1 * multa u2 ---by(IH1,IH2)

RHS= multb (Node x u1 u2) 1 ---by (MA)

= multb u1 (x * (multb u2 acc)) ---by(MB2)

≠LHS

-- note: I have changed a to x to show specific instance.. right?

Although I have used the IH1 & IH2, both sides are not the same. Therefore, we need to prove a stronger property than the one we is given.

∀ acc. acc * mult t = multb t acc

By induction on t,

Base Case P(Nul)

∀ acc. acc * mult Nul = multb Nul acc

RHS= acc ---by (MB1)

LHS= acc * 1 ---by (M1)

= acc

=RHS

Step Case∀a.∀t1.∀t2. P(t1)^P(t2)→P(Node a t1 t2)

Assume, P(u1)^ P(u2)

∀ acc. acc * mult u1 = multb u1 acc --- (IH3)

∀ acc. acc * mult u2 = multb u2 acc --- (IH4)

Prove,

∀ acc. acc * mult (Node x u1 u2) = multb (Node x u1 u2) acc

RHS= multb u1 (x*(multb u2 acc)) -- by(MB2)

= multb u1 (x * acc * mult u2)-- by(IH4)

= (x * acc * mult u2)*mult u1 -- by(IH3)

LHS= acc * x * mult u1 * mult u2 -- by(M2)

=RHS

Then we need to generalise over acc by using∀→I.

We have now proved ∀ t. P(t), that is: [is this right? proved that for all t, P(t)? not too sure]

∀ t. ∀ acc. acc * mult t = multb t acc [is it okay to change Node a t1 t2 to t?]

Change the order of the quantifiers :

∀ acc. ∀ t. acc * mult t = multb t acc

Instantiate at (acc = 1),

∀ t. 1 * mult t = multb 1 accby∀→E

∀ t. mult t = multb 1 accby arithmetic

∀ t. mult t = multa tby MA

Which was the original property required. after instantiating the proof finishes right? not too sure about it.

Red texts are my questions... thank you