WARNING: You should seriously try to answer this question before looking at the solution -- it's just a good study skill. Also, some answers on this page may be more brief than you would want to put down in an actual exam. If you want any type of partial credit, you should write more than just the solution.
Base case ( P(empty) ).
(mirror (mirror empty)) -->*
(mirror (if (null? empty) empty
(let ((i (head empty))
(left (head (tail empty)))
(right (tail (tail empty))))
(cons i (cons (mirror right) (mirror left))))) -->*
(mirror empty) -->*
(if (null? empty) empty
(let ((i (head empty))
(left (head (tail empty)))
(right (tail (tail empty))))
(cons i (cons (mirror right) (mirror left))))) -->*
empty
Inductive case: Assume P(x) and P(y) and that i is an integer. We will show that P(pair i (pair x y)) holds.
(mirror (mirror (cons i (cons x y)))) -->
(mirror ((lambda (t)
(if (null? t) empty
(let ((i (head t))
(left (head t)))
(right (tail (tail t))))
(cons i (cons (mirror right) (mirror left))))))
(cons i (cons x y)))) -->
(mirror (if (null? (cons i (cons x y))) empty
(let ((i (head (cons i (cons x y))))
(left (head (tail (cons i (cons x y)))))
(right (tail (tail (cons i (cons x y))))))
(cons i (cons (mirror right) (mirror left)))))) -->
...
(mirror (cons i (cons (mirror y) (mirror x))))
...
(cons i (cons (mirror (mirror x)) (mirror (mirror y)))) -->* [By IH]
(pair i (pair x y))