[ProofPower] Proving Properties of SML functions

[Marcel Oliveira]

Hello everybody,

I am trying to prove that the result of the application of a sml function
defined by me is the same for two given arguments. By way of illustration, I
am sending an example attached. In this example, I define two SML functions
nat_union and itself. The property I want to prove is that for all int list
xs, I have that nat_union xs xs = itself xs. This example is just an
abstraction of my real problem, which I give a short description at the end
of the att. Can anyone help me to prove this?

Thanks,
Marcel

===============================
Marcel Oliveira
PhD Researcher - Circus Project
Formal Methods
Computing Laboratory
University of Kent
Canterbury, Kent, UK  CT2 7NF
Tel: 44 (0)1227 823192
E-Mail: mvmo2 at kent.ac.uk
===============================
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test-proof.doc
Type: application/msword
Size: 2152 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040518/b8c18cba/attachment.doc>