Re: How do I put proof obs onto operator args?
To: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
Subject: Re: How do I put proof obs onto operator args?
Date: Tue, 08 Mar 94 12:31:54 -0800
Delivery-Date: Tue, 08 Mar 94 12:32:01 -0800
In-Reply-To: Message of Tue, 08 Mar 94 11:55:50 -0800 from kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
I am investigating the mailer problem.
LSL 2.3 deals only with total functions, so I don't see any obvious way to
impose the style of proof obligation you are requesting. (Maybe if I knew
why you wanted to impose it, I could suggest some other way of getting the
We are planning the inclusion of conditional equations in a future version
of LSL. This would let you say something like
P(t) :: op(t) == t_set(...);
Then, in order to use the equation to reduce op(t), you would need to prove
P(t). Is this what you had in mind?