% iteration of binary relations R, i.e., R composed with itself n times
% R o ... o R
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
relation_iterate[T: TYPE]: THEORY
BEGIN
IMPORTING relations_extra[T], relation_props2[T, T, T, T]
R, R1, R2, S1, S2: VAR pred[[T, T]]
m, n: VAR nat
p: VAR posnat
x, y, z: VAR T
comp_equal_r: LEMMA
R o =[T] = R
comp_equal_l: LEMMA
=[T] o R = R
iterate(R, n): RECURSIVE pred[[T, T]] =
IF n = 0 THEN =[T] ELSE iterate(R, n - 1) o R ENDIF
MEASURE n
iterate_add: LEMMA
iterate(R, m + n) = iterate(R, m) o iterate(R, n)
iterate_add_applied: LEMMA
iterate(R, m)(x,y) & iterate(R, n)(y,z) => iterate(R, m + n)(x,z)
iterate_1: LEMMA
iterate(R, 1) = R
iterate_add_one: LEMMA
iterate(R, n + 1) = R o iterate(R, n)
iterate_mult: LEMMA
iterate(iterate(R, m), n) = iterate(R, m * n)
converse_equal: LEMMA
converse(=[T]) = =[T]
converse_comp: LEMMA
converse(R1 o R2) = converse(R2) o converse(R1)
iterate_converse: LEMMA
iterate(converse(R), n) = converse(iterate(R, n))
comp_is_monotone: LEMMA
subset?(R1, R2) & subset?(S1, S2) => subset?(R1 o S1, R2 o S2)
iterate_is_monotone: LEMMA
subset?(R1, R2) => subset?(iterate(R1, n), iterate(R2, n))
END relation_iterate
¤ Dauer der Verarbeitung: 0.14 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.
|
