# [PVS-Help] Pvs sets types

Title: Pvs sets types

Hello,

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+ = [#
t:setof[T],
g:setof[G],
l:setof[L],
ln:Ln,
gn:Gn,
<...>
#]

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,
Thijs