From 8c09d8af35c34798270b484f2dfe6098be2eb0a2 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:46:58 -0500 Subject: Refresh patches Remove 0002-Remove-test-4366-too-picky-on-the-timeout.patch, since upstream has increased the timeout. --- ...Remove-test-4366-too-picky-on-the-timeout.patch | 30 - debian/patches/0002-Remove-test-4429.patch | 46 + ....v-and-4811.v-due-to-timeout-on-small-pla.patch | 1717 +++++++++++++++++++ debian/patches/0003-Remove-test-4429.patch | 46 - debian/patches/0004-5127-fails-on-mips.patch | 30 + ....v-and-4811.v-due-to-timeout-on-small-pla.patch | 1732 -------------------- debian/patches/0005-5127-fails-on-mips.patch | 30 - debian/patches/series | 7 +- 8 files changed, 1796 insertions(+), 1842 deletions(-) delete mode 100644 debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch create mode 100644 debian/patches/0002-Remove-test-4429.patch create mode 100644 debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch delete mode 100644 debian/patches/0003-Remove-test-4429.patch create mode 100644 debian/patches/0004-5127-fails-on-mips.patch delete mode 100644 debian/patches/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch delete mode 100644 debian/patches/0005-5127-fails-on-mips.patch diff --git a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch deleted file mode 100644 index e71306ce..00000000 --- a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Enrico Tassi -Date: Tue, 26 Jan 2016 16:58:25 +0100 -Subject: Remove test 4366 (too picky on the timeout) - ---- - test-suite/bugs/closed/4366.v | 15 --------------- - 1 file changed, 15 deletions(-) - delete mode 100644 test-suite/bugs/closed/4366.v - -diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v -deleted file mode 100644 -index 6a5e9a4..0000000 ---- a/test-suite/bugs/closed/4366.v -+++ /dev/null -@@ -1,15 +0,0 @@ --Fixpoint stupid (n : nat) : unit := --match n with --| 0 => tt --| S n => -- let () := stupid n in -- let () := stupid n in -- tt --end. -- --Goal True. --Proof. --pose (v := stupid 24). --Timeout 2 vm_compute in v. --exact I. --Qed. diff --git a/debian/patches/0002-Remove-test-4429.patch b/debian/patches/0002-Remove-test-4429.patch new file mode 100644 index 00000000..9baee306 --- /dev/null +++ b/debian/patches/0002-Remove-test-4429.patch @@ -0,0 +1,46 @@ +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/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch new file mode 100644 index 00000000..45acd396 --- /dev/null +++ b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch @@ -0,0 +1,1717 @@ +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/0003-Remove-test-4429.patch b/debian/patches/0003-Remove-test-4429.patch deleted file mode 100644 index 9baee306..00000000 --- a/debian/patches/0003-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/0004-5127-fails-on-mips.patch b/debian/patches/0004-5127-fails-on-mips.patch new file mode 100644 index 00000000..949c33a7 --- /dev/null +++ b/debian/patches/0004-5127-fails-on-mips.patch @@ -0,0 +1,30 @@ +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/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch deleted file mode 100644 index f762e040..00000000 --- a/debian/patches/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +++ /dev/null @@ -1,1732 +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 - ---- - test-suite/bugs/closed/3441.v | 23 - - test-suite/bugs/closed/4811.v | 1685 ----------------------------------------- - 2 files changed, 1708 deletions(-) - delete mode 100644 test-suite/bugs/closed/3441.v - delete mode 100644 test-suite/bugs/closed/4811.v - -diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v -deleted file mode 100644 -index 50d2978..0000000 ---- 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) *) -\ No newline at end of file -diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v -deleted file mode 100644 -index a914962..0000000 ---- 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: ("-emacs" "-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/0005-5127-fails-on-mips.patch b/debian/patches/0005-5127-fails-on-mips.patch deleted file mode 100644 index 949c33a7..00000000 --- a/debian/patches/0005-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/series b/debian/patches/series index 7285ccd8..aea3a7f2 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,5 +1,4 @@ 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch -0002-Remove-test-4366-too-picky-on-the-timeout.patch -0003-Remove-test-4429.patch -0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch -0005-5127-fails-on-mips.patch +0002-Remove-test-4429.patch +0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +0004-5127-fails-on-mips.patch -- cgit v1.2.3