|
gcd_fractions: THEORY
%------------------------------------------------------------------------------
% Author: Alfons Geser, HTWK Leipzig, Germany
% Date: May, 2009
%------------------------------------------------------------------------------
BEGIN
IMPORTING gcd
p, q, k: VAR posint
r: VAR posrat
div_by_gcd_prep: LEMMA FORALL (p: posint, q: posint):
integer_pred(p / gcd(p, q)) AND p / gcd(p, q) >= 0 AND p / gcd(p, q) > 0;
div_by_gcd(p, q): posint = p / gcd(p, q)
gcd_div_by_gcd: LEMMA gcd(div_by_gcd(p, q), div_by_gcd(q, p)) = 1
quotient_fully_cancelled: THEOREM
EXISTS p, q: gcd(p, q) = 1 AND r = p / q
END gcd_fractions
¤ Dauer der Verarbeitung: 0.15 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.
|
