| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle relation_iterate.pvs Sprache: PVS |
|||||||||
|
% iteration of binary relations R, i.e., R composed with itself n times
% R o ... o R % % Author: Alfons Geser (geser@nianet.org), 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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28