From: Enrico Tassi Date: Sun, 1 Dec 2002 20:37:14 +0000 (+0000) Subject: - now esempi/fourier/ is he dir for all fourier extras X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd122839ef59652446b521d79e1192cd2e709b00;p=helm.git - now esempi/fourier/ is he dir for all fourier extras - fourier.cic some tests - fourier_benchmarks.cic some test computionally interesting - fourier_make_benchmarks.ml a simple tool to generate big systems of inequations --- diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic deleted file mode 100644 index d2f9e4983..000000000 --- a/helm/gTopLevel/esempi/fourier.cic +++ /dev/null @@ -1,138 +0,0 @@ -alias Rge /Coq/Reals/Rdefinitions/Rge.con -alias Rle /Coq/Reals/Rdefinitions/Rle.con -alias Rgt /Coq/Reals/Rdefinitions/Rgt.con -alias Rlt /Coq/Reals/Rdefinitions/Rlt.con -alias Ropp /Coq/Reals/Rdefinitions/Ropp.con -alias Rinv /Coq/Reals/Rdefinitions/Rinv.con -alias Rplus /Coq/Reals/Rdefinitions/Rplus.con -alias Rminus /Coq/Reals/Rdefinitions/Rminus.con -alias Rmult /Coq/Reals/Rdefinitions/Rmult.con -alias R1 /Coq/Reals/Rdefinitions/R1.con -alias R0 /Coq/Reals/Rdefinitions/R0.con -alias R /Coq/Reals/Rdefinitions/R.con -alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 -alias not /Coq/Init/Logic/not.con -alias or /Coq/Init/Logic/or.ind#1/1 - -//baco -!x:R. -(Rlt (Rmult(Ropp x)R1) -R0) -->(Rlt R0 x) - -// test 3x4 -> 35'' -!x:R.!y:R.!z:R. -(Rge -(Rplus - (Rmult (Ropp (Rplus R1 R1)) x) (Rplus - (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus - (Rmult (Rplus R1 (Rplus R1 R1)) z) R1) -)) R0) --> -(Rge -(Rplus - (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus - (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus - R1 (Rplus R1 R1)) -)) R0) --> -(Rgt -(Rplus - x (Rplus - (Rmult (Rplus R1 R1) y) (Ropp z) ) -) R0) --> -(Rgt -(Rplus - (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus - z (Ropp R1)) -) R0) - --> (Rlt z R1) - -// test 6x6 -> - -!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. -(Rgt -(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1))))))) - R0) --> -(Rgt -(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1)))))) - R0) --> -(Rgt -(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1))))) - R0) --> -(Rgt -(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1))))) - R0) --> -(Rgt -(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1))))) - R0) --> -(Rlt -(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y)) - R0) --> (Rlt (Rmult (Rplus R1 R1) x) R0) - - - - - - -//test base1 ok -!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) - -//test base2 ok -!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1)) - -//test base3 ok -!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) - -/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con - -intros - -/Coq/Init/Logic/False.ind#1/1 - -(not (Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))) - -/Coq/fourier/Fourier_util/Rnot_le_le.con - -t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) - -t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) - -(t1-t2)=(Rminus -(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) -(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))) - -tc=(Rmult (Ropp R1) (Rinv R1)) - -rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) - (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1))) - -change=(not (or -(Rlt R0 (Rmult (Ropp R1) (Rinv R1))) -(eqT R R0 (Rmult (Ropp R1) (Rinv R1))) -)) - -tac2 -/Coq/fourier/Fourier_util/Rnot_lt0.con - -//test base4 ok -!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1)) - -//test base5 ok -!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0)) - -//test base6 ok -!x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) - -//test base7 (should fail) ok -!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1)) - - diff --git a/helm/gTopLevel/esempi/fourier/fourier.cic b/helm/gTopLevel/esempi/fourier/fourier.cic new file mode 100644 index 000000000..23062f3bd --- /dev/null +++ b/helm/gTopLevel/esempi/fourier/fourier.cic @@ -0,0 +1,137 @@ +alias Rge /Coq/Reals/Rdefinitions/Rge.con +alias Rle /Coq/Reals/Rdefinitions/Rle.con +alias Rgt /Coq/Reals/Rdefinitions/Rgt.con +alias Rlt /Coq/Reals/Rdefinitions/Rlt.con +alias Ropp /Coq/Reals/Rdefinitions/Ropp.con +alias Rinv /Coq/Reals/Rdefinitions/Rinv.con +alias Rplus /Coq/Reals/Rdefinitions/Rplus.con +alias Rminus /Coq/Reals/Rdefinitions/Rminus.con +alias Rmult /Coq/Reals/Rdefinitions/Rmult.con +alias R1 /Coq/Reals/Rdefinitions/R1.con +alias R0 /Coq/Reals/Rdefinitions/R0.con +alias R /Coq/Reals/Rdefinitions/R.con +alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 +alias not /Coq/Init/Logic/not.con +alias or /Coq/Init/Logic/or.ind#1/1 + +!x:R. +(Rlt (Rmult(Ropp x)R1) +R0) +->(Rlt R0 x) + +// test 3x4 -> 35'' +!x:R.!y:R.!z:R. +(Rge +(Rplus + (Rmult (Ropp (Rplus R1 R1)) x) (Rplus + (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus + (Rmult (Rplus R1 (Rplus R1 R1)) z) R1) +)) R0) +-> +(Rge +(Rplus + (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus + (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus + R1 (Rplus R1 R1)) +)) R0) +-> +(Rgt +(Rplus + x (Rplus + (Rmult (Rplus R1 R1) y) (Ropp z) ) +) R0) +-> +(Rgt +(Rplus + (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus + z (Ropp R1)) +) R0) + +-> (Rlt z R1) + +// test 6x6 -> + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rgt +(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1))))))) + R0) +-> +(Rgt +(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1)))))) + R0) +-> +(Rgt +(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1))))) + R0) +-> +(Rgt +(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1))))) + R0) +-> +(Rgt +(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1))))) + R0) +-> +(Rlt +(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y)) + R0) +-> (Rlt (Rmult (Rplus R1 R1) x) R0) + + + + + + +//test base1 ok +!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) + +//test base2 ok +!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base3 ok +!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) + +/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con + +intros + +/Coq/Init/Logic/False.ind#1/1 + +(not (Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))) + +/Coq/fourier/Fourier_util/Rnot_le_le.con + +t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) + +t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) + +(t1-t2)=(Rminus +(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) +(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))) + +tc=(Rmult (Ropp R1) (Rinv R1)) + +rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) + (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1))) + +change=(not (or +(Rlt R0 (Rmult (Ropp R1) (Rinv R1))) +(eqT R R0 (Rmult (Ropp R1) (Rinv R1))) +)) + +tac2 +/Coq/fourier/Fourier_util/Rnot_lt0.con + +//test base4 ok +!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1)) + +//test base5 ok +!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0)) + +//test base6 ok +!x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base7 (should fail) ok +!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1)) + + diff --git a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic new file mode 100644 index 000000000..68166c149 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic @@ -0,0 +1,170 @@ +!x:R.!y:R.!z:R.!t:R. +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult R1 t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 R1) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Ropp R1))))) R0) + +[1'02'' 363K m=5 n=4 K=8] + +------------------------------------------------------------------------------------------------------------ +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Ropp (Rplus R1 R1)) u) (Rplus (Rmult R1 v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) + +[1'25'' 501K m=7 n=6 K=8] + +----------------------------------------------------------------------------------------------------------- +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult R1 t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Ropp R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R0 g) (Rplus (Rmult R1 h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Ropp (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult R1 t) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) j) (Ropp R1))))))))))) R0) + +[1'50'' 787K m=11 n=10 K=8] + +------------------------------------------------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.!l:R.!m:R.!n:R.!o:R.!p:R.!q:R.!r:R.!s:R.!a:R.!b:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult R0 t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) a) (Rplus (Rmult R0 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult R1 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult R1 n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult R1 r) (Rplus (Rmult R1 s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 R1) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp R1) v) (Rplus (Rmult (Rplus R1 R1) w) (Rplus (Rmult R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult R1 j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult R0 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) r) (Rplus (Rmult (Rplus R1 R1) s) (Rplus (Rmult (Rplus R1 R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult R1 t) (Rplus (Rmult R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult R1 j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) q) (Rplus (Rmult R0 r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Rplus R1 R1) q) (Rplus (Rmult R0 r) (Rplus (Rmult R1 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) h) (Rplus (Rmult R1 j) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) l) (Rplus (Rmult R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) r) (Rplus (Rmult R0 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 R1) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R1 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult R0 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Rplus (Rmult (Rplus R1 R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult R0 j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) r) (Rplus (Rmult (Rplus R1 R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) m) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) o) (Rplus (Rmult R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult R0 g) (Rplus (Rmult R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) n) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Ropp R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult R1 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) g) (Rplus (Rmult (Rplus R1 R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) n) (Rplus (Rmult R0 o) (Rplus (Rmult (Rplus R1 R1) p) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult R1 r) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult R1 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) j) (Rplus (Rmult R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) q) (Rplus (Rmult R0 r) (Rplus (Rmult (Ropp R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult R1 b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Rplus (Rmult (Rplus R1 R1) l) (Rplus (Rmult (Rplus R1 R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R0 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult R0 v) (Rplus (Rmult R0 w) (Rplus (Rmult R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) h) (Rplus (Rmult (Rplus R1 R1) j) (Rplus (Rmult R0 l) (Rplus (Rmult R1 m) (Rplus (Rmult R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) p) (Rplus (Rmult R0 q) (Rplus (Rmult (Rplus R1 R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) b) (Ropp R1))))))))))))))))))))) R0) + + +[19'30'' 1.9M m=21 n=20 K=8 ty=13'35''] + +-------------------------------------------------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Rplus (Rmult R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) h) (Rplus (Rmult (Rplus R1 R1) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) g) (Rplus (Rmult R0 h) (Rplus (Rmult R1 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))))) t) (Rplus (Rmult (Ropp (Rplus R1 R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) h) (Rplus (Rmult R0 j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Ropp R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) u) (Rplus (Rmult (Rplus R1 R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) j) (Ropp R1))))))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))))) j) (Ropp R1))))))))))) R0) + +[ K m=11 n=10 K=18 ty=] (TRASH) + + +---------------------------------------------- + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) y) (Rplus (Rmult R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) u) (Rplus (Rmult R0 v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) x) (Rplus (Rmult R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 R1)) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) x) (Rplus (Rmult R1 y) (Rplus (Rmult R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) v) (Ropp R1))))))) R0) + +[4' 658K m=7 n=6 K=13 ty=50''] + +---------------------------------------------------------------- + +!x:R.!y:R.!z:R.!t:R. +(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))) x) (Rplus (Rmult (Ropp (Rplus R1 R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))) z) (Rplus (Rmult (Rplus R1 R1) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Ropp R1))))) R0) +-> +(Rle (Rplus (Rmult (Rplus R1 R1) x) (Rplus (Rmult R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1))))))))))) t) (Ropp R1))))) R0) + +[3':20'' 658K m=5 n=4 K=13 ty=41''] + + + + diff --git a/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml b/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml new file mode 100644 index 000000000..d783089a2 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml @@ -0,0 +1,61 @@ +let rec int_to_cic n = + if n < 0 then + "(Ropp "^int_to_cic (-n)^")" + else + match n with + 0 -> " R0" + |1 -> " R1" + |k -> "(Rplus R1 " ^ int_to_cic (n-1) ^")" +;; + +let dimx = ref 3;; +let dimy = ref 3;; +let kmax = ref 5;; +let vl = [|"x";"y";"z";"t";"u";"v";"w";"g";"h";"j";"l";"m";"n";"o";"p";"q";"r";"s";"a";"b";"c";"d"|] +;; + +let nth_inc n = + vl.(n) +;; + +let preamble () = + for i = 0 to !dimx do + print_string ("!"^nth_inc i^":R."); + done; + print_string "\n"; +;; + +let main () = + print_string "Immetti m : ";dimy := (read_int ()) - 1; + print_string "Immetti n : ";dimx := (read_int ()) - 1; + print_string "Immetti K : ";kmax := (read_int ()) + 1; + print_string ("Genero un sistema di "^ + string_of_int (!dimy+1)^" disequazioni in "^ + string_of_int (!dimx+1)^" incognite con coefficenti "^string_of_int !kmax^"\n\n"); + Random.self_init (); + preamble (); + let max = ref 0 in + for i=0 to !dimy do + begin + print_string "(Rle "; + for o=0 to !dimx do + let k = ref ((Random.int !kmax)) in + if !k > !max then max := !k; + if i=o then + k := - !k + else + k := !k; + print_string ("(Rplus (Rmult "^int_to_cic !k^" "^nth_inc o^") "); + done; + print_string "(Ropp R1)"; + for o=0 to !dimx do + print_string (")"); + done; + print_string (" R0)\n->\n"); + end + done; + print_string ("\n\nIl massimo K e' "^string_of_int !max^".\nLa tesi la puoi scegliere tu, ma se ricopi una ipotesi vai tranquillo.\n"); +;; + + +main ();; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5ad73d2be..ce2af709a 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,23 +60,26 @@ let htmlfooter = "" ;; -(* TASSI +(* TASSI *) let prooffile = "/home/tassi/miohelm/tmp/currentproof";; let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; + +(* +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; *) -let prooffile = "/public/natile/currentproof";; -let prooffiletype = "/public/natile/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) -(* TASSI +(* TASSI *) let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; -*) -let innertypesfile = "/public/natile/innertypes";; -let constanttypefile = "/public/natile/constanttype";; +(* +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; +*) let empty_id_to_uris = ([],function _ -> None);;