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

about prove commands!



Hello,

I got a big problem when I proved the following lemma. Because I don't
know too much prover commands, who could give me any suggestions.
That's so appreciated!


hide_para.1.2 :

[-1]  P2!1(t1!3)
[-2]  P1!1(t1!2)
[-3]  t1!1 = leak(t1!2, X!1)
[-4]  t2!1 = leak(t1!3, X!1)
{-5}  prod(A!1)(leak(t1!2, X!1), leak(t1!3, X!1), x!1)
[-6]  disjoint?(A!1, X!1)
  |-------
[1]   EXISTS (t1_1:
                ({t: trace[E] |
                    EXISTS (t1: (P1!1), t2: (P2!1)):
                      prod(A!1)(t1, t2, t)})):
        x!1 = leak(t1_1, X!1)

====================================================
ps: Here prod is a function in which t is observed as a result if t1
and t2 can be executed concurrently by two processes which synchronise
on A. Indeed, t,t1 and t2 are traces denoted as lists.


prod(A)(t1, t2, t) : RECURSIVE bool =
    CASES t OF 
        null : null?(t1) AND null?(t2),
        cons(x, y) :
          IF A(x)
          THEN  
                cons?(t1) AND cons?(t2) AND
                car(t1) = x AND car(t2) = x
                AND prod(A)(cdr(t1), cdr(t2), y)
          ELSE 
                (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) 
             OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y))
          ENDIF
    ENDCASES
  MEASURE length(t)


leak(t,A) is a function that gets rid of t's events included in set A
for example:

 t: a->b->c-> Stop
 A:{a,b}
 leak(t,A)= c->Stop


ok, let's go back the above question. In 1.2, I can't use inst?
because I can't find a instance.  Please suggest me some commands to
make the prove carry on.

Many thanks!

Kun Wei