moved some old stuff to the history

[helm.git] / helm / gTopLevel / esempi / fourier / fourier_benchmarks.cic

diff --git a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic
deleted file mode 100644 (file)
index 68166c1..0000000
--- a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic
+++ /dev/null
@@ -1,170 +0,0 @@
-!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'']
-
-
-
-