fact: Definition mul x y := match x, y with | N0 wx, N0 wy => reduce_1 (w0_mul_c wx wy) | N0 wx, N1 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 1 wy wx w_0 in if w0_eq0 w then N1 r else N2 (WW (WW w_0 w) r) | N0 wx, N2 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 2 wy wx w_0 in if w0_eq0 w then N2 r else N3 (WW (extend1 w0 (WW w_0 w)) r) | N0 wx, N3 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 3 wy wx w_0 in if w0_eq0 w then N3 r else N4 (WW (extend2 w0 (WW w_0 w)) r) | N0 wx, N4 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 4 wy wx w_0 in if w0_eq0 w then N4 r else N5 (WW (extend3 w0 (WW w_0 w)) r) | N0 wx, N5 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 5 wy wx w_0 in if w0_eq0 w then N5 r else N6 (WW (extend4 w0 (WW w_0 w)) r) | N0 wx, N6 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 6 wy wx w_0 in if w0_eq0 w then N6 r else N7 (WW (extend5 w0 (WW w_0 w)) r) | N0 wx, N7 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 7 wy wx w_0 in if w0_eq0 w then N7 r else N8 (WW (extend6 w0 (WW w_0 w)) r) | N0 wx, N8 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 8 wy wx w_0 in if w0_eq0 w then N8 r else N9 (WW (extend7 w0 (WW w_0 w)) r) | N0 wx, N9 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 9 wy wx w_0 in if w0_eq0 w then N9 r else N10 (WW (extend8 w0 (WW w_0 w)) r) | N0 wx, N10 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 10 wy wx w_0 in if w0_eq0 w then N10 r else N11 (WW (extend9 w0 (WW w_0 w)) r) | N0 wx, N11 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 11 wy wx w_0 in if w0_eq0 w then N11 r else N12 (WW (extend10 w0 (WW w_0 w)) r) | N0 wx, N12 wy => if w0_eq0 wx then zero else let (w,r) := w0_mul_add_n1 12 wy wx w_0 in if w0_eq0 w then N12 r else Nn 0 (WW (extend11 w0 (WW w_0 w)) r) | N0 wx, Nn n wy => if w0_eq0 wx then zero else let (w,r) := gen_mul_add_mn1 w_0 (fun r => extend11 w0 (WW w_0 r)) w12_op.(znz_0W) w12_op.(znz_WW) (w0_mul_add_n1 12) (S n) wy wx w_0 in if w0_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (extend12 w0 (WW w_0 w))) r) | N1 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 1 wx wy w_0 in if w0_eq0 w then N1 r else N2 (WW (WW w_0 w) r) | N1 wx, N1 wy => N2 (w1_mul_c wx wy) | N1 wx, N2 wy => let (w,r) := w1_mul_add_n1 1 wy wx W0 in if w1_eq0 w then N2 r else N3 (WW (extend1 w0 w) r) | N1 wx, N3 wy => let (w,r) := w1_mul_add_n1 2 wy wx W0 in if w1_eq0 w then N3 r else N4 (WW (extend2 w0 w) r) | N1 wx, N4 wy => let (w,r) := w1_mul_add_n1 3 wy wx W0 in if w1_eq0 w then N4 r else N5 (WW (extend3 w0 w) r) | N1 wx, N5 wy => let (w,r) := w1_mul_add_n1 4 wy wx W0 in if w1_eq0 w then N5 r else N6 (WW (extend4 w0 w) r) | N1 wx, N6 wy => let (w,r) := w1_mul_add_n1 5 wy wx W0 in if w1_eq0 w then N6 r else N7 (WW (extend5 w0 w) r) | N1 wx, N7 wy => let (w,r) := w1_mul_add_n1 6 wy wx W0 in if w1_eq0 w then N7 r else N8 (WW (extend6 w0 w) r) | N1 wx, N8 wy => let (w,r) := w1_mul_add_n1 7 wy wx W0 in if w1_eq0 w then N8 r else N9 (WW (extend7 w0 w) r) | N1 wx, N9 wy => let (w,r) := w1_mul_add_n1 8 wy wx W0 in if w1_eq0 w then N9 r else N10 (WW (extend8 w0 w) r) | N1 wx, N10 wy => let (w,r) := w1_mul_add_n1 9 wy wx W0 in if w1_eq0 w then N10 r else N11 (WW (extend9 w0 w) r) | N1 wx, N11 wy => let (w,r) := w1_mul_add_n1 10 wy wx W0 in if w1_eq0 w then N11 r else N12 (WW (extend10 w0 w) r) | N1 wx, N12 wy => let (w,r) := w1_mul_add_n1 11 wy wx W0 in if w1_eq0 w then N12 r else Nn 0 (WW (extend11 w0 w) r) | N1 wx, Nn n wy => let (w,r) := gen_mul_add_mn1 W0 (fun r => extend11 w0 r) w12_op.(znz_0W) w12_op.(znz_WW) (w1_mul_add_n1 11) (S n) wy wx W0 in if w1_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (extend12 w0 w)) r) | N2 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 2 wx wy w_0 in if w0_eq0 w then N2 r else N3 (WW (extend1 w0 (WW w_0 w)) r) | N2 wx, N1 wy => let (w,r) := w1_mul_add_n1 1 wx wy W0 in if w1_eq0 w then N2 r else N3 (WW (extend1 w0 w) r) | N2 wx, N2 wy => N3 (w2_mul_c wx wy) | N2 wx, N3 wy => let (w,r) := w2_mul_add_n1 1 wy wx W0 in if w2_eq0 w then N3 r else N4 (WW (extend1 w1 w) r) | N2 wx, N4 wy => let (w,r) := w2_mul_add_n1 2 wy wx W0 in if w2_eq0 w then N4 r else N5 (WW (extend2 w1 w) r) | N2 wx, N5 wy => let (w,r) := w2_mul_add_n1 3 wy wx W0 in if w2_eq0 w then N5 r else N6 (WW (extend3 w1 w) r) | N2 wx, N6 wy => let (w,r) := w2_mul_add_n1 4 wy wx W0 in if w2_eq0 w then N6 r else N7 (WW (extend4 w1 w) r) | N2 wx, N7 wy => let (w,r) := w2_mul_add_n1 5 wy wx W0 in if w2_eq0 w then N7 r else N8 (WW (extend5 w1 w) r) | N2 wx, N8 wy => let (w,r) := w2_mul_add_n1 6 wy wx W0 in if w2_eq0 w then N8 r else N9 (WW (extend6 w1 w) r) | N2 wx, N9 wy => let (w,r) := w2_mul_add_n1 7 wy wx W0 in if w2_eq0 w then N9 r else N10 (WW (extend7 w1 w) r) | N2 wx, N10 wy => let (w,r) := w2_mul_add_n1 8 wy wx W0 in if w2_eq0 w then N10 r else N11 (WW (extend8 w1 w) r) | N2 wx, N11 wy => let (w,r) := w2_mul_add_n1 9 wy wx W0 in if w2_eq0 w then N11 r else N12 (WW (extend9 w1 w) r) | N2 wx, N12 wy => let (w,r) := w2_mul_add_n1 10 wy wx W0 in if w2_eq0 w then N12 r else Nn 0 (WW (extend10 w1 w) r) | N2 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend10 w1 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N3 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 3 wx wy w_0 in if w0_eq0 w then N3 r else N4 (WW (extend2 w0 (WW w_0 w)) r) | N3 wx, N1 wy => let (w,r) := w1_mul_add_n1 2 wx wy W0 in if w1_eq0 w then N3 r else N4 (WW (extend2 w0 w) r) | N3 wx, N2 wy => let (w,r) := w2_mul_add_n1 1 wx wy W0 in if w2_eq0 w then N3 r else N4 (WW (extend1 w1 w) r) | N3 wx, N3 wy => N4 (w3_mul_c wx wy) | N3 wx, N4 wy => let (w,r) := w3_mul_add_n1 1 wy wx W0 in if w3_eq0 w then N4 r else N5 (WW (extend1 w2 w) r) | N3 wx, N5 wy => let (w,r) := w3_mul_add_n1 2 wy wx W0 in if w3_eq0 w then N5 r else N6 (WW (extend2 w2 w) r) | N3 wx, N6 wy => let (w,r) := w3_mul_add_n1 3 wy wx W0 in if w3_eq0 w then N6 r else N7 (WW (extend3 w2 w) r) | N3 wx, N7 wy => let (w,r) := w3_mul_add_n1 4 wy wx W0 in if w3_eq0 w then N7 r else N8 (WW (extend4 w2 w) r) | N3 wx, N8 wy => let (w,r) := w3_mul_add_n1 5 wy wx W0 in if w3_eq0 w then N8 r else N9 (WW (extend5 w2 w) r) | N3 wx, N9 wy => let (w,r) := w3_mul_add_n1 6 wy wx W0 in if w3_eq0 w then N9 r else N10 (WW (extend6 w2 w) r) | N3 wx, N10 wy => let (w,r) := w3_mul_add_n1 7 wy wx W0 in if w3_eq0 w then N10 r else N11 (WW (extend7 w2 w) r) | N3 wx, N11 wy => let (w,r) := w3_mul_add_n1 8 wy wx W0 in if w3_eq0 w then N11 r else N12 (WW (extend8 w2 w) r) | N3 wx, N12 wy => let (w,r) := w3_mul_add_n1 9 wy wx W0 in if w3_eq0 w then N12 r else Nn 0 (WW (extend9 w2 w) r) | N3 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend9 w2 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N4 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 4 wx wy w_0 in if w0_eq0 w then N4 r else N5 (WW (extend3 w0 (WW w_0 w)) r) | N4 wx, N1 wy => let (w,r) := w1_mul_add_n1 3 wx wy W0 in if w1_eq0 w then N4 r else N5 (WW (extend3 w0 w) r) | N4 wx, N2 wy => let (w,r) := w2_mul_add_n1 2 wx wy W0 in if w2_eq0 w then N4 r else N5 (WW (extend2 w1 w) r) | N4 wx, N3 wy => let (w,r) := w3_mul_add_n1 1 wx wy W0 in if w3_eq0 w then N4 r else N5 (WW (extend1 w2 w) r) | N4 wx, N4 wy => N5 (w4_mul_c wx wy) | N4 wx, N5 wy => let (w,r) := w4_mul_add_n1 1 wy wx W0 in if w4_eq0 w then N5 r else N6 (WW (extend1 w3 w) r) | N4 wx, N6 wy => let (w,r) := w4_mul_add_n1 2 wy wx W0 in if w4_eq0 w then N6 r else N7 (WW (extend2 w3 w) r) | N4 wx, N7 wy => let (w,r) := w4_mul_add_n1 3 wy wx W0 in if w4_eq0 w then N7 r else N8 (WW (extend3 w3 w) r) | N4 wx, N8 wy => let (w,r) := w4_mul_add_n1 4 wy wx W0 in if w4_eq0 w then N8 r else N9 (WW (extend4 w3 w) r) | N4 wx, N9 wy => let (w,r) := w4_mul_add_n1 5 wy wx W0 in if w4_eq0 w then N9 r else N10 (WW (extend5 w3 w) r) | N4 wx, N10 wy => let (w,r) := w4_mul_add_n1 6 wy wx W0 in if w4_eq0 w then N10 r else N11 (WW (extend6 w3 w) r) | N4 wx, N11 wy => let (w,r) := w4_mul_add_n1 7 wy wx W0 in if w4_eq0 w then N11 r else N12 (WW (extend7 w3 w) r) | N4 wx, N12 wy => let (w,r) := w4_mul_add_n1 8 wy wx W0 in if w4_eq0 w then N12 r else Nn 0 (WW (extend8 w3 w) r) | N4 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend8 w3 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N5 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 5 wx wy w_0 in if w0_eq0 w then N5 r else N6 (WW (extend4 w0 (WW w_0 w)) r) | N5 wx, N1 wy => let (w,r) := w1_mul_add_n1 4 wx wy W0 in if w1_eq0 w then N5 r else N6 (WW (extend4 w0 w) r) | N5 wx, N2 wy => let (w,r) := w2_mul_add_n1 3 wx wy W0 in if w2_eq0 w then N5 r else N6 (WW (extend3 w1 w) r) | N5 wx, N3 wy => let (w,r) := w3_mul_add_n1 2 wx wy W0 in if w3_eq0 w then N5 r else N6 (WW (extend2 w2 w) r) | N5 wx, N4 wy => let (w,r) := w4_mul_add_n1 1 wx wy W0 in if w4_eq0 w then N5 r else N6 (WW (extend1 w3 w) r) | N5 wx, N5 wy => N6 (w5_mul_c wx wy) | N5 wx, N6 wy => let (w,r) := w5_mul_add_n1 1 wy wx W0 in if w5_eq0 w then N6 r else N7 (WW (extend1 w4 w) r) | N5 wx, N7 wy => let (w,r) := w5_mul_add_n1 2 wy wx W0 in if w5_eq0 w then N7 r else N8 (WW (extend2 w4 w) r) | N5 wx, N8 wy => let (w,r) := w5_mul_add_n1 3 wy wx W0 in if w5_eq0 w then N8 r else N9 (WW (extend3 w4 w) r) | N5 wx, N9 wy => let (w,r) := w5_mul_add_n1 4 wy wx W0 in if w5_eq0 w then N9 r else N10 (WW (extend4 w4 w) r) | N5 wx, N10 wy => let (w,r) := w5_mul_add_n1 5 wy wx W0 in if w5_eq0 w then N10 r else N11 (WW (extend5 w4 w) r) | N5 wx, N11 wy => let (w,r) := w5_mul_add_n1 6 wy wx W0 in if w5_eq0 w then N11 r else N12 (WW (extend6 w4 w) r) | N5 wx, N12 wy => let (w,r) := w5_mul_add_n1 7 wy wx W0 in if w5_eq0 w then N12 r else Nn 0 (WW (extend7 w4 w) r) | N5 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend7 w4 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N6 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 6 wx wy w_0 in if w0_eq0 w then N6 r else N7 (WW (extend5 w0 (WW w_0 w)) r) | N6 wx, N1 wy => let (w,r) := w1_mul_add_n1 5 wx wy W0 in if w1_eq0 w then N6 r else N7 (WW (extend5 w0 w) r) | N6 wx, N2 wy => let (w,r) := w2_mul_add_n1 4 wx wy W0 in if w2_eq0 w then N6 r else N7 (WW (extend4 w1 w) r) | N6 wx, N3 wy => let (w,r) := w3_mul_add_n1 3 wx wy W0 in if w3_eq0 w then N6 r else N7 (WW (extend3 w2 w) r) | N6 wx, N4 wy => let (w,r) := w4_mul_add_n1 2 wx wy W0 in if w4_eq0 w then N6 r else N7 (WW (extend2 w3 w) r) | N6 wx, N5 wy => let (w,r) := w5_mul_add_n1 1 wx wy W0 in if w5_eq0 w then N6 r else N7 (WW (extend1 w4 w) r) | N6 wx, N6 wy => N7 (w6_mul_c wx wy) | N6 wx, N7 wy => let (w,r) := w6_mul_add_n1 1 wy wx W0 in if w6_eq0 w then N7 r else N8 (WW (extend1 w5 w) r) | N6 wx, N8 wy => let (w,r) := w6_mul_add_n1 2 wy wx W0 in if w6_eq0 w then N8 r else N9 (WW (extend2 w5 w) r) | N6 wx, N9 wy => let (w,r) := w6_mul_add_n1 3 wy wx W0 in if w6_eq0 w then N9 r else N10 (WW (extend3 w5 w) r) | N6 wx, N10 wy => let (w,r) := w6_mul_add_n1 4 wy wx W0 in if w6_eq0 w then N10 r else N11 (WW (extend4 w5 w) r) | N6 wx, N11 wy => let (w,r) := w6_mul_add_n1 5 wy wx W0 in if w6_eq0 w then N11 r else N12 (WW (extend5 w5 w) r) | N6 wx, N12 wy => let (w,r) := w6_mul_add_n1 6 wy wx W0 in if w6_eq0 w then N12 r else Nn 0 (WW (extend6 w5 w) r) | N6 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend6 w5 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N7 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 7 wx wy w_0 in if w0_eq0 w then N7 r else N8 (WW (extend6 w0 (WW w_0 w)) r) | N7 wx, N1 wy => let (w,r) := w1_mul_add_n1 6 wx wy W0 in if w1_eq0 w then N7 r else N8 (WW (extend6 w0 w) r) | N7 wx, N2 wy => let (w,r) := w2_mul_add_n1 5 wx wy W0 in if w2_eq0 w then N7 r else N8 (WW (extend5 w1 w) r) | N7 wx, N3 wy => let (w,r) := w3_mul_add_n1 4 wx wy W0 in if w3_eq0 w then N7 r else N8 (WW (extend4 w2 w) r) | N7 wx, N4 wy => let (w,r) := w4_mul_add_n1 3 wx wy W0 in if w4_eq0 w then N7 r else N8 (WW (extend3 w3 w) r) | N7 wx, N5 wy => let (w,r) := w5_mul_add_n1 2 wx wy W0 in if w5_eq0 w then N7 r else N8 (WW (extend2 w4 w) r) | N7 wx, N6 wy => let (w,r) := w6_mul_add_n1 1 wx wy W0 in if w6_eq0 w then N7 r else N8 (WW (extend1 w5 w) r) | N7 wx, N7 wy => N8 (w7_mul_c wx wy) | N7 wx, N8 wy => let (w,r) := w7_mul_add_n1 1 wy wx W0 in if w7_eq0 w then N8 r else N9 (WW (extend1 w6 w) r) | N7 wx, N9 wy => let (w,r) := w7_mul_add_n1 2 wy wx W0 in if w7_eq0 w then N9 r else N10 (WW (extend2 w6 w) r) | N7 wx, N10 wy => let (w,r) := w7_mul_add_n1 3 wy wx W0 in if w7_eq0 w then N10 r else N11 (WW (extend3 w6 w) r) | N7 wx, N11 wy => let (w,r) := w7_mul_add_n1 4 wy wx W0 in if w7_eq0 w then N11 r else N12 (WW (extend4 w6 w) r) | N7 wx, N12 wy => let (w,r) := w7_mul_add_n1 5 wy wx W0 in if w7_eq0 w then N12 r else Nn 0 (WW (extend5 w6 w) r) | N7 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend5 w6 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N8 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 8 wx wy w_0 in if w0_eq0 w then N8 r else N9 (WW (extend7 w0 (WW w_0 w)) r) | N8 wx, N1 wy => let (w,r) := w1_mul_add_n1 7 wx wy W0 in if w1_eq0 w then N8 r else N9 (WW (extend7 w0 w) r) | N8 wx, N2 wy => let (w,r) := w2_mul_add_n1 6 wx wy W0 in if w2_eq0 w then N8 r else N9 (WW (extend6 w1 w) r) | N8 wx, N3 wy => let (w,r) := w3_mul_add_n1 5 wx wy W0 in if w3_eq0 w then N8 r else N9 (WW (extend5 w2 w) r) | N8 wx, N4 wy => let (w,r) := w4_mul_add_n1 4 wx wy W0 in if w4_eq0 w then N8 r else N9 (WW (extend4 w3 w) r) | N8 wx, N5 wy => let (w,r) := w5_mul_add_n1 3 wx wy W0 in if w5_eq0 w then N8 r else N9 (WW (extend3 w4 w) r) | N8 wx, N6 wy => let (w,r) := w6_mul_add_n1 2 wx wy W0 in if w6_eq0 w then N8 r else N9 (WW (extend2 w5 w) r) | N8 wx, N7 wy => let (w,r) := w7_mul_add_n1 1 wx wy W0 in if w7_eq0 w then N8 r else N9 (WW (extend1 w6 w) r) | N8 wx, N8 wy => N9 (w8_mul_c wx wy) | N8 wx, N9 wy => let (w,r) := w8_mul_add_n1 1 wy wx W0 in if w8_eq0 w then N9 r else N10 (WW (extend1 w7 w) r) | N8 wx, N10 wy => let (w,r) := w8_mul_add_n1 2 wy wx W0 in if w8_eq0 w then N10 r else N11 (WW (extend2 w7 w) r) | N8 wx, N11 wy => let (w,r) := w8_mul_add_n1 3 wy wx W0 in if w8_eq0 w then N11 r else N12 (WW (extend3 w7 w) r) | N8 wx, N12 wy => let (w,r) := w8_mul_add_n1 4 wy wx W0 in if w8_eq0 w then N12 r else Nn 0 (WW (extend4 w7 w) r) | N8 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend4 w7 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N9 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 9 wx wy w_0 in if w0_eq0 w then N9 r else N10 (WW (extend8 w0 (WW w_0 w)) r) | N9 wx, N1 wy => let (w,r) := w1_mul_add_n1 8 wx wy W0 in if w1_eq0 w then N9 r else N10 (WW (extend8 w0 w) r) | N9 wx, N2 wy => let (w,r) := w2_mul_add_n1 7 wx wy W0 in if w2_eq0 w then N9 r else N10 (WW (extend7 w1 w) r) | N9 wx, N3 wy => let (w,r) := w3_mul_add_n1 6 wx wy W0 in if w3_eq0 w then N9 r else N10 (WW (extend6 w2 w) r) | N9 wx, N4 wy => let (w,r) := w4_mul_add_n1 5 wx wy W0 in if w4_eq0 w then N9 r else N10 (WW (extend5 w3 w) r) | N9 wx, N5 wy => let (w,r) := w5_mul_add_n1 4 wx wy W0 in if w5_eq0 w then N9 r else N10 (WW (extend4 w4 w) r) | N9 wx, N6 wy => let (w,r) := w6_mul_add_n1 3 wx wy W0 in if w6_eq0 w then N9 r else N10 (WW (extend3 w5 w) r) | N9 wx, N7 wy => let (w,r) := w7_mul_add_n1 2 wx wy W0 in if w7_eq0 w then N9 r else N10 (WW (extend2 w6 w) r) | N9 wx, N8 wy => let (w,r) := w8_mul_add_n1 1 wx wy W0 in if w8_eq0 w then N9 r else N10 (WW (extend1 w7 w) r) | N9 wx, N9 wy => N10 (w9_mul_c wx wy) | N9 wx, N10 wy => let (w,r) := w9_mul_add_n1 1 wy wx W0 in if w9_eq0 w then N10 r else N11 (WW (extend1 w8 w) r) | N9 wx, N11 wy => let (w,r) := w9_mul_add_n1 2 wy wx W0 in if w9_eq0 w then N11 r else N12 (WW (extend2 w8 w) r) | N9 wx, N12 wy => let (w,r) := w9_mul_add_n1 3 wy wx W0 in if w9_eq0 w then N12 r else Nn 0 (WW (extend3 w8 w) r) | N9 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend3 w8 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N10 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 10 wx wy w_0 in if w0_eq0 w then N10 r else N11 (WW (extend9 w0 (WW w_0 w)) r) | N10 wx, N1 wy => let (w,r) := w1_mul_add_n1 9 wx wy W0 in if w1_eq0 w then N10 r else N11 (WW (extend9 w0 w) r) | N10 wx, N2 wy => let (w,r) := w2_mul_add_n1 8 wx wy W0 in if w2_eq0 w then N10 r else N11 (WW (extend8 w1 w) r) | N10 wx, N3 wy => let (w,r) := w3_mul_add_n1 7 wx wy W0 in if w3_eq0 w then N10 r else N11 (WW (extend7 w2 w) r) | N10 wx, N4 wy => let (w,r) := w4_mul_add_n1 6 wx wy W0 in if w4_eq0 w then N10 r else N11 (WW (extend6 w3 w) r) | N10 wx, N5 wy => let (w,r) := w5_mul_add_n1 5 wx wy W0 in if w5_eq0 w then N10 r else N11 (WW (extend5 w4 w) r) | N10 wx, N6 wy => let (w,r) := w6_mul_add_n1 4 wx wy W0 in if w6_eq0 w then N10 r else N11 (WW (extend4 w5 w) r) | N10 wx, N7 wy => let (w,r) := w7_mul_add_n1 3 wx wy W0 in if w7_eq0 w then N10 r else N11 (WW (extend3 w6 w) r) | N10 wx, N8 wy => let (w,r) := w8_mul_add_n1 2 wx wy W0 in if w8_eq0 w then N10 r else N11 (WW (extend2 w7 w) r) | N10 wx, N9 wy => let (w,r) := w9_mul_add_n1 1 wx wy W0 in if w9_eq0 w then N10 r else N11 (WW (extend1 w8 w) r) | N10 wx, N10 wy => N11 (w10_mul_c wx wy) | N10 wx, N11 wy => let (w,r) := w10_mul_add_n1 1 wy wx W0 in if w10_eq0 w then N11 r else N12 (WW (extend1 w9 w) r) | N10 wx, N12 wy => let (w,r) := w10_mul_add_n1 2 wy wx W0 in if w10_eq0 w then N12 r else Nn 0 (WW (extend2 w9 w) r) | N10 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend2 w9 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N11 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 11 wx wy w_0 in if w0_eq0 w then N11 r else N12 (WW (extend10 w0 (WW w_0 w)) r) | N11 wx, N1 wy => let (w,r) := w1_mul_add_n1 10 wx wy W0 in if w1_eq0 w then N11 r else N12 (WW (extend10 w0 w) r) | N11 wx, N2 wy => let (w,r) := w2_mul_add_n1 9 wx wy W0 in if w2_eq0 w then N11 r else N12 (WW (extend9 w1 w) r) | N11 wx, N3 wy => let (w,r) := w3_mul_add_n1 8 wx wy W0 in if w3_eq0 w then N11 r else N12 (WW (extend8 w2 w) r) | N11 wx, N4 wy => let (w,r) := w4_mul_add_n1 7 wx wy W0 in if w4_eq0 w then N11 r else N12 (WW (extend7 w3 w) r) | N11 wx, N5 wy => let (w,r) := w5_mul_add_n1 6 wx wy W0 in if w5_eq0 w then N11 r else N12 (WW (extend6 w4 w) r) | N11 wx, N6 wy => let (w,r) := w6_mul_add_n1 5 wx wy W0 in if w6_eq0 w then N11 r else N12 (WW (extend5 w5 w) r) | N11 wx, N7 wy => let (w,r) := w7_mul_add_n1 4 wx wy W0 in if w7_eq0 w then N11 r else N12 (WW (extend4 w6 w) r) | N11 wx, N8 wy => let (w,r) := w8_mul_add_n1 3 wx wy W0 in if w8_eq0 w then N11 r else N12 (WW (extend3 w7 w) r) | N11 wx, N9 wy => let (w,r) := w9_mul_add_n1 2 wx wy W0 in if w9_eq0 w then N11 r else N12 (WW (extend2 w8 w) r) | N11 wx, N10 wy => let (w,r) := w10_mul_add_n1 1 wx wy W0 in if w10_eq0 w then N11 r else N12 (WW (extend1 w9 w) r) | N11 wx, N11 wy => N12 (w11_mul_c wx wy) | N11 wx, N12 wy => let (w,r) := w11_mul_add_n1 1 wy wx W0 in if w11_eq0 w then N12 r else Nn 0 (WW (extend1 w10 w) r) | N11 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy (extend1 w10 wx) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | N12 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 12 wx wy w_0 in if w0_eq0 w then N12 r else Nn 0 (WW (extend11 w0 (WW w_0 w)) r) | N12 wx, N1 wy => let (w,r) := w1_mul_add_n1 11 wx wy W0 in if w1_eq0 w then N12 r else Nn 0 (WW (extend11 w0 w) r) | N12 wx, N2 wy => let (w,r) := w2_mul_add_n1 10 wx wy W0 in if w2_eq0 w then N12 r else Nn 0 (WW (extend10 w1 w) r) | N12 wx, N3 wy => let (w,r) := w3_mul_add_n1 9 wx wy W0 in if w3_eq0 w then N12 r else Nn 0 (WW (extend9 w2 w) r) | N12 wx, N4 wy => let (w,r) := w4_mul_add_n1 8 wx wy W0 in if w4_eq0 w then N12 r else Nn 0 (WW (extend8 w3 w) r) | N12 wx, N5 wy => let (w,r) := w5_mul_add_n1 7 wx wy W0 in if w5_eq0 w then N12 r else Nn 0 (WW (extend7 w4 w) r) | N12 wx, N6 wy => let (w,r) := w6_mul_add_n1 6 wx wy W0 in if w6_eq0 w then N12 r else Nn 0 (WW (extend6 w5 w) r) | N12 wx, N7 wy => let (w,r) := w7_mul_add_n1 5 wx wy W0 in if w7_eq0 w then N12 r else Nn 0 (WW (extend5 w6 w) r) | N12 wx, N8 wy => let (w,r) := w8_mul_add_n1 4 wx wy W0 in if w8_eq0 w then N12 r else Nn 0 (WW (extend4 w7 w) r) | N12 wx, N9 wy => let (w,r) := w9_mul_add_n1 3 wx wy W0 in if w9_eq0 w then N12 r else Nn 0 (WW (extend3 w8 w) r) | N12 wx, N10 wy => let (w,r) := w10_mul_add_n1 2 wx wy W0 in if w10_eq0 w then N12 r else Nn 0 (WW (extend2 w9 w) r) | N12 wx, N11 wy => let (w,r) := w11_mul_add_n1 1 wx wy W0 in if w11_eq0 w then N12 r else Nn 0 (WW (extend1 w10 w) r) | N12 wx, N12 wy => Nn 0 (w12_mul_c wx wy) | N12 wx, Nn n wy => let (w,r) := w12_mul_add_n1 (S n) wy wx W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := gen_mul_add_mn1 w_0 (fun r => extend11 w0 (WW w_0 r)) w12_op.(znz_0W) w12_op.(znz_WW) (w0_mul_add_n1 12) (S n) wx wy w_0 in if w0_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (extend12 w0 (WW w_0 w))) r) | Nn n wx, N1 wy => let (w,r) := gen_mul_add_mn1 W0 (fun r => extend11 w0 r) w12_op.(znz_0W) w12_op.(znz_WW) (w1_mul_add_n1 11) (S n) wx wy W0 in if w1_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (extend12 w0 w)) r) | Nn n wx, N2 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend10 w1 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N3 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend9 w2 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N4 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend8 w3 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N5 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend7 w4 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N6 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend6 w5 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N7 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend5 w6 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N8 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend4 w7 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N9 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend3 w8 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N10 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend2 w9 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N11 wy => let (w,r) := w12_mul_add_n1 (S n) wx (extend1 w10 wy) W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, N12 wy => let (w,r) := w12_mul_add_n1 (S n) wx wy W0 in if w12_eq0 w then Nn n r else Nn (S n) (WW (extend n w12 (WW W0 w)) r) | Nn n wx, Nn m wy => match extend_to_max w12 n m wx wy with | inl wx' => let op := make_op m in reduce_n (S m) (op.(znz_mul_c) wx' wy) | inr wy' => let op := make_op n in reduce_n (S n) (op.(znz_mul_c) wx wy') end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1