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

Re: A problem about rule "inst"



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,