Original finite natural-sum permutation invariance preserves both actual component sums, hence their canonical signed result.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.
forall F G pb pc nb nc qb qc mb mc r s l u v. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> ((G) = (((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) * S ((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) + ((((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))))) -> (forall pfp_i_sum_map_bounded. (exists pfp_gap_sum_map_boundedindex. pfp_gap_sum_map_boundedindex + S (pfp_i_sum_map_bounded) = (l)) -> exists pfp_a_sum_map_bounded. (((exists ff_h_pfp_sum_map_boundedentry. ff_h_pfp_sum_map_boundedentry + S (pfp_a_sum_map_bounded) = S ((S (pfp_i_sum_map_bounded)) * s)) /\ exists ff_q_pfp_sum_map_boundedentry. r = ff_q_pfp_sum_map_boundedentry * S ((S (pfp_i_sum_map_bounded)) * s) + (pfp_a_sum_map_bounded))) /\ (exists pfp_gap_sum_map_boundedvalue. pfp_gap_sum_map_boundedvalue + S (pfp_a_sum_map_bounded) = (l))) -> (forall pfp_i_sum_map_injective pfp_j_sum_map_injective pfp_a_sum_map_injective. (exists pfp_gap_sum_map_injectivefirst. pfp_gap_sum_map_injectivefirst + S (pfp_i_sum_map_injective) = (l)) -> (exists pfp_gap_sum_map_injectivesecond. pfp_gap_sum_map_injectivesecond + S (pfp_j_sum_map_injective) = (l)) -> (((exists ff_h_pfp_sum_map_injectiveleft. ff_h_pfp_sum_map_injectiveleft + S (pfp_a_sum_map_injective) = S ((S (pfp_i_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveleft. r = ff_q_pfp_sum_map_injectiveleft * S ((S (pfp_i_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> (((exists ff_h_pfp_sum_map_injectiveright. ff_h_pfp_sum_map_injectiveright + S (pfp_a_sum_map_injective) = S ((S (pfp_j_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveright. r = ff_q_pfp_sum_map_injectiveright * S ((S (pfp_j_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> pfp_i_sum_map_injective = pfp_j_sum_map_injective) -> (((forall fms_i_sum_component_compositionpositive fms_j_sum_component_compositionpositive fms_v_sum_component_compositionpositive. (exists fms_gap_sum_component_compositionpositive. fms_gap_sum_component_compositionpositive + S (fms_i_sum_component_compositionpositive) = (l)) -> (((exists fs_h_fms_sum_component_compositionpositive_index. fs_h_fms_sum_component_compositionpositive_index + S (fms_j_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * s)) /\ exists fs_q_fms_sum_component_compositionpositive_index. r = fs_q_fms_sum_component_compositionpositive_index * S ((S (fms_i_sum_component_compositionpositive)) * s) + (fms_j_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_source. fs_h_fms_sum_component_compositionpositive_source + S (fms_v_sum_component_compositionpositive) = S ((S (fms_j_sum_component_compositionpositive)) * pc)) /\ exists fs_q_fms_sum_component_compositionpositive_source. pb = fs_q_fms_sum_component_compositionpositive_source * S ((S (fms_j_sum_component_compositionpositive)) * pc) + (fms_v_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_target. fs_h_fms_sum_component_compositionpositive_target + S (fms_v_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * qc)) /\ exists fs_q_fms_sum_component_compositionpositive_target. qb = fs_q_fms_sum_component_compositionpositive_target * S ((S (fms_i_sum_component_compositionpositive)) * qc) + (fms_v_sum_component_compositionpositive)))) /\ (forall fms_i_sum_component_compositionnegative fms_j_sum_component_compositionnegative fms_v_sum_component_compositionnegative. (exists fms_gap_sum_component_compositionnegative. fms_gap_sum_component_compositionnegative + S (fms_i_sum_component_compositionnegative) = (l)) -> (((exists fs_h_fms_sum_component_compositionnegative_index. fs_h_fms_sum_component_compositionnegative_index + S (fms_j_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * s)) /\ exists fs_q_fms_sum_component_compositionnegative_index. r = fs_q_fms_sum_component_compositionnegative_index * S ((S (fms_i_sum_component_compositionnegative)) * s) + (fms_j_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_source. fs_h_fms_sum_component_compositionnegative_source + S (fms_v_sum_component_compositionnegative) = S ((S (fms_j_sum_component_compositionnegative)) * nc)) /\ exists fs_q_fms_sum_component_compositionnegative_source. nb = fs_q_fms_sum_component_compositionnegative_source * S ((S (fms_j_sum_component_compositionnegative)) * nc) + (fms_v_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_target. fs_h_fms_sum_component_compositionnegative_target + S (fms_v_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * mc)) /\ exists fs_q_fms_sum_component_compositionnegative_target. mb = fs_q_fms_sum_component_compositionnegative_target * S ((S (fms_i_sum_component_compositionnegative)) * mc) + (fms_v_sum_component_compositionnegative)))))) -> (exists dst_positive_code_sum_source dst_positive_scale_sum_source dst_negative_code_sum_source dst_negative_scale_sum_source dst_positive_sum_sum_source dst_negative_sum_sum_source. (((F) = (((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) * S ((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) + ((((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))))) /\ (((exists fs_u_dst_sum_sourcepositive fs_v_dst_sum_sourcepositive. ((((exists fs_h_dst_sum_sourcepositive_body_start. fs_h_dst_sum_sourcepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_start. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_start * S ((S (0)) * fs_v_dst_sum_sourcepositive) + (0))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_terminal. fs_h_dst_sum_sourcepositive_body_terminal + S (dst_positive_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_terminal. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcepositive) + (dst_positive_sum_sum_source))) /\ forall fs_i_dst_sum_sourcepositive_body_steps. (exists fs_lt_dst_sum_sourcepositive_body_steps_bound. fs_lt_dst_sum_sourcepositive_body_steps_bound + S fs_i_dst_sum_sourcepositive_body_steps = l) -> exists fs_a_dst_sum_sourcepositive_body_steps fs_r_dst_sum_sourcepositive_body_steps fs_s_dst_sum_sourcepositive_body_steps. ((((exists fs_h_dst_sum_sourcepositive_body_steps_summand. fs_h_dst_sum_sourcepositive_body_steps_summand + S (fs_a_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_summand. dst_positive_code_sum_source = fs_q_dst_sum_sourcepositive_body_steps_summand * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source) + (fs_a_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_partial. fs_h_dst_sum_sourcepositive_body_steps_partial + S (fs_r_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_partial. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_partial * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_r_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_successor. fs_h_dst_sum_sourcepositive_body_steps_successor + S (fs_s_dst_sum_sourcepositive_body_steps) = S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_successor. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_successor * S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_s_dst_sum_sourcepositive_body_steps))) /\ fs_s_dst_sum_sourcepositive_body_steps = fs_r_dst_sum_sourcepositive_body_steps + fs_a_dst_sum_sourcepositive_body_steps)))))) /\ (((exists fs_u_dst_sum_sourcenegative fs_v_dst_sum_sourcenegative. ((((exists fs_h_dst_sum_sourcenegative_body_start. fs_h_dst_sum_sourcenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_start. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_start * S ((S (0)) * fs_v_dst_sum_sourcenegative) + (0))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_terminal. fs_h_dst_sum_sourcenegative_body_terminal + S (dst_negative_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_terminal. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcenegative) + (dst_negative_sum_sum_source))) /\ forall fs_i_dst_sum_sourcenegative_body_steps. (exists fs_lt_dst_sum_sourcenegative_body_steps_bound. fs_lt_dst_sum_sourcenegative_body_steps_bound + S fs_i_dst_sum_sourcenegative_body_steps = l) -> exists fs_a_dst_sum_sourcenegative_body_steps fs_r_dst_sum_sourcenegative_body_steps fs_s_dst_sum_sourcenegative_body_steps. ((((exists fs_h_dst_sum_sourcenegative_body_steps_summand. fs_h_dst_sum_sourcenegative_body_steps_summand + S (fs_a_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_summand. dst_negative_code_sum_source = fs_q_dst_sum_sourcenegative_body_steps_summand * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source) + (fs_a_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_partial. fs_h_dst_sum_sourcenegative_body_steps_partial + S (fs_r_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_partial. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_partial * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_r_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_successor. fs_h_dst_sum_sourcenegative_body_steps_successor + S (fs_s_dst_sum_sourcenegative_body_steps) = S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_successor. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_successor * S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_s_dst_sum_sourcenegative_body_steps))) /\ fs_s_dst_sum_sourcenegative_body_steps = fs_r_dst_sum_sourcenegative_body_steps + fs_a_dst_sum_sourcenegative_body_steps)))))) /\ (exists ge_balance_positive_sum_sourceresult ge_balance_negative_sum_sourceresult. (((((u) = 2 * (ge_balance_positive_sum_sourceresult) /\ (ge_balance_negative_sum_sourceresult) = 0) \/ exists ge_signed_half_sum_sourceresultdecode. (((u) = 2 * ge_signed_half_sum_sourceresultdecode + 1 /\ (ge_balance_positive_sum_sourceresult) = 0) /\ (ge_balance_negative_sum_sourceresult) = S ge_signed_half_sum_sourceresultdecode))) /\ ((dst_positive_sum_sum_source) + ge_balance_negative_sum_sourceresult = (dst_negative_sum_sum_source) + ge_balance_positive_sum_sourceresult))))))))) -> (exists dst_positive_code_sum_target dst_positive_scale_sum_target dst_negative_code_sum_target dst_negative_scale_sum_target dst_positive_sum_sum_target dst_negative_sum_sum_target. (((G) = (((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) * S ((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) + ((((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))))) /\ (((exists fs_u_dst_sum_targetpositive fs_v_dst_sum_targetpositive. ((((exists fs_h_dst_sum_targetpositive_body_start. fs_h_dst_sum_targetpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_start. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_start * S ((S (0)) * fs_v_dst_sum_targetpositive) + (0))) /\ ((((exists fs_h_dst_sum_targetpositive_body_terminal. fs_h_dst_sum_targetpositive_body_terminal + S (dst_positive_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_terminal. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_targetpositive) + (dst_positive_sum_sum_target))) /\ forall fs_i_dst_sum_targetpositive_body_steps. (exists fs_lt_dst_sum_targetpositive_body_steps_bound. fs_lt_dst_sum_targetpositive_body_steps_bound + S fs_i_dst_sum_targetpositive_body_steps = l) -> exists fs_a_dst_sum_targetpositive_body_steps fs_r_dst_sum_targetpositive_body_steps fs_s_dst_sum_targetpositive_body_steps. ((((exists fs_h_dst_sum_targetpositive_body_steps_summand. fs_h_dst_sum_targetpositive_body_steps_summand + S (fs_a_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target)) /\ exists fs_q_dst_sum_targetpositive_body_steps_summand. dst_positive_code_sum_target = fs_q_dst_sum_targetpositive_body_steps_summand * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target) + (fs_a_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_partial. fs_h_dst_sum_targetpositive_body_steps_partial + S (fs_r_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_partial. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_partial * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_r_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_successor. fs_h_dst_sum_targetpositive_body_steps_successor + S (fs_s_dst_sum_targetpositive_body_steps) = S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_successor. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_successor * S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_s_dst_sum_targetpositive_body_steps))) /\ fs_s_dst_sum_targetpositive_body_steps = fs_r_dst_sum_targetpositive_body_steps + fs_a_dst_sum_targetpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_targetnegative fs_v_dst_sum_targetnegative. ((((exists fs_h_dst_sum_targetnegative_body_start. fs_h_dst_sum_targetnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_start. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_start * S ((S (0)) * fs_v_dst_sum_targetnegative) + (0))) /\ ((((exists fs_h_dst_sum_targetnegative_body_terminal. fs_h_dst_sum_targetnegative_body_terminal + S (dst_negative_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_terminal. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_targetnegative) + (dst_negative_sum_sum_target))) /\ forall fs_i_dst_sum_targetnegative_body_steps. (exists fs_lt_dst_sum_targetnegative_body_steps_bound. fs_lt_dst_sum_targetnegative_body_steps_bound + S fs_i_dst_sum_targetnegative_body_steps = l) -> exists fs_a_dst_sum_targetnegative_body_steps fs_r_dst_sum_targetnegative_body_steps fs_s_dst_sum_targetnegative_body_steps. ((((exists fs_h_dst_sum_targetnegative_body_steps_summand. fs_h_dst_sum_targetnegative_body_steps_summand + S (fs_a_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target)) /\ exists fs_q_dst_sum_targetnegative_body_steps_summand. dst_negative_code_sum_target = fs_q_dst_sum_targetnegative_body_steps_summand * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target) + (fs_a_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_partial. fs_h_dst_sum_targetnegative_body_steps_partial + S (fs_r_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_partial. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_partial * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_r_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_successor. fs_h_dst_sum_targetnegative_body_steps_successor + S (fs_s_dst_sum_targetnegative_body_steps) = S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_successor. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_successor * S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_s_dst_sum_targetnegative_body_steps))) /\ fs_s_dst_sum_targetnegative_body_steps = fs_r_dst_sum_targetnegative_body_steps + fs_a_dst_sum_targetnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_targetresult ge_balance_negative_sum_targetresult. (((((v) = 2 * (ge_balance_positive_sum_targetresult) /\ (ge_balance_negative_sum_targetresult) = 0) \/ exists ge_signed_half_sum_targetresultdecode. (((v) = 2 * ge_signed_half_sum_targetresultdecode + 1 /\ (ge_balance_positive_sum_targetresult) = 0) /\ (ge_balance_negative_sum_targetresult) = S ge_signed_half_sum_targetresultdecode))) /\ ((dst_positive_sum_sum_target) + ge_balance_negative_sum_targetresult = (dst_negative_sum_sum_target) + ge_balance_positive_sum_targetresult))))))))) -> u = v
Complete tactic proof in conservative notation
All 96 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.