From c40a76c5acdba3dc141cbeaf250ca394ae29ee20 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 12:11:16 -0500 Subject: Consolidate patches to disable tests that are too big or too slow Consolidate the several patches that disable tests that time out on MIPS or use too much RAM/time on the buildds. --- debian/patches/5127-fails-on-mips.patch | 30 - ....v-and-4811.v-due-to-timeout-on-small-pla.patch | 1717 ------------------- debian/patches/Remove-test-4429.patch | 46 - debian/patches/remove-heavy-tests.patch | 43 + debian/patches/remove-time-sensitive-tests.patch | 1754 ++++++++++++++++++++ debian/patches/series | 6 +- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 - 7 files changed, 1799 insertions(+), 1826 deletions(-) delete mode 100644 debian/patches/5127-fails-on-mips.patch delete mode 100644 debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch delete mode 100644 debian/patches/Remove-test-4429.patch create mode 100644 debian/patches/remove-heavy-tests.patch create mode 100644 debian/patches/remove-time-sensitive-tests.patch delete mode 100644 debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch diff --git a/debian/patches/5127-fails-on-mips.patch b/debian/patches/5127-fails-on-mips.patch deleted file mode 100644 index 949c33a7..00000000 --- a/debian/patches/5127-fails-on-mips.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Enrico Tassi -Date: Thu, 29 Dec 2016 08:56:45 +0100 -Subject: 5127 fails on mips - ---- - test-suite/bugs/closed/5127.v | 15 --------------- - 1 file changed, 15 deletions(-) - delete mode 100644 test-suite/bugs/closed/5127.v - -diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v -deleted file mode 100644 -index 831e8fb..0000000 ---- a/test-suite/bugs/closed/5127.v -+++ /dev/null -@@ -1,15 +0,0 @@ --Fixpoint arrow (n: nat) := -- match n with -- | S n => bool -> arrow n -- | O => bool -- end. -- --Fixpoint apply (n : nat) : arrow n -> bool := -- match n return arrow n -> bool with -- | S n => fun f => apply _ (f true) -- | O => fun x => x -- end. -- --Axiom f : arrow 10000. --Definition v : bool := Eval compute in apply _ f. --Definition w : bool := Eval vm_compute in v. diff --git a/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch deleted file mode 100644 index 45acd396..00000000 --- a/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +++ /dev/null @@ -1,1717 +0,0 @@ -From: Enrico Tassi -Date: Wed, 28 Dec 2016 18:18:34 +0100 -Subject: Remove 3441.v and 4811.v due to timeout on small platforms ---- a/test-suite/bugs/closed/3441.v -+++ /dev/null -@@ -1,23 +0,0 @@ --Axiom f : nat -> nat -> nat. --Fixpoint do_n (n : nat) (k : nat) := -- match n with -- | 0 => k -- | S n' => do_n n' (f k k) -- end. -- --Notation big := (_ = _). --Axiom k : nat. --Goal True. --Timeout 1 let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) --Timeout 1 let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) -- --Timeout 1 Time let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) ---- a/test-suite/bugs/closed/4811.v -+++ /dev/null -@@ -1,1685 +0,0 @@ --(* Test about a slowness of f_equal in 8.5pl1 *) -- --(* Submitted by Jason Gross *) -- --(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) --(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) --(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 -- coqtop version 8.5pl1 (April 2016) *) --Require Coq.ZArith.ZArith. -- --Import Coq.ZArith.ZArith. -- --Axiom F : Z -> Set. --Definition Let_In {A P} (x : A) (f : forall y : A, P y) -- := let y := x in f y. --Local Open Scope Z_scope. --Definition modulus : Z := 2^255 - 19. --Axiom decode : list Z -> F modulus. --Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, -- let Zmul := Z.mul in -- let Zadd := Z.add in -- let Zsub := Z.sub in -- let Zpow_pos := Z.pow_pos in -- @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) -- (@decode -- (@Let_In Z (fun _ : Z => list Z) -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (fun z : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (fun z0 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (fun z1 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (fun z2 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (fun z3 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (fun z4 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (fun z5 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (fun z6 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) -- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (fun z7 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) -- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) -- (Zmul x1 y8)) (Zmul x0 y9))) -- (fun z8 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land z -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (fun z9 : Z => -- @cons Z -- (Z.land z9 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) -- (Z.land z0 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z1 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z2 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z3 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z4 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z5 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z6 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z7 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z8 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@nil Z))))))))))))))))))))))) -- (@decode -- (@cons Z -- (Z.land -- (Zadd -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) -- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) -- (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) -- (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) -- (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Zadd -- (Z.shiftr -- (Zadd -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) -- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) -- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) -- (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) -- (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) -- (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) -- (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul (Zmul x9 y1) (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) -- (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) -- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul -- (Zmul x3 y7) -- (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y3) -- (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) -- (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) -- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) -- (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) -- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) -- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) -- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul -- (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul -- (Zmul x3 y7) -- (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul -- (Zmul x1 y9) -- (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y3) -- (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul -- (Zmul x7 y5) -- (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul -- (Zmul x5 y7) -- (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) -- (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) -- (Zmul x6 y7)) -- (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x4 y0) -- (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) -- (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x6 y0) -- (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) -- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) -- (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) -- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) -- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) -- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) -- (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) -- (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) -- (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@nil Z)))))))))))). -- cbv beta zeta. -- intros. -- (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". -- Undo. -- Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/debian/patches/Remove-test-4429.patch b/debian/patches/Remove-test-4429.patch deleted file mode 100644 index 9baee306..00000000 --- a/debian/patches/Remove-test-4429.patch +++ /dev/null @@ -1,46 +0,0 @@ -From: Enrico Tassi -Date: Thu, 28 Jan 2016 10:11:08 +0100 -Subject: Remove test 4429 - ---- - test-suite/bugs/closed/4429.v | 31 ------------------------------- - 1 file changed, 31 deletions(-) - delete mode 100644 test-suite/bugs/closed/4429.v - -diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v -deleted file mode 100644 -index bf0e570..0000000 ---- a/test-suite/bugs/closed/4429.v -+++ /dev/null -@@ -1,31 +0,0 @@ --Require Import Arith.Compare_dec. --Require Import Unicode.Utf8. -- --Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := -- match n with -- | O => x -- | S n' => f (my_nat_iter n' f x) -- end. -- --Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := -- match mn with -- | (0, 0) => 0 -- | (0, S n') => S n' -- | (S m', 0) => S m' -- | (S m', S n') => -- match le_gt_dec (S m') (S n') with -- | left _ => f (S m', S n' - S m') -- | right _ => f (S m' - S n', S n') -- end -- end. -- --Axiom max_correct_l : ∀ m n : nat, m <= max m n. --Axiom max_correct_r : ∀ m n : nat, n <= max m n. -- --Hint Resolve max_correct_l max_correct_r : arith. -- --Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). --Proof. -- intros. -- Timeout 3 eauto with arith. --Qed. diff --git a/debian/patches/remove-heavy-tests.patch b/debian/patches/remove-heavy-tests.patch new file mode 100644 index 00000000..2cc8e17c --- /dev/null +++ b/debian/patches/remove-heavy-tests.patch @@ -0,0 +1,43 @@ +From: Benjamin Barenblat +Subject: Remove heavyweight tests +Forwarded: not-needed + +Remove tests that use too much RAM or time to run on a buildd. (The MIPS +buildd is frequently the culprit, as MIPS lacks an OCaml native +compiler.) +--- a/test-suite/bugs/closed/5127.v ++++ /dev/null +@@ -1,15 +0,0 @@ +-Fixpoint arrow (n: nat) := +- match n with +- | S n => bool -> arrow n +- | O => bool +- end. +- +-Fixpoint apply (n : nat) : arrow n -> bool := +- match n return arrow n -> bool with +- | S n => fun f => apply _ (f true) +- | O => fun x => x +- end. +- +-Axiom f : arrow 10000. +-Definition v : bool := Eval compute in apply _ f. +-Definition w : bool := Eval vm_compute in v. +--- a/test-suite/success/Nsatz.v ++++ b/test-suite/success/Nsatz.v +@@ -462,6 +462,7 @@ idtac "chords". + (*Finished transaction in 4. secs (3.959398u,0.s)*) + Qed. + ++(* + Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> +@@ -473,6 +474,7 @@ idtac "Ceva". + Time nsatz. + (*Finished transaction in 105. secs (104.121171u,0.474928s)*) + Qed. ++*) + + Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> diff --git a/debian/patches/remove-time-sensitive-tests.patch b/debian/patches/remove-time-sensitive-tests.patch new file mode 100644 index 00000000..8a5d640b --- /dev/null +++ b/debian/patches/remove-time-sensitive-tests.patch @@ -0,0 +1,1754 @@ +From: Benjamin Barenblat +Subject: Remove time-sensitive tests +Forwarded: not-needed + +Remove tests that have tight timing bounds. These tests consistently run +too slowly to pass on platforms without OCaml native compilers (MIPS). +--- a/test-suite/bugs/closed/3441.v ++++ /dev/null +@@ -1,23 +0,0 @@ +-Axiom f : nat -> nat -> nat. +-Fixpoint do_n (n : nat) (k : nat) := +- match n with +- | 0 => k +- | S n' => do_n n' (f k k) +- end. +- +-Notation big := (_ = _). +-Axiom k : nat. +-Goal True. +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) +- +-Timeout 1 Time let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) +--- a/test-suite/bugs/closed/4429.v ++++ /dev/null +@@ -1,31 +0,0 @@ +-Require Import Arith.Compare_dec. +-Require Import Unicode.Utf8. +- +-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := +- match n with +- | O => x +- | S n' => f (my_nat_iter n' f x) +- end. +- +-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := +- match mn with +- | (0, 0) => 0 +- | (0, S n') => S n' +- | (S m', 0) => S m' +- | (S m', S n') => +- match le_gt_dec (S m') (S n') with +- | left _ => f (S m', S n' - S m') +- | right _ => f (S m' - S n', S n') +- end +- end. +- +-Axiom max_correct_l : ∀ m n : nat, m <= max m n. +-Axiom max_correct_r : ∀ m n : nat, n <= max m n. +- +-Hint Resolve max_correct_l max_correct_r : arith. +- +-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +-Proof. +- intros. +- Timeout 3 eauto with arith. +-Qed. +--- a/test-suite/bugs/closed/4811.v ++++ /dev/null +@@ -1,1685 +0,0 @@ +-(* Test about a slowness of f_equal in 8.5pl1 *) +- +-(* Submitted by Jason Gross *) +- +-(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +-(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) +-(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 +- coqtop version 8.5pl1 (April 2016) *) +-Require Coq.ZArith.ZArith. +- +-Import Coq.ZArith.ZArith. +- +-Axiom F : Z -> Set. +-Definition Let_In {A P} (x : A) (f : forall y : A, P y) +- := let y := x in f y. +-Local Open Scope Z_scope. +-Definition modulus : Z := 2^255 - 19. +-Axiom decode : list Z -> F modulus. +-Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, +- let Zmul := Z.mul in +- let Zadd := Z.add in +- let Zsub := Z.sub in +- let Zpow_pos := Z.pow_pos in +- @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) +- (@decode +- (@Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (fun z : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (fun z0 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (fun z1 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (fun z2 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (fun z3 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (fun z4 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (fun z5 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (fun z6 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (fun z7 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) +- (fun z8 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land z +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (fun z9 : Z => +- @cons Z +- (Z.land z9 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land z0 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z1 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z2 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z3 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z4 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z5 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z6 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z7 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z8 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z))))))))))))))))))))))) +- (@decode +- (@cons Z +- (Z.land +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) +- (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd +- (Z.shiftr +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul +- (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul +- (Zmul x1 y9) +- (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul +- (Zmul x7 y5) +- (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul +- (Zmul x5 y7) +- (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) +- (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) +- (Zmul x6 y7)) +- (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) +- (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x6 y0) +- (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) +- (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) +- (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z)))))))))))). +- cbv beta zeta. +- intros. +- (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". +- Undo. +- Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/debian/patches/series b/debian/patches/series index 4f1f3fcf..eb7aeee1 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,7 +1,5 @@ -test-suite-success-Nsatz.v-comment-out-Ceva.patch -Remove-test-4429.patch -Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch -5127-fails-on-mips.patch +remove-heavy-tests.patch +remove-time-sensitive-tests.patch remove-tests-that-need-coqlib.patch avoid-usr-bin-env.patch python-scripts-libraries.patch diff --git a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch deleted file mode 100644 index 2cf6af5c..00000000 --- a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,29 +0,0 @@ -From: Stephane Glondu -Date: Sun, 15 Jan 2012 12:34:19 +0100 -Subject: test-suite/success/Nsatz.v: comment out Ceva - -This lemma uses too much memory for many buildds... ---- - test-suite/success/Nsatz.v | 2 ++ - 1 file changed, 2 insertions(+) - -diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v -index e38affd..040169e 100644 ---- a/test-suite/success/Nsatz.v -+++ b/test-suite/success/Nsatz.v -@@ -462,6 +462,7 @@ idtac "chords". - (*Finished transaction in 4. secs (3.959398u,0.s)*) - Qed. - -+(* - Lemma Ceva: forall A B C D E F M:point, - collinear M A D -> collinear M B E -> collinear M C F -> - collinear B C D -> collinear E A C -> collinear F A B -> -@@ -473,6 +474,7 @@ idtac "Ceva". - Time nsatz. - (*Finished transaction in 105. secs (104.121171u,0.474928s)*) - Qed. -+*) - - Lemma bissectrices: forall A B C M:point, - equaltangente C A M M A B -> -- cgit v1.2.3