[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: lemma,inst? and replace*From*: Bill Majurski <william.majurski@nist.gov>*Date*: Fri, 25 Jul 1997 13:16:15 -0400*CC*: bill@dogbert.ncsl.nist.gov*Organization*: NIST*Sender*: bill@dogbert.ncsl.nist.gov

Hello After defining a transitive relationship in succ_ax: role : TYPE succT : TYPE = PRED[[role,role]] succ : succT succ_ax : AXIOM FORALL(x:role,y:role,z:role) : (succ(x,y) AND succ(y,z)) = succ(x,z) I prove the first part of: x1 : THEOREM reduce(succ(U,M) AND succ(M,N) AND succ(N,O), succ(U,O)) using (then (use "succ_ax")(replace -1 * lr)(delete -1)) which after several iterations of the above prover command looks like: x1 : |------- [1] reduce(succ(U, o), succ(U, o)) which I complete with another axiom. I then repeat the theorem with a few terms in different order: x2 : THEOREM reduce(succ(U,M) AND succ(N,O) AND succ(M,N), succ(U,O)) The (use "succ_ax") [ as (lemma "succ_ax")(inst?)(inst?) ] correctly identifies the assignment of variables in the axiom creating: x2 : {-1} (succ(U, M) AND succ(M, N)) = succ(U, N) |------- [1] reduce(succ(U, M) AND succ(N, o) AND succ(M, N), succ(U, o)) But in this case (replace -1 * lr) fails. I presume because (inst?) looked into the structure of the formula where as (replace) does a simple left to right scan. But, intuition says that if (inst?) can do the variable mapping correctly why can (replace) not take advantage of it? Does anyone have an ideas how to approach this simple sounding problem? It is not that this simple example cannot be restructured to match the power of (replace) but the intended later use will be in a much more complicated formula which would be very ackward to continually rearrange. thanks bill

- Prev by Date:
**Re: Inequations in long proof** - Next by Date:
**trivial theorem** - Prev by thread:
**Re: trivial theorem** - Next by thread:
**Inequations in long proof** - Index(es):