| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quellcode-Bibliothek factorial.pvs Sprache: PVS |
|||||||||
|
factorial: THEORY
%---------------------------------------------------------------------------- % % Factorial function: factorial(n) = n! % % Author: Rick Butler NASA Langley Research Center % %---------------------------------------------------------------------------- BEGIN n,k: VAR nat factorial(n): recursive posnat = (if n = 0 then 1 else n*factorial(n-1) endif) MEASURE n factorial_0: LEMMA factorial(0) = 1 factorial_1: LEMMA factorial(1) = 1 factorial_2: LEMMA factorial(2) = 2 factorial_3: LEMMA factorial(3) = 6 factorial_def: LEMMA factorial(n) = IF n = 0 THEN 1 ELSE n*factorial(n-1) ENDIF factorial_n: LEMMA n > 0 IMPLIES factorial(n) = n*factorial(n-1) factorial_plus1: LEMMA factorial(n+1) = (n+1)*factorial(n) factorial_gt: LEMMA n > k IMPLIES factorial(n) > k^(n-k)*factorial(k) factorial_ge: LEMMA n >= k IMPLIES factorial(n) >= k^(n-k)*factorial(k) factorial_incr: LEMMA k <= n IMPLIES factorial(k) <= factorial(n) factorial_strict_incr: LEMMA k /= 0 AND k < n IMPLIES factorial(k) < factorial(n) factorial_lt_n2n: LEMMA factorial(n) <= n^n AUTO_REWRITE+ factorial_0 AUTO_REWRITE+ factorial_1 END factorial ¤ 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.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
