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

*To*: Hu Chengjun <hcj@iist.unu.edu>*Subject*: Re: A problem about rule "inst"*From*: Hu Chengjun <hcj@iist.unu.edu>*Date*: Tue, 23 Dec 1997 15:33:44 +0800*cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Tue, 23 Dec 1997 10:43:09 +0800." <199712230243.KAA04564@iist.unu.edu>

Sorry, I just asked a stupid problem. Someone told me that I could "solve" it by writing "/\\" instead of "/\". Everything is ok now. {-1} (FORALL (A: Form[dcTV]): |>(([] A) => A)) [-2] |>([] (Des_1 /\ Des_2 => Triple)) |------- [1] |>(Des_1 /\ Des_2 => Req) Rule? (inst -1 "(Des_1 /\\ Des_2 => Triple)") Instantiating the top quantifier in -1 with the terms: (Des_1 /\ Des_2 => Triple), this simplifies to: test : {-1} |>(([] (Des_1 /\ Des_2 => Triple)) => (Des_1 /\ Des_2 => Triple)) [-2] |>([] (Des_1 /\ Des_2 => Triple)) |------- [1] |>(Des_1 /\ Des_2 => Req) Yours,

**References**:**A problem about rule "inst"***From:*Hu Chengjun <hcj@iist.unu.edu>

- Prev by Date:
**A problem about rule "inst"** - Next by Date:
**Re: Recursive declarations** - Prev by thread:
**A problem about rule "inst"** - Next by thread:
**cannot ftp to ftp.csl.sri.com as anonymous** - Index(es):