Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
transclosure[T: TYPE]: THEORY % Wim H. Hesselink, 25 april 2002 % adapted by Gerard Renardel, 3 september 2003 BEGIN relation: TYPE = pred[[T, T]] R, S: VAR relation x, y, z: VAR T % IMPLIES(R, S: relation): bool = (FORALL (x, y): R(x, y) IMPLIES S(x, y)) % this is an overloading of IMPLIES % Kleene's star operation: star(R: relation): relation = (LAMBDA (x, y): (EXISTS (f: [nat -> T], n: nat): f(0) = x AND f(n) = y AND (FORALL (i: nat): i < n IMPLIES R(f(i), f(i + 1))))) % The prelude of PVS contains definitions of reflexive?, symmetric? % and transitive?. % You can therefore try to prove the next lemmas: star_reflexive: LEMMA reflexive?(star(R)) star_implied: LEMMA (FORALL (x,y): R(x,y) IMPLIES star(R)(x,y)) star_preserves_symmetry: LEMMA symmetric?(R) IMPLIES symmetric?(star(R)) star_transitive: LEMMA transitive?(star(R)) % State and prove the assertion that every reflexive and transitive % relation S that is implied by R, is also implied by star(R). % It may be convenient to use an auxiliary lemma. END transclosure