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))
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.
