MC0014

signed_prefix_sum_pointwise_negate

Pointwise opposite canonical signed entries have opposite actual finite sums, by genuine swapped-component folds and representation independence.

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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ l. ∀ a. ∀ b. ArithNegate(F,G,l) → SignedPrefixSum(F,l,a) → SignedPrefixSum(G,l,b) → SignedNegate(a,b)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedNegate(a,b) · 3ArithAt(F,i,z) · 3SignedPrefixSum(F,l,z) · 3ArithNegate(F,G,l) · 1Lt(a,b) · 1

Actual proof prerequisites

signed_negate_total · checked external prerequisitedivisor_signed_sum_negation_transport · checked external prerequisitedivisor_signed_table_lookup_from_components · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitesigned_table_swapped_components_negation_atsigned_negate_functional · checked external prerequisitedivisor_signed_sum_extensional · checked external prerequisite
Original expanded first-order statement 
forall F G l a b. (forall mdc_index_sum_negation_entries mdc_source_sum_negation_entries mdc_target_sum_negation_entries. (exists pvs_gap_sum_negation_entriesbound. pvs_gap_sum_negation_entriesbound + S (mdc_index_sum_negation_entries) = (l)) -> (exists dst_positive_code_sum_negation_entriesfirst dst_positive_scale_sum_negation_entriesfirst dst_negative_code_sum_negation_entriesfirst dst_negative_scale_sum_negation_entriesfirst dst_positive_sum_negation_entriesfirst dst_negative_sum_negation_entriesfirst. (((F) = (((((dst_positive_code_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst)) * S ((dst_positive_code_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst)) + ((dst_positive_scale_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst))) + (((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) * S ((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) + ((dst_negative_scale_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)))) * S ((((dst_positive_code_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst)) * S ((dst_positive_code_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst)) + ((dst_positive_scale_sum_negation_entriesfirst) + (dst_positive_scale_sum_negation_entriesfirst))) + (((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) * S ((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) + ((dst_negative_scale_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)))) + ((((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) * S ((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) + ((dst_negative_scale_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst))) + (((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) * S ((dst_negative_code_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)) + ((dst_negative_scale_sum_negation_entriesfirst) + (dst_negative_scale_sum_negation_entriesfirst)))))) /\ (((((exists ff_h_pvs_sum_negation_entriesfirstpositive. ff_h_pvs_sum_negation_entriesfirstpositive + S (dst_positive_sum_negation_entriesfirst) = S ((S (mdc_index_sum_negation_entries)) * dst_positive_scale_sum_negation_entriesfirst)) /\ exists ff_q_pvs_sum_negation_entriesfirstpositive. dst_positive_code_sum_negation_entriesfirst = ff_q_pvs_sum_negation_entriesfirstpositive * S ((S (mdc_index_sum_negation_entries)) * dst_positive_scale_sum_negation_entriesfirst) + (dst_positive_sum_negation_entriesfirst))) /\ (((((exists ff_h_pvs_sum_negation_entriesfirstnegative. ff_h_pvs_sum_negation_entriesfirstnegative + S (dst_negative_sum_negation_entriesfirst) = S ((S (mdc_index_sum_negation_entries)) * dst_negative_scale_sum_negation_entriesfirst)) /\ exists ff_q_pvs_sum_negation_entriesfirstnegative. dst_negative_code_sum_negation_entriesfirst = ff_q_pvs_sum_negation_entriesfirstnegative * S ((S (mdc_index_sum_negation_entries)) * dst_negative_scale_sum_negation_entriesfirst) + (dst_negative_sum_negation_entriesfirst))) /\ (exists ge_balance_positive_sum_negation_entriesfirstvalue ge_balance_negative_sum_negation_entriesfirstvalue. (((((mdc_source_sum_negation_entries) = 2 * (ge_balance_positive_sum_negation_entriesfirstvalue) /\ (ge_balance_negative_sum_negation_entriesfirstvalue) = 0) \/ exists ge_signed_half_sum_negation_entriesfirstvaluedecode. (((mdc_source_sum_negation_entries) = 2 * ge_signed_half_sum_negation_entriesfirstvaluedecode + 1 /\ (ge_balance_positive_sum_negation_entriesfirstvalue) = 0) /\ (ge_balance_negative_sum_negation_entriesfirstvalue) = S ge_signed_half_sum_negation_entriesfirstvaluedecode))) /\ ((dst_positive_sum_negation_entriesfirst) + ge_balance_negative_sum_negation_entriesfirstvalue = (dst_negative_sum_negation_entriesfirst) + ge_balance_positive_sum_negation_entriesfirstvalue))))))))) -> (exists dst_positive_code_sum_negation_entriessecond dst_positive_scale_sum_negation_entriessecond dst_negative_code_sum_negation_entriessecond dst_negative_scale_sum_negation_entriessecond dst_positive_sum_negation_entriessecond dst_negative_sum_negation_entriessecond. (((G) = (((((dst_positive_code_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond)) * S ((dst_positive_code_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond)) + ((dst_positive_scale_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond))) + (((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) * S ((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) + ((dst_negative_scale_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)))) * S ((((dst_positive_code_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond)) * S ((dst_positive_code_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond)) + ((dst_positive_scale_sum_negation_entriessecond) + (dst_positive_scale_sum_negation_entriessecond))) + (((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) * S ((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) + ((dst_negative_scale_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)))) + ((((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) * S ((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) + ((dst_negative_scale_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond))) + (((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) * S ((dst_negative_code_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)) + ((dst_negative_scale_sum_negation_entriessecond) + (dst_negative_scale_sum_negation_entriessecond)))))) /\ (((((exists ff_h_pvs_sum_negation_entriessecondpositive. ff_h_pvs_sum_negation_entriessecondpositive + S (dst_positive_sum_negation_entriessecond) = S ((S (mdc_index_sum_negation_entries)) * dst_positive_scale_sum_negation_entriessecond)) /\ exists ff_q_pvs_sum_negation_entriessecondpositive. dst_positive_code_sum_negation_entriessecond = ff_q_pvs_sum_negation_entriessecondpositive * S ((S (mdc_index_sum_negation_entries)) * dst_positive_scale_sum_negation_entriessecond) + (dst_positive_sum_negation_entriessecond))) /\ (((((exists ff_h_pvs_sum_negation_entriessecondnegative. ff_h_pvs_sum_negation_entriessecondnegative + S (dst_negative_sum_negation_entriessecond) = S ((S (mdc_index_sum_negation_entries)) * dst_negative_scale_sum_negation_entriessecond)) /\ exists ff_q_pvs_sum_negation_entriessecondnegative. dst_negative_code_sum_negation_entriessecond = ff_q_pvs_sum_negation_entriessecondnegative * S ((S (mdc_index_sum_negation_entries)) * dst_negative_scale_sum_negation_entriessecond) + (dst_negative_sum_negation_entriessecond))) /\ (exists ge_balance_positive_sum_negation_entriessecondvalue ge_balance_negative_sum_negation_entriessecondvalue. (((((mdc_target_sum_negation_entries) = 2 * (ge_balance_positive_sum_negation_entriessecondvalue) /\ (ge_balance_negative_sum_negation_entriessecondvalue) = 0) \/ exists ge_signed_half_sum_negation_entriessecondvaluedecode. (((mdc_target_sum_negation_entries) = 2 * ge_signed_half_sum_negation_entriessecondvaluedecode + 1 /\ (ge_balance_positive_sum_negation_entriessecondvalue) = 0) /\ (ge_balance_negative_sum_negation_entriessecondvalue) = S ge_signed_half_sum_negation_entriessecondvaluedecode))) /\ ((dst_positive_sum_negation_entriessecond) + ge_balance_negative_sum_negation_entriessecondvalue = (dst_negative_sum_negation_entriessecond) + ge_balance_positive_sum_negation_entriessecondvalue))))))))) -> (exists mps_positive_sum_negation_entriesnegation mps_negative_sum_negation_entriesnegation. (((((mdc_source_sum_negation_entries) = 2 * (mps_positive_sum_negation_entriesnegation) /\ (mps_negative_sum_negation_entriesnegation) = 0) \/ exists ge_signed_half_sum_negation_entriesnegationsource. (((mdc_source_sum_negation_entries) = 2 * ge_signed_half_sum_negation_entriesnegationsource + 1 /\ (mps_positive_sum_negation_entriesnegation) = 0) /\ (mps_negative_sum_negation_entriesnegation) = S ge_signed_half_sum_negation_entriesnegationsource))) /\ ((((mdc_target_sum_negation_entries) = 2 * (mps_negative_sum_negation_entriesnegation) /\ (mps_positive_sum_negation_entriesnegation) = 0) \/ exists ge_signed_half_sum_negation_entriesnegationtarget. (((mdc_target_sum_negation_entries) = 2 * ge_signed_half_sum_negation_entriesnegationtarget + 1 /\ (mps_negative_sum_negation_entriesnegation) = 0) /\ (mps_positive_sum_negation_entriesnegation) = S ge_signed_half_sum_negation_entriesnegationtarget)))))) -> (exists dst_positive_code_sum_negation_first dst_positive_scale_sum_negation_first dst_negative_code_sum_negation_first dst_negative_scale_sum_negation_first dst_positive_sum_sum_negation_first dst_negative_sum_sum_negation_first. (((F) = (((((dst_positive_code_sum_negation_first) + (dst_positive_scale_sum_negation_first)) * S ((dst_positive_code_sum_negation_first) + (dst_positive_scale_sum_negation_first)) + ((dst_positive_scale_sum_negation_first) + (dst_positive_scale_sum_negation_first))) + (((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) * S ((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) + ((dst_negative_scale_sum_negation_first) + (dst_negative_scale_sum_negation_first)))) * S ((((dst_positive_code_sum_negation_first) + (dst_positive_scale_sum_negation_first)) * S ((dst_positive_code_sum_negation_first) + (dst_positive_scale_sum_negation_first)) + ((dst_positive_scale_sum_negation_first) + (dst_positive_scale_sum_negation_first))) + (((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) * S ((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) + ((dst_negative_scale_sum_negation_first) + (dst_negative_scale_sum_negation_first)))) + ((((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) * S ((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) + ((dst_negative_scale_sum_negation_first) + (dst_negative_scale_sum_negation_first))) + (((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) * S ((dst_negative_code_sum_negation_first) + (dst_negative_scale_sum_negation_first)) + ((dst_negative_scale_sum_negation_first) + (dst_negative_scale_sum_negation_first)))))) /\ (((exists fs_u_dst_sum_negation_firstpositive fs_v_dst_sum_negation_firstpositive. ((((exists fs_h_dst_sum_negation_firstpositive_body_start. fs_h_dst_sum_negation_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_negation_firstpositive)) /\ exists fs_q_dst_sum_negation_firstpositive_body_start. fs_u_dst_sum_negation_firstpositive = fs_q_dst_sum_negation_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_negation_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_negation_firstpositive_body_terminal. fs_h_dst_sum_negation_firstpositive_body_terminal + S (dst_positive_sum_sum_negation_first) = S ((S (l)) * fs_v_dst_sum_negation_firstpositive)) /\ exists fs_q_dst_sum_negation_firstpositive_body_terminal. fs_u_dst_sum_negation_firstpositive = fs_q_dst_sum_negation_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_negation_firstpositive) + (dst_positive_sum_sum_negation_first))) /\ forall fs_i_dst_sum_negation_firstpositive_body_steps. (exists fs_lt_dst_sum_negation_firstpositive_body_steps_bound. fs_lt_dst_sum_negation_firstpositive_body_steps_bound + S fs_i_dst_sum_negation_firstpositive_body_steps = l) -> exists fs_a_dst_sum_negation_firstpositive_body_steps fs_r_dst_sum_negation_firstpositive_body_steps fs_s_dst_sum_negation_firstpositive_body_steps. ((((exists fs_h_dst_sum_negation_firstpositive_body_steps_summand. fs_h_dst_sum_negation_firstpositive_body_steps_summand + S (fs_a_dst_sum_negation_firstpositive_body_steps) = S ((S (fs_i_dst_sum_negation_firstpositive_body_steps)) * dst_positive_scale_sum_negation_first)) /\ exists fs_q_dst_sum_negation_firstpositive_body_steps_summand. dst_positive_code_sum_negation_first = fs_q_dst_sum_negation_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_negation_firstpositive_body_steps)) * dst_positive_scale_sum_negation_first) + (fs_a_dst_sum_negation_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_negation_firstpositive_body_steps_partial. fs_h_dst_sum_negation_firstpositive_body_steps_partial + S (fs_r_dst_sum_negation_firstpositive_body_steps) = S ((S (fs_i_dst_sum_negation_firstpositive_body_steps)) * fs_v_dst_sum_negation_firstpositive)) /\ exists fs_q_dst_sum_negation_firstpositive_body_steps_partial. fs_u_dst_sum_negation_firstpositive = fs_q_dst_sum_negation_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_negation_firstpositive_body_steps)) * fs_v_dst_sum_negation_firstpositive) + (fs_r_dst_sum_negation_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_negation_firstpositive_body_steps_successor. fs_h_dst_sum_negation_firstpositive_body_steps_successor + S (fs_s_dst_sum_negation_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_negation_firstpositive_body_steps)) * fs_v_dst_sum_negation_firstpositive)) /\ exists fs_q_dst_sum_negation_firstpositive_body_steps_successor. fs_u_dst_sum_negation_firstpositive = fs_q_dst_sum_negation_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_negation_firstpositive_body_steps)) * fs_v_dst_sum_negation_firstpositive) + (fs_s_dst_sum_negation_firstpositive_body_steps))) /\ fs_s_dst_sum_negation_firstpositive_body_steps = fs_r_dst_sum_negation_firstpositive_body_steps + fs_a_dst_sum_negation_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_negation_firstnegative fs_v_dst_sum_negation_firstnegative. ((((exists fs_h_dst_sum_negation_firstnegative_body_start. fs_h_dst_sum_negation_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_negation_firstnegative)) /\ exists fs_q_dst_sum_negation_firstnegative_body_start. fs_u_dst_sum_negation_firstnegative = fs_q_dst_sum_negation_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_negation_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_negation_firstnegative_body_terminal. fs_h_dst_sum_negation_firstnegative_body_terminal + S (dst_negative_sum_sum_negation_first) = S ((S (l)) * fs_v_dst_sum_negation_firstnegative)) /\ exists fs_q_dst_sum_negation_firstnegative_body_terminal. fs_u_dst_sum_negation_firstnegative = fs_q_dst_sum_negation_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_negation_firstnegative) + (dst_negative_sum_sum_negation_first))) /\ forall fs_i_dst_sum_negation_firstnegative_body_steps. (exists fs_lt_dst_sum_negation_firstnegative_body_steps_bound. fs_lt_dst_sum_negation_firstnegative_body_steps_bound + S fs_i_dst_sum_negation_firstnegative_body_steps = l) -> exists fs_a_dst_sum_negation_firstnegative_body_steps fs_r_dst_sum_negation_firstnegative_body_steps fs_s_dst_sum_negation_firstnegative_body_steps. ((((exists fs_h_dst_sum_negation_firstnegative_body_steps_summand. fs_h_dst_sum_negation_firstnegative_body_steps_summand + S (fs_a_dst_sum_negation_firstnegative_body_steps) = S ((S (fs_i_dst_sum_negation_firstnegative_body_steps)) * dst_negative_scale_sum_negation_first)) /\ exists fs_q_dst_sum_negation_firstnegative_body_steps_summand. dst_negative_code_sum_negation_first = fs_q_dst_sum_negation_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_negation_firstnegative_body_steps)) * dst_negative_scale_sum_negation_first) + (fs_a_dst_sum_negation_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_negation_firstnegative_body_steps_partial. fs_h_dst_sum_negation_firstnegative_body_steps_partial + S (fs_r_dst_sum_negation_firstnegative_body_steps) = S ((S (fs_i_dst_sum_negation_firstnegative_body_steps)) * fs_v_dst_sum_negation_firstnegative)) /\ exists fs_q_dst_sum_negation_firstnegative_body_steps_partial. fs_u_dst_sum_negation_firstnegative = fs_q_dst_sum_negation_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_negation_firstnegative_body_steps)) * fs_v_dst_sum_negation_firstnegative) + (fs_r_dst_sum_negation_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_negation_firstnegative_body_steps_successor. fs_h_dst_sum_negation_firstnegative_body_steps_successor + S (fs_s_dst_sum_negation_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_negation_firstnegative_body_steps)) * fs_v_dst_sum_negation_firstnegative)) /\ exists fs_q_dst_sum_negation_firstnegative_body_steps_successor. fs_u_dst_sum_negation_firstnegative = fs_q_dst_sum_negation_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_negation_firstnegative_body_steps)) * fs_v_dst_sum_negation_firstnegative) + (fs_s_dst_sum_negation_firstnegative_body_steps))) /\ fs_s_dst_sum_negation_firstnegative_body_steps = fs_r_dst_sum_negation_firstnegative_body_steps + fs_a_dst_sum_negation_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_negation_firstresult ge_balance_negative_sum_negation_firstresult. (((((a) = 2 * (ge_balance_positive_sum_negation_firstresult) /\ (ge_balance_negative_sum_negation_firstresult) = 0) \/ exists ge_signed_half_sum_negation_firstresultdecode. (((a) = 2 * ge_signed_half_sum_negation_firstresultdecode + 1 /\ (ge_balance_positive_sum_negation_firstresult) = 0) /\ (ge_balance_negative_sum_negation_firstresult) = S ge_signed_half_sum_negation_firstresultdecode))) /\ ((dst_positive_sum_sum_negation_first) + ge_balance_negative_sum_negation_firstresult = (dst_negative_sum_sum_negation_first) + ge_balance_positive_sum_negation_firstresult))))))))) -> (exists dst_positive_code_sum_negation_second dst_positive_scale_sum_negation_second dst_negative_code_sum_negation_second dst_negative_scale_sum_negation_second dst_positive_sum_sum_negation_second dst_negative_sum_sum_negation_second. (((G) = (((((dst_positive_code_sum_negation_second) + (dst_positive_scale_sum_negation_second)) * S ((dst_positive_code_sum_negation_second) + (dst_positive_scale_sum_negation_second)) + ((dst_positive_scale_sum_negation_second) + (dst_positive_scale_sum_negation_second))) + (((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) * S ((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) + ((dst_negative_scale_sum_negation_second) + (dst_negative_scale_sum_negation_second)))) * S ((((dst_positive_code_sum_negation_second) + (dst_positive_scale_sum_negation_second)) * S ((dst_positive_code_sum_negation_second) + (dst_positive_scale_sum_negation_second)) + ((dst_positive_scale_sum_negation_second) + (dst_positive_scale_sum_negation_second))) + (((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) * S ((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) + ((dst_negative_scale_sum_negation_second) + (dst_negative_scale_sum_negation_second)))) + ((((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) * S ((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) + ((dst_negative_scale_sum_negation_second) + (dst_negative_scale_sum_negation_second))) + (((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) * S ((dst_negative_code_sum_negation_second) + (dst_negative_scale_sum_negation_second)) + ((dst_negative_scale_sum_negation_second) + (dst_negative_scale_sum_negation_second)))))) /\ (((exists fs_u_dst_sum_negation_secondpositive fs_v_dst_sum_negation_secondpositive. ((((exists fs_h_dst_sum_negation_secondpositive_body_start. fs_h_dst_sum_negation_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_negation_secondpositive)) /\ exists fs_q_dst_sum_negation_secondpositive_body_start. fs_u_dst_sum_negation_secondpositive = fs_q_dst_sum_negation_secondpositive_body_start * S ((S (0)) * fs_v_dst_sum_negation_secondpositive) + (0))) /\ ((((exists fs_h_dst_sum_negation_secondpositive_body_terminal. fs_h_dst_sum_negation_secondpositive_body_terminal + S (dst_positive_sum_sum_negation_second) = S ((S (l)) * fs_v_dst_sum_negation_secondpositive)) /\ exists fs_q_dst_sum_negation_secondpositive_body_terminal. fs_u_dst_sum_negation_secondpositive = fs_q_dst_sum_negation_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_negation_secondpositive) + (dst_positive_sum_sum_negation_second))) /\ forall fs_i_dst_sum_negation_secondpositive_body_steps. (exists fs_lt_dst_sum_negation_secondpositive_body_steps_bound. fs_lt_dst_sum_negation_secondpositive_body_steps_bound + S fs_i_dst_sum_negation_secondpositive_body_steps = l) -> exists fs_a_dst_sum_negation_secondpositive_body_steps fs_r_dst_sum_negation_secondpositive_body_steps fs_s_dst_sum_negation_secondpositive_body_steps. ((((exists fs_h_dst_sum_negation_secondpositive_body_steps_summand. fs_h_dst_sum_negation_secondpositive_body_steps_summand + S (fs_a_dst_sum_negation_secondpositive_body_steps) = S ((S (fs_i_dst_sum_negation_secondpositive_body_steps)) * dst_positive_scale_sum_negation_second)) /\ exists fs_q_dst_sum_negation_secondpositive_body_steps_summand. dst_positive_code_sum_negation_second = fs_q_dst_sum_negation_secondpositive_body_steps_summand * S ((S (fs_i_dst_sum_negation_secondpositive_body_steps)) * dst_positive_scale_sum_negation_second) + (fs_a_dst_sum_negation_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_negation_secondpositive_body_steps_partial. fs_h_dst_sum_negation_secondpositive_body_steps_partial + S (fs_r_dst_sum_negation_secondpositive_body_steps) = S ((S (fs_i_dst_sum_negation_secondpositive_body_steps)) * fs_v_dst_sum_negation_secondpositive)) /\ exists fs_q_dst_sum_negation_secondpositive_body_steps_partial. fs_u_dst_sum_negation_secondpositive = fs_q_dst_sum_negation_secondpositive_body_steps_partial * S ((S (fs_i_dst_sum_negation_secondpositive_body_steps)) * fs_v_dst_sum_negation_secondpositive) + (fs_r_dst_sum_negation_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_negation_secondpositive_body_steps_successor. fs_h_dst_sum_negation_secondpositive_body_steps_successor + S (fs_s_dst_sum_negation_secondpositive_body_steps) = S ((S (S fs_i_dst_sum_negation_secondpositive_body_steps)) * fs_v_dst_sum_negation_secondpositive)) /\ exists fs_q_dst_sum_negation_secondpositive_body_steps_successor. fs_u_dst_sum_negation_secondpositive = fs_q_dst_sum_negation_secondpositive_body_steps_successor * S ((S (S fs_i_dst_sum_negation_secondpositive_body_steps)) * fs_v_dst_sum_negation_secondpositive) + (fs_s_dst_sum_negation_secondpositive_body_steps))) /\ fs_s_dst_sum_negation_secondpositive_body_steps = fs_r_dst_sum_negation_secondpositive_body_steps + fs_a_dst_sum_negation_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_negation_secondnegative fs_v_dst_sum_negation_secondnegative. ((((exists fs_h_dst_sum_negation_secondnegative_body_start. fs_h_dst_sum_negation_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_negation_secondnegative)) /\ exists fs_q_dst_sum_negation_secondnegative_body_start. fs_u_dst_sum_negation_secondnegative = fs_q_dst_sum_negation_secondnegative_body_start * S ((S (0)) * fs_v_dst_sum_negation_secondnegative) + (0))) /\ ((((exists fs_h_dst_sum_negation_secondnegative_body_terminal. fs_h_dst_sum_negation_secondnegative_body_terminal + S (dst_negative_sum_sum_negation_second) = S ((S (l)) * fs_v_dst_sum_negation_secondnegative)) /\ exists fs_q_dst_sum_negation_secondnegative_body_terminal. fs_u_dst_sum_negation_secondnegative = fs_q_dst_sum_negation_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_negation_secondnegative) + (dst_negative_sum_sum_negation_second))) /\ forall fs_i_dst_sum_negation_secondnegative_body_steps. (exists fs_lt_dst_sum_negation_secondnegative_body_steps_bound. fs_lt_dst_sum_negation_secondnegative_body_steps_bound + S fs_i_dst_sum_negation_secondnegative_body_steps = l) -> exists fs_a_dst_sum_negation_secondnegative_body_steps fs_r_dst_sum_negation_secondnegative_body_steps fs_s_dst_sum_negation_secondnegative_body_steps. ((((exists fs_h_dst_sum_negation_secondnegative_body_steps_summand. fs_h_dst_sum_negation_secondnegative_body_steps_summand + S (fs_a_dst_sum_negation_secondnegative_body_steps) = S ((S (fs_i_dst_sum_negation_secondnegative_body_steps)) * dst_negative_scale_sum_negation_second)) /\ exists fs_q_dst_sum_negation_secondnegative_body_steps_summand. dst_negative_code_sum_negation_second = fs_q_dst_sum_negation_secondnegative_body_steps_summand * S ((S (fs_i_dst_sum_negation_secondnegative_body_steps)) * dst_negative_scale_sum_negation_second) + (fs_a_dst_sum_negation_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_negation_secondnegative_body_steps_partial. fs_h_dst_sum_negation_secondnegative_body_steps_partial + S (fs_r_dst_sum_negation_secondnegative_body_steps) = S ((S (fs_i_dst_sum_negation_secondnegative_body_steps)) * fs_v_dst_sum_negation_secondnegative)) /\ exists fs_q_dst_sum_negation_secondnegative_body_steps_partial. fs_u_dst_sum_negation_secondnegative = fs_q_dst_sum_negation_secondnegative_body_steps_partial * S ((S (fs_i_dst_sum_negation_secondnegative_body_steps)) * fs_v_dst_sum_negation_secondnegative) + (fs_r_dst_sum_negation_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_negation_secondnegative_body_steps_successor. fs_h_dst_sum_negation_secondnegative_body_steps_successor + S (fs_s_dst_sum_negation_secondnegative_body_steps) = S ((S (S fs_i_dst_sum_negation_secondnegative_body_steps)) * fs_v_dst_sum_negation_secondnegative)) /\ exists fs_q_dst_sum_negation_secondnegative_body_steps_successor. fs_u_dst_sum_negation_secondnegative = fs_q_dst_sum_negation_secondnegative_body_steps_successor * S ((S (S fs_i_dst_sum_negation_secondnegative_body_steps)) * fs_v_dst_sum_negation_secondnegative) + (fs_s_dst_sum_negation_secondnegative_body_steps))) /\ fs_s_dst_sum_negation_secondnegative_body_steps = fs_r_dst_sum_negation_secondnegative_body_steps + fs_a_dst_sum_negation_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_negation_secondresult ge_balance_negative_sum_negation_secondresult. (((((b) = 2 * (ge_balance_positive_sum_negation_secondresult) /\ (ge_balance_negative_sum_negation_secondresult) = 0) \/ exists ge_signed_half_sum_negation_secondresultdecode. (((b) = 2 * ge_signed_half_sum_negation_secondresultdecode + 1 /\ (ge_balance_positive_sum_negation_secondresult) = 0) /\ (ge_balance_negative_sum_negation_secondresult) = S ge_signed_half_sum_negation_secondresultdecode))) /\ ((dst_positive_sum_sum_negation_second) + ge_balance_negative_sum_negation_secondresult = (dst_negative_sum_sum_negation_second) + ge_balance_positive_sum_negation_secondresult))))))))) -> (exists mps_positive_sum_negation_result mps_negative_sum_negation_result. (((((a) = 2 * (mps_positive_sum_negation_result) /\ (mps_negative_sum_negation_result) = 0) \/ exists ge_signed_half_sum_negation_resultsource. (((a) = 2 * ge_signed_half_sum_negation_resultsource + 1 /\ (mps_positive_sum_negation_result) = 0) /\ (mps_negative_sum_negation_result) = S ge_signed_half_sum_negation_resultsource))) /\ ((((b) = 2 * (mps_negative_sum_negation_result) /\ (mps_positive_sum_negation_result) = 0) \/ exists ge_signed_half_sum_negation_resulttarget. (((b) = 2 * ge_signed_half_sum_negation_resulttarget + 1 /\ (mps_negative_sum_negation_result) = 0) /\ (mps_positive_sum_negation_result) = S ge_signed_half_sum_negation_resulttarget)))))

Complete tactic proof in conservative notation

All 103 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.

Read the argument

Proof checkpoints

103 script commands · 22 reading checkpoints · 6 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
signed table swapped components negation at
01Fix variables and assumptionsL1–8

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro l
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro hpoint
  7. L7
    intro hF
  8. L8
    intro hG
02Separate the logical casesL9–17

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

  1. L9
    cases hF
  2. L10
    cases hF_witness
  3. L11
    cases hF_witness_witness
  4. L12
    cases hF_witness_witness_witness
  5. L13
    cases hF_witness_witness_witness_witness
  6. L14
    cases hF_witness_witness_witness_witness_witness
  7. L15
    cases hF_witness_witness_witness_witness_witness_witness
  8. L16
    cases hF_witness_witness_witness_witness_witness_witness_right
  9. L17
    cases hF_witness_witness_witness_witness_witness_witness_right_right
03Establish hnL18–20

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

  1. L18
    have hn : ∃ v. SignedNegate(a,v)Definitions: SignedNegate(a,v)Original native command in the exact edition
  2. L19
    specialize signed_negate_total (a)
  3. L20
    apply signed_negate_total
04Separate the logical casesL21–21

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

  1. L21
    cases hn
05Establish hHL22–31

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

  1. L22
    have hH : SignedPrefixSum(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),l,x6)Definitions: SignedPrefixSum(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),l,x6)Original native command in the exact edition
  2. L23
    specialize divisor_signed_sum_negation_transport (F)
  3. L24
    specialize divisor_signed_sum_negation_transport (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  4. L25
    specialize divisor_signed_sum_negation_transport (x)
  5. L26
    specialize divisor_signed_sum_negation_transport (x1)
  6. L27
    specialize divisor_signed_sum_negation_transport (x2)
  7. L28
    specialize divisor_signed_sum_negation_transport (x3)
  8. L29
    specialize divisor_signed_sum_negation_transport (l)
  9. L30
    specialize divisor_signed_sum_negation_transport (a)
  10. L31
    specialize divisor_signed_sum_negation_transport (x6)
06Use earlier factsL32–33

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

  1. L32
    apply divisor_signed_sum_negation_transport
  2. L33
    exact hF_witness_witness_witness_witness_witness_witness_left
07Calculate and transport equalitiesL34–34

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

  1. L34
    refl
08Use earlier factsL35–36

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

  1. L35
    exact hF
  2. L36
    exact hn_witness
09Establish hequalL37–43

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

  1. L37
    have hequal : ∀ dst_index_sum_negation_equal. ∀ dst_first_sum_negation_equal. ∀ dst_second_sum_negation_equal. Lt(dst_index_sum_negation_equal,l) → ArithAt(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),dst_index_sum_negation_equal,dst_first_sum_negation_equal) → ArithAt(G,dst_index_sum_negation_equal,dst_second_sum_negation_equal) → dst_first_sum_negation_equal = dst_second_sum_negation_equalDefinitions: Lt(dst_index_sum_negation_equal,l)ArithAt(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),dst_index_sum_negation_equal,dst_first_sum_negation_equal)ArithAt(G,dst_index_sum_negation_equal,dst_second_sum_negation_equal)Original native command in the exact edition
  2. L38
    intro i
  3. L39
    intro u
  4. L40
    intro v
  5. L41
    intro hi
  6. L42
    intro hu
  7. L43
    intro hv
10Establish heL44–52

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

  1. L44
    have he : ∃ w. ArithAt(F,i,w)Definitions: ArithAt(F,i,w)Original native command in the exact edition
  2. L45
    specialize divisor_signed_table_lookup_from_components (F)
  3. L46
    specialize divisor_signed_table_lookup_from_components (x)
  4. L47
    specialize divisor_signed_table_lookup_from_components (x1)
  5. L48
    specialize divisor_signed_table_lookup_from_components (x2)
  6. L49
    specialize divisor_signed_table_lookup_from_components (x3)
  7. L50
    specialize divisor_signed_table_lookup_from_components (i)
  8. L51
    apply divisor_signed_table_lookup_from_components
  9. L52
    exact hF_witness_witness_witness_witness_witness_witness_left
11Separate the logical casesL53–53

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

  1. L53
    cases he
12Establish heoppL54–56

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

  1. L54
    have heopp : ∃ w. SignedNegate(x7,w)Definitions: SignedNegate(x7,w)Original native command in the exact edition
  2. L55
    specialize signed_negate_total (x7)
  3. L56
    apply signed_negate_total
13Separate the logical casesL57–57

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

  1. L57
    cases heopp
14Calculate and transport equalitiesL58–58

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

  1. L58
    trans x8
15Use earlier factsL59–68

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

  1. L59
    specialize divisor_signed_table_at_functional (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  2. L60
    specialize divisor_signed_table_at_functional (i)
  3. L61
    specialize divisor_signed_table_at_functional (u)
  4. L62
    specialize divisor_signed_table_at_functional (x8)
  5. L63
    apply divisor_signed_table_at_functional
  6. L64
    exact hu
  7. L65
    specialize signed_table_swapped_components_negation_at (F)
  8. L66
    specialize signed_table_swapped_components_negation_at (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  9. L67
    specialize signed_table_swapped_components_negation_at (x)
  10. L68
    specialize signed_table_swapped_components_negation_at (x1)
16Use earlier factsL69–75

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

  1. L69
    specialize signed_table_swapped_components_negation_at (x2)
  2. L70
    specialize signed_table_swapped_components_negation_at (x3)
  3. L71
    specialize signed_table_swapped_components_negation_at (i)
  4. L72
    specialize signed_table_swapped_components_negation_at (x7)
  5. L73
    specialize signed_table_swapped_components_negation_at (x8)
  6. L74
    apply signed_table_swapped_components_negation_at
  7. L75
    exact hF_witness_witness_witness_witness_witness_witness_left
17Calculate and transport equalitiesL76–76

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

  1. L76
    refl
18Use earlier factsL77–86

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

  1. L77
    exact he_witness
  2. L78
    exact heopp_witness
  3. L79
    specialize signed_negate_functional (x7)
  4. L80
    specialize signed_negate_functional (x8)
  5. L81
    specialize signed_negate_functional (v)
  6. L82
    apply signed_negate_functional
  7. L83
    exact heopp_witness
  8. L84
    specialize hpoint (i)
  9. L85
    specialize hpoint (x7)
  10. L86
    specialize hpoint (v)
19Use earlier factsL87–90

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

  1. L87
    apply hpoint
  2. L88
    exact hi
  3. L89
    exact he_witness
  4. L90
    exact hv
20Establish hresultL91–100

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

  1. L91
    have hresult : x6=b
  2. L92
    specialize divisor_signed_sum_extensional (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  3. L93
    specialize divisor_signed_sum_extensional (G)
  4. L94
    specialize divisor_signed_sum_extensional (l)
  5. L95
    specialize divisor_signed_sum_extensional (x6)
  6. L96
    specialize divisor_signed_sum_extensional (b)
  7. L97
    apply divisor_signed_sum_extensional
  8. L98
    exact hequal
  9. L99
    exact hH
  10. L100
    exact hG
21Calculate and transport equalitiesL101–102

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

  1. L101
    rewrite hresult at hn_witness
  2. L102
    rewrite hresult at hn_witness
22Use earlier factsL103–103

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

  1. L103
    exact hn_witness

Library-wide reading audit

Original defined command ledger · 103 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro l
  4. 0004intro a
  5. 0005intro b
  6. 0006intro hpoint
  7. 0007intro hF
  8. 0008intro hG
  9. 0009cases hF
  10. 0010cases hF_witness
  11. 0011cases hF_witness_witness
  12. 0012cases hF_witness_witness_witness
  13. 0013cases hF_witness_witness_witness_witness
  14. 0014cases hF_witness_witness_witness_witness_witness
  15. 0015cases hF_witness_witness_witness_witness_witness_witness
  16. 0016cases hF_witness_witness_witness_witness_witness_witness_right
  17. 0017cases hF_witness_witness_witness_witness_witness_witness_right_right
  18. 0018have hn : ∃ v. SignedNegate(a,v)
  19. 0019specialize signed_negate_total (a)
  20. 0020apply signed_negate_total
  21. 0021cases hn
  22. 0022have hH : SignedPrefixSum(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),l,x6)
  23. 0023specialize divisor_signed_sum_negation_transport (F)
  24. 0024specialize divisor_signed_sum_negation_transport (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  25. 0025specialize divisor_signed_sum_negation_transport (x)
  26. 0026specialize divisor_signed_sum_negation_transport (x1)
  27. 0027specialize divisor_signed_sum_negation_transport (x2)
  28. 0028specialize divisor_signed_sum_negation_transport (x3)
  29. 0029specialize divisor_signed_sum_negation_transport (l)
  30. 0030specialize divisor_signed_sum_negation_transport (a)
  31. 0031specialize divisor_signed_sum_negation_transport (x6)
  32. 0032apply divisor_signed_sum_negation_transport
  33. 0033exact hF_witness_witness_witness_witness_witness_witness_left
  34. 0034refl
  35. 0035exact hF
  36. 0036exact hn_witness
  37. 0037have hequal : ∀ dst_index_sum_negation_equal. ∀ dst_first_sum_negation_equal. ∀ dst_second_sum_negation_equal. Lt(dst_index_sum_negation_equal,l) → ArithAt(((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) · S ((x2 + x3) · S (x2 + x3) + (x3 + x3) + ((x + x1) · S (x + x1) + (x1 + x1))) + ((x + x1) · S (x + x1) + (x1 + x1) + ((x + x1) · S (x + x1) + (x1 + x1))),dst_index_sum_negation_equal,dst_first_sum_negation_equal) → ArithAt(G,dst_index_sum_negation_equal,dst_second_sum_negation_equal) → dst_first_sum_negation_equal = dst_second_sum_negation_equal
  38. 0038intro i
  39. 0039intro u
  40. 0040intro v
  41. 0041intro hi
  42. 0042intro hu
  43. 0043intro hv
  44. 0044have he : ∃ w. ArithAt(F,i,w)
  45. 0045specialize divisor_signed_table_lookup_from_components (F)
  46. 0046specialize divisor_signed_table_lookup_from_components (x)
  47. 0047specialize divisor_signed_table_lookup_from_components (x1)
  48. 0048specialize divisor_signed_table_lookup_from_components (x2)
  49. 0049specialize divisor_signed_table_lookup_from_components (x3)
  50. 0050specialize divisor_signed_table_lookup_from_components (i)
  51. 0051apply divisor_signed_table_lookup_from_components
  52. 0052exact hF_witness_witness_witness_witness_witness_witness_left
  53. 0053cases he
  54. 0054have heopp : ∃ w. SignedNegate(x7,w)
  55. 0055specialize signed_negate_total (x7)
  56. 0056apply signed_negate_total
  57. 0057cases heopp
  58. 0058trans x8
  59. 0059specialize divisor_signed_table_at_functional (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  60. 0060specialize divisor_signed_table_at_functional (i)
  61. 0061specialize divisor_signed_table_at_functional (u)
  62. 0062specialize divisor_signed_table_at_functional (x8)
  63. 0063apply divisor_signed_table_at_functional
  64. 0064exact hu
  65. 0065specialize signed_table_swapped_components_negation_at (F)
  66. 0066specialize signed_table_swapped_components_negation_at (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  67. 0067specialize signed_table_swapped_components_negation_at (x)
  68. 0068specialize signed_table_swapped_components_negation_at (x1)
  69. 0069specialize signed_table_swapped_components_negation_at (x2)
  70. 0070specialize signed_table_swapped_components_negation_at (x3)
  71. 0071specialize signed_table_swapped_components_negation_at (i)
  72. 0072specialize signed_table_swapped_components_negation_at (x7)
  73. 0073specialize signed_table_swapped_components_negation_at (x8)
  74. 0074apply signed_table_swapped_components_negation_at
  75. 0075exact hF_witness_witness_witness_witness_witness_witness_left
  76. 0076refl
  77. 0077exact he_witness
  78. 0078exact heopp_witness
  79. 0079specialize signed_negate_functional (x7)
  80. 0080specialize signed_negate_functional (x8)
  81. 0081specialize signed_negate_functional (v)
  82. 0082apply signed_negate_functional
  83. 0083exact heopp_witness
  84. 0084specialize hpoint (i)
  85. 0085specialize hpoint (x7)
  86. 0086specialize hpoint (v)
  87. 0087apply hpoint
  88. 0088exact hi
  89. 0089exact he_witness
  90. 0090exact hv
  91. 0091have hresult : x6=b
  92. 0092specialize divisor_signed_sum_extensional (((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) * S ((((x2) + (x3)) * S ((x2) + (x3)) + ((x3) + (x3))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))) + ((((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))) + (((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1)))))
  93. 0093specialize divisor_signed_sum_extensional (G)
  94. 0094specialize divisor_signed_sum_extensional (l)
  95. 0095specialize divisor_signed_sum_extensional (x6)
  96. 0096specialize divisor_signed_sum_extensional (b)
  97. 0097apply divisor_signed_sum_extensional
  98. 0098exact hequal
  99. 0099exact hH
  100. 0100exact hG
  101. 0101rewrite hresult at hn_witness
  102. 0102rewrite hresult at hn_witness
  103. 0103exact hn_witness