SS001E

divisor_signed_sum_permutation_invariant

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

Any actual bounded injective beta permutation preserves the genuine signed sum, even for unrelated positive/negative representations of the pullback table.

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 G r s l u v. (forall pfp_i_permutation_bound. (exists pfp_gap_permutation_boundindex. pfp_gap_permutation_boundindex + S (pfp_i_permutation_bound) = (l)) -> exists pfp_a_permutation_bound. (((exists ff_h_pfp_permutation_boundentry. ff_h_pfp_permutation_boundentry + S (pfp_a_permutation_bound) = S ((S (pfp_i_permutation_bound)) * s)) /\ exists ff_q_pfp_permutation_boundentry. r = ff_q_pfp_permutation_boundentry * S ((S (pfp_i_permutation_bound)) * s) + (pfp_a_permutation_bound))) /\ (exists pfp_gap_permutation_boundvalue. pfp_gap_permutation_boundvalue + S (pfp_a_permutation_bound) = (l))) -> (forall pfp_i_permutation_injective pfp_j_permutation_injective pfp_a_permutation_injective. (exists pfp_gap_permutation_injectivefirst. pfp_gap_permutation_injectivefirst + S (pfp_i_permutation_injective) = (l)) -> (exists pfp_gap_permutation_injectivesecond. pfp_gap_permutation_injectivesecond + S (pfp_j_permutation_injective) = (l)) -> (((exists ff_h_pfp_permutation_injectiveleft. ff_h_pfp_permutation_injectiveleft + S (pfp_a_permutation_injective) = S ((S (pfp_i_permutation_injective)) * s)) /\ exists ff_q_pfp_permutation_injectiveleft. r = ff_q_pfp_permutation_injectiveleft * S ((S (pfp_i_permutation_injective)) * s) + (pfp_a_permutation_injective))) -> (((exists ff_h_pfp_permutation_injectiveright. ff_h_pfp_permutation_injectiveright + S (pfp_a_permutation_injective) = S ((S (pfp_j_permutation_injective)) * s)) /\ exists ff_q_pfp_permutation_injectiveright. r = ff_q_pfp_permutation_injectiveright * S ((S (pfp_j_permutation_injective)) * s) + (pfp_a_permutation_injective))) -> pfp_i_permutation_injective = pfp_j_permutation_injective) -> (forall dsr_index_permutation_pullback dsr_image_permutation_pullback dsr_value_permutation_pullback. (exists pvs_gap_permutation_pullbackbound. pvs_gap_permutation_pullbackbound + S (dsr_index_permutation_pullback) = (l)) -> (((exists ff_h_pvs_permutation_pullbackmap. ff_h_pvs_permutation_pullbackmap + S (dsr_image_permutation_pullback) = S ((S (dsr_index_permutation_pullback)) * s)) /\ exists ff_q_pvs_permutation_pullbackmap. r = ff_q_pvs_permutation_pullbackmap * S ((S (dsr_index_permutation_pullback)) * s) + (dsr_image_permutation_pullback))) -> (exists dst_positive_code_permutation_pullbacksource dst_positive_scale_permutation_pullbacksource dst_negative_code_permutation_pullbacksource dst_negative_scale_permutation_pullbacksource dst_positive_permutation_pullbacksource dst_negative_permutation_pullbacksource. (((F) = (((((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) * S ((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) + ((dst_positive_scale_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))) * S ((((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) * S ((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) + ((dst_positive_scale_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))) + ((((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))))) /\ (((((exists ff_h_pvs_permutation_pullbacksourcepositive. ff_h_pvs_permutation_pullbacksourcepositive + S (dst_positive_permutation_pullbacksource) = S ((S (dsr_image_permutation_pullback)) * dst_positive_scale_permutation_pullbacksource)) /\ exists ff_q_pvs_permutation_pullbacksourcepositive. dst_positive_code_permutation_pullbacksource = ff_q_pvs_permutation_pullbacksourcepositive * S ((S (dsr_image_permutation_pullback)) * dst_positive_scale_permutation_pullbacksource) + (dst_positive_permutation_pullbacksource))) /\ (((((exists ff_h_pvs_permutation_pullbacksourcenegative. ff_h_pvs_permutation_pullbacksourcenegative + S (dst_negative_permutation_pullbacksource) = S ((S (dsr_image_permutation_pullback)) * dst_negative_scale_permutation_pullbacksource)) /\ exists ff_q_pvs_permutation_pullbacksourcenegative. dst_negative_code_permutation_pullbacksource = ff_q_pvs_permutation_pullbacksourcenegative * S ((S (dsr_image_permutation_pullback)) * dst_negative_scale_permutation_pullbacksource) + (dst_negative_permutation_pullbacksource))) /\ (exists ge_balance_positive_permutation_pullbacksourcevalue ge_balance_negative_permutation_pullbacksourcevalue. (((((dsr_value_permutation_pullback) = 2 * (ge_balance_positive_permutation_pullbacksourcevalue) /\ (ge_balance_negative_permutation_pullbacksourcevalue) = 0) \/ exists ge_signed_half_permutation_pullbacksourcevaluedecode. (((dsr_value_permutation_pullback) = 2 * ge_signed_half_permutation_pullbacksourcevaluedecode + 1 /\ (ge_balance_positive_permutation_pullbacksourcevalue) = 0) /\ (ge_balance_negative_permutation_pullbacksourcevalue) = S ge_signed_half_permutation_pullbacksourcevaluedecode))) /\ ((dst_positive_permutation_pullbacksource) + ge_balance_negative_permutation_pullbacksourcevalue = (dst_negative_permutation_pullbacksource) + ge_balance_positive_permutation_pullbacksourcevalue))))))))) -> (exists dst_positive_code_permutation_pullbacktarget dst_positive_scale_permutation_pullbacktarget dst_negative_code_permutation_pullbacktarget dst_negative_scale_permutation_pullbacktarget dst_positive_permutation_pullbacktarget dst_negative_permutation_pullbacktarget. (((G) = (((((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) * S ((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) + ((dst_positive_scale_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))) * S ((((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) * S ((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) + ((dst_positive_scale_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))) + ((((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))))) /\ (((((exists ff_h_pvs_permutation_pullbacktargetpositive. ff_h_pvs_permutation_pullbacktargetpositive + S (dst_positive_permutation_pullbacktarget) = S ((S (dsr_index_permutation_pullback)) * dst_positive_scale_permutation_pullbacktarget)) /\ exists ff_q_pvs_permutation_pullbacktargetpositive. dst_positive_code_permutation_pullbacktarget = ff_q_pvs_permutation_pullbacktargetpositive * S ((S (dsr_index_permutation_pullback)) * dst_positive_scale_permutation_pullbacktarget) + (dst_positive_permutation_pullbacktarget))) /\ (((((exists ff_h_pvs_permutation_pullbacktargetnegative. ff_h_pvs_permutation_pullbacktargetnegative + S (dst_negative_permutation_pullbacktarget) = S ((S (dsr_index_permutation_pullback)) * dst_negative_scale_permutation_pullbacktarget)) /\ exists ff_q_pvs_permutation_pullbacktargetnegative. dst_negative_code_permutation_pullbacktarget = ff_q_pvs_permutation_pullbacktargetnegative * S ((S (dsr_index_permutation_pullback)) * dst_negative_scale_permutation_pullbacktarget) + (dst_negative_permutation_pullbacktarget))) /\ (exists ge_balance_positive_permutation_pullbacktargetvalue ge_balance_negative_permutation_pullbacktargetvalue. (((((dsr_value_permutation_pullback) = 2 * (ge_balance_positive_permutation_pullbacktargetvalue) /\ (ge_balance_negative_permutation_pullbacktargetvalue) = 0) \/ exists ge_signed_half_permutation_pullbacktargetvaluedecode. (((dsr_value_permutation_pullback) = 2 * ge_signed_half_permutation_pullbacktargetvaluedecode + 1 /\ (ge_balance_positive_permutation_pullbacktargetvalue) = 0) /\ (ge_balance_negative_permutation_pullbacktargetvalue) = S ge_signed_half_permutation_pullbacktargetvaluedecode))) /\ ((dst_positive_permutation_pullbacktarget) + ge_balance_negative_permutation_pullbacktargetvalue = (dst_negative_permutation_pullbacktarget) + ge_balance_positive_permutation_pullbacktargetvalue)))))))))) -> (exists dst_positive_code_permutation_source dst_positive_scale_permutation_source dst_negative_code_permutation_source dst_negative_scale_permutation_source dst_positive_sum_permutation_source dst_negative_sum_permutation_source. (((F) = (((((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) * S ((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) + ((dst_positive_scale_permutation_source) + (dst_positive_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))) * S ((((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) * S ((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) + ((dst_positive_scale_permutation_source) + (dst_positive_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))) + ((((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))))) /\ (((exists fs_u_dst_permutation_sourcepositive fs_v_dst_permutation_sourcepositive. ((((exists fs_h_dst_permutation_sourcepositive_body_start. fs_h_dst_permutation_sourcepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_start. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_start * S ((S (0)) * fs_v_dst_permutation_sourcepositive) + (0))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_terminal. fs_h_dst_permutation_sourcepositive_body_terminal + S (dst_positive_sum_permutation_source) = S ((S (l)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_terminal. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_terminal * S ((S (l)) * fs_v_dst_permutation_sourcepositive) + (dst_positive_sum_permutation_source))) /\ forall fs_i_dst_permutation_sourcepositive_body_steps. (exists fs_lt_dst_permutation_sourcepositive_body_steps_bound. fs_lt_dst_permutation_sourcepositive_body_steps_bound + S fs_i_dst_permutation_sourcepositive_body_steps = l) -> exists fs_a_dst_permutation_sourcepositive_body_steps fs_r_dst_permutation_sourcepositive_body_steps fs_s_dst_permutation_sourcepositive_body_steps. ((((exists fs_h_dst_permutation_sourcepositive_body_steps_summand. fs_h_dst_permutation_sourcepositive_body_steps_summand + S (fs_a_dst_permutation_sourcepositive_body_steps) = S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * dst_positive_scale_permutation_source)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_summand. dst_positive_code_permutation_source = fs_q_dst_permutation_sourcepositive_body_steps_summand * S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * dst_positive_scale_permutation_source) + (fs_a_dst_permutation_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_steps_partial. fs_h_dst_permutation_sourcepositive_body_steps_partial + S (fs_r_dst_permutation_sourcepositive_body_steps) = S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_partial. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_steps_partial * S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive) + (fs_r_dst_permutation_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_steps_successor. fs_h_dst_permutation_sourcepositive_body_steps_successor + S (fs_s_dst_permutation_sourcepositive_body_steps) = S ((S (S fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_successor. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_steps_successor * S ((S (S fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive) + (fs_s_dst_permutation_sourcepositive_body_steps))) /\ fs_s_dst_permutation_sourcepositive_body_steps = fs_r_dst_permutation_sourcepositive_body_steps + fs_a_dst_permutation_sourcepositive_body_steps)))))) /\ (((exists fs_u_dst_permutation_sourcenegative fs_v_dst_permutation_sourcenegative. ((((exists fs_h_dst_permutation_sourcenegative_body_start. fs_h_dst_permutation_sourcenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_start. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_start * S ((S (0)) * fs_v_dst_permutation_sourcenegative) + (0))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_terminal. fs_h_dst_permutation_sourcenegative_body_terminal + S (dst_negative_sum_permutation_source) = S ((S (l)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_terminal. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_terminal * S ((S (l)) * fs_v_dst_permutation_sourcenegative) + (dst_negative_sum_permutation_source))) /\ forall fs_i_dst_permutation_sourcenegative_body_steps. (exists fs_lt_dst_permutation_sourcenegative_body_steps_bound. fs_lt_dst_permutation_sourcenegative_body_steps_bound + S fs_i_dst_permutation_sourcenegative_body_steps = l) -> exists fs_a_dst_permutation_sourcenegative_body_steps fs_r_dst_permutation_sourcenegative_body_steps fs_s_dst_permutation_sourcenegative_body_steps. ((((exists fs_h_dst_permutation_sourcenegative_body_steps_summand. fs_h_dst_permutation_sourcenegative_body_steps_summand + S (fs_a_dst_permutation_sourcenegative_body_steps) = S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * dst_negative_scale_permutation_source)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_summand. dst_negative_code_permutation_source = fs_q_dst_permutation_sourcenegative_body_steps_summand * S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * dst_negative_scale_permutation_source) + (fs_a_dst_permutation_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_steps_partial. fs_h_dst_permutation_sourcenegative_body_steps_partial + S (fs_r_dst_permutation_sourcenegative_body_steps) = S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_partial. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_steps_partial * S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative) + (fs_r_dst_permutation_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_steps_successor. fs_h_dst_permutation_sourcenegative_body_steps_successor + S (fs_s_dst_permutation_sourcenegative_body_steps) = S ((S (S fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_successor. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_steps_successor * S ((S (S fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative) + (fs_s_dst_permutation_sourcenegative_body_steps))) /\ fs_s_dst_permutation_sourcenegative_body_steps = fs_r_dst_permutation_sourcenegative_body_steps + fs_a_dst_permutation_sourcenegative_body_steps)))))) /\ (exists ge_balance_positive_permutation_sourceresult ge_balance_negative_permutation_sourceresult. (((((u) = 2 * (ge_balance_positive_permutation_sourceresult) /\ (ge_balance_negative_permutation_sourceresult) = 0) \/ exists ge_signed_half_permutation_sourceresultdecode. (((u) = 2 * ge_signed_half_permutation_sourceresultdecode + 1 /\ (ge_balance_positive_permutation_sourceresult) = 0) /\ (ge_balance_negative_permutation_sourceresult) = S ge_signed_half_permutation_sourceresultdecode))) /\ ((dst_positive_sum_permutation_source) + ge_balance_negative_permutation_sourceresult = (dst_negative_sum_permutation_source) + ge_balance_positive_permutation_sourceresult))))))))) -> (exists dst_positive_code_permutation_target dst_positive_scale_permutation_target dst_negative_code_permutation_target dst_negative_scale_permutation_target dst_positive_sum_permutation_target dst_negative_sum_permutation_target. (((G) = (((((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) * S ((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) + ((dst_positive_scale_permutation_target) + (dst_positive_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))) * S ((((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) * S ((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) + ((dst_positive_scale_permutation_target) + (dst_positive_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))) + ((((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))))) /\ (((exists fs_u_dst_permutation_targetpositive fs_v_dst_permutation_targetpositive. ((((exists fs_h_dst_permutation_targetpositive_body_start. fs_h_dst_permutation_targetpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_start. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_start * S ((S (0)) * fs_v_dst_permutation_targetpositive) + (0))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_terminal. fs_h_dst_permutation_targetpositive_body_terminal + S (dst_positive_sum_permutation_target) = S ((S (l)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_terminal. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_terminal * S ((S (l)) * fs_v_dst_permutation_targetpositive) + (dst_positive_sum_permutation_target))) /\ forall fs_i_dst_permutation_targetpositive_body_steps. (exists fs_lt_dst_permutation_targetpositive_body_steps_bound. fs_lt_dst_permutation_targetpositive_body_steps_bound + S fs_i_dst_permutation_targetpositive_body_steps = l) -> exists fs_a_dst_permutation_targetpositive_body_steps fs_r_dst_permutation_targetpositive_body_steps fs_s_dst_permutation_targetpositive_body_steps. ((((exists fs_h_dst_permutation_targetpositive_body_steps_summand. fs_h_dst_permutation_targetpositive_body_steps_summand + S (fs_a_dst_permutation_targetpositive_body_steps) = S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * dst_positive_scale_permutation_target)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_summand. dst_positive_code_permutation_target = fs_q_dst_permutation_targetpositive_body_steps_summand * S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * dst_positive_scale_permutation_target) + (fs_a_dst_permutation_targetpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_steps_partial. fs_h_dst_permutation_targetpositive_body_steps_partial + S (fs_r_dst_permutation_targetpositive_body_steps) = S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_partial. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_steps_partial * S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive) + (fs_r_dst_permutation_targetpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_steps_successor. fs_h_dst_permutation_targetpositive_body_steps_successor + S (fs_s_dst_permutation_targetpositive_body_steps) = S ((S (S fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_successor. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_steps_successor * S ((S (S fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive) + (fs_s_dst_permutation_targetpositive_body_steps))) /\ fs_s_dst_permutation_targetpositive_body_steps = fs_r_dst_permutation_targetpositive_body_steps + fs_a_dst_permutation_targetpositive_body_steps)))))) /\ (((exists fs_u_dst_permutation_targetnegative fs_v_dst_permutation_targetnegative. ((((exists fs_h_dst_permutation_targetnegative_body_start. fs_h_dst_permutation_targetnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_start. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_start * S ((S (0)) * fs_v_dst_permutation_targetnegative) + (0))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_terminal. fs_h_dst_permutation_targetnegative_body_terminal + S (dst_negative_sum_permutation_target) = S ((S (l)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_terminal. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_terminal * S ((S (l)) * fs_v_dst_permutation_targetnegative) + (dst_negative_sum_permutation_target))) /\ forall fs_i_dst_permutation_targetnegative_body_steps. (exists fs_lt_dst_permutation_targetnegative_body_steps_bound. fs_lt_dst_permutation_targetnegative_body_steps_bound + S fs_i_dst_permutation_targetnegative_body_steps = l) -> exists fs_a_dst_permutation_targetnegative_body_steps fs_r_dst_permutation_targetnegative_body_steps fs_s_dst_permutation_targetnegative_body_steps. ((((exists fs_h_dst_permutation_targetnegative_body_steps_summand. fs_h_dst_permutation_targetnegative_body_steps_summand + S (fs_a_dst_permutation_targetnegative_body_steps) = S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * dst_negative_scale_permutation_target)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_summand. dst_negative_code_permutation_target = fs_q_dst_permutation_targetnegative_body_steps_summand * S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * dst_negative_scale_permutation_target) + (fs_a_dst_permutation_targetnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_steps_partial. fs_h_dst_permutation_targetnegative_body_steps_partial + S (fs_r_dst_permutation_targetnegative_body_steps) = S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_partial. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_steps_partial * S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative) + (fs_r_dst_permutation_targetnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_steps_successor. fs_h_dst_permutation_targetnegative_body_steps_successor + S (fs_s_dst_permutation_targetnegative_body_steps) = S ((S (S fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_successor. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_steps_successor * S ((S (S fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative) + (fs_s_dst_permutation_targetnegative_body_steps))) /\ fs_s_dst_permutation_targetnegative_body_steps = fs_r_dst_permutation_targetnegative_body_steps + fs_a_dst_permutation_targetnegative_body_steps)))))) /\ (exists ge_balance_positive_permutation_targetresult ge_balance_negative_permutation_targetresult. (((((v) = 2 * (ge_balance_positive_permutation_targetresult) /\ (ge_balance_negative_permutation_targetresult) = 0) \/ exists ge_signed_half_permutation_targetresultdecode. (((v) = 2 * ge_signed_half_permutation_targetresultdecode + 1 /\ (ge_balance_positive_permutation_targetresult) = 0) /\ (ge_balance_negative_permutation_targetresult) = S ge_signed_half_permutation_targetresultdecode))) /\ ((dst_positive_sum_permutation_target) + ge_balance_negative_permutation_targetresult = (dst_negative_sum_permutation_target) + ge_balance_positive_permutation_targetresult))))))))) -> u = v

Constructive proof overview

Generated structural guide

Any actual bounded injective beta permutation preserves the genuine signed sum, even for unrelated positive/negative representations of the pullback table.

The unchanged tactic script uses 6 declared prerequisites and contains 108 exact native proof lines.

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

Proof neighborhood

Direct dependencies

SS0019 divisor_signed_table_reindex_data_exists SS000B divisor_signed_sum_exists_from_components SS001D divisor_signed_sum_component_reindex SS0014 divisor_signed_sum_extensional SS001C divisor_signed_table_reindex_functional SS001A divisor_signed_table_reindex_from_components

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

108 script commands · 18 reading checkpoints · 3 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 (6)
divisor signed table reindex data existsdivisor signed sum exists from componentsdivisor signed sum component reindexdivisor signed sum extensionaldivisor signed table reindex functionaldivisor signed table reindex 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–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro l
  6. L6
    intro u
  7. L7
    intro v
  8. L8
    intro hbound
  9. L9
    intro hinj
  10. L10
    intro hreindex
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hu
  2. L12
    intro hv
03Separate the logical casesL13–21

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

  1. L13
    cases hu
  2. L14
    cases hu_witness
  3. L15
    cases hu_witness_witness
  4. L16
    cases hu_witness_witness_witness
  5. L17
    cases hu_witness_witness_witness_witness
  6. L18
    cases hu_witness_witness_witness_witness_witness
  7. L19
    cases hu_witness_witness_witness_witness_witness_witness
  8. L20
    cases hu_witness_witness_witness_witness_witness_witness_right
  9. L21
    cases hu_witness_witness_witness_witness_witness_witness_right_right
04Establish hdataL22–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table reindex data exists.

  1. L22
    have hdata : ∃ qb. ∃ qc. ∃ mb. ∃ mc. (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x,x1,z,n) → BetaAt(qb,qc,y,n)) ∧ (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x2,x3,z,n) → BetaAt(mb,mc,y,n))Definitions: LtBetaAt
  2. L23
    specialize divisor_signed_table_reindex_data_exists (x)
  3. L24
    specialize divisor_signed_table_reindex_data_exists (x1)
  4. L25
    specialize divisor_signed_table_reindex_data_exists (x2)
  5. L26
    specialize divisor_signed_table_reindex_data_exists (x3)
  6. L27
    specialize divisor_signed_table_reindex_data_exists (r)
  7. L28
    specialize divisor_signed_table_reindex_data_exists (s)
  8. L29
    specialize divisor_signed_table_reindex_data_exists (l)
  9. L30
    apply divisor_signed_table_reindex_data_exists
05Separate the logical casesL31–34

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

  1. L31
    cases hdata
  2. L32
    cases hdata_witness
  3. L33
    cases hdata_witness_witness
  4. L34
    cases hdata_witness_witness_witness
06Establish hsumL35–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed sum exists from components.

  1. L35
    have hsum : ∃ z. SignedPrefixSum(((x6 + x7) · S (x6 + x7) + (x7 + x7) + ((x8 + x9) · S (x8 + x9) + (x9 + x9))) · S ((x6 + x7) · S (x6 + x7) + (x7 + x7) + ((x8 + x9) · S (x8 + x9) + (x9 + x9))) + ((x8 + x9) · S (x8 + x9) + (x9 + x9) + ((x8 + x9) · S (x8 + x9) + (x9 + x9))),l,z)Definitions: SignedPrefixSum
  2. L36
    specialize divisor_signed_sum_exists_from_components (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  3. L37
    specialize divisor_signed_sum_exists_from_components (x6)
  4. L38
    specialize divisor_signed_sum_exists_from_components (x7)
  5. L39
    specialize divisor_signed_sum_exists_from_components (x8)
  6. L40
    specialize divisor_signed_sum_exists_from_components (x9)
  7. L41
    specialize divisor_signed_sum_exists_from_components (l)
  8. L42
    apply divisor_signed_sum_exists_from_components
  9. L43
    refl
07Separate the logical casesL44–44

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

  1. L44
    cases hsum
08Establish heqL45–54

Establish this local claim before using it. It is not an additional assumption.

  1. L45
    have heq : u = x10
  2. L46
    specialize divisor_signed_sum_component_reindex (F)
  3. L47
    specialize divisor_signed_sum_component_reindex (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  4. L48
    specialize divisor_signed_sum_component_reindex (x)
  5. L49
    specialize divisor_signed_sum_component_reindex (x1)
  6. L50
    specialize divisor_signed_sum_component_reindex (x2)
  7. L51
    specialize divisor_signed_sum_component_reindex (x3)
  8. L52
    specialize divisor_signed_sum_component_reindex (x6)
  9. L53
    specialize divisor_signed_sum_component_reindex (x7)
  10. L54
    specialize divisor_signed_sum_component_reindex (x8)
09Use earlier factsL55–62

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

  1. L55
    specialize divisor_signed_sum_component_reindex (x9)
  2. L56
    specialize divisor_signed_sum_component_reindex (r)
  3. L57
    specialize divisor_signed_sum_component_reindex (s)
  4. L58
    specialize divisor_signed_sum_component_reindex (l)
  5. L59
    specialize divisor_signed_sum_component_reindex (u)
  6. L60
    specialize divisor_signed_sum_component_reindex (x10)
  7. L61
    apply divisor_signed_sum_component_reindex
  8. L62
    exact hu_witness_witness_witness_witness_witness_witness_left
10Calculate and transport equalitiesL63–63

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

  1. L63
    refl
11Use earlier factsL64–68

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

  1. L64
    exact hbound
  2. L65
    exact hinj
  3. L66
    exact hdata_witness_witness_witness_witness
  4. L67
    exact hu
  5. L68
    exact hsum_witness
12Calculate and transport equalitiesL69–69

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

  1. L69
    trans x10
13Use earlier factsL70–79

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

  1. L70
    exact heq
  2. L71
    specialize divisor_signed_sum_extensional (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  3. L72
    specialize divisor_signed_sum_extensional (G)
  4. L73
    specialize divisor_signed_sum_extensional (l)
  5. L74
    specialize divisor_signed_sum_extensional (x10)
  6. L75
    specialize divisor_signed_sum_extensional (v)
  7. L76
    apply divisor_signed_sum_extensional
  8. L77
    specialize divisor_signed_table_reindex_functional (F)
  9. L78
    specialize divisor_signed_table_reindex_functional (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  10. L79
    specialize divisor_signed_table_reindex_functional (G)
14Use earlier factsL80–89

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

  1. L80
    specialize divisor_signed_table_reindex_functional (x)
  2. L81
    specialize divisor_signed_table_reindex_functional (x1)
  3. L82
    specialize divisor_signed_table_reindex_functional (x2)
  4. L83
    specialize divisor_signed_table_reindex_functional (x3)
  5. L84
    specialize divisor_signed_table_reindex_functional (r)
  6. L85
    specialize divisor_signed_table_reindex_functional (s)
  7. L86
    specialize divisor_signed_table_reindex_functional (l)
  8. L87
    apply divisor_signed_table_reindex_functional
  9. L88
    exact hu_witness_witness_witness_witness_witness_witness_left
  10. L89
    specialize divisor_signed_table_reindex_from_components (F)
15Use earlier factsL90–99

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

  1. L90
    specialize divisor_signed_table_reindex_from_components (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  2. L91
    specialize divisor_signed_table_reindex_from_components (x)
  3. L92
    specialize divisor_signed_table_reindex_from_components (x1)
  4. L93
    specialize divisor_signed_table_reindex_from_components (x2)
  5. L94
    specialize divisor_signed_table_reindex_from_components (x3)
  6. L95
    specialize divisor_signed_table_reindex_from_components (x6)
  7. L96
    specialize divisor_signed_table_reindex_from_components (x7)
  8. L97
    specialize divisor_signed_table_reindex_from_components (x8)
  9. L98
    specialize divisor_signed_table_reindex_from_components (x9)
  10. L99
    specialize divisor_signed_table_reindex_from_components (r)
16Use earlier factsL100–103

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

  1. L100
    specialize divisor_signed_table_reindex_from_components (s)
  2. L101
    specialize divisor_signed_table_reindex_from_components (l)
  3. L102
    apply divisor_signed_table_reindex_from_components
  4. L103
    exact hu_witness_witness_witness_witness_witness_witness_left
17Calculate and transport equalitiesL104–104

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

  1. L104
    refl
18Use earlier factsL105–108

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

  1. L105
    exact hdata_witness_witness_witness_witness
  2. L106
    exact hreindex
  3. L107
    exact hsum_witness
  4. L108
    exact hv

Library-wide reading audit

Original exact command ledger · 108 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro r
  4. 0004intro s
  5. 0005intro l
  6. 0006intro u
  7. 0007intro v
  8. 0008intro hbound
  9. 0009intro hinj
  10. 0010intro hreindex
  11. 0011intro hu
  12. 0012intro hv
  13. 0013cases hu
  14. 0014cases hu_witness
  15. 0015cases hu_witness_witness
  16. 0016cases hu_witness_witness_witness
  17. 0017cases hu_witness_witness_witness_witness
  18. 0018cases hu_witness_witness_witness_witness_witness
  19. 0019cases hu_witness_witness_witness_witness_witness_witness
  20. 0020cases hu_witness_witness_witness_witness_witness_witness_right
  21. 0021cases hu_witness_witness_witness_witness_witness_witness_right_right
  22. 0022have hdata : exists qb qc mb mc. (((forall fms_i_permutation_constructedpositive fms_j_permutation_constructedpositive fms_v_permutation_constructedpositive. (exists fms_gap_permutation_constructedpositive. fms_gap_permutation_constructedpositive + S (fms_i_permutation_constructedpositive) = (l)) -> (((exists fs_h_fms_permutation_constructedpositive_index. fs_h_fms_permutation_constructedpositive_index + S (fms_j_permutation_constructedpositive) = S ((S (fms_i_permutation_constructedpositive)) * s)) /\ exists fs_q_fms_permutation_constructedpositive_index. r = fs_q_fms_permutation_constructedpositive_index * S ((S (fms_i_permutation_constructedpositive)) * s) + (fms_j_permutation_constructedpositive))) -> (((exists fs_h_fms_permutation_constructedpositive_source. fs_h_fms_permutation_constructedpositive_source + S (fms_v_permutation_constructedpositive) = S ((S (fms_j_permutation_constructedpositive)) * x1)) /\ exists fs_q_fms_permutation_constructedpositive_source. x = fs_q_fms_permutation_constructedpositive_source * S ((S (fms_j_permutation_constructedpositive)) * x1) + (fms_v_permutation_constructedpositive))) -> (((exists fs_h_fms_permutation_constructedpositive_target. fs_h_fms_permutation_constructedpositive_target + S (fms_v_permutation_constructedpositive) = S ((S (fms_i_permutation_constructedpositive)) * qc)) /\ exists fs_q_fms_permutation_constructedpositive_target. qb = fs_q_fms_permutation_constructedpositive_target * S ((S (fms_i_permutation_constructedpositive)) * qc) + (fms_v_permutation_constructedpositive)))) /\ (forall fms_i_permutation_constructednegative fms_j_permutation_constructednegative fms_v_permutation_constructednegative. (exists fms_gap_permutation_constructednegative. fms_gap_permutation_constructednegative + S (fms_i_permutation_constructednegative) = (l)) -> (((exists fs_h_fms_permutation_constructednegative_index. fs_h_fms_permutation_constructednegative_index + S (fms_j_permutation_constructednegative) = S ((S (fms_i_permutation_constructednegative)) * s)) /\ exists fs_q_fms_permutation_constructednegative_index. r = fs_q_fms_permutation_constructednegative_index * S ((S (fms_i_permutation_constructednegative)) * s) + (fms_j_permutation_constructednegative))) -> (((exists fs_h_fms_permutation_constructednegative_source. fs_h_fms_permutation_constructednegative_source + S (fms_v_permutation_constructednegative) = S ((S (fms_j_permutation_constructednegative)) * x3)) /\ exists fs_q_fms_permutation_constructednegative_source. x2 = fs_q_fms_permutation_constructednegative_source * S ((S (fms_j_permutation_constructednegative)) * x3) + (fms_v_permutation_constructednegative))) -> (((exists fs_h_fms_permutation_constructednegative_target. fs_h_fms_permutation_constructednegative_target + S (fms_v_permutation_constructednegative) = S ((S (fms_i_permutation_constructednegative)) * mc)) /\ exists fs_q_fms_permutation_constructednegative_target. mb = fs_q_fms_permutation_constructednegative_target * S ((S (fms_i_permutation_constructednegative)) * mc) + (fms_v_permutation_constructednegative))))))
  23. 0023specialize divisor_signed_table_reindex_data_exists (x)
  24. 0024specialize divisor_signed_table_reindex_data_exists (x1)
  25. 0025specialize divisor_signed_table_reindex_data_exists (x2)
  26. 0026specialize divisor_signed_table_reindex_data_exists (x3)
  27. 0027specialize divisor_signed_table_reindex_data_exists (r)
  28. 0028specialize divisor_signed_table_reindex_data_exists (s)
  29. 0029specialize divisor_signed_table_reindex_data_exists (l)
  30. 0030apply divisor_signed_table_reindex_data_exists
  31. 0031cases hdata
  32. 0032cases hdata_witness
  33. 0033cases hdata_witness_witness
  34. 0034cases hdata_witness_witness_witness
  35. 0035have hsum : exists z. (exists dst_positive_code_permutation_actual_sum dst_positive_scale_permutation_actual_sum dst_negative_code_permutation_actual_sum dst_negative_scale_permutation_actual_sum dst_positive_sum_permutation_actual_sum dst_negative_sum_permutation_actual_sum. (((((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))))) = (((((dst_positive_code_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum)) * S ((dst_positive_code_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum)) + ((dst_positive_scale_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum))) + (((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) * S ((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) + ((dst_negative_scale_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)))) * S ((((dst_positive_code_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum)) * S ((dst_positive_code_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum)) + ((dst_positive_scale_permutation_actual_sum) + (dst_positive_scale_permutation_actual_sum))) + (((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) * S ((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) + ((dst_negative_scale_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)))) + ((((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) * S ((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) + ((dst_negative_scale_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum))) + (((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) * S ((dst_negative_code_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)) + ((dst_negative_scale_permutation_actual_sum) + (dst_negative_scale_permutation_actual_sum)))))) /\ (((exists fs_u_dst_permutation_actual_sumpositive fs_v_dst_permutation_actual_sumpositive. ((((exists fs_h_dst_permutation_actual_sumpositive_body_start. fs_h_dst_permutation_actual_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_actual_sumpositive)) /\ exists fs_q_dst_permutation_actual_sumpositive_body_start. fs_u_dst_permutation_actual_sumpositive = fs_q_dst_permutation_actual_sumpositive_body_start * S ((S (0)) * fs_v_dst_permutation_actual_sumpositive) + (0))) /\ ((((exists fs_h_dst_permutation_actual_sumpositive_body_terminal. fs_h_dst_permutation_actual_sumpositive_body_terminal + S (dst_positive_sum_permutation_actual_sum) = S ((S (l)) * fs_v_dst_permutation_actual_sumpositive)) /\ exists fs_q_dst_permutation_actual_sumpositive_body_terminal. fs_u_dst_permutation_actual_sumpositive = fs_q_dst_permutation_actual_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_permutation_actual_sumpositive) + (dst_positive_sum_permutation_actual_sum))) /\ forall fs_i_dst_permutation_actual_sumpositive_body_steps. (exists fs_lt_dst_permutation_actual_sumpositive_body_steps_bound. fs_lt_dst_permutation_actual_sumpositive_body_steps_bound + S fs_i_dst_permutation_actual_sumpositive_body_steps = l) -> exists fs_a_dst_permutation_actual_sumpositive_body_steps fs_r_dst_permutation_actual_sumpositive_body_steps fs_s_dst_permutation_actual_sumpositive_body_steps. ((((exists fs_h_dst_permutation_actual_sumpositive_body_steps_summand. fs_h_dst_permutation_actual_sumpositive_body_steps_summand + S (fs_a_dst_permutation_actual_sumpositive_body_steps) = S ((S (fs_i_dst_permutation_actual_sumpositive_body_steps)) * dst_positive_scale_permutation_actual_sum)) /\ exists fs_q_dst_permutation_actual_sumpositive_body_steps_summand. dst_positive_code_permutation_actual_sum = fs_q_dst_permutation_actual_sumpositive_body_steps_summand * S ((S (fs_i_dst_permutation_actual_sumpositive_body_steps)) * dst_positive_scale_permutation_actual_sum) + (fs_a_dst_permutation_actual_sumpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_actual_sumpositive_body_steps_partial. fs_h_dst_permutation_actual_sumpositive_body_steps_partial + S (fs_r_dst_permutation_actual_sumpositive_body_steps) = S ((S (fs_i_dst_permutation_actual_sumpositive_body_steps)) * fs_v_dst_permutation_actual_sumpositive)) /\ exists fs_q_dst_permutation_actual_sumpositive_body_steps_partial. fs_u_dst_permutation_actual_sumpositive = fs_q_dst_permutation_actual_sumpositive_body_steps_partial * S ((S (fs_i_dst_permutation_actual_sumpositive_body_steps)) * fs_v_dst_permutation_actual_sumpositive) + (fs_r_dst_permutation_actual_sumpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_actual_sumpositive_body_steps_successor. fs_h_dst_permutation_actual_sumpositive_body_steps_successor + S (fs_s_dst_permutation_actual_sumpositive_body_steps) = S ((S (S fs_i_dst_permutation_actual_sumpositive_body_steps)) * fs_v_dst_permutation_actual_sumpositive)) /\ exists fs_q_dst_permutation_actual_sumpositive_body_steps_successor. fs_u_dst_permutation_actual_sumpositive = fs_q_dst_permutation_actual_sumpositive_body_steps_successor * S ((S (S fs_i_dst_permutation_actual_sumpositive_body_steps)) * fs_v_dst_permutation_actual_sumpositive) + (fs_s_dst_permutation_actual_sumpositive_body_steps))) /\ fs_s_dst_permutation_actual_sumpositive_body_steps = fs_r_dst_permutation_actual_sumpositive_body_steps + fs_a_dst_permutation_actual_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_permutation_actual_sumnegative fs_v_dst_permutation_actual_sumnegative. ((((exists fs_h_dst_permutation_actual_sumnegative_body_start. fs_h_dst_permutation_actual_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_actual_sumnegative)) /\ exists fs_q_dst_permutation_actual_sumnegative_body_start. fs_u_dst_permutation_actual_sumnegative = fs_q_dst_permutation_actual_sumnegative_body_start * S ((S (0)) * fs_v_dst_permutation_actual_sumnegative) + (0))) /\ ((((exists fs_h_dst_permutation_actual_sumnegative_body_terminal. fs_h_dst_permutation_actual_sumnegative_body_terminal + S (dst_negative_sum_permutation_actual_sum) = S ((S (l)) * fs_v_dst_permutation_actual_sumnegative)) /\ exists fs_q_dst_permutation_actual_sumnegative_body_terminal. fs_u_dst_permutation_actual_sumnegative = fs_q_dst_permutation_actual_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_permutation_actual_sumnegative) + (dst_negative_sum_permutation_actual_sum))) /\ forall fs_i_dst_permutation_actual_sumnegative_body_steps. (exists fs_lt_dst_permutation_actual_sumnegative_body_steps_bound. fs_lt_dst_permutation_actual_sumnegative_body_steps_bound + S fs_i_dst_permutation_actual_sumnegative_body_steps = l) -> exists fs_a_dst_permutation_actual_sumnegative_body_steps fs_r_dst_permutation_actual_sumnegative_body_steps fs_s_dst_permutation_actual_sumnegative_body_steps. ((((exists fs_h_dst_permutation_actual_sumnegative_body_steps_summand. fs_h_dst_permutation_actual_sumnegative_body_steps_summand + S (fs_a_dst_permutation_actual_sumnegative_body_steps) = S ((S (fs_i_dst_permutation_actual_sumnegative_body_steps)) * dst_negative_scale_permutation_actual_sum)) /\ exists fs_q_dst_permutation_actual_sumnegative_body_steps_summand. dst_negative_code_permutation_actual_sum = fs_q_dst_permutation_actual_sumnegative_body_steps_summand * S ((S (fs_i_dst_permutation_actual_sumnegative_body_steps)) * dst_negative_scale_permutation_actual_sum) + (fs_a_dst_permutation_actual_sumnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_actual_sumnegative_body_steps_partial. fs_h_dst_permutation_actual_sumnegative_body_steps_partial + S (fs_r_dst_permutation_actual_sumnegative_body_steps) = S ((S (fs_i_dst_permutation_actual_sumnegative_body_steps)) * fs_v_dst_permutation_actual_sumnegative)) /\ exists fs_q_dst_permutation_actual_sumnegative_body_steps_partial. fs_u_dst_permutation_actual_sumnegative = fs_q_dst_permutation_actual_sumnegative_body_steps_partial * S ((S (fs_i_dst_permutation_actual_sumnegative_body_steps)) * fs_v_dst_permutation_actual_sumnegative) + (fs_r_dst_permutation_actual_sumnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_actual_sumnegative_body_steps_successor. fs_h_dst_permutation_actual_sumnegative_body_steps_successor + S (fs_s_dst_permutation_actual_sumnegative_body_steps) = S ((S (S fs_i_dst_permutation_actual_sumnegative_body_steps)) * fs_v_dst_permutation_actual_sumnegative)) /\ exists fs_q_dst_permutation_actual_sumnegative_body_steps_successor. fs_u_dst_permutation_actual_sumnegative = fs_q_dst_permutation_actual_sumnegative_body_steps_successor * S ((S (S fs_i_dst_permutation_actual_sumnegative_body_steps)) * fs_v_dst_permutation_actual_sumnegative) + (fs_s_dst_permutation_actual_sumnegative_body_steps))) /\ fs_s_dst_permutation_actual_sumnegative_body_steps = fs_r_dst_permutation_actual_sumnegative_body_steps + fs_a_dst_permutation_actual_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_permutation_actual_sumresult ge_balance_negative_permutation_actual_sumresult. (((((z) = 2 * (ge_balance_positive_permutation_actual_sumresult) /\ (ge_balance_negative_permutation_actual_sumresult) = 0) \/ exists ge_signed_half_permutation_actual_sumresultdecode. (((z) = 2 * ge_signed_half_permutation_actual_sumresultdecode + 1 /\ (ge_balance_positive_permutation_actual_sumresult) = 0) /\ (ge_balance_negative_permutation_actual_sumresult) = S ge_signed_half_permutation_actual_sumresultdecode))) /\ ((dst_positive_sum_permutation_actual_sum) + ge_balance_negative_permutation_actual_sumresult = (dst_negative_sum_permutation_actual_sum) + ge_balance_positive_permutation_actual_sumresult)))))))))
  36. 0036specialize divisor_signed_sum_exists_from_components (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  37. 0037specialize divisor_signed_sum_exists_from_components (x6)
  38. 0038specialize divisor_signed_sum_exists_from_components (x7)
  39. 0039specialize divisor_signed_sum_exists_from_components (x8)
  40. 0040specialize divisor_signed_sum_exists_from_components (x9)
  41. 0041specialize divisor_signed_sum_exists_from_components (l)
  42. 0042apply divisor_signed_sum_exists_from_components
  43. 0043refl
  44. 0044cases hsum
  45. 0045have heq : u = x10
  46. 0046specialize divisor_signed_sum_component_reindex (F)
  47. 0047specialize divisor_signed_sum_component_reindex (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  48. 0048specialize divisor_signed_sum_component_reindex (x)
  49. 0049specialize divisor_signed_sum_component_reindex (x1)
  50. 0050specialize divisor_signed_sum_component_reindex (x2)
  51. 0051specialize divisor_signed_sum_component_reindex (x3)
  52. 0052specialize divisor_signed_sum_component_reindex (x6)
  53. 0053specialize divisor_signed_sum_component_reindex (x7)
  54. 0054specialize divisor_signed_sum_component_reindex (x8)
  55. 0055specialize divisor_signed_sum_component_reindex (x9)
  56. 0056specialize divisor_signed_sum_component_reindex (r)
  57. 0057specialize divisor_signed_sum_component_reindex (s)
  58. 0058specialize divisor_signed_sum_component_reindex (l)
  59. 0059specialize divisor_signed_sum_component_reindex (u)
  60. 0060specialize divisor_signed_sum_component_reindex (x10)
  61. 0061apply divisor_signed_sum_component_reindex
  62. 0062exact hu_witness_witness_witness_witness_witness_witness_left
  63. 0063refl
  64. 0064exact hbound
  65. 0065exact hinj
  66. 0066exact hdata_witness_witness_witness_witness
  67. 0067exact hu
  68. 0068exact hsum_witness
  69. 0069trans x10
  70. 0070exact heq
  71. 0071specialize divisor_signed_sum_extensional (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  72. 0072specialize divisor_signed_sum_extensional (G)
  73. 0073specialize divisor_signed_sum_extensional (l)
  74. 0074specialize divisor_signed_sum_extensional (x10)
  75. 0075specialize divisor_signed_sum_extensional (v)
  76. 0076apply divisor_signed_sum_extensional
  77. 0077specialize divisor_signed_table_reindex_functional (F)
  78. 0078specialize divisor_signed_table_reindex_functional (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  79. 0079specialize divisor_signed_table_reindex_functional (G)
  80. 0080specialize divisor_signed_table_reindex_functional (x)
  81. 0081specialize divisor_signed_table_reindex_functional (x1)
  82. 0082specialize divisor_signed_table_reindex_functional (x2)
  83. 0083specialize divisor_signed_table_reindex_functional (x3)
  84. 0084specialize divisor_signed_table_reindex_functional (r)
  85. 0085specialize divisor_signed_table_reindex_functional (s)
  86. 0086specialize divisor_signed_table_reindex_functional (l)
  87. 0087apply divisor_signed_table_reindex_functional
  88. 0088exact hu_witness_witness_witness_witness_witness_witness_left
  89. 0089specialize divisor_signed_table_reindex_from_components (F)
  90. 0090specialize divisor_signed_table_reindex_from_components (((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  91. 0091specialize divisor_signed_table_reindex_from_components (x)
  92. 0092specialize divisor_signed_table_reindex_from_components (x1)
  93. 0093specialize divisor_signed_table_reindex_from_components (x2)
  94. 0094specialize divisor_signed_table_reindex_from_components (x3)
  95. 0095specialize divisor_signed_table_reindex_from_components (x6)
  96. 0096specialize divisor_signed_table_reindex_from_components (x7)
  97. 0097specialize divisor_signed_table_reindex_from_components (x8)
  98. 0098specialize divisor_signed_table_reindex_from_components (x9)
  99. 0099specialize divisor_signed_table_reindex_from_components (r)
  100. 0100specialize divisor_signed_table_reindex_from_components (s)
  101. 0101specialize divisor_signed_table_reindex_from_components (l)
  102. 0102apply divisor_signed_table_reindex_from_components
  103. 0103exact hu_witness_witness_witness_witness_witness_witness_left
  104. 0104refl
  105. 0105exact hdata_witness_witness_witness_witness
  106. 0106exact hreindex
  107. 0107exact hsum_witness
  108. 0108exact hv