GF00A0

gaussian_product_replace_balance

Ordinary induction proves the actual Gaussian replacement balance Q*p=P*q with genuine product traces and actual common output code, including zero and unit factors.

Alpha v34 checked-use · first admitted v30 · 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. Exact original first-admission records.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ k. ∀ b. ∀ c. ∀ d. ∀ e. ∀ i. ∀ p. ∀ q. ∀ P. ∀ Q. ∀ T. Lt(i,k) → BetaAt(b,c,i,p) → BetaAt(d,e,i,q) → (∀ x. ∀ y. Lt(x,k) → ¬x = i → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) → GProduct(b,c,k,P) → GProduct(d,e,k,Q) → GMul(Q,p,T) → GMul(P,q,T)

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

Definition DAG

GMul(a,b,c) · 7GProduct(b,c,l,P) · 5Lt(a,b) · 3BetaAt(b,c,i,x) · 7

Actual proof prerequisites

gaussian_search_no_index_below_zerofinite_lt_succ_eq_or_lt · checked external prerequisitegaussian_product_successor_decomposebeta_at_unique · checked external prerequisitegaussian_product_beta_index_transportgaussian_product_prefix_recodele_succ · checked external prerequisitelt_irrefl_expanded · checked external prerequisitegaussian_product_functionalgaussian_multiply_swap_taille_refl · checked external prerequisitegaussian_multiply_exists · checked external prerequisitegaussian_product_result_validgaussian_multiply_input_right_valid
Original expanded first-order statement 
forall k b c d e i p q P Q T. (exists ge_gap_replace_index. ge_gap_replace_index + S (i) = (k)) -> (((exists ff_h_gprod_replace_old_factor. ff_h_gprod_replace_old_factor + S (p) = S ((S (i)) * c)) /\ exists ff_q_gprod_replace_old_factor. b = ff_q_gprod_replace_old_factor * S ((S (i)) * c) + (p))) -> (((exists ff_h_gprod_replace_new_factor. ff_h_gprod_replace_new_factor + S (q) = S ((S (i)) * e)) /\ exists ff_q_gprod_replace_new_factor. d = ff_q_gprod_replace_new_factor * S ((S (i)) * e) + (q))) -> (forall gr_replacement_index_replace_other_factors gr_replacement_value_replace_other_factors. (exists ge_gap_replace_other_factorsbound. ge_gap_replace_other_factorsbound + S (gr_replacement_index_replace_other_factors) = (k)) -> ~(gr_replacement_index_replace_other_factors=(i)) -> (((exists ff_h_gprod_replace_other_factorsold. ff_h_gprod_replace_other_factorsold + S (gr_replacement_value_replace_other_factors) = S ((S (gr_replacement_index_replace_other_factors)) * c)) /\ exists ff_q_gprod_replace_other_factorsold. b = ff_q_gprod_replace_other_factorsold * S ((S (gr_replacement_index_replace_other_factors)) * c) + (gr_replacement_value_replace_other_factors))) -> (((exists ff_h_gprod_replace_other_factorsnew. ff_h_gprod_replace_other_factorsnew + S (gr_replacement_value_replace_other_factors) = S ((S (gr_replacement_index_replace_other_factors)) * e)) /\ exists ff_q_gprod_replace_other_factorsnew. d = ff_q_gprod_replace_other_factorsnew * S ((S (gr_replacement_index_replace_other_factors)) * e) + (gr_replacement_value_replace_other_factors)))) -> (exists gr_product_trace_replace_old_product gr_product_scale_replace_old_product. ((((exists ff_h_gprod_replace_old_productstart. ff_h_gprod_replace_old_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstart. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstart * S ((S (0)) * gr_product_scale_replace_old_product) + (6))) /\ ((((exists ff_h_gprod_replace_old_productend. ff_h_gprod_replace_old_productend + S (P) = S ((S (k)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productend. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productend * S ((S (k)) * gr_product_scale_replace_old_product) + (P))) /\ (forall gr_product_index_replace_old_productsteps. (exists ge_gap_replace_old_productstepsindex_bound. ge_gap_replace_old_productstepsindex_bound + S (gr_product_index_replace_old_productsteps) = (k)) -> exists gr_product_factor_replace_old_productsteps gr_product_before_replace_old_productsteps gr_product_after_replace_old_productsteps. ((((exists ff_h_gprod_replace_old_productstepsfactor. ff_h_gprod_replace_old_productstepsfactor + S (gr_product_factor_replace_old_productsteps) = S ((S (gr_product_index_replace_old_productsteps)) * c)) /\ exists ff_q_gprod_replace_old_productstepsfactor. b = ff_q_gprod_replace_old_productstepsfactor * S ((S (gr_product_index_replace_old_productsteps)) * c) + (gr_product_factor_replace_old_productsteps))) /\ ((((exists ff_h_gprod_replace_old_productstepsbefore. ff_h_gprod_replace_old_productstepsbefore + S (gr_product_before_replace_old_productsteps) = S ((S (gr_product_index_replace_old_productsteps)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstepsbefore. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstepsbefore * S ((S (gr_product_index_replace_old_productsteps)) * gr_product_scale_replace_old_product) + (gr_product_before_replace_old_productsteps))) /\ ((((exists ff_h_gprod_replace_old_productstepsafter. ff_h_gprod_replace_old_productstepsafter + S (gr_product_after_replace_old_productsteps) = S ((S (S (gr_product_index_replace_old_productsteps))) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstepsafter. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstepsafter * S ((S (S (gr_product_index_replace_old_productsteps))) * gr_product_scale_replace_old_product) + (gr_product_after_replace_old_productsteps))) /\ (exists ge_first_rp_replace_old_productstepsmultiply ge_first_rn_replace_old_productstepsmultiply ge_first_ip_replace_old_productstepsmultiply ge_first_in_replace_old_productstepsmultiply ge_second_rp_replace_old_productstepsmultiply ge_second_rn_replace_old_productstepsmultiply ge_second_ip_replace_old_productstepsmultiply ge_second_in_replace_old_productstepsmultiply. ((exists ge_representation_real_code_replace_old_productstepsmultiplyfirst ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst. (((gr_product_before_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplyfirstreal ge_balance_negative_replace_old_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstreal) = S ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplyfirstreal = (ge_first_rn_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary = (ge_first_in_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_old_productstepsmultiplysecond ge_representation_imaginary_code_replace_old_productstepsmultiplysecond. (((gr_product_factor_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplysecondreal ge_balance_negative_replace_old_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_old_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_old_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondreal) = S ge_signed_half_replace_old_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplysecondreal = (ge_second_rn_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplysecondimaginary ge_balance_negative_replace_old_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_old_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplysecondimaginary = (ge_second_in_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_old_productstepsmultiplyoutput ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput. (((gr_product_after_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplyoutputreal ge_balance_negative_replace_old_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputreal) = S ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))))))) + ge_balance_negative_replace_old_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))))))) + ge_balance_positive_replace_old_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))))))) + ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))))))) + ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_replace_new_product gr_product_scale_replace_new_product. ((((exists ff_h_gprod_replace_new_productstart. ff_h_gprod_replace_new_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstart. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstart * S ((S (0)) * gr_product_scale_replace_new_product) + (6))) /\ ((((exists ff_h_gprod_replace_new_productend. ff_h_gprod_replace_new_productend + S (Q) = S ((S (k)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productend. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productend * S ((S (k)) * gr_product_scale_replace_new_product) + (Q))) /\ (forall gr_product_index_replace_new_productsteps. (exists ge_gap_replace_new_productstepsindex_bound. ge_gap_replace_new_productstepsindex_bound + S (gr_product_index_replace_new_productsteps) = (k)) -> exists gr_product_factor_replace_new_productsteps gr_product_before_replace_new_productsteps gr_product_after_replace_new_productsteps. ((((exists ff_h_gprod_replace_new_productstepsfactor. ff_h_gprod_replace_new_productstepsfactor + S (gr_product_factor_replace_new_productsteps) = S ((S (gr_product_index_replace_new_productsteps)) * e)) /\ exists ff_q_gprod_replace_new_productstepsfactor. d = ff_q_gprod_replace_new_productstepsfactor * S ((S (gr_product_index_replace_new_productsteps)) * e) + (gr_product_factor_replace_new_productsteps))) /\ ((((exists ff_h_gprod_replace_new_productstepsbefore. ff_h_gprod_replace_new_productstepsbefore + S (gr_product_before_replace_new_productsteps) = S ((S (gr_product_index_replace_new_productsteps)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstepsbefore. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstepsbefore * S ((S (gr_product_index_replace_new_productsteps)) * gr_product_scale_replace_new_product) + (gr_product_before_replace_new_productsteps))) /\ ((((exists ff_h_gprod_replace_new_productstepsafter. ff_h_gprod_replace_new_productstepsafter + S (gr_product_after_replace_new_productsteps) = S ((S (S (gr_product_index_replace_new_productsteps))) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstepsafter. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstepsafter * S ((S (S (gr_product_index_replace_new_productsteps))) * gr_product_scale_replace_new_product) + (gr_product_after_replace_new_productsteps))) /\ (exists ge_first_rp_replace_new_productstepsmultiply ge_first_rn_replace_new_productstepsmultiply ge_first_ip_replace_new_productstepsmultiply ge_first_in_replace_new_productstepsmultiply ge_second_rp_replace_new_productstepsmultiply ge_second_rn_replace_new_productstepsmultiply ge_second_ip_replace_new_productstepsmultiply ge_second_in_replace_new_productstepsmultiply. ((exists ge_representation_real_code_replace_new_productstepsmultiplyfirst ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst. (((gr_product_before_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplyfirstreal ge_balance_negative_replace_new_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstreal) = S ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplyfirstreal = (ge_first_rn_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary = (ge_first_in_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_new_productstepsmultiplysecond ge_representation_imaginary_code_replace_new_productstepsmultiplysecond. (((gr_product_factor_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplysecondreal ge_balance_negative_replace_new_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_new_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_new_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondreal) = S ge_signed_half_replace_new_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplysecondreal = (ge_second_rn_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplysecondimaginary ge_balance_negative_replace_new_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_new_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplysecondimaginary = (ge_second_in_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_new_productstepsmultiplyoutput ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput. (((gr_product_after_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplyoutputreal ge_balance_negative_replace_new_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputreal) = S ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))))))) + ge_balance_negative_replace_new_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))))))) + ge_balance_positive_replace_new_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))))))) + ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))))))) + ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_first_rp_replace_balance_source ge_first_rn_replace_balance_source ge_first_ip_replace_balance_source ge_first_in_replace_balance_source ge_second_rp_replace_balance_source ge_second_rn_replace_balance_source ge_second_ip_replace_balance_source ge_second_in_replace_balance_source. ((exists ge_representation_real_code_replace_balance_sourcefirst ge_representation_imaginary_code_replace_balance_sourcefirst. (((Q) = ((ge_representation_real_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst)) * S ((ge_representation_real_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst)) + ((ge_representation_imaginary_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst))) /\ ((exists ge_balance_positive_replace_balance_sourcefirstreal ge_balance_negative_replace_balance_sourcefirstreal. (((((ge_representation_real_code_replace_balance_sourcefirst) = 2 * (ge_balance_positive_replace_balance_sourcefirstreal) /\ (ge_balance_negative_replace_balance_sourcefirstreal) = 0) \/ exists ge_signed_half_replace_balance_sourcefirstrealdecode. (((ge_representation_real_code_replace_balance_sourcefirst) = 2 * ge_signed_half_replace_balance_sourcefirstrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourcefirstreal) = 0) /\ (ge_balance_negative_replace_balance_sourcefirstreal) = S ge_signed_half_replace_balance_sourcefirstrealdecode))) /\ ((ge_first_rp_replace_balance_source) + ge_balance_negative_replace_balance_sourcefirstreal = (ge_first_rn_replace_balance_source) + ge_balance_positive_replace_balance_sourcefirstreal))) /\ (exists ge_balance_positive_replace_balance_sourcefirstimaginary ge_balance_negative_replace_balance_sourcefirstimaginary. (((((ge_representation_imaginary_code_replace_balance_sourcefirst) = 2 * (ge_balance_positive_replace_balance_sourcefirstimaginary) /\ (ge_balance_negative_replace_balance_sourcefirstimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourcefirstimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourcefirst) = 2 * ge_signed_half_replace_balance_sourcefirstimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourcefirstimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourcefirstimaginary) = S ge_signed_half_replace_balance_sourcefirstimaginarydecode))) /\ ((ge_first_ip_replace_balance_source) + ge_balance_negative_replace_balance_sourcefirstimaginary = (ge_first_in_replace_balance_source) + ge_balance_positive_replace_balance_sourcefirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_balance_sourcesecond ge_representation_imaginary_code_replace_balance_sourcesecond. (((p) = ((ge_representation_real_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond)) * S ((ge_representation_real_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond)) + ((ge_representation_imaginary_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond))) /\ ((exists ge_balance_positive_replace_balance_sourcesecondreal ge_balance_negative_replace_balance_sourcesecondreal. (((((ge_representation_real_code_replace_balance_sourcesecond) = 2 * (ge_balance_positive_replace_balance_sourcesecondreal) /\ (ge_balance_negative_replace_balance_sourcesecondreal) = 0) \/ exists ge_signed_half_replace_balance_sourcesecondrealdecode. (((ge_representation_real_code_replace_balance_sourcesecond) = 2 * ge_signed_half_replace_balance_sourcesecondrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourcesecondreal) = 0) /\ (ge_balance_negative_replace_balance_sourcesecondreal) = S ge_signed_half_replace_balance_sourcesecondrealdecode))) /\ ((ge_second_rp_replace_balance_source) + ge_balance_negative_replace_balance_sourcesecondreal = (ge_second_rn_replace_balance_source) + ge_balance_positive_replace_balance_sourcesecondreal))) /\ (exists ge_balance_positive_replace_balance_sourcesecondimaginary ge_balance_negative_replace_balance_sourcesecondimaginary. (((((ge_representation_imaginary_code_replace_balance_sourcesecond) = 2 * (ge_balance_positive_replace_balance_sourcesecondimaginary) /\ (ge_balance_negative_replace_balance_sourcesecondimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourcesecondimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourcesecond) = 2 * ge_signed_half_replace_balance_sourcesecondimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourcesecondimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourcesecondimaginary) = S ge_signed_half_replace_balance_sourcesecondimaginarydecode))) /\ ((ge_second_ip_replace_balance_source) + ge_balance_negative_replace_balance_sourcesecondimaginary = (ge_second_in_replace_balance_source) + ge_balance_positive_replace_balance_sourcesecondimaginary)))))) /\ (exists ge_representation_real_code_replace_balance_sourceoutput ge_representation_imaginary_code_replace_balance_sourceoutput. (((T) = ((ge_representation_real_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput)) * S ((ge_representation_real_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput)) + ((ge_representation_imaginary_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput))) /\ ((exists ge_balance_positive_replace_balance_sourceoutputreal ge_balance_negative_replace_balance_sourceoutputreal. (((((ge_representation_real_code_replace_balance_sourceoutput) = 2 * (ge_balance_positive_replace_balance_sourceoutputreal) /\ (ge_balance_negative_replace_balance_sourceoutputreal) = 0) \/ exists ge_signed_half_replace_balance_sourceoutputrealdecode. (((ge_representation_real_code_replace_balance_sourceoutput) = 2 * ge_signed_half_replace_balance_sourceoutputrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourceoutputreal) = 0) /\ (ge_balance_negative_replace_balance_sourceoutputreal) = S ge_signed_half_replace_balance_sourceoutputrealdecode))) /\ ((((((((ge_first_rp_replace_balance_source) * (ge_second_rp_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_rn_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_in_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_ip_replace_balance_source))))))) + ge_balance_negative_replace_balance_sourceoutputreal = (((((((ge_first_rp_replace_balance_source) * (ge_second_rn_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_rp_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_ip_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_in_replace_balance_source))))))) + ge_balance_positive_replace_balance_sourceoutputreal))) /\ (exists ge_balance_positive_replace_balance_sourceoutputimaginary ge_balance_negative_replace_balance_sourceoutputimaginary. (((((ge_representation_imaginary_code_replace_balance_sourceoutput) = 2 * (ge_balance_positive_replace_balance_sourceoutputimaginary) /\ (ge_balance_negative_replace_balance_sourceoutputimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourceoutputimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourceoutput) = 2 * ge_signed_half_replace_balance_sourceoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourceoutputimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourceoutputimaginary) = S ge_signed_half_replace_balance_sourceoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_balance_source) * (ge_second_ip_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_in_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_rp_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_rn_replace_balance_source))))))) + ge_balance_negative_replace_balance_sourceoutputimaginary = (((((((ge_first_rp_replace_balance_source) * (ge_second_in_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_ip_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_rn_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_rp_replace_balance_source))))))) + ge_balance_positive_replace_balance_sourceoutputimaginary))))))))) -> (exists ge_first_rp_replace_balance_target ge_first_rn_replace_balance_target ge_first_ip_replace_balance_target ge_first_in_replace_balance_target ge_second_rp_replace_balance_target ge_second_rn_replace_balance_target ge_second_ip_replace_balance_target ge_second_in_replace_balance_target. ((exists ge_representation_real_code_replace_balance_targetfirst ge_representation_imaginary_code_replace_balance_targetfirst. (((P) = ((ge_representation_real_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst)) * S ((ge_representation_real_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst)) + ((ge_representation_imaginary_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst))) /\ ((exists ge_balance_positive_replace_balance_targetfirstreal ge_balance_negative_replace_balance_targetfirstreal. (((((ge_representation_real_code_replace_balance_targetfirst) = 2 * (ge_balance_positive_replace_balance_targetfirstreal) /\ (ge_balance_negative_replace_balance_targetfirstreal) = 0) \/ exists ge_signed_half_replace_balance_targetfirstrealdecode. (((ge_representation_real_code_replace_balance_targetfirst) = 2 * ge_signed_half_replace_balance_targetfirstrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetfirstreal) = 0) /\ (ge_balance_negative_replace_balance_targetfirstreal) = S ge_signed_half_replace_balance_targetfirstrealdecode))) /\ ((ge_first_rp_replace_balance_target) + ge_balance_negative_replace_balance_targetfirstreal = (ge_first_rn_replace_balance_target) + ge_balance_positive_replace_balance_targetfirstreal))) /\ (exists ge_balance_positive_replace_balance_targetfirstimaginary ge_balance_negative_replace_balance_targetfirstimaginary. (((((ge_representation_imaginary_code_replace_balance_targetfirst) = 2 * (ge_balance_positive_replace_balance_targetfirstimaginary) /\ (ge_balance_negative_replace_balance_targetfirstimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetfirstimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetfirst) = 2 * ge_signed_half_replace_balance_targetfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetfirstimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetfirstimaginary) = S ge_signed_half_replace_balance_targetfirstimaginarydecode))) /\ ((ge_first_ip_replace_balance_target) + ge_balance_negative_replace_balance_targetfirstimaginary = (ge_first_in_replace_balance_target) + ge_balance_positive_replace_balance_targetfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_balance_targetsecond ge_representation_imaginary_code_replace_balance_targetsecond. (((q) = ((ge_representation_real_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond)) * S ((ge_representation_real_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond)) + ((ge_representation_imaginary_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond))) /\ ((exists ge_balance_positive_replace_balance_targetsecondreal ge_balance_negative_replace_balance_targetsecondreal. (((((ge_representation_real_code_replace_balance_targetsecond) = 2 * (ge_balance_positive_replace_balance_targetsecondreal) /\ (ge_balance_negative_replace_balance_targetsecondreal) = 0) \/ exists ge_signed_half_replace_balance_targetsecondrealdecode. (((ge_representation_real_code_replace_balance_targetsecond) = 2 * ge_signed_half_replace_balance_targetsecondrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetsecondreal) = 0) /\ (ge_balance_negative_replace_balance_targetsecondreal) = S ge_signed_half_replace_balance_targetsecondrealdecode))) /\ ((ge_second_rp_replace_balance_target) + ge_balance_negative_replace_balance_targetsecondreal = (ge_second_rn_replace_balance_target) + ge_balance_positive_replace_balance_targetsecondreal))) /\ (exists ge_balance_positive_replace_balance_targetsecondimaginary ge_balance_negative_replace_balance_targetsecondimaginary. (((((ge_representation_imaginary_code_replace_balance_targetsecond) = 2 * (ge_balance_positive_replace_balance_targetsecondimaginary) /\ (ge_balance_negative_replace_balance_targetsecondimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetsecondimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetsecond) = 2 * ge_signed_half_replace_balance_targetsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetsecondimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetsecondimaginary) = S ge_signed_half_replace_balance_targetsecondimaginarydecode))) /\ ((ge_second_ip_replace_balance_target) + ge_balance_negative_replace_balance_targetsecondimaginary = (ge_second_in_replace_balance_target) + ge_balance_positive_replace_balance_targetsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_balance_targetoutput ge_representation_imaginary_code_replace_balance_targetoutput. (((T) = ((ge_representation_real_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput)) * S ((ge_representation_real_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput)) + ((ge_representation_imaginary_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput))) /\ ((exists ge_balance_positive_replace_balance_targetoutputreal ge_balance_negative_replace_balance_targetoutputreal. (((((ge_representation_real_code_replace_balance_targetoutput) = 2 * (ge_balance_positive_replace_balance_targetoutputreal) /\ (ge_balance_negative_replace_balance_targetoutputreal) = 0) \/ exists ge_signed_half_replace_balance_targetoutputrealdecode. (((ge_representation_real_code_replace_balance_targetoutput) = 2 * ge_signed_half_replace_balance_targetoutputrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetoutputreal) = 0) /\ (ge_balance_negative_replace_balance_targetoutputreal) = S ge_signed_half_replace_balance_targetoutputrealdecode))) /\ ((((((((ge_first_rp_replace_balance_target) * (ge_second_rp_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_rn_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_in_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_ip_replace_balance_target))))))) + ge_balance_negative_replace_balance_targetoutputreal = (((((((ge_first_rp_replace_balance_target) * (ge_second_rn_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_rp_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_ip_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_in_replace_balance_target))))))) + ge_balance_positive_replace_balance_targetoutputreal))) /\ (exists ge_balance_positive_replace_balance_targetoutputimaginary ge_balance_negative_replace_balance_targetoutputimaginary. (((((ge_representation_imaginary_code_replace_balance_targetoutput) = 2 * (ge_balance_positive_replace_balance_targetoutputimaginary) /\ (ge_balance_negative_replace_balance_targetoutputimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetoutputimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetoutput) = 2 * ge_signed_half_replace_balance_targetoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetoutputimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetoutputimaginary) = S ge_signed_half_replace_balance_targetoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_balance_target) * (ge_second_ip_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_in_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_rp_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_rn_replace_balance_target))))))) + ge_balance_negative_replace_balance_targetoutputimaginary = (((((((ge_first_rp_replace_balance_target) * (ge_second_in_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_ip_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_rn_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_rp_replace_balance_target))))))) + ge_balance_positive_replace_balance_targetoutputimaginary)))))))))

Complete tactic proof in conservative notation

All 241 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

241 script commands · 38 reading checkpoints · 13 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 (8)
gaussian search no index below zerogaussian product successor decomposegaussian product beta index transportgaussian product prefix recodegaussian product functionalgaussian multiply swap tailgaussian product result validgaussian multiply input right valid
01Induction on kL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction k
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro i
  7. L7
    intro p
  8. L8
    intro q
  9. L9
    intro P
  10. L10
    intro Q
02Fix variables and assumptionsL11–18

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

  1. L11
    intro T
  2. L12
    intro hi
  3. L13
    intro hp
  4. L14
    intro hq
  5. L15
    intro hpreserve
  6. L16
    intro hP
  7. L17
    intro hQ
  8. L18
    intro hmultiply
03Separate the logical casesL19–19

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

  1. L19
    exfalso
04Use earlier factsL20–22

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

  1. L20
    specialize gaussian_search_no_index_below_zero (i)
  2. L21
    apply gaussian_search_no_index_below_zero
  3. L22
    exact hi
05Fix variables and assumptionsL23–32

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

  1. L23
    intro b
  2. L24
    intro c
  3. L25
    intro d
  4. L26
    intro e
  5. L27
    intro i
  6. L28
    intro p
  7. L29
    intro q
  8. L30
    intro P
  9. L31
    intro Q
  10. L32
    intro T
06Fix variables and assumptionsL33–39

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

  1. L33
    intro hi
  2. L34
    intro hp
  3. L35
    intro hq
  4. L36
    intro hpreserve
  5. L37
    intro hP
  6. L38
    intro hQ
  7. L39
    intro hmultiply
07Establish hcasesL40–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L40
    have hcases : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L41
    specialize finite_lt_succ_eq_or_lt (k)
  3. L42
    specialize finite_lt_succ_eq_or_lt (i)
  4. L43
    apply finite_lt_succ_eq_or_lt
  5. L44
    exact hi
08Establish holdL45–51

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

  1. L45
    have hold : ∃ a. ∃ R. BetaAt(b,c,k,a) ∧ (GProduct(b,c,k,R) ∧ GMul(R,a,P))Definitions: BetaAt(b,c,k,a)GProduct(b,c,k,R)GMul(R,a,P)Original native command in the exact edition
  2. L46
    specialize gaussian_product_successor_decompose (b)
  3. L47
    specialize gaussian_product_successor_decompose (c)
  4. L48
    specialize gaussian_product_successor_decompose (k)
  5. L49
    specialize gaussian_product_successor_decompose (P)
  6. L50
    apply gaussian_product_successor_decompose
  7. L51
    exact hP
09Establish hnewL52–58

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

  1. L52
    have hnew : ∃ a. ∃ R. BetaAt(d,e,k,a) ∧ (GProduct(d,e,k,R) ∧ GMul(R,a,Q))Definitions: BetaAt(d,e,k,a)GProduct(d,e,k,R)GMul(R,a,Q)Original native command in the exact edition
  2. L53
    specialize gaussian_product_successor_decompose (d)
  3. L54
    specialize gaussian_product_successor_decompose (e)
  4. L55
    specialize gaussian_product_successor_decompose (k)
  5. L56
    specialize gaussian_product_successor_decompose (Q)
  6. L57
    apply gaussian_product_successor_decompose
  7. L58
    exact hQ
10Separate the logical casesL59–67

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

  1. L59
    cases hold
  2. L60
    cases hold_witness
  3. L61
    cases hold_witness_witness
  4. L62
    cases hold_witness_witness_right
  5. L63
    cases hnew
  6. L64
    cases hnew_witness
  7. L65
    cases hnew_witness_witness
  8. L66
    cases hnew_witness_witness_right
  9. L67
    cases hcases
11Establish hlastoldL68–77

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

  1. L68
    have hlastold : x=p
  2. L69
    specialize beta_at_unique (b)
  3. L70
    specialize beta_at_unique (c)
  4. L71
    specialize beta_at_unique (k)
  5. L72
    specialize beta_at_unique (x)
  6. L73
    specialize beta_at_unique (p)
  7. L74
    apply beta_at_unique
  8. L75
    exact hold_witness_witness_left
  9. L76
    specialize gaussian_product_beta_index_transport (b)
  10. L77
    specialize gaussian_product_beta_index_transport (c)
12Use earlier factsL78–83

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

  1. L78
    specialize gaussian_product_beta_index_transport (i)
  2. L79
    specialize gaussian_product_beta_index_transport (k)
  3. L80
    specialize gaussian_product_beta_index_transport (p)
  4. L81
    apply gaussian_product_beta_index_transport
  5. L82
    exact hcases_left
  6. L83
    exact hp
13Establish hlastnewL84–93

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

  1. L84
    have hlastnew : x2=q
  2. L85
    specialize beta_at_unique (d)
  3. L86
    specialize beta_at_unique (e)
  4. L87
    specialize beta_at_unique (k)
  5. L88
    specialize beta_at_unique (x2)
  6. L89
    specialize beta_at_unique (q)
  7. L90
    apply beta_at_unique
  8. L91
    exact hnew_witness_witness_left
  9. L92
    specialize gaussian_product_beta_index_transport (d)
  10. L93
    specialize gaussian_product_beta_index_transport (e)
14Use earlier factsL94–99

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

  1. L94
    specialize gaussian_product_beta_index_transport (i)
  2. L95
    specialize gaussian_product_beta_index_transport (k)
  3. L96
    specialize gaussian_product_beta_index_transport (q)
  4. L97
    apply gaussian_product_beta_index_transport
  5. L98
    exact hcases_left
  6. L99
    exact hq
15Establish hprefixL100–109

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

  1. L100
    have hprefix : GProduct(d,e,k,x1)Definitions: GProduct(d,e,k,x1)Original native command in the exact edition
  2. L101
    specialize gaussian_product_prefix_recode (b)
  3. L102
    specialize gaussian_product_prefix_recode (c)
  4. L103
    specialize gaussian_product_prefix_recode (d)
  5. L104
    specialize gaussian_product_prefix_recode (e)
  6. L105
    specialize gaussian_product_prefix_recode (k)
  7. L106
    specialize gaussian_product_prefix_recode (x1)
  8. L107
    apply gaussian_product_prefix_recode
  9. L108
    exact hold_witness_witness_right_left
  10. L109
    intro j
16Fix variables and assumptionsL110–112

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

  1. L110
    intro a
  2. L111
    intro hj
  3. L112
    intro hentry
17Use earlier factsL113–119

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

  1. L113
    specialize hpreserve (j)
  2. L114
    specialize hpreserve (a)
  3. L115
    apply hpreserve
  4. L116
    specialize le_succ (S j)
  5. L117
    specialize le_succ (k)
  6. L118
    apply le_succ
  7. L119
    exact hj
18Fix variables and assumptionsL120–120

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

  1. L120
    intro heq
19Use earlier factsL121–122

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

  1. L121
    specialize lt_irrefl_expanded (k)
  2. L122
    apply lt_irrefl_expanded
20Calculate and transport equalitiesL123–124

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

  1. L123
    rewrite heq at hj
  2. L124
    rewrite hcases_left at hj
21Use earlier factsL125–126

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

  1. L125
    exact hj
  2. L126
    exact hentry
22Establish hprefixeqL127–136

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

  1. L127
    have hprefixeq : x1=x3
  2. L128
    specialize gaussian_product_functional (k)
  3. L129
    specialize gaussian_product_functional (d)
  4. L130
    specialize gaussian_product_functional (e)
  5. L131
    specialize gaussian_product_functional (x1)
  6. L132
    specialize gaussian_product_functional (x3)
  7. L133
    apply gaussian_product_functional
  8. L134
    exact hprefix
  9. L135
    exact hnew_witness_witness_right_left
  10. L136
    rewrite hlastold at hold_witness_witness_right_right
23Calculate and transport equalitiesL137–138

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

  1. L137
    rewrite hprefixeq at hold_witness_witness_right_right
  2. L138
    rewrite hlastnew at hnew_witness_witness_right_right
24Use earlier factsL139–148

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

  1. L139
    specialize gaussian_multiply_swap_tail (x3)
  2. L140
    specialize gaussian_multiply_swap_tail (q)
  3. L141
    specialize gaussian_multiply_swap_tail (p)
  4. L142
    specialize gaussian_multiply_swap_tail (Q)
  5. L143
    specialize gaussian_multiply_swap_tail (P)
  6. L144
    specialize gaussian_multiply_swap_tail (T)
  7. L145
    apply gaussian_multiply_swap_tail
  8. L146
    exact hnew_witness_witness_right_right
  9. L147
    exact hmultiply
  10. L148
    exact hold_witness_witness_right_right
25Establish hkiL149–154

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt irrefl expanded.

  1. L149
    have hki : ~(k=i)
  2. L150
    intro heq
  3. L151
    specialize lt_irrefl_expanded (k)
  4. L152
    apply lt_irrefl_expanded
  5. L153
    rewrite <- heq at hcases_right
  6. L154
    exact hcases_right
26Establish hlastL155–162

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

  1. L155
    have hlast : BetaAt(d,e,k,x)Definitions: BetaAt(d,e,k,x)Original native command in the exact edition
  2. L156
    specialize hpreserve (k)
  3. L157
    specialize hpreserve (x)
  4. L158
    apply hpreserve
  5. L159
    specialize le_refl (S k)
  6. L160
    apply le_refl
  7. L161
    exact hki
  8. L162
    exact hold_witness_witness_left
27Establish hlastmatchL163–172

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

  1. L163
    have hlastmatch : x2=x
  2. L164
    specialize beta_at_unique (d)
  3. L165
    specialize beta_at_unique (e)
  4. L166
    specialize beta_at_unique (k)
  5. L167
    specialize beta_at_unique (x2)
  6. L168
    specialize beta_at_unique (x)
  7. L169
    apply beta_at_unique
  8. L170
    exact hnew_witness_witness_left
  9. L171
    exact hlast
  10. L172
    rewrite hlastmatch at hnew_witness_witness_right_right
28Establish hRL173–182

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

  1. L173
    have hR : ∃ R. GMul(x3,p,R)Definitions: GMul(x3,p,R)Original native command in the exact edition
  2. L174
    specialize gaussian_multiply_exists (x3)
  3. L175
    specialize gaussian_multiply_exists (p)
  4. L176
    apply gaussian_multiply_exists
  5. L177
    specialize gaussian_product_result_valid (k)
  6. L178
    specialize gaussian_product_result_valid (d)
  7. L179
    specialize gaussian_product_result_valid (e)
  8. L180
    specialize gaussian_product_result_valid (x3)
  9. L181
    apply gaussian_product_result_valid
  10. L182
    exact hnew_witness_witness_right_left
29Use earlier factsL183–187

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

  1. L183
    specialize gaussian_multiply_input_right_valid (Q)
  2. L184
    specialize gaussian_multiply_input_right_valid (p)
  3. L185
    specialize gaussian_multiply_input_right_valid (T)
  4. L186
    apply gaussian_multiply_input_right_valid
  5. L187
    exact hmultiply
30Separate the logical casesL188–188

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

  1. L188
    cases hR
31Establish hmiddleL189–198

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply swap tail.

  1. L189
    have hmiddle : GMul(x4,x,T)Definitions: GMul(x4,x,T)Original native command in the exact edition
  2. L190
    specialize gaussian_multiply_swap_tail (x3)
  3. L191
    specialize gaussian_multiply_swap_tail (x)
  4. L192
    specialize gaussian_multiply_swap_tail (p)
  5. L193
    specialize gaussian_multiply_swap_tail (Q)
  6. L194
    specialize gaussian_multiply_swap_tail (x4)
  7. L195
    specialize gaussian_multiply_swap_tail (T)
  8. L196
    apply gaussian_multiply_swap_tail
  9. L197
    exact hnew_witness_witness_right_right
  10. L198
    exact hmultiply
32Use earlier factsL199–199

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

  1. L199
    exact hR_witness
33Establish hbalanceL200–209

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

  1. L200
    have hbalance : GMul(x1,q,x4)Definitions: GMul(x1,q,x4)Original native command in the exact edition
  2. L201
    specialize IH (b)
  3. L202
    specialize IH (c)
  4. L203
    specialize IH (d)
  5. L204
    specialize IH (e)
  6. L205
    specialize IH (i)
  7. L206
    specialize IH (p)
  8. L207
    specialize IH (q)
  9. L208
    specialize IH (x1)
  10. L209
    specialize IH (x3)
34Use earlier factsL210–214

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

  1. L210
    specialize IH (x4)
  2. L211
    apply IH
  3. L212
    exact hcases_right
  4. L213
    exact hp
  5. L214
    exact hq
35Fix variables and assumptionsL215–219

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

  1. L215
    intro j
  2. L216
    intro a
  3. L217
    intro hj
  4. L218
    intro hne
  5. L219
    intro hentry
36Use earlier factsL220–229

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

  1. L220
    specialize hpreserve (j)
  2. L221
    specialize hpreserve (a)
  3. L222
    apply hpreserve
  4. L223
    specialize le_succ (S j)
  5. L224
    specialize le_succ (k)
  6. L225
    apply le_succ
  7. L226
    exact hj
  8. L227
    exact hne
  9. L228
    exact hentry
  10. L229
    exact hold_witness_witness_right_left
37Use earlier factsL230–239

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

  1. L230
    exact hnew_witness_witness_right_left
  2. L231
    exact hR_witness
  3. L232
    specialize gaussian_multiply_swap_tail (x1)
  4. L233
    specialize gaussian_multiply_swap_tail (q)
  5. L234
    specialize gaussian_multiply_swap_tail (x)
  6. L235
    specialize gaussian_multiply_swap_tail (x4)
  7. L236
    specialize gaussian_multiply_swap_tail (P)
  8. L237
    specialize gaussian_multiply_swap_tail (T)
  9. L238
    apply gaussian_multiply_swap_tail
  10. L239
    exact hbalance
38Use earlier factsL240–241

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

  1. L240
    exact hmiddle
  2. L241
    exact hold_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 241 lines
  1. 0001induction k
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro i
  7. 0007intro p
  8. 0008intro q
  9. 0009intro P
  10. 0010intro Q
  11. 0011intro T
  12. 0012intro hi
  13. 0013intro hp
  14. 0014intro hq
  15. 0015intro hpreserve
  16. 0016intro hP
  17. 0017intro hQ
  18. 0018intro hmultiply
  19. 0019exfalso
  20. 0020specialize gaussian_search_no_index_below_zero (i)
  21. 0021apply gaussian_search_no_index_below_zero
  22. 0022exact hi
  23. 0023intro b
  24. 0024intro c
  25. 0025intro d
  26. 0026intro e
  27. 0027intro i
  28. 0028intro p
  29. 0029intro q
  30. 0030intro P
  31. 0031intro Q
  32. 0032intro T
  33. 0033intro hi
  34. 0034intro hp
  35. 0035intro hq
  36. 0036intro hpreserve
  37. 0037intro hP
  38. 0038intro hQ
  39. 0039intro hmultiply
  40. 0040have hcases : i = k ∨ Lt(i,k)
  41. 0041specialize finite_lt_succ_eq_or_lt (k)
  42. 0042specialize finite_lt_succ_eq_or_lt (i)
  43. 0043apply finite_lt_succ_eq_or_lt
  44. 0044exact hi
  45. 0045have hold : ∃ a. ∃ R. BetaAt(b,c,k,a) ∧ (GProduct(b,c,k,R) ∧ GMul(R,a,P))
  46. 0046specialize gaussian_product_successor_decompose (b)
  47. 0047specialize gaussian_product_successor_decompose (c)
  48. 0048specialize gaussian_product_successor_decompose (k)
  49. 0049specialize gaussian_product_successor_decompose (P)
  50. 0050apply gaussian_product_successor_decompose
  51. 0051exact hP
  52. 0052have hnew : ∃ a. ∃ R. BetaAt(d,e,k,a) ∧ (GProduct(d,e,k,R) ∧ GMul(R,a,Q))
  53. 0053specialize gaussian_product_successor_decompose (d)
  54. 0054specialize gaussian_product_successor_decompose (e)
  55. 0055specialize gaussian_product_successor_decompose (k)
  56. 0056specialize gaussian_product_successor_decompose (Q)
  57. 0057apply gaussian_product_successor_decompose
  58. 0058exact hQ
  59. 0059cases hold
  60. 0060cases hold_witness
  61. 0061cases hold_witness_witness
  62. 0062cases hold_witness_witness_right
  63. 0063cases hnew
  64. 0064cases hnew_witness
  65. 0065cases hnew_witness_witness
  66. 0066cases hnew_witness_witness_right
  67. 0067cases hcases
  68. 0068have hlastold : x=p
  69. 0069specialize beta_at_unique (b)
  70. 0070specialize beta_at_unique (c)
  71. 0071specialize beta_at_unique (k)
  72. 0072specialize beta_at_unique (x)
  73. 0073specialize beta_at_unique (p)
  74. 0074apply beta_at_unique
  75. 0075exact hold_witness_witness_left
  76. 0076specialize gaussian_product_beta_index_transport (b)
  77. 0077specialize gaussian_product_beta_index_transport (c)
  78. 0078specialize gaussian_product_beta_index_transport (i)
  79. 0079specialize gaussian_product_beta_index_transport (k)
  80. 0080specialize gaussian_product_beta_index_transport (p)
  81. 0081apply gaussian_product_beta_index_transport
  82. 0082exact hcases_left
  83. 0083exact hp
  84. 0084have hlastnew : x2=q
  85. 0085specialize beta_at_unique (d)
  86. 0086specialize beta_at_unique (e)
  87. 0087specialize beta_at_unique (k)
  88. 0088specialize beta_at_unique (x2)
  89. 0089specialize beta_at_unique (q)
  90. 0090apply beta_at_unique
  91. 0091exact hnew_witness_witness_left
  92. 0092specialize gaussian_product_beta_index_transport (d)
  93. 0093specialize gaussian_product_beta_index_transport (e)
  94. 0094specialize gaussian_product_beta_index_transport (i)
  95. 0095specialize gaussian_product_beta_index_transport (k)
  96. 0096specialize gaussian_product_beta_index_transport (q)
  97. 0097apply gaussian_product_beta_index_transport
  98. 0098exact hcases_left
  99. 0099exact hq
  100. 0100have hprefix : GProduct(d,e,k,x1)
  101. 0101specialize gaussian_product_prefix_recode (b)
  102. 0102specialize gaussian_product_prefix_recode (c)
  103. 0103specialize gaussian_product_prefix_recode (d)
  104. 0104specialize gaussian_product_prefix_recode (e)
  105. 0105specialize gaussian_product_prefix_recode (k)
  106. 0106specialize gaussian_product_prefix_recode (x1)
  107. 0107apply gaussian_product_prefix_recode
  108. 0108exact hold_witness_witness_right_left
  109. 0109intro j
  110. 0110intro a
  111. 0111intro hj
  112. 0112intro hentry
  113. 0113specialize hpreserve (j)
  114. 0114specialize hpreserve (a)
  115. 0115apply hpreserve
  116. 0116specialize le_succ (S j)
  117. 0117specialize le_succ (k)
  118. 0118apply le_succ
  119. 0119exact hj
  120. 0120intro heq
  121. 0121specialize lt_irrefl_expanded (k)
  122. 0122apply lt_irrefl_expanded
  123. 0123rewrite heq at hj
  124. 0124rewrite hcases_left at hj
  125. 0125exact hj
  126. 0126exact hentry
  127. 0127have hprefixeq : x1=x3
  128. 0128specialize gaussian_product_functional (k)
  129. 0129specialize gaussian_product_functional (d)
  130. 0130specialize gaussian_product_functional (e)
  131. 0131specialize gaussian_product_functional (x1)
  132. 0132specialize gaussian_product_functional (x3)
  133. 0133apply gaussian_product_functional
  134. 0134exact hprefix
  135. 0135exact hnew_witness_witness_right_left
  136. 0136rewrite hlastold at hold_witness_witness_right_right
  137. 0137rewrite hprefixeq at hold_witness_witness_right_right
  138. 0138rewrite hlastnew at hnew_witness_witness_right_right
  139. 0139specialize gaussian_multiply_swap_tail (x3)
  140. 0140specialize gaussian_multiply_swap_tail (q)
  141. 0141specialize gaussian_multiply_swap_tail (p)
  142. 0142specialize gaussian_multiply_swap_tail (Q)
  143. 0143specialize gaussian_multiply_swap_tail (P)
  144. 0144specialize gaussian_multiply_swap_tail (T)
  145. 0145apply gaussian_multiply_swap_tail
  146. 0146exact hnew_witness_witness_right_right
  147. 0147exact hmultiply
  148. 0148exact hold_witness_witness_right_right
  149. 0149have hki : ~(k=i)
  150. 0150intro heq
  151. 0151specialize lt_irrefl_expanded (k)
  152. 0152apply lt_irrefl_expanded
  153. 0153rewrite <- heq at hcases_right
  154. 0154exact hcases_right
  155. 0155have hlast : BetaAt(d,e,k,x)
  156. 0156specialize hpreserve (k)
  157. 0157specialize hpreserve (x)
  158. 0158apply hpreserve
  159. 0159specialize le_refl (S k)
  160. 0160apply le_refl
  161. 0161exact hki
  162. 0162exact hold_witness_witness_left
  163. 0163have hlastmatch : x2=x
  164. 0164specialize beta_at_unique (d)
  165. 0165specialize beta_at_unique (e)
  166. 0166specialize beta_at_unique (k)
  167. 0167specialize beta_at_unique (x2)
  168. 0168specialize beta_at_unique (x)
  169. 0169apply beta_at_unique
  170. 0170exact hnew_witness_witness_left
  171. 0171exact hlast
  172. 0172rewrite hlastmatch at hnew_witness_witness_right_right
  173. 0173have hR : ∃ R. GMul(x3,p,R)
  174. 0174specialize gaussian_multiply_exists (x3)
  175. 0175specialize gaussian_multiply_exists (p)
  176. 0176apply gaussian_multiply_exists
  177. 0177specialize gaussian_product_result_valid (k)
  178. 0178specialize gaussian_product_result_valid (d)
  179. 0179specialize gaussian_product_result_valid (e)
  180. 0180specialize gaussian_product_result_valid (x3)
  181. 0181apply gaussian_product_result_valid
  182. 0182exact hnew_witness_witness_right_left
  183. 0183specialize gaussian_multiply_input_right_valid (Q)
  184. 0184specialize gaussian_multiply_input_right_valid (p)
  185. 0185specialize gaussian_multiply_input_right_valid (T)
  186. 0186apply gaussian_multiply_input_right_valid
  187. 0187exact hmultiply
  188. 0188cases hR
  189. 0189have hmiddle : GMul(x4,x,T)
  190. 0190specialize gaussian_multiply_swap_tail (x3)
  191. 0191specialize gaussian_multiply_swap_tail (x)
  192. 0192specialize gaussian_multiply_swap_tail (p)
  193. 0193specialize gaussian_multiply_swap_tail (Q)
  194. 0194specialize gaussian_multiply_swap_tail (x4)
  195. 0195specialize gaussian_multiply_swap_tail (T)
  196. 0196apply gaussian_multiply_swap_tail
  197. 0197exact hnew_witness_witness_right_right
  198. 0198exact hmultiply
  199. 0199exact hR_witness
  200. 0200have hbalance : GMul(x1,q,x4)
  201. 0201specialize IH (b)
  202. 0202specialize IH (c)
  203. 0203specialize IH (d)
  204. 0204specialize IH (e)
  205. 0205specialize IH (i)
  206. 0206specialize IH (p)
  207. 0207specialize IH (q)
  208. 0208specialize IH (x1)
  209. 0209specialize IH (x3)
  210. 0210specialize IH (x4)
  211. 0211apply IH
  212. 0212exact hcases_right
  213. 0213exact hp
  214. 0214exact hq
  215. 0215intro j
  216. 0216intro a
  217. 0217intro hj
  218. 0218intro hne
  219. 0219intro hentry
  220. 0220specialize hpreserve (j)
  221. 0221specialize hpreserve (a)
  222. 0222apply hpreserve
  223. 0223specialize le_succ (S j)
  224. 0224specialize le_succ (k)
  225. 0225apply le_succ
  226. 0226exact hj
  227. 0227exact hne
  228. 0228exact hentry
  229. 0229exact hold_witness_witness_right_left
  230. 0230exact hnew_witness_witness_right_left
  231. 0231exact hR_witness
  232. 0232specialize gaussian_multiply_swap_tail (x1)
  233. 0233specialize gaussian_multiply_swap_tail (q)
  234. 0234specialize gaussian_multiply_swap_tail (x)
  235. 0235specialize gaussian_multiply_swap_tail (x4)
  236. 0236specialize gaussian_multiply_swap_tail (P)
  237. 0237specialize gaussian_multiply_swap_tail (T)
  238. 0238apply gaussian_multiply_swap_tail
  239. 0239exact hbalance
  240. 0240exact hmiddle
  241. 0241exact hold_witness_witness_right_right