GF0025

gaussian_multiply_associative

The actual canonical Gaussian multiply graph associates, with all intermediate product/sum codes witnessed.

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

∀ a. ∀ b. ∀ c. ∀ ab. ∀ bc. ∀ t. GMul(a,b,ab) → GMul(ab,c,t) → GMul(b,c,bc) → GMul(a,bc,t)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 6GMul(a,b,c) · 4

Actual proof prerequisites

gaussian_valid_has_representationgaussian_multiply_input_left_validgaussian_multiply_input_right_validgaussian_multiply_for_representations · checked external prerequisitegaussian_multiply_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_product_associate · checked external prerequisite
Original expanded first-order statement 
forall a b c ab bc t. (exists ge_first_rp_associate_first_multiply ge_first_rn_associate_first_multiply ge_first_ip_associate_first_multiply ge_first_in_associate_first_multiply ge_second_rp_associate_first_multiply ge_second_rn_associate_first_multiply ge_second_ip_associate_first_multiply ge_second_in_associate_first_multiply. ((exists ge_representation_real_code_associate_first_multiplyfirst ge_representation_imaginary_code_associate_first_multiplyfirst. (((a) = ((ge_representation_real_code_associate_first_multiplyfirst) + (ge_representation_imaginary_code_associate_first_multiplyfirst)) * S ((ge_representation_real_code_associate_first_multiplyfirst) + (ge_representation_imaginary_code_associate_first_multiplyfirst)) + ((ge_representation_imaginary_code_associate_first_multiplyfirst) + (ge_representation_imaginary_code_associate_first_multiplyfirst))) /\ ((exists ge_balance_positive_associate_first_multiplyfirstreal ge_balance_negative_associate_first_multiplyfirstreal. (((((ge_representation_real_code_associate_first_multiplyfirst) = 2 * (ge_balance_positive_associate_first_multiplyfirstreal) /\ (ge_balance_negative_associate_first_multiplyfirstreal) = 0) \/ exists ge_signed_half_associate_first_multiplyfirstrealdecode. (((ge_representation_real_code_associate_first_multiplyfirst) = 2 * ge_signed_half_associate_first_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_associate_first_multiplyfirstreal) = 0) /\ (ge_balance_negative_associate_first_multiplyfirstreal) = S ge_signed_half_associate_first_multiplyfirstrealdecode))) /\ ((ge_first_rp_associate_first_multiply) + ge_balance_negative_associate_first_multiplyfirstreal = (ge_first_rn_associate_first_multiply) + ge_balance_positive_associate_first_multiplyfirstreal))) /\ (exists ge_balance_positive_associate_first_multiplyfirstimaginary ge_balance_negative_associate_first_multiplyfirstimaginary. (((((ge_representation_imaginary_code_associate_first_multiplyfirst) = 2 * (ge_balance_positive_associate_first_multiplyfirstimaginary) /\ (ge_balance_negative_associate_first_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_associate_first_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_associate_first_multiplyfirst) = 2 * ge_signed_half_associate_first_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_first_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_associate_first_multiplyfirstimaginary) = S ge_signed_half_associate_first_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_associate_first_multiply) + ge_balance_negative_associate_first_multiplyfirstimaginary = (ge_first_in_associate_first_multiply) + ge_balance_positive_associate_first_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_first_multiplysecond ge_representation_imaginary_code_associate_first_multiplysecond. (((b) = ((ge_representation_real_code_associate_first_multiplysecond) + (ge_representation_imaginary_code_associate_first_multiplysecond)) * S ((ge_representation_real_code_associate_first_multiplysecond) + (ge_representation_imaginary_code_associate_first_multiplysecond)) + ((ge_representation_imaginary_code_associate_first_multiplysecond) + (ge_representation_imaginary_code_associate_first_multiplysecond))) /\ ((exists ge_balance_positive_associate_first_multiplysecondreal ge_balance_negative_associate_first_multiplysecondreal. (((((ge_representation_real_code_associate_first_multiplysecond) = 2 * (ge_balance_positive_associate_first_multiplysecondreal) /\ (ge_balance_negative_associate_first_multiplysecondreal) = 0) \/ exists ge_signed_half_associate_first_multiplysecondrealdecode. (((ge_representation_real_code_associate_first_multiplysecond) = 2 * ge_signed_half_associate_first_multiplysecondrealdecode + 1 /\ (ge_balance_positive_associate_first_multiplysecondreal) = 0) /\ (ge_balance_negative_associate_first_multiplysecondreal) = S ge_signed_half_associate_first_multiplysecondrealdecode))) /\ ((ge_second_rp_associate_first_multiply) + ge_balance_negative_associate_first_multiplysecondreal = (ge_second_rn_associate_first_multiply) + ge_balance_positive_associate_first_multiplysecondreal))) /\ (exists ge_balance_positive_associate_first_multiplysecondimaginary ge_balance_negative_associate_first_multiplysecondimaginary. (((((ge_representation_imaginary_code_associate_first_multiplysecond) = 2 * (ge_balance_positive_associate_first_multiplysecondimaginary) /\ (ge_balance_negative_associate_first_multiplysecondimaginary) = 0) \/ exists ge_signed_half_associate_first_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_associate_first_multiplysecond) = 2 * ge_signed_half_associate_first_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_first_multiplysecondimaginary) = 0) /\ (ge_balance_negative_associate_first_multiplysecondimaginary) = S ge_signed_half_associate_first_multiplysecondimaginarydecode))) /\ ((ge_second_ip_associate_first_multiply) + ge_balance_negative_associate_first_multiplysecondimaginary = (ge_second_in_associate_first_multiply) + ge_balance_positive_associate_first_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_first_multiplyoutput ge_representation_imaginary_code_associate_first_multiplyoutput. (((ab) = ((ge_representation_real_code_associate_first_multiplyoutput) + (ge_representation_imaginary_code_associate_first_multiplyoutput)) * S ((ge_representation_real_code_associate_first_multiplyoutput) + (ge_representation_imaginary_code_associate_first_multiplyoutput)) + ((ge_representation_imaginary_code_associate_first_multiplyoutput) + (ge_representation_imaginary_code_associate_first_multiplyoutput))) /\ ((exists ge_balance_positive_associate_first_multiplyoutputreal ge_balance_negative_associate_first_multiplyoutputreal. (((((ge_representation_real_code_associate_first_multiplyoutput) = 2 * (ge_balance_positive_associate_first_multiplyoutputreal) /\ (ge_balance_negative_associate_first_multiplyoutputreal) = 0) \/ exists ge_signed_half_associate_first_multiplyoutputrealdecode. (((ge_representation_real_code_associate_first_multiplyoutput) = 2 * ge_signed_half_associate_first_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_associate_first_multiplyoutputreal) = 0) /\ (ge_balance_negative_associate_first_multiplyoutputreal) = S ge_signed_half_associate_first_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_associate_first_multiply) * (ge_second_rp_associate_first_multiply))) + (((ge_first_rn_associate_first_multiply) * (ge_second_rn_associate_first_multiply))))) + (((((ge_first_ip_associate_first_multiply) * (ge_second_in_associate_first_multiply))) + (((ge_first_in_associate_first_multiply) * (ge_second_ip_associate_first_multiply))))))) + ge_balance_negative_associate_first_multiplyoutputreal = (((((((ge_first_rp_associate_first_multiply) * (ge_second_rn_associate_first_multiply))) + (((ge_first_rn_associate_first_multiply) * (ge_second_rp_associate_first_multiply))))) + (((((ge_first_ip_associate_first_multiply) * (ge_second_ip_associate_first_multiply))) + (((ge_first_in_associate_first_multiply) * (ge_second_in_associate_first_multiply))))))) + ge_balance_positive_associate_first_multiplyoutputreal))) /\ (exists ge_balance_positive_associate_first_multiplyoutputimaginary ge_balance_negative_associate_first_multiplyoutputimaginary. (((((ge_representation_imaginary_code_associate_first_multiplyoutput) = 2 * (ge_balance_positive_associate_first_multiplyoutputimaginary) /\ (ge_balance_negative_associate_first_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_associate_first_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_associate_first_multiplyoutput) = 2 * ge_signed_half_associate_first_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_first_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_associate_first_multiplyoutputimaginary) = S ge_signed_half_associate_first_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_first_multiply) * (ge_second_ip_associate_first_multiply))) + (((ge_first_rn_associate_first_multiply) * (ge_second_in_associate_first_multiply))))) + (((((ge_first_ip_associate_first_multiply) * (ge_second_rp_associate_first_multiply))) + (((ge_first_in_associate_first_multiply) * (ge_second_rn_associate_first_multiply))))))) + ge_balance_negative_associate_first_multiplyoutputimaginary = (((((((ge_first_rp_associate_first_multiply) * (ge_second_in_associate_first_multiply))) + (((ge_first_rn_associate_first_multiply) * (ge_second_ip_associate_first_multiply))))) + (((((ge_first_ip_associate_first_multiply) * (ge_second_rn_associate_first_multiply))) + (((ge_first_in_associate_first_multiply) * (ge_second_rp_associate_first_multiply))))))) + ge_balance_positive_associate_first_multiplyoutputimaginary))))))))) -> (exists ge_first_rp_associate_second_multiply ge_first_rn_associate_second_multiply ge_first_ip_associate_second_multiply ge_first_in_associate_second_multiply ge_second_rp_associate_second_multiply ge_second_rn_associate_second_multiply ge_second_ip_associate_second_multiply ge_second_in_associate_second_multiply. ((exists ge_representation_real_code_associate_second_multiplyfirst ge_representation_imaginary_code_associate_second_multiplyfirst. (((ab) = ((ge_representation_real_code_associate_second_multiplyfirst) + (ge_representation_imaginary_code_associate_second_multiplyfirst)) * S ((ge_representation_real_code_associate_second_multiplyfirst) + (ge_representation_imaginary_code_associate_second_multiplyfirst)) + ((ge_representation_imaginary_code_associate_second_multiplyfirst) + (ge_representation_imaginary_code_associate_second_multiplyfirst))) /\ ((exists ge_balance_positive_associate_second_multiplyfirstreal ge_balance_negative_associate_second_multiplyfirstreal. (((((ge_representation_real_code_associate_second_multiplyfirst) = 2 * (ge_balance_positive_associate_second_multiplyfirstreal) /\ (ge_balance_negative_associate_second_multiplyfirstreal) = 0) \/ exists ge_signed_half_associate_second_multiplyfirstrealdecode. (((ge_representation_real_code_associate_second_multiplyfirst) = 2 * ge_signed_half_associate_second_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_associate_second_multiplyfirstreal) = 0) /\ (ge_balance_negative_associate_second_multiplyfirstreal) = S ge_signed_half_associate_second_multiplyfirstrealdecode))) /\ ((ge_first_rp_associate_second_multiply) + ge_balance_negative_associate_second_multiplyfirstreal = (ge_first_rn_associate_second_multiply) + ge_balance_positive_associate_second_multiplyfirstreal))) /\ (exists ge_balance_positive_associate_second_multiplyfirstimaginary ge_balance_negative_associate_second_multiplyfirstimaginary. (((((ge_representation_imaginary_code_associate_second_multiplyfirst) = 2 * (ge_balance_positive_associate_second_multiplyfirstimaginary) /\ (ge_balance_negative_associate_second_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_associate_second_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_associate_second_multiplyfirst) = 2 * ge_signed_half_associate_second_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_second_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_associate_second_multiplyfirstimaginary) = S ge_signed_half_associate_second_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_associate_second_multiply) + ge_balance_negative_associate_second_multiplyfirstimaginary = (ge_first_in_associate_second_multiply) + ge_balance_positive_associate_second_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_second_multiplysecond ge_representation_imaginary_code_associate_second_multiplysecond. (((c) = ((ge_representation_real_code_associate_second_multiplysecond) + (ge_representation_imaginary_code_associate_second_multiplysecond)) * S ((ge_representation_real_code_associate_second_multiplysecond) + (ge_representation_imaginary_code_associate_second_multiplysecond)) + ((ge_representation_imaginary_code_associate_second_multiplysecond) + (ge_representation_imaginary_code_associate_second_multiplysecond))) /\ ((exists ge_balance_positive_associate_second_multiplysecondreal ge_balance_negative_associate_second_multiplysecondreal. (((((ge_representation_real_code_associate_second_multiplysecond) = 2 * (ge_balance_positive_associate_second_multiplysecondreal) /\ (ge_balance_negative_associate_second_multiplysecondreal) = 0) \/ exists ge_signed_half_associate_second_multiplysecondrealdecode. (((ge_representation_real_code_associate_second_multiplysecond) = 2 * ge_signed_half_associate_second_multiplysecondrealdecode + 1 /\ (ge_balance_positive_associate_second_multiplysecondreal) = 0) /\ (ge_balance_negative_associate_second_multiplysecondreal) = S ge_signed_half_associate_second_multiplysecondrealdecode))) /\ ((ge_second_rp_associate_second_multiply) + ge_balance_negative_associate_second_multiplysecondreal = (ge_second_rn_associate_second_multiply) + ge_balance_positive_associate_second_multiplysecondreal))) /\ (exists ge_balance_positive_associate_second_multiplysecondimaginary ge_balance_negative_associate_second_multiplysecondimaginary. (((((ge_representation_imaginary_code_associate_second_multiplysecond) = 2 * (ge_balance_positive_associate_second_multiplysecondimaginary) /\ (ge_balance_negative_associate_second_multiplysecondimaginary) = 0) \/ exists ge_signed_half_associate_second_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_associate_second_multiplysecond) = 2 * ge_signed_half_associate_second_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_second_multiplysecondimaginary) = 0) /\ (ge_balance_negative_associate_second_multiplysecondimaginary) = S ge_signed_half_associate_second_multiplysecondimaginarydecode))) /\ ((ge_second_ip_associate_second_multiply) + ge_balance_negative_associate_second_multiplysecondimaginary = (ge_second_in_associate_second_multiply) + ge_balance_positive_associate_second_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_second_multiplyoutput ge_representation_imaginary_code_associate_second_multiplyoutput. (((t) = ((ge_representation_real_code_associate_second_multiplyoutput) + (ge_representation_imaginary_code_associate_second_multiplyoutput)) * S ((ge_representation_real_code_associate_second_multiplyoutput) + (ge_representation_imaginary_code_associate_second_multiplyoutput)) + ((ge_representation_imaginary_code_associate_second_multiplyoutput) + (ge_representation_imaginary_code_associate_second_multiplyoutput))) /\ ((exists ge_balance_positive_associate_second_multiplyoutputreal ge_balance_negative_associate_second_multiplyoutputreal. (((((ge_representation_real_code_associate_second_multiplyoutput) = 2 * (ge_balance_positive_associate_second_multiplyoutputreal) /\ (ge_balance_negative_associate_second_multiplyoutputreal) = 0) \/ exists ge_signed_half_associate_second_multiplyoutputrealdecode. (((ge_representation_real_code_associate_second_multiplyoutput) = 2 * ge_signed_half_associate_second_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_associate_second_multiplyoutputreal) = 0) /\ (ge_balance_negative_associate_second_multiplyoutputreal) = S ge_signed_half_associate_second_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_associate_second_multiply) * (ge_second_rp_associate_second_multiply))) + (((ge_first_rn_associate_second_multiply) * (ge_second_rn_associate_second_multiply))))) + (((((ge_first_ip_associate_second_multiply) * (ge_second_in_associate_second_multiply))) + (((ge_first_in_associate_second_multiply) * (ge_second_ip_associate_second_multiply))))))) + ge_balance_negative_associate_second_multiplyoutputreal = (((((((ge_first_rp_associate_second_multiply) * (ge_second_rn_associate_second_multiply))) + (((ge_first_rn_associate_second_multiply) * (ge_second_rp_associate_second_multiply))))) + (((((ge_first_ip_associate_second_multiply) * (ge_second_ip_associate_second_multiply))) + (((ge_first_in_associate_second_multiply) * (ge_second_in_associate_second_multiply))))))) + ge_balance_positive_associate_second_multiplyoutputreal))) /\ (exists ge_balance_positive_associate_second_multiplyoutputimaginary ge_balance_negative_associate_second_multiplyoutputimaginary. (((((ge_representation_imaginary_code_associate_second_multiplyoutput) = 2 * (ge_balance_positive_associate_second_multiplyoutputimaginary) /\ (ge_balance_negative_associate_second_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_associate_second_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_associate_second_multiplyoutput) = 2 * ge_signed_half_associate_second_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_second_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_associate_second_multiplyoutputimaginary) = S ge_signed_half_associate_second_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_second_multiply) * (ge_second_ip_associate_second_multiply))) + (((ge_first_rn_associate_second_multiply) * (ge_second_in_associate_second_multiply))))) + (((((ge_first_ip_associate_second_multiply) * (ge_second_rp_associate_second_multiply))) + (((ge_first_in_associate_second_multiply) * (ge_second_rn_associate_second_multiply))))))) + ge_balance_negative_associate_second_multiplyoutputimaginary = (((((((ge_first_rp_associate_second_multiply) * (ge_second_in_associate_second_multiply))) + (((ge_first_rn_associate_second_multiply) * (ge_second_ip_associate_second_multiply))))) + (((((ge_first_ip_associate_second_multiply) * (ge_second_rn_associate_second_multiply))) + (((ge_first_in_associate_second_multiply) * (ge_second_rp_associate_second_multiply))))))) + ge_balance_positive_associate_second_multiplyoutputimaginary))))))))) -> (exists ge_first_rp_associate_third_multiply ge_first_rn_associate_third_multiply ge_first_ip_associate_third_multiply ge_first_in_associate_third_multiply ge_second_rp_associate_third_multiply ge_second_rn_associate_third_multiply ge_second_ip_associate_third_multiply ge_second_in_associate_third_multiply. ((exists ge_representation_real_code_associate_third_multiplyfirst ge_representation_imaginary_code_associate_third_multiplyfirst. (((b) = ((ge_representation_real_code_associate_third_multiplyfirst) + (ge_representation_imaginary_code_associate_third_multiplyfirst)) * S ((ge_representation_real_code_associate_third_multiplyfirst) + (ge_representation_imaginary_code_associate_third_multiplyfirst)) + ((ge_representation_imaginary_code_associate_third_multiplyfirst) + (ge_representation_imaginary_code_associate_third_multiplyfirst))) /\ ((exists ge_balance_positive_associate_third_multiplyfirstreal ge_balance_negative_associate_third_multiplyfirstreal. (((((ge_representation_real_code_associate_third_multiplyfirst) = 2 * (ge_balance_positive_associate_third_multiplyfirstreal) /\ (ge_balance_negative_associate_third_multiplyfirstreal) = 0) \/ exists ge_signed_half_associate_third_multiplyfirstrealdecode. (((ge_representation_real_code_associate_third_multiplyfirst) = 2 * ge_signed_half_associate_third_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_associate_third_multiplyfirstreal) = 0) /\ (ge_balance_negative_associate_third_multiplyfirstreal) = S ge_signed_half_associate_third_multiplyfirstrealdecode))) /\ ((ge_first_rp_associate_third_multiply) + ge_balance_negative_associate_third_multiplyfirstreal = (ge_first_rn_associate_third_multiply) + ge_balance_positive_associate_third_multiplyfirstreal))) /\ (exists ge_balance_positive_associate_third_multiplyfirstimaginary ge_balance_negative_associate_third_multiplyfirstimaginary. (((((ge_representation_imaginary_code_associate_third_multiplyfirst) = 2 * (ge_balance_positive_associate_third_multiplyfirstimaginary) /\ (ge_balance_negative_associate_third_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_associate_third_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_associate_third_multiplyfirst) = 2 * ge_signed_half_associate_third_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_third_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_associate_third_multiplyfirstimaginary) = S ge_signed_half_associate_third_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_associate_third_multiply) + ge_balance_negative_associate_third_multiplyfirstimaginary = (ge_first_in_associate_third_multiply) + ge_balance_positive_associate_third_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_third_multiplysecond ge_representation_imaginary_code_associate_third_multiplysecond. (((c) = ((ge_representation_real_code_associate_third_multiplysecond) + (ge_representation_imaginary_code_associate_third_multiplysecond)) * S ((ge_representation_real_code_associate_third_multiplysecond) + (ge_representation_imaginary_code_associate_third_multiplysecond)) + ((ge_representation_imaginary_code_associate_third_multiplysecond) + (ge_representation_imaginary_code_associate_third_multiplysecond))) /\ ((exists ge_balance_positive_associate_third_multiplysecondreal ge_balance_negative_associate_third_multiplysecondreal. (((((ge_representation_real_code_associate_third_multiplysecond) = 2 * (ge_balance_positive_associate_third_multiplysecondreal) /\ (ge_balance_negative_associate_third_multiplysecondreal) = 0) \/ exists ge_signed_half_associate_third_multiplysecondrealdecode. (((ge_representation_real_code_associate_third_multiplysecond) = 2 * ge_signed_half_associate_third_multiplysecondrealdecode + 1 /\ (ge_balance_positive_associate_third_multiplysecondreal) = 0) /\ (ge_balance_negative_associate_third_multiplysecondreal) = S ge_signed_half_associate_third_multiplysecondrealdecode))) /\ ((ge_second_rp_associate_third_multiply) + ge_balance_negative_associate_third_multiplysecondreal = (ge_second_rn_associate_third_multiply) + ge_balance_positive_associate_third_multiplysecondreal))) /\ (exists ge_balance_positive_associate_third_multiplysecondimaginary ge_balance_negative_associate_third_multiplysecondimaginary. (((((ge_representation_imaginary_code_associate_third_multiplysecond) = 2 * (ge_balance_positive_associate_third_multiplysecondimaginary) /\ (ge_balance_negative_associate_third_multiplysecondimaginary) = 0) \/ exists ge_signed_half_associate_third_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_associate_third_multiplysecond) = 2 * ge_signed_half_associate_third_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_third_multiplysecondimaginary) = 0) /\ (ge_balance_negative_associate_third_multiplysecondimaginary) = S ge_signed_half_associate_third_multiplysecondimaginarydecode))) /\ ((ge_second_ip_associate_third_multiply) + ge_balance_negative_associate_third_multiplysecondimaginary = (ge_second_in_associate_third_multiply) + ge_balance_positive_associate_third_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_third_multiplyoutput ge_representation_imaginary_code_associate_third_multiplyoutput. (((bc) = ((ge_representation_real_code_associate_third_multiplyoutput) + (ge_representation_imaginary_code_associate_third_multiplyoutput)) * S ((ge_representation_real_code_associate_third_multiplyoutput) + (ge_representation_imaginary_code_associate_third_multiplyoutput)) + ((ge_representation_imaginary_code_associate_third_multiplyoutput) + (ge_representation_imaginary_code_associate_third_multiplyoutput))) /\ ((exists ge_balance_positive_associate_third_multiplyoutputreal ge_balance_negative_associate_third_multiplyoutputreal. (((((ge_representation_real_code_associate_third_multiplyoutput) = 2 * (ge_balance_positive_associate_third_multiplyoutputreal) /\ (ge_balance_negative_associate_third_multiplyoutputreal) = 0) \/ exists ge_signed_half_associate_third_multiplyoutputrealdecode. (((ge_representation_real_code_associate_third_multiplyoutput) = 2 * ge_signed_half_associate_third_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_associate_third_multiplyoutputreal) = 0) /\ (ge_balance_negative_associate_third_multiplyoutputreal) = S ge_signed_half_associate_third_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_associate_third_multiply) * (ge_second_rp_associate_third_multiply))) + (((ge_first_rn_associate_third_multiply) * (ge_second_rn_associate_third_multiply))))) + (((((ge_first_ip_associate_third_multiply) * (ge_second_in_associate_third_multiply))) + (((ge_first_in_associate_third_multiply) * (ge_second_ip_associate_third_multiply))))))) + ge_balance_negative_associate_third_multiplyoutputreal = (((((((ge_first_rp_associate_third_multiply) * (ge_second_rn_associate_third_multiply))) + (((ge_first_rn_associate_third_multiply) * (ge_second_rp_associate_third_multiply))))) + (((((ge_first_ip_associate_third_multiply) * (ge_second_ip_associate_third_multiply))) + (((ge_first_in_associate_third_multiply) * (ge_second_in_associate_third_multiply))))))) + ge_balance_positive_associate_third_multiplyoutputreal))) /\ (exists ge_balance_positive_associate_third_multiplyoutputimaginary ge_balance_negative_associate_third_multiplyoutputimaginary. (((((ge_representation_imaginary_code_associate_third_multiplyoutput) = 2 * (ge_balance_positive_associate_third_multiplyoutputimaginary) /\ (ge_balance_negative_associate_third_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_associate_third_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_associate_third_multiplyoutput) = 2 * ge_signed_half_associate_third_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_third_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_associate_third_multiplyoutputimaginary) = S ge_signed_half_associate_third_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_third_multiply) * (ge_second_ip_associate_third_multiply))) + (((ge_first_rn_associate_third_multiply) * (ge_second_in_associate_third_multiply))))) + (((((ge_first_ip_associate_third_multiply) * (ge_second_rp_associate_third_multiply))) + (((ge_first_in_associate_third_multiply) * (ge_second_rn_associate_third_multiply))))))) + ge_balance_negative_associate_third_multiplyoutputimaginary = (((((((ge_first_rp_associate_third_multiply) * (ge_second_in_associate_third_multiply))) + (((ge_first_rn_associate_third_multiply) * (ge_second_ip_associate_third_multiply))))) + (((((ge_first_ip_associate_third_multiply) * (ge_second_rn_associate_third_multiply))) + (((ge_first_in_associate_third_multiply) * (ge_second_rp_associate_third_multiply))))))) + ge_balance_positive_associate_third_multiplyoutputimaginary))))))))) -> (exists ge_first_rp_associate_output_multiply ge_first_rn_associate_output_multiply ge_first_ip_associate_output_multiply ge_first_in_associate_output_multiply ge_second_rp_associate_output_multiply ge_second_rn_associate_output_multiply ge_second_ip_associate_output_multiply ge_second_in_associate_output_multiply. ((exists ge_representation_real_code_associate_output_multiplyfirst ge_representation_imaginary_code_associate_output_multiplyfirst. (((a) = ((ge_representation_real_code_associate_output_multiplyfirst) + (ge_representation_imaginary_code_associate_output_multiplyfirst)) * S ((ge_representation_real_code_associate_output_multiplyfirst) + (ge_representation_imaginary_code_associate_output_multiplyfirst)) + ((ge_representation_imaginary_code_associate_output_multiplyfirst) + (ge_representation_imaginary_code_associate_output_multiplyfirst))) /\ ((exists ge_balance_positive_associate_output_multiplyfirstreal ge_balance_negative_associate_output_multiplyfirstreal. (((((ge_representation_real_code_associate_output_multiplyfirst) = 2 * (ge_balance_positive_associate_output_multiplyfirstreal) /\ (ge_balance_negative_associate_output_multiplyfirstreal) = 0) \/ exists ge_signed_half_associate_output_multiplyfirstrealdecode. (((ge_representation_real_code_associate_output_multiplyfirst) = 2 * ge_signed_half_associate_output_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_associate_output_multiplyfirstreal) = 0) /\ (ge_balance_negative_associate_output_multiplyfirstreal) = S ge_signed_half_associate_output_multiplyfirstrealdecode))) /\ ((ge_first_rp_associate_output_multiply) + ge_balance_negative_associate_output_multiplyfirstreal = (ge_first_rn_associate_output_multiply) + ge_balance_positive_associate_output_multiplyfirstreal))) /\ (exists ge_balance_positive_associate_output_multiplyfirstimaginary ge_balance_negative_associate_output_multiplyfirstimaginary. (((((ge_representation_imaginary_code_associate_output_multiplyfirst) = 2 * (ge_balance_positive_associate_output_multiplyfirstimaginary) /\ (ge_balance_negative_associate_output_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_associate_output_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_associate_output_multiplyfirst) = 2 * ge_signed_half_associate_output_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_output_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_associate_output_multiplyfirstimaginary) = S ge_signed_half_associate_output_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_associate_output_multiply) + ge_balance_negative_associate_output_multiplyfirstimaginary = (ge_first_in_associate_output_multiply) + ge_balance_positive_associate_output_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_output_multiplysecond ge_representation_imaginary_code_associate_output_multiplysecond. (((bc) = ((ge_representation_real_code_associate_output_multiplysecond) + (ge_representation_imaginary_code_associate_output_multiplysecond)) * S ((ge_representation_real_code_associate_output_multiplysecond) + (ge_representation_imaginary_code_associate_output_multiplysecond)) + ((ge_representation_imaginary_code_associate_output_multiplysecond) + (ge_representation_imaginary_code_associate_output_multiplysecond))) /\ ((exists ge_balance_positive_associate_output_multiplysecondreal ge_balance_negative_associate_output_multiplysecondreal. (((((ge_representation_real_code_associate_output_multiplysecond) = 2 * (ge_balance_positive_associate_output_multiplysecondreal) /\ (ge_balance_negative_associate_output_multiplysecondreal) = 0) \/ exists ge_signed_half_associate_output_multiplysecondrealdecode. (((ge_representation_real_code_associate_output_multiplysecond) = 2 * ge_signed_half_associate_output_multiplysecondrealdecode + 1 /\ (ge_balance_positive_associate_output_multiplysecondreal) = 0) /\ (ge_balance_negative_associate_output_multiplysecondreal) = S ge_signed_half_associate_output_multiplysecondrealdecode))) /\ ((ge_second_rp_associate_output_multiply) + ge_balance_negative_associate_output_multiplysecondreal = (ge_second_rn_associate_output_multiply) + ge_balance_positive_associate_output_multiplysecondreal))) /\ (exists ge_balance_positive_associate_output_multiplysecondimaginary ge_balance_negative_associate_output_multiplysecondimaginary. (((((ge_representation_imaginary_code_associate_output_multiplysecond) = 2 * (ge_balance_positive_associate_output_multiplysecondimaginary) /\ (ge_balance_negative_associate_output_multiplysecondimaginary) = 0) \/ exists ge_signed_half_associate_output_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_associate_output_multiplysecond) = 2 * ge_signed_half_associate_output_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_output_multiplysecondimaginary) = 0) /\ (ge_balance_negative_associate_output_multiplysecondimaginary) = S ge_signed_half_associate_output_multiplysecondimaginarydecode))) /\ ((ge_second_ip_associate_output_multiply) + ge_balance_negative_associate_output_multiplysecondimaginary = (ge_second_in_associate_output_multiply) + ge_balance_positive_associate_output_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_output_multiplyoutput ge_representation_imaginary_code_associate_output_multiplyoutput. (((t) = ((ge_representation_real_code_associate_output_multiplyoutput) + (ge_representation_imaginary_code_associate_output_multiplyoutput)) * S ((ge_representation_real_code_associate_output_multiplyoutput) + (ge_representation_imaginary_code_associate_output_multiplyoutput)) + ((ge_representation_imaginary_code_associate_output_multiplyoutput) + (ge_representation_imaginary_code_associate_output_multiplyoutput))) /\ ((exists ge_balance_positive_associate_output_multiplyoutputreal ge_balance_negative_associate_output_multiplyoutputreal. (((((ge_representation_real_code_associate_output_multiplyoutput) = 2 * (ge_balance_positive_associate_output_multiplyoutputreal) /\ (ge_balance_negative_associate_output_multiplyoutputreal) = 0) \/ exists ge_signed_half_associate_output_multiplyoutputrealdecode. (((ge_representation_real_code_associate_output_multiplyoutput) = 2 * ge_signed_half_associate_output_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_associate_output_multiplyoutputreal) = 0) /\ (ge_balance_negative_associate_output_multiplyoutputreal) = S ge_signed_half_associate_output_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_associate_output_multiply) * (ge_second_rp_associate_output_multiply))) + (((ge_first_rn_associate_output_multiply) * (ge_second_rn_associate_output_multiply))))) + (((((ge_first_ip_associate_output_multiply) * (ge_second_in_associate_output_multiply))) + (((ge_first_in_associate_output_multiply) * (ge_second_ip_associate_output_multiply))))))) + ge_balance_negative_associate_output_multiplyoutputreal = (((((((ge_first_rp_associate_output_multiply) * (ge_second_rn_associate_output_multiply))) + (((ge_first_rn_associate_output_multiply) * (ge_second_rp_associate_output_multiply))))) + (((((ge_first_ip_associate_output_multiply) * (ge_second_ip_associate_output_multiply))) + (((ge_first_in_associate_output_multiply) * (ge_second_in_associate_output_multiply))))))) + ge_balance_positive_associate_output_multiplyoutputreal))) /\ (exists ge_balance_positive_associate_output_multiplyoutputimaginary ge_balance_negative_associate_output_multiplyoutputimaginary. (((((ge_representation_imaginary_code_associate_output_multiplyoutput) = 2 * (ge_balance_positive_associate_output_multiplyoutputimaginary) /\ (ge_balance_negative_associate_output_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_associate_output_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_associate_output_multiplyoutput) = 2 * ge_signed_half_associate_output_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_output_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_associate_output_multiplyoutputimaginary) = S ge_signed_half_associate_output_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_output_multiply) * (ge_second_ip_associate_output_multiply))) + (((ge_first_rn_associate_output_multiply) * (ge_second_in_associate_output_multiply))))) + (((((ge_first_ip_associate_output_multiply) * (ge_second_rp_associate_output_multiply))) + (((ge_first_in_associate_output_multiply) * (ge_second_rn_associate_output_multiply))))))) + ge_balance_negative_associate_output_multiplyoutputimaginary = (((((((ge_first_rp_associate_output_multiply) * (ge_second_in_associate_output_multiply))) + (((ge_first_rn_associate_output_multiply) * (ge_second_ip_associate_output_multiply))))) + (((((ge_first_ip_associate_output_multiply) * (ge_second_rn_associate_output_multiply))) + (((ge_first_in_associate_output_multiply) * (ge_second_rp_associate_output_multiply))))))) + ge_balance_positive_associate_output_multiplyoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

131 script commands · 17 reading checkpoints · 6 local claims

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

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

Named ingredients (3)
gaussian valid has representationgaussian multiply input left validgaussian multiply input right valid
01Fix variables and assumptionsL1–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro ab
  5. L5
    intro bc
  6. L6
    intro t
  7. L7
    intro hAB
  8. L8
    intro hABC
  9. L9
    intro hBC
02Establish hAL10–17

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

  1. L10
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep(a,rp,rn,ip,inn)Original native command in the exact edition
  2. L11
    specialize gaussian_valid_has_representation (a)
  3. L12
    apply gaussian_valid_has_representation
  4. L13
    specialize gaussian_multiply_input_left_valid (a)
  5. L14
    specialize gaussian_multiply_input_left_valid (b)
  6. L15
    specialize gaussian_multiply_input_left_valid (ab)
  7. L16
    apply gaussian_multiply_input_left_valid
  8. L17
    exact hAB
03Separate the logical casesL18–21

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

  1. L18
    cases hA
  2. L19
    cases hA_witness
  3. L20
    cases hA_witness_witness
  4. L21
    cases hA_witness_witness_witness
04Establish hBL22–29

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

  1. L22
    have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)Definitions: ZPairRep(b,rp,rn,ip,inn)Original native command in the exact edition
  2. L23
    specialize gaussian_valid_has_representation (b)
  3. L24
    apply gaussian_valid_has_representation
  4. L25
    specialize gaussian_multiply_input_right_valid (a)
  5. L26
    specialize gaussian_multiply_input_right_valid (b)
  6. L27
    specialize gaussian_multiply_input_right_valid (ab)
  7. L28
    apply gaussian_multiply_input_right_valid
  8. L29
    exact hAB
05Separate the logical casesL30–33

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

  1. L30
    cases hB
  2. L31
    cases hB_witness
  3. L32
    cases hB_witness_witness
  4. L33
    cases hB_witness_witness_witness
06Establish hCL34–41

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

  1. L34
    have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)Definitions: ZPairRep(c,rp,rn,ip,inn)Original native command in the exact edition
  2. L35
    specialize gaussian_valid_has_representation (c)
  3. L36
    apply gaussian_valid_has_representation
  4. L37
    specialize gaussian_multiply_input_right_valid (ab)
  5. L38
    specialize gaussian_multiply_input_right_valid (c)
  6. L39
    specialize gaussian_multiply_input_right_valid (t)
  7. L40
    apply gaussian_multiply_input_right_valid
  8. L41
    exact hABC
07Separate the logical casesL42–45

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

  1. L42
    cases hC
  2. L43
    cases hC_witness
  3. L44
    cases hC_witness_witness
  4. L45
    cases hC_witness_witness_witness
08Establish habL46–55

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

  1. L46
    have hab : ZPairRep(ab,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))Definitions: ZPairRep(ab,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))Original native command in the exact edition
  2. L47
    specialize gaussian_multiply_for_representations (a)
  3. L48
    specialize gaussian_multiply_for_representations (b)
  4. L49
    specialize gaussian_multiply_for_representations (ab)
  5. L50
    specialize gaussian_multiply_for_representations (x)
  6. L51
    specialize gaussian_multiply_for_representations (x1)
  7. L52
    specialize gaussian_multiply_for_representations (x2)
  8. L53
    specialize gaussian_multiply_for_representations (x3)
  9. L54
    specialize gaussian_multiply_for_representations (x4)
  10. L55
    specialize gaussian_multiply_for_representations (x5)
09Use earlier factsL56–61

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

  1. L56
    specialize gaussian_multiply_for_representations (x6)
  2. L57
    specialize gaussian_multiply_for_representations (x7)
  3. L58
    apply gaussian_multiply_for_representations
  4. L59
    exact hA_witness_witness_witness_witness
  5. L60
    exact hB_witness_witness_witness_witness
  6. L61
    exact hAB
10Establish hbcL62–71

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

  1. L62
    have hbc : ZPairRep(bc,x4 · x8 + x5 · x9 + (x6 · x11 + x7 · x10),x4 · x9 + x5 · x8 + (x6 · x10 + x7 · x11),x4 · x10 + x5 · x11 + (x6 · x8 + x7 · x9),x4 · x11 + x5 · x10 + (x6 · x9 + x7 · x8))Definitions: ZPairRep(bc,x4 · x8 + x5 · x9 + (x6 · x11 + x7 · x10),x4 · x9 + x5 · x8 + (x6 · x10 + x7 · x11),x4 · x10 + x5 · x11 + (x6 · x8 + x7 · x9),x4 · x11 + x5 · x10 + (x6 · x9 + x7 · x8))Original native command in the exact edition
  2. L63
    specialize gaussian_multiply_for_representations (b)
  3. L64
    specialize gaussian_multiply_for_representations (c)
  4. L65
    specialize gaussian_multiply_for_representations (bc)
  5. L66
    specialize gaussian_multiply_for_representations (x4)
  6. L67
    specialize gaussian_multiply_for_representations (x5)
  7. L68
    specialize gaussian_multiply_for_representations (x6)
  8. L69
    specialize gaussian_multiply_for_representations (x7)
  9. L70
    specialize gaussian_multiply_for_representations (x8)
  10. L71
    specialize gaussian_multiply_for_representations (x9)
11Use earlier factsL72–77

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

  1. L72
    specialize gaussian_multiply_for_representations (x10)
  2. L73
    specialize gaussian_multiply_for_representations (x11)
  3. L74
    apply gaussian_multiply_for_representations
  4. L75
    exact hB_witness_witness_witness_witness
  5. L76
    exact hC_witness_witness_witness_witness
  6. L77
    exact hBC
12Establish htL78–87

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

  1. L78
    have ht · expand full local formula (797 characters)have ht : ZPairRep(t,(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x8 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x9 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x11 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x10),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x9 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x8 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x10 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x11),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x10 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x11 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x8 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x9),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x11 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x10 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x9 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x8))
    Definitions: ZPairRep(t,(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x8 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x9 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x11 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x10),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x9 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x8 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x10 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x11),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x10 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x11 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x8 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x9),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x11 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x10 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x9 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x8))Original native command in the exact edition
  2. L79
    specialize gaussian_multiply_for_representations (ab)
  3. L80
    specialize gaussian_multiply_for_representations (c)
  4. L81
    specialize gaussian_multiply_for_representations (t)
  5. L82
    specialize gaussian_multiply_for_representations (((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6)))))))
  6. L83
    specialize gaussian_multiply_for_representations (((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7)))))))
  7. L84
    specialize gaussian_multiply_for_representations (((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5)))))))
  8. L85
    specialize gaussian_multiply_for_representations (((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4)))))))
  9. L86
    specialize gaussian_multiply_for_representations (x8)
  10. L87
    specialize gaussian_multiply_for_representations (x9)
13Use earlier factsL88–97

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

  1. L88
    specialize gaussian_multiply_for_representations (x10)
  2. L89
    specialize gaussian_multiply_for_representations (x11)
  3. L90
    apply gaussian_multiply_for_representations
  4. L91
    exact hab
  5. L92
    exact hC_witness_witness_witness_witness
  6. L93
    exact hABC
  7. L94
    specialize gaussian_multiply_of_representations (a)
  8. L95
    specialize gaussian_multiply_of_representations (bc)
  9. L96
    specialize gaussian_multiply_of_representations (t)
  10. L97
    specialize gaussian_multiply_of_representations (x)
14Use earlier factsL98–107

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

  1. L98
    specialize gaussian_multiply_of_representations (x1)
  2. L99
    specialize gaussian_multiply_of_representations (x2)
  3. L100
    specialize gaussian_multiply_of_representations (x3)
  4. L101
    specialize gaussian_multiply_of_representations (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10)))))))
  5. L102
    specialize gaussian_multiply_of_representations (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11)))))))
  6. L103
    specialize gaussian_multiply_of_representations (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9)))))))
  7. L104
    specialize gaussian_multiply_of_representations (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8)))))))
  8. L105
    apply gaussian_multiply_of_representations
  9. L106
    exact hA_witness_witness_witness_witness
  10. L107
    exact hbc
15Use earlier factsL108–117

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

  1. L108
    specialize gaussian_representation_integer_transport (t)
  2. L109
    specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x8))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x9))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x11))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x10)))))))
  3. L110
    specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x9))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x8))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x10))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x11)))))))
  4. L111
    specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x10))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x11))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x8))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x9)))))))
  5. L112
    specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x11))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x10))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x9))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x8)))))))
  6. L113
    specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))) + (((x1) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))))) + (((((x2) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))) + (((x3) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9)))))))))))))
  7. L114
    specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))) + (((x1) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))))) + (((((x2) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))) + (((x3) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8)))))))))))))
  8. L115
    specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))) + (((x1) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))))) + (((((x2) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))) + (((x3) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11)))))))))))))
  9. L116
    specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))) + (((x1) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))))) + (((((x2) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))) + (((x3) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10)))))))))))))
  10. L117
    apply gaussian_representation_integer_transport
16Use earlier factsL118–127

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

  1. L118
    specialize gaussian_product_associate (x)
  2. L119
    specialize gaussian_product_associate (x1)
  3. L120
    specialize gaussian_product_associate (x2)
  4. L121
    specialize gaussian_product_associate (x3)
  5. L122
    specialize gaussian_product_associate (x4)
  6. L123
    specialize gaussian_product_associate (x5)
  7. L124
    specialize gaussian_product_associate (x6)
  8. L125
    specialize gaussian_product_associate (x7)
  9. L126
    specialize gaussian_product_associate (x8)
  10. L127
    specialize gaussian_product_associate (x9)
17Use earlier factsL128–131

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

  1. L128
    specialize gaussian_product_associate (x10)
  2. L129
    specialize gaussian_product_associate (x11)
  3. L130
    apply gaussian_product_associate
  4. L131
    exact ht

Library-wide reading audit

Original defined command ledger · 131 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro ab
  5. 0005intro bc
  6. 0006intro t
  7. 0007intro hAB
  8. 0008intro hABC
  9. 0009intro hBC
  10. 0010have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  11. 0011specialize gaussian_valid_has_representation (a)
  12. 0012apply gaussian_valid_has_representation
  13. 0013specialize gaussian_multiply_input_left_valid (a)
  14. 0014specialize gaussian_multiply_input_left_valid (b)
  15. 0015specialize gaussian_multiply_input_left_valid (ab)
  16. 0016apply gaussian_multiply_input_left_valid
  17. 0017exact hAB
  18. 0018cases hA
  19. 0019cases hA_witness
  20. 0020cases hA_witness_witness
  21. 0021cases hA_witness_witness_witness
  22. 0022have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)
  23. 0023specialize gaussian_valid_has_representation (b)
  24. 0024apply gaussian_valid_has_representation
  25. 0025specialize gaussian_multiply_input_right_valid (a)
  26. 0026specialize gaussian_multiply_input_right_valid (b)
  27. 0027specialize gaussian_multiply_input_right_valid (ab)
  28. 0028apply gaussian_multiply_input_right_valid
  29. 0029exact hAB
  30. 0030cases hB
  31. 0031cases hB_witness
  32. 0032cases hB_witness_witness
  33. 0033cases hB_witness_witness_witness
  34. 0034have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)
  35. 0035specialize gaussian_valid_has_representation (c)
  36. 0036apply gaussian_valid_has_representation
  37. 0037specialize gaussian_multiply_input_right_valid (ab)
  38. 0038specialize gaussian_multiply_input_right_valid (c)
  39. 0039specialize gaussian_multiply_input_right_valid (t)
  40. 0040apply gaussian_multiply_input_right_valid
  41. 0041exact hABC
  42. 0042cases hC
  43. 0043cases hC_witness
  44. 0044cases hC_witness_witness
  45. 0045cases hC_witness_witness_witness
  46. 0046have hab : ZPairRep(ab,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))
  47. 0047specialize gaussian_multiply_for_representations (a)
  48. 0048specialize gaussian_multiply_for_representations (b)
  49. 0049specialize gaussian_multiply_for_representations (ab)
  50. 0050specialize gaussian_multiply_for_representations (x)
  51. 0051specialize gaussian_multiply_for_representations (x1)
  52. 0052specialize gaussian_multiply_for_representations (x2)
  53. 0053specialize gaussian_multiply_for_representations (x3)
  54. 0054specialize gaussian_multiply_for_representations (x4)
  55. 0055specialize gaussian_multiply_for_representations (x5)
  56. 0056specialize gaussian_multiply_for_representations (x6)
  57. 0057specialize gaussian_multiply_for_representations (x7)
  58. 0058apply gaussian_multiply_for_representations
  59. 0059exact hA_witness_witness_witness_witness
  60. 0060exact hB_witness_witness_witness_witness
  61. 0061exact hAB
  62. 0062have hbc : ZPairRep(bc,x4 · x8 + x5 · x9 + (x6 · x11 + x7 · x10),x4 · x9 + x5 · x8 + (x6 · x10 + x7 · x11),x4 · x10 + x5 · x11 + (x6 · x8 + x7 · x9),x4 · x11 + x5 · x10 + (x6 · x9 + x7 · x8))
  63. 0063specialize gaussian_multiply_for_representations (b)
  64. 0064specialize gaussian_multiply_for_representations (c)
  65. 0065specialize gaussian_multiply_for_representations (bc)
  66. 0066specialize gaussian_multiply_for_representations (x4)
  67. 0067specialize gaussian_multiply_for_representations (x5)
  68. 0068specialize gaussian_multiply_for_representations (x6)
  69. 0069specialize gaussian_multiply_for_representations (x7)
  70. 0070specialize gaussian_multiply_for_representations (x8)
  71. 0071specialize gaussian_multiply_for_representations (x9)
  72. 0072specialize gaussian_multiply_for_representations (x10)
  73. 0073specialize gaussian_multiply_for_representations (x11)
  74. 0074apply gaussian_multiply_for_representations
  75. 0075exact hB_witness_witness_witness_witness
  76. 0076exact hC_witness_witness_witness_witness
  77. 0077exact hBC
  78. 0078have ht : ZPairRep(t,(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x8 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x9 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x11 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x10),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x9 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x8 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x10 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x11),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x10 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x11 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x8 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x9),(x · x4 + x1 · x5 + (x2 · x7 + x3 · x6)) · x11 + (x · x5 + x1 · x4 + (x2 · x6 + x3 · x7)) · x10 + ((x · x6 + x1 · x7 + (x2 · x4 + x3 · x5)) · x9 + (x · x7 + x1 · x6 + (x2 · x5 + x3 · x4)) · x8))
  79. 0079specialize gaussian_multiply_for_representations (ab)
  80. 0080specialize gaussian_multiply_for_representations (c)
  81. 0081specialize gaussian_multiply_for_representations (t)
  82. 0082specialize gaussian_multiply_for_representations (((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6)))))))
  83. 0083specialize gaussian_multiply_for_representations (((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7)))))))
  84. 0084specialize gaussian_multiply_for_representations (((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5)))))))
  85. 0085specialize gaussian_multiply_for_representations (((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4)))))))
  86. 0086specialize gaussian_multiply_for_representations (x8)
  87. 0087specialize gaussian_multiply_for_representations (x9)
  88. 0088specialize gaussian_multiply_for_representations (x10)
  89. 0089specialize gaussian_multiply_for_representations (x11)
  90. 0090apply gaussian_multiply_for_representations
  91. 0091exact hab
  92. 0092exact hC_witness_witness_witness_witness
  93. 0093exact hABC
  94. 0094specialize gaussian_multiply_of_representations (a)
  95. 0095specialize gaussian_multiply_of_representations (bc)
  96. 0096specialize gaussian_multiply_of_representations (t)
  97. 0097specialize gaussian_multiply_of_representations (x)
  98. 0098specialize gaussian_multiply_of_representations (x1)
  99. 0099specialize gaussian_multiply_of_representations (x2)
  100. 0100specialize gaussian_multiply_of_representations (x3)
  101. 0101specialize gaussian_multiply_of_representations (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10)))))))
  102. 0102specialize gaussian_multiply_of_representations (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11)))))))
  103. 0103specialize gaussian_multiply_of_representations (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9)))))))
  104. 0104specialize gaussian_multiply_of_representations (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8)))))))
  105. 0105apply gaussian_multiply_of_representations
  106. 0106exact hA_witness_witness_witness_witness
  107. 0107exact hbc
  108. 0108specialize gaussian_representation_integer_transport (t)
  109. 0109specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x8))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x9))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x11))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x10)))))))
  110. 0110specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x9))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x8))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x10))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x11)))))))
  111. 0111specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x10))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x11))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x8))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x9)))))))
  112. 0112specialize gaussian_representation_integer_transport (((((((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) * (x11))) + (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) * (x10))))) + (((((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) * (x9))) + (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) * (x8)))))))
  113. 0113specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))) + (((x1) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))))) + (((((x2) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))) + (((x3) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9)))))))))))))
  114. 0114specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))) + (((x1) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))))) + (((((x2) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))) + (((x3) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8)))))))))))))
  115. 0115specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))) + (((x1) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))))) + (((((x2) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10))))))))) + (((x3) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11)))))))))))))
  116. 0116specialize gaussian_representation_integer_transport (((((((x) * (((((((x4) * (x11))) + (((x5) * (x10))))) + (((((x6) * (x9))) + (((x7) * (x8))))))))) + (((x1) * (((((((x4) * (x10))) + (((x5) * (x11))))) + (((((x6) * (x8))) + (((x7) * (x9))))))))))) + (((((x2) * (((((((x4) * (x9))) + (((x5) * (x8))))) + (((((x6) * (x10))) + (((x7) * (x11))))))))) + (((x3) * (((((((x4) * (x8))) + (((x5) * (x9))))) + (((((x6) * (x11))) + (((x7) * (x10)))))))))))))
  117. 0117apply gaussian_representation_integer_transport
  118. 0118specialize gaussian_product_associate (x)
  119. 0119specialize gaussian_product_associate (x1)
  120. 0120specialize gaussian_product_associate (x2)
  121. 0121specialize gaussian_product_associate (x3)
  122. 0122specialize gaussian_product_associate (x4)
  123. 0123specialize gaussian_product_associate (x5)
  124. 0124specialize gaussian_product_associate (x6)
  125. 0125specialize gaussian_product_associate (x7)
  126. 0126specialize gaussian_product_associate (x8)
  127. 0127specialize gaussian_product_associate (x9)
  128. 0128specialize gaussian_product_associate (x10)
  129. 0129specialize gaussian_product_associate (x11)
  130. 0130apply gaussian_product_associate
  131. 0131exact ht