|
finite_bags_inductions[T: TYPE]: THEORY
%-------------------------------------------------------------------------
%
% Induction scheme for finite bags, plural in name of this theory is
% misleading at this moment.
%
% Author: David Griffioen. (CWI Amsterdam and KUN)
%
%-------------------------------------------------------------------------
BEGIN
IMPORTING finite_bags_aux[T]
x: VAR T
b: VAR finite_bag
pb: VAR pred[finite_bag[T]]
n: VAR nat
cardinal_induction: LEMMA
(FORALL b : pb(b)) IFF (FORALL n, b : card(b) = n IMPLIES pb(b))
finite_bag_induction: THEOREM
(FORALL pb: (pb(emptybag[T]) AND
(FORALL x,b: pb(b) IMPLIES pb(insert(x,b))))
IMPLIES (FORALL b: pb(b)))
END finite_bags_inductions
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
