Quelle top_bags.pvs Sprache: PVS

top_bags: THEORY
%-------------------------------------------------------------------------
%
%  Theory of bags and finite bags.   Version 2.0       2/23/04
%
%    Authors: Rick Butler       NASA Langley Research Center
%             David Griffioen   CWI (National Research Institute for
%                               Mathematics and Computer Science
%                               and KUN (Catholic University Nijmegen),
%                               the Netherlands.
%             Lee Pike          NASA Langley Research Center
%
%    bags                     : fundamental definitions and properties
%    bags_aux                 : definition of filter, rest, and choose
%    bags_to_sets             : converts bags to sets
%    finite_bags              : basic definitions and lemmas
%    finite_bags_lems         : lemmas need induction
%    finite_bags_aux          : lemmas about filter, rest, and choose
%    finite_bags_inductions   : induction schemes
%    bag_filters              : filtering linearly-ordered bags, pigeonhole,
%                               majority pigeonhole results, and overlap
%                               existence proof
%    majority_vote            : defines a majority vote over finite bags
%    middle_value_select      : defines middle value selection over finite bags
%    fault_masking_vote       : proves an equivalence between majority and
%                               middle value selection
%    finite_bags_minmax       : defines tghe minimum and maximum of a finite
%                               ordered bag.
%------------------------------------------------------------------------
BEGIN

    IMPORTING   bags_aux, bags_to_sets, finite_bags_lems,
                finite_bags_aux, finite_bags_inductions,
                fault_masking_vote, finite_bags_minmax

END top_bags

quality84%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.