| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/SPARK/Manual/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 605 B |
|
Quelle Simple_Greatest_Common_Divisor.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Author: Stefan Berghofer Copyright: secunet Security Networks AG *) theory Simple_Greatest_Common_Divisor imports "HOL-SPARK.SPARK" begin spark_proof_functions gcd = "gcd :: int → int → int" spark_open ‹simple_greatest_common_divisor/g_c_d› spark_vc procedure_g_c_d_4 using ‹0 < d› ‹gcd c d = gcd m n› by (simp add: gcd_non_0_int) spark_vc procedure_g_c_d_9 using ‹0 ≤ c› ‹gcd c 0 = gcd m n› by simp spark_end end
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09