From dd122839ef59652446b521d79e1192cd2e709b00 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 1 Dec 2002 20:37:14 +0000 Subject: [PATCH] - now esempi/fourier/ is he dir for all fourier extras - fourier.cic some tests - fourier_benchmarks.cic some test computionally interesting - fourier_make_benchmarks.ml a simple tool to generate big systems of inequations --- .../esempi/{ => fourier}/fourier.cic | 1 - .../esempi/fourier/fourier_benchmarks.cic | 170 ++++++++++++++++++ .../esempi/fourier/fourier_make_benchmarks.ml | 61 +++++++ helm/gTopLevel/gTopLevel.ml | 17 +- 4 files changed, 241 insertions(+), 8 deletions(-) rename helm/gTopLevel/esempi/{ => fourier}/fourier.cic (99%) create mode 100644 helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic create mode 100644 helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier/fourier.cic similarity index 99% rename from helm/gTopLevel/esempi/fourier.cic rename to helm/gTopLevel/esempi/fourier/fourier.cic index d2f9e4983..23062f3bd 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier/fourier.cic @@ -14,7 +14,6 @@ alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 alias not /Coq/Init/Logic/not.con alias or /Coq/Init/Logic/or.ind#1/1 -//baco !x:R. (Rlt (Rmult(Ropp x)R1) R0) diff --git a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic new file mode 100644 index 000000000..68166c149 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic @@ -0,0 +1,170 @@ +!x:R.!y:R.!z:R.!t:R. +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult R1 t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 R1) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Ropp R1))))) R0) + +[1'02'' 363K m=5 n=4 K=8] + +------------------------------------------------------------------------------------------------------------ +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Ropp (Rplus R1 R1)) u) (Rplus (Rmult R1 v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) + +[1'25'' 501K m=7 n=6 K=8] + +----------------------------------------------------------------------------------------------------------- +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult R1 t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Ropp R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R0 g) (Rplus (Rmult R1 h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Ropp (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult R1 t) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) + +[1'50'' 787K m=11 n=10 K=8] + +------------------------------------------------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.!l:R.!m:R.!n:R.!o:R.!p:R.!q:R.!r:R.!s:R.!a:R.!b:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult R0 t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) a) (Rplus (Rmult R0 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult R1 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult R1 n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult R1 r) (Rplus (Rmult R1 s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 R1) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp R1) v) (Rplus (Rmult (Rplus R1 R1) w) (Rplus (Rmult R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult R1 j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult R0 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) r) (Rplus (Rmult (Rplus R1 R1) s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult R1 t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult R1 j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) q) (Rplus (Rmult R0 r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Rplus R1 R1) q) (Rplus (Rmult R0 r) (Rplus (Rmult R1 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) h) (Rplus (Rmult R1 j) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) l) (Rplus (Rmult R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 R1) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R1 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult R0 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Rplus (Rmult (Rplus R1 R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult R0 j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) r) (Rplus (Rmult (Rplus R1 R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) m) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult R0 g) (Rplus (Rmult R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Ropp R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult R1 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult R0 o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult R1 r) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult R1 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult R0 r) (Rplus (Rmult (Ropp R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R0 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R0 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) + + +[19'30'' 1.9M m=21 n=20 K=8 ty=13'35''] + +-------------------------------------------------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) h) (Rplus (Rmult (Rplus R1 R1) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) t) (Rplus (Rmult (Ropp (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) h) (Rplus (Rmult R0 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Ropp R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) j) (Ropp R1))))))))))) R0) + +[ K m=11 n=10 K=18 ty=] (TRASH) + + +---------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) u) (Rplus (Rmult R0 v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) + +[4' 658K m=7 n=6 K=13 ty=50''] + +---------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Ropp (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Ropp R1))))) R0) + +[3':20'' 658K m=5 n=4 K=13 ty=41''] + + + + diff --git a/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml b/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml new file mode 100644 index 000000000..d783089a2 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml @@ -0,0 +1,61 @@ +let rec int_to_cic n = + if n < 0 then + "(Ropp "^int_to_cic (-n)^")" + else + match n with + 0 -> " R0" + |1 -> " R1" + |k -> "(Rplus R1 " ^ int_to_cic (n-1) ^")" +;; + +let dimx = ref 3;; +let dimy = ref 3;; +let kmax = ref 5;; +let vl = [|"x";"y";"z";"t";"u";"v";"w";"g";"h";"j";"l";"m";"n";"o";"p";"q";"r";"s";"a";"b";"c";"d"|] +;; + +let nth_inc n = + vl.(n) +;; + +let preamble () = + for i = 0 to !dimx do + print_string ("!"^nth_inc i^":R."); + done; + print_string "\n"; +;; + +let main () = + print_string "Immetti m : ";dimy := (read_int ()) - 1; + print_string "Immetti n : ";dimx := (read_int ()) - 1; + print_string "Immetti K : ";kmax := (read_int ()) + 1; + print_string ("Genero un sistema di "^ + string_of_int (!dimy+1)^" disequazioni in "^ + string_of_int (!dimx+1)^" incognite con coefficenti "^string_of_int !kmax^"\n\n"); + Random.self_init (); + preamble (); + let max = ref 0 in + for i=0 to !dimy do + begin + print_string "(Rle "; + for o=0 to !dimx do + let k = ref ((Random.int !kmax)) in + if !k > !max then max := !k; + if i=o then + k := - !k + else + k := !k; + print_string ("(Rplus (Rmult "^int_to_cic !k^" "^nth_inc o^") "); + done; + print_string "(Ropp R1)"; + for o=0 to !dimx do + print_string (")"); + done; + print_string (" R0)\n->\n"); + end + done; + print_string ("\n\nIl massimo K e' "^string_of_int !max^".\nLa tesi la puoi scegliere tu, ma se ricopi una ipotesi vai tranquillo.\n"); +;; + + +main ();; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5ad73d2be..ce2af709a 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,23 +60,26 @@ let htmlfooter = "" ;; -(* TASSI +(* TASSI *) let prooffile = "/home/tassi/miohelm/tmp/currentproof";; let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; + +(* +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; *) -let prooffile = "/public/natile/currentproof";; -let prooffiletype = "/public/natile/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) -(* TASSI +(* TASSI *) let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; -*) -let innertypesfile = "/public/natile/innertypes";; -let constanttypefile = "/public/natile/constanttype";; +(* +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; +*) let empty_id_to_uris = ([],function _ -> None);; -- 2.39.2