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
∃ ee_first_rp_lowerlayer. ∃ ee_first_rn_lowerlayer. ∃ ee_first_ip_lowerlayer. ∃ ee_first_in_lowerlayer. ∃ ee_second_rp_lowerlayer. ∃ ee_second_rn_lowerlayer. ∃ ee_second_ip_lowerlayer. ∃ ee_second_in_lowerlayer. ZPairRep(a,ee_first_rp_lowerlayer,ee_first_rn_lowerlayer,ee_first_ip_lowerlayer,ee_first_in_lowerlayer) ∧ (ZPairRep(b,ee_second_rp_lowerlayer,ee_second_rn_lowerlayer,ee_second_ip_lowerlayer,ee_second_in_lowerlayer) ∧ ZPairRep(c,ee_first_rp_lowerlayer · ee_second_rp_lowerlayer + ee_first_rn_lowerlayer · ee_second_rn_lowerlayer + (ee_first_ip_lowerlayer · ee_second_in_lowerlayer + ee_first_in_lowerlayer · ee_second_ip_lowerlayer),ee_first_rp_lowerlayer · ee_second_rn_lowerlayer + ee_first_rn_lowerlayer · ee_second_rp_lowerlayer + (ee_first_ip_lowerlayer · ee_second_ip_lowerlayer + ee_first_in_lowerlayer · ee_second_in_lowerlayer),ee_first_rp_lowerlayer · ee_second_ip_lowerlayer + ee_first_rn_lowerlayer · ee_second_in_lowerlayer + (ee_first_ip_lowerlayer · ee_second_rp_lowerlayer + ee_first_in_lowerlayer · ee_second_rn_lowerlayer) + (ee_first_ip_lowerlayer · ee_second_in_lowerlayer + ee_first_in_lowerlayer · ee_second_ip_lowerlayer),ee_first_rp_lowerlayer · ee_second_in_lowerlayer + ee_first_rn_lowerlayer · ee_second_ip_lowerlayer + (ee_first_ip_lowerlayer · ee_second_rn_lowerlayer + ee_first_in_lowerlayer · ee_second_rp_lowerlayer) + (ee_first_ip_lowerlayer · ee_second_ip_lowerlayer + ee_first_in_lowerlayer · ee_second_in_lowerlayer)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ee_first_rp_lowerlayer ee_first_rn_lowerlayer ee_first_ip_lowerlayer ee_first_in_lowerlayer ee_second_rp_lowerlayer ee_second_rn_lowerlayer ee_second_ip_lowerlayer ee_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))) /\ ((ee_first_rp_lowerlayer) + ge_balance_negative_lowerlayerfirstreal = (ee_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))) /\ ((ee_first_ip_lowerlayer) + ge_balance_negative_lowerlayerfirstimaginary = (ee_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))) /\ ((ee_second_rp_lowerlayer) + ge_balance_negative_lowerlayersecondreal = (ee_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))) /\ ((ee_second_ip_lowerlayer) + ge_balance_negative_lowerlayersecondimaginary = (ee_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))) /\ ((((((((ee_first_rp_lowerlayer) * (ee_second_rp_lowerlayer))) + (((ee_first_rn_lowerlayer) * (ee_second_rn_lowerlayer))))) + (((((ee_first_ip_lowerlayer) * (ee_second_in_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_second_ip_lowerlayer))))))) + ge_balance_negative_lowerlayeroutputreal = (((((((ee_first_rp_lowerlayer) * (ee_second_rn_lowerlayer))) + (((ee_first_rn_lowerlayer) * (ee_second_rp_lowerlayer))))) + (((((ee_first_ip_lowerlayer) * (ee_second_ip_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_second_in_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))) /\ ((((((((((ee_first_rp_lowerlayer) * (ee_second_ip_lowerlayer))) + (((ee_first_rn_lowerlayer) * (ee_second_in_lowerlayer))))) + (((((ee_first_ip_lowerlayer) * (ee_second_rp_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_second_rn_lowerlayer))))))) + (((((ee_first_ip_lowerlayer) * (ee_second_in_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_second_ip_lowerlayer))))))) + ge_balance_negative_lowerlayeroutputimaginary = (((((((((ee_first_rp_lowerlayer) * (ee_second_in_lowerlayer))) + (((ee_first_rn_lowerlayer) * (ee_second_ip_lowerlayer))))) + (((((ee_first_ip_lowerlayer) * (ee_second_rn_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_second_rp_lowerlayer))))))) + (((((ee_first_ip_lowerlayer) * (ee_second_ip_lowerlayer))) + (((ee_first_in_lowerlayer) * (ee_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.