Dear all,
thank you for your help and advice. I've modelled it using the functional
version:
val replace_smaller_def = Define `replace_smaller p q = \a : int - int. if
(a p) (a q) then (p =+ (a q)) a else a`;
val system_def = Define `system n = {replace_smaller (n-1) 0} UNION
{replace_smaller
Hi JJ:
The definition of replace_smaller is fine, but the rest needs some
tweaking.
My understanding of system_def is the following (I include replace_smaller
too):
val replace_smaller_def =
Define
`replace_smaller p q (A:num-num) = if A p A q then (p =+ A q) A
else A`;
val
