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 l b c P Q. (exists gr_product_trace_functional_first gr_product_scale_functional_first. ((((exists ff_h_gprod_functional_firststart. ff_h_gprod_functional_firststart + S (6) = S ((S (0)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststart. gr_product_trace_functional_first = ff_q_gprod_functional_firststart * S ((S (0)) * gr_product_scale_functional_first) + (6))) /\ ((((exists ff_h_gprod_functional_firstend. ff_h_gprod_functional_firstend + S (P) = S ((S (l)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firstend. gr_product_trace_functional_first = ff_q_gprod_functional_firstend * S ((S (l)) * gr_product_scale_functional_first) + (P))) /\ (forall gr_product_index_functional_firststeps. (exists ge_gap_functional_firststepsindex_bound. ge_gap_functional_firststepsindex_bound + S (gr_product_index_functional_firststeps) = (l)) -> exists gr_product_factor_functional_firststeps gr_product_before_functional_firststeps gr_product_after_functional_firststeps. ((((exists ff_h_gprod_functional_firststepsfactor. ff_h_gprod_functional_firststepsfactor + S (gr_product_factor_functional_firststeps) = S ((S (gr_product_index_functional_firststeps)) * c)) /\ exists ff_q_gprod_functional_firststepsfactor. b = ff_q_gprod_functional_firststepsfactor * S ((S (gr_product_index_functional_firststeps)) * c) + (gr_product_factor_functional_firststeps))) /\ ((((exists ff_h_gprod_functional_firststepsbefore. ff_h_gprod_functional_firststepsbefore + S (gr_product_before_functional_firststeps) = S ((S (gr_product_index_functional_firststeps)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststepsbefore. gr_product_trace_functional_first = ff_q_gprod_functional_firststepsbefore * S ((S (gr_product_index_functional_firststeps)) * gr_product_scale_functional_first) + (gr_product_before_functional_firststeps))) /\ ((((exists ff_h_gprod_functional_firststepsafter. ff_h_gprod_functional_firststepsafter + S (gr_product_after_functional_firststeps) = S ((S (S (gr_product_index_functional_firststeps))) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststepsafter. gr_product_trace_functional_first = ff_q_gprod_functional_firststepsafter * S ((S (S (gr_product_index_functional_firststeps))) * gr_product_scale_functional_first) + (gr_product_after_functional_firststeps))) /\ (exists ge_first_rp_functional_firststepsmultiply ge_first_rn_functional_firststepsmultiply ge_first_ip_functional_firststepsmultiply ge_first_in_functional_firststepsmultiply ge_second_rp_functional_firststepsmultiply ge_second_rn_functional_firststepsmultiply ge_second_ip_functional_firststepsmultiply ge_second_in_functional_firststepsmultiply. ((exists ge_representation_real_code_functional_firststepsmultiplyfirst ge_representation_imaginary_code_functional_firststepsmultiplyfirst. (((gr_product_before_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst)) * S ((ge_representation_real_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_firststepsmultiplyfirstreal ge_balance_negative_functional_firststepsmultiplyfirstreal. (((((ge_representation_real_code_functional_firststepsmultiplyfirst) = 2 * (ge_balance_positive_functional_firststepsmultiplyfirstreal) /\ (ge_balance_negative_functional_firststepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_firststepsmultiplyfirst) = 2 * ge_signed_half_functional_firststepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyfirstreal) = S ge_signed_half_functional_firststepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplyfirstreal = (ge_first_rn_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplyfirstimaginary ge_balance_negative_functional_firststepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) = 2 * (ge_balance_positive_functional_firststepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_firststepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) = 2 * ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyfirstimaginary) = S ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplyfirstimaginary = (ge_first_in_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_firststepsmultiplysecond ge_representation_imaginary_code_functional_firststepsmultiplysecond. (((gr_product_factor_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond)) * S ((ge_representation_real_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_firststepsmultiplysecondreal ge_balance_negative_functional_firststepsmultiplysecondreal. (((((ge_representation_real_code_functional_firststepsmultiplysecond) = 2 * (ge_balance_positive_functional_firststepsmultiplysecondreal) /\ (ge_balance_negative_functional_firststepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_firststepsmultiplysecond) = 2 * ge_signed_half_functional_firststepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplysecondreal) = S ge_signed_half_functional_firststepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplysecondreal = (ge_second_rn_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplysecondimaginary ge_balance_negative_functional_firststepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplysecond) = 2 * (ge_balance_positive_functional_firststepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_firststepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplysecond) = 2 * ge_signed_half_functional_firststepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplysecondimaginary) = S ge_signed_half_functional_firststepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplysecondimaginary = (ge_second_in_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_firststepsmultiplyoutput ge_representation_imaginary_code_functional_firststepsmultiplyoutput. (((gr_product_after_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput)) * S ((ge_representation_real_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_firststepsmultiplyoutputreal ge_balance_negative_functional_firststepsmultiplyoutputreal. (((((ge_representation_real_code_functional_firststepsmultiplyoutput) = 2 * (ge_balance_positive_functional_firststepsmultiplyoutputreal) /\ (ge_balance_negative_functional_firststepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_firststepsmultiplyoutput) = 2 * ge_signed_half_functional_firststepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyoutputreal) = S ge_signed_half_functional_firststepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))))))) + ge_balance_negative_functional_firststepsmultiplyoutputreal = (((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))))))) + ge_balance_positive_functional_firststepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplyoutputimaginary ge_balance_negative_functional_firststepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) = 2 * (ge_balance_positive_functional_firststepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_firststepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) = 2 * ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyoutputimaginary) = S ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))))))) + ge_balance_negative_functional_firststepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))))))) + ge_balance_positive_functional_firststepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_functional_second gr_product_scale_functional_second. ((((exists ff_h_gprod_functional_secondstart. ff_h_gprod_functional_secondstart + S (6) = S ((S (0)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstart. gr_product_trace_functional_second = ff_q_gprod_functional_secondstart * S ((S (0)) * gr_product_scale_functional_second) + (6))) /\ ((((exists ff_h_gprod_functional_secondend. ff_h_gprod_functional_secondend + S (Q) = S ((S (l)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondend. gr_product_trace_functional_second = ff_q_gprod_functional_secondend * S ((S (l)) * gr_product_scale_functional_second) + (Q))) /\ (forall gr_product_index_functional_secondsteps. (exists ge_gap_functional_secondstepsindex_bound. ge_gap_functional_secondstepsindex_bound + S (gr_product_index_functional_secondsteps) = (l)) -> exists gr_product_factor_functional_secondsteps gr_product_before_functional_secondsteps gr_product_after_functional_secondsteps. ((((exists ff_h_gprod_functional_secondstepsfactor. ff_h_gprod_functional_secondstepsfactor + S (gr_product_factor_functional_secondsteps) = S ((S (gr_product_index_functional_secondsteps)) * c)) /\ exists ff_q_gprod_functional_secondstepsfactor. b = ff_q_gprod_functional_secondstepsfactor * S ((S (gr_product_index_functional_secondsteps)) * c) + (gr_product_factor_functional_secondsteps))) /\ ((((exists ff_h_gprod_functional_secondstepsbefore. ff_h_gprod_functional_secondstepsbefore + S (gr_product_before_functional_secondsteps) = S ((S (gr_product_index_functional_secondsteps)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstepsbefore. gr_product_trace_functional_second = ff_q_gprod_functional_secondstepsbefore * S ((S (gr_product_index_functional_secondsteps)) * gr_product_scale_functional_second) + (gr_product_before_functional_secondsteps))) /\ ((((exists ff_h_gprod_functional_secondstepsafter. ff_h_gprod_functional_secondstepsafter + S (gr_product_after_functional_secondsteps) = S ((S (S (gr_product_index_functional_secondsteps))) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstepsafter. gr_product_trace_functional_second = ff_q_gprod_functional_secondstepsafter * S ((S (S (gr_product_index_functional_secondsteps))) * gr_product_scale_functional_second) + (gr_product_after_functional_secondsteps))) /\ (exists ge_first_rp_functional_secondstepsmultiply ge_first_rn_functional_secondstepsmultiply ge_first_ip_functional_secondstepsmultiply ge_first_in_functional_secondstepsmultiply ge_second_rp_functional_secondstepsmultiply ge_second_rn_functional_secondstepsmultiply ge_second_ip_functional_secondstepsmultiply ge_second_in_functional_secondstepsmultiply. ((exists ge_representation_real_code_functional_secondstepsmultiplyfirst ge_representation_imaginary_code_functional_secondstepsmultiplyfirst. (((gr_product_before_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst)) * S ((ge_representation_real_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplyfirstreal ge_balance_negative_functional_secondstepsmultiplyfirstreal. (((((ge_representation_real_code_functional_secondstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_secondstepsmultiplyfirstreal) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplyfirst) = 2 * ge_signed_half_functional_secondstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstreal) = S ge_signed_half_functional_secondstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplyfirstreal = (ge_first_rn_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplyfirstimaginary ge_balance_negative_functional_secondstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_secondstepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) = 2 * ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstimaginary) = S ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplyfirstimaginary = (ge_first_in_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_secondstepsmultiplysecond ge_representation_imaginary_code_functional_secondstepsmultiplysecond. (((gr_product_factor_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond)) * S ((ge_representation_real_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplysecondreal ge_balance_negative_functional_secondstepsmultiplysecondreal. (((((ge_representation_real_code_functional_secondstepsmultiplysecond) = 2 * (ge_balance_positive_functional_secondstepsmultiplysecondreal) /\ (ge_balance_negative_functional_secondstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplysecond) = 2 * ge_signed_half_functional_secondstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplysecondreal) = S ge_signed_half_functional_secondstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplysecondreal = (ge_second_rn_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplysecondimaginary ge_balance_negative_functional_secondstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) = 2 * (ge_balance_positive_functional_secondstepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) = 2 * ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplysecondimaginary) = S ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplysecondimaginary = (ge_second_in_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_secondstepsmultiplyoutput ge_representation_imaginary_code_functional_secondstepsmultiplyoutput. (((gr_product_after_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput)) * S ((ge_representation_real_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplyoutputreal ge_balance_negative_functional_secondstepsmultiplyoutputreal. (((((ge_representation_real_code_functional_secondstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_secondstepsmultiplyoutputreal) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplyoutput) = 2 * ge_signed_half_functional_secondstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputreal) = S ge_signed_half_functional_secondstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))))))) + ge_balance_negative_functional_secondstepsmultiplyoutputreal = (((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))))))) + ge_balance_positive_functional_secondstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplyoutputimaginary ge_balance_negative_functional_secondstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_secondstepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) = 2 * ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputimaginary) = S ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))))))) + ge_balance_negative_functional_secondstepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))))))) + ge_balance_positive_functional_secondstepsmultiplyoutputimaginary)))))))))))))))) -> P=QConstructive proof overview
Generated structural guide
Two actual Gaussian multiplication traces on the same finite beta prefix have literally equal canonical endpoint codes.
The unchanged tactic script uses 4 declared prerequisites and contains 75 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
GF0087 gaussian_product_empty_value GF0089 gaussian_product_successor_decompose beta_at_unique Stable theorem; checked-use authorized gaussian_multiply_functional Alpha theorem; checked-use authorizedDirect dependents
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
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)
01Induction on lL1–10
02Use earlier factsL11–13
03Establish heqL14–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product empty value.
04Fix variables and assumptionsL24–27
05Establish hsL28–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.
06Separate the logical casesL35–38
07Establish htL39–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.
08Separate the logical casesL46–49
09Establish hfactorL50–58
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
10Establish hprefixL59–68
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
11Use earlier factsL69–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L69
specialize gaussian_multiply_functional (x3) - L70
specialize gaussian_multiply_functional (x2) - L71
specialize gaussian_multiply_functional (P) - L72
specialize gaussian_multiply_functional (Q) - L73
apply gaussian_multiply_functional - L74
exact hs_witness_witness_right_right - L75
exact ht_witness_witness_right_right
Original exact command ledger · 75 lines
- 0001
induction l - 0002
intro b - 0003
intro c - 0004
intro P - 0005
intro Q - 0006
intro hP - 0007
intro hQ - 0008
trans 6 - 0009
specialize gaussian_product_empty_value (b) - 0010
specialize gaussian_product_empty_value (c) - 0011
specialize gaussian_product_empty_value (P) - 0012
apply gaussian_product_empty_value - 0013
exact hP - 0014
have heq : Q=6 - 0015
specialize gaussian_product_empty_value (b) - 0016
specialize gaussian_product_empty_value (c) - 0017
specialize gaussian_product_empty_value (Q) - 0018
apply gaussian_product_empty_value - 0019
exact hQ - 0020
symm - 0021
exact heq - 0022
intro b - 0023
intro c - 0024
intro P - 0025
intro Q - 0026
intro hP - 0027
intro hQ - 0028
have hs : exists a R. ((((exists ff_h_gprod_functional_first_factor. ff_h_gprod_functional_first_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_functional_first_factor. b = ff_q_gprod_functional_first_factor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_functional_first_prefix gr_product_scale_functional_first_prefix. ((((exists ff_h_gprod_functional_first_prefixstart. ff_h_gprod_functional_first_prefixstart + S (6) = S ((S (0)) * gr_product_scale_functional_first_prefix)) /\ exists ff_q_gprod_functional_first_prefixstart. gr_product_trace_functional_first_prefix = ff_q_gprod_functional_first_prefixstart * S ((S (0)) * gr_product_scale_functional_first_prefix) + (6))) /\ ((((exists ff_h_gprod_functional_first_prefixend. ff_h_gprod_functional_first_prefixend + S (R) = S ((S (l)) * gr_product_scale_functional_first_prefix)) /\ exists ff_q_gprod_functional_first_prefixend. gr_product_trace_functional_first_prefix = ff_q_gprod_functional_first_prefixend * S ((S (l)) * gr_product_scale_functional_first_prefix) + (R))) /\ (forall gr_product_index_functional_first_prefixsteps. (exists ge_gap_functional_first_prefixstepsindex_bound. ge_gap_functional_first_prefixstepsindex_bound + S (gr_product_index_functional_first_prefixsteps) = (l)) -> exists gr_product_factor_functional_first_prefixsteps gr_product_before_functional_first_prefixsteps gr_product_after_functional_first_prefixsteps. ((((exists ff_h_gprod_functional_first_prefixstepsfactor. ff_h_gprod_functional_first_prefixstepsfactor + S (gr_product_factor_functional_first_prefixsteps) = S ((S (gr_product_index_functional_first_prefixsteps)) * c)) /\ exists ff_q_gprod_functional_first_prefixstepsfactor. b = ff_q_gprod_functional_first_prefixstepsfactor * S ((S (gr_product_index_functional_first_prefixsteps)) * c) + (gr_product_factor_functional_first_prefixsteps))) /\ ((((exists ff_h_gprod_functional_first_prefixstepsbefore. ff_h_gprod_functional_first_prefixstepsbefore + S (gr_product_before_functional_first_prefixsteps) = S ((S (gr_product_index_functional_first_prefixsteps)) * gr_product_scale_functional_first_prefix)) /\ exists ff_q_gprod_functional_first_prefixstepsbefore. gr_product_trace_functional_first_prefix = ff_q_gprod_functional_first_prefixstepsbefore * S ((S (gr_product_index_functional_first_prefixsteps)) * gr_product_scale_functional_first_prefix) + (gr_product_before_functional_first_prefixsteps))) /\ ((((exists ff_h_gprod_functional_first_prefixstepsafter. ff_h_gprod_functional_first_prefixstepsafter + S (gr_product_after_functional_first_prefixsteps) = S ((S (S (gr_product_index_functional_first_prefixsteps))) * gr_product_scale_functional_first_prefix)) /\ exists ff_q_gprod_functional_first_prefixstepsafter. gr_product_trace_functional_first_prefix = ff_q_gprod_functional_first_prefixstepsafter * S ((S (S (gr_product_index_functional_first_prefixsteps))) * gr_product_scale_functional_first_prefix) + (gr_product_after_functional_first_prefixsteps))) /\ (exists ge_first_rp_functional_first_prefixstepsmultiply ge_first_rn_functional_first_prefixstepsmultiply ge_first_ip_functional_first_prefixstepsmultiply ge_first_in_functional_first_prefixstepsmultiply ge_second_rp_functional_first_prefixstepsmultiply ge_second_rn_functional_first_prefixstepsmultiply ge_second_ip_functional_first_prefixstepsmultiply ge_second_in_functional_first_prefixstepsmultiply. ((exists ge_representation_real_code_functional_first_prefixstepsmultiplyfirst ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst. (((gr_product_before_functional_first_prefixsteps) = ((ge_representation_real_code_functional_first_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_functional_first_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_first_prefixstepsmultiplyfirstreal ge_balance_negative_functional_first_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_functional_first_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_first_prefixstepsmultiplyfirst) = 2 * ge_signed_half_functional_first_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyfirstreal) = S ge_signed_half_functional_first_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_first_prefixstepsmultiply) + ge_balance_negative_functional_first_prefixstepsmultiplyfirstreal = (ge_first_rn_functional_first_prefixstepsmultiply) + ge_balance_positive_functional_first_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_first_prefixstepsmultiplyfirstimaginary ge_balance_negative_functional_first_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyfirst) = 2 * ge_signed_half_functional_first_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_functional_first_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_first_prefixstepsmultiply) + ge_balance_negative_functional_first_prefixstepsmultiplyfirstimaginary = (ge_first_in_functional_first_prefixstepsmultiply) + ge_balance_positive_functional_first_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_first_prefixstepsmultiplysecond ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond. (((gr_product_factor_functional_first_prefixsteps) = ((ge_representation_real_code_functional_first_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_functional_first_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_first_prefixstepsmultiplysecondreal ge_balance_negative_functional_first_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_functional_first_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_functional_first_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_first_prefixstepsmultiplysecond) = 2 * ge_signed_half_functional_first_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplysecondreal) = S ge_signed_half_functional_first_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_first_prefixstepsmultiply) + ge_balance_negative_functional_first_prefixstepsmultiplysecondreal = (ge_second_rn_functional_first_prefixstepsmultiply) + ge_balance_positive_functional_first_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_first_prefixstepsmultiplysecondimaginary ge_balance_negative_functional_first_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_first_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_first_prefixstepsmultiplysecond) = 2 * ge_signed_half_functional_first_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplysecondimaginary) = S ge_signed_half_functional_first_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_first_prefixstepsmultiply) + ge_balance_negative_functional_first_prefixstepsmultiplysecondimaginary = (ge_second_in_functional_first_prefixstepsmultiply) + ge_balance_positive_functional_first_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_first_prefixstepsmultiplyoutput ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput. (((gr_product_after_functional_first_prefixsteps) = ((ge_representation_real_code_functional_first_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_functional_first_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_first_prefixstepsmultiplyoutputreal ge_balance_negative_functional_first_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_functional_first_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_first_prefixstepsmultiplyoutput) = 2 * ge_signed_half_functional_first_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyoutputreal) = S ge_signed_half_functional_first_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_first_prefixstepsmultiply) * (ge_second_rp_functional_first_prefixstepsmultiply))) + (((ge_first_rn_functional_first_prefixstepsmultiply) * (ge_second_rn_functional_first_prefixstepsmultiply))))) + (((((ge_first_ip_functional_first_prefixstepsmultiply) * (ge_second_in_functional_first_prefixstepsmultiply))) + (((ge_first_in_functional_first_prefixstepsmultiply) * (ge_second_ip_functional_first_prefixstepsmultiply))))))) + ge_balance_negative_functional_first_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_functional_first_prefixstepsmultiply) * (ge_second_rn_functional_first_prefixstepsmultiply))) + (((ge_first_rn_functional_first_prefixstepsmultiply) * (ge_second_rp_functional_first_prefixstepsmultiply))))) + (((((ge_first_ip_functional_first_prefixstepsmultiply) * (ge_second_ip_functional_first_prefixstepsmultiply))) + (((ge_first_in_functional_first_prefixstepsmultiply) * (ge_second_in_functional_first_prefixstepsmultiply))))))) + ge_balance_positive_functional_first_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_first_prefixstepsmultiplyoutputimaginary ge_balance_negative_functional_first_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_first_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_first_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_first_prefixstepsmultiplyoutput) = 2 * ge_signed_half_functional_first_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_first_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_first_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_functional_first_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_first_prefixstepsmultiply) * (ge_second_ip_functional_first_prefixstepsmultiply))) + (((ge_first_rn_functional_first_prefixstepsmultiply) * (ge_second_in_functional_first_prefixstepsmultiply))))) + (((((ge_first_ip_functional_first_prefixstepsmultiply) * (ge_second_rp_functional_first_prefixstepsmultiply))) + (((ge_first_in_functional_first_prefixstepsmultiply) * (ge_second_rn_functional_first_prefixstepsmultiply))))))) + ge_balance_negative_functional_first_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_first_prefixstepsmultiply) * (ge_second_in_functional_first_prefixstepsmultiply))) + (((ge_first_rn_functional_first_prefixstepsmultiply) * (ge_second_ip_functional_first_prefixstepsmultiply))))) + (((((ge_first_ip_functional_first_prefixstepsmultiply) * (ge_second_rn_functional_first_prefixstepsmultiply))) + (((ge_first_in_functional_first_prefixstepsmultiply) * (ge_second_rp_functional_first_prefixstepsmultiply))))))) + ge_balance_positive_functional_first_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_functional_first_multiply ge_first_rn_functional_first_multiply ge_first_ip_functional_first_multiply ge_first_in_functional_first_multiply ge_second_rp_functional_first_multiply ge_second_rn_functional_first_multiply ge_second_ip_functional_first_multiply ge_second_in_functional_first_multiply. ((exists ge_representation_real_code_functional_first_multiplyfirst ge_representation_imaginary_code_functional_first_multiplyfirst. (((R) = ((ge_representation_real_code_functional_first_multiplyfirst) + (ge_representation_imaginary_code_functional_first_multiplyfirst)) * S ((ge_representation_real_code_functional_first_multiplyfirst) + (ge_representation_imaginary_code_functional_first_multiplyfirst)) + ((ge_representation_imaginary_code_functional_first_multiplyfirst) + (ge_representation_imaginary_code_functional_first_multiplyfirst))) /\ ((exists ge_balance_positive_functional_first_multiplyfirstreal ge_balance_negative_functional_first_multiplyfirstreal. (((((ge_representation_real_code_functional_first_multiplyfirst) = 2 * (ge_balance_positive_functional_first_multiplyfirstreal) /\ (ge_balance_negative_functional_first_multiplyfirstreal) = 0) \/ exists ge_signed_half_functional_first_multiplyfirstrealdecode. (((ge_representation_real_code_functional_first_multiplyfirst) = 2 * ge_signed_half_functional_first_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_first_multiplyfirstreal) = 0) /\ (ge_balance_negative_functional_first_multiplyfirstreal) = S ge_signed_half_functional_first_multiplyfirstrealdecode))) /\ ((ge_first_rp_functional_first_multiply) + ge_balance_negative_functional_first_multiplyfirstreal = (ge_first_rn_functional_first_multiply) + ge_balance_positive_functional_first_multiplyfirstreal))) /\ (exists ge_balance_positive_functional_first_multiplyfirstimaginary ge_balance_negative_functional_first_multiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_first_multiplyfirst) = 2 * (ge_balance_positive_functional_first_multiplyfirstimaginary) /\ (ge_balance_negative_functional_first_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_first_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_first_multiplyfirst) = 2 * ge_signed_half_functional_first_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_first_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_first_multiplyfirstimaginary) = S ge_signed_half_functional_first_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_first_multiply) + ge_balance_negative_functional_first_multiplyfirstimaginary = (ge_first_in_functional_first_multiply) + ge_balance_positive_functional_first_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_first_multiplysecond ge_representation_imaginary_code_functional_first_multiplysecond. (((a) = ((ge_representation_real_code_functional_first_multiplysecond) + (ge_representation_imaginary_code_functional_first_multiplysecond)) * S ((ge_representation_real_code_functional_first_multiplysecond) + (ge_representation_imaginary_code_functional_first_multiplysecond)) + ((ge_representation_imaginary_code_functional_first_multiplysecond) + (ge_representation_imaginary_code_functional_first_multiplysecond))) /\ ((exists ge_balance_positive_functional_first_multiplysecondreal ge_balance_negative_functional_first_multiplysecondreal. (((((ge_representation_real_code_functional_first_multiplysecond) = 2 * (ge_balance_positive_functional_first_multiplysecondreal) /\ (ge_balance_negative_functional_first_multiplysecondreal) = 0) \/ exists ge_signed_half_functional_first_multiplysecondrealdecode. (((ge_representation_real_code_functional_first_multiplysecond) = 2 * ge_signed_half_functional_first_multiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_first_multiplysecondreal) = 0) /\ (ge_balance_negative_functional_first_multiplysecondreal) = S ge_signed_half_functional_first_multiplysecondrealdecode))) /\ ((ge_second_rp_functional_first_multiply) + ge_balance_negative_functional_first_multiplysecondreal = (ge_second_rn_functional_first_multiply) + ge_balance_positive_functional_first_multiplysecondreal))) /\ (exists ge_balance_positive_functional_first_multiplysecondimaginary ge_balance_negative_functional_first_multiplysecondimaginary. (((((ge_representation_imaginary_code_functional_first_multiplysecond) = 2 * (ge_balance_positive_functional_first_multiplysecondimaginary) /\ (ge_balance_negative_functional_first_multiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_first_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_first_multiplysecond) = 2 * ge_signed_half_functional_first_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_first_multiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_first_multiplysecondimaginary) = S ge_signed_half_functional_first_multiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_first_multiply) + ge_balance_negative_functional_first_multiplysecondimaginary = (ge_second_in_functional_first_multiply) + ge_balance_positive_functional_first_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_first_multiplyoutput ge_representation_imaginary_code_functional_first_multiplyoutput. (((P) = ((ge_representation_real_code_functional_first_multiplyoutput) + (ge_representation_imaginary_code_functional_first_multiplyoutput)) * S ((ge_representation_real_code_functional_first_multiplyoutput) + (ge_representation_imaginary_code_functional_first_multiplyoutput)) + ((ge_representation_imaginary_code_functional_first_multiplyoutput) + (ge_representation_imaginary_code_functional_first_multiplyoutput))) /\ ((exists ge_balance_positive_functional_first_multiplyoutputreal ge_balance_negative_functional_first_multiplyoutputreal. (((((ge_representation_real_code_functional_first_multiplyoutput) = 2 * (ge_balance_positive_functional_first_multiplyoutputreal) /\ (ge_balance_negative_functional_first_multiplyoutputreal) = 0) \/ exists ge_signed_half_functional_first_multiplyoutputrealdecode. (((ge_representation_real_code_functional_first_multiplyoutput) = 2 * ge_signed_half_functional_first_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_first_multiplyoutputreal) = 0) /\ (ge_balance_negative_functional_first_multiplyoutputreal) = S ge_signed_half_functional_first_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_first_multiply) * (ge_second_rp_functional_first_multiply))) + (((ge_first_rn_functional_first_multiply) * (ge_second_rn_functional_first_multiply))))) + (((((ge_first_ip_functional_first_multiply) * (ge_second_in_functional_first_multiply))) + (((ge_first_in_functional_first_multiply) * (ge_second_ip_functional_first_multiply))))))) + ge_balance_negative_functional_first_multiplyoutputreal = (((((((ge_first_rp_functional_first_multiply) * (ge_second_rn_functional_first_multiply))) + (((ge_first_rn_functional_first_multiply) * (ge_second_rp_functional_first_multiply))))) + (((((ge_first_ip_functional_first_multiply) * (ge_second_ip_functional_first_multiply))) + (((ge_first_in_functional_first_multiply) * (ge_second_in_functional_first_multiply))))))) + ge_balance_positive_functional_first_multiplyoutputreal))) /\ (exists ge_balance_positive_functional_first_multiplyoutputimaginary ge_balance_negative_functional_first_multiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_first_multiplyoutput) = 2 * (ge_balance_positive_functional_first_multiplyoutputimaginary) /\ (ge_balance_negative_functional_first_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_first_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_first_multiplyoutput) = 2 * ge_signed_half_functional_first_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_first_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_first_multiplyoutputimaginary) = S ge_signed_half_functional_first_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_first_multiply) * (ge_second_ip_functional_first_multiply))) + (((ge_first_rn_functional_first_multiply) * (ge_second_in_functional_first_multiply))))) + (((((ge_first_ip_functional_first_multiply) * (ge_second_rp_functional_first_multiply))) + (((ge_first_in_functional_first_multiply) * (ge_second_rn_functional_first_multiply))))))) + ge_balance_negative_functional_first_multiplyoutputimaginary = (((((((ge_first_rp_functional_first_multiply) * (ge_second_in_functional_first_multiply))) + (((ge_first_rn_functional_first_multiply) * (ge_second_ip_functional_first_multiply))))) + (((((ge_first_ip_functional_first_multiply) * (ge_second_rn_functional_first_multiply))) + (((ge_first_in_functional_first_multiply) * (ge_second_rp_functional_first_multiply))))))) + ge_balance_positive_functional_first_multiplyoutputimaginary))))))))))) - 0029
specialize gaussian_product_successor_decompose (b) - 0030
specialize gaussian_product_successor_decompose (c) - 0031
specialize gaussian_product_successor_decompose (l) - 0032
specialize gaussian_product_successor_decompose (P) - 0033
apply gaussian_product_successor_decompose - 0034
exact hP - 0035
cases hs - 0036
cases hs_witness - 0037
cases hs_witness_witness - 0038
cases hs_witness_witness_right - 0039
have ht : exists a R. ((((exists ff_h_gprod_functional_second_factor. ff_h_gprod_functional_second_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_functional_second_factor. b = ff_q_gprod_functional_second_factor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_functional_second_prefix gr_product_scale_functional_second_prefix. ((((exists ff_h_gprod_functional_second_prefixstart. ff_h_gprod_functional_second_prefixstart + S (6) = S ((S (0)) * gr_product_scale_functional_second_prefix)) /\ exists ff_q_gprod_functional_second_prefixstart. gr_product_trace_functional_second_prefix = ff_q_gprod_functional_second_prefixstart * S ((S (0)) * gr_product_scale_functional_second_prefix) + (6))) /\ ((((exists ff_h_gprod_functional_second_prefixend. ff_h_gprod_functional_second_prefixend + S (R) = S ((S (l)) * gr_product_scale_functional_second_prefix)) /\ exists ff_q_gprod_functional_second_prefixend. gr_product_trace_functional_second_prefix = ff_q_gprod_functional_second_prefixend * S ((S (l)) * gr_product_scale_functional_second_prefix) + (R))) /\ (forall gr_product_index_functional_second_prefixsteps. (exists ge_gap_functional_second_prefixstepsindex_bound. ge_gap_functional_second_prefixstepsindex_bound + S (gr_product_index_functional_second_prefixsteps) = (l)) -> exists gr_product_factor_functional_second_prefixsteps gr_product_before_functional_second_prefixsteps gr_product_after_functional_second_prefixsteps. ((((exists ff_h_gprod_functional_second_prefixstepsfactor. ff_h_gprod_functional_second_prefixstepsfactor + S (gr_product_factor_functional_second_prefixsteps) = S ((S (gr_product_index_functional_second_prefixsteps)) * c)) /\ exists ff_q_gprod_functional_second_prefixstepsfactor. b = ff_q_gprod_functional_second_prefixstepsfactor * S ((S (gr_product_index_functional_second_prefixsteps)) * c) + (gr_product_factor_functional_second_prefixsteps))) /\ ((((exists ff_h_gprod_functional_second_prefixstepsbefore. ff_h_gprod_functional_second_prefixstepsbefore + S (gr_product_before_functional_second_prefixsteps) = S ((S (gr_product_index_functional_second_prefixsteps)) * gr_product_scale_functional_second_prefix)) /\ exists ff_q_gprod_functional_second_prefixstepsbefore. gr_product_trace_functional_second_prefix = ff_q_gprod_functional_second_prefixstepsbefore * S ((S (gr_product_index_functional_second_prefixsteps)) * gr_product_scale_functional_second_prefix) + (gr_product_before_functional_second_prefixsteps))) /\ ((((exists ff_h_gprod_functional_second_prefixstepsafter. ff_h_gprod_functional_second_prefixstepsafter + S (gr_product_after_functional_second_prefixsteps) = S ((S (S (gr_product_index_functional_second_prefixsteps))) * gr_product_scale_functional_second_prefix)) /\ exists ff_q_gprod_functional_second_prefixstepsafter. gr_product_trace_functional_second_prefix = ff_q_gprod_functional_second_prefixstepsafter * S ((S (S (gr_product_index_functional_second_prefixsteps))) * gr_product_scale_functional_second_prefix) + (gr_product_after_functional_second_prefixsteps))) /\ (exists ge_first_rp_functional_second_prefixstepsmultiply ge_first_rn_functional_second_prefixstepsmultiply ge_first_ip_functional_second_prefixstepsmultiply ge_first_in_functional_second_prefixstepsmultiply ge_second_rp_functional_second_prefixstepsmultiply ge_second_rn_functional_second_prefixstepsmultiply ge_second_ip_functional_second_prefixstepsmultiply ge_second_in_functional_second_prefixstepsmultiply. ((exists ge_representation_real_code_functional_second_prefixstepsmultiplyfirst ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst. (((gr_product_before_functional_second_prefixsteps) = ((ge_representation_real_code_functional_second_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_functional_second_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_second_prefixstepsmultiplyfirstreal ge_balance_negative_functional_second_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_functional_second_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_second_prefixstepsmultiplyfirst) = 2 * ge_signed_half_functional_second_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyfirstreal) = S ge_signed_half_functional_second_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_second_prefixstepsmultiply) + ge_balance_negative_functional_second_prefixstepsmultiplyfirstreal = (ge_first_rn_functional_second_prefixstepsmultiply) + ge_balance_positive_functional_second_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_second_prefixstepsmultiplyfirstimaginary ge_balance_negative_functional_second_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyfirst) = 2 * ge_signed_half_functional_second_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_functional_second_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_second_prefixstepsmultiply) + ge_balance_negative_functional_second_prefixstepsmultiplyfirstimaginary = (ge_first_in_functional_second_prefixstepsmultiply) + ge_balance_positive_functional_second_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_second_prefixstepsmultiplysecond ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond. (((gr_product_factor_functional_second_prefixsteps) = ((ge_representation_real_code_functional_second_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_functional_second_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_second_prefixstepsmultiplysecondreal ge_balance_negative_functional_second_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_functional_second_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_functional_second_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_second_prefixstepsmultiplysecond) = 2 * ge_signed_half_functional_second_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplysecondreal) = S ge_signed_half_functional_second_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_second_prefixstepsmultiply) + ge_balance_negative_functional_second_prefixstepsmultiplysecondreal = (ge_second_rn_functional_second_prefixstepsmultiply) + ge_balance_positive_functional_second_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_second_prefixstepsmultiplysecondimaginary ge_balance_negative_functional_second_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_second_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_second_prefixstepsmultiplysecond) = 2 * ge_signed_half_functional_second_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplysecondimaginary) = S ge_signed_half_functional_second_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_second_prefixstepsmultiply) + ge_balance_negative_functional_second_prefixstepsmultiplysecondimaginary = (ge_second_in_functional_second_prefixstepsmultiply) + ge_balance_positive_functional_second_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_second_prefixstepsmultiplyoutput ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput. (((gr_product_after_functional_second_prefixsteps) = ((ge_representation_real_code_functional_second_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_functional_second_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_second_prefixstepsmultiplyoutputreal ge_balance_negative_functional_second_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_functional_second_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_second_prefixstepsmultiplyoutput) = 2 * ge_signed_half_functional_second_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyoutputreal) = S ge_signed_half_functional_second_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_second_prefixstepsmultiply) * (ge_second_rp_functional_second_prefixstepsmultiply))) + (((ge_first_rn_functional_second_prefixstepsmultiply) * (ge_second_rn_functional_second_prefixstepsmultiply))))) + (((((ge_first_ip_functional_second_prefixstepsmultiply) * (ge_second_in_functional_second_prefixstepsmultiply))) + (((ge_first_in_functional_second_prefixstepsmultiply) * (ge_second_ip_functional_second_prefixstepsmultiply))))))) + ge_balance_negative_functional_second_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_functional_second_prefixstepsmultiply) * (ge_second_rn_functional_second_prefixstepsmultiply))) + (((ge_first_rn_functional_second_prefixstepsmultiply) * (ge_second_rp_functional_second_prefixstepsmultiply))))) + (((((ge_first_ip_functional_second_prefixstepsmultiply) * (ge_second_ip_functional_second_prefixstepsmultiply))) + (((ge_first_in_functional_second_prefixstepsmultiply) * (ge_second_in_functional_second_prefixstepsmultiply))))))) + ge_balance_positive_functional_second_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_second_prefixstepsmultiplyoutputimaginary ge_balance_negative_functional_second_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_second_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_second_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_second_prefixstepsmultiplyoutput) = 2 * ge_signed_half_functional_second_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_second_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_second_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_functional_second_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_second_prefixstepsmultiply) * (ge_second_ip_functional_second_prefixstepsmultiply))) + (((ge_first_rn_functional_second_prefixstepsmultiply) * (ge_second_in_functional_second_prefixstepsmultiply))))) + (((((ge_first_ip_functional_second_prefixstepsmultiply) * (ge_second_rp_functional_second_prefixstepsmultiply))) + (((ge_first_in_functional_second_prefixstepsmultiply) * (ge_second_rn_functional_second_prefixstepsmultiply))))))) + ge_balance_negative_functional_second_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_second_prefixstepsmultiply) * (ge_second_in_functional_second_prefixstepsmultiply))) + (((ge_first_rn_functional_second_prefixstepsmultiply) * (ge_second_ip_functional_second_prefixstepsmultiply))))) + (((((ge_first_ip_functional_second_prefixstepsmultiply) * (ge_second_rn_functional_second_prefixstepsmultiply))) + (((ge_first_in_functional_second_prefixstepsmultiply) * (ge_second_rp_functional_second_prefixstepsmultiply))))))) + ge_balance_positive_functional_second_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_functional_second_multiply ge_first_rn_functional_second_multiply ge_first_ip_functional_second_multiply ge_first_in_functional_second_multiply ge_second_rp_functional_second_multiply ge_second_rn_functional_second_multiply ge_second_ip_functional_second_multiply ge_second_in_functional_second_multiply. ((exists ge_representation_real_code_functional_second_multiplyfirst ge_representation_imaginary_code_functional_second_multiplyfirst. (((R) = ((ge_representation_real_code_functional_second_multiplyfirst) + (ge_representation_imaginary_code_functional_second_multiplyfirst)) * S ((ge_representation_real_code_functional_second_multiplyfirst) + (ge_representation_imaginary_code_functional_second_multiplyfirst)) + ((ge_representation_imaginary_code_functional_second_multiplyfirst) + (ge_representation_imaginary_code_functional_second_multiplyfirst))) /\ ((exists ge_balance_positive_functional_second_multiplyfirstreal ge_balance_negative_functional_second_multiplyfirstreal. (((((ge_representation_real_code_functional_second_multiplyfirst) = 2 * (ge_balance_positive_functional_second_multiplyfirstreal) /\ (ge_balance_negative_functional_second_multiplyfirstreal) = 0) \/ exists ge_signed_half_functional_second_multiplyfirstrealdecode. (((ge_representation_real_code_functional_second_multiplyfirst) = 2 * ge_signed_half_functional_second_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_second_multiplyfirstreal) = 0) /\ (ge_balance_negative_functional_second_multiplyfirstreal) = S ge_signed_half_functional_second_multiplyfirstrealdecode))) /\ ((ge_first_rp_functional_second_multiply) + ge_balance_negative_functional_second_multiplyfirstreal = (ge_first_rn_functional_second_multiply) + ge_balance_positive_functional_second_multiplyfirstreal))) /\ (exists ge_balance_positive_functional_second_multiplyfirstimaginary ge_balance_negative_functional_second_multiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_second_multiplyfirst) = 2 * (ge_balance_positive_functional_second_multiplyfirstimaginary) /\ (ge_balance_negative_functional_second_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_second_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_second_multiplyfirst) = 2 * ge_signed_half_functional_second_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_second_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_second_multiplyfirstimaginary) = S ge_signed_half_functional_second_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_second_multiply) + ge_balance_negative_functional_second_multiplyfirstimaginary = (ge_first_in_functional_second_multiply) + ge_balance_positive_functional_second_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_second_multiplysecond ge_representation_imaginary_code_functional_second_multiplysecond. (((a) = ((ge_representation_real_code_functional_second_multiplysecond) + (ge_representation_imaginary_code_functional_second_multiplysecond)) * S ((ge_representation_real_code_functional_second_multiplysecond) + (ge_representation_imaginary_code_functional_second_multiplysecond)) + ((ge_representation_imaginary_code_functional_second_multiplysecond) + (ge_representation_imaginary_code_functional_second_multiplysecond))) /\ ((exists ge_balance_positive_functional_second_multiplysecondreal ge_balance_negative_functional_second_multiplysecondreal. (((((ge_representation_real_code_functional_second_multiplysecond) = 2 * (ge_balance_positive_functional_second_multiplysecondreal) /\ (ge_balance_negative_functional_second_multiplysecondreal) = 0) \/ exists ge_signed_half_functional_second_multiplysecondrealdecode. (((ge_representation_real_code_functional_second_multiplysecond) = 2 * ge_signed_half_functional_second_multiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_second_multiplysecondreal) = 0) /\ (ge_balance_negative_functional_second_multiplysecondreal) = S ge_signed_half_functional_second_multiplysecondrealdecode))) /\ ((ge_second_rp_functional_second_multiply) + ge_balance_negative_functional_second_multiplysecondreal = (ge_second_rn_functional_second_multiply) + ge_balance_positive_functional_second_multiplysecondreal))) /\ (exists ge_balance_positive_functional_second_multiplysecondimaginary ge_balance_negative_functional_second_multiplysecondimaginary. (((((ge_representation_imaginary_code_functional_second_multiplysecond) = 2 * (ge_balance_positive_functional_second_multiplysecondimaginary) /\ (ge_balance_negative_functional_second_multiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_second_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_second_multiplysecond) = 2 * ge_signed_half_functional_second_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_second_multiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_second_multiplysecondimaginary) = S ge_signed_half_functional_second_multiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_second_multiply) + ge_balance_negative_functional_second_multiplysecondimaginary = (ge_second_in_functional_second_multiply) + ge_balance_positive_functional_second_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_second_multiplyoutput ge_representation_imaginary_code_functional_second_multiplyoutput. (((Q) = ((ge_representation_real_code_functional_second_multiplyoutput) + (ge_representation_imaginary_code_functional_second_multiplyoutput)) * S ((ge_representation_real_code_functional_second_multiplyoutput) + (ge_representation_imaginary_code_functional_second_multiplyoutput)) + ((ge_representation_imaginary_code_functional_second_multiplyoutput) + (ge_representation_imaginary_code_functional_second_multiplyoutput))) /\ ((exists ge_balance_positive_functional_second_multiplyoutputreal ge_balance_negative_functional_second_multiplyoutputreal. (((((ge_representation_real_code_functional_second_multiplyoutput) = 2 * (ge_balance_positive_functional_second_multiplyoutputreal) /\ (ge_balance_negative_functional_second_multiplyoutputreal) = 0) \/ exists ge_signed_half_functional_second_multiplyoutputrealdecode. (((ge_representation_real_code_functional_second_multiplyoutput) = 2 * ge_signed_half_functional_second_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_second_multiplyoutputreal) = 0) /\ (ge_balance_negative_functional_second_multiplyoutputreal) = S ge_signed_half_functional_second_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_second_multiply) * (ge_second_rp_functional_second_multiply))) + (((ge_first_rn_functional_second_multiply) * (ge_second_rn_functional_second_multiply))))) + (((((ge_first_ip_functional_second_multiply) * (ge_second_in_functional_second_multiply))) + (((ge_first_in_functional_second_multiply) * (ge_second_ip_functional_second_multiply))))))) + ge_balance_negative_functional_second_multiplyoutputreal = (((((((ge_first_rp_functional_second_multiply) * (ge_second_rn_functional_second_multiply))) + (((ge_first_rn_functional_second_multiply) * (ge_second_rp_functional_second_multiply))))) + (((((ge_first_ip_functional_second_multiply) * (ge_second_ip_functional_second_multiply))) + (((ge_first_in_functional_second_multiply) * (ge_second_in_functional_second_multiply))))))) + ge_balance_positive_functional_second_multiplyoutputreal))) /\ (exists ge_balance_positive_functional_second_multiplyoutputimaginary ge_balance_negative_functional_second_multiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_second_multiplyoutput) = 2 * (ge_balance_positive_functional_second_multiplyoutputimaginary) /\ (ge_balance_negative_functional_second_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_second_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_second_multiplyoutput) = 2 * ge_signed_half_functional_second_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_second_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_second_multiplyoutputimaginary) = S ge_signed_half_functional_second_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_second_multiply) * (ge_second_ip_functional_second_multiply))) + (((ge_first_rn_functional_second_multiply) * (ge_second_in_functional_second_multiply))))) + (((((ge_first_ip_functional_second_multiply) * (ge_second_rp_functional_second_multiply))) + (((ge_first_in_functional_second_multiply) * (ge_second_rn_functional_second_multiply))))))) + ge_balance_negative_functional_second_multiplyoutputimaginary = (((((((ge_first_rp_functional_second_multiply) * (ge_second_in_functional_second_multiply))) + (((ge_first_rn_functional_second_multiply) * (ge_second_ip_functional_second_multiply))))) + (((((ge_first_ip_functional_second_multiply) * (ge_second_rn_functional_second_multiply))) + (((ge_first_in_functional_second_multiply) * (ge_second_rp_functional_second_multiply))))))) + ge_balance_positive_functional_second_multiplyoutputimaginary))))))))))) - 0040
specialize gaussian_product_successor_decompose (b) - 0041
specialize gaussian_product_successor_decompose (c) - 0042
specialize gaussian_product_successor_decompose (l) - 0043
specialize gaussian_product_successor_decompose (Q) - 0044
apply gaussian_product_successor_decompose - 0045
exact hQ - 0046
cases ht - 0047
cases ht_witness - 0048
cases ht_witness_witness - 0049
cases ht_witness_witness_right - 0050
have hfactor : x=x2 - 0051
specialize beta_at_unique (b) - 0052
specialize beta_at_unique (c) - 0053
specialize beta_at_unique (l) - 0054
specialize beta_at_unique (x) - 0055
specialize beta_at_unique (x2) - 0056
apply beta_at_unique - 0057
exact hs_witness_witness_left - 0058
exact ht_witness_witness_left - 0059
have hprefix : x1=x3 - 0060
specialize IH (b) - 0061
specialize IH (c) - 0062
specialize IH (x1) - 0063
specialize IH (x3) - 0064
apply IH - 0065
exact hs_witness_witness_right_left - 0066
exact ht_witness_witness_right_left - 0067
rewrite hfactor at hs_witness_witness_right_right - 0068
rewrite hprefix at hs_witness_witness_right_right - 0069
specialize gaussian_multiply_functional (x3) - 0070
specialize gaussian_multiply_functional (x2) - 0071
specialize gaussian_multiply_functional (P) - 0072
specialize gaussian_multiply_functional (Q) - 0073
apply gaussian_multiply_functional - 0074
exact hs_witness_witness_right_right - 0075
exact ht_witness_witness_right_right