Signed arithmetic tables and finite sums — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

214 checked bundle nodes · 571 proof edges · 13724 body proof nodes.

Literal self-contained proof bundle · SHA-256 35bc01ab3f12cc09a5ed9aa3098225090dcc40ac241f9cbd669f99cef4737e57

divisor_sum_algebra_candidate.py · divisor_sum_reindex_candidate.py · divisor_sum_table_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites

SS0001 divisor_signed_table_at_from_components · actual bundle node 183
SS0002 divisor_signed_table_at_to_components · actual bundle node 184
SS0003 divisor_signed_table_from_components · actual bundle node 185
SS0004 divisor_signed_table_construct · actual bundle node 186
SS0005 divisor_signed_table_components · actual bundle node 187
SS0006 divisor_signed_table_lookup · actual bundle node 188
SS0007 divisor_signed_table_at_functional · actual bundle node 189
SS0008 divisor_signed_table_restrict · actual bundle node 190
SS0009 divisor_signed_sum_from_components · actual bundle node 191
SS000A divisor_signed_sum_to_components · actual bundle node 192
SS000B divisor_signed_sum_exists_from_components · actual bundle node 193
SS000C divisor_signed_sum_functional · actual bundle node 194
SS000D divisor_signed_sum_empty_value · actual bundle node 195
SS000E divisor_signed_sum_empty_exists · actual bundle node 196
SS000F divisor_signed_balance_negate · actual bundle node 197
SS0010 divisor_signed_balance_negate_intro · actual bundle node 198
SS0011 divisor_signed_negate_fixed_zero · actual bundle node 199
SS0012 divisor_natural_sum_successor_intro · actual bundle node 200
SS0013 divisor_signed_table_equality_component_balance · actual bundle node 201
SS0014 divisor_signed_sum_extensional · actual bundle node 202
SS0015 divisor_signed_sum_negation_transport · actual bundle node 203
SS0016 divisor_signed_sum_successor_intro · actual bundle node 204
SS0017 divisor_signed_sum_successor_decompose · actual bundle node 205
SS0018 divisor_signed_table_lookup_from_components · actual bundle node 206
SS0019 divisor_signed_table_reindex_data_exists · actual bundle node 207
SS001A divisor_signed_table_reindex_from_components · actual bundle node 208
SS001B divisor_signed_table_reindex_exists · actual bundle node 209
SS001C divisor_signed_table_reindex_functional · actual bundle node 210
SS001D divisor_signed_sum_component_reindex · actual bundle node 211
SS001E divisor_signed_sum_permutation_invariant · actual bundle node 212
add_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n + m = m + n
```

beta_at_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c i. exists x. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

beta_at_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

beta_sum_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l. exists n. (exists ff_u_x ff_v_x. ((((exists ff_h_x_start. ff_h_x_start + S (0) = S ((S (0)) * ff_v_x)) /\ exists ff_q_x_start. ff_u_x = ff_q_x_start * S ((S (0)) * ff_v_x) + (0))) /\ ((((exists ff_h_x_terminal. ff_h_x_terminal + S (n) = S ((S (l)) * ff_v_x)) /\ exists ff_q_x_terminal. ff_u_x = ff_q_x_terminal * S ((S (l)) * ff_v_x) + (n))) /\ forall ff_i_x. (exists ff_lt_x_bound. ff_lt_x_bound + S ff_i_x = l) -> exists ff_a_x ff_r_x ff_s_x. ((((exists ff_h_x_summand. ff_h_x_summand + S (ff_a_x) = S ((S (ff_i_x)) * c)) /\ exists ff_q_x_summand. b = ff_q_x_summand * S ((S (ff_i_x)) * c) + (ff_a_x))) /\ ((((exists ff_h_x_partial. ff_h_x_partial + S (ff_r_x) = S ((S (ff_i_x)) * ff_v_x)) /\ exists ff_q_x_partial. ff_u_x = ff_q_x_partial * S ((S (ff_i_x)) * ff_v_x) + (ff_r_x))) /\ ((((exists ff_h_x_successor. ff_h_x_successor + S (ff_s_x) = S ((S (S ff_i_x)) * ff_v_x)) /\ exists ff_q_x_successor. ff_u_x = ff_q_x_successor * S ((S (S ff_i_x)) * ff_v_x) + (ff_s_x))) /\ ff_s_x = ff_r_x + ff_a_x))))))

beta_sum_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l n m. (exists ff_u_l ff_v_l. ((((exists ff_h_l_start. ff_h_l_start + S (0) = S ((S (0)) * ff_v_l)) /\ exists ff_q_l_start. ff_u_l = ff_q_l_start * S ((S (0)) * ff_v_l) + (0))) /\ ((((exists ff_h_l_terminal. ff_h_l_terminal + S (n) = S ((S (l)) * ff_v_l)) /\ exists ff_q_l_terminal. ff_u_l = ff_q_l_terminal * S ((S (l)) * ff_v_l) + (n))) /\ forall ff_i_l. (exists ff_lt_l_bound. ff_lt_l_bound + S ff_i_l = l) -> exists ff_a_l ff_r_l ff_s_l. ((((exists ff_h_l_summand. ff_h_l_summand + S (ff_a_l) = S ((S (ff_i_l)) * c)) /\ exists ff_q_l_summand. b = ff_q_l_summand * S ((S (ff_i_l)) * c) + (ff_a_l))) /\ ((((exists ff_h_l_partial. ff_h_l_partial + S (ff_r_l) = S ((S (ff_i_l)) * ff_v_l)) /\ exists ff_q_l_partial. ff_u_l = ff_q_l_partial * S ((S (ff_i_l)) * ff_v_l) + (ff_r_l))) /\ ((((exists ff_h_l_successor. ff_h_l_successor + S (ff_s_l) = S ((S (S ff_i_l)) * ff_v_l)) /\ exists ff_q_l_successor. ff_u_l = ff_q_l_successor * S ((S (S ff_i_l)) * ff_v_l) + (ff_s_l))) /\ ff_s_l = ff_r_l + ff_a_l)))))) -> (exists ff_u_r ff_v_r. ((((exists ff_h_r_start. ff_h_r_start + S (0) = S ((S (0)) * ff_v_r)) /\ exists ff_q_r_start. ff_u_r = ff_q_r_start * S ((S (0)) * ff_v_r) + (0))) /\ ((((exists ff_h_r_terminal. ff_h_r_terminal + S (m) = S ((S (l)) * ff_v_r)) /\ exists ff_q_r_terminal. ff_u_r = ff_q_r_terminal * S ((S (l)) * ff_v_r) + (m))) /\ forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> exists ff_a_r ff_r_r ff_s_r. ((((exists ff_h_r_summand. ff_h_r_summand + S (ff_a_r) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_summand. b = ff_q_r_summand * S ((S (ff_i_r)) * c) + (ff_a_r))) /\ ((((exists ff_h_r_partial. ff_h_r_partial + S (ff_r_r) = S ((S (ff_i_r)) * ff_v_r)) /\ exists ff_q_r_partial. ff_u_r = ff_q_r_partial * S ((S (ff_i_r)) * ff_v_r) + (ff_r_r))) /\ ((((exists ff_h_r_successor. ff_h_r_successor + S (ff_s_r) = S ((S (S ff_i_r)) * ff_v_r)) /\ exists ff_q_r_successor. ff_u_r = ff_q_r_successor * S ((S (S ff_i_r)) * ff_v_r) + (ff_s_r))) /\ ff_s_r = ff_r_r + ff_a_r)))))) -> n = m

beta_sum_permutation_invariant · checked inherited prerequisite

Exact statement in the checked dependency cone

forall l r s b c z d p q. (forall fp_i_reindex_bounded. (exists fp_gap_reindex_bounded_index. fp_gap_reindex_bounded_index + S fp_i_reindex_bounded = l) -> exists fp_value_reindex_bounded. ((((exists ff_h_reindex_bounded_entry. ff_h_reindex_bounded_entry + S (fp_value_reindex_bounded) = S ((S (fp_i_reindex_bounded)) * s)) /\ exists ff_q_reindex_bounded_entry. r = ff_q_reindex_bounded_entry * S ((S (fp_i_reindex_bounded)) * s) + (fp_value_reindex_bounded))) /\ (exists fp_gap_reindex_bounded_value. fp_gap_reindex_bounded_value + S fp_value_reindex_bounded = l))) -> (forall fp_i_reindex_injective fp_j_reindex_injective fp_value_reindex_injective. (exists fp_gap_reindex_injective_i. fp_gap_reindex_injective_i + S fp_i_reindex_injective = l) -> (exists fp_gap_reindex_injective_j. fp_gap_reindex_injective_j + S fp_j_reindex_injective = l) -> (((exists ff_h_reindex_injective_left. ff_h_reindex_injective_left + S (fp_value_reindex_injective) = S ((S (fp_i_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_left. r = ff_q_reindex_injective_left * S ((S (fp_i_reindex_injective)) * s) + (fp_value_reindex_injective))) -> (((exists ff_h_reindex_injective_right. ff_h_reindex_injective_right + S (fp_value_reindex_injective) = S ((S (fp_j_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_right. r = ff_q_reindex_injective_right * S ((S (fp_j_reindex_injective)) * s) + (fp_value_reindex_injective))) -> fp_i_reindex_injective = fp_j_reindex_injective) -> (forall fpr_i_reindex_aligned fpr_j_reindex_aligned fpr_x_reindex_aligned. (exists fpr_h_reindex_aligned. fpr_h_reindex_aligned + S fpr_i_reindex_aligned = l) -> (((exists ff_h_reindex_aligned_map. ff_h_reindex_aligned_map + S (fpr_j_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * s)) /\ exists ff_q_reindex_aligned_map. r = ff_q_reindex_aligned_map * S ((S (fpr_i_reindex_aligned)) * s) + (fpr_j_reindex_aligned))) -> (((exists ff_h_reindex_aligned_source. ff_h_reindex_aligned_source + S (fpr_x_reindex_aligned) = S ((S (fpr_j_reindex_aligned)) * c)) /\ exists ff_q_reindex_aligned_source. b = ff_q_reindex_aligned_source * S ((S (fpr_j_reindex_aligned)) * c) + (fpr_x_reindex_aligned))) -> (((exists ff_h_reindex_aligned_target. ff_h_reindex_aligned_target + S (fpr_x_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * d)) /\ exists ff_q_reindex_aligned_target. z = ff_q_reindex_aligned_target * S ((S (fpr_i_reindex_aligned)) * d) + (fpr_x_reindex_aligned)))) -> (exists ff_u_reindex_source_product ff_v_reindex_source_product. ((((exists ff_h_reindex_source_product_start. ff_h_reindex_source_product_start + S (0) = S ((S (0)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_start. ff_u_reindex_source_product = ff_q_reindex_source_product_start * S ((S (0)) * ff_v_reindex_source_product) + (0))) /\ ((((exists ff_h_reindex_source_product_terminal. ff_h_reindex_source_product_terminal + S (p) = S ((S (l)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_terminal. ff_u_reindex_source_product = ff_q_reindex_source_product_terminal * S ((S (l)) * ff_v_reindex_source_product) + (p))) /\ forall ff_i_reindex_source_product. (exists ff_lt_reindex_source_product_bound. ff_lt_reindex_source_product_bound + S ff_i_reindex_source_product = l) -> exists ff_a_reindex_source_product ff_r_reindex_source_product ff_s_reindex_source_product. ((((exists ff_h_reindex_source_product_summand. ff_h_reindex_source_product_summand + S (ff_a_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * c)) /\ exists ff_q_reindex_source_product_summand. b = ff_q_reindex_source_product_summand * S ((S (ff_i_reindex_source_product)) * c) + (ff_a_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_partial. ff_h_reindex_source_product_partial + S (ff_r_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_partial. ff_u_reindex_source_product = ff_q_reindex_source_product_partial * S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_r_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_successor. ff_h_reindex_source_product_successor + S (ff_s_reindex_source_product) = S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_successor. ff_u_reindex_source_product = ff_q_reindex_source_product_successor * S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_s_reindex_source_product))) /\ ff_s_reindex_source_product = ff_r_reindex_source_product + ff_a_reindex_source_product)))))) -> (exists ff_u_reindex_target_product ff_v_reindex_target_product. ((((exists ff_h_reindex_target_product_start. ff_h_reindex_target_product_start + S (0) = S ((S (0)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_start. ff_u_reindex_target_product = ff_q_reindex_target_product_start * S ((S (0)) * ff_v_reindex_target_product) + (0))) /\ ((((exists ff_h_reindex_target_product_terminal. ff_h_reindex_target_product_terminal + S (q) = S ((S (l)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_terminal. ff_u_reindex_target_product = ff_q_reindex_target_product_terminal * S ((S (l)) * ff_v_reindex_target_product) + (q))) /\ forall ff_i_reindex_target_product. (exists ff_lt_reindex_target_product_bound. ff_lt_reindex_target_product_bound + S ff_i_reindex_target_product = l) -> exists ff_a_reindex_target_product ff_r_reindex_target_product ff_s_reindex_target_product. ((((exists ff_h_reindex_target_product_summand. ff_h_reindex_target_product_summand + S (ff_a_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * d)) /\ exists ff_q_reindex_target_product_summand. z = ff_q_reindex_target_product_summand * S ((S (ff_i_reindex_target_product)) * d) + (ff_a_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_partial. ff_h_reindex_target_product_partial + S (ff_r_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_partial. ff_u_reindex_target_product = ff_q_reindex_target_product_partial * S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_r_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_successor. ff_h_reindex_target_product_successor + S (ff_s_reindex_target_product) = S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_successor. ff_u_reindex_target_product = ff_q_reindex_target_product_successor * S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_s_reindex_target_product))) /\ ff_s_reindex_target_product = ff_r_reindex_target_product + ff_a_reindex_target_product)))))) -> p = q

beta_sum_succ_decompose · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l n. (exists fs_u_succ fs_v_succ. ((((exists fs_h_succ_body_start. fs_h_succ_body_start + S (0) = S ((S (0)) * fs_v_succ)) /\ exists fs_q_succ_body_start. fs_u_succ = fs_q_succ_body_start * S ((S (0)) * fs_v_succ) + (0))) /\ ((((exists fs_h_succ_body_terminal. fs_h_succ_body_terminal + S (n) = S ((S (S l)) * fs_v_succ)) /\ exists fs_q_succ_body_terminal. fs_u_succ = fs_q_succ_body_terminal * S ((S (S l)) * fs_v_succ) + (n))) /\ forall fs_i_succ_body_steps. (exists fs_lt_succ_body_steps_bound. fs_lt_succ_body_steps_bound + S fs_i_succ_body_steps = S l) -> exists fs_a_succ_body_steps fs_r_succ_body_steps fs_s_succ_body_steps. ((((exists fs_h_succ_body_steps_summand. fs_h_succ_body_steps_summand + S (fs_a_succ_body_steps) = S ((S (fs_i_succ_body_steps)) * c)) /\ exists fs_q_succ_body_steps_summand. b = fs_q_succ_body_steps_summand * S ((S (fs_i_succ_body_steps)) * c) + (fs_a_succ_body_steps))) /\ ((((exists fs_h_succ_body_steps_partial. fs_h_succ_body_steps_partial + S (fs_r_succ_body_steps) = S ((S (fs_i_succ_body_steps)) * fs_v_succ)) /\ exists fs_q_succ_body_steps_partial. fs_u_succ = fs_q_succ_body_steps_partial * S ((S (fs_i_succ_body_steps)) * fs_v_succ) + (fs_r_succ_body_steps))) /\ ((((exists fs_h_succ_body_steps_successor. fs_h_succ_body_steps_successor + S (fs_s_succ_body_steps) = S ((S (S fs_i_succ_body_steps)) * fs_v_succ)) /\ exists fs_q_succ_body_steps_successor. fs_u_succ = fs_q_succ_body_steps_successor * S ((S (S fs_i_succ_body_steps)) * fs_v_succ) + (fs_s_succ_body_steps))) /\ fs_s_succ_body_steps = fs_r_succ_body_steps + fs_a_succ_body_steps)))))) -> exists a r. (((exists fs_h_succ_factor. fs_h_succ_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_succ_factor. b = fs_q_succ_factor * S ((S (l)) * c) + (a))) /\ ((exists ff_u_prefix ff_v_prefix. ((((exists ff_h_prefix_start. ff_h_prefix_start + S (0) = S ((S (0)) * ff_v_prefix)) /\ exists ff_q_prefix_start. ff_u_prefix = ff_q_prefix_start * S ((S (0)) * ff_v_prefix) + (0))) /\ ((((exists ff_h_prefix_terminal. ff_h_prefix_terminal + S (r) = S ((S (l)) * ff_v_prefix)) /\ exists ff_q_prefix_terminal. ff_u_prefix = ff_q_prefix_terminal * S ((S (l)) * ff_v_prefix) + (r))) /\ forall ff_i_prefix. (exists ff_lt_prefix_bound. ff_lt_prefix_bound + S ff_i_prefix = l) -> exists ff_a_prefix ff_r_prefix ff_s_prefix. ((((exists ff_h_prefix_summand. ff_h_prefix_summand + S (ff_a_prefix) = S ((S (ff_i_prefix)) * c)) /\ exists ff_q_prefix_summand. b = ff_q_prefix_summand * S ((S (ff_i_prefix)) * c) + (ff_a_prefix))) /\ ((((exists ff_h_prefix_partial. ff_h_prefix_partial + S (ff_r_prefix) = S ((S (ff_i_prefix)) * ff_v_prefix)) /\ exists ff_q_prefix_partial. ff_u_prefix = ff_q_prefix_partial * S ((S (ff_i_prefix)) * ff_v_prefix) + (ff_r_prefix))) /\ ((((exists ff_h_prefix_successor. ff_h_prefix_successor + S (ff_s_prefix) = S ((S (S ff_i_prefix)) * ff_v_prefix)) /\ exists ff_q_prefix_successor. ff_u_prefix = ff_q_prefix_successor * S ((S (S ff_i_prefix)) * ff_v_prefix) + (ff_s_prefix))) /\ ff_s_prefix = ff_r_prefix + ff_a_prefix)))))) /\ n = r + a)

beta_sum_zero · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c n. (exists fs_u_zero fs_v_zero. ((((exists fs_h_zero_body_start. fs_h_zero_body_start + S (0) = S ((S (0)) * fs_v_zero)) /\ exists fs_q_zero_body_start. fs_u_zero = fs_q_zero_body_start * S ((S (0)) * fs_v_zero) + (0))) /\ ((((exists fs_h_zero_body_terminal. fs_h_zero_body_terminal + S (n) = S ((S (0)) * fs_v_zero)) /\ exists fs_q_zero_body_terminal. fs_u_zero = fs_q_zero_body_terminal * S ((S (0)) * fs_v_zero) + (n))) /\ forall fs_i_zero_body_steps. (exists fs_lt_zero_body_steps_bound. fs_lt_zero_body_steps_bound + S fs_i_zero_body_steps = 0) -> exists fs_a_zero_body_steps fs_r_zero_body_steps fs_s_zero_body_steps. ((((exists fs_h_zero_body_steps_summand. fs_h_zero_body_steps_summand + S (fs_a_zero_body_steps) = S ((S (fs_i_zero_body_steps)) * c)) /\ exists fs_q_zero_body_steps_summand. b = fs_q_zero_body_steps_summand * S ((S (fs_i_zero_body_steps)) * c) + (fs_a_zero_body_steps))) /\ ((((exists fs_h_zero_body_steps_partial. fs_h_zero_body_steps_partial + S (fs_r_zero_body_steps) = S ((S (fs_i_zero_body_steps)) * fs_v_zero)) /\ exists fs_q_zero_body_steps_partial. fs_u_zero = fs_q_zero_body_steps_partial * S ((S (fs_i_zero_body_steps)) * fs_v_zero) + (fs_r_zero_body_steps))) /\ ((((exists fs_h_zero_body_steps_successor. fs_h_zero_body_steps_successor + S (fs_s_zero_body_steps) = S ((S (S fs_i_zero_body_steps)) * fs_v_zero)) /\ exists fs_q_zero_body_steps_successor. fs_u_zero = fs_q_zero_body_steps_successor * S ((S (S fs_i_zero_body_steps)) * fs_v_zero) + (fs_s_zero_body_steps))) /\ fs_s_zero_body_steps = fs_r_zero_body_steps + fs_a_zero_body_steps)))))) -> n = 0

finite_beta_composition_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall r s b c l. exists z d. (forall fms_i_compose fms_j_compose fms_v_compose. (exists fms_gap_compose. fms_gap_compose + S (fms_i_compose) = (l)) -> (((exists fs_h_fms_compose_index. fs_h_fms_compose_index + S (fms_j_compose) = S ((S (fms_i_compose)) * s)) /\ exists fs_q_fms_compose_index. r = fs_q_fms_compose_index * S ((S (fms_i_compose)) * s) + (fms_j_compose))) -> (((exists fs_h_fms_compose_source. fs_h_fms_compose_source + S (fms_v_compose) = S ((S (fms_j_compose)) * c)) /\ exists fs_q_fms_compose_source. b = fs_q_fms_compose_source * S ((S (fms_j_compose)) * c) + (fms_v_compose))) -> (((exists fs_h_fms_compose_target. fs_h_fms_compose_target + S (fms_v_compose) = S ((S (fms_i_compose)) * d)) /\ exists fs_q_fms_compose_target. z = fs_q_fms_compose_target * S ((S (fms_i_compose)) * d) + (fms_v_compose))))

gaussian_signed_add_of_balances · checked inherited prerequisite

Exact statement in the checked dependency cone

forall ac bc cc p n q m. (exists ge_balance_positive_bridge_first_add ge_balance_negative_bridge_first_add. (((((ac) = 2 * (ge_balance_positive_bridge_first_add) /\ (ge_balance_negative_bridge_first_add) = 0) \/ exists ge_signed_half_bridge_first_adddecode. (((ac) = 2 * ge_signed_half_bridge_first_adddecode + 1 /\ (ge_balance_positive_bridge_first_add) = 0) /\ (ge_balance_negative_bridge_first_add) = S ge_signed_half_bridge_first_adddecode))) /\ ((p) + ge_balance_negative_bridge_first_add = (n) + ge_balance_positive_bridge_first_add))) -> (exists ge_balance_positive_bridge_second_add ge_balance_negative_bridge_second_add. (((((bc) = 2 * (ge_balance_positive_bridge_second_add) /\ (ge_balance_negative_bridge_second_add) = 0) \/ exists ge_signed_half_bridge_second_adddecode. (((bc) = 2 * ge_signed_half_bridge_second_adddecode + 1 /\ (ge_balance_positive_bridge_second_add) = 0) /\ (ge_balance_negative_bridge_second_add) = S ge_signed_half_bridge_second_adddecode))) /\ ((q) + ge_balance_negative_bridge_second_add = (m) + ge_balance_positive_bridge_second_add))) -> (exists ge_balance_positive_bridge_output_add ge_balance_negative_bridge_output_add. (((((cc) = 2 * (ge_balance_positive_bridge_output_add) /\ (ge_balance_negative_bridge_output_add) = 0) \/ exists ge_signed_half_bridge_output_adddecode. (((cc) = 2 * ge_signed_half_bridge_output_adddecode + 1 /\ (ge_balance_positive_bridge_output_add) = 0) /\ (ge_balance_negative_bridge_output_add) = S ge_signed_half_bridge_output_adddecode))) /\ ((((p) + (q))) + ge_balance_negative_bridge_output_add = (((n) + (m))) + ge_balance_positive_bridge_output_add))) -> (exists sa_lp_gaussian_bridge_add sa_ln_gaussian_bridge_add sa_rp_gaussian_bridge_add sa_rn_gaussian_bridge_add sa_op_gaussian_bridge_add sa_on_gaussian_bridge_add. (((ac = 2 * sa_lp_gaussian_bridge_add /\ sa_ln_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_left. ((ac = 2 * sd_half_gaussian_bridge_add_left + 1 /\ sa_lp_gaussian_bridge_add = 0) /\ sa_ln_gaussian_bridge_add = S sd_half_gaussian_bridge_add_left)) /\ (((bc = 2 * sa_rp_gaussian_bridge_add /\ sa_rn_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_right. ((bc = 2 * sd_half_gaussian_bridge_add_right + 1 /\ sa_rp_gaussian_bridge_add = 0) /\ sa_rn_gaussian_bridge_add = S sd_half_gaussian_bridge_add_right)) /\ (((cc = 2 * sa_op_gaussian_bridge_add /\ sa_on_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_output. ((cc = 2 * sd_half_gaussian_bridge_add_output + 1 /\ sa_op_gaussian_bridge_add = 0) /\ sa_on_gaussian_bridge_add = S sd_half_gaussian_bridge_add_output)) /\ (sa_lp_gaussian_bridge_add + sa_rp_gaussian_bridge_add) + sa_on_gaussian_bridge_add = (sa_ln_gaussian_bridge_add + sa_rn_gaussian_bridge_add) + sa_op_gaussian_bridge_add))))

gaussian_signed_add_to_balance · checked inherited prerequisite

Exact statement in the checked dependency cone

forall ac bc cc p n q m. (exists ge_balance_positive_bridge_elim_first_add ge_balance_negative_bridge_elim_first_add. (((((ac) = 2 * (ge_balance_positive_bridge_elim_first_add) /\ (ge_balance_negative_bridge_elim_first_add) = 0) \/ exists ge_signed_half_bridge_elim_first_adddecode. (((ac) = 2 * ge_signed_half_bridge_elim_first_adddecode + 1 /\ (ge_balance_positive_bridge_elim_first_add) = 0) /\ (ge_balance_negative_bridge_elim_first_add) = S ge_signed_half_bridge_elim_first_adddecode))) /\ ((p) + ge_balance_negative_bridge_elim_first_add = (n) + ge_balance_positive_bridge_elim_first_add))) -> (exists ge_balance_positive_bridge_elim_second_add ge_balance_negative_bridge_elim_second_add. (((((bc) = 2 * (ge_balance_positive_bridge_elim_second_add) /\ (ge_balance_negative_bridge_elim_second_add) = 0) \/ exists ge_signed_half_bridge_elim_second_adddecode. (((bc) = 2 * ge_signed_half_bridge_elim_second_adddecode + 1 /\ (ge_balance_positive_bridge_elim_second_add) = 0) /\ (ge_balance_negative_bridge_elim_second_add) = S ge_signed_half_bridge_elim_second_adddecode))) /\ ((q) + ge_balance_negative_bridge_elim_second_add = (m) + ge_balance_positive_bridge_elim_second_add))) -> (exists sa_lp_gaussian_bridge_elim_add sa_ln_gaussian_bridge_elim_add sa_rp_gaussian_bridge_elim_add sa_rn_gaussian_bridge_elim_add sa_op_gaussian_bridge_elim_add sa_on_gaussian_bridge_elim_add. (((ac = 2 * sa_lp_gaussian_bridge_elim_add /\ sa_ln_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_left. ((ac = 2 * sd_half_gaussian_bridge_elim_add_left + 1 /\ sa_lp_gaussian_bridge_elim_add = 0) /\ sa_ln_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_left)) /\ (((bc = 2 * sa_rp_gaussian_bridge_elim_add /\ sa_rn_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_right. ((bc = 2 * sd_half_gaussian_bridge_elim_add_right + 1 /\ sa_rp_gaussian_bridge_elim_add = 0) /\ sa_rn_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_right)) /\ (((cc = 2 * sa_op_gaussian_bridge_elim_add /\ sa_on_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_output. ((cc = 2 * sd_half_gaussian_bridge_elim_add_output + 1 /\ sa_op_gaussian_bridge_elim_add = 0) /\ sa_on_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_output)) /\ (sa_lp_gaussian_bridge_elim_add + sa_rp_gaussian_bridge_elim_add) + sa_on_gaussian_bridge_elim_add = (sa_ln_gaussian_bridge_elim_add + sa_rn_gaussian_bridge_elim_add) + sa_op_gaussian_bridge_elim_add)))) -> (exists ge_balance_positive_signed_bridge_elimination_add ge_balance_negative_signed_bridge_elimination_add. (((((cc) = 2 * (ge_balance_positive_signed_bridge_elimination_add) /\ (ge_balance_negative_signed_bridge_elimination_add) = 0) \/ exists ge_signed_half_signed_bridge_elimination_adddecode. (((cc) = 2 * ge_signed_half_signed_bridge_elimination_adddecode + 1 /\ (ge_balance_positive_signed_bridge_elimination_add) = 0) /\ (ge_balance_negative_signed_bridge_elimination_add) = S ge_signed_half_signed_bridge_elimination_adddecode))) /\ ((((p) + (q))) + ge_balance_negative_signed_bridge_elimination_add = (((n) + (m))) + ge_balance_positive_signed_bridge_elimination_add)))

gaussian_signed_balance_same_code · checked inherited prerequisite

Exact statement in the checked dependency cone

forall code p n q m. (exists ge_balance_positive_same_code_first ge_balance_negative_same_code_first. (((((code) = 2 * (ge_balance_positive_same_code_first) /\ (ge_balance_negative_same_code_first) = 0) \/ exists ge_signed_half_same_code_firstdecode. (((code) = 2 * ge_signed_half_same_code_firstdecode + 1 /\ (ge_balance_positive_same_code_first) = 0) /\ (ge_balance_negative_same_code_first) = S ge_signed_half_same_code_firstdecode))) /\ ((p) + ge_balance_negative_same_code_first = (n) + ge_balance_positive_same_code_first))) -> (exists ge_balance_positive_same_code_second ge_balance_negative_same_code_second. (((((code) = 2 * (ge_balance_positive_same_code_second) /\ (ge_balance_negative_same_code_second) = 0) \/ exists ge_signed_half_same_code_seconddecode. (((code) = 2 * ge_signed_half_same_code_seconddecode + 1 /\ (ge_balance_positive_same_code_second) = 0) /\ (ge_balance_negative_same_code_second) = S ge_signed_half_same_code_seconddecode))) /\ ((q) + ge_balance_negative_same_code_second = (m) + ge_balance_positive_same_code_second))) -> (((p) + (m)) = ((q) + (n)))

le_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= n
```

matrix_integer_signed_sum_balance · checked inherited prerequisite

Exact statement in the checked dependency cone

forall ab ac bb bc eb ec fb fc l p n P N. (forall ics_index_sum_pointwise ics_value0_sum_pointwise ics_value1_sum_pointwise ics_value2_sum_pointwise ics_value3_sum_pointwise. (exists ics_gap_sum_pointwise_bound. ics_gap_sum_pointwise_bound + S (ics_index_sum_pointwise) = (l)) -> (((exists fs_h_ics_sum_pointwise_at0. fs_h_ics_sum_pointwise_at0 + S (ics_value0_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * ac)) /\ exists fs_q_ics_sum_pointwise_at0. ab = fs_q_ics_sum_pointwise_at0 * S ((S (ics_index_sum_pointwise)) * ac) + (ics_value0_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at1. fs_h_ics_sum_pointwise_at1 + S (ics_value1_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * bc)) /\ exists fs_q_ics_sum_pointwise_at1. bb = fs_q_ics_sum_pointwise_at1 * S ((S (ics_index_sum_pointwise)) * bc) + (ics_value1_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at2. fs_h_ics_sum_pointwise_at2 + S (ics_value2_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * ec)) /\ exists fs_q_ics_sum_pointwise_at2. eb = fs_q_ics_sum_pointwise_at2 * S ((S (ics_index_sum_pointwise)) * ec) + (ics_value2_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at3. fs_h_ics_sum_pointwise_at3 + S (ics_value3_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * fc)) /\ exists fs_q_ics_sum_pointwise_at3. fb = fs_q_ics_sum_pointwise_at3 * S ((S (ics_index_sum_pointwise)) * fc) + (ics_value3_sum_pointwise))) -> ics_value0_sum_pointwise + ics_value3_sum_pointwise = ics_value2_sum_pointwise + ics_value1_sum_pointwise) -> (exists ff_u_mce_integer_sum_ap ff_v_mce_integer_sum_ap. ((((exists ff_h_mce_integer_sum_ap_start. ff_h_mce_integer_sum_ap_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_start. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_start * S ((S (0)) * ff_v_mce_integer_sum_ap) + (0))) /\ ((((exists ff_h_mce_integer_sum_ap_terminal. ff_h_mce_integer_sum_ap_terminal + S (p) = S ((S (l)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_terminal. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_terminal * S ((S (l)) * ff_v_mce_integer_sum_ap) + (p))) /\ forall ff_i_mce_integer_sum_ap. (exists ff_lt_mce_integer_sum_ap_bound. ff_lt_mce_integer_sum_ap_bound + S ff_i_mce_integer_sum_ap = l) -> exists ff_a_mce_integer_sum_ap ff_r_mce_integer_sum_ap ff_s_mce_integer_sum_ap. ((((exists ff_h_mce_integer_sum_ap_summand. ff_h_mce_integer_sum_ap_summand + S (ff_a_mce_integer_sum_ap) = S ((S (ff_i_mce_integer_sum_ap)) * ac)) /\ exists ff_q_mce_integer_sum_ap_summand. ab = ff_q_mce_integer_sum_ap_summand * S ((S (ff_i_mce_integer_sum_ap)) * ac) + (ff_a_mce_integer_sum_ap))) /\ ((((exists ff_h_mce_integer_sum_ap_partial. ff_h_mce_integer_sum_ap_partial + S (ff_r_mce_integer_sum_ap) = S ((S (ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_partial. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_partial * S ((S (ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap) + (ff_r_mce_integer_sum_ap))) /\ ((((exists ff_h_mce_integer_sum_ap_successor. ff_h_mce_integer_sum_ap_successor + S (ff_s_mce_integer_sum_ap) = S ((S (S ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_successor. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_successor * S ((S (S ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap) + (ff_s_mce_integer_sum_ap))) /\ ff_s_mce_integer_sum_ap = ff_r_mce_integer_sum_ap + ff_a_mce_integer_sum_ap)))))) -> (exists ff_u_mce_integer_sum_an ff_v_mce_integer_sum_an. ((((exists ff_h_mce_integer_sum_an_start. ff_h_mce_integer_sum_an_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_start. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_start * S ((S (0)) * ff_v_mce_integer_sum_an) + (0))) /\ ((((exists ff_h_mce_integer_sum_an_terminal. ff_h_mce_integer_sum_an_terminal + S (n) = S ((S (l)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_terminal. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_terminal * S ((S (l)) * ff_v_mce_integer_sum_an) + (n))) /\ forall ff_i_mce_integer_sum_an. (exists ff_lt_mce_integer_sum_an_bound. ff_lt_mce_integer_sum_an_bound + S ff_i_mce_integer_sum_an = l) -> exists ff_a_mce_integer_sum_an ff_r_mce_integer_sum_an ff_s_mce_integer_sum_an. ((((exists ff_h_mce_integer_sum_an_summand. ff_h_mce_integer_sum_an_summand + S (ff_a_mce_integer_sum_an) = S ((S (ff_i_mce_integer_sum_an)) * bc)) /\ exists ff_q_mce_integer_sum_an_summand. bb = ff_q_mce_integer_sum_an_summand * S ((S (ff_i_mce_integer_sum_an)) * bc) + (ff_a_mce_integer_sum_an))) /\ ((((exists ff_h_mce_integer_sum_an_partial. ff_h_mce_integer_sum_an_partial + S (ff_r_mce_integer_sum_an) = S ((S (ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_partial. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_partial * S ((S (ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an) + (ff_r_mce_integer_sum_an))) /\ ((((exists ff_h_mce_integer_sum_an_successor. ff_h_mce_integer_sum_an_successor + S (ff_s_mce_integer_sum_an) = S ((S (S ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_successor. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_successor * S ((S (S ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an) + (ff_s_mce_integer_sum_an))) /\ ff_s_mce_integer_sum_an = ff_r_mce_integer_sum_an + ff_a_mce_integer_sum_an)))))) -> (exists ff_u_mce_integer_sum_bp ff_v_mce_integer_sum_bp. ((((exists ff_h_mce_integer_sum_bp_start. ff_h_mce_integer_sum_bp_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_start. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_start * S ((S (0)) * ff_v_mce_integer_sum_bp) + (0))) /\ ((((exists ff_h_mce_integer_sum_bp_terminal. ff_h_mce_integer_sum_bp_terminal + S (P) = S ((S (l)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_terminal. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_terminal * S ((S (l)) * ff_v_mce_integer_sum_bp) + (P))) /\ forall ff_i_mce_integer_sum_bp. (exists ff_lt_mce_integer_sum_bp_bound. ff_lt_mce_integer_sum_bp_bound + S ff_i_mce_integer_sum_bp = l) -> exists ff_a_mce_integer_sum_bp ff_r_mce_integer_sum_bp ff_s_mce_integer_sum_bp. ((((exists ff_h_mce_integer_sum_bp_summand. ff_h_mce_integer_sum_bp_summand + S (ff_a_mce_integer_sum_bp) = S ((S (ff_i_mce_integer_sum_bp)) * ec)) /\ exists ff_q_mce_integer_sum_bp_summand. eb = ff_q_mce_integer_sum_bp_summand * S ((S (ff_i_mce_integer_sum_bp)) * ec) + (ff_a_mce_integer_sum_bp))) /\ ((((exists ff_h_mce_integer_sum_bp_partial. ff_h_mce_integer_sum_bp_partial + S (ff_r_mce_integer_sum_bp) = S ((S (ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_partial. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_partial * S ((S (ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp) + (ff_r_mce_integer_sum_bp))) /\ ((((exists ff_h_mce_integer_sum_bp_successor. ff_h_mce_integer_sum_bp_successor + S (ff_s_mce_integer_sum_bp) = S ((S (S ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_successor. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_successor * S ((S (S ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp) + (ff_s_mce_integer_sum_bp))) /\ ff_s_mce_integer_sum_bp = ff_r_mce_integer_sum_bp + ff_a_mce_integer_sum_bp)))))) -> (exists ff_u_mce_integer_sum_bn ff_v_mce_integer_sum_bn. ((((exists ff_h_mce_integer_sum_bn_start. ff_h_mce_integer_sum_bn_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_start. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_start * S ((S (0)) * ff_v_mce_integer_sum_bn) + (0))) /\ ((((exists ff_h_mce_integer_sum_bn_terminal. ff_h_mce_integer_sum_bn_terminal + S (N) = S ((S (l)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_terminal. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_terminal * S ((S (l)) * ff_v_mce_integer_sum_bn) + (N))) /\ forall ff_i_mce_integer_sum_bn. (exists ff_lt_mce_integer_sum_bn_bound. ff_lt_mce_integer_sum_bn_bound + S ff_i_mce_integer_sum_bn = l) -> exists ff_a_mce_integer_sum_bn ff_r_mce_integer_sum_bn ff_s_mce_integer_sum_bn. ((((exists ff_h_mce_integer_sum_bn_summand. ff_h_mce_integer_sum_bn_summand + S (ff_a_mce_integer_sum_bn) = S ((S (ff_i_mce_integer_sum_bn)) * fc)) /\ exists ff_q_mce_integer_sum_bn_summand. fb = ff_q_mce_integer_sum_bn_summand * S ((S (ff_i_mce_integer_sum_bn)) * fc) + (ff_a_mce_integer_sum_bn))) /\ ((((exists ff_h_mce_integer_sum_bn_partial. ff_h_mce_integer_sum_bn_partial + S (ff_r_mce_integer_sum_bn) = S ((S (ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_partial. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_partial * S ((S (ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn) + (ff_r_mce_integer_sum_bn))) /\ ((((exists ff_h_mce_integer_sum_bn_successor. ff_h_mce_integer_sum_bn_successor + S (ff_s_mce_integer_sum_bn) = S ((S (S ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_successor. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_successor * S ((S (S ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn) + (ff_s_mce_integer_sum_bn))) /\ ff_s_mce_integer_sum_bn = ff_r_mce_integer_sum_bn + ff_a_mce_integer_sum_bn)))))) -> p + N = P + n

matrix_minor_four_code_components_injective · checked inherited prerequisite

Exact statement in the checked dependency cone

forall z up us un ut vp vs vn vt. z = ((((up) + (us)) * S ((up) + (us)) + ((us) + (us))) + (((un) + (ut)) * S ((un) + (ut)) + ((ut) + (ut)))) * S ((((up) + (us)) * S ((up) + (us)) + ((us) + (us))) + (((un) + (ut)) * S ((un) + (ut)) + ((ut) + (ut)))) + ((((un) + (ut)) * S ((un) + (ut)) + ((ut) + (ut))) + (((un) + (ut)) * S ((un) + (ut)) + ((ut) + (ut)))) -> z = ((((vp) + (vs)) * S ((vp) + (vs)) + ((vs) + (vs))) + (((vn) + (vt)) * S ((vn) + (vt)) + ((vt) + (vt)))) * S ((((vp) + (vs)) * S ((vp) + (vs)) + ((vs) + (vs))) + (((vn) + (vt)) * S ((vn) + (vt)) + ((vt) + (vt)))) + ((((vn) + (vt)) * S ((vn) + (vt)) + ((vt) + (vt))) + (((vn) + (vt)) * S ((vn) + (vt)) + ((vt) + (vt)))) -> (up = vp /\ (us = vs /\ (un = vn /\ ut = vt)))

signed_balance_extensional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall code1 code2 left1 right1 left2 right2. (exists sb_pos_ext_left sb_neg_ext_left. (((code1 = 2 * sb_pos_ext_left /\ sb_neg_ext_left = 0) \/ exists sd_half_ext_left. ((code1 = 2 * sd_half_ext_left + 1 /\ sb_pos_ext_left = 0) /\ sb_neg_ext_left = S sd_half_ext_left)) /\ left1 + sb_neg_ext_left = right1 + sb_pos_ext_left)) -> (exists sb_pos_ext_right sb_neg_ext_right. (((code2 = 2 * sb_pos_ext_right /\ sb_neg_ext_right = 0) \/ exists sd_half_ext_right. ((code2 = 2 * sd_half_ext_right + 1 /\ sb_pos_ext_right = 0) /\ sb_neg_ext_right = S sd_half_ext_right)) /\ left2 + sb_neg_ext_right = right2 + sb_pos_ext_right)) -> left1 + right2 = right1 + left2 -> code1 = code2

signed_balance_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right code1 code2. (exists sb_pos_functional_left sb_neg_functional_left. (((code1 = 2 * sb_pos_functional_left /\ sb_neg_functional_left = 0) \/ exists sd_half_functional_left. ((code1 = 2 * sd_half_functional_left + 1 /\ sb_pos_functional_left = 0) /\ sb_neg_functional_left = S sd_half_functional_left)) /\ left + sb_neg_functional_left = right + sb_pos_functional_left)) -> (exists sb_pos_functional_right sb_neg_functional_right. (((code2 = 2 * sb_pos_functional_right /\ sb_neg_functional_right = 0) \/ exists sd_half_functional_right. ((code2 = 2 * sd_half_functional_right + 1 /\ sb_pos_functional_right = 0) /\ sb_neg_functional_right = S sd_half_functional_right)) /\ left + sb_neg_functional_right = right + sb_pos_functional_right)) -> code1 = code2

signed_balance_total · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right. exists code. (exists sb_pos_total sb_neg_total. (((code = 2 * sb_pos_total /\ sb_neg_total = 0) \/ exists sd_half_total. ((code = 2 * sd_half_total + 1 /\ sb_pos_total = 0) /\ sb_neg_total = S sd_half_total)) /\ left + sb_neg_total = right + sb_pos_total))

signed_balance_zero_iff · checked inherited prerequisite

Exact statement in the checked dependency cone

forall code left right. (exists sb_pos_zero sb_neg_zero. (((code = 2 * sb_pos_zero /\ sb_neg_zero = 0) \/ exists sd_half_zero. ((code = 2 * sd_half_zero + 1 /\ sb_pos_zero = 0) /\ sb_neg_zero = S sd_half_zero)) /\ left + sb_neg_zero = right + sb_pos_zero)) -> ((code = 0 -> left = right) /\ (left = right -> code = 0))

signed_decode_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall code pos1 neg1 pos2 neg2. ((code = 2 * pos1 /\ neg1 = 0) \/ exists sd_half_left. ((code = 2 * sd_half_left + 1 /\ pos1 = 0) /\ neg1 = S sd_half_left)) -> ((code = 2 * pos2 /\ neg2 = 0) \/ exists sd_half_right. ((code = 2 * sd_half_right + 1 /\ pos2 = 0) /\ neg2 = S sd_half_right)) -> pos1 = pos2 /\ neg1 = neg2

signed_negate_to_swapped_decode · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input output pos neg. ((input = 2 * pos /\ neg = 0) \/ exists sd_half_elim_source. ((input = 2 * sd_half_elim_source + 1 /\ pos = 0) /\ neg = S sd_half_elim_source)) -> (exists sn_pos_elim sn_neg_elim. (((input = 2 * sn_pos_elim /\ sn_neg_elim = 0) \/ exists sd_half_elim_input. ((input = 2 * sd_half_elim_input + 1 /\ sn_pos_elim = 0) /\ sn_neg_elim = S sd_half_elim_input)) /\ ((output = 2 * sn_neg_elim /\ sn_pos_elim = 0) \/ exists sd_half_elim_output. ((output = 2 * sd_half_elim_output + 1 /\ sn_neg_elim = 0) /\ sn_pos_elim = S sd_half_elim_output)))) -> ((output = 2 * neg /\ pos = 0) \/ exists sd_half_elim_target. ((output = 2 * sd_half_elim_target + 1 /\ neg = 0) /\ pos = S sd_half_elim_target))

signed_negate_total · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input. exists output. (exists sn_pos_total sn_neg_total. (((input = 2 * sn_pos_total /\ sn_neg_total = 0) \/ exists sd_half_total_input. ((input = 2 * sd_half_total_input + 1 /\ sn_pos_total = 0) /\ sn_neg_total = S sd_half_total_input)) /\ ((output = 2 * sn_neg_total /\ sn_pos_total = 0) \/ exists sd_half_total_output. ((output = 2 * sd_half_total_output + 1 /\ sn_neg_total = 0) /\ sn_pos_total = S sd_half_total_output))))