Due Date: Thurs, May 1, 2003
and
.
Show that both and
are theorems in
.
l:list. (
(l=[])
i:
.(i
l
j:
.(j
l
j
i)))
Give a -PRL definition of the predicate
, prove the
above statement in
-PRL's refinement logic, and describe the extracted
algorithm in
-PRL notation.