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

Re: A problem about rule "inst"

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):
- Date
- Thread