|
%%-------------------** Term Rewriting System (TRS) **------------------------
%%
%% Authors : Andre Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% and
%%
%% Mauricio Ayala Rincon
%% Universidade de Brasília - Brasil
%%
%% Last Modified On: March 24, 2008
%%
%%----------------------------------------------------------------------------
IUnion_extra[T: TYPE]: THEORY
BEGIN
i, n: VAR nat
x, y: VAR T
A, B,
C, D: VAR set[T]
%%%%%%%%%%%% Defining the finite set 1 <= i <= n %%%%%%%%%%%%%%%%%%%%%%%%%%
upto?(n: posnat): NONEMPTY_TYPE = {i: posnat | i <= n} CONTAINING n
%%%%%%%%%%%% Auxiliar Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
disjoint_subset: LEMMA subset?(A,B) & subset?(C,D) & disjoint?(B,D)
=> disjoint?(A,C)
disjoint_commute: LEMMA disjoint?(A,B) => disjoint?(B,A)
IUnion_of_finite_is_finite: LEMMA
FORALL (n: posnat, (f:[upto?(n) -> set[T]])):
(FORALL (i: upto?(n)): is_finite(f(i)))
=> is_finite(IUnion(LAMBDA (i: upto?(n)): f(i)))
IUnion_of_finite_is_finite1: LEMMA
FORALL (n: posnat, (f:[below[n] -> set[T]])):
(FORALL (i: below[n]): is_finite(f(i)))
=> is_finite(IUnion(LAMBDA (i: below[n]): f(i)))
END IUnion_extra
¤ Dauer der Verarbeitung: 0.2 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.
|
