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

[PVS-Help] finite sets TCC



Title: finite sets TCC

Hello,

I get a TCC which I don't know how to prove. I hope you can help me.
I want to prove the following:

        tr1!1`s = tr2!1`s
|-----------------------------
        FORALL (res:R): is_finite[M](s3(ss,ds)(tr1!1,tr2!1)`ms(res))

With:

R: TYPE+ = finite_set
M: TYPE+ = finite_set
Ms: TYPE+ = [R -> setof[M]
N: TYPE+ = finite_set
tp3(tp:setof[N],t:N): setof[N] = union(tp,singleton(t))

ms3(ss:staticSystem,ds:dynamicSystem)(tr1:setC_el, tr2:Tau): Ms =
    LAMBDA (res:R):
      COND
        NOT member(res,union(tr1`ac`r,tr2`ac`r)) -> tr1`s`ms(res),
        member(res,difference(tr1`ac`r,tr2`ac`r)) -> tr1`s1`ms(res),
        member(res,difference(tr2`ac`r,tr1`ac`r)) -> tr2`s1`ms(res),
        member(res,intersection(tr1`ac`r,tr2`ac`r)) -> union(difference(union(difference(tr1`s`ms(res),ds`cb(tr1`ac`t,ss`a(res))),ds`ce(tr1`ac`t,ss`a(res))),ds`cb(tr2`ac`t,ss`a(res))),ds`ce(tr2`ac`t,ss`a(res)))

      ENDCOND

  s3(ss:staticSystem, ds:dynamicSystem)(tr1:setC_el, tr2:Tau): State = (# `tp := tp3(tr1`s1`tp,tr2`ac`t), `ms := ms3(ss,ds)(tr1,tr2) #) % tr2`ac`t = tr3`ac`t


Do you know how to prove this TCC or give some hints? Any help is appreciated.
Thanks in advance.

Best regards,
Thijs Kuijpers