Just want to confirm whether I've got this right or not.. (should be right tho)

(tip: ++ is concatenation therefore joining two lists [ ] [ ] or (x:xs))

1. Prove xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Base case P( [ ] )

[ ] ++ (ys ++ zs) = ( [ ] ++ ys ) ++ zs

= ys ++ zs (RH)

= [ ] ++ (ys ++ zs)

= ys ++ zs (LH)

Step Case P (as)

Assume

as ++ (ys ++ zs) = (as ++ ys) ++ zs -- (IH)

Prove P (a:as)

(a:as) ++ (ys ++ zs) = ( (a:as) ++ ys) ++ zs

= ( (a:as) ++ ys) ++ zs --- (IH) (LH)

Theorem Proved. (I'm not too sure because it seems so simple though...something may be missing)

--------------------------------------------------------------------------------------------------------

revT :: Tree a -> Tree a

revT Nil = Nil -- (T1)

revT (Node x t1 t2) = Node x (revT t2) (revT t1) -- (T2)

2. Prove revT (revT t) = t

Base Case P(Nil)

revT (revT Nil) = Nil

= revT (Nil) - T1

= Nil -- T1 (LH)

Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2)

Assume P (u1) ^ P (u2)

revT (rev T u1) = u1 ---- IH1

revT (rev T u2) = u2 ---- IH2

Prove P(Node a u1 u2)

revT (revT (Node a u1 u2)) = Node a u1 u2

= revT ( Node a (revT u2) (revT u1) ) -- T2

= Node a (revT(revT u1)) (revT(revT u2)) -- T2

= Node a u1 u2 -- IH1, IH2 (LH)

Theorem Proved

3. (Extension work) Prove count(revT t) = count (t)

Base Case P (Nil)

count (rev T Nil) = count (Nil)

= count (rev T Nil) (LH)

= count (Nil) -- T1

Step Case Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2))

Assume P (u1) ^ P (u2)

count (rev T u1) = count (u1) -- IH1

count (rev T u2) = count (u2) -- IH2

Prove P (Node a u1 u2), that is

count (revT (Node a u1 u2)) = count (Node a u1 u2)

= count (Node a (revT u2) (revT u1)) -- T2

= Node (count a) (count(revT u2) (count (rev u1)) -

= Node (count a) (count u2) (count u1) -- IH1, IH2

= count (Node a u2 u1) (LH)

Well, looking at it, they are two different thing but if count function is merely counting number of nodes it should be the same.

4. Final question: natural deduction..

I thought I was able to solve all natural deduction questions but failed one.. which is:

(c V d) /\ ㄱc

----------------

d

(contradiction elimination rule can be used for this one)

Thank you (Fitch style please thank you)

It is a bit long but thank you very much!