bf_basic: Traditional notion of when rippling is blocked, attempts to conjecture lemmas/apply fertilisation when no more rippling is possible. bf_basic_delay: As above, but using delays in the search if a lemma is conjectured for which an attempt is already in progress. bf_eager: Eagerly try to apply weak fertilisation/critic when no more skeleton preserving steps are available. bf_eager_delay: As above with delayed search. dsum: Ordinary, depth-first rippling. techn | prob | term | solved | time | timeout -------------------+----------------------------------+-------------------------------------------------------------------+--------+--------+--------- bf_basic | BF_L_destr_app | l ~= [] --> l @ m = head l # tail l @ m | 1 | 0.261 | 0 bf_basic | BF_L_destr_downto | n ~= 0 --> down_to n = n # down_to (pre n) | 1 | 0.051 | 0 bf_basic | BF_L_destr_len | l ~= [] --> len l = suc len tail l | 1 | 0.047 | 0 bf_basic | BF_L_destr_map | l ~= [] --> map f l = f (head l) # map f tail l | 1 | 0.143 | 0 bf_basic | BF_L_destr_mem | l ~= [] --> x mem l = (if x = head l then True else x mem tail l) | 1 | 0.168 | 0 bf_basic | BF_L_destr_pairify | l ~= [] --> pairify l = head l # head l # pairify (tail l) | 1 | 0.148 | 0 bf_basic | BF_L_destr_qrev | l ~= [] --> qrev l [] = qrev tail l [] @ [head l] | 0 | 0.465 | 0 bf_basic | BF_L_destr_rev | l ~= [] --> rev l = rev tail l @ [head l] | 1 | 0.118 | 0 bf_basic | BF_L_destr_upto | n ~= 0 --> up_to n = up_to (pre n) @ [n] | 1 | 0.057 | 0 bf_basic | BF_L_double_len_app | double (len x @ y) = double (len y @ x) | 1 | 4.781 | 0 bf_basic | BF_L_evenM_pairify | evenM (len pairify l) | 1 | 0.028 | 0 bf_basic | BF_L_Gen_destr_len | pre (len l) = len tail l | 1 | 0.021 | 0 bf_basic | BF_L_len_app | len x @ y = len y @ x | 1 | 0.585 | 0 bf_basic | BF_L_len_rev_upto_downto | len up_to (n + m) = len rev down_to (n + m) | 1 | 0.157 | 0 bf_basic | BF_L_rev_upto_downto | down_to (n + m) = rev up_to (n + m) | 1 | 0.354 | 0 bf_basic | BF_L_zip_pairify | zip l l = pairify l | 1 | 0.054 | 0 bf_basic | 2ST_Mut_add_evens | (evenM n = evenM m) = evenM (n + m) | 1 | 0.487 | 0 bf_basic | 2ST_Mut_even_not_odd | evenM n = (~ oddM n) | 1 | 0.032 | 0 bf_basic | 2ST_Mut_even_not_suc | evenM n = (~ evenM (suc n)) | 1 | 0.066 | 0 bf_basic | 2ST_Mut_even_or_odd | evenM n | oddM n | 1 | 0.029 | 0 bf_basic | 2ST_Mut_even_or_suc | evenM n | evenM (suc n) | 1 | 0.063 | 0 bf_basic | 2ST_Mut_plus2_l | evenM n = evenM (suc suc 0 + n) | 1 | 0.094 | 0 bf_basic | 2ST_Mut_plus2_r | evenM n = evenM (n + suc suc 0) | 1 | 0.08 | 0 bf_basic | 3ST_Mod3_disj | ZMT n | OMT n | TMT n | 1 | 0.124 | 0 bf_basic | 3ST_Zero_Mod3 | ZMT n | ZMT (suc n) | ZMT (suc suc n) | 1 | 0.895 | 0 bf_basic | 3ST_Zero_Mod3_times3_l | ZMT n = ZMT (n + suc suc suc 0) | 1 | 0.145 | 0 bf_basic | 3ST_Zero_Mod3_times3_r | ZMT n = ZMT (suc suc suc 0 + n) | 1 | 0.147 | 0 bf_basic | BF_PN_binom_minus | binom (x, suc 0) - x = 0 | 1 | 0.115 | 0 bf_basic | BF_PN_destr_Add | x ~= 0 --> x + y = suc (pre x + y) | 1 | 0.156 | 0 bf_basic | BF_PN_destr_double | n ~= 0 --> double n = suc suc double (pre n) | 1 | 0.06 | 0 bf_basic | BF_PN_destr_Mult | x ~= 0 --> x * y = pre x * y + y | 1 | 0.251 | 0 bf_basic | BF_PN_destr_sum | sum n = sum (pre n) + n | 1 | 0.031 | 0 bf_basic | BF_PN_evenM_times2_l | evenM (n * suc suc 0) | 1 | 0.049 | 0 bf_basic | BF_PN_evenM_times2_r | evenM (suc suc 0 * n) | 0 | 30 | 1 bf_basic | BF_PN_evenR_times2_l | evenR (n * suc suc 0) | 1 | 0.035 | 0 bf_basic | BF_PN_evenR_times2_r | evenR (suc suc 0 * n) | 0 | 0.89 | 0 bf_basic | BF_PN_Manning7 | x + suc suc z * y = x + y * suc suc z | 1 | 1.548 | 0 bf_basic | BF_PN_ZeroMod_times3_l | ZMT (n * suc suc suc 0) | 1 | 0.076 | 0 bf_basic | BF_PN_ZeroMod_times3_r | ZMT (suc suc suc 0 * n) | 0 | 30 | 1 bf_basic | add_0_left | 0 + a = a | 1 | 0.009 | 0 bf_basic | add_0_right | a + 0 = a | 1 | 0.013 | 0 bf_basic | add_assoc | b + c + a = b + (c + a) | 1 | 0.075 | 0 bf_basic | add_commute | a + b = b + a | 1 | 0.142 | 0 bf_basic | add_left_cancel | (k + m = k + n) = (m = n) | 1 | 0.044 | 0 bf_basic | add_left_commute | a + (b + c) = b + (a + c) | 1 | 0.217 | 0 bf_basic | add_mult_distrib2 | k * (m + n) = k * m + k * n | 1 | 10.008 | 0 bf_basic | add_mult_distrib | (m + n) * k = m * k + n * k | 1 | 1.17 | 0 bf_basic | add_right_cancel | (m + k = n + k) = (m = n) | 0 | 0.181 | 0 bf_basic | add_right_commute | a + b + c = a + c + b | 1 | 0.254 | 0 bf_basic | add_suc_right | a + suc b = suc (a + b) | 1 | 0.034 | 0 bf_basic | mult_0_left | 0 * m = 0 | 1 | 0.009 | 0 bf_basic | mult_0_right | m * 0 = 0 | 1 | 0.012 | 0 bf_basic | mult_1_left | suc 0 * n = n | 1 | 0.036 | 0 bf_basic | mult_1_right | n * suc 0 = n | 1 | 0.021 | 0 bf_basic | mult_assoc | m * n * k = m * (n * k) | 1 | 1.45 | 0 bf_basic | mult_commute | m * n = n * m | 1 | 0.429 | 0 bf_basic | mult_left_commute | x * (y * z) = y * (x * z) | 1 | 11.753 | 0 bf_basic | mult_right_commute | x * y * z = x * z * y | 0 | 2.52 | 0 bf_basic | mult_suc_left | suc m * b = b + m * b | 1 | 0.05 | 0 bf_basic | mult_suc_right | m * suc b = m + m * b | 1 | 0.346 | 0 bf_basic | NT_add_0_left | 0 + a = 0 | 0 | 0.007 | 0 bf_basic | NT_add_0_right | a + 0 = 0 | 0 | 0.015 | 0 bf_basic | NT_add_assoc1 | b + c + a = b + (c + c) | 0 | 0.044 | 0 bf_basic | NT_add_assoc2 | b + c + a = b + (c + b) | 0 | 0.047 | 0 bf_basic | NT_add_assoc3 | b + c + a = c + (c + a) | 0 | 0.068 | 0 bf_basic | NT_add_commute | a + b = a + a | 0 | 0.019 | 0 bf_basic | NT_add_left_cancel | (k + m = k + n) = (k = n) | 0 | 0.028 | 0 bf_basic | NT_add_mult_distrib1 | (m + n) * k = m * k * (n * k) | 0 | 0.6 | 0 bf_basic | NT_add_mult_distrib2_1 | k * (m + n) = k * m * (k * n) | 0 | 4.932 | 0 bf_basic | NT_add_mult_distrib2_2 | k * (m + n) = k + m + k * n | 0 | 0.062 | 0 bf_basic | NT_add_mult_distrib2_3 | k * (m + n) = k * m + (k + n) | 0 | 0.05 | 0 bf_basic | NT_add_mult_distrib2_4 | k * (m + n) = k * n + k * n | 0 | 1.046 | 0 bf_basic | NT_add_mult_distrib2_5 | k * (m + n) = (k + m) * (k + n) | 0 | 0.664 | 0 bf_basic | NT_add_mult_distrib2 | (m + n) * k = m + k + n * k | 0 | 0.067 | 0 bf_basic | NT_add_mult_distrib3 | (m + n) * k = m * k + (n + k) | 0 | 0.06 | 0 bf_basic | NT_add_mult_distrib4 | (m + n) * k = m * n + n * k | 0 | 2.799 | 0 bf_basic | NT_add_mult_distrib5 | (m + n) * k = (m + k) * (n + k) | 0 | 0.279 | 0 bf_basic | NT_add_right_cancel | (m + k = n + k) = (k = n) | 0 | 0.067 | 0 bf_basic | NT_add_suc_suc_right | a + suc b = suc (suc a + b) | 0 | 0.02 | 0 bf_basic | NT_mult_0_left | 0 * m = m | 0 | 0.008 | 0 bf_basic | NT_mult_0_right | m * 0 = m | 0 | 0.016 | 0 bf_basic | NT_mult_1_left1 | suc 0 * n = suc 0 | 0 | 0.005 | 0 bf_basic | NT_mult_1_left2 | suc 0 * n = 0 | 0 | 0.018 | 0 bf_basic | NT_mult_1_left3 | suc 0 * n = n + n | 0 | 0.06 | 0 bf_basic | NT_mult_1_right1 | n * suc 0 = suc 0 | 0 | 0.005 | 0 bf_basic | NT_mult_1_right2 | n * suc 0 = 0 | 0 | 0.021 | 0 bf_basic | NT_mult_1_right3 | n * suc 0 = n + n | 0 | 0.054 | 0 bf_basic | NT_mult_assoc2 | m * n * k = m + (n + k) | 0 | 0.054 | 0 bf_basic | NT_mult_assoc3 | m * n * k = m * (m * k) | 0 | 0.919 | 0 bf_basic | NT_mult_assoc4 | m * n * k = m + n * k | 0 | 0.113 | 0 bf_basic | NT_mult_commute1 | m * n = m * m | 0 | 0.109 | 0 bf_basic | NT_mult_commute2 | m * n = n + m | 0 | 0.038 | 0 bf_basic | NT_mult_left_commute1 | x * (y * z) = y * (y * z) | 0 | 3.64 | 0 bf_basic | NT_mult_left_commute2 | x * (y * z) = z * (x * z) | 0 | 4.851 | 0 bf_basic | NT_mult_right_commute1 | x * y * z = x * y * y | 0 | 0.086 | 0 bf_basic | NT_mult_right_commute2 | x * y * z = y * z * y | 0 | 5.477 | 0 bf_basic | NT_mult_suc_right1 | m * suc b = b + m * b | 0 | 0.027 | 0 bf_basic | NT_mult_suc_right2 | m * suc b = m * (m + b) | 0 | 0.837 | 0 bf_basic | NT_mult_suc_right3 | m * suc b = b * (m + b) | 0 | 0.05 | 0 bf_basic | NT_power_1_1 | x ^ suc 0 = 0 | 0 | 0.038 | 0 bf_basic | NT_power_1_2 | x ^ suc 0 = suc 0 | 0 | 0.005 | 0 bf_basic | NT_power_1_3 | x ^ 0 = x | 0 | 0.004 | 0 bf_basic | NT_power_add1 | i ^ (j + k) = i ^ j + i ^ k | 0 | 0.036 | 0 bf_basic | NT_power_add2 | i ^ (j + k) = i ^ j ^ k | 0 | 0.057 | 0 bf_basic | NT_power_add3 | i ^ (j + k) = i ^ j * j ^ k | 0 | 3.273 | 0 bf_basic | NT_power_add4 | i ^ (j + k) = j ^ k * i ^ k | 0 | 0.127 | 0 bf_basic | NT_power_add5 | i ^ (j + k) = (i ^ j) ^ k | 0 | 0.067 | 0 bf_basic | NT_power_mult1 | i ^ (j * k) = (i * j) ^ k | 0 | 0.167 | 0 bf_basic | NT_power_mult2 | i ^ (j * k) = i ^ j * k | 0 | 0.023 | 0 bf_basic | NT_power_mult3 | i ^ (j * k) = (i + j) ^ k | 0 | 0.212 | 0 bf_basic | NT_power_mult4 | i ^ (j * k) = (i + j) * k | 0 | 0.033 | 0 bf_basic | NT_power_squared1 | x ^ suc 0 = x * x | 0 | 2.776 | 0 bf_basic | NT_power_squared2 | x ^ suc suc 0 = x + x | 0 | 4.343 | 0 bf_basic | NT_power_squared3 | x ^ suc suc 0 = x * suc x | 0 | 30 | 1 bf_basic | power_1 | x ^ suc 0 = x | 1 | 0.051 | 0 bf_basic | power_add | i ^ (j + k) = i ^ j * i ^ k | 1 | 2.996 | 0 bf_basic | power_mult | i ^ (j * k) = (i ^ j) ^ k | 0 | 30 | 1 bf_basic | power_squared | x ^ suc suc 0 = x * x | 0 | 9.74 | 0 bf_basic | SP_add_0_0_left | 0 + 0 + a = a | 1 | 0.012 | 0 bf_basic | SP_add_0_a_right | a + 0 + a = a + a | 1 | 0.057 | 0 bf_basic | SP_add_a_a_commute | a + a + b = b + (a + a) | 1 | 0.101 | 0 bf_basic | SP_add_assoc | d + b + c + a = b + (c + (a + d)) | 1 | 7.464 | 0 bf_basic | SP_add_left_cancel | (suc 0 + m = suc 0 + n) = (m = n) | 1 | 0.053 | 0 bf_basic | SP_add_right_cancel | (m + suc 0 = n + suc 0) = (m = n) | 0 | 0.182 | 0 bf_basic | SP_add_suc_suc_right | suc a + suc b = suc suc (a + b) | 1 | 0.102 | 0 bf_basic | SP_mult_0_left_m_k | 0 * m * k = 0 | 1 | 0.02 | 0 bf_basic | SP_mult_0_left_n_plus_m | 0 * (n + m) = 0 | 1 | 0.023 | 0 bf_basic | SP_mult_0_right_n_plus_m | (n + m) * 0 = 0 | 1 | 0.038 | 0 bf_basic | SP_mult_suc_right_and_distr_mult | m * suc b * k = m * k + m * b * k | 0 | 30 | 1 bf_basic | SP_power_add_add | i ^ (j + k + l) = i ^ j * i ^ k * i ^ l | 0 | 30 | 1 bf_basic | L_append_assoc | x @ y @ z = x @ (y @ z) | 1 | 0.097 | 0 bf_basic | L_append_nil2 | l = l @ [] | 1 | 0.018 | 0 bf_basic | L_len_append | len x @ y = len x + len y | 1 | 0.282 | 0 bf_basic | L_len_map | len map f x = len x | 1 | 0.035 | 0 bf_basic | L_len_qrev | len qrev x [] = len x | 0 | 0.224 | 0 bf_basic | L_len_rev | len rev x = len x | 1 | 0.08 | 0 bf_basic | L_map_append | map f x @ y = map f x @ map f y | 1 | 0.238 | 0 bf_basic | L_qrev_map | qrev (map f x) [] = map f qrev x [] | 0 | 2.7 | 0 bf_basic | L_qrev_qrev_gen | qrev qrev xs ys zs = xs @ qrev ys zs | 0 | 7.228 | 0 bf_basic | L_qrev_qrev | qrev qrev x [] [] = x | 0 | 0.157 | 0 bf_basic | L_rev_append_distr | rev (a @ b) = rev b @ rev a | 1 | 0.315 | 0 bf_basic | L_rev_map | rev (map f x) = map f rev x | 1 | 0.318 | 0 bf_basic | L_rev_qrev_gen | qrev x y = rev x @ y | 1 | 0.447 | 0 bf_basic | L_rev_qrev | rev x = qrev x [] | 1 | 0.868 | 0 bf_basic | L_rev_rev_append | rev (rev t @ l) = rev l @ t | 0 | 30 | 1 bf_basic | L_rev_rev | rev rev x = x | 1 | 0.1 | 0 bf_basic | L_rot_append | rot (len l, l @ k) = k @ l | 0 | 30 | 1 bf_basic | L_rot_len | rot (len l, l) = l | 0 | 0.291 | 0 bf_basic_delay | BF_L_destr_app | l ~= [] --> l @ m = head l # tail l @ m | 1 | 0.261 | 0 bf_basic_delay | BF_L_destr_downto | n ~= 0 --> down_to n = n # down_to (pre n) | 1 | 0.041 | 0 bf_basic_delay | BF_L_destr_len | l ~= [] --> len l = suc len tail l | 1 | 0.041 | 0 bf_basic_delay | BF_L_destr_map | l ~= [] --> map f l = f (head l) # map f tail l | 1 | 0.145 | 0 bf_basic_delay | BF_L_destr_mem | l ~= [] --> x mem l = (if x = head l then True else x mem tail l) | 1 | 0.172 | 0 bf_basic_delay | BF_L_destr_pairify | l ~= [] --> pairify l = head l # head l # pairify (tail l) | 1 | 0.151 | 0 bf_basic_delay | BF_L_destr_qrev | l ~= [] --> qrev l [] = qrev tail l [] @ [head l] | 0 | 0.48 | 0 bf_basic_delay | BF_L_destr_rev | l ~= [] --> rev l = rev tail l @ [head l] | 1 | 0.107 | 0 bf_basic_delay | BF_L_destr_upto | n ~= 0 --> up_to n = up_to (pre n) @ [n] | 1 | 0.047 | 0 bf_basic_delay | BF_L_double_len_app | double (len x @ y) = double (len y @ x) | 1 | 1.394 | 0 bf_basic_delay | BF_L_evenM_pairify | evenM (len pairify l) | 1 | 0.027 | 0 bf_basic_delay | BF_L_Gen_destr_len | pre (len l) = len tail l | 1 | 0.02 | 0 bf_basic_delay | BF_L_len_app | len x @ y = len y @ x | 1 | 0.391 | 0 bf_basic_delay | BF_L_len_rev_upto_downto | len up_to (n + m) = len rev down_to (n + m) | 1 | 0.159 | 0 bf_basic_delay | BF_L_rev_upto_downto | down_to (n + m) = rev up_to (n + m) | 1 | 0.335 | 0 bf_basic_delay | BF_L_zip_pairify | zip l l = pairify l | 1 | 0.042 | 0 bf_basic_delay | 2ST_Mut_add_evens | (evenM n = evenM m) = evenM (n + m) | 1 | 0.493 | 0 bf_basic_delay | 2ST_Mut_even_not_odd | evenM n = (~ oddM n) | 1 | 0.033 | 0 bf_basic_delay | 2ST_Mut_even_not_suc | evenM n = (~ evenM (suc n)) | 1 | 0.058 | 0 bf_basic_delay | 2ST_Mut_even_or_odd | evenM n | oddM n | 1 | 0.03 | 0 bf_basic_delay | 2ST_Mut_even_or_suc | evenM n | evenM (suc n) | 1 | 0.054 | 0 bf_basic_delay | 2ST_Mut_plus2_l | evenM n = evenM (suc suc 0 + n) | 1 | 0.088 | 0 bf_basic_delay | 2ST_Mut_plus2_r | evenM n = evenM (n + suc suc 0) | 1 | 0.073 | 0 bf_basic_delay | 3ST_Mod3_disj | ZMT n | OMT n | TMT n | 1 | 0.124 | 0 bf_basic_delay | 3ST_Zero_Mod3 | ZMT n | ZMT (suc n) | ZMT (suc suc n) | 1 | 0.85 | 0 bf_basic_delay | 3ST_Zero_Mod3_times3_l | ZMT n = ZMT (n + suc suc suc 0) | 1 | 0.137 | 0 bf_basic_delay | 3ST_Zero_Mod3_times3_r | ZMT n = ZMT (suc suc suc 0 + n) | 1 | 0.141 | 0 bf_basic_delay | BF_PN_binom_minus | binom (x, suc 0) - x = 0 | 1 | 0.108 | 0 bf_basic_delay | BF_PN_destr_Add | x ~= 0 --> x + y = suc (pre x + y) | 1 | 0.162 | 0 bf_basic_delay | BF_PN_destr_double | n ~= 0 --> double n = suc suc double (pre n) | 1 | 0.057 | 0 bf_basic_delay | BF_PN_destr_Mult | x ~= 0 --> x * y = pre x * y + y | 1 | 0.207 | 0 bf_basic_delay | BF_PN_destr_sum | sum n = sum (pre n) + n | 1 | 0.025 | 0 bf_basic_delay | BF_PN_evenM_times2_l | evenM (n * suc suc 0) | 1 | 0.042 | 0 bf_basic_delay | BF_PN_evenM_times2_r | evenM (suc suc 0 * n) | 0 | 1.493 | 0 bf_basic_delay | BF_PN_evenR_times2_l | evenR (n * suc suc 0) | 1 | 0.03 | 0 bf_basic_delay | BF_PN_evenR_times2_r | evenR (suc suc 0 * n) | 0 | 0.234 | 0 bf_basic_delay | BF_PN_Manning7 | x + suc suc z * y = x + y * suc suc z | 1 | 0.709 | 0 bf_basic_delay | BF_PN_ZeroMod_times3_l | ZMT (n * suc suc suc 0) | 1 | 0.071 | 0 bf_basic_delay | BF_PN_ZeroMod_times3_r | ZMT (suc suc suc 0 * n) | 0 | 30 | 1 bf_basic_delay | add_0_left | 0 + a = a | 1 | 0.009 | 0 bf_basic_delay | add_0_right | a + 0 = a | 1 | 0.013 | 0 bf_basic_delay | add_assoc | b + c + a = b + (c + a) | 1 | 0.076 | 0 bf_basic_delay | add_commute | a + b = b + a | 1 | 0.076 | 0 bf_basic_delay | add_left_cancel | (k + m = k + n) = (m = n) | 1 | 0.043 | 0 bf_basic_delay | add_left_commute | a + (b + c) = b + (a + c) | 1 | 0.118 | 0 bf_basic_delay | add_mult_distrib2 | k * (m + n) = k * m + k * n | 1 | 4.12 | 0 bf_basic_delay | add_mult_distrib | (m + n) * k = m * k + n * k | 1 | 0.738 | 0 bf_basic_delay | add_right_cancel | (m + k = n + k) = (m = n) | 0 | 0.129 | 0 bf_basic_delay | add_right_commute | a + b + c = a + c + b | 1 | 0.192 | 0 bf_basic_delay | add_suc_right | a + suc b = suc (a + b) | 1 | 0.033 | 0 bf_basic_delay | mult_0_left | 0 * m = 0 | 1 | 0.008 | 0 bf_basic_delay | mult_0_right | m * 0 = 0 | 1 | 0.011 | 0 bf_basic_delay | mult_1_left | suc 0 * n = n | 1 | 0.035 | 0 bf_basic_delay | mult_1_right | n * suc 0 = n | 1 | 0.022 | 0 bf_basic_delay | mult_assoc | m * n * k = m * (n * k) | 1 | 0.922 | 0 bf_basic_delay | mult_commute | m * n = n * m | 1 | 0.285 | 0 bf_basic_delay | mult_left_commute | x * (y * z) = y * (x * z) | 1 | 4.433 | 0 bf_basic_delay | mult_right_commute | x * y * z = x * z * y | 0 | 0.323 | 0 bf_basic_delay | mult_suc_left | suc m * b = b + m * b | 1 | 0.05 | 0 bf_basic_delay | mult_suc_right | m * suc b = m + m * b | 1 | 0.243 | 0 bf_basic_delay | NT_add_0_left | 0 + a = 0 | 0 | 0.009 | 0 bf_basic_delay | NT_add_0_right | a + 0 = 0 | 0 | 0.016 | 0 bf_basic_delay | NT_add_assoc1 | b + c + a = b + (c + c) | 0 | 0.043 | 0 bf_basic_delay | NT_add_assoc2 | b + c + a = b + (c + b) | 0 | 0.039 | 0 bf_basic_delay | NT_add_assoc3 | b + c + a = c + (c + a) | 0 | 0.068 | 0 bf_basic_delay | NT_add_commute | a + b = a + a | 0 | 0.02 | 0 bf_basic_delay | NT_add_left_cancel | (k + m = k + n) = (k = n) | 0 | 0.029 | 0 bf_basic_delay | NT_add_mult_distrib1 | (m + n) * k = m * k * (n * k) | 0 | 0.274 | 0 bf_basic_delay | NT_add_mult_distrib2_1 | k * (m + n) = k * m * (k * n) | 0 | 1.117 | 0 bf_basic_delay | NT_add_mult_distrib2_2 | k * (m + n) = k + m + k * n | 0 | 0.061 | 0 bf_basic_delay | NT_add_mult_distrib2_3 | k * (m + n) = k * m + (k + n) | 0 | 0.041 | 0 bf_basic_delay | NT_add_mult_distrib2_4 | k * (m + n) = k * n + k * n | 0 | 0.584 | 0 bf_basic_delay | NT_add_mult_distrib2_5 | k * (m + n) = (k + m) * (k + n) | 0 | 0.664 | 0 bf_basic_delay | NT_add_mult_distrib2 | (m + n) * k = m + k + n * k | 0 | 0.066 | 0 bf_basic_delay | NT_add_mult_distrib3 | (m + n) * k = m * k + (n + k) | 0 | 0.051 | 0 bf_basic_delay | NT_add_mult_distrib4 | (m + n) * k = m * n + n * k | 0 | 0.708 | 0 bf_basic_delay | NT_add_mult_distrib5 | (m + n) * k = (m + k) * (n + k) | 0 | 0.225 | 0 bf_basic_delay | NT_add_right_cancel | (m + k = n + k) = (k = n) | 0 | 0.059 | 0 bf_basic_delay | NT_add_suc_suc_right | a + suc b = suc (suc a + b) | 0 | 0.02 | 0 bf_basic_delay | NT_mult_0_left | 0 * m = m | 0 | 0.008 | 0 bf_basic_delay | NT_mult_0_right | m * 0 = m | 0 | 0.016 | 0 bf_basic_delay | NT_mult_1_left1 | suc 0 * n = suc 0 | 0 | 0.005 | 0 bf_basic_delay | NT_mult_1_left2 | suc 0 * n = 0 | 0 | 0.018 | 0 bf_basic_delay | NT_mult_1_left3 | suc 0 * n = n + n | 0 | 0.061 | 0 bf_basic_delay | NT_mult_1_right1 | n * suc 0 = suc 0 | 0 | 0.005 | 0 bf_basic_delay | NT_mult_1_right2 | n * suc 0 = 0 | 0 | 0.02 | 0 bf_basic_delay | NT_mult_1_right3 | n * suc 0 = n + n | 0 | 0.054 | 0 bf_basic_delay | NT_mult_assoc2 | m * n * k = m + (n + k) | 0 | 0.048 | 0 bf_basic_delay | NT_mult_assoc3 | m * n * k = m * (m * k) | 0 | 0.897 | 0 bf_basic_delay | NT_mult_assoc4 | m * n * k = m + n * k | 0 | 0.099 | 0 bf_basic_delay | NT_mult_commute1 | m * n = m * m | 0 | 0.11 | 0 bf_basic_delay | NT_mult_commute2 | m * n = n + m | 0 | 0.037 | 0 bf_basic_delay | NT_mult_left_commute1 | x * (y * z) = y * (y * z) | 0 | 1.007 | 0 bf_basic_delay | NT_mult_left_commute2 | x * (y * z) = z * (x * z) | 0 | 1.319 | 0 bf_basic_delay | NT_mult_right_commute1 | x * y * z = x * y * y | 0 | 0.085 | 0 bf_basic_delay | NT_mult_right_commute2 | x * y * z = y * z * y | 0 | 0.654 | 0 bf_basic_delay | NT_mult_suc_right1 | m * suc b = b + m * b | 0 | 0.027 | 0 bf_basic_delay | NT_mult_suc_right2 | m * suc b = m * (m + b) | 0 | 0.842 | 0 bf_basic_delay | NT_mult_suc_right3 | m * suc b = b * (m + b) | 0 | 0.051 | 0 bf_basic_delay | NT_power_1_1 | x ^ suc 0 = 0 | 0 | 0.038 | 0 bf_basic_delay | NT_power_1_2 | x ^ suc 0 = suc 0 | 0 | 0.005 | 0 bf_basic_delay | NT_power_1_3 | x ^ 0 = x | 0 | 0.005 | 0 bf_basic_delay | NT_power_add1 | i ^ (j + k) = i ^ j + i ^ k | 0 | 0.036 | 0 bf_basic_delay | NT_power_add2 | i ^ (j + k) = i ^ j ^ k | 0 | 0.058 | 0 bf_basic_delay | NT_power_add3 | i ^ (j + k) = i ^ j * j ^ k | 0 | 1.421 | 0 bf_basic_delay | NT_power_add4 | i ^ (j + k) = j ^ k * i ^ k | 0 | 0.136 | 0 bf_basic_delay | NT_power_add5 | i ^ (j + k) = (i ^ j) ^ k | 0 | 0.066 | 0 bf_basic_delay | NT_power_mult1 | i ^ (j * k) = (i * j) ^ k | 0 | 0.174 | 0 bf_basic_delay | NT_power_mult2 | i ^ (j * k) = i ^ j * k | 0 | 0.025 | 0 bf_basic_delay | NT_power_mult3 | i ^ (j * k) = (i + j) ^ k | 0 | 0.216 | 0 bf_basic_delay | NT_power_mult4 | i ^ (j * k) = (i + j) * k | 0 | 0.033 | 0 bf_basic_delay | NT_power_squared1 | x ^ suc 0 = x * x | 0 | 2.779 | 0 bf_basic_delay | NT_power_squared2 | x ^ suc suc 0 = x + x | 0 | 4.376 | 0 bf_basic_delay | NT_power_squared3 | x ^ suc suc 0 = x * suc x | 0 | 30 | 1 bf_basic_delay | power_1 | x ^ suc 0 = x | 1 | 0.052 | 0 bf_basic_delay | power_add | i ^ (j + k) = i ^ j * i ^ k | 1 | 1.177 | 0 bf_basic_delay | power_mult | i ^ (j * k) = (i ^ j) ^ k | 0 | 12.745 | 0 bf_basic_delay | power_squared | x ^ suc suc 0 = x * x | 0 | 9.747 | 0 bf_basic_delay | SP_add_0_0_left | 0 + 0 + a = a | 1 | 0.012 | 0 bf_basic_delay | SP_add_0_a_right | a + 0 + a = a + a | 1 | 0.057 | 0 bf_basic_delay | SP_add_a_a_commute | a + a + b = b + (a + a) | 1 | 0.198 | 0 bf_basic_delay | SP_add_assoc | d + b + c + a = b + (c + (a + d)) | 1 | 3.226 | 0 bf_basic_delay | SP_add_left_cancel | (suc 0 + m = suc 0 + n) = (m = n) | 1 | 0.052 | 0 bf_basic_delay | SP_add_right_cancel | (m + suc 0 = n + suc 0) = (m = n) | 0 | 0.122 | 0 bf_basic_delay | SP_add_suc_suc_right | suc a + suc b = suc suc (a + b) | 1 | 0.101 | 0 bf_basic_delay | SP_mult_0_left_m_k | 0 * m * k = 0 | 1 | 0.02 | 0 bf_basic_delay | SP_mult_0_left_n_plus_m | 0 * (n + m) = 0 | 1 | 0.023 | 0 bf_basic_delay | SP_mult_0_right_n_plus_m | (n + m) * 0 = 0 | 1 | 0.038 | 0 bf_basic_delay | SP_mult_suc_right_and_distr_mult | m * suc b * k = m * k + m * b * k | 0 | 9.557 | 0 bf_basic_delay | SP_power_add_add | i ^ (j + k + l) = i ^ j * i ^ k * i ^ l | 0 | 8.805 | 0 bf_basic_delay | L_append_assoc | x @ y @ z = x @ (y @ z) | 1 | 0.104 | 0 bf_basic_delay | L_append_nil2 | l = l @ [] | 1 | 0.019 | 0 bf_basic_delay | L_len_append | len x @ y = len x + len y | 1 | 0.293 | 0 bf_basic_delay | L_len_map | len map f x = len x | 1 | 0.035 | 0 bf_basic_delay | L_len_qrev | len qrev x [] = len x | 0 | 0.233 | 0 bf_basic_delay | L_len_rev | len rev x = len x | 1 | 0.081 | 0 bf_basic_delay | L_map_append | map f x @ y = map f x @ map f y | 1 | 0.248 | 0 bf_basic_delay | L_qrev_map | qrev (map f x) [] = map f qrev x [] | 0 | 0.589 | 0 bf_basic_delay | L_qrev_qrev_gen | qrev qrev xs ys zs = xs @ qrev ys zs | 0 | 1.233 | 0 bf_basic_delay | L_qrev_qrev | qrev qrev x [] [] = x | 0 | 0.162 | 0 bf_basic_delay | L_rev_append_distr | rev (a @ b) = rev b @ rev a | 1 | 0.242 | 0 bf_basic_delay | L_rev_map | rev (map f x) = map f rev x | 1 | 0.253 | 0 bf_basic_delay | L_rev_qrev_gen | qrev x y = rev x @ y | 1 | 0.34 | 0 bf_basic_delay | L_rev_qrev | rev x = qrev x [] | 1 | 0.267 | 0 bf_basic_delay | L_rev_rev_append | rev (rev t @ l) = rev l @ t | 0 | 5.595 | 0 bf_basic_delay | L_rev_rev | rev rev x = x | 1 | 0.104 | 0 bf_basic_delay | L_rot_append | rot (len l, l @ k) = k @ l | 0 | 4.318 | 0 bf_eager | BF_L_destr_app | l ~= [] --> l @ m = head l # tail l @ m | 1 | 0.257 | 0 bf_eager | BF_L_destr_downto | n ~= 0 --> down_to n = n # down_to (pre n) | 1 | 0.05 | 0 bf_eager | BF_L_destr_len | l ~= [] --> len l = suc len tail l | 1 | 0.047 | 0 bf_eager | BF_L_destr_map | l ~= [] --> map f l = f (head l) # map f tail l | 1 | 0.147 | 0 bf_eager | BF_L_destr_mem | l ~= [] --> x mem l = (if x = head l then True else x mem tail l) | 1 | 0.123 | 0 bf_eager | BF_L_destr_pairify | l ~= [] --> pairify l = head l # head l # pairify (tail l) | 1 | 0.147 | 0 bf_eager | BF_L_destr_qrev | l ~= [] --> qrev l [] = qrev tail l [] @ [head l] | 0 | 0.487 | 0 bf_eager | BF_L_destr_rev | l ~= [] --> rev l = rev tail l @ [head l] | 1 | 0.123 | 0 bf_eager | BF_L_destr_upto | n ~= 0 --> up_to n = up_to (pre n) @ [n] | 1 | 0.055 | 0 bf_eager | BF_L_double_len_app | double (len x @ y) = double (len y @ x) | 1 | 4.769 | 0 bf_eager | BF_L_evenM_pairify | evenM (len pairify l) | 1 | 0.029 | 0 bf_eager | BF_L_Gen_destr_len | pre (len l) = len tail l | 1 | 0.02 | 0 bf_eager | BF_L_len_app | len x @ y = len y @ x | 1 | 0.587 | 0 bf_eager | BF_L_len_rev_upto_downto | len up_to (n + m) = len rev down_to (n + m) | 1 | 0.162 | 0 bf_eager | BF_L_rev_upto_downto | down_to (n + m) = rev up_to (n + m) | 1 | 0.348 | 0 bf_eager | BF_L_zip_pairify | zip l l = pairify l | 1 | 0.043 | 0 bf_eager | 2ST_Mut_add_evens | (evenM n = evenM m) = evenM (n + m) | 1 | 0.758 | 0 bf_eager | 2ST_Mut_even_not_odd | evenM n = (~ oddM n) | 1 | 0.068 | 0 bf_eager | 2ST_Mut_even_not_suc | evenM n = (~ evenM (suc n)) | 1 | 0.121 | 0 bf_eager | 2ST_Mut_even_or_odd | evenM n | oddM n | 1 | 0.032 | 0 bf_eager | 2ST_Mut_even_or_suc | evenM n | evenM (suc n) | 1 | 0.109 | 0 bf_eager | 2ST_Mut_plus2_l | evenM n = evenM (suc suc 0 + n) | 1 | 0.026 | 0 bf_eager | 2ST_Mut_plus2_r | evenM n = evenM (n + suc suc 0) | 1 | 0.086 | 0 bf_eager | 3ST_Mod3_disj | ZMT n | OMT n | TMT n | 1 | 0.129 | 0 bf_eager | 3ST_Zero_Mod3 | ZMT n | ZMT (suc n) | ZMT (suc suc n) | 1 | 1.841 | 0 bf_eager | 3ST_Zero_Mod3_times3_l | ZMT n = ZMT (n + suc suc suc 0) | 1 | 0.146 | 0 bf_eager | 3ST_Zero_Mod3_times3_r | ZMT n = ZMT (suc suc suc 0 + n) | 1 | 0.038 | 0 bf_eager | BF_PN_binom_minus | binom (x, suc 0) - x = 0 | 1 | 0.132 | 0 bf_eager | BF_PN_destr_Add | x ~= 0 --> x + y = suc (pre x + y) | 1 | 0.15 | 0 bf_eager | BF_PN_destr_double | n ~= 0 --> double n = suc suc double (pre n) | 1 | 0.067 | 0 bf_eager | BF_PN_destr_Mult | x ~= 0 --> x * y = pre x * y + y | 1 | 0.26 | 0 bf_eager | BF_PN_destr_sum | sum n = sum (pre n) + n | 1 | 0.014 | 0 bf_eager | BF_PN_evenM_times2_l | evenM (n * suc suc 0) | 1 | 0.042 | 0 bf_eager | BF_PN_evenM_times2_r | evenM (suc suc 0 * n) | 0 | 30 | 1 bf_eager | BF_PN_evenR_times2_l | evenR (n * suc suc 0) | 1 | 0.026 | 0 bf_eager | BF_PN_evenR_times2_r | evenR (suc suc 0 * n) | 0 | 1.85 | 0 bf_eager | BF_PN_Manning7 | x + suc suc z * y = x + y * suc suc z | 1 | 1.686 | 0 bf_eager | BF_PN_ZeroMod_times3_l | ZMT (n * suc suc suc 0) | 1 | 0.079 | 0 bf_eager | BF_PN_ZeroMod_times3_r | ZMT (suc suc suc 0 * n) | 0 | 30 | 1 bf_eager | add_0_left | 0 + a = a | 1 | 0.011 | 0 bf_eager | add_0_right | a + 0 = a | 1 | 0.013 | 0 bf_eager | add_assoc | b + c + a = b + (c + a) | 1 | 0.09 | 0 bf_eager | add_commute | a + b = b + a | 1 | 0.156 | 0 bf_eager | add_left_cancel | (k + m = k + n) = (m = n) | 1 | 0.044 | 0 bf_eager | add_left_commute | a + (b + c) = b + (a + c) | 1 | 0.215 | 0 bf_eager | add_mult_distrib2 | k * (m + n) = k * m + k * n | 1 | 9.706 | 0 bf_eager | add_mult_distrib | (m + n) * k = m * k + n * k | 1 | 1.179 | 0 bf_eager | add_right_cancel | (m + k = n + k) = (m = n) | 0 | 0.198 | 0 bf_eager | add_right_commute | a + b + c = a + c + b | 1 | 0.258 | 0 bf_eager | add_suc_right | a + suc b = suc (a + b) | 1 | 0.033 | 0 bf_eager | mult_0_left | 0 * m = 0 | 1 | 0.011 | 0 bf_eager | mult_0_right | m * 0 = 0 | 1 | 0.011 | 0 bf_eager | mult_1_left | suc 0 * n = n | 1 | 0.014 | 0 bf_eager | mult_1_right | n * suc 0 = n | 1 | 0.021 | 0 bf_eager | mult_assoc | m * n * k = m * (n * k) | 1 | 1.452 | 0 bf_eager | mult_commute | m * n = n * m | 1 | 0.44 | 0 bf_eager | mult_left_commute | x * (y * z) = y * (x * z) | 1 | 11.568 | 0 bf_eager | mult_right_commute | x * y * z = x * z * y | 0 | 2.621 | 0 bf_eager | mult_suc_left | suc m * b = b + m * b | 1 | 0.045 | 0 bf_eager | mult_suc_right | m * suc b = m + m * b | 1 | 0.339 | 0 bf_eager | NT_add_0_left | 0 + a = 0 | 0 | 0.013 | 0 bf_eager | NT_add_0_right | a + 0 = 0 | 0 | 0.015 | 0 bf_eager | NT_add_assoc1 | b + c + a = b + (c + c) | 0 | 0.045 | 0 bf_eager | NT_add_assoc2 | b + c + a = b + (c + b) | 0 | 0.047 | 0 bf_eager | NT_add_assoc3 | b + c + a = c + (c + a) | 0 | 0.078 | 0 bf_eager | NT_add_commute | a + b = a + a | 0 | 0.02 | 0 bf_eager | NT_add_left_cancel | (k + m = k + n) = (k = n) | 0 | 0.029 | 0 bf_eager | NT_add_mult_distrib1 | (m + n) * k = m * k * (n * k) | 0 | 0.596 | 0 bf_eager | NT_add_mult_distrib2_1 | k * (m + n) = k * m * (k * n) | 0 | 5.03 | 0 bf_eager | NT_add_mult_distrib2_2 | k * (m + n) = k + m + k * n | 0 | 0.072 | 0 bf_eager | NT_add_mult_distrib2_3 | k * (m + n) = k * m + (k + n) | 0 | 0.059 | 0 bf_eager | NT_add_mult_distrib2_4 | k * (m + n) = k * n + k * n | 0 | 1.047 | 0 bf_eager | NT_add_mult_distrib2_5 | k * (m + n) = (k + m) * (k + n) | 0 | 0.67 | 0 bf_eager | NT_add_mult_distrib2 | (m + n) * k = m + k + n * k | 0 | 0.077 | 0 bf_eager | NT_add_mult_distrib3 | (m + n) * k = m * k + (n + k) | 0 | 0.069 | 0 bf_eager | NT_add_mult_distrib4 | (m + n) * k = m * n + n * k | 0 | 2.834 | 0 bf_eager | NT_add_mult_distrib5 | (m + n) * k = (m + k) * (n + k) | 0 | 0.284 | 0 bf_eager | NT_add_right_cancel | (m + k = n + k) = (k = n) | 0 | 0.077 | 0 bf_eager | NT_add_suc_suc_right | a + suc b = suc (suc a + b) | 0 | 0.02 | 0 bf_eager | NT_mult_0_left | 0 * m = m | 0 | 0.01 | 0 bf_eager | NT_mult_0_right | m * 0 = m | 0 | 0.016 | 0 bf_eager | NT_mult_1_left1 | suc 0 * n = suc 0 | 0 | 0.005 | 0 bf_eager | NT_mult_1_left2 | suc 0 * n = 0 | 0 | 0.027 | 0 bf_eager | NT_mult_1_left3 | suc 0 * n = n + n | 0 | 0.082 | 0 bf_eager | NT_mult_1_right1 | n * suc 0 = suc 0 | 0 | 0.005 | 0 bf_eager | NT_mult_1_right2 | n * suc 0 = 0 | 0 | 0.021 | 0 bf_eager | NT_mult_1_right3 | n * suc 0 = n + n | 0 | 0.064 | 0 bf_eager | NT_mult_assoc2 | m * n * k = m + (n + k) | 0 | 0.063 | 0 bf_eager | NT_mult_assoc3 | m * n * k = m * (m * k) | 0 | 0.925 | 0 bf_eager | NT_mult_assoc4 | m * n * k = m + n * k | 0 | 0.12 | 0 bf_eager | NT_mult_commute1 | m * n = m * m | 0 | 0.118 | 0 bf_eager | NT_mult_commute2 | m * n = n + m | 0 | 0.037 | 0 bf_eager | NT_mult_left_commute1 | x * (y * z) = y * (y * z) | 0 | 3.655 | 0 bf_eager | NT_mult_left_commute2 | x * (y * z) = z * (x * z) | 0 | 4.907 | 0 bf_eager | NT_mult_right_commute1 | x * y * z = x * y * y | 0 | 0.094 | 0 bf_eager | NT_mult_right_commute2 | x * y * z = y * z * y | 0 | 5.485 | 0 bf_eager | NT_mult_suc_right1 | m * suc b = b + m * b | 0 | 0.026 | 0 bf_eager | NT_mult_suc_right2 | m * suc b = m * (m + b) | 0 | 0.838 | 0 bf_eager | NT_mult_suc_right3 | m * suc b = b * (m + b) | 0 | 0.06 | 0 bf_eager | NT_power_1_1 | x ^ suc 0 = 0 | 0 | 0.063 | 0 bf_eager | NT_power_1_2 | x ^ suc 0 = suc 0 | 0 | 0.004 | 0 bf_eager | NT_power_1_3 | x ^ 0 = x | 0 | 0.004 | 0 bf_eager | NT_power_add1 | i ^ (j + k) = i ^ j + i ^ k | 0 | 0.044 | 0 bf_eager | NT_power_add2 | i ^ (j + k) = i ^ j ^ k | 0 | 0.067 | 0 bf_eager | NT_power_add3 | i ^ (j + k) = i ^ j * j ^ k | 0 | 3.343 | 0 bf_eager | NT_power_add4 | i ^ (j + k) = j ^ k * i ^ k | 0 | 0.137 | 0 bf_eager | NT_power_add5 | i ^ (j + k) = (i ^ j) ^ k | 0 | 0.074 | 0 bf_eager | NT_power_mult1 | i ^ (j * k) = (i * j) ^ k | 0 | 0.172 | 0 bf_eager | NT_power_mult2 | i ^ (j * k) = i ^ j * k | 0 | 0.032 | 0 bf_eager | NT_power_mult3 | i ^ (j * k) = (i + j) ^ k | 0 | 0.23 | 0 bf_eager | NT_power_mult4 | i ^ (j * k) = (i + j) * k | 0 | 0.041 | 0 bf_eager | NT_power_squared1 | x ^ suc 0 = x * x | 0 | 2.819 | 0 bf_eager | NT_power_squared2 | x ^ suc suc 0 = x + x | 0 | 4.616 | 0 bf_eager | NT_power_squared3 | x ^ suc suc 0 = x * suc x | 0 | 30 | 1 bf_eager | power_1 | x ^ suc 0 = x | 1 | 0.015 | 0 bf_eager | power_add | i ^ (j + k) = i ^ j * i ^ k | 1 | 3.004 | 0 bf_eager | power_mult | i ^ (j * k) = (i ^ j) ^ k | 0 | 30 | 1 bf_eager | power_squared | x ^ suc suc 0 = x * x | 0 | 10.194 | 0 bf_eager | SP_add_0_0_left | 0 + 0 + a = a | 1 | 0.014 | 0 bf_eager | SP_add_0_a_right | a + 0 + a = a + a | 1 | 0.071 | 0 bf_eager | SP_add_a_a_commute | a + a + b = b + (a + a) | 1 | 0.115 | 0 bf_eager | SP_add_assoc | d + b + c + a = b + (c + (a + d)) | 1 | 7.665 | 0 bf_eager | SP_add_left_cancel | (suc 0 + m = suc 0 + n) = (m = n) | 1 | 0.032 | 0 bf_eager | SP_add_right_cancel | (m + suc 0 = n + suc 0) = (m = n) | 0 | 0.192 | 0 bf_eager | SP_add_suc_suc_right | suc a + suc b = suc suc (a + b) | 1 | 0.122 | 0 bf_eager | SP_mult_0_left_m_k | 0 * m * k = 0 | 1 | 0.019 | 0 bf_eager | SP_mult_0_left_n_plus_m | 0 * (n + m) = 0 | 1 | 0.023 | 0 bf_eager | SP_mult_0_right_n_plus_m | (n + m) * 0 = 0 | 1 | 0.037 | 0 bf_eager | SP_mult_suc_right_and_distr_mult | m * suc b * k = m * k + m * b * k | 0 | 30 | 1 bf_eager | SP_power_add_add | i ^ (j + k + l) = i ^ j * i ^ k * i ^ l | 0 | 30 | 1 bf_eager | L_append_assoc | x @ y @ z = x @ (y @ z) | 1 | 0.098 | 0 bf_eager | L_append_nil2 | l = l @ [] | 1 | 0.018 | 0 bf_eager | L_len_append | len x @ y = len x + len y | 1 | 0.274 | 0 bf_eager | L_len_map | len map f x = len x | 1 | 0.034 | 0 bf_eager | L_len_qrev | len qrev x [] = len x | 0 | 0.229 | 0 bf_eager | L_len_rev | len rev x = len x | 1 | 0.079 | 0 bf_eager | L_map_append | map f x @ y = map f x @ map f y | 1 | 0.241 | 0 bf_eager | L_qrev_map | qrev (map f x) [] = map f qrev x [] | 0 | 2.849 | 0 bf_eager | L_qrev_qrev_gen | qrev qrev xs ys zs = xs @ qrev ys zs | 0 | 7.477 | 0 bf_eager | L_qrev_qrev | qrev qrev x [] [] = x | 0 | 0.155 | 0 bf_eager | L_rev_append_distr | rev (a @ b) = rev b @ rev a | 1 | 0.318 | 0 bf_eager | L_rev_map | rev (map f x) = map f rev x | 1 | 0.32 | 0 bf_eager | L_rev_qrev_gen | qrev x y = rev x @ y | 1 | 0.45 | 0 bf_eager | L_rev_qrev | rev x = qrev x [] | 1 | 0.865 | 0 bf_eager | L_rev_rev_append | rev (rev t @ l) = rev l @ t | 0 | 30 | 1 bf_eager | L_rev_rev | rev rev x = x | 1 | 0.102 | 0 bf_eager | L_rot_append | rot (len l, l @ k) = k @ l | 0 | 30 | 1 bf_eager | L_rot_len | rot (len l, l) = l | 0 | 0.339 | 0 bf_eager_delay | BF_L_destr_app | l ~= [] --> l @ m = head l # tail l @ m | 1 | 0.257 | 0 bf_eager_delay | BF_L_destr_downto | n ~= 0 --> down_to n = n # down_to (pre n) | 1 | 0.058 | 0 bf_eager_delay | BF_L_destr_len | l ~= [] --> len l = suc len tail l | 1 | 0.056 | 0 bf_eager_delay | BF_L_destr_map | l ~= [] --> map f l = f (head l) # map f tail l | 1 | 0.142 | 0 bf_eager_delay | BF_L_destr_mem | l ~= [] --> x mem l = (if x = head l then True else x mem tail l) | 1 | 0.12 | 0 bf_eager_delay | BF_L_destr_pairify | l ~= [] --> pairify l = head l # head l # pairify (tail l) | 1 | 0.145 | 0 bf_eager_delay | BF_L_destr_qrev | l ~= [] --> qrev l [] = qrev tail l [] @ [head l] | 0 | 0.487 | 0 bf_eager_delay | BF_L_destr_rev | l ~= [] --> rev l = rev tail l @ [head l] | 1 | 0.117 | 0 bf_eager_delay | BF_L_destr_upto | n ~= 0 --> up_to n = up_to (pre n) @ [n] | 1 | 0.065 | 0 bf_eager_delay | BF_L_double_len_app | double (len x @ y) = double (len y @ x) | 1 | 1.401 | 0 bf_eager_delay | BF_L_evenM_pairify | evenM (len pairify l) | 1 | 0.04 | 0 bf_eager_delay | BF_L_Gen_destr_len | pre (len l) = len tail l | 1 | 0.03 | 0 bf_eager_delay | BF_L_len_app | len x @ y = len y @ x | 1 | 0.397 | 0 bf_eager_delay | BF_L_len_rev_upto_downto | len up_to (n + m) = len rev down_to (n + m) | 1 | 0.154 | 0 bf_eager_delay | BF_L_rev_upto_downto | down_to (n + m) = rev up_to (n + m) | 1 | 0.342 | 0 bf_eager_delay | BF_L_zip_pairify | zip l l = pairify l | 1 | 0.051 | 0 bf_eager_delay | 2ST_Mut_add_evens | (evenM n = evenM m) = evenM (n + m) | 1 | 0.514 | 0 bf_eager_delay | 2ST_Mut_even_not_odd | evenM n = (~ oddM n) | 1 | 0.058 | 0 bf_eager_delay | 2ST_Mut_even_not_suc | evenM n = (~ evenM (suc n)) | 1 | 0.081 | 0 bf_eager_delay | 2ST_Mut_even_or_odd | evenM n | oddM n | 1 | 0.033 | 0 bf_eager_delay | 2ST_Mut_even_or_suc | evenM n | evenM (suc n) | 1 | 0.071 | 0 bf_eager_delay | 2ST_Mut_plus2_l | evenM n = evenM (suc suc 0 + n) | 1 | 0.026 | 0 bf_eager_delay | 2ST_Mut_plus2_r | evenM n = evenM (n + suc suc 0) | 1 | 0.08 | 0 bf_eager_delay | 3ST_Mod3_disj | ZMT n | OMT n | TMT n | 1 | 0.126 | 0 bf_eager_delay | 3ST_Zero_Mod3 | ZMT n | ZMT (suc n) | ZMT (suc suc n) | 1 | 0.895 | 0 bf_eager_delay | 3ST_Zero_Mod3_times3_l | ZMT n = ZMT (n + suc suc suc 0) | 1 | 0.137 | 0 bf_eager_delay | 3ST_Zero_Mod3_times3_r | ZMT n = ZMT (suc suc suc 0 + n) | 1 | 0.039 | 0 bf_eager_delay | BF_PN_binom_minus | binom (x, suc 0) - x = 0 | 1 | 0.123 | 0 bf_eager_delay | BF_PN_destr_Add | x ~= 0 --> x + y = suc (pre x + y) | 1 | 0.156 | 0 bf_eager_delay | BF_PN_destr_double | n ~= 0 --> double n = suc suc double (pre n) | 1 | 0.061 | 0 bf_eager_delay | BF_PN_destr_Mult | x ~= 0 --> x * y = pre x * y + y | 1 | 0.215 | 0 bf_eager_delay | BF_PN_destr_sum | sum n = sum (pre n) + n | 1 | 0.015 | 0 bf_eager_delay | BF_PN_evenM_times2_l | evenM (n * suc suc 0) | 1 | 0.044 | 0 bf_eager_delay | BF_PN_evenM_times2_r | evenM (suc suc 0 * n) | 0 | 1.643 | 0 bf_eager_delay | BF_PN_evenR_times2_l | evenR (n * suc suc 0) | 1 | 0.028 | 0 bf_eager_delay | BF_PN_evenR_times2_r | evenR (suc suc 0 * n) | 0 | 0.245 | 0 bf_eager_delay | BF_PN_Manning7 | x + suc suc z * y = x + y * suc suc z | 1 | 0.564 | 0 bf_eager_delay | BF_PN_ZeroMod_times3_l | ZMT (n * suc suc suc 0) | 1 | 0.07 | 0 bf_eager_delay | BF_PN_ZeroMod_times3_r | ZMT (suc suc suc 0 * n) | 0 | 30 | 1 bf_eager_delay | add_0_left | 0 + a = a | 1 | 0.011 | 0 bf_eager_delay | add_0_right | a + 0 = a | 1 | 0.014 | 0 bf_eager_delay | add_assoc | b + c + a = b + (c + a) | 1 | 0.088 | 0 bf_eager_delay | add_commute | a + b = b + a | 1 | 0.09 | 0 bf_eager_delay | add_left_cancel | (k + m = k + n) = (m = n) | 1 | 0.044 | 0 bf_eager_delay | add_left_commute | a + (b + c) = b + (a + c) | 1 | 0.132 | 0 bf_eager_delay | add_mult_distrib2 | k * (m + n) = k * m + k * n | 1 | 4.163 | 0 bf_eager_delay | add_mult_distrib | (m + n) * k = m * k + n * k | 1 | 0.733 | 0 bf_eager_delay | add_right_cancel | (m + k = n + k) = (m = n) | 0 | 0.146 | 0 bf_eager_delay | add_right_commute | a + b + c = a + c + b | 1 | 0.19 | 0 bf_eager_delay | add_suc_right | a + suc b = suc (a + b) | 1 | 0.033 | 0 bf_eager_delay | mult_0_left | 0 * m = 0 | 1 | 0.011 | 0 bf_eager_delay | mult_0_right | m * 0 = 0 | 1 | 0.011 | 0 bf_eager_delay | mult_1_left | suc 0 * n = n | 1 | 0.014 | 0 bf_eager_delay | mult_1_right | n * suc 0 = n | 1 | 0.021 | 0 bf_eager_delay | mult_assoc | m * n * k = m * (n * k) | 1 | 0.933 | 0 bf_eager_delay | mult_commute | m * n = n * m | 1 | 0.295 | 0 bf_eager_delay | mult_left_commute | x * (y * z) = y * (x * z) | 1 | 4.574 | 0 bf_eager_delay | mult_right_commute | x * y * z = x * z * y | 0 | 0.329 | 0 bf_eager_delay | mult_suc_left | suc m * b = b + m * b | 1 | 0.044 | 0 bf_eager_delay | mult_suc_right | m * suc b = m + m * b | 1 | 0.253 | 0 bf_eager_delay | NT_add_0_left | 0 + a = 0 | 0 | 0.013 | 0 bf_eager_delay | NT_add_0_right | a + 0 = 0 | 0 | 0.015 | 0 bf_eager_delay | NT_add_assoc1 | b + c + a = b + (c + c) | 0 | 0.055 | 0 bf_eager_delay | NT_add_assoc2 | b + c + a = b + (c + b) | 0 | 0.04 | 0 bf_eager_delay | NT_add_assoc3 | b + c + a = c + (c + a) | 0 | 0.078 | 0 bf_eager_delay | NT_add_commute | a + b = a + a | 0 | 0.02 | 0 bf_eager_delay | NT_add_left_cancel | (k + m = k + n) = (k = n) | 0 | 0.029 | 0 bf_eager_delay | NT_add_mult_distrib1 | (m + n) * k = m * k * (n * k) | 0 | 0.278 | 0 bf_eager_delay | NT_add_mult_distrib2_1 | k * (m + n) = k * m * (k * n) | 0 | 1.123 | 0 bf_eager_delay | NT_add_mult_distrib2_2 | k * (m + n) = k + m + k * n | 0 | 0.074 | 0 bf_eager_delay | NT_add_mult_distrib2_3 | k * (m + n) = k * m + (k + n) | 0 | 0.054 | 0 bf_eager_delay | NT_add_mult_distrib2_4 | k * (m + n) = k * n + k * n | 0 | 0.58 | 0 bf_eager_delay | NT_add_mult_distrib2_5 | k * (m + n) = (k + m) * (k + n) | 0 | 0.665 | 0 bf_eager_delay | NT_add_mult_distrib2 | (m + n) * k = m + k + n * k | 0 | 0.076 | 0 bf_eager_delay | NT_add_mult_distrib3 | (m + n) * k = m * k + (n + k) | 0 | 0.062 | 0 bf_eager_delay | NT_add_mult_distrib4 | (m + n) * k = m * n + n * k | 0 | 0.712 | 0 bf_eager_delay | NT_add_mult_distrib5 | (m + n) * k = (m + k) * (n + k) | 0 | 0.234 | 0 bf_eager_delay | NT_add_right_cancel | (m + k = n + k) = (k = n) | 0 | 0.071 | 0 bf_eager_delay | NT_add_suc_suc_right | a + suc b = suc (suc a + b) | 0 | 0.02 | 0 bf_eager_delay | NT_mult_0_left | 0 * m = m | 0 | 0.01 | 0 bf_eager_delay | NT_mult_0_right | m * 0 = m | 0 | 0.017 | 0 bf_eager_delay | NT_mult_1_left1 | suc 0 * n = suc 0 | 0 | 0.005 | 0 bf_eager_delay | NT_mult_1_left2 | suc 0 * n = 0 | 0 | 0.027 | 0 bf_eager_delay | NT_mult_1_left3 | suc 0 * n = n + n | 0 | 0.082 | 0 bf_eager_delay | NT_mult_1_right1 | n * suc 0 = suc 0 | 0 | 0.004 | 0 bf_eager_delay | NT_mult_1_right2 | n * suc 0 = 0 | 0 | 0.019 | 0 bf_eager_delay | NT_mult_1_right3 | n * suc 0 = n + n | 0 | 0.065 | 0 bf_eager_delay | NT_mult_assoc2 | m * n * k = m + (n + k) | 0 | 0.057 | 0 bf_eager_delay | NT_mult_assoc3 | m * n * k = m * (m * k) | 0 | 0.895 | 0 bf_eager_delay | NT_mult_assoc4 | m * n * k = m + n * k | 0 | 0.111 | 0 bf_eager_delay | NT_mult_commute1 | m * n = m * m | 0 | 0.119 | 0 bf_eager_delay | NT_mult_commute2 | m * n = n + m | 0 | 0.048 | 0 bf_eager_delay | NT_mult_left_commute1 | x * (y * z) = y * (y * z) | 0 | 1.009 | 0 bf_eager_delay | NT_mult_left_commute2 | x * (y * z) = z * (x * z) | 0 | 1.331 | 0 bf_eager_delay | NT_mult_right_commute1 | x * y * z = x * y * y | 0 | 0.094 | 0 bf_eager_delay | NT_mult_right_commute2 | x * y * z = y * z * y | 0 | 0.656 | 0 bf_eager_delay | NT_mult_suc_right1 | m * suc b = b + m * b | 0 | 0.027 | 0 bf_eager_delay | NT_mult_suc_right2 | m * suc b = m * (m + b) | 0 | 0.845 | 0 bf_eager_delay | NT_mult_suc_right3 | m * suc b = b * (m + b) | 0 | 0.063 | 0 bf_eager_delay | NT_power_1_1 | x ^ suc 0 = 0 | 0 | 0.064 | 0 bf_eager_delay | NT_power_1_2 | x ^ suc 0 = suc 0 | 0 | 0.005 | 0 bf_eager_delay | NT_power_1_3 | x ^ 0 = x | 0 | 0.004 | 0 bf_eager_delay | NT_power_add1 | i ^ (j + k) = i ^ j + i ^ k | 0 | 0.045 | 0 bf_eager_delay | NT_power_add2 | i ^ (j + k) = i ^ j ^ k | 0 | 0.067 | 0 bf_eager_delay | NT_power_add3 | i ^ (j + k) = i ^ j * j ^ k | 0 | 1.407 | 0 bf_eager_delay | NT_power_add4 | i ^ (j + k) = j ^ k * i ^ k | 0 | 0.138 | 0 bf_eager_delay | NT_power_add5 | i ^ (j + k) = (i ^ j) ^ k | 0 | 0.077 | 0 bf_eager_delay | NT_power_mult1 | i ^ (j * k) = (i * j) ^ k | 0 | 0.173 | 0 bf_eager_delay | NT_power_mult2 | i ^ (j * k) = i ^ j * k | 0 | 0.033 | 0 bf_eager_delay | NT_power_mult3 | i ^ (j * k) = (i + j) ^ k | 0 | 0.215 | 0 bf_eager_delay | NT_power_mult4 | i ^ (j * k) = (i + j) * k | 0 | 0.04 | 0 bf_eager_delay | NT_power_squared1 | x ^ suc 0 = x * x | 0 | 2.811 | 0 bf_eager_delay | NT_power_squared2 | x ^ suc suc 0 = x + x | 0 | 4.607 | 0 bf_eager_delay | NT_power_squared3 | x ^ suc suc 0 = x * suc x | 0 | 30 | 1 bf_eager_delay | power_1 | x ^ suc 0 = x | 1 | 0.014 | 0 bf_eager_delay | power_add | i ^ (j + k) = i ^ j * i ^ k | 1 | 1.18 | 0 bf_eager_delay | power_mult | i ^ (j * k) = (i ^ j) ^ k | 0 | 13.032 | 0 bf_eager_delay | power_squared | x ^ suc suc 0 = x * x | 0 | 10.161 | 0 bf_eager_delay | SP_add_0_0_left | 0 + 0 + a = a | 1 | 0.013 | 0 bf_eager_delay | SP_add_0_a_right | a + 0 + a = a + a | 1 | 0.069 | 0 bf_eager_delay | SP_add_a_a_commute | a + a + b = b + (a + a) | 1 | 0.19 | 0 bf_eager_delay | SP_add_assoc | d + b + c + a = b + (c + (a + d)) | 1 | 1.751 | 0 bf_eager_delay | SP_add_left_cancel | (suc 0 + m = suc 0 + n) = (m = n) | 1 | 0.032 | 0 bf_eager_delay | SP_add_right_cancel | (m + suc 0 = n + suc 0) = (m = n) | 0 | 0.139 | 0 bf_eager_delay | SP_add_suc_suc_right | suc a + suc b = suc suc (a + b) | 1 | 0.122 | 0 bf_eager_delay | SP_mult_0_left_m_k | 0 * m * k = 0 | 1 | 0.019 | 0 bf_eager_delay | SP_mult_0_left_n_plus_m | 0 * (n + m) = 0 | 1 | 0.023 | 0 bf_eager_delay | SP_mult_0_right_n_plus_m | (n + m) * 0 = 0 | 1 | 0.036 | 0 bf_eager_delay | SP_mult_suc_right_and_distr_mult | m * suc b * k = m * k + m * b * k | 0 | 9.788 | 0 bf_eager_delay | SP_power_add_add | i ^ (j + k + l) = i ^ j * i ^ k * i ^ l | 0 | 9.03 | 0 bf_eager_delay | L_append_assoc | x @ y @ z = x @ (y @ z) | 1 | 0.101 | 0 bf_eager_delay | L_append_nil2 | l = l @ [] | 1 | 0.019 | 0 bf_eager_delay | L_len_append | len x @ y = len x + len y | 1 | 0.284 | 0 bf_eager_delay | L_len_map | len map f x = len x | 1 | 0.035 | 0 bf_eager_delay | L_len_qrev | len qrev x [] = len x | 0 | 0.235 | 0 bf_eager_delay | L_len_rev | len rev x = len x | 1 | 0.084 | 0 bf_eager_delay | L_map_append | map f x @ y = map f x @ map f y | 1 | 0.249 | 0 bf_eager_delay | L_qrev_map | qrev (map f x) [] = map f qrev x [] | 0 | 0.61 | 0 bf_eager_delay | L_qrev_qrev_gen | qrev qrev xs ys zs = xs @ qrev ys zs | 0 | 1.252 | 0 bf_eager_delay | L_qrev_qrev | qrev qrev x [] [] = x | 0 | 0.164 | 0 bf_eager_delay | L_rev_append_distr | rev (a @ b) = rev b @ rev a | 1 | 0.245 | 0 bf_eager_delay | L_rev_map | rev (map f x) = map f rev x | 1 | 0.256 | 0 bf_eager_delay | L_rev_qrev_gen | qrev x y = rev x @ y | 1 | 0.35 | 0 bf_eager_delay | L_rev_qrev | rev x = qrev x [] | 1 | 0.268 | 0 bf_eager_delay | L_rev_rev_append | rev (rev t @ l) = rev l @ t | 0 | 5.645 | 0 bf_eager_delay | L_rev_rev | rev rev x = x | 1 | 0.104 | 0 bf_eager_delay | L_rot_append | rot (len l, l @ k) = k @ l | 0 | 4.489 | 0 bf_eager_delay | L_rot_len | rot (len l, l) = l | 0 | 0.354 | 0 dsum | BF_L_destr_app | l ~= [] --> l @ m = head l # tail l @ m | 0 | 0.266 | 0 dsum | BF_L_destr_downto | n ~= 0 --> down_to n = n # down_to (pre n) | 0 | 0.032 | 0 dsum | BF_L_destr_len | l ~= [] --> len l = suc len tail l | 0 | 0.031 | 0 dsum | BF_L_destr_map | l ~= [] --> map f l = f (head l) # map f tail l | 0 | 0.277 | 0 dsum | BF_L_destr_mem | l ~= [] --> x mem l = (if x = head l then True else x mem tail l) | 1 | 0.111 | 0 dsum | BF_L_destr_pairify | l ~= [] --> pairify l = head l # head l # pairify (tail l) | 0 | 0.079 | 0 dsum | BF_L_destr_qrev | l ~= [] --> qrev l [] = qrev tail l [] @ [head l] | 0 | 0.122 | 0 dsum | BF_L_destr_rev | l ~= [] --> rev l = rev tail l @ [head l] | 0 | 0.064 | 0 dsum | BF_L_destr_upto | n ~= 0 --> up_to n = up_to (pre n) @ [n] | 0 | 0.036 | 0 dsum | BF_L_double_len_app | double (len x @ y) = double (len y @ x) | 1 | 14.231 | 0 dsum | BF_L_evenM_pairify | evenM (len pairify l) | 0 | 0.014 | 0 dsum | BF_L_Gen_destr_len | pre (len l) = len tail l | 1 | 0.018 | 0 dsum | BF_L_len_app | len x @ y = len y @ x | 1 | 0.513 | 0 dsum | BF_L_len_rev_upto_downto | len up_to (n + m) = len rev down_to (n + m) | 1 | 0.084 | 0 dsum | BF_L_rev_upto_downto | down_to (n + m) = rev up_to (n + m) | 1 | 0.279 | 0 dsum | BF_L_zip_pairify | zip l l = pairify l | 1 | 0.042 | 0 dsum | 2ST_Mut_add_evens | (evenM n = evenM m) = evenM (n + m) | 0 | 0.086 | 0 dsum | 2ST_Mut_even_not_odd | evenM n = (~ oddM n) | 0 | 0.042 | 0 dsum | 2ST_Mut_even_not_suc | evenM n = (~ evenM (suc n)) | 0 | 0.061 | 0 dsum | 2ST_Mut_even_or_odd | evenM n | oddM n | 0 | 0.023 | 0 dsum | 2ST_Mut_even_or_suc | evenM n | evenM (suc n) | 0 | 0.054 | 0 dsum | 2ST_Mut_plus2_l | evenM n = evenM (suc suc 0 + n) | 1 | 0.032 | 0 dsum | 2ST_Mut_plus2_r | evenM n = evenM (n + suc suc 0) | 0 | 0.035 | 0 dsum | 3ST_Mod3_disj | ZMT n | OMT n | TMT n | 0 | 0.048 | 0 dsum | 3ST_Zero_Mod3 | ZMT n | ZMT (suc n) | ZMT (suc suc n) | 0 | 0.711 | 0 dsum | 3ST_Zero_Mod3_times3_l | ZMT n = ZMT (n + suc suc suc 0) | 0 | 0.048 | 0 dsum | 3ST_Zero_Mod3_times3_r | ZMT n = ZMT (suc suc suc 0 + n) | 1 | 0.045 | 0 dsum | BF_PN_binom_minus | binom (x, suc 0) - x = 0 | 1 | 0.12 | 0 dsum | BF_PN_destr_Add | x ~= 0 --> x + y = suc (pre x + y) | 0 | 0.147 | 0 dsum | BF_PN_destr_double | n ~= 0 --> double n = suc suc double (pre n) | 0 | 0.037 | 0 dsum | BF_PN_destr_Mult | x ~= 0 --> x * y = pre x * y + y | 0 | 0.124 | 0 dsum | BF_PN_destr_sum | sum n = sum (pre n) + n | 0 | 0.034 | 0 dsum | BF_PN_evenM_times2_l | evenM (n * suc suc 0) | 0 | 0.016 | 0 dsum | BF_PN_evenM_times2_r | evenM (suc suc 0 * n) | 0 | 0.211 | 0 dsum | BF_PN_evenR_times2_l | evenR (n * suc suc 0) | 0 | 0.012 | 0 dsum | BF_PN_evenR_times2_r | evenR (suc suc 0 * n) | 0 | 0.211 | 0 dsum | BF_PN_Manning7 | x + suc suc z * y = x + y * suc suc z | 0 | 30 | 1 dsum | BF_PN_ZeroMod_times3_l | ZMT (n * suc suc suc 0) | 0 | 0.018 | 0 dsum | BF_PN_ZeroMod_times3_r | ZMT (suc suc suc 0 * n) | 0 | 30 | 1 dsum | add_0_left | 0 + a = a | 1 | 0.011 | 0 dsum | add_0_right | a + 0 = a | 1 | 0.012 | 0 dsum | add_assoc | b + c + a = b + (c + a) | 1 | 0.04 | 0 dsum | add_commute | a + b = b + a | 1 | 0.059 | 0 dsum | add_left_cancel | (k + m = k + n) = (m = n) | 1 | 0.032 | 0 dsum | add_left_commute | a + (b + c) = b + (a + c) | 1 | 0.06 | 0 dsum | add_mult_distrib2 | k * (m + n) = k * m + k * n | 1 | 0.201 | 0 dsum | add_mult_distrib | (m + n) * k = m * k + n * k | 1 | 0.387 | 0 dsum | add_right_cancel | (m + k = n + k) = (m = n) | 0 | 0.138 | 0 dsum | add_right_commute | a + b + c = a + c + b | 1 | 0.134 | 0 dsum | add_suc_right | a + suc b = suc (a + b) | 1 | 0.028 | 0 dsum | mult_0_left | 0 * m = 0 | 1 | 0.01 | 0 dsum | mult_0_right | m * 0 = 0 | 1 | 0.012 | 0 dsum | mult_1_left | suc 0 * n = n | 1 | 0.014 | 0 dsum | mult_1_right | n * suc 0 = n | 1 | 0.016 | 0 dsum | mult_assoc | m * n * k = m * (n * k) | 1 | 0.144 | 0 dsum | mult_commute | m * n = n * m | 1 | 0.161 | 0 dsum | mult_left_commute | x * (y * z) = y * (x * z) | 1 | 0.234 | 0 dsum | mult_right_commute | x * y * z = x * z * y | 0 | 0.745 | 0 dsum | mult_suc_left | suc m * b = b + m * b | 1 | 0.025 | 0 dsum | mult_suc_right | m * suc b = m + m * b | 1 | 0.145 | 0 dsum | NT_add_0_left | 0 + a = 0 | 0 | 0.013 | 0 dsum | NT_add_0_right | a + 0 = 0 | 0 | 0.016 | 0 dsum | NT_add_assoc1 | b + c + a = b + (c + c) | 0 | 0.045 | 0 dsum | NT_add_assoc2 | b + c + a = b + (c + b) | 0 | 0.039 | 0 dsum | NT_add_assoc3 | b + c + a = c + (c + a) | 0 | 0.068 | 0 dsum | NT_add_commute | a + b = a + a | 0 | 0.02 | 0 dsum | NT_add_left_cancel | (k + m = k + n) = (k = n) | 0 | 0.03 | 0 dsum | NT_add_mult_distrib1 | (m + n) * k = m * k * (n * k) | 0 | 0.357 | 0 dsum | NT_add_mult_distrib2_1 | k * (m + n) = k * m * (k * n) | 0 | 1.217 | 0 dsum | NT_add_mult_distrib2_2 | k * (m + n) = k + m + k * n | 0 | 0.072 | 0 dsum | NT_add_mult_distrib2_3 | k * (m + n) = k * m + (k + n) | 0 | 0.041 | 0 dsum | NT_add_mult_distrib2_4 | k * (m + n) = k * n + k * n | 0 | 3.994 | 0 dsum | NT_add_mult_distrib2_5 | k * (m + n) = (k + m) * (k + n) | 0 | 3.835 | 0 dsum | NT_add_mult_distrib2 | (m + n) * k = m + k + n * k | 0 | 0.077 | 0 dsum | NT_add_mult_distrib3 | (m + n) * k = m * k + (n + k) | 0 | 0.052 | 0 dsum | NT_add_mult_distrib4 | (m + n) * k = m * n + n * k | 0 | 1.519 | 0 dsum | NT_add_mult_distrib5 | (m + n) * k = (m + k) * (n + k) | 0 | 0.204 | 0 dsum | NT_add_right_cancel | (m + k = n + k) = (k = n) | 0 | 0.06 | 0 dsum | NT_add_suc_suc_right | a + suc b = suc (suc a + b) | 0 | 0.021 | 0 dsum | NT_mult_0_left | 0 * m = m | 0 | 0.009 | 0 dsum | NT_mult_0_right | m * 0 = m | 0 | 0.016 | 0 dsum | NT_mult_1_left1 | suc 0 * n = suc 0 | 0 | 0.005 | 0 dsum | NT_mult_1_left2 | suc 0 * n = 0 | 0 | 0.015 | 0 dsum | NT_mult_1_left3 | suc 0 * n = n + n | 0 | 0.021 | 0 dsum | NT_mult_1_right1 | n * suc 0 = suc 0 | 0 | 0.004 | 0 dsum | NT_mult_1_right2 | n * suc 0 = 0 | 0 | 0.019 | 0 dsum | NT_mult_1_right3 | n * suc 0 = n + n | 0 | 0.041 | 0 dsum | NT_mult_assoc2 | m * n * k = m + (n + k) | 0 | 0.049 | 0 dsum | NT_mult_assoc3 | m * n * k = m * (m * k) | 0 | 30 | 1 dsum | NT_mult_assoc4 | m * n * k = m + n * k | 0 | 0.108 | 0 dsum | NT_mult_commute1 | m * n = m * m | 0 | 0.108 | 0 dsum | NT_mult_commute2 | m * n = n + m | 0 | 0.036 | 0 dsum | NT_mult_left_commute1 | x * (y * z) = y * (y * z) | 0 | 30 | 1 dsum | NT_mult_left_commute2 | x * (y * z) = z * (x * z) | 0 | 3.023 | 0 dsum | NT_mult_right_commute1 | x * y * z = x * y * y | 0 | 0.148 | 0 dsum | NT_mult_right_commute2 | x * y * z = y * z * y | 0 | 0.55 | 0 dsum | NT_mult_suc_right1 | m * suc b = b + m * b | 0 | 0.027 | 0 dsum | NT_mult_suc_right2 | m * suc b = m * (m + b) | 0 | 0.685 | 0 dsum | NT_mult_suc_right3 | m * suc b = b * (m + b) | 0 | 0.047 | 0 dsum | NT_power_1_1 | x ^ suc 0 = 0 | 0 | 0.016 | 0 dsum | NT_power_1_2 | x ^ suc 0 = suc 0 | 0 | 0.005 | 0 dsum | NT_power_1_3 | x ^ 0 = x | 0 | 0.004 | 0 dsum | NT_power_add1 | i ^ (j + k) = i ^ j + i ^ k | 0 | 0.037 | 0 dsum | NT_power_add2 | i ^ (j + k) = i ^ j ^ k | 0 | 0.067 | 0 dsum | NT_power_add3 | i ^ (j + k) = i ^ j * j ^ k | 0 | 0.405 | 0 dsum | NT_power_add4 | i ^ (j + k) = j ^ k * i ^ k | 0 | 0.138 | 0 dsum | NT_power_add5 | i ^ (j + k) = (i ^ j) ^ k | 0 | 0.078 | 0 dsum | NT_power_mult1 | i ^ (j * k) = (i * j) ^ k | 0 | 0.16 | 0 dsum | NT_power_mult2 | i ^ (j * k) = i ^ j * k | 0 | 0.022 | 0 dsum | NT_power_mult3 | i ^ (j * k) = (i + j) ^ k | 0 | 0.2 | 0 dsum | NT_power_mult4 | i ^ (j * k) = (i + j) * k | 0 | 0.033 | 0 dsum | NT_power_squared1 | x ^ suc 0 = x * x | 0 | 12.996 | 0 dsum | NT_power_squared2 | x ^ suc suc 0 = x + x | 0 | 0.041 | 0 dsum | NT_power_squared3 | x ^ suc suc 0 = x * suc x | 0 | 0.094 | 0 dsum | power_1 | x ^ suc 0 = x | 1 | 0.014 | 0 dsum | power_add | i ^ (j + k) = i ^ j * i ^ k | 1 | 0.967 | 0 dsum | power_mult | i ^ (j * k) = (i ^ j) ^ k | 0 | 30 | 1 dsum | power_squared | x ^ suc suc 0 = x * x | 0 | 0.029 | 0 dsum | SP_add_0_0_left | 0 + 0 + a = a | 1 | 0.014 | 0 dsum | SP_add_0_a_right | a + 0 + a = a + a | 1 | 0.049 | 0 dsum | SP_add_a_a_commute | a + a + b = b + (a + a) | 1 | 0.137 | 0 dsum | SP_add_assoc | d + b + c + a = b + (c + (a + d)) | 1 | 0.674 | 0 dsum | SP_add_left_cancel | (suc 0 + m = suc 0 + n) = (m = n) | 1 | 0.021 | 0 dsum | SP_add_right_cancel | (m + suc 0 = n + suc 0) = (m = n) | 0 | 0.135 | 0 dsum | SP_add_suc_suc_right | suc a + suc b = suc suc (a + b) | 1 | 0.037 | 0 dsum | SP_mult_0_left_m_k | 0 * m * k = 0 | 1 | 0.012 | 0 dsum | SP_mult_0_left_n_plus_m | 0 * (n + m) = 0 | 1 | 0.012 | 0 dsum | SP_mult_0_right_n_plus_m | (n + m) * 0 = 0 | 1 | 0.041 | 0 dsum | SP_mult_suc_right_and_distr_mult | m * suc b * k = m * k + m * b * k | 0 | 30 | 1 dsum | SP_power_add_add | i ^ (j + k + l) = i ^ j * i ^ k * i ^ l | 0 | 15.068 | 0 dsum | L_append_assoc | x @ y @ z = x @ (y @ z) | 1 | 0.047 | 0 dsum | L_append_nil2 | l = l @ [] | 1 | 0.017 | 0 dsum | L_len_append | len x @ y = len x + len y | 1 | 0.047 | 0 dsum | L_len_map | len map f x = len x | 1 | 0.044 | 0 dsum | L_len_qrev | len qrev x [] = len x | 0 | 0.047 | 0 dsum | L_len_rev | len rev x = len x | 1 | 0.076 | 0 dsum | L_map_append | map f x @ y = map f x @ map f y | 1 | 0.175 | 0 dsum | L_qrev_map | qrev (map f x) [] = map f qrev x [] | 0 | 0.278 | 0 dsum | L_qrev_qrev_gen | qrev qrev xs ys zs = xs @ qrev ys zs | 0 | 0.428 | 0 dsum | L_qrev_qrev | qrev qrev x [] [] = x | 0 | 0.054 | 0 dsum | L_rev_append_distr | rev (a @ b) = rev b @ rev a | 1 | 0.271 | 0 dsum | L_rev_map | rev (map f x) = map f rev x | 1 | 0.248 | 0 dsum | L_rev_qrev_gen | qrev x y = rev x @ y | 1 | 0.107 | 0 dsum | L_rev_qrev | rev x = qrev x [] | 0 | 0.106 | 0 dsum | L_rev_rev_append | rev (rev t @ l) = rev l @ t | 0 | 5.895 | 0 dsum | L_rev_rev | rev rev x = x | 1 | 0.099 | 0 dsum | L_rot_append | rot (len l, l @ k) = k @ l | 0 | 30 | 1 dsum | L_rot_len | rot (len l, l) = l | 0 | 0.207 | 0