| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: pvs-sbcl | Distribution: Fedora Project |
| Version: 7.1 | Vendor: Fedora Project |
| Release: 9.fc38 | Build date: Fri Jan 20 11:55:03 2023 |
| Group: Unspecified | Build host: buildhw-x86-05.iad2.fedoraproject.org |
| Size: 178662327 | Source RPM: pvs-sbcl-7.1-9.fc38.src.rpm |
| Packager: Fedora Project | |
| Url: https://pvs.csl.sri.com/ | |
| Summary: Interactive theorem prover from SRI | |
PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. This build of PVS must be invoked as "pvs-sbcl", both to distinguish it from builds with other Common Lisp engines, and to distinguish it from /usr/sbin/pvs in the lvm2 package.
GPL-2.0-or-later AND GPL-3.0-or-later AND MIT AND LicenseRef-Fedora-Public-Domain AND Knuth-CTAN
* Fri Jan 20 2023 Fedora Release Engineering <releng@fedoraproject.org> - 7.1-9 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild * Tue Jan 17 2023 Jerry James <loganjerry@gmail.com> - 7.1-8 - Convert License tag to SPDX * Mon Aug 01 2022 Jerry James <loganjerry@gmail.com> - 7.1-8 - Add -emacs patch for Emacs 28 compatibility - Limit builds to x86_64 * Fri Jul 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 7.1-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild * Wed Jan 26 2022 Jerry James <loganjerry@gmail.com> - 7.1-7 - Rebuild to fix sbcl dependency * Fri Jan 21 2022 Fedora Release Engineering <releng@fedoraproject.org> - 7.1-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild * Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 7.1-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild * Thu Jun 03 2021 Jerry James <loganjerry@gmail.com> - 7.1-4 - Add -language patch to work around possible TeXLive 2021 bug - BR ghostscript instead of ghostscript-core * Thu Feb 04 2021 Jerry James <loganjerry@gmail.com> - 7.1-3 - Rebuild to fix sbcl dependency - Add MIME type for pvs source files * Wed Jan 27 2021 Fedora Release Engineering <releng@fedoraproject.org> - 7.1-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
/usr/bin/proveit /usr/bin/provethem /usr/bin/pvs-sbcl /usr/bin/pvsio /usr/lib/.build-id /usr/lib/.build-id/69 /usr/lib/.build-id/69/d64617e248dcb4d7ee8fd841d1d8b3278179eb /usr/lib/.build-id/6b /usr/lib/.build-id/6b/47bf83d9637323f29b9211a2d21081c93bea3f /usr/lib/.build-id/6f /usr/lib/.build-id/6f/953469b250bc9c3c52c81a5072bc7798553ec7 /usr/lib/.build-id/ce /usr/lib/.build-id/ce/9d978485874764cbff97ee4ea90d480649e5f1 /usr/lib64/pvs /usr/lib64/pvs/bin /usr/lib64/pvs/bin/ix86_64-Linux /usr/lib64/pvs/bin/ix86_64-Linux/b64 /usr/lib64/pvs/bin/ix86_64-Linux/runtime /usr/lib64/pvs/bin/ix86_64-Linux/runtime/bdd-sbcl.fasl /usr/lib64/pvs/bin/ix86_64-Linux/runtime/bdd-sbcl.lisp /usr/lib64/pvs/bin/ix86_64-Linux/runtime/dfa-foreign-sbcl.fasl /usr/lib64/pvs/bin/ix86_64-Linux/runtime/dfa-foreign-sbcl.lisp /usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu-sbcl.fasl /usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu-sbcl.lisp /usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu.so /usr/lib64/pvs/bin/ix86_64-Linux/runtime/pvs-sbclisp /usr/lib64/pvs/bin/ix86_64-Linux/runtime/sbcl /usr/lib64/pvs/bin/ix86_64-Linux/runtime/ws1s.so /usr/lib64/pvs/bin/ix86_64-Linux/yices2 /usr/lib64/pvs/bin/pvs-platform /usr/lib64/pvs/bin/tar-b64-mail /usr/lib64/pvs/bin/tarmail /usr/lib64/pvs/bin/untarmail /usr/lib64/pvs/doc /usr/lib64/pvs/doc/release-notes /usr/lib64/pvs/doc/release-notes/pvs-release-notes.info /usr/lib64/pvs/emacs /usr/lib64/pvs/emacs/README /usr/lib64/pvs/emacs/configured-for-x /usr/lib64/pvs/emacs/go-pvs.el /usr/lib64/pvs/emacs/ilisp /usr/lib64/pvs/emacs/ilisp/ACKNOWLEDGMENTS /usr/lib64/pvs/emacs/ilisp/COPYING /usr/lib64/pvs/emacs/ilisp/HISTORY /usr/lib64/pvs/emacs/ilisp/comint-ipc.el /usr/lib64/pvs/emacs/ilisp/comint-ipc.elc /usr/lib64/pvs/emacs/ilisp/completer.el /usr/lib64/pvs/emacs/ilisp/completer.elc /usr/lib64/pvs/emacs/ilisp/docs /usr/lib64/pvs/emacs/ilisp/docs/ilisp.texi /usr/lib64/pvs/emacs/ilisp/ilcompat.el /usr/lib64/pvs/emacs/ilisp/ilcompat.elc /usr/lib64/pvs/emacs/ilisp/ilfsf18.el /usr/lib64/pvs/emacs/ilisp/ilfsf19.el /usr/lib64/pvs/emacs/ilisp/ilfsf20.el /usr/lib64/pvs/emacs/ilisp/ilfsf20.elc /usr/lib64/pvs/emacs/ilisp/ilisp-acl.el /usr/lib64/pvs/emacs/ilisp/ilisp-acl.elc /usr/lib64/pvs/emacs/ilisp/ilisp-aut.el /usr/lib64/pvs/emacs/ilisp/ilisp-aut.elc /usr/lib64/pvs/emacs/ilisp/ilisp-bat.el /usr/lib64/pvs/emacs/ilisp/ilisp-bat.elc /usr/lib64/pvs/emacs/ilisp/ilisp-chs.el /usr/lib64/pvs/emacs/ilisp/ilisp-chs.elc /usr/lib64/pvs/emacs/ilisp/ilisp-cl-easy-menu.el /usr/lib64/pvs/emacs/ilisp/ilisp-cl-easy-menu.elc /usr/lib64/pvs/emacs/ilisp/ilisp-cl.el /usr/lib64/pvs/emacs/ilisp/ilisp-cl.elc /usr/lib64/pvs/emacs/ilisp/ilisp-cmp.el /usr/lib64/pvs/emacs/ilisp/ilisp-cmp.elc /usr/lib64/pvs/emacs/ilisp/ilisp-cmt.el /usr/lib64/pvs/emacs/ilisp/ilisp-cmt.elc /usr/lib64/pvs/emacs/ilisp/ilisp-cmu.el /usr/lib64/pvs/emacs/ilisp/ilisp-cmu.elc /usr/lib64/pvs/emacs/ilisp/ilisp-def.el /usr/lib64/pvs/emacs/ilisp/ilisp-def.elc /usr/lib64/pvs/emacs/ilisp/ilisp-dia.el /usr/lib64/pvs/emacs/ilisp/ilisp-dia.elc /usr/lib64/pvs/emacs/ilisp/ilisp-doc.el /usr/lib64/pvs/emacs/ilisp/ilisp-doc.elc /usr/lib64/pvs/emacs/ilisp/ilisp-ext.el /usr/lib64/pvs/emacs/ilisp/ilisp-ext.elc /usr/lib64/pvs/emacs/ilisp/ilisp-hi.el /usr/lib64/pvs/emacs/ilisp/ilisp-hi.elc /usr/lib64/pvs/emacs/ilisp/ilisp-hnd.el /usr/lib64/pvs/emacs/ilisp/ilisp-hnd.elc /usr/lib64/pvs/emacs/ilisp/ilisp-imenu.el /usr/lib64/pvs/emacs/ilisp/ilisp-imenu.elc /usr/lib64/pvs/emacs/ilisp/ilisp-ind.el /usr/lib64/pvs/emacs/ilisp/ilisp-ind.elc /usr/lib64/pvs/emacs/ilisp/ilisp-inp.el /usr/lib64/pvs/emacs/ilisp/ilisp-inp.elc /usr/lib64/pvs/emacs/ilisp/ilisp-key.el /usr/lib64/pvs/emacs/ilisp/ilisp-key.elc /usr/lib64/pvs/emacs/ilisp/ilisp-kil.el /usr/lib64/pvs/emacs/ilisp/ilisp-kil.elc /usr/lib64/pvs/emacs/ilisp/ilisp-low.el /usr/lib64/pvs/emacs/ilisp/ilisp-low.elc /usr/lib64/pvs/emacs/ilisp/ilisp-menu.el /usr/lib64/pvs/emacs/ilisp/ilisp-mnb.el /usr/lib64/pvs/emacs/ilisp/ilisp-mnb.elc /usr/lib64/pvs/emacs/ilisp/ilisp-mod.el /usr/lib64/pvs/emacs/ilisp/ilisp-mod.elc /usr/lib64/pvs/emacs/ilisp/ilisp-mov.el /usr/lib64/pvs/emacs/ilisp/ilisp-mov.elc /usr/lib64/pvs/emacs/ilisp/ilisp-out.el /usr/lib64/pvs/emacs/ilisp/ilisp-out.elc /usr/lib64/pvs/emacs/ilisp/ilisp-prc.el /usr/lib64/pvs/emacs/ilisp/ilisp-prc.elc /usr/lib64/pvs/emacs/ilisp/ilisp-prn.el /usr/lib64/pvs/emacs/ilisp/ilisp-prn.elc /usr/lib64/pvs/emacs/ilisp/ilisp-rng.el /usr/lib64/pvs/emacs/ilisp/ilisp-rng.elc /usr/lib64/pvs/emacs/ilisp/ilisp-sbcl.el /usr/lib64/pvs/emacs/ilisp/ilisp-sbcl.elc /usr/lib64/pvs/emacs/ilisp/ilisp-snd.el /usr/lib64/pvs/emacs/ilisp/ilisp-snd.elc /usr/lib64/pvs/emacs/ilisp/ilisp-src.el /usr/lib64/pvs/emacs/ilisp/ilisp-src.elc /usr/lib64/pvs/emacs/ilisp/ilisp-sym.el /usr/lib64/pvs/emacs/ilisp/ilisp-sym.elc /usr/lib64/pvs/emacs/ilisp/ilisp-utl.el /usr/lib64/pvs/emacs/ilisp/ilisp-utl.elc /usr/lib64/pvs/emacs/ilisp/ilisp-val.el /usr/lib64/pvs/emacs/ilisp/ilisp-val.elc /usr/lib64/pvs/emacs/ilisp/ilisp-xfr.el /usr/lib64/pvs/emacs/ilisp/ilisp-xfr.elc /usr/lib64/pvs/emacs/ilisp/ilisp-xls.el /usr/lib64/pvs/emacs/ilisp/ilisp-xls.elc /usr/lib64/pvs/emacs/ilisp/ilisp.el /usr/lib64/pvs/emacs/ilisp/ilisp.elc /usr/lib64/pvs/emacs/ilisp/illuc19.el /usr/lib64/pvs/emacs/ilisp/ilxemacs.el /usr/lib64/pvs/emacs/manip-debug-utils.el /usr/lib64/pvs/emacs/manip-debug-utils.elc /usr/lib64/pvs/emacs/newcomment.el /usr/lib64/pvs/emacs/newcomment.elc /usr/lib64/pvs/emacs/prooflite.el /usr/lib64/pvs/emacs/prooflite.elc /usr/lib64/pvs/emacs/pvs-abbreviations.el /usr/lib64/pvs/emacs/pvs-abbreviations.elc /usr/lib64/pvs/emacs/pvs-browser.el /usr/lib64/pvs/emacs/pvs-browser.elc /usr/lib64/pvs/emacs/pvs-byte-compile.el /usr/lib64/pvs/emacs/pvs-byte-compile.elc /usr/lib64/pvs/emacs/pvs-cmds.el /usr/lib64/pvs/emacs/pvs-cmds.elc /usr/lib64/pvs/emacs/pvs-eval.el /usr/lib64/pvs/emacs/pvs-eval.elc /usr/lib64/pvs/emacs/pvs-file-list.el /usr/lib64/pvs/emacs/pvs-file-list.elc /usr/lib64/pvs/emacs/pvs-ilisp.el /usr/lib64/pvs/emacs/pvs-ilisp.elc /usr/lib64/pvs/emacs/pvs-load.el /usr/lib64/pvs/emacs/pvs-load.elc /usr/lib64/pvs/emacs/pvs-ltx.el /usr/lib64/pvs/emacs/pvs-ltx.elc /usr/lib64/pvs/emacs/pvs-macros.el /usr/lib64/pvs/emacs/pvs-macros.elc /usr/lib64/pvs/emacs/pvs-menu.el /usr/lib64/pvs/emacs/pvs-menu.elc /usr/lib64/pvs/emacs/pvs-mode.el /usr/lib64/pvs/emacs/pvs-mode.elc /usr/lib64/pvs/emacs/pvs-prelude-files-and-regions.el /usr/lib64/pvs/emacs/pvs-prelude-files-and-regions.elc /usr/lib64/pvs/emacs/pvs-print.el /usr/lib64/pvs/emacs/pvs-print.elc /usr/lib64/pvs/emacs/pvs-proofstate.el /usr/lib64/pvs/emacs/pvs-proofstate.elc /usr/lib64/pvs/emacs/pvs-prover-helps.el /usr/lib64/pvs/emacs/pvs-prover-helps.elc /usr/lib64/pvs/emacs/pvs-prover-manip.el /usr/lib64/pvs/emacs/pvs-prover-manip.elc /usr/lib64/pvs/emacs/pvs-prover.el /usr/lib64/pvs/emacs/pvs-prover.elc /usr/lib64/pvs/emacs/pvs-pvsio.el /usr/lib64/pvs/emacs/pvs-pvsio.elc /usr/lib64/pvs/emacs/pvs-set-prelude-info.el /usr/lib64/pvs/emacs/pvs-set-prelude-info.elc /usr/lib64/pvs/emacs/pvs-tcl.el /usr/lib64/pvs/emacs/pvs-tcl.elc /usr/lib64/pvs/emacs/pvs-utils.el /usr/lib64/pvs/emacs/pvs-utils.elc /usr/lib64/pvs/emacs/pvs-view.el /usr/lib64/pvs/emacs/pvs-view.elc /usr/lib64/pvs/emacs/pvs.xpm /usr/lib64/pvs/emacs/pvslogo.gif /usr/lib64/pvs/emacs/tcl.el /usr/lib64/pvs/emacs/tcl.elc /usr/lib64/pvs/lib /usr/lib64/pvs/lib/bitvectors /usr/lib64/pvs/lib/bitvectors/BitvectorMultiplication.prf /usr/lib64/pvs/lib/bitvectors/BitvectorMultiplication.pvs /usr/lib64/pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.prf /usr/lib64/pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.pvs /usr/lib64/pvs/lib/bitvectors/BitvectorOneComplementDivision.prf /usr/lib64/pvs/lib/bitvectors/BitvectorOneComplementDivision.pvs /usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivision.prf /usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivision.pvs /usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.prf /usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.pvs /usr/lib64/pvs/lib/bitvectors/BitvectorUtil.prf /usr/lib64/pvs/lib/bitvectors/BitvectorUtil.pvs /usr/lib64/pvs/lib/bitvectors/DivisionUtil.prf /usr/lib64/pvs/lib/bitvectors/DivisionUtil.pvs /usr/lib64/pvs/lib/bitvectors/bv_adder.prf /usr/lib64/pvs/lib/bitvectors/bv_adder.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_caret.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_caret.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_caret_concat_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_caret_concat_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_caret_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_caret_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_concat.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_concat.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_extend.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_extend.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_int_caret.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_int_caret.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_int_concat.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_int_concat.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_int_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_int_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_minus_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_minus_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_nat.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_nat.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_nat_caret_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_nat_caret_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_nat_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_nat_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arith_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_arith_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_arithmetic.prf /usr/lib64/pvs/lib/bitvectors/bv_arithmetic.pvs /usr/lib64/pvs/lib/bitvectors/bv_bitwise_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_bitwise_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise.prf /usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise.pvs /usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_caret_concat.prf /usr/lib64/pvs/lib/bitvectors/bv_caret_concat.pvs /usr/lib64/pvs/lib/bitvectors/bv_caret_concat_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_caret_concat_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_caret_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_caret_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_concat.prf /usr/lib64/pvs/lib/bitvectors/bv_concat.pvs /usr/lib64/pvs/lib/bitvectors/bv_concat_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_concat_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_constants.prf /usr/lib64/pvs/lib/bitvectors/bv_constants.pvs /usr/lib64/pvs/lib/bitvectors/bv_core.pvs /usr/lib64/pvs/lib/bitvectors/bv_extend.prf /usr/lib64/pvs/lib/bitvectors/bv_extend.pvs /usr/lib64/pvs/lib/bitvectors/bv_fract.prf /usr/lib64/pvs/lib/bitvectors/bv_fract.pvs /usr/lib64/pvs/lib/bitvectors/bv_int.prf /usr/lib64/pvs/lib/bitvectors/bv_int.pvs /usr/lib64/pvs/lib/bitvectors/bv_mult_div_rem.prf /usr/lib64/pvs/lib/bitvectors/bv_mult_div_rem.pvs /usr/lib64/pvs/lib/bitvectors/bv_nat_rules.prf /usr/lib64/pvs/lib/bitvectors/bv_nat_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_notes.pvs /usr/lib64/pvs/lib/bitvectors/bv_overflow.prf /usr/lib64/pvs/lib/bitvectors/bv_overflow.pvs /usr/lib64/pvs/lib/bitvectors/bv_rotate.prf /usr/lib64/pvs/lib/bitvectors/bv_rotate.pvs /usr/lib64/pvs/lib/bitvectors/bv_rules.pvs /usr/lib64/pvs/lib/bitvectors/bv_shift.prf /usr/lib64/pvs/lib/bitvectors/bv_shift.pvs /usr/lib64/pvs/lib/bitvectors/bv_sum.prf /usr/lib64/pvs/lib/bitvectors/bv_sum.pvs /usr/lib64/pvs/lib/bitvectors/div.prf /usr/lib64/pvs/lib/bitvectors/div.pvs /usr/lib64/pvs/lib/bitvectors/mod_rules.prf /usr/lib64/pvs/lib/bitvectors/mod_rules.pvs /usr/lib64/pvs/lib/bitvectors/sums.prf /usr/lib64/pvs/lib/bitvectors/sums.pvs /usr/lib64/pvs/lib/bitvectors/top.pvs /usr/lib64/pvs/lib/character_adt.pvs /usr/lib64/pvs/lib/finite_sets /usr/lib64/pvs/lib/finite_sets/card_tricks.prf /usr/lib64/pvs/lib/finite_sets/card_tricks.pvs /usr/lib64/pvs/lib/finite_sets/finite_cross.prf /usr/lib64/pvs/lib/finite_sets/finite_cross.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_below.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_below.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_card_eq.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_card_eq.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_eq.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_eq.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_inductions.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_inductions.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_int.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_int.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_minmax.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_minmax.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_minmax_props.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_minmax_props.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_nat.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_nat.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_pred.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_pred.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_product.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_product.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_product_real.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_product_real.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_subtype_props.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_subtype_props.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_sum.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_sum.pvs /usr/lib64/pvs/lib/finite_sets/finite_sets_sum_real.prf /usr/lib64/pvs/lib/finite_sets/finite_sets_sum_real.pvs /usr/lib64/pvs/lib/finite_sets/fs_constructors.prf /usr/lib64/pvs/lib/finite_sets/fs_constructors.pvs /usr/lib64/pvs/lib/finite_sets/func_composition.prf /usr/lib64/pvs/lib/finite_sets/func_composition.pvs /usr/lib64/pvs/lib/finite_sets/prelude_aux.prf /usr/lib64/pvs/lib/finite_sets/prelude_aux.pvs /usr/lib64/pvs/lib/finite_sets/top.prf /usr/lib64/pvs/lib/finite_sets/top.pvs /usr/lib64/pvs/lib/lift_adt.pvs /usr/lib64/pvs/lib/list_adt.pvs /usr/lib64/pvs/lib/ordstruct_adt.pvs /usr/lib64/pvs/lib/orphaned-proofs.prf /usr/lib64/pvs/lib/prelude.prf /usr/lib64/pvs/lib/prelude.pvs /usr/lib64/pvs/lib/pvs-gui.json /usr/lib64/pvs/lib/pvs-language.help /usr/lib64/pvs/lib/pvs-prover.help /usr/lib64/pvs/lib/pvs-style.css /usr/lib64/pvs/lib/pvs-unicode.help /usr/lib64/pvs/lib/pvs.bnf /usr/lib64/pvs/lib/pvs.grammar /usr/lib64/pvs/lib/pvs.help /usr/lib64/pvs/lib/pvs.json /usr/lib64/pvs/lib/pvs.rnc /usr/lib64/pvs/lib/pvsio_prelude.prf /usr/lib64/pvs/lib/pvsio_prelude.pvs /usr/lib64/pvs/lib/union_adt.pvs /usr/lib64/pvs/pvs-tex.sub /usr/lib64/pvs/wish /usr/lib64/pvs/wish/gray.xbm /usr/lib64/pvs/wish/pvs-support.tcl /usr/lib64/pvs/wish/sequent.xbm /usr/share/applications/pvs-sbcl.desktop /usr/share/doc/pvs-sbcl /usr/share/doc/pvs-sbcl/Examples /usr/share/doc/pvs-sbcl/Examples/AgExample /usr/share/doc/pvs-sbcl/Examples/AgExample/AgExample.dmp /usr/share/doc/pvs-sbcl/Examples/AgExample/AgSpec.txt /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_Element.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_Language.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_axioms.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_axioms.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_lemmas.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_semantic.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FA_semantic.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_Language.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_axioms.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_axioms.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_conversions.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_conversions.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_lemmas.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_lemmas.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_semantic.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_semantic.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/RTC.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/SRI-report.pdf /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecActions.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecActions.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecPredicates.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecPredicates.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecProperties.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/SpecProperties.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/ag-pp.lisp /usr/share/doc/pvs-sbcl/Examples/AgExample/dom-finitos.txt /usr/share/doc/pvs-sbcl/Examples/AgExample/list_max.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/list_max.pvs /usr/share/doc/pvs-sbcl/Examples/AgExample/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/AgExample/run.el /usr/share/doc/pvs-sbcl/Examples/AgExample/validate.el /usr/share/doc/pvs-sbcl/Examples/AgExample/wf_FODL_Language.prf /usr/share/doc/pvs-sbcl/Examples/AgExample/wf_FODL_Language.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/transition.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110 /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/components.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/quantifier_rules.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/quantifier_rules.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/signal.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/time.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5 /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/signal.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/sum.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/sum.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/time.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/new_pipe.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/new_pipe.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/pipe.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/signal.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/time.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/README /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/hard2.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/hard2.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/microrom_rewrite.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/microrom_rewrite.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/soft.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/tamarack.dump /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/trace_equiv.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/trace_equiv.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/traces.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/traces.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification_rewrites.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification_rewrites.pvs /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/wordth.prf /usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/wordth.pvs /usr/share/doc/pvs-sbcl/Examples/README /usr/share/doc/pvs-sbcl/Examples/ackerman.pvs /usr/share/doc/pvs-sbcl/Examples/byzantine /usr/share/doc/pvs-sbcl/Examples/byzantine/C1.ps /usr/share/doc/pvs-sbcl/Examples/byzantine/C2.ps /usr/share/doc/pvs-sbcl/Examples/byzantine/README /usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.dmp /usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.prf /usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.ps /usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.pvs /usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality /usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality/cardinality.prf /usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality/cardinality.pvs /usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.dvi.Z /usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.html /usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.ps /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/README /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline.dmp /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/basic_defs.prf /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/basic_defs.pvs /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/ops.prf /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/ops.pvs /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/validate.el /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/csl-95-10.html /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/csl-95-10.ps /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar.dmp /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/mizar.prf /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/mizar.pvs /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/validate.el /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/noninterference.sub /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/pvs-strategies /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding.dmp /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/unwinding.prf /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/unwinding.pvs /usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/validate.el /usr/share/doc/pvs-sbcl/Examples/f91.pvs /usr/share/doc/pvs-sbcl/Examples/fm99 /usr/share/doc/pvs-sbcl/Examples/fm99/bakery.prf /usr/share/doc/pvs-sbcl/Examples/fm99/bakery.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/bakery.sal /usr/share/doc/pvs-sbcl/Examples/fm99/bijections.prf /usr/share/doc/pvs-sbcl/Examples/fm99/bijections.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/eval.lisp /usr/share/doc/pvs-sbcl/Examples/fm99/expression.prf /usr/share/doc/pvs-sbcl/Examples/fm99/expression.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.pdf /usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.ps /usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.tex /usr/share/doc/pvs-sbcl/Examples/fm99/glade.lisp /usr/share/doc/pvs-sbcl/Examples/fm99/gprint.lisp /usr/share/doc/pvs-sbcl/Examples/fm99/hassen.ps /usr/share/doc/pvs-sbcl/Examples/fm99/lang.prf /usr/share/doc/pvs-sbcl/Examples/fm99/lang.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/light_bakery.prf /usr/share/doc/pvs-sbcl/Examples/fm99/light_bakery.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/phone_1.prf /usr/share/doc/pvs-sbcl/Examples/fm99/phone_1.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/phone_2.prf /usr/share/doc/pvs-sbcl/Examples/fm99/phone_2.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/phone_3.prf /usr/share/doc/pvs-sbcl/Examples/fm99/phone_3.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/phone_4.prf /usr/share/doc/pvs-sbcl/Examples/fm99/phone_4.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/phones.dmp /usr/share/doc/pvs-sbcl/Examples/fm99/phones.prf /usr/share/doc/pvs-sbcl/Examples/fm99/phones.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/print.lisp /usr/share/doc/pvs-sbcl/Examples/fm99/print.prf /usr/share/doc/pvs-sbcl/Examples/fm99/print.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/sine.prf /usr/share/doc/pvs-sbcl/Examples/fm99/sine.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/stamps.prf /usr/share/doc/pvs-sbcl/Examples/fm99/stamps.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/sum.lisp /usr/share/doc/pvs-sbcl/Examples/fm99/sum.prf /usr/share/doc/pvs-sbcl/Examples/fm99/sum.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/top.pvs /usr/share/doc/pvs-sbcl/Examples/fm99/validate.el /usr/share/doc/pvs-sbcl/Examples/fme96 /usr/share/doc/pvs-sbcl/Examples/fme96/fme96-tutorial.ps /usr/share/doc/pvs-sbcl/Examples/fme96/half.dmp /usr/share/doc/pvs-sbcl/Examples/fme96/half.prf /usr/share/doc/pvs-sbcl/Examples/fme96/half.pvs /usr/share/doc/pvs-sbcl/Examples/fme96/index.shtml /usr/share/doc/pvs-sbcl/Examples/fme96/validate.el /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/README /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache.dmp /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/abs_cache.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/abs_cache.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache2.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache2.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache_array.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache_array.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/refinement.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/refinement.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/top.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/trans.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2-3.dmp /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3 /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/abs_cache.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/abs_cache.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache2.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache2.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache_array.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache_array.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/refinement.prf /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/refinement.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/top.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/trans.pvs /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.dvi.Z /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.html /usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.ps.gz /usr/share/doc/pvs-sbcl/Examples/groups.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot.dmp /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/autopilot.prf /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/autopilot.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/hassen.prf /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/hassen.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/scr.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/validate.el /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise.dmp /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/cruise.prf /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/cruise.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/scr.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/validate.el /usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.dvi.Z /usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.html /usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.ps.gz /usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables /usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables.dmp /usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/tablewise.prf /usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/tablewise.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/validate.el /usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables /usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables.dmp /usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/simple_tables.prf /usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/simple_tables.pvs /usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/validate.el /usr/share/doc/pvs-sbcl/Examples/stack.pvs /usr/share/doc/pvs-sbcl/Examples/stacks.pvs /usr/share/doc/pvs-sbcl/Examples/sum.prf /usr/share/doc/pvs-sbcl/Examples/sum.pvs /usr/share/doc/pvs-sbcl/Examples/sum2.pvs /usr/share/doc/pvs-sbcl/Examples/ustacks.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12 /usr/share/doc/pvs-sbcl/Examples/vstte12/BFS.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/BFS.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/README /usr/share/doc/pvs-sbcl/Examples/vstte12/combinators.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/combinators.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/finseq_ops.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/finseq_ops.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/problems.pdf /usr/share/doc/pvs-sbcl/Examples/vstte12/ring_buffer.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/ring_buffer.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/sri-vstte12-competition.tgz /usr/share/doc/pvs-sbcl/Examples/vstte12/top.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/tree_reconstruction.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/tree_reconstruction.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/two_way_sort.prf /usr/share/doc/pvs-sbcl/Examples/vstte12/two_way_sort.pvs /usr/share/doc/pvs-sbcl/Examples/vstte12/vstte12-pvs.tgz /usr/share/doc/pvs-sbcl/Examples/wift-tutorial /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/README.md /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder.dmp /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/adder.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/adder.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/validate.el /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones.dmp /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_1.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_1.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_2.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_2.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_3.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_3.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_4.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_4.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phones.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phones.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/validate.el /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe.dmp /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/pipe.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/pipe.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/signal.prf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/signal.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/time.pvs /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/validate.el /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift-tutorial.pdf /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift95.html /usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift95.ps /usr/share/doc/pvs-sbcl/PVSio-2.d.pdf /usr/share/doc/pvs-sbcl/ProofLite-4.2.pdf /usr/share/doc/pvs-sbcl/README.md /usr/share/doc/pvs-sbcl/csl-93-9.ps.gz /usr/share/doc/pvs-sbcl/csl-97-2.ps.gz /usr/share/doc/pvs-sbcl/extrategies.pdf /usr/share/doc/pvs-sbcl/interpretations.pdf /usr/share/doc/pvs-sbcl/language.pdf /usr/share/doc/pvs-sbcl/manip-guide.pdf /usr/share/doc/pvs-sbcl/prover.pdf /usr/share/doc/pvs-sbcl/pvs-api.pdf /usr/share/doc/pvs-sbcl/pvs-prelude.pdf /usr/share/doc/pvs-sbcl/pvs-release-notes.pdf /usr/share/doc/pvs-sbcl/user-guide.pdf /usr/share/licenses/pvs-sbcl /usr/share/licenses/pvs-sbcl/LICENSE /usr/share/licenses/pvs-sbcl/NOTICES /usr/share/mime/packages/pvs.xml /usr/share/texlive/texmf-local/tex/latex/pvs /usr/share/texlive/texmf-local/tex/latex/pvs/pvs.sty
Generated by rpm2html 1.8.1
Fabrice Bellet, Wed Apr 9 17:50:32 2025