| products/Sources/formale Sprachen/Roqc/test-suite/success/ (Browser von der Mozilla Stiftung Version 136.0.1©) Datei vom 15.8.2025 mit Größe 136 B |
|
Impressum sqrt_exists.pvsSprache: PVS |
|||||||||||||||
|
sqrt_exists: THEORY %------------------------------------------------------------------------------- % % This theory provides a non-constructive proof of the existence of the % square root function. The proof has been adapted from Rosenlicht's % Introduction to Analysis. % %------------------------------------------------------------------------------- BEGIN e: VAR posreal x, y: VAR real nnx, nny: VAR nonneg_real i: var posnat epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y expt_0 : LEMMA 0^i = 0 lt1_expt_le : LEMMA nnx < 1 => nnx^i <= nnx sqrt_exists : LEMMA EXISTS (x1: [nnx: nonneg_real -> {nny | nny*nny = nnx}]): TRUE END sqrt_exists
¤ 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.14Bemerkung: (vorverarbeitet am 2026-05-06) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26