helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic

   1 !x:R.!y:R.!z:R.!t:R.
   2 (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)
   3 ->
   4 (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)
   5 ->
   6 (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)
   7 ->
   8 (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)
   9 ->
  10 (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)
  11
  12 [1'02'' 363K m=5 n=4 K=8]
  13
  14 ------------------------------------------------------------------------------------------------------------
  15 !x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
  16 (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)
  17 ->
  18 (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)
  19 ->
  20 (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)
  21 ->
  22 (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)
  23 ->
  24 (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)
  25 ->
  26 (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)
  27 ->
  28 (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)
  29
  30 [1'25'' 501K m=7 n=6 K=8]
  31
  32 -----------------------------------------------------------------------------------------------------------
  33 !x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.
  34 (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)
  35 ->
  36 (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)
  37 ->
  38 (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)
  39 ->
  40 (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)
  41 ->
  42 (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)
  43 ->
  44 (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)
  45 ->
  46 (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)
  47 ->
  48 (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)
  49 ->
  50 (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)
  51 ->
  52 (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)
  53 ->
  54 (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)
  55
  56 [1'50'' 787K m=11 n=10 K=8]
  57
  58 -------------------------------------------------------------------------------------------------------
  59
  60 !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.
  61 (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)
  62 ->
  63 (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)
  64 ->
  65 (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)
  66 ->
  67 (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)
  68 ->
  69 (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)
  70 ->
  71 (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)
  72 ->
  73 (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)
  74 ->
  75 (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)
  76 ->
  77 (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)
  78 ->
  79 (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)
  80 ->
  81 (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)
  82 ->
  83 (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)
  84 ->
  85 (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)
  86 ->
  87 (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)
  88 ->
  89 (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)
  90 ->
  91 (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)
  92 ->
  93 (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)
  94 ->
  95 (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)
  96 ->
  97 (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)
  98 ->
  99 (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)
 100 ->
 101 (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)
 102
 103
 104 [19'30'' 1.9M m=21 n=20 K=8 ty=13'35'']
 105
 106 --------------------------------------------------------------------------------------------------------
 107
 108 !x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.
 109 (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)
 110 ->
 111 (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)
 112 ->
 113 (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)
 114 ->
 115 (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)
 116 ->
 117 (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)
 118 ->
 119 (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)
 120 ->
 121 (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)
 122 ->
 123 (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)
 124 ->
 125 (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)
 126 ->
 127 (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)
 128 ->
 129 (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)
 130
 131 [ K m=11 n=10 K=18 ty=] (TRASH)
 132
 133
 134 ----------------------------------------------
 135
 136 !x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
 137 (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)
 138 ->
 139 (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)
 140 ->
 141 (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)
 142 ->
 143 (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)
 144 ->
 145 (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)
 146 ->
 147 (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)
 148 ->
 149 (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)
 150
 151 [4'  658K m=7 n=6 K=13 ty=50'']
 152
 153 ----------------------------------------------------------------
 154
 155 !x:R.!y:R.!z:R.!t:R.
 156 (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)
 157 ->
 158 (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)
 159 ->
 160 (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)
 161 ->
 162 (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)
 163 ->
 164 (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)
 165
 166 [3':20''  658K m=5 n=4 K=13 ty=41'']
 167
 168
 169
 170