X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Ffourier%2Ffourier_benchmarks.cic;fp=helm%2FgTopLevel%2Fesempi%2Ffourier%2Ffourier_benchmarks.cic;h=0000000000000000000000000000000000000000;hp=68166c14911198377e5fd573407f358f35cda74c;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic deleted file mode 100644 index 68166c149..000000000 --- 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''] - - - -