GF00A2

gaussian_product_swap_last_invariant

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

An actual interior/last beta swap preserves the literal canonical value of a genuine Gaussian multiplication trace, without nonzero, irreducibility or unit hypotheses.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall b c d e l i p q P Q. (exists ge_gap_swap_interior. ge_gap_swap_interior + S (i) = (l)) -> (((((exists ff_h_pfp_swap_actual_entriesoldi. ff_h_pfp_swap_actual_entriesoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_actual_entriesoldi. b = ff_q_pfp_swap_actual_entriesoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_actual_entriesoldlast. ff_h_pfp_swap_actual_entriesoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_actual_entriesoldlast. b = ff_q_pfp_swap_actual_entriesoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_actual_entriesnewi. ff_h_pfp_swap_actual_entriesnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnewi. d = ff_q_pfp_swap_actual_entriesnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_actual_entriesnewlast. ff_h_pfp_swap_actual_entriesnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnewlast. d = ff_q_pfp_swap_actual_entriesnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_actual_entries pfp_a_swap_actual_entries. (exists pfp_gap_swap_actual_entriesbound. pfp_gap_swap_actual_entriesbound + S (pfp_j_swap_actual_entries) = (S (l))) -> ~(pfp_j_swap_actual_entries = i) -> ~(pfp_j_swap_actual_entries = l) -> (((exists ff_h_pfp_swap_actual_entriesold. ff_h_pfp_swap_actual_entriesold + S (pfp_a_swap_actual_entries) = S ((S (pfp_j_swap_actual_entries)) * c)) /\ exists ff_q_pfp_swap_actual_entriesold. b = ff_q_pfp_swap_actual_entriesold * S ((S (pfp_j_swap_actual_entries)) * c) + (pfp_a_swap_actual_entries))) -> (((exists ff_h_pfp_swap_actual_entriesnew. ff_h_pfp_swap_actual_entriesnew + S (pfp_a_swap_actual_entries) = S ((S (pfp_j_swap_actual_entries)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnew. d = ff_q_pfp_swap_actual_entriesnew * S ((S (pfp_j_swap_actual_entries)) * e) + (pfp_a_swap_actual_entries)))))))))))) -> (exists gr_product_trace_swap_first_product gr_product_scale_swap_first_product. ((((exists ff_h_gprod_swap_first_productstart. ff_h_gprod_swap_first_productstart + S (6) = S ((S (0)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstart. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstart * S ((S (0)) * gr_product_scale_swap_first_product) + (6))) /\ ((((exists ff_h_gprod_swap_first_productend. ff_h_gprod_swap_first_productend + S (P) = S ((S (S l)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productend. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productend * S ((S (S l)) * gr_product_scale_swap_first_product) + (P))) /\ (forall gr_product_index_swap_first_productsteps. (exists ge_gap_swap_first_productstepsindex_bound. ge_gap_swap_first_productstepsindex_bound + S (gr_product_index_swap_first_productsteps) = (S l)) -> exists gr_product_factor_swap_first_productsteps gr_product_before_swap_first_productsteps gr_product_after_swap_first_productsteps. ((((exists ff_h_gprod_swap_first_productstepsfactor. ff_h_gprod_swap_first_productstepsfactor + S (gr_product_factor_swap_first_productsteps) = S ((S (gr_product_index_swap_first_productsteps)) * c)) /\ exists ff_q_gprod_swap_first_productstepsfactor. b = ff_q_gprod_swap_first_productstepsfactor * S ((S (gr_product_index_swap_first_productsteps)) * c) + (gr_product_factor_swap_first_productsteps))) /\ ((((exists ff_h_gprod_swap_first_productstepsbefore. ff_h_gprod_swap_first_productstepsbefore + S (gr_product_before_swap_first_productsteps) = S ((S (gr_product_index_swap_first_productsteps)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstepsbefore. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstepsbefore * S ((S (gr_product_index_swap_first_productsteps)) * gr_product_scale_swap_first_product) + (gr_product_before_swap_first_productsteps))) /\ ((((exists ff_h_gprod_swap_first_productstepsafter. ff_h_gprod_swap_first_productstepsafter + S (gr_product_after_swap_first_productsteps) = S ((S (S (gr_product_index_swap_first_productsteps))) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstepsafter. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstepsafter * S ((S (S (gr_product_index_swap_first_productsteps))) * gr_product_scale_swap_first_product) + (gr_product_after_swap_first_productsteps))) /\ (exists ge_first_rp_swap_first_productstepsmultiply ge_first_rn_swap_first_productstepsmultiply ge_first_ip_swap_first_productstepsmultiply ge_first_in_swap_first_productstepsmultiply ge_second_rp_swap_first_productstepsmultiply ge_second_rn_swap_first_productstepsmultiply ge_second_ip_swap_first_productstepsmultiply ge_second_in_swap_first_productstepsmultiply. ((exists ge_representation_real_code_swap_first_productstepsmultiplyfirst ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst. (((gr_product_before_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplyfirstreal ge_balance_negative_swap_first_productstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_first_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstreal) = S ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplyfirstreal = (ge_first_rn_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary) = S ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary = (ge_first_in_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_first_productstepsmultiplysecond ge_representation_imaginary_code_swap_first_productstepsmultiplysecond. (((gr_product_factor_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond)) * S ((ge_representation_real_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplysecondreal ge_balance_negative_swap_first_productstepsmultiplysecondreal. (((((ge_representation_real_code_swap_first_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_first_productstepsmultiplysecondreal) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplysecond) = 2 * ge_signed_half_swap_first_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondreal) = S ge_signed_half_swap_first_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplysecondreal = (ge_second_rn_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplysecondimaginary ge_balance_negative_swap_first_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_first_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) = 2 * ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondimaginary) = S ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplysecondimaginary = (ge_second_in_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_first_productstepsmultiplyoutput ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput. (((gr_product_after_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplyoutputreal ge_balance_negative_swap_first_productstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_first_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputreal) = S ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))))))) + ge_balance_negative_swap_first_productstepsmultiplyoutputreal = (((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))))))) + ge_balance_positive_swap_first_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary) = S ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))))))) + ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))))))) + ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_swap_second_product gr_product_scale_swap_second_product. ((((exists ff_h_gprod_swap_second_productstart. ff_h_gprod_swap_second_productstart + S (6) = S ((S (0)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstart. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstart * S ((S (0)) * gr_product_scale_swap_second_product) + (6))) /\ ((((exists ff_h_gprod_swap_second_productend. ff_h_gprod_swap_second_productend + S (Q) = S ((S (S l)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productend. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productend * S ((S (S l)) * gr_product_scale_swap_second_product) + (Q))) /\ (forall gr_product_index_swap_second_productsteps. (exists ge_gap_swap_second_productstepsindex_bound. ge_gap_swap_second_productstepsindex_bound + S (gr_product_index_swap_second_productsteps) = (S l)) -> exists gr_product_factor_swap_second_productsteps gr_product_before_swap_second_productsteps gr_product_after_swap_second_productsteps. ((((exists ff_h_gprod_swap_second_productstepsfactor. ff_h_gprod_swap_second_productstepsfactor + S (gr_product_factor_swap_second_productsteps) = S ((S (gr_product_index_swap_second_productsteps)) * e)) /\ exists ff_q_gprod_swap_second_productstepsfactor. d = ff_q_gprod_swap_second_productstepsfactor * S ((S (gr_product_index_swap_second_productsteps)) * e) + (gr_product_factor_swap_second_productsteps))) /\ ((((exists ff_h_gprod_swap_second_productstepsbefore. ff_h_gprod_swap_second_productstepsbefore + S (gr_product_before_swap_second_productsteps) = S ((S (gr_product_index_swap_second_productsteps)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstepsbefore. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstepsbefore * S ((S (gr_product_index_swap_second_productsteps)) * gr_product_scale_swap_second_product) + (gr_product_before_swap_second_productsteps))) /\ ((((exists ff_h_gprod_swap_second_productstepsafter. ff_h_gprod_swap_second_productstepsafter + S (gr_product_after_swap_second_productsteps) = S ((S (S (gr_product_index_swap_second_productsteps))) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstepsafter. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstepsafter * S ((S (S (gr_product_index_swap_second_productsteps))) * gr_product_scale_swap_second_product) + (gr_product_after_swap_second_productsteps))) /\ (exists ge_first_rp_swap_second_productstepsmultiply ge_first_rn_swap_second_productstepsmultiply ge_first_ip_swap_second_productstepsmultiply ge_first_in_swap_second_productstepsmultiply ge_second_rp_swap_second_productstepsmultiply ge_second_rn_swap_second_productstepsmultiply ge_second_ip_swap_second_productstepsmultiply ge_second_in_swap_second_productstepsmultiply. ((exists ge_representation_real_code_swap_second_productstepsmultiplyfirst ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst. (((gr_product_before_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplyfirstreal ge_balance_negative_swap_second_productstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_second_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstreal) = S ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplyfirstreal = (ge_first_rn_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary) = S ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary = (ge_first_in_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_second_productstepsmultiplysecond ge_representation_imaginary_code_swap_second_productstepsmultiplysecond. (((gr_product_factor_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond)) * S ((ge_representation_real_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplysecondreal ge_balance_negative_swap_second_productstepsmultiplysecondreal. (((((ge_representation_real_code_swap_second_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_second_productstepsmultiplysecondreal) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplysecond) = 2 * ge_signed_half_swap_second_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondreal) = S ge_signed_half_swap_second_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplysecondreal = (ge_second_rn_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplysecondimaginary ge_balance_negative_swap_second_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_second_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) = 2 * ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondimaginary) = S ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplysecondimaginary = (ge_second_in_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_second_productstepsmultiplyoutput ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput. (((gr_product_after_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplyoutputreal ge_balance_negative_swap_second_productstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_second_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputreal) = S ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))))))) + ge_balance_negative_swap_second_productstepsmultiplyoutputreal = (((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))))))) + ge_balance_positive_swap_second_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary) = S ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))))))) + ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))))))) + ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary)))))))))))))))) -> P=Q

Constructive proof overview

Generated structural guide

An actual interior/last beta swap preserves the literal canonical value of a genuine Gaussian multiplication trace, without nonzero, irreducibility or unit hypotheses.

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

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

Proof neighborhood

Direct dependencies

GF0089 gaussian_product_successor_decompose beta_at_unique Stable theorem; checked-use authorized gaussian_multiply_functional Alpha theorem; checked-use authorized GF00A0 gaussian_product_replace_balance le_succ Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized

Direct dependents

GF00AE gaussian_factor_swapped_product_exists

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

103 script commands · 18 reading checkpoints · 4 local claims

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

Named ingredients (2)
gaussian product successor decomposegaussian product replace balance

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 b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro i
  7. L7
    intro p
  8. L8
    intro q
  9. L9
    intro P
  10. L10
    intro Q
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hi
  2. L12
    intro hswap
  3. L13
    intro hP
  4. L14
    intro hQ
03Separate the logical casesL15–18

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

  1. L15
    cases hswap
  2. L16
    cases hswap_right
  3. L17
    cases hswap_right_right
  4. L18
    cases hswap_right_right_right
04Establish holdL19–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

  1. L19
    have hold : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,P))Definitions: GMulGProductBetaAt
  2. L20
    specialize gaussian_product_successor_decompose (b)
  3. L21
    specialize gaussian_product_successor_decompose (c)
  4. L22
    specialize gaussian_product_successor_decompose (l)
  5. L23
    specialize gaussian_product_successor_decompose (P)
  6. L24
    apply gaussian_product_successor_decompose
  7. L25
    exact hP
05Establish hnewL26–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

  1. L26
    have hnew : ∃ a. ∃ R. BetaAt(d,e,l,a) ∧ (GProduct(d,e,l,R) ∧ GMul(R,a,Q))Definitions: GMulGProductBetaAt
  2. L27
    specialize gaussian_product_successor_decompose (d)
  3. L28
    specialize gaussian_product_successor_decompose (e)
  4. L29
    specialize gaussian_product_successor_decompose (l)
  5. L30
    specialize gaussian_product_successor_decompose (Q)
  6. L31
    apply gaussian_product_successor_decompose
  7. L32
    exact hQ
06Separate the logical casesL33–40

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

  1. L33
    cases hold
  2. L34
    cases hold_witness
  3. L35
    cases hold_witness_witness
  4. L36
    cases hold_witness_witness_right
  5. L37
    cases hnew
  6. L38
    cases hnew_witness
  7. L39
    cases hnew_witness_witness
  8. L40
    cases hnew_witness_witness_right
07Establish hlastoldL41–49

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

  1. L41
    have hlastold : x=q
  2. L42
    specialize beta_at_unique (b)
  3. L43
    specialize beta_at_unique (c)
  4. L44
    specialize beta_at_unique (l)
  5. L45
    specialize beta_at_unique (x)
  6. L46
    specialize beta_at_unique (q)
  7. L47
    apply beta_at_unique
  8. L48
    exact hold_witness_witness_left
  9. L49
    exact hswap_right_left
08Establish hlastnewL50–59

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

  1. L50
    have hlastnew : x2=p
  2. L51
    specialize beta_at_unique (d)
  3. L52
    specialize beta_at_unique (e)
  4. L53
    specialize beta_at_unique (l)
  5. L54
    specialize beta_at_unique (x2)
  6. L55
    specialize beta_at_unique (p)
  7. L56
    apply beta_at_unique
  8. L57
    exact hnew_witness_witness_left
  9. L58
    exact hswap_right_right_right_left
  10. L59
    rewrite hlastold at hold_witness_witness_right_right
09Calculate and transport equalitiesL60–60

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

  1. L60
    rewrite hlastnew at hnew_witness_witness_right_right
10Use earlier factsL61–70

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

  1. L61
    specialize gaussian_multiply_functional (x1)
  2. L62
    specialize gaussian_multiply_functional (q)
  3. L63
    specialize gaussian_multiply_functional (P)
  4. L64
    specialize gaussian_multiply_functional (Q)
  5. L65
    apply gaussian_multiply_functional
  6. L66
    exact hold_witness_witness_right_right
  7. L67
    specialize gaussian_product_replace_balance (l)
  8. L68
    specialize gaussian_product_replace_balance (b)
  9. L69
    specialize gaussian_product_replace_balance (c)
  10. L70
    specialize gaussian_product_replace_balance (d)
11Use earlier factsL71–80

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

  1. L71
    specialize gaussian_product_replace_balance (e)
  2. L72
    specialize gaussian_product_replace_balance (i)
  3. L73
    specialize gaussian_product_replace_balance (p)
  4. L74
    specialize gaussian_product_replace_balance (q)
  5. L75
    specialize gaussian_product_replace_balance (x1)
  6. L76
    specialize gaussian_product_replace_balance (x3)
  7. L77
    specialize gaussian_product_replace_balance (Q)
  8. L78
    apply gaussian_product_replace_balance
  9. L79
    exact hi
  10. L80
    exact hswap_left
12Use earlier factsL81–81

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

  1. L81
    exact hswap_right_right_left
13Fix variables and assumptionsL82–86

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

  1. L82
    intro j
  2. L83
    intro a
  3. L84
    intro hj
  4. L85
    intro hne
  5. L86
    intro hentry
14Use earlier factsL87–94

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

  1. L87
    specialize hswap_right_right_right_right (j)
  2. L88
    specialize hswap_right_right_right_right (a)
  3. L89
    apply hswap_right_right_right_right
  4. L90
    specialize le_succ (S j)
  5. L91
    specialize le_succ (l)
  6. L92
    apply le_succ
  7. L93
    exact hj
  8. L94
    exact hne
15Fix variables and assumptionsL95–95

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

  1. L95
    intro heq
16Use earlier factsL96–97

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

  1. L96
    specialize lt_irrefl_expanded (l)
  2. L97
    apply lt_irrefl_expanded
17Calculate and transport equalitiesL98–98

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

  1. L98
    rewrite heq at hj
18Use earlier factsL99–103

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

  1. L99
    exact hj
  2. L100
    exact hentry
  3. L101
    exact hold_witness_witness_right_left
  4. L102
    exact hnew_witness_witness_right_left
  5. L103
    exact hnew_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 103 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro i
  7. 0007intro p
  8. 0008intro q
  9. 0009intro P
  10. 0010intro Q
  11. 0011intro hi
  12. 0012intro hswap
  13. 0013intro hP
  14. 0014intro hQ
  15. 0015cases hswap
  16. 0016cases hswap_right
  17. 0017cases hswap_right_right
  18. 0018cases hswap_right_right_right
  19. 0019have hold : exists a R. ((((exists ff_h_gprod_swap_oldfactor. ff_h_gprod_swap_oldfactor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_swap_oldfactor. b = ff_q_gprod_swap_oldfactor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_swap_oldprefix gr_product_scale_swap_oldprefix. ((((exists ff_h_gprod_swap_oldprefixstart. ff_h_gprod_swap_oldprefixstart + S (6) = S ((S (0)) * gr_product_scale_swap_oldprefix)) /\ exists ff_q_gprod_swap_oldprefixstart. gr_product_trace_swap_oldprefix = ff_q_gprod_swap_oldprefixstart * S ((S (0)) * gr_product_scale_swap_oldprefix) + (6))) /\ ((((exists ff_h_gprod_swap_oldprefixend. ff_h_gprod_swap_oldprefixend + S (R) = S ((S (l)) * gr_product_scale_swap_oldprefix)) /\ exists ff_q_gprod_swap_oldprefixend. gr_product_trace_swap_oldprefix = ff_q_gprod_swap_oldprefixend * S ((S (l)) * gr_product_scale_swap_oldprefix) + (R))) /\ (forall gr_product_index_swap_oldprefixsteps. (exists ge_gap_swap_oldprefixstepsindex_bound. ge_gap_swap_oldprefixstepsindex_bound + S (gr_product_index_swap_oldprefixsteps) = (l)) -> exists gr_product_factor_swap_oldprefixsteps gr_product_before_swap_oldprefixsteps gr_product_after_swap_oldprefixsteps. ((((exists ff_h_gprod_swap_oldprefixstepsfactor. ff_h_gprod_swap_oldprefixstepsfactor + S (gr_product_factor_swap_oldprefixsteps) = S ((S (gr_product_index_swap_oldprefixsteps)) * c)) /\ exists ff_q_gprod_swap_oldprefixstepsfactor. b = ff_q_gprod_swap_oldprefixstepsfactor * S ((S (gr_product_index_swap_oldprefixsteps)) * c) + (gr_product_factor_swap_oldprefixsteps))) /\ ((((exists ff_h_gprod_swap_oldprefixstepsbefore. ff_h_gprod_swap_oldprefixstepsbefore + S (gr_product_before_swap_oldprefixsteps) = S ((S (gr_product_index_swap_oldprefixsteps)) * gr_product_scale_swap_oldprefix)) /\ exists ff_q_gprod_swap_oldprefixstepsbefore. gr_product_trace_swap_oldprefix = ff_q_gprod_swap_oldprefixstepsbefore * S ((S (gr_product_index_swap_oldprefixsteps)) * gr_product_scale_swap_oldprefix) + (gr_product_before_swap_oldprefixsteps))) /\ ((((exists ff_h_gprod_swap_oldprefixstepsafter. ff_h_gprod_swap_oldprefixstepsafter + S (gr_product_after_swap_oldprefixsteps) = S ((S (S (gr_product_index_swap_oldprefixsteps))) * gr_product_scale_swap_oldprefix)) /\ exists ff_q_gprod_swap_oldprefixstepsafter. gr_product_trace_swap_oldprefix = ff_q_gprod_swap_oldprefixstepsafter * S ((S (S (gr_product_index_swap_oldprefixsteps))) * gr_product_scale_swap_oldprefix) + (gr_product_after_swap_oldprefixsteps))) /\ (exists ge_first_rp_swap_oldprefixstepsmultiply ge_first_rn_swap_oldprefixstepsmultiply ge_first_ip_swap_oldprefixstepsmultiply ge_first_in_swap_oldprefixstepsmultiply ge_second_rp_swap_oldprefixstepsmultiply ge_second_rn_swap_oldprefixstepsmultiply ge_second_ip_swap_oldprefixstepsmultiply ge_second_in_swap_oldprefixstepsmultiply. ((exists ge_representation_real_code_swap_oldprefixstepsmultiplyfirst ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst. (((gr_product_before_swap_oldprefixsteps) = ((ge_representation_real_code_swap_oldprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_oldprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_oldprefixstepsmultiplyfirstreal ge_balance_negative_swap_oldprefixstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_oldprefixstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_oldprefixstepsmultiplyfirst) = 2 * ge_signed_half_swap_oldprefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyfirstreal) = S ge_signed_half_swap_oldprefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_oldprefixstepsmultiply) + ge_balance_negative_swap_oldprefixstepsmultiplyfirstreal = (ge_first_rn_swap_oldprefixstepsmultiply) + ge_balance_positive_swap_oldprefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_oldprefixstepsmultiplyfirstimaginary ge_balance_negative_swap_oldprefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyfirst) = 2 * ge_signed_half_swap_oldprefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyfirstimaginary) = S ge_signed_half_swap_oldprefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_oldprefixstepsmultiply) + ge_balance_negative_swap_oldprefixstepsmultiplyfirstimaginary = (ge_first_in_swap_oldprefixstepsmultiply) + ge_balance_positive_swap_oldprefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_oldprefixstepsmultiplysecond ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond. (((gr_product_factor_swap_oldprefixsteps) = ((ge_representation_real_code_swap_oldprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond)) * S ((ge_representation_real_code_swap_oldprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_oldprefixstepsmultiplysecondreal ge_balance_negative_swap_oldprefixstepsmultiplysecondreal. (((((ge_representation_real_code_swap_oldprefixstepsmultiplysecond) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplysecondreal) /\ (ge_balance_negative_swap_oldprefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_oldprefixstepsmultiplysecond) = 2 * ge_signed_half_swap_oldprefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplysecondreal) = S ge_signed_half_swap_oldprefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_oldprefixstepsmultiply) + ge_balance_negative_swap_oldprefixstepsmultiplysecondreal = (ge_second_rn_swap_oldprefixstepsmultiply) + ge_balance_positive_swap_oldprefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_oldprefixstepsmultiplysecondimaginary ge_balance_negative_swap_oldprefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_oldprefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_oldprefixstepsmultiplysecond) = 2 * ge_signed_half_swap_oldprefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplysecondimaginary) = S ge_signed_half_swap_oldprefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_oldprefixstepsmultiply) + ge_balance_negative_swap_oldprefixstepsmultiplysecondimaginary = (ge_second_in_swap_oldprefixstepsmultiply) + ge_balance_positive_swap_oldprefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_oldprefixstepsmultiplyoutput ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput. (((gr_product_after_swap_oldprefixsteps) = ((ge_representation_real_code_swap_oldprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_oldprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_oldprefixstepsmultiplyoutputreal ge_balance_negative_swap_oldprefixstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_oldprefixstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_oldprefixstepsmultiplyoutput) = 2 * ge_signed_half_swap_oldprefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyoutputreal) = S ge_signed_half_swap_oldprefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_oldprefixstepsmultiply) * (ge_second_rp_swap_oldprefixstepsmultiply))) + (((ge_first_rn_swap_oldprefixstepsmultiply) * (ge_second_rn_swap_oldprefixstepsmultiply))))) + (((((ge_first_ip_swap_oldprefixstepsmultiply) * (ge_second_in_swap_oldprefixstepsmultiply))) + (((ge_first_in_swap_oldprefixstepsmultiply) * (ge_second_ip_swap_oldprefixstepsmultiply))))))) + ge_balance_negative_swap_oldprefixstepsmultiplyoutputreal = (((((((ge_first_rp_swap_oldprefixstepsmultiply) * (ge_second_rn_swap_oldprefixstepsmultiply))) + (((ge_first_rn_swap_oldprefixstepsmultiply) * (ge_second_rp_swap_oldprefixstepsmultiply))))) + (((((ge_first_ip_swap_oldprefixstepsmultiply) * (ge_second_ip_swap_oldprefixstepsmultiply))) + (((ge_first_in_swap_oldprefixstepsmultiply) * (ge_second_in_swap_oldprefixstepsmultiply))))))) + ge_balance_positive_swap_oldprefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_oldprefixstepsmultiplyoutputimaginary ge_balance_negative_swap_oldprefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_oldprefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_oldprefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_oldprefixstepsmultiplyoutput) = 2 * ge_signed_half_swap_oldprefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_oldprefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_oldprefixstepsmultiplyoutputimaginary) = S ge_signed_half_swap_oldprefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_oldprefixstepsmultiply) * (ge_second_ip_swap_oldprefixstepsmultiply))) + (((ge_first_rn_swap_oldprefixstepsmultiply) * (ge_second_in_swap_oldprefixstepsmultiply))))) + (((((ge_first_ip_swap_oldprefixstepsmultiply) * (ge_second_rp_swap_oldprefixstepsmultiply))) + (((ge_first_in_swap_oldprefixstepsmultiply) * (ge_second_rn_swap_oldprefixstepsmultiply))))))) + ge_balance_negative_swap_oldprefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_oldprefixstepsmultiply) * (ge_second_in_swap_oldprefixstepsmultiply))) + (((ge_first_rn_swap_oldprefixstepsmultiply) * (ge_second_ip_swap_oldprefixstepsmultiply))))) + (((((ge_first_ip_swap_oldprefixstepsmultiply) * (ge_second_rn_swap_oldprefixstepsmultiply))) + (((ge_first_in_swap_oldprefixstepsmultiply) * (ge_second_rp_swap_oldprefixstepsmultiply))))))) + ge_balance_positive_swap_oldprefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_swap_oldlast ge_first_rn_swap_oldlast ge_first_ip_swap_oldlast ge_first_in_swap_oldlast ge_second_rp_swap_oldlast ge_second_rn_swap_oldlast ge_second_ip_swap_oldlast ge_second_in_swap_oldlast. ((exists ge_representation_real_code_swap_oldlastfirst ge_representation_imaginary_code_swap_oldlastfirst. (((R) = ((ge_representation_real_code_swap_oldlastfirst) + (ge_representation_imaginary_code_swap_oldlastfirst)) * S ((ge_representation_real_code_swap_oldlastfirst) + (ge_representation_imaginary_code_swap_oldlastfirst)) + ((ge_representation_imaginary_code_swap_oldlastfirst) + (ge_representation_imaginary_code_swap_oldlastfirst))) /\ ((exists ge_balance_positive_swap_oldlastfirstreal ge_balance_negative_swap_oldlastfirstreal. (((((ge_representation_real_code_swap_oldlastfirst) = 2 * (ge_balance_positive_swap_oldlastfirstreal) /\ (ge_balance_negative_swap_oldlastfirstreal) = 0) \/ exists ge_signed_half_swap_oldlastfirstrealdecode. (((ge_representation_real_code_swap_oldlastfirst) = 2 * ge_signed_half_swap_oldlastfirstrealdecode + 1 /\ (ge_balance_positive_swap_oldlastfirstreal) = 0) /\ (ge_balance_negative_swap_oldlastfirstreal) = S ge_signed_half_swap_oldlastfirstrealdecode))) /\ ((ge_first_rp_swap_oldlast) + ge_balance_negative_swap_oldlastfirstreal = (ge_first_rn_swap_oldlast) + ge_balance_positive_swap_oldlastfirstreal))) /\ (exists ge_balance_positive_swap_oldlastfirstimaginary ge_balance_negative_swap_oldlastfirstimaginary. (((((ge_representation_imaginary_code_swap_oldlastfirst) = 2 * (ge_balance_positive_swap_oldlastfirstimaginary) /\ (ge_balance_negative_swap_oldlastfirstimaginary) = 0) \/ exists ge_signed_half_swap_oldlastfirstimaginarydecode. (((ge_representation_imaginary_code_swap_oldlastfirst) = 2 * ge_signed_half_swap_oldlastfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_oldlastfirstimaginary) = 0) /\ (ge_balance_negative_swap_oldlastfirstimaginary) = S ge_signed_half_swap_oldlastfirstimaginarydecode))) /\ ((ge_first_ip_swap_oldlast) + ge_balance_negative_swap_oldlastfirstimaginary = (ge_first_in_swap_oldlast) + ge_balance_positive_swap_oldlastfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_oldlastsecond ge_representation_imaginary_code_swap_oldlastsecond. (((a) = ((ge_representation_real_code_swap_oldlastsecond) + (ge_representation_imaginary_code_swap_oldlastsecond)) * S ((ge_representation_real_code_swap_oldlastsecond) + (ge_representation_imaginary_code_swap_oldlastsecond)) + ((ge_representation_imaginary_code_swap_oldlastsecond) + (ge_representation_imaginary_code_swap_oldlastsecond))) /\ ((exists ge_balance_positive_swap_oldlastsecondreal ge_balance_negative_swap_oldlastsecondreal. (((((ge_representation_real_code_swap_oldlastsecond) = 2 * (ge_balance_positive_swap_oldlastsecondreal) /\ (ge_balance_negative_swap_oldlastsecondreal) = 0) \/ exists ge_signed_half_swap_oldlastsecondrealdecode. (((ge_representation_real_code_swap_oldlastsecond) = 2 * ge_signed_half_swap_oldlastsecondrealdecode + 1 /\ (ge_balance_positive_swap_oldlastsecondreal) = 0) /\ (ge_balance_negative_swap_oldlastsecondreal) = S ge_signed_half_swap_oldlastsecondrealdecode))) /\ ((ge_second_rp_swap_oldlast) + ge_balance_negative_swap_oldlastsecondreal = (ge_second_rn_swap_oldlast) + ge_balance_positive_swap_oldlastsecondreal))) /\ (exists ge_balance_positive_swap_oldlastsecondimaginary ge_balance_negative_swap_oldlastsecondimaginary. (((((ge_representation_imaginary_code_swap_oldlastsecond) = 2 * (ge_balance_positive_swap_oldlastsecondimaginary) /\ (ge_balance_negative_swap_oldlastsecondimaginary) = 0) \/ exists ge_signed_half_swap_oldlastsecondimaginarydecode. (((ge_representation_imaginary_code_swap_oldlastsecond) = 2 * ge_signed_half_swap_oldlastsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_oldlastsecondimaginary) = 0) /\ (ge_balance_negative_swap_oldlastsecondimaginary) = S ge_signed_half_swap_oldlastsecondimaginarydecode))) /\ ((ge_second_ip_swap_oldlast) + ge_balance_negative_swap_oldlastsecondimaginary = (ge_second_in_swap_oldlast) + ge_balance_positive_swap_oldlastsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_oldlastoutput ge_representation_imaginary_code_swap_oldlastoutput. (((P) = ((ge_representation_real_code_swap_oldlastoutput) + (ge_representation_imaginary_code_swap_oldlastoutput)) * S ((ge_representation_real_code_swap_oldlastoutput) + (ge_representation_imaginary_code_swap_oldlastoutput)) + ((ge_representation_imaginary_code_swap_oldlastoutput) + (ge_representation_imaginary_code_swap_oldlastoutput))) /\ ((exists ge_balance_positive_swap_oldlastoutputreal ge_balance_negative_swap_oldlastoutputreal. (((((ge_representation_real_code_swap_oldlastoutput) = 2 * (ge_balance_positive_swap_oldlastoutputreal) /\ (ge_balance_negative_swap_oldlastoutputreal) = 0) \/ exists ge_signed_half_swap_oldlastoutputrealdecode. (((ge_representation_real_code_swap_oldlastoutput) = 2 * ge_signed_half_swap_oldlastoutputrealdecode + 1 /\ (ge_balance_positive_swap_oldlastoutputreal) = 0) /\ (ge_balance_negative_swap_oldlastoutputreal) = S ge_signed_half_swap_oldlastoutputrealdecode))) /\ ((((((((ge_first_rp_swap_oldlast) * (ge_second_rp_swap_oldlast))) + (((ge_first_rn_swap_oldlast) * (ge_second_rn_swap_oldlast))))) + (((((ge_first_ip_swap_oldlast) * (ge_second_in_swap_oldlast))) + (((ge_first_in_swap_oldlast) * (ge_second_ip_swap_oldlast))))))) + ge_balance_negative_swap_oldlastoutputreal = (((((((ge_first_rp_swap_oldlast) * (ge_second_rn_swap_oldlast))) + (((ge_first_rn_swap_oldlast) * (ge_second_rp_swap_oldlast))))) + (((((ge_first_ip_swap_oldlast) * (ge_second_ip_swap_oldlast))) + (((ge_first_in_swap_oldlast) * (ge_second_in_swap_oldlast))))))) + ge_balance_positive_swap_oldlastoutputreal))) /\ (exists ge_balance_positive_swap_oldlastoutputimaginary ge_balance_negative_swap_oldlastoutputimaginary. (((((ge_representation_imaginary_code_swap_oldlastoutput) = 2 * (ge_balance_positive_swap_oldlastoutputimaginary) /\ (ge_balance_negative_swap_oldlastoutputimaginary) = 0) \/ exists ge_signed_half_swap_oldlastoutputimaginarydecode. (((ge_representation_imaginary_code_swap_oldlastoutput) = 2 * ge_signed_half_swap_oldlastoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_oldlastoutputimaginary) = 0) /\ (ge_balance_negative_swap_oldlastoutputimaginary) = S ge_signed_half_swap_oldlastoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_oldlast) * (ge_second_ip_swap_oldlast))) + (((ge_first_rn_swap_oldlast) * (ge_second_in_swap_oldlast))))) + (((((ge_first_ip_swap_oldlast) * (ge_second_rp_swap_oldlast))) + (((ge_first_in_swap_oldlast) * (ge_second_rn_swap_oldlast))))))) + ge_balance_negative_swap_oldlastoutputimaginary = (((((((ge_first_rp_swap_oldlast) * (ge_second_in_swap_oldlast))) + (((ge_first_rn_swap_oldlast) * (ge_second_ip_swap_oldlast))))) + (((((ge_first_ip_swap_oldlast) * (ge_second_rn_swap_oldlast))) + (((ge_first_in_swap_oldlast) * (ge_second_rp_swap_oldlast))))))) + ge_balance_positive_swap_oldlastoutputimaginary)))))))))))
  20. 0020specialize gaussian_product_successor_decompose (b)
  21. 0021specialize gaussian_product_successor_decompose (c)
  22. 0022specialize gaussian_product_successor_decompose (l)
  23. 0023specialize gaussian_product_successor_decompose (P)
  24. 0024apply gaussian_product_successor_decompose
  25. 0025exact hP
  26. 0026have hnew : exists a R. ((((exists ff_h_gprod_swap_newfactor. ff_h_gprod_swap_newfactor + S (a) = S ((S (l)) * e)) /\ exists ff_q_gprod_swap_newfactor. d = ff_q_gprod_swap_newfactor * S ((S (l)) * e) + (a))) /\ ((exists gr_product_trace_swap_newprefix gr_product_scale_swap_newprefix. ((((exists ff_h_gprod_swap_newprefixstart. ff_h_gprod_swap_newprefixstart + S (6) = S ((S (0)) * gr_product_scale_swap_newprefix)) /\ exists ff_q_gprod_swap_newprefixstart. gr_product_trace_swap_newprefix = ff_q_gprod_swap_newprefixstart * S ((S (0)) * gr_product_scale_swap_newprefix) + (6))) /\ ((((exists ff_h_gprod_swap_newprefixend. ff_h_gprod_swap_newprefixend + S (R) = S ((S (l)) * gr_product_scale_swap_newprefix)) /\ exists ff_q_gprod_swap_newprefixend. gr_product_trace_swap_newprefix = ff_q_gprod_swap_newprefixend * S ((S (l)) * gr_product_scale_swap_newprefix) + (R))) /\ (forall gr_product_index_swap_newprefixsteps. (exists ge_gap_swap_newprefixstepsindex_bound. ge_gap_swap_newprefixstepsindex_bound + S (gr_product_index_swap_newprefixsteps) = (l)) -> exists gr_product_factor_swap_newprefixsteps gr_product_before_swap_newprefixsteps gr_product_after_swap_newprefixsteps. ((((exists ff_h_gprod_swap_newprefixstepsfactor. ff_h_gprod_swap_newprefixstepsfactor + S (gr_product_factor_swap_newprefixsteps) = S ((S (gr_product_index_swap_newprefixsteps)) * e)) /\ exists ff_q_gprod_swap_newprefixstepsfactor. d = ff_q_gprod_swap_newprefixstepsfactor * S ((S (gr_product_index_swap_newprefixsteps)) * e) + (gr_product_factor_swap_newprefixsteps))) /\ ((((exists ff_h_gprod_swap_newprefixstepsbefore. ff_h_gprod_swap_newprefixstepsbefore + S (gr_product_before_swap_newprefixsteps) = S ((S (gr_product_index_swap_newprefixsteps)) * gr_product_scale_swap_newprefix)) /\ exists ff_q_gprod_swap_newprefixstepsbefore. gr_product_trace_swap_newprefix = ff_q_gprod_swap_newprefixstepsbefore * S ((S (gr_product_index_swap_newprefixsteps)) * gr_product_scale_swap_newprefix) + (gr_product_before_swap_newprefixsteps))) /\ ((((exists ff_h_gprod_swap_newprefixstepsafter. ff_h_gprod_swap_newprefixstepsafter + S (gr_product_after_swap_newprefixsteps) = S ((S (S (gr_product_index_swap_newprefixsteps))) * gr_product_scale_swap_newprefix)) /\ exists ff_q_gprod_swap_newprefixstepsafter. gr_product_trace_swap_newprefix = ff_q_gprod_swap_newprefixstepsafter * S ((S (S (gr_product_index_swap_newprefixsteps))) * gr_product_scale_swap_newprefix) + (gr_product_after_swap_newprefixsteps))) /\ (exists ge_first_rp_swap_newprefixstepsmultiply ge_first_rn_swap_newprefixstepsmultiply ge_first_ip_swap_newprefixstepsmultiply ge_first_in_swap_newprefixstepsmultiply ge_second_rp_swap_newprefixstepsmultiply ge_second_rn_swap_newprefixstepsmultiply ge_second_ip_swap_newprefixstepsmultiply ge_second_in_swap_newprefixstepsmultiply. ((exists ge_representation_real_code_swap_newprefixstepsmultiplyfirst ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst. (((gr_product_before_swap_newprefixsteps) = ((ge_representation_real_code_swap_newprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_newprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_newprefixstepsmultiplyfirstreal ge_balance_negative_swap_newprefixstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_newprefixstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_newprefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_newprefixstepsmultiplyfirst) = 2 * ge_signed_half_swap_newprefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplyfirstreal) = S ge_signed_half_swap_newprefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_newprefixstepsmultiply) + ge_balance_negative_swap_newprefixstepsmultiplyfirstreal = (ge_first_rn_swap_newprefixstepsmultiply) + ge_balance_positive_swap_newprefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_newprefixstepsmultiplyfirstimaginary ge_balance_negative_swap_newprefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_newprefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_newprefixstepsmultiplyfirst) = 2 * ge_signed_half_swap_newprefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplyfirstimaginary) = S ge_signed_half_swap_newprefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_newprefixstepsmultiply) + ge_balance_negative_swap_newprefixstepsmultiplyfirstimaginary = (ge_first_in_swap_newprefixstepsmultiply) + ge_balance_positive_swap_newprefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_newprefixstepsmultiplysecond ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond. (((gr_product_factor_swap_newprefixsteps) = ((ge_representation_real_code_swap_newprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond)) * S ((ge_representation_real_code_swap_newprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_newprefixstepsmultiplysecondreal ge_balance_negative_swap_newprefixstepsmultiplysecondreal. (((((ge_representation_real_code_swap_newprefixstepsmultiplysecond) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplysecondreal) /\ (ge_balance_negative_swap_newprefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_newprefixstepsmultiplysecond) = 2 * ge_signed_half_swap_newprefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplysecondreal) = S ge_signed_half_swap_newprefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_newprefixstepsmultiply) + ge_balance_negative_swap_newprefixstepsmultiplysecondreal = (ge_second_rn_swap_newprefixstepsmultiply) + ge_balance_positive_swap_newprefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_newprefixstepsmultiplysecondimaginary ge_balance_negative_swap_newprefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_newprefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_newprefixstepsmultiplysecond) = 2 * ge_signed_half_swap_newprefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplysecondimaginary) = S ge_signed_half_swap_newprefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_newprefixstepsmultiply) + ge_balance_negative_swap_newprefixstepsmultiplysecondimaginary = (ge_second_in_swap_newprefixstepsmultiply) + ge_balance_positive_swap_newprefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_newprefixstepsmultiplyoutput ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput. (((gr_product_after_swap_newprefixsteps) = ((ge_representation_real_code_swap_newprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_newprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_newprefixstepsmultiplyoutputreal ge_balance_negative_swap_newprefixstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_newprefixstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_newprefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_newprefixstepsmultiplyoutput) = 2 * ge_signed_half_swap_newprefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplyoutputreal) = S ge_signed_half_swap_newprefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_newprefixstepsmultiply) * (ge_second_rp_swap_newprefixstepsmultiply))) + (((ge_first_rn_swap_newprefixstepsmultiply) * (ge_second_rn_swap_newprefixstepsmultiply))))) + (((((ge_first_ip_swap_newprefixstepsmultiply) * (ge_second_in_swap_newprefixstepsmultiply))) + (((ge_first_in_swap_newprefixstepsmultiply) * (ge_second_ip_swap_newprefixstepsmultiply))))))) + ge_balance_negative_swap_newprefixstepsmultiplyoutputreal = (((((((ge_first_rp_swap_newprefixstepsmultiply) * (ge_second_rn_swap_newprefixstepsmultiply))) + (((ge_first_rn_swap_newprefixstepsmultiply) * (ge_second_rp_swap_newprefixstepsmultiply))))) + (((((ge_first_ip_swap_newprefixstepsmultiply) * (ge_second_ip_swap_newprefixstepsmultiply))) + (((ge_first_in_swap_newprefixstepsmultiply) * (ge_second_in_swap_newprefixstepsmultiply))))))) + ge_balance_positive_swap_newprefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_newprefixstepsmultiplyoutputimaginary ge_balance_negative_swap_newprefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_newprefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_newprefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_newprefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_newprefixstepsmultiplyoutput) = 2 * ge_signed_half_swap_newprefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_newprefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_newprefixstepsmultiplyoutputimaginary) = S ge_signed_half_swap_newprefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_newprefixstepsmultiply) * (ge_second_ip_swap_newprefixstepsmultiply))) + (((ge_first_rn_swap_newprefixstepsmultiply) * (ge_second_in_swap_newprefixstepsmultiply))))) + (((((ge_first_ip_swap_newprefixstepsmultiply) * (ge_second_rp_swap_newprefixstepsmultiply))) + (((ge_first_in_swap_newprefixstepsmultiply) * (ge_second_rn_swap_newprefixstepsmultiply))))))) + ge_balance_negative_swap_newprefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_newprefixstepsmultiply) * (ge_second_in_swap_newprefixstepsmultiply))) + (((ge_first_rn_swap_newprefixstepsmultiply) * (ge_second_ip_swap_newprefixstepsmultiply))))) + (((((ge_first_ip_swap_newprefixstepsmultiply) * (ge_second_rn_swap_newprefixstepsmultiply))) + (((ge_first_in_swap_newprefixstepsmultiply) * (ge_second_rp_swap_newprefixstepsmultiply))))))) + ge_balance_positive_swap_newprefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_swap_newlast ge_first_rn_swap_newlast ge_first_ip_swap_newlast ge_first_in_swap_newlast ge_second_rp_swap_newlast ge_second_rn_swap_newlast ge_second_ip_swap_newlast ge_second_in_swap_newlast. ((exists ge_representation_real_code_swap_newlastfirst ge_representation_imaginary_code_swap_newlastfirst. (((R) = ((ge_representation_real_code_swap_newlastfirst) + (ge_representation_imaginary_code_swap_newlastfirst)) * S ((ge_representation_real_code_swap_newlastfirst) + (ge_representation_imaginary_code_swap_newlastfirst)) + ((ge_representation_imaginary_code_swap_newlastfirst) + (ge_representation_imaginary_code_swap_newlastfirst))) /\ ((exists ge_balance_positive_swap_newlastfirstreal ge_balance_negative_swap_newlastfirstreal. (((((ge_representation_real_code_swap_newlastfirst) = 2 * (ge_balance_positive_swap_newlastfirstreal) /\ (ge_balance_negative_swap_newlastfirstreal) = 0) \/ exists ge_signed_half_swap_newlastfirstrealdecode. (((ge_representation_real_code_swap_newlastfirst) = 2 * ge_signed_half_swap_newlastfirstrealdecode + 1 /\ (ge_balance_positive_swap_newlastfirstreal) = 0) /\ (ge_balance_negative_swap_newlastfirstreal) = S ge_signed_half_swap_newlastfirstrealdecode))) /\ ((ge_first_rp_swap_newlast) + ge_balance_negative_swap_newlastfirstreal = (ge_first_rn_swap_newlast) + ge_balance_positive_swap_newlastfirstreal))) /\ (exists ge_balance_positive_swap_newlastfirstimaginary ge_balance_negative_swap_newlastfirstimaginary. (((((ge_representation_imaginary_code_swap_newlastfirst) = 2 * (ge_balance_positive_swap_newlastfirstimaginary) /\ (ge_balance_negative_swap_newlastfirstimaginary) = 0) \/ exists ge_signed_half_swap_newlastfirstimaginarydecode. (((ge_representation_imaginary_code_swap_newlastfirst) = 2 * ge_signed_half_swap_newlastfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_newlastfirstimaginary) = 0) /\ (ge_balance_negative_swap_newlastfirstimaginary) = S ge_signed_half_swap_newlastfirstimaginarydecode))) /\ ((ge_first_ip_swap_newlast) + ge_balance_negative_swap_newlastfirstimaginary = (ge_first_in_swap_newlast) + ge_balance_positive_swap_newlastfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_newlastsecond ge_representation_imaginary_code_swap_newlastsecond. (((a) = ((ge_representation_real_code_swap_newlastsecond) + (ge_representation_imaginary_code_swap_newlastsecond)) * S ((ge_representation_real_code_swap_newlastsecond) + (ge_representation_imaginary_code_swap_newlastsecond)) + ((ge_representation_imaginary_code_swap_newlastsecond) + (ge_representation_imaginary_code_swap_newlastsecond))) /\ ((exists ge_balance_positive_swap_newlastsecondreal ge_balance_negative_swap_newlastsecondreal. (((((ge_representation_real_code_swap_newlastsecond) = 2 * (ge_balance_positive_swap_newlastsecondreal) /\ (ge_balance_negative_swap_newlastsecondreal) = 0) \/ exists ge_signed_half_swap_newlastsecondrealdecode. (((ge_representation_real_code_swap_newlastsecond) = 2 * ge_signed_half_swap_newlastsecondrealdecode + 1 /\ (ge_balance_positive_swap_newlastsecondreal) = 0) /\ (ge_balance_negative_swap_newlastsecondreal) = S ge_signed_half_swap_newlastsecondrealdecode))) /\ ((ge_second_rp_swap_newlast) + ge_balance_negative_swap_newlastsecondreal = (ge_second_rn_swap_newlast) + ge_balance_positive_swap_newlastsecondreal))) /\ (exists ge_balance_positive_swap_newlastsecondimaginary ge_balance_negative_swap_newlastsecondimaginary. (((((ge_representation_imaginary_code_swap_newlastsecond) = 2 * (ge_balance_positive_swap_newlastsecondimaginary) /\ (ge_balance_negative_swap_newlastsecondimaginary) = 0) \/ exists ge_signed_half_swap_newlastsecondimaginarydecode. (((ge_representation_imaginary_code_swap_newlastsecond) = 2 * ge_signed_half_swap_newlastsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_newlastsecondimaginary) = 0) /\ (ge_balance_negative_swap_newlastsecondimaginary) = S ge_signed_half_swap_newlastsecondimaginarydecode))) /\ ((ge_second_ip_swap_newlast) + ge_balance_negative_swap_newlastsecondimaginary = (ge_second_in_swap_newlast) + ge_balance_positive_swap_newlastsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_newlastoutput ge_representation_imaginary_code_swap_newlastoutput. (((Q) = ((ge_representation_real_code_swap_newlastoutput) + (ge_representation_imaginary_code_swap_newlastoutput)) * S ((ge_representation_real_code_swap_newlastoutput) + (ge_representation_imaginary_code_swap_newlastoutput)) + ((ge_representation_imaginary_code_swap_newlastoutput) + (ge_representation_imaginary_code_swap_newlastoutput))) /\ ((exists ge_balance_positive_swap_newlastoutputreal ge_balance_negative_swap_newlastoutputreal. (((((ge_representation_real_code_swap_newlastoutput) = 2 * (ge_balance_positive_swap_newlastoutputreal) /\ (ge_balance_negative_swap_newlastoutputreal) = 0) \/ exists ge_signed_half_swap_newlastoutputrealdecode. (((ge_representation_real_code_swap_newlastoutput) = 2 * ge_signed_half_swap_newlastoutputrealdecode + 1 /\ (ge_balance_positive_swap_newlastoutputreal) = 0) /\ (ge_balance_negative_swap_newlastoutputreal) = S ge_signed_half_swap_newlastoutputrealdecode))) /\ ((((((((ge_first_rp_swap_newlast) * (ge_second_rp_swap_newlast))) + (((ge_first_rn_swap_newlast) * (ge_second_rn_swap_newlast))))) + (((((ge_first_ip_swap_newlast) * (ge_second_in_swap_newlast))) + (((ge_first_in_swap_newlast) * (ge_second_ip_swap_newlast))))))) + ge_balance_negative_swap_newlastoutputreal = (((((((ge_first_rp_swap_newlast) * (ge_second_rn_swap_newlast))) + (((ge_first_rn_swap_newlast) * (ge_second_rp_swap_newlast))))) + (((((ge_first_ip_swap_newlast) * (ge_second_ip_swap_newlast))) + (((ge_first_in_swap_newlast) * (ge_second_in_swap_newlast))))))) + ge_balance_positive_swap_newlastoutputreal))) /\ (exists ge_balance_positive_swap_newlastoutputimaginary ge_balance_negative_swap_newlastoutputimaginary. (((((ge_representation_imaginary_code_swap_newlastoutput) = 2 * (ge_balance_positive_swap_newlastoutputimaginary) /\ (ge_balance_negative_swap_newlastoutputimaginary) = 0) \/ exists ge_signed_half_swap_newlastoutputimaginarydecode. (((ge_representation_imaginary_code_swap_newlastoutput) = 2 * ge_signed_half_swap_newlastoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_newlastoutputimaginary) = 0) /\ (ge_balance_negative_swap_newlastoutputimaginary) = S ge_signed_half_swap_newlastoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_newlast) * (ge_second_ip_swap_newlast))) + (((ge_first_rn_swap_newlast) * (ge_second_in_swap_newlast))))) + (((((ge_first_ip_swap_newlast) * (ge_second_rp_swap_newlast))) + (((ge_first_in_swap_newlast) * (ge_second_rn_swap_newlast))))))) + ge_balance_negative_swap_newlastoutputimaginary = (((((((ge_first_rp_swap_newlast) * (ge_second_in_swap_newlast))) + (((ge_first_rn_swap_newlast) * (ge_second_ip_swap_newlast))))) + (((((ge_first_ip_swap_newlast) * (ge_second_rn_swap_newlast))) + (((ge_first_in_swap_newlast) * (ge_second_rp_swap_newlast))))))) + ge_balance_positive_swap_newlastoutputimaginary)))))))))))
  27. 0027specialize gaussian_product_successor_decompose (d)
  28. 0028specialize gaussian_product_successor_decompose (e)
  29. 0029specialize gaussian_product_successor_decompose (l)
  30. 0030specialize gaussian_product_successor_decompose (Q)
  31. 0031apply gaussian_product_successor_decompose
  32. 0032exact hQ
  33. 0033cases hold
  34. 0034cases hold_witness
  35. 0035cases hold_witness_witness
  36. 0036cases hold_witness_witness_right
  37. 0037cases hnew
  38. 0038cases hnew_witness
  39. 0039cases hnew_witness_witness
  40. 0040cases hnew_witness_witness_right
  41. 0041have hlastold : x=q
  42. 0042specialize beta_at_unique (b)
  43. 0043specialize beta_at_unique (c)
  44. 0044specialize beta_at_unique (l)
  45. 0045specialize beta_at_unique (x)
  46. 0046specialize beta_at_unique (q)
  47. 0047apply beta_at_unique
  48. 0048exact hold_witness_witness_left
  49. 0049exact hswap_right_left
  50. 0050have hlastnew : x2=p
  51. 0051specialize beta_at_unique (d)
  52. 0052specialize beta_at_unique (e)
  53. 0053specialize beta_at_unique (l)
  54. 0054specialize beta_at_unique (x2)
  55. 0055specialize beta_at_unique (p)
  56. 0056apply beta_at_unique
  57. 0057exact hnew_witness_witness_left
  58. 0058exact hswap_right_right_right_left
  59. 0059rewrite hlastold at hold_witness_witness_right_right
  60. 0060rewrite hlastnew at hnew_witness_witness_right_right
  61. 0061specialize gaussian_multiply_functional (x1)
  62. 0062specialize gaussian_multiply_functional (q)
  63. 0063specialize gaussian_multiply_functional (P)
  64. 0064specialize gaussian_multiply_functional (Q)
  65. 0065apply gaussian_multiply_functional
  66. 0066exact hold_witness_witness_right_right
  67. 0067specialize gaussian_product_replace_balance (l)
  68. 0068specialize gaussian_product_replace_balance (b)
  69. 0069specialize gaussian_product_replace_balance (c)
  70. 0070specialize gaussian_product_replace_balance (d)
  71. 0071specialize gaussian_product_replace_balance (e)
  72. 0072specialize gaussian_product_replace_balance (i)
  73. 0073specialize gaussian_product_replace_balance (p)
  74. 0074specialize gaussian_product_replace_balance (q)
  75. 0075specialize gaussian_product_replace_balance (x1)
  76. 0076specialize gaussian_product_replace_balance (x3)
  77. 0077specialize gaussian_product_replace_balance (Q)
  78. 0078apply gaussian_product_replace_balance
  79. 0079exact hi
  80. 0080exact hswap_left
  81. 0081exact hswap_right_right_left
  82. 0082intro j
  83. 0083intro a
  84. 0084intro hj
  85. 0085intro hne
  86. 0086intro hentry
  87. 0087specialize hswap_right_right_right_right (j)
  88. 0088specialize hswap_right_right_right_right (a)
  89. 0089apply hswap_right_right_right_right
  90. 0090specialize le_succ (S j)
  91. 0091specialize le_succ (l)
  92. 0092apply le_succ
  93. 0093exact hj
  94. 0094exact hne
  95. 0095intro heq
  96. 0096specialize lt_irrefl_expanded (l)
  97. 0097apply lt_irrefl_expanded
  98. 0098rewrite heq at hj
  99. 0099exact hj
  100. 0100exact hentry
  101. 0101exact hold_witness_witness_right_left
  102. 0102exact hnew_witness_witness_right_left
  103. 0103exact hnew_witness_witness_right_right