Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ k. ∀ z. ∀ N. Le(N,k) → GNorm(z,N) → ¬z = 0 → ¬GUnit(z) → ∃ x. GIrreducible(x) ∧ GDvd(x,z)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
le_zero · checked external prerequisitegaussian_norm_value_transportgaussian_norm_zero_implies_code_zerogaussian_irreducible_or_strict_nonunit_factorizationgaussian_divides_reflexivegaussian_norm_input_validle_of_succ_le_succ · checked external prerequisitelt_of_lt_of_le · checked external prerequisitegaussian_search_divisor_of_nonzero_nonzerogaussian_divides_transitive
Original expanded first-order statement
forall k z N. (exists ge_gap_prime_divisor_bound. ge_gap_prime_divisor_bound + (N) = (k)) -> (exists ge_norm_rp_prime_divisor_norm ge_norm_rn_prime_divisor_norm ge_norm_ip_prime_divisor_norm ge_norm_in_prime_divisor_norm. ((exists ge_representation_real_code_prime_divisor_normrepresentation ge_representation_imaginary_code_prime_divisor_normrepresentation. (((z) = ((ge_representation_real_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation)) * S ((ge_representation_real_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation)) + ((ge_representation_imaginary_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation))) /\ ((exists ge_balance_positive_prime_divisor_normrepresentationreal ge_balance_negative_prime_divisor_normrepresentationreal. (((((ge_representation_real_code_prime_divisor_normrepresentation) = 2 * (ge_balance_positive_prime_divisor_normrepresentationreal) /\ (ge_balance_negative_prime_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_prime_divisor_normrepresentationrealdecode. (((ge_representation_real_code_prime_divisor_normrepresentation) = 2 * ge_signed_half_prime_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_prime_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_prime_divisor_normrepresentationreal) = S ge_signed_half_prime_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_prime_divisor_norm) + ge_balance_negative_prime_divisor_normrepresentationreal = (ge_norm_rn_prime_divisor_norm) + ge_balance_positive_prime_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_prime_divisor_normrepresentationimaginary ge_balance_negative_prime_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_prime_divisor_normrepresentation) = 2 * (ge_balance_positive_prime_divisor_normrepresentationimaginary) /\ (ge_balance_negative_prime_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_prime_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_normrepresentation) = 2 * ge_signed_half_prime_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_prime_divisor_normrepresentationimaginary) = S ge_signed_half_prime_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_prime_divisor_norm) + ge_balance_negative_prime_divisor_normrepresentationimaginary = (ge_norm_in_prime_divisor_norm) + ge_balance_positive_prime_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_prime_divisor_normsquare ge_imaginary_square_prime_divisor_normsquare. ((((((ge_norm_rp_prime_divisor_norm) * (ge_norm_rp_prime_divisor_norm))) + (((ge_norm_rn_prime_divisor_norm) * (ge_norm_rn_prime_divisor_norm)))) = ((ge_real_square_prime_divisor_normsquare) + (((((ge_norm_rp_prime_divisor_norm) * (ge_norm_rn_prime_divisor_norm))) + (((ge_norm_rn_prime_divisor_norm) * (ge_norm_rp_prime_divisor_norm))))))) /\ ((((((ge_norm_ip_prime_divisor_norm) * (ge_norm_ip_prime_divisor_norm))) + (((ge_norm_in_prime_divisor_norm) * (ge_norm_in_prime_divisor_norm)))) = ((ge_imaginary_square_prime_divisor_normsquare) + (((((ge_norm_ip_prime_divisor_norm) * (ge_norm_in_prime_divisor_norm))) + (((ge_norm_in_prime_divisor_norm) * (ge_norm_ip_prime_divisor_norm))))))) /\ ((N) = ge_real_square_prime_divisor_normsquare + ge_imaginary_square_prime_divisor_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_prime_divisor_nonunit. (exists ge_first_rp_prime_divisor_nonunitidentity ge_first_rn_prime_divisor_nonunitidentity ge_first_ip_prime_divisor_nonunitidentity ge_first_in_prime_divisor_nonunitidentity ge_second_rp_prime_divisor_nonunitidentity ge_second_rn_prime_divisor_nonunitidentity ge_second_ip_prime_divisor_nonunitidentity ge_second_in_prime_divisor_nonunitidentity. ((exists ge_representation_real_code_prime_divisor_nonunitidentityfirst ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst. (((z) = ((ge_representation_real_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentityfirstreal ge_balance_negative_prime_divisor_nonunitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstreal) = S ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentityfirstreal = (ge_first_rn_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary) = S ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary = (ge_first_in_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_nonunitidentitysecond ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond. (((gr_inverse_prime_divisor_nonunit) = ((ge_representation_real_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentitysecondreal ge_balance_negative_prime_divisor_nonunitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_nonunitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondreal) = S ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentitysecondreal = (ge_second_rn_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary) = S ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary = (ge_second_in_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_nonunitidentityoutput ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentityoutputreal ge_balance_negative_prime_divisor_nonunitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputreal) = S ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))))))) + ge_balance_negative_prime_divisor_nonunitidentityoutputreal = (((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))))))) + ge_balance_positive_prime_divisor_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary) = S ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))))))) + ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))))))) + ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary)))))))))) -> (exists p. ((((exists ge_real_positive_prime_divisor_resultirreduciblecarrier ge_real_negative_prime_divisor_resultirreduciblecarrier ge_imaginary_positive_prime_divisor_resultirreduciblecarrier ge_imaginary_negative_prime_divisor_resultirreduciblecarrier. (exists ge_real_code_prime_divisor_resultirreduciblecarrierdecode ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode. (((p) = ((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode)) * S ((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode)) + ((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode))) /\ (((((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * (ge_real_positive_prime_divisor_resultirreduciblecarrier) /\ (ge_real_negative_prime_divisor_resultirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real. (((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_prime_divisor_resultirreduciblecarrier) = 0) /\ (ge_real_negative_prime_divisor_resultirreduciblecarrier) = S ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_prime_divisor_resultirreduciblecarrier) /\ (ge_imaginary_negative_prime_divisor_resultirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_divisor_resultirreduciblecarrier) = 0) /\ (ge_imaginary_negative_prime_divisor_resultirreduciblecarrier) = S ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_divisor_resultirreduciblenonunit. (exists ge_first_rp_prime_divisor_resultirreduciblenonunitidentity ge_first_rn_prime_divisor_resultirreduciblenonunitidentity ge_first_ip_prime_divisor_resultirreduciblenonunitidentity ge_first_in_prime_divisor_resultirreduciblenonunitidentity ge_second_rp_prime_divisor_resultirreduciblenonunitidentity ge_second_rn_prime_divisor_resultirreduciblenonunitidentity ge_second_ip_prime_divisor_resultirreduciblenonunitidentity ge_second_in_prime_divisor_resultirreduciblenonunitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblenonunit) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_divisor_resultirreducible gr_second_factor_prime_divisor_resultirreducible. (exists ge_first_rp_prime_divisor_resultirreduciblefactorization ge_first_rn_prime_divisor_resultirreduciblefactorization ge_first_ip_prime_divisor_resultirreduciblefactorization ge_first_in_prime_divisor_resultirreduciblefactorization ge_second_rp_prime_divisor_resultirreduciblefactorization ge_second_rn_prime_divisor_resultirreduciblefactorization ge_second_ip_prime_divisor_resultirreduciblefactorization ge_second_in_prime_divisor_resultirreduciblefactorization. ((exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst. (((gr_first_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal = (ge_first_rn_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond. (((gr_second_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal = (ge_second_rn_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary = (ge_second_in_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput. (((p) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_prime_divisor_resultirreduciblefirst_unit. (exists ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst. (((gr_first_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblefirst_unit) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_prime_divisor_resultirreduciblesecond_unit. (exists ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst. (((gr_second_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblesecond_unit) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary))))))))))))))) /\ (exists gr_quotient_prime_divisor_resultdivisor. (exists ge_first_rp_prime_divisor_resultdivisorproduct ge_first_rn_prime_divisor_resultdivisorproduct ge_first_ip_prime_divisor_resultdivisorproduct ge_first_in_prime_divisor_resultdivisorproduct ge_second_rp_prime_divisor_resultdivisorproduct ge_second_rn_prime_divisor_resultdivisorproduct ge_second_ip_prime_divisor_resultdivisorproduct ge_second_in_prime_divisor_resultdivisorproduct. ((exists ge_representation_real_code_prime_divisor_resultdivisorproductfirst ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst. (((p) = ((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductfirstreal ge_balance_negative_prime_divisor_resultdivisorproductfirstreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductfirstreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) = 2 * ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstreal) = S ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductfirstreal = (ge_first_rn_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) = 2 * ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary = (ge_first_in_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultdivisorproductsecond ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond. (((gr_quotient_prime_divisor_resultdivisor) = ((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductsecondreal ge_balance_negative_prime_divisor_resultdivisorproductsecondreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductsecondreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) = 2 * ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondreal) = S ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductsecondreal = (ge_second_rn_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) = 2 * ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary = (ge_second_in_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultdivisorproductoutput ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput. (((z) = ((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductoutputreal ge_balance_negative_prime_divisor_resultdivisorproductoutputreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductoutputreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) = 2 * ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputreal) = S ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))))))) + ge_balance_negative_prime_divisor_resultdivisorproductoutputreal = (((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))))))) + ge_balance_positive_prime_divisor_resultdivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) = 2 * ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))))))) + ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary = (((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))))))) + ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary))))))))))))Complete tactic proof in conservative notation
All 87 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
87 script commands · 23 reading checkpoints · 2 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 (7)
01Induction on kL1–7
02Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
exfalso
03Use earlier factsL9–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
apply hz - L10
specialize gaussian_norm_zero_implies_code_zero (z) - L11
apply gaussian_norm_zero_implies_code_zero - L12
specialize gaussian_norm_value_transport (z) - L13
specialize gaussian_norm_value_transport (N) - L14
specialize gaussian_norm_value_transport (0) - L15
apply gaussian_norm_value_transport - L16
specialize le_zero (N) - L17
apply le_zero - L18
exact hb
04Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
exact hn
05Fix variables and assumptionsL20–25
06Establish hsL26–32
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian irreducible or strict nonunit factorization.
- L26
have hs : GIrreducible(z) ∨ (∃ x. ∃ y. ∃ n. ∃ m. GStrictNonunitFactorization(z,N,x,y,n,m))Definitions: GIrreducible(z)GStrictNonunitFactorization(z,N,x,y,n,m)Original native command in the exact edition - L27
specialize gaussian_irreducible_or_strict_nonunit_factorization (z) - L28
specialize gaussian_irreducible_or_strict_nonunit_factorization (N) - L29
apply gaussian_irreducible_or_strict_nonunit_factorization - L30
exact hn - L31
exact hz - L32
exact hu
07Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
cases hs
08Construct an explicit witnessL34–34
Supply the displayed value, then prove that it has the required property.
- L34
exists (z)
09Separate the logical casesL35–35
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L35
split
10Use earlier factsL36–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
11Separate the logical casesL43–52
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L43
cases hs_right - L44
cases hs_right_witness - L45
cases hs_right_witness_witness - L46
cases hs_right_witness_witness_witness - L47
cases hs_right_witness_witness_witness_witness - L48
cases hs_right_witness_witness_witness_witness_right - L49
cases hs_right_witness_witness_witness_witness_right_right - L50
cases hs_right_witness_witness_witness_witness_right_right_right - L51
cases hs_right_witness_witness_witness_witness_right_right_right_right - L52
cases hs_right_witness_witness_witness_witness_right_right_right_right_right
12Establish hrecL53–62
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L53
have hrec : ∃ p. GIrreducible(p) ∧ GDvd(p,x)Definitions: GIrreducible(p)GDvd(p,x)Original native command in the exact edition - L54
specialize IH (x) - L55
specialize IH (x2) - L56
apply IH - L57
specialize le_of_succ_le_succ (x2) - L58
specialize le_of_succ_le_succ (k) - L59
apply le_of_succ_le_succ - L60
specialize lt_of_lt_of_le (x2) - L61
specialize lt_of_lt_of_le (N) - L62
specialize lt_of_lt_of_le (S k)
13Use earlier factsL63–66
14Fix variables and assumptionsL67–67
Work with arbitrary variables or the premises of the current implication.
- L67
intro hzero
15Use earlier factsL68–70
16Construct an explicit witnessL71–71
Supply the displayed value, then prove that it has the required property.
- L71
exists (x1)
17Use earlier factsL72–75
18Separate the logical casesL76–77
19Construct an explicit witnessL78–78
Supply the displayed value, then prove that it has the required property.
- L78
exists (x4)
20Separate the logical casesL79–79
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L79
split
21Use earlier factsL80–85
Instantiate or apply named facts and discharge the corresponding proof obligations.
22Construct an explicit witnessL86–86
Supply the displayed value, then prove that it has the required property.
- L86
exists (x1)
23Use earlier factsL87–87
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L87
exact hs_right_witness_witness_witness_witness_left
Original defined command ledger · 87 lines
- 0001
induction k - 0002
intro z - 0003
intro N - 0004
intro hb - 0005
intro hn - 0006
intro hz - 0007
intro hu - 0008
exfalso - 0009
apply hz - 0010
specialize gaussian_norm_zero_implies_code_zero (z) - 0011
apply gaussian_norm_zero_implies_code_zero - 0012
specialize gaussian_norm_value_transport (z) - 0013
specialize gaussian_norm_value_transport (N) - 0014
specialize gaussian_norm_value_transport (0) - 0015
apply gaussian_norm_value_transport - 0016
specialize le_zero (N) - 0017
apply le_zero - 0018
exact hb - 0019
exact hn - 0020
intro z - 0021
intro N - 0022
intro hb - 0023
intro hn - 0024
intro hz - 0025
intro hu - 0026
have hs : GIrreducible(z) ∨ (∃ x. ∃ y. ∃ n. ∃ m. GStrictNonunitFactorization(z,N,x,y,n,m)) - 0027
specialize gaussian_irreducible_or_strict_nonunit_factorization (z) - 0028
specialize gaussian_irreducible_or_strict_nonunit_factorization (N) - 0029
apply gaussian_irreducible_or_strict_nonunit_factorization - 0030
exact hn - 0031
exact hz - 0032
exact hu - 0033
cases hs - 0034
exists (z) - 0035
split - 0036
exact hs_left - 0037
specialize gaussian_divides_reflexive (z) - 0038
apply gaussian_divides_reflexive - 0039
specialize gaussian_norm_input_valid (z) - 0040
specialize gaussian_norm_input_valid (N) - 0041
apply gaussian_norm_input_valid - 0042
exact hn - 0043
cases hs_right - 0044
cases hs_right_witness - 0045
cases hs_right_witness_witness - 0046
cases hs_right_witness_witness_witness - 0047
cases hs_right_witness_witness_witness_witness - 0048
cases hs_right_witness_witness_witness_witness_right - 0049
cases hs_right_witness_witness_witness_witness_right_right - 0050
cases hs_right_witness_witness_witness_witness_right_right_right - 0051
cases hs_right_witness_witness_witness_witness_right_right_right_right - 0052
cases hs_right_witness_witness_witness_witness_right_right_right_right_right - 0053
have hrec : ∃ p. GIrreducible(p) ∧ GDvd(p,x) - 0054
specialize IH (x) - 0055
specialize IH (x2) - 0056
apply IH - 0057
specialize le_of_succ_le_succ (x2) - 0058
specialize le_of_succ_le_succ (k) - 0059
apply le_of_succ_le_succ - 0060
specialize lt_of_lt_of_le (x2) - 0061
specialize lt_of_lt_of_le (N) - 0062
specialize lt_of_lt_of_le (S k) - 0063
apply lt_of_lt_of_le - 0064
exact hs_right_witness_witness_witness_witness_right_right_right_right_right_left - 0065
exact hb - 0066
exact hs_right_witness_witness_witness_witness_right_left - 0067
intro hzero - 0068
specialize gaussian_search_divisor_of_nonzero_nonzero (x) - 0069
specialize gaussian_search_divisor_of_nonzero_nonzero (z) - 0070
apply gaussian_search_divisor_of_nonzero_nonzero - 0071
exists (x1) - 0072
exact hs_right_witness_witness_witness_witness_left - 0073
exact hz - 0074
exact hzero - 0075
exact hs_right_witness_witness_witness_witness_right_right_right_left - 0076
cases hrec - 0077
cases hrec_witness - 0078
exists (x4) - 0079
split - 0080
exact hrec_witness_left - 0081
specialize gaussian_divides_transitive (x4) - 0082
specialize gaussian_divides_transitive (x) - 0083
specialize gaussian_divides_transitive (z) - 0084
apply gaussian_divides_transitive - 0085
exact hrec_witness_right - 0086
exists (x1) - 0087
exact hs_right_witness_witness_witness_witness_left