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

[PVS-Help] Pvs sets types

Title: Pvs sets types


I try to prove a very simple conjecture w.r.t. sets and types.

The following is a part of the pvs theory:


% Definition 2.2

  setofNat: TYPE+ = {x:setof[nat] | NOT (subset?(x, singleton[nat](0)) AND subset?(singleton[nat](0),x))}      
  N:  TYPE+ = {tE2Rp0, tE2Rp1, tE2Rp2, tR2Pp0, tR2Pp1, tR2Pp2, t0p0, t0p1, t0p2, t3p2, t4p2, t1p0, t1p1, t2p0, t2p1, t5p2, tP2Rp0, tP2Rp1, tP2Rp2, tR2Ep0, tR2Ep1, tR2Ep2, g0p2, c0p2}

% finite, non-empty set of nodes (N = T union G union L)

  n1,n2,n3 : N
  disj: AXIOM n1 /= n2 AND n1 /= n3 AND n2 /= n3

  T:  TYPE+ = {x:N | x /= g0p2 AND x /= c0p2}
  G:  TYPE+ = {x:N | x = g0p2}
  L:  TYPE+ = {x:N | x = c0p2}
  Ln: TYPE+ = [L -> setof[N]]                                          
  Gn: TYPE+ = [G -> setof[N]]                                           

  dynamicSystem: TYPE+ = [#            
ds: dynamicSystem = (#
      t  := LAMBDA (t:T): TRUE,
      g  := LAMBDA (g:G): TRUE,
      l  := LAMBDA (l:L): TRUE,
      ln := LAMBDA (l:L): COND l=c0p2 -> {x:N | x = t3p2 OR x = t4p2}, ELSE -> emptyset ENDCOND,
      gn := LAMBDA (g:G): COND g=g0p2 -> {x:N | x = t0p2 OR x = c0p2}, ELSE -> emptyset ENDCOND,

% -1-
  ancRel(ds:dynamicSystem)(n1:N, n:N): INDUCTIVE boolean =                                     
    (member(n,ds`g) AND member(n1,ds`gn(n))) OR (member(n,ds`l) AND member(n1,ds`ln(n))) OR                                            

    (EXISTS (n2:N): ancRel(ds)(n1,n2) AND ancRel(ds)(n2,n))                                    

  anc(ds:dynamicSystem)(n:N): setof[N] = LAMBDA(n1:N): ancRel(ds)(n1,n)

% --- Tests ---

testAnc: CONJECTURE anc(ds)(tE2Rp2) = emptyset


To prove the conjecture testAnc I need information about tE2Rp2. Unfortunatey, using typepred I don't get any further and I do not know how to prove this in any other way.

Has anyone a suggestion? Thanks in advance.

Best regards,