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

*To*: pvs-help@csl.sri.com*Subject*: Questions on conversion/coercion.*From*: Tae Ho Kim <thkim@salmosa.kaist.ac.kr>*Date*: Thu, 21 Aug 1997 23:14:39 +0900 (KST)

Hi. I have a question about conversion/coercion. 1. I specified two enumerated types. Every member of A type is the member of B type. And I want to verify every member of A is the member of B (theorem t). But I cannot do it. Because the set A type and the set B type is different. How can I prove it? comp : THEORY BEGIN aset : TYPE = {a, b} bset : TYPE = {a, b, c, d, e, f} t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2 END comp 2. I tried to define and use a conversion funtion. It is incorrect. What is the false? How can I modify it? I know that conv function is incorrect (skipping g), but I cannot find theorem t is incorrect. comp1 : THEORY BEGIN aset : TYPE = {a, b, g} bset : TYPE = {a, b, c, d, e, f} conv(aele:aset): bset = cases aele OF a : a:bset, b : b:bset endcases t : THEOREM FORALL(e1:aset):EXISTS (e2:bset): conv(e1) = e2 END comp1 -- Kim, Tae-ho thkim@salmosa.kaist.ac.kr http://salmosa.kaist.ac.kr/~thkim

- Prev by Date:
**regarding status-proof-theory** - Next by Date:
**Re: Questions on conversion/coercion.** - Prev by thread:
**Re: Two trivial questions during proof..** - Next by thread:
**Re: Questions on conversion/coercion.** - Index(es):