SS0017

divisor_signed_sum_successor_decompose

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every successor signed sum supplies real predecessor and last-entry codes whose original SignedAdd graph gives its result.

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

Exact expanded first-order arithmetic statement

forall F l z. (exists dst_positive_code_decomp_sum dst_positive_scale_decomp_sum dst_negative_code_decomp_sum dst_negative_scale_decomp_sum dst_positive_sum_decomp_sum dst_negative_sum_decomp_sum. (((F) = (((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) * S ((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) + ((((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))))) /\ (((exists fs_u_dst_decomp_sumpositive fs_v_dst_decomp_sumpositive. ((((exists fs_h_dst_decomp_sumpositive_body_start. fs_h_dst_decomp_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_start. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_start * S ((S (0)) * fs_v_dst_decomp_sumpositive) + (0))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_terminal. fs_h_dst_decomp_sumpositive_body_terminal + S (dst_positive_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_terminal. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumpositive) + (dst_positive_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumpositive_body_steps. (exists fs_lt_dst_decomp_sumpositive_body_steps_bound. fs_lt_dst_decomp_sumpositive_body_steps_bound + S fs_i_dst_decomp_sumpositive_body_steps = S l) -> exists fs_a_dst_decomp_sumpositive_body_steps fs_r_dst_decomp_sumpositive_body_steps fs_s_dst_decomp_sumpositive_body_steps. ((((exists fs_h_dst_decomp_sumpositive_body_steps_summand. fs_h_dst_decomp_sumpositive_body_steps_summand + S (fs_a_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_summand. dst_positive_code_decomp_sum = fs_q_dst_decomp_sumpositive_body_steps_summand * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum) + (fs_a_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_partial. fs_h_dst_decomp_sumpositive_body_steps_partial + S (fs_r_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_partial. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_partial * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_r_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_successor. fs_h_dst_decomp_sumpositive_body_steps_successor + S (fs_s_dst_decomp_sumpositive_body_steps) = S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_successor. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_s_dst_decomp_sumpositive_body_steps))) /\ fs_s_dst_decomp_sumpositive_body_steps = fs_r_dst_decomp_sumpositive_body_steps + fs_a_dst_decomp_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_sumnegative fs_v_dst_decomp_sumnegative. ((((exists fs_h_dst_decomp_sumnegative_body_start. fs_h_dst_decomp_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_start. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_start * S ((S (0)) * fs_v_dst_decomp_sumnegative) + (0))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_terminal. fs_h_dst_decomp_sumnegative_body_terminal + S (dst_negative_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_terminal. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumnegative) + (dst_negative_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumnegative_body_steps. (exists fs_lt_dst_decomp_sumnegative_body_steps_bound. fs_lt_dst_decomp_sumnegative_body_steps_bound + S fs_i_dst_decomp_sumnegative_body_steps = S l) -> exists fs_a_dst_decomp_sumnegative_body_steps fs_r_dst_decomp_sumnegative_body_steps fs_s_dst_decomp_sumnegative_body_steps. ((((exists fs_h_dst_decomp_sumnegative_body_steps_summand. fs_h_dst_decomp_sumnegative_body_steps_summand + S (fs_a_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_summand. dst_negative_code_decomp_sum = fs_q_dst_decomp_sumnegative_body_steps_summand * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum) + (fs_a_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_partial. fs_h_dst_decomp_sumnegative_body_steps_partial + S (fs_r_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_partial. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_partial * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_r_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_successor. fs_h_dst_decomp_sumnegative_body_steps_successor + S (fs_s_dst_decomp_sumnegative_body_steps) = S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_successor. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_s_dst_decomp_sumnegative_body_steps))) /\ fs_s_dst_decomp_sumnegative_body_steps = fs_r_dst_decomp_sumnegative_body_steps + fs_a_dst_decomp_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_sumresult ge_balance_negative_decomp_sumresult. (((((z) = 2 * (ge_balance_positive_decomp_sumresult) /\ (ge_balance_negative_decomp_sumresult) = 0) \/ exists ge_signed_half_decomp_sumresultdecode. (((z) = 2 * ge_signed_half_decomp_sumresultdecode + 1 /\ (ge_balance_positive_decomp_sumresult) = 0) /\ (ge_balance_negative_decomp_sumresult) = S ge_signed_half_decomp_sumresultdecode))) /\ ((dst_positive_sum_decomp_sum) + ge_balance_negative_decomp_sumresult = (dst_negative_sum_decomp_sum) + ge_balance_positive_decomp_sumresult))))))))) -> exists a b. ((exists dst_positive_code_decomp_prefix dst_positive_scale_decomp_prefix dst_negative_code_decomp_prefix dst_negative_scale_decomp_prefix dst_positive_sum_decomp_prefix dst_negative_sum_decomp_prefix. (((F) = (((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) * S ((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) + ((((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))))) /\ (((exists fs_u_dst_decomp_prefixpositive fs_v_dst_decomp_prefixpositive. ((((exists fs_h_dst_decomp_prefixpositive_body_start. fs_h_dst_decomp_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_start. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_start * S ((S (0)) * fs_v_dst_decomp_prefixpositive) + (0))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_terminal. fs_h_dst_decomp_prefixpositive_body_terminal + S (dst_positive_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_terminal. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixpositive) + (dst_positive_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixpositive_body_steps. (exists fs_lt_dst_decomp_prefixpositive_body_steps_bound. fs_lt_dst_decomp_prefixpositive_body_steps_bound + S fs_i_dst_decomp_prefixpositive_body_steps = l) -> exists fs_a_dst_decomp_prefixpositive_body_steps fs_r_dst_decomp_prefixpositive_body_steps fs_s_dst_decomp_prefixpositive_body_steps. ((((exists fs_h_dst_decomp_prefixpositive_body_steps_summand. fs_h_dst_decomp_prefixpositive_body_steps_summand + S (fs_a_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_summand. dst_positive_code_decomp_prefix = fs_q_dst_decomp_prefixpositive_body_steps_summand * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix) + (fs_a_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_partial. fs_h_dst_decomp_prefixpositive_body_steps_partial + S (fs_r_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_partial. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_partial * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_r_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_successor. fs_h_dst_decomp_prefixpositive_body_steps_successor + S (fs_s_dst_decomp_prefixpositive_body_steps) = S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_successor. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_s_dst_decomp_prefixpositive_body_steps))) /\ fs_s_dst_decomp_prefixpositive_body_steps = fs_r_dst_decomp_prefixpositive_body_steps + fs_a_dst_decomp_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_prefixnegative fs_v_dst_decomp_prefixnegative. ((((exists fs_h_dst_decomp_prefixnegative_body_start. fs_h_dst_decomp_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_start. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_start * S ((S (0)) * fs_v_dst_decomp_prefixnegative) + (0))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_terminal. fs_h_dst_decomp_prefixnegative_body_terminal + S (dst_negative_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_terminal. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixnegative) + (dst_negative_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixnegative_body_steps. (exists fs_lt_dst_decomp_prefixnegative_body_steps_bound. fs_lt_dst_decomp_prefixnegative_body_steps_bound + S fs_i_dst_decomp_prefixnegative_body_steps = l) -> exists fs_a_dst_decomp_prefixnegative_body_steps fs_r_dst_decomp_prefixnegative_body_steps fs_s_dst_decomp_prefixnegative_body_steps. ((((exists fs_h_dst_decomp_prefixnegative_body_steps_summand. fs_h_dst_decomp_prefixnegative_body_steps_summand + S (fs_a_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_summand. dst_negative_code_decomp_prefix = fs_q_dst_decomp_prefixnegative_body_steps_summand * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix) + (fs_a_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_partial. fs_h_dst_decomp_prefixnegative_body_steps_partial + S (fs_r_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_partial. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_partial * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_r_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_successor. fs_h_dst_decomp_prefixnegative_body_steps_successor + S (fs_s_dst_decomp_prefixnegative_body_steps) = S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_successor. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_s_dst_decomp_prefixnegative_body_steps))) /\ fs_s_dst_decomp_prefixnegative_body_steps = fs_r_dst_decomp_prefixnegative_body_steps + fs_a_dst_decomp_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_prefixresult ge_balance_negative_decomp_prefixresult. (((((a) = 2 * (ge_balance_positive_decomp_prefixresult) /\ (ge_balance_negative_decomp_prefixresult) = 0) \/ exists ge_signed_half_decomp_prefixresultdecode. (((a) = 2 * ge_signed_half_decomp_prefixresultdecode + 1 /\ (ge_balance_positive_decomp_prefixresult) = 0) /\ (ge_balance_negative_decomp_prefixresult) = S ge_signed_half_decomp_prefixresultdecode))) /\ ((dst_positive_sum_decomp_prefix) + ge_balance_negative_decomp_prefixresult = (dst_negative_sum_decomp_prefix) + ge_balance_positive_decomp_prefixresult))))))))) /\ (((exists dst_positive_code_decomp_entry dst_positive_scale_decomp_entry dst_negative_code_decomp_entry dst_negative_scale_decomp_entry dst_positive_decomp_entry dst_negative_decomp_entry. (((F) = (((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) * S ((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) + ((((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))))) /\ (((((exists ff_h_pvs_decomp_entrypositive. ff_h_pvs_decomp_entrypositive + S (dst_positive_decomp_entry) = S ((S (l)) * dst_positive_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrypositive. dst_positive_code_decomp_entry = ff_q_pvs_decomp_entrypositive * S ((S (l)) * dst_positive_scale_decomp_entry) + (dst_positive_decomp_entry))) /\ (((((exists ff_h_pvs_decomp_entrynegative. ff_h_pvs_decomp_entrynegative + S (dst_negative_decomp_entry) = S ((S (l)) * dst_negative_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrynegative. dst_negative_code_decomp_entry = ff_q_pvs_decomp_entrynegative * S ((S (l)) * dst_negative_scale_decomp_entry) + (dst_negative_decomp_entry))) /\ (exists ge_balance_positive_decomp_entryvalue ge_balance_negative_decomp_entryvalue. (((((b) = 2 * (ge_balance_positive_decomp_entryvalue) /\ (ge_balance_negative_decomp_entryvalue) = 0) \/ exists ge_signed_half_decomp_entryvaluedecode. (((b) = 2 * ge_signed_half_decomp_entryvaluedecode + 1 /\ (ge_balance_positive_decomp_entryvalue) = 0) /\ (ge_balance_negative_decomp_entryvalue) = S ge_signed_half_decomp_entryvaluedecode))) /\ ((dst_positive_decomp_entry) + ge_balance_negative_decomp_entryvalue = (dst_negative_decomp_entry) + ge_balance_positive_decomp_entryvalue))))))))) /\ (exists dsa_ap_decomp_add dsa_an_decomp_add dsa_bp_decomp_add dsa_bn_decomp_add dsa_cp_decomp_add dsa_cn_decomp_add. (((((a) = 2 * (dsa_ap_decomp_add) /\ (dsa_an_decomp_add) = 0) \/ exists ge_signed_half_decomp_addleft. (((a) = 2 * ge_signed_half_decomp_addleft + 1 /\ (dsa_ap_decomp_add) = 0) /\ (dsa_an_decomp_add) = S ge_signed_half_decomp_addleft))) /\ ((((((b) = 2 * (dsa_bp_decomp_add) /\ (dsa_bn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addright. (((b) = 2 * ge_signed_half_decomp_addright + 1 /\ (dsa_bp_decomp_add) = 0) /\ (dsa_bn_decomp_add) = S ge_signed_half_decomp_addright))) /\ ((((((z) = 2 * (dsa_cp_decomp_add) /\ (dsa_cn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addoutput. (((z) = 2 * ge_signed_half_decomp_addoutput + 1 /\ (dsa_cp_decomp_add) = 0) /\ (dsa_cn_decomp_add) = S ge_signed_half_decomp_addoutput))) /\ ((dsa_ap_decomp_add + dsa_bp_decomp_add) + dsa_cn_decomp_add = (dsa_an_decomp_add + dsa_bn_decomp_add) + dsa_cp_decomp_add))))))))))

Constructive proof overview

Generated structural guide

Every successor signed sum supplies real predecessor and last-entry codes whose original SignedAdd graph gives its result.

The unchanged tactic script uses 5 declared prerequisites and contains 90 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_sum_succ_decompose Stable theorem; checked-use authorized signed_balance_total Alpha theorem; checked-use authorized SS0009 divisor_signed_sum_from_components SS0001 divisor_signed_table_at_from_components gaussian_signed_add_of_balances Alpha theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

90 script commands · 20 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
divisor signed sum from componentsdivisor signed table at from components

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro z
  4. L4
    intro hs
02Separate the logical casesL5–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L5
    cases hs
  2. L6
    cases hs_witness
  3. L7
    cases hs_witness_witness
  4. L8
    cases hs_witness_witness_witness
  5. L9
    cases hs_witness_witness_witness_witness
  6. L10
    cases hs_witness_witness_witness_witness_witness
  7. L11
    cases hs_witness_witness_witness_witness_witness_witness
  8. L12
    cases hs_witness_witness_witness_witness_witness_witness_right
  9. L13
    cases hs_witness_witness_witness_witness_witness_witness_right_right
03Establish hpL14–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L14
    have hp : ∃ dsa_summand_decomp_positive. ∃ dsa_partial_decomp_positive. BetaAt(x,x1,l,dsa_summand_decomp_positive) ∧ (Sum(x,x1,l,dsa_partial_decomp_positive) ∧ x4 = dsa_partial_decomp_positive + dsa_summand_decomp_positive)Definitions: BetaAtSum
  2. L15
    specialize beta_sum_succ_decompose (x)
  3. L16
    specialize beta_sum_succ_decompose (x1)
  4. L17
    specialize beta_sum_succ_decompose (l)
  5. L18
    specialize beta_sum_succ_decompose (x4)
  6. L19
    apply beta_sum_succ_decompose
  7. L20
    exact hs_witness_witness_witness_witness_witness_witness_right_left
04Separate the logical casesL21–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hp
  2. L22
    cases hp_witness
  3. L23
    cases hp_witness_witness
  4. L24
    cases hp_witness_witness_right
05Establish hnL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L25
    have hn : ∃ dsa_summand_decomp_negative. ∃ dsa_partial_decomp_negative. BetaAt(x2,x3,l,dsa_summand_decomp_negative) ∧ (Sum(x2,x3,l,dsa_partial_decomp_negative) ∧ x5 = dsa_partial_decomp_negative + dsa_summand_decomp_negative)Definitions: BetaAtSum
  2. L26
    specialize beta_sum_succ_decompose (x2)
  3. L27
    specialize beta_sum_succ_decompose (x3)
  4. L28
    specialize beta_sum_succ_decompose (l)
  5. L29
    specialize beta_sum_succ_decompose (x5)
  6. L30
    apply beta_sum_succ_decompose
  7. L31
    exact hs_witness_witness_witness_witness_witness_witness_right_right_left
06Separate the logical casesL32–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    cases hn
  2. L33
    cases hn_witness
  3. L34
    cases hn_witness_witness
  4. L35
    cases hn_witness_witness_right
07Establish haL36–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L36
    have ha : exists a. (exists ge_balance_positive_decomp_prefix_code ge_balance_negative_decomp_prefix_code. (((((a) = 2 * (ge_balance_positive_decomp_prefix_code) /\ (ge_balance_negative_decomp_prefix_code) = 0) \/ exists ge_signed_half_decomp_prefix_codedecode. (((a) = 2 * ge_signed_half_decomp_prefix_codedecode + 1 /\ (ge_balance_positive_decomp_prefix_code) = 0) /\ (ge_balance_negative_decomp_prefix_code) = S ge_signed_half_decomp_prefix_codedecode))) /\ ((x7) + ge_balance_negative_decomp_prefix_code = (x9) + ge_balance_positive_decomp_prefix_code)))
  2. L37
    specialize signed_balance_total (x7)
  3. L38
    specialize signed_balance_total (x9)
  4. L39
    apply signed_balance_total
08Separate the logical casesL40–40

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L40
    cases ha
09Establish hbL41–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L41
    have hb : exists b. (exists ge_balance_positive_decomp_entry_code ge_balance_negative_decomp_entry_code. (((((b) = 2 * (ge_balance_positive_decomp_entry_code) /\ (ge_balance_negative_decomp_entry_code) = 0) \/ exists ge_signed_half_decomp_entry_codedecode. (((b) = 2 * ge_signed_half_decomp_entry_codedecode + 1 /\ (ge_balance_positive_decomp_entry_code) = 0) /\ (ge_balance_negative_decomp_entry_code) = S ge_signed_half_decomp_entry_codedecode))) /\ ((x6) + ge_balance_negative_decomp_entry_code = (x8) + ge_balance_positive_decomp_entry_code)))
  2. L42
    specialize signed_balance_total (x6)
  3. L43
    specialize signed_balance_total (x8)
  4. L44
    apply signed_balance_total
10Separate the logical casesL45–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    cases hb
11Construct an explicit witnessL46–47

Supply the displayed value, then prove that it has the required property.

  1. L46
    exists x10
  2. L47
    exists x11
12Separate the logical casesL48–48

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L48
    split
13Use earlier factsL49–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize divisor_signed_sum_from_components (F)
  2. L50
    specialize divisor_signed_sum_from_components (x)
  3. L51
    specialize divisor_signed_sum_from_components (x1)
  4. L52
    specialize divisor_signed_sum_from_components (x2)
  5. L53
    specialize divisor_signed_sum_from_components (x3)
  6. L54
    specialize divisor_signed_sum_from_components (l)
  7. L55
    specialize divisor_signed_sum_from_components (x7)
  8. L56
    specialize divisor_signed_sum_from_components (x9)
  9. L57
    specialize divisor_signed_sum_from_components (x10)
  10. L58
    apply divisor_signed_sum_from_components
14Use earlier factsL59–62

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    exact hs_witness_witness_witness_witness_witness_witness_left
  2. L60
    exact hp_witness_witness_right_left
  3. L61
    exact hn_witness_witness_right_left
  4. L62
    exact ha_witness
15Separate the logical casesL63–63

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L63
    split
16Use earlier factsL64–73

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    specialize divisor_signed_table_at_from_components (F)
  2. L65
    specialize divisor_signed_table_at_from_components (x)
  3. L66
    specialize divisor_signed_table_at_from_components (x1)
  4. L67
    specialize divisor_signed_table_at_from_components (x2)
  5. L68
    specialize divisor_signed_table_at_from_components (x3)
  6. L69
    specialize divisor_signed_table_at_from_components (l)
  7. L70
    specialize divisor_signed_table_at_from_components (x6)
  8. L71
    specialize divisor_signed_table_at_from_components (x8)
  9. L72
    specialize divisor_signed_table_at_from_components (x11)
  10. L73
    apply divisor_signed_table_at_from_components
17Use earlier factsL74–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L74
    exact hs_witness_witness_witness_witness_witness_witness_left
  2. L75
    exact hp_witness_witness_left
  3. L76
    exact hn_witness_witness_left
  4. L77
    exact hb_witness
  5. L78
    specialize gaussian_signed_add_of_balances (x10)
  6. L79
    specialize gaussian_signed_add_of_balances (x11)
  7. L80
    specialize gaussian_signed_add_of_balances (z)
  8. L81
    specialize gaussian_signed_add_of_balances (x7)
  9. L82
    specialize gaussian_signed_add_of_balances (x9)
  10. L83
    specialize gaussian_signed_add_of_balances (x6)
18Use earlier factsL84–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L84
    specialize gaussian_signed_add_of_balances (x8)
  2. L85
    apply gaussian_signed_add_of_balances
  3. L86
    exact ha_witness
  4. L87
    exact hb_witness
19Calculate and transport equalitiesL88–89

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L88
    rewrite hp_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  2. L89
    rewrite hn_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
20Use earlier factsL90–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L90
    exact hs_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 90 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro z
  4. 0004intro hs
  5. 0005cases hs
  6. 0006cases hs_witness
  7. 0007cases hs_witness_witness
  8. 0008cases hs_witness_witness_witness
  9. 0009cases hs_witness_witness_witness_witness
  10. 0010cases hs_witness_witness_witness_witness_witness
  11. 0011cases hs_witness_witness_witness_witness_witness_witness
  12. 0012cases hs_witness_witness_witness_witness_witness_witness_right
  13. 0013cases hs_witness_witness_witness_witness_witness_witness_right_right
  14. 0014have hp : exists dsa_summand_decomp_positive dsa_partial_decomp_positive. ((((exists ff_h_pvs_decomp_positivelast. ff_h_pvs_decomp_positivelast + S (dsa_summand_decomp_positive) = S ((S (l)) * x1)) /\ exists ff_q_pvs_decomp_positivelast. x = ff_q_pvs_decomp_positivelast * S ((S (l)) * x1) + (dsa_summand_decomp_positive))) /\ (((exists fs_u_dst_decomp_positiveprefix fs_v_dst_decomp_positiveprefix. ((((exists fs_h_dst_decomp_positiveprefix_body_start. fs_h_dst_decomp_positiveprefix_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_positiveprefix)) /\ exists fs_q_dst_decomp_positiveprefix_body_start. fs_u_dst_decomp_positiveprefix = fs_q_dst_decomp_positiveprefix_body_start * S ((S (0)) * fs_v_dst_decomp_positiveprefix) + (0))) /\ ((((exists fs_h_dst_decomp_positiveprefix_body_terminal. fs_h_dst_decomp_positiveprefix_body_terminal + S (dsa_partial_decomp_positive) = S ((S (l)) * fs_v_dst_decomp_positiveprefix)) /\ exists fs_q_dst_decomp_positiveprefix_body_terminal. fs_u_dst_decomp_positiveprefix = fs_q_dst_decomp_positiveprefix_body_terminal * S ((S (l)) * fs_v_dst_decomp_positiveprefix) + (dsa_partial_decomp_positive))) /\ forall fs_i_dst_decomp_positiveprefix_body_steps. (exists fs_lt_dst_decomp_positiveprefix_body_steps_bound. fs_lt_dst_decomp_positiveprefix_body_steps_bound + S fs_i_dst_decomp_positiveprefix_body_steps = l) -> exists fs_a_dst_decomp_positiveprefix_body_steps fs_r_dst_decomp_positiveprefix_body_steps fs_s_dst_decomp_positiveprefix_body_steps. ((((exists fs_h_dst_decomp_positiveprefix_body_steps_summand. fs_h_dst_decomp_positiveprefix_body_steps_summand + S (fs_a_dst_decomp_positiveprefix_body_steps) = S ((S (fs_i_dst_decomp_positiveprefix_body_steps)) * x1)) /\ exists fs_q_dst_decomp_positiveprefix_body_steps_summand. x = fs_q_dst_decomp_positiveprefix_body_steps_summand * S ((S (fs_i_dst_decomp_positiveprefix_body_steps)) * x1) + (fs_a_dst_decomp_positiveprefix_body_steps))) /\ ((((exists fs_h_dst_decomp_positiveprefix_body_steps_partial. fs_h_dst_decomp_positiveprefix_body_steps_partial + S (fs_r_dst_decomp_positiveprefix_body_steps) = S ((S (fs_i_dst_decomp_positiveprefix_body_steps)) * fs_v_dst_decomp_positiveprefix)) /\ exists fs_q_dst_decomp_positiveprefix_body_steps_partial. fs_u_dst_decomp_positiveprefix = fs_q_dst_decomp_positiveprefix_body_steps_partial * S ((S (fs_i_dst_decomp_positiveprefix_body_steps)) * fs_v_dst_decomp_positiveprefix) + (fs_r_dst_decomp_positiveprefix_body_steps))) /\ ((((exists fs_h_dst_decomp_positiveprefix_body_steps_successor. fs_h_dst_decomp_positiveprefix_body_steps_successor + S (fs_s_dst_decomp_positiveprefix_body_steps) = S ((S (S fs_i_dst_decomp_positiveprefix_body_steps)) * fs_v_dst_decomp_positiveprefix)) /\ exists fs_q_dst_decomp_positiveprefix_body_steps_successor. fs_u_dst_decomp_positiveprefix = fs_q_dst_decomp_positiveprefix_body_steps_successor * S ((S (S fs_i_dst_decomp_positiveprefix_body_steps)) * fs_v_dst_decomp_positiveprefix) + (fs_s_dst_decomp_positiveprefix_body_steps))) /\ fs_s_dst_decomp_positiveprefix_body_steps = fs_r_dst_decomp_positiveprefix_body_steps + fs_a_dst_decomp_positiveprefix_body_steps)))))) /\ ((x4) = dsa_partial_decomp_positive + dsa_summand_decomp_positive))))
  15. 0015specialize beta_sum_succ_decompose (x)
  16. 0016specialize beta_sum_succ_decompose (x1)
  17. 0017specialize beta_sum_succ_decompose (l)
  18. 0018specialize beta_sum_succ_decompose (x4)
  19. 0019apply beta_sum_succ_decompose
  20. 0020exact hs_witness_witness_witness_witness_witness_witness_right_left
  21. 0021cases hp
  22. 0022cases hp_witness
  23. 0023cases hp_witness_witness
  24. 0024cases hp_witness_witness_right
  25. 0025have hn : exists dsa_summand_decomp_negative dsa_partial_decomp_negative. ((((exists ff_h_pvs_decomp_negativelast. ff_h_pvs_decomp_negativelast + S (dsa_summand_decomp_negative) = S ((S (l)) * x3)) /\ exists ff_q_pvs_decomp_negativelast. x2 = ff_q_pvs_decomp_negativelast * S ((S (l)) * x3) + (dsa_summand_decomp_negative))) /\ (((exists fs_u_dst_decomp_negativeprefix fs_v_dst_decomp_negativeprefix. ((((exists fs_h_dst_decomp_negativeprefix_body_start. fs_h_dst_decomp_negativeprefix_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_negativeprefix)) /\ exists fs_q_dst_decomp_negativeprefix_body_start. fs_u_dst_decomp_negativeprefix = fs_q_dst_decomp_negativeprefix_body_start * S ((S (0)) * fs_v_dst_decomp_negativeprefix) + (0))) /\ ((((exists fs_h_dst_decomp_negativeprefix_body_terminal. fs_h_dst_decomp_negativeprefix_body_terminal + S (dsa_partial_decomp_negative) = S ((S (l)) * fs_v_dst_decomp_negativeprefix)) /\ exists fs_q_dst_decomp_negativeprefix_body_terminal. fs_u_dst_decomp_negativeprefix = fs_q_dst_decomp_negativeprefix_body_terminal * S ((S (l)) * fs_v_dst_decomp_negativeprefix) + (dsa_partial_decomp_negative))) /\ forall fs_i_dst_decomp_negativeprefix_body_steps. (exists fs_lt_dst_decomp_negativeprefix_body_steps_bound. fs_lt_dst_decomp_negativeprefix_body_steps_bound + S fs_i_dst_decomp_negativeprefix_body_steps = l) -> exists fs_a_dst_decomp_negativeprefix_body_steps fs_r_dst_decomp_negativeprefix_body_steps fs_s_dst_decomp_negativeprefix_body_steps. ((((exists fs_h_dst_decomp_negativeprefix_body_steps_summand. fs_h_dst_decomp_negativeprefix_body_steps_summand + S (fs_a_dst_decomp_negativeprefix_body_steps) = S ((S (fs_i_dst_decomp_negativeprefix_body_steps)) * x3)) /\ exists fs_q_dst_decomp_negativeprefix_body_steps_summand. x2 = fs_q_dst_decomp_negativeprefix_body_steps_summand * S ((S (fs_i_dst_decomp_negativeprefix_body_steps)) * x3) + (fs_a_dst_decomp_negativeprefix_body_steps))) /\ ((((exists fs_h_dst_decomp_negativeprefix_body_steps_partial. fs_h_dst_decomp_negativeprefix_body_steps_partial + S (fs_r_dst_decomp_negativeprefix_body_steps) = S ((S (fs_i_dst_decomp_negativeprefix_body_steps)) * fs_v_dst_decomp_negativeprefix)) /\ exists fs_q_dst_decomp_negativeprefix_body_steps_partial. fs_u_dst_decomp_negativeprefix = fs_q_dst_decomp_negativeprefix_body_steps_partial * S ((S (fs_i_dst_decomp_negativeprefix_body_steps)) * fs_v_dst_decomp_negativeprefix) + (fs_r_dst_decomp_negativeprefix_body_steps))) /\ ((((exists fs_h_dst_decomp_negativeprefix_body_steps_successor. fs_h_dst_decomp_negativeprefix_body_steps_successor + S (fs_s_dst_decomp_negativeprefix_body_steps) = S ((S (S fs_i_dst_decomp_negativeprefix_body_steps)) * fs_v_dst_decomp_negativeprefix)) /\ exists fs_q_dst_decomp_negativeprefix_body_steps_successor. fs_u_dst_decomp_negativeprefix = fs_q_dst_decomp_negativeprefix_body_steps_successor * S ((S (S fs_i_dst_decomp_negativeprefix_body_steps)) * fs_v_dst_decomp_negativeprefix) + (fs_s_dst_decomp_negativeprefix_body_steps))) /\ fs_s_dst_decomp_negativeprefix_body_steps = fs_r_dst_decomp_negativeprefix_body_steps + fs_a_dst_decomp_negativeprefix_body_steps)))))) /\ ((x5) = dsa_partial_decomp_negative + dsa_summand_decomp_negative))))
  26. 0026specialize beta_sum_succ_decompose (x2)
  27. 0027specialize beta_sum_succ_decompose (x3)
  28. 0028specialize beta_sum_succ_decompose (l)
  29. 0029specialize beta_sum_succ_decompose (x5)
  30. 0030apply beta_sum_succ_decompose
  31. 0031exact hs_witness_witness_witness_witness_witness_witness_right_right_left
  32. 0032cases hn
  33. 0033cases hn_witness
  34. 0034cases hn_witness_witness
  35. 0035cases hn_witness_witness_right
  36. 0036have ha : exists a. (exists ge_balance_positive_decomp_prefix_code ge_balance_negative_decomp_prefix_code. (((((a) = 2 * (ge_balance_positive_decomp_prefix_code) /\ (ge_balance_negative_decomp_prefix_code) = 0) \/ exists ge_signed_half_decomp_prefix_codedecode. (((a) = 2 * ge_signed_half_decomp_prefix_codedecode + 1 /\ (ge_balance_positive_decomp_prefix_code) = 0) /\ (ge_balance_negative_decomp_prefix_code) = S ge_signed_half_decomp_prefix_codedecode))) /\ ((x7) + ge_balance_negative_decomp_prefix_code = (x9) + ge_balance_positive_decomp_prefix_code)))
  37. 0037specialize signed_balance_total (x7)
  38. 0038specialize signed_balance_total (x9)
  39. 0039apply signed_balance_total
  40. 0040cases ha
  41. 0041have hb : exists b. (exists ge_balance_positive_decomp_entry_code ge_balance_negative_decomp_entry_code. (((((b) = 2 * (ge_balance_positive_decomp_entry_code) /\ (ge_balance_negative_decomp_entry_code) = 0) \/ exists ge_signed_half_decomp_entry_codedecode. (((b) = 2 * ge_signed_half_decomp_entry_codedecode + 1 /\ (ge_balance_positive_decomp_entry_code) = 0) /\ (ge_balance_negative_decomp_entry_code) = S ge_signed_half_decomp_entry_codedecode))) /\ ((x6) + ge_balance_negative_decomp_entry_code = (x8) + ge_balance_positive_decomp_entry_code)))
  42. 0042specialize signed_balance_total (x6)
  43. 0043specialize signed_balance_total (x8)
  44. 0044apply signed_balance_total
  45. 0045cases hb
  46. 0046exists x10
  47. 0047exists x11
  48. 0048split
  49. 0049specialize divisor_signed_sum_from_components (F)
  50. 0050specialize divisor_signed_sum_from_components (x)
  51. 0051specialize divisor_signed_sum_from_components (x1)
  52. 0052specialize divisor_signed_sum_from_components (x2)
  53. 0053specialize divisor_signed_sum_from_components (x3)
  54. 0054specialize divisor_signed_sum_from_components (l)
  55. 0055specialize divisor_signed_sum_from_components (x7)
  56. 0056specialize divisor_signed_sum_from_components (x9)
  57. 0057specialize divisor_signed_sum_from_components (x10)
  58. 0058apply divisor_signed_sum_from_components
  59. 0059exact hs_witness_witness_witness_witness_witness_witness_left
  60. 0060exact hp_witness_witness_right_left
  61. 0061exact hn_witness_witness_right_left
  62. 0062exact ha_witness
  63. 0063split
  64. 0064specialize divisor_signed_table_at_from_components (F)
  65. 0065specialize divisor_signed_table_at_from_components (x)
  66. 0066specialize divisor_signed_table_at_from_components (x1)
  67. 0067specialize divisor_signed_table_at_from_components (x2)
  68. 0068specialize divisor_signed_table_at_from_components (x3)
  69. 0069specialize divisor_signed_table_at_from_components (l)
  70. 0070specialize divisor_signed_table_at_from_components (x6)
  71. 0071specialize divisor_signed_table_at_from_components (x8)
  72. 0072specialize divisor_signed_table_at_from_components (x11)
  73. 0073apply divisor_signed_table_at_from_components
  74. 0074exact hs_witness_witness_witness_witness_witness_witness_left
  75. 0075exact hp_witness_witness_left
  76. 0076exact hn_witness_witness_left
  77. 0077exact hb_witness
  78. 0078specialize gaussian_signed_add_of_balances (x10)
  79. 0079specialize gaussian_signed_add_of_balances (x11)
  80. 0080specialize gaussian_signed_add_of_balances (z)
  81. 0081specialize gaussian_signed_add_of_balances (x7)
  82. 0082specialize gaussian_signed_add_of_balances (x9)
  83. 0083specialize gaussian_signed_add_of_balances (x6)
  84. 0084specialize gaussian_signed_add_of_balances (x8)
  85. 0085apply gaussian_signed_add_of_balances
  86. 0086exact ha_witness
  87. 0087exact hb_witness
  88. 0088rewrite hp_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  89. 0089rewrite hn_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  90. 0090exact hs_witness_witness_witness_witness_witness_witness_right_right_right