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.
Definition in prerequisite notation
∃ ge_first_rp_lowerlayer. ∃ ge_first_rn_lowerlayer. ∃ ge_first_ip_lowerlayer. ∃ ge_first_in_lowerlayer. ∃ ge_second_rp_lowerlayer. ∃ ge_second_rn_lowerlayer. ∃ ge_second_ip_lowerlayer. ∃ ge_second_in_lowerlayer. ZPairRep(a,ge_first_rp_lowerlayer,ge_first_rn_lowerlayer,ge_first_ip_lowerlayer,ge_first_in_lowerlayer) ∧ (ZPairRep(b,ge_second_rp_lowerlayer,ge_second_rn_lowerlayer,ge_second_ip_lowerlayer,ge_second_in_lowerlayer) ∧ ZPairRep(c,ge_first_rp_lowerlayer + ge_second_rp_lowerlayer,ge_first_rn_lowerlayer + ge_second_rn_lowerlayer,ge_first_ip_lowerlayer + ge_second_ip_lowerlayer,ge_first_in_lowerlayer + ge_second_in_lowerlayer))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ge_first_rp_lowerlayer ge_first_rn_lowerlayer ge_first_ip_lowerlayer ge_first_in_lowerlayer ge_second_rp_lowerlayer ge_second_rn_lowerlayer ge_second_ip_lowerlayer ge_second_in_lowerlayer. ((exists ge_representation_real_code_lowerlayerfirst ge_representation_imaginary_code_lowerlayerfirst. (((a) = ((ge_representation_real_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst)) * S ((ge_representation_real_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst)) + ((ge_representation_imaginary_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst))) /\ ((exists ge_balance_positive_lowerlayerfirstreal ge_balance_negative_lowerlayerfirstreal. (((((ge_representation_real_code_lowerlayerfirst) = 2 * (ge_balance_positive_lowerlayerfirstreal) /\ (ge_balance_negative_lowerlayerfirstreal) = 0) \/ exists ge_signed_half_lowerlayerfirstrealdecode. (((ge_representation_real_code_lowerlayerfirst) = 2 * ge_signed_half_lowerlayerfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayerfirstreal) = 0) /\ (ge_balance_negative_lowerlayerfirstreal) = S ge_signed_half_lowerlayerfirstrealdecode))) /\ ((ge_first_rp_lowerlayer) + ge_balance_negative_lowerlayerfirstreal = (ge_first_rn_lowerlayer) + ge_balance_positive_lowerlayerfirstreal))) /\ (exists ge_balance_positive_lowerlayerfirstimaginary ge_balance_negative_lowerlayerfirstimaginary. (((((ge_representation_imaginary_code_lowerlayerfirst) = 2 * (ge_balance_positive_lowerlayerfirstimaginary) /\ (ge_balance_negative_lowerlayerfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayerfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayerfirst) = 2 * ge_signed_half_lowerlayerfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayerfirstimaginary) = S ge_signed_half_lowerlayerfirstimaginarydecode))) /\ ((ge_first_ip_lowerlayer) + ge_balance_negative_lowerlayerfirstimaginary = (ge_first_in_lowerlayer) + ge_balance_positive_lowerlayerfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayersecond ge_representation_imaginary_code_lowerlayersecond. (((b) = ((ge_representation_real_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond)) * S ((ge_representation_real_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond)) + ((ge_representation_imaginary_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond))) /\ ((exists ge_balance_positive_lowerlayersecondreal ge_balance_negative_lowerlayersecondreal. (((((ge_representation_real_code_lowerlayersecond) = 2 * (ge_balance_positive_lowerlayersecondreal) /\ (ge_balance_negative_lowerlayersecondreal) = 0) \/ exists ge_signed_half_lowerlayersecondrealdecode. (((ge_representation_real_code_lowerlayersecond) = 2 * ge_signed_half_lowerlayersecondrealdecode + 1 /\ (ge_balance_positive_lowerlayersecondreal) = 0) /\ (ge_balance_negative_lowerlayersecondreal) = S ge_signed_half_lowerlayersecondrealdecode))) /\ ((ge_second_rp_lowerlayer) + ge_balance_negative_lowerlayersecondreal = (ge_second_rn_lowerlayer) + ge_balance_positive_lowerlayersecondreal))) /\ (exists ge_balance_positive_lowerlayersecondimaginary ge_balance_negative_lowerlayersecondimaginary. (((((ge_representation_imaginary_code_lowerlayersecond) = 2 * (ge_balance_positive_lowerlayersecondimaginary) /\ (ge_balance_negative_lowerlayersecondimaginary) = 0) \/ exists ge_signed_half_lowerlayersecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayersecond) = 2 * ge_signed_half_lowerlayersecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersecondimaginary) = 0) /\ (ge_balance_negative_lowerlayersecondimaginary) = S ge_signed_half_lowerlayersecondimaginarydecode))) /\ ((ge_second_ip_lowerlayer) + ge_balance_negative_lowerlayersecondimaginary = (ge_second_in_lowerlayer) + ge_balance_positive_lowerlayersecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayeroutput ge_representation_imaginary_code_lowerlayeroutput. (((c) = ((ge_representation_real_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput)) * S ((ge_representation_real_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput)) + ((ge_representation_imaginary_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput))) /\ ((exists ge_balance_positive_lowerlayeroutputreal ge_balance_negative_lowerlayeroutputreal. (((((ge_representation_real_code_lowerlayeroutput) = 2 * (ge_balance_positive_lowerlayeroutputreal) /\ (ge_balance_negative_lowerlayeroutputreal) = 0) \/ exists ge_signed_half_lowerlayeroutputrealdecode. (((ge_representation_real_code_lowerlayeroutput) = 2 * ge_signed_half_lowerlayeroutputrealdecode + 1 /\ (ge_balance_positive_lowerlayeroutputreal) = 0) /\ (ge_balance_negative_lowerlayeroutputreal) = S ge_signed_half_lowerlayeroutputrealdecode))) /\ ((((ge_first_rp_lowerlayer) + (ge_second_rp_lowerlayer))) + ge_balance_negative_lowerlayeroutputreal = (((ge_first_rn_lowerlayer) + (ge_second_rn_lowerlayer))) + ge_balance_positive_lowerlayeroutputreal))) /\ (exists ge_balance_positive_lowerlayeroutputimaginary ge_balance_negative_lowerlayeroutputimaginary. (((((ge_representation_imaginary_code_lowerlayeroutput) = 2 * (ge_balance_positive_lowerlayeroutputimaginary) /\ (ge_balance_negative_lowerlayeroutputimaginary) = 0) \/ exists ge_signed_half_lowerlayeroutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayeroutput) = 2 * ge_signed_half_lowerlayeroutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayeroutputimaginary) = 0) /\ (ge_balance_negative_lowerlayeroutputimaginary) = S ge_signed_half_lowerlayeroutputimaginarydecode))) /\ ((((ge_first_ip_lowerlayer) + (ge_second_ip_lowerlayer))) + ge_balance_negative_lowerlayeroutputimaginary = (((ge_first_in_lowerlayer) + (ge_second_in_lowerlayer))) + ge_balance_positive_lowerlayeroutputimaginary))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.