| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle bisection_nat_sqrt.pvs Sprache: PVS |
|||||||||
|
bisection_nat_sqrt: THEORY
BEGIN IMPORTING appendix n,m,x: VAR nat pn: VAR posnat fs_lt?(n,m):bool = sq(m+1) <= n fs_eq?(n,m):bool = sq(m) <= n AND n < sq(m+1) fs_gt?(n,m):bool = n < sq(m) fs_lt?(n)(m):bool = fs_lt?(n,m) fs_le?(n)(m):bool = fs_lt?(n,m) OR fs_eq?(n,m) fs_eq?(n)(m):bool = fs_eq?(n,m) fs_gt?(n)(m):bool = fs_gt?(n,m) fs_ge?(n)(m):bool = fs_eq?(n,m) OR fs_gt?(n,m) fs_lt_def: LEMMA fs_lt?(n,m) => (NOT fs_eq?(n,m) AND NOT fs_gt?(n,m)) fs_eq_def: LEMMA fs_eq?(n,m) => (NOT fs_lt?(n,m) AND NOT fs_gt?(n,m)) fs_gt_def: LEMMA fs_gt?(n,m) => (NOT fs_lt?(n,m) AND NOT fs_eq?(n,m)) fs_trichotomy: LEMMA fs_lt?(n,m) OR fs_eq?(n,m) OR fs_gt?(n,m) fs_le_ge: LEMMA fs_le?(x)(m) AND fs_ge?(x)(n) AND m /= n => m < n bisection_sqrt_aux(x:nat,m:(fs_le?(x)),n:(fs_ge?(x))): RECURSIVE nat = IF m = n THEN m ELSE LET t = floor((n+m)/2) IN IF fs_lt?(x,t) THEN bisection_sqrt_aux(x,t+1,n) ELSIF fs_eq?(x,t) THEN t ELSE bisection_sqrt_aux(x,m,t) ENDIF ENDIF MEASURE (LAMBDA (x:nat,m:(fs_le?(x)),n:(fs_ge?(x))): (n-m)+1) bisection_sqrt_aux_prop: LEMMA fs_le?(x)(m) AND fs_ge?(x)(n) => fs_eq?(x,bisection_sqrt_aux(x,m,n)) bisection_sqrt(n):nat = bisection_sqrt_aux(n,0,n) bisection_sqrt_def: LEMMA bisection_sqrt(n) = floor(sqrt(n)) END bisection_nat_sqrt ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28