| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quellcode-Bibliothek Proc1.thy Sprache: Isabelle |
|||||||||
|
theory Proc1
imports "HOL-SPARK.SPARK" begin spark_open \<open>loop_invariant/proc1\<close> spark_vc procedure_proc1_5 by (simp add: ring_distribs mod_simps) spark_vc procedure_proc1_8 by (simp add: ring_distribs mod_simps) spark_end lemma pow_2_32_simp: "4294967296 = (2::int)^32" by simp end ¤ 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 |
|
