Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∃ sm_lp_lowerlayer. ∃ sm_ln_lowerlayer. ∃ sm_rp_lowerlayer. ∃ sm_rn_lowerlayer. ∃ sm_op_lowerlayer. ∃ sm_on_lowerlayer. SignedDecode(a,sm_lp_lowerlayer,sm_ln_lowerlayer) ∧ (SignedDecode(b,sm_rp_lowerlayer,sm_rn_lowerlayer) ∧ (SignedDecode(c,sm_op_lowerlayer,sm_on_lowerlayer) ∧ sm_lp_lowerlayer · sm_rp_lowerlayer + sm_ln_lowerlayer · sm_rn_lowerlayer + sm_on_lowerlayer = sm_lp_lowerlayer · sm_rn_lowerlayer + sm_ln_lowerlayer · sm_rp_lowerlayer + sm_op_lowerlayer))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists sm_lp_lowerlayer sm_ln_lowerlayer sm_rp_lowerlayer sm_rn_lowerlayer sm_op_lowerlayer sm_on_lowerlayer. (((a = 2 * sm_lp_lowerlayer /\ sm_ln_lowerlayer = 0) \/ exists sd_half_lowerlayer_left. ((a = 2 * sd_half_lowerlayer_left + 1 /\ sm_lp_lowerlayer = 0) /\ sm_ln_lowerlayer = S sd_half_lowerlayer_left)) /\ (((b = 2 * sm_rp_lowerlayer /\ sm_rn_lowerlayer = 0) \/ exists sd_half_lowerlayer_right. ((b = 2 * sd_half_lowerlayer_right + 1 /\ sm_rp_lowerlayer = 0) /\ sm_rn_lowerlayer = S sd_half_lowerlayer_right)) /\ (((c = 2 * sm_op_lowerlayer /\ sm_on_lowerlayer = 0) \/ exists sd_half_lowerlayer_output. ((c = 2 * sd_half_lowerlayer_output + 1 /\ sm_op_lowerlayer = 0) /\ sm_on_lowerlayer = S sd_half_lowerlayer_output)) /\ (sm_lp_lowerlayer * sm_rp_lowerlayer + sm_ln_lowerlayer * sm_rn_lowerlayer) + sm_on_lowerlayer = (sm_lp_lowerlayer * sm_rn_lowerlayer + sm_ln_lowerlayer * sm_rp_lowerlayer) + sm_op_lowerlayer)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
ZU0001 · dirichlet_signed_unit_self_productZU0002 · dirichlet_signed_unit_product_classificationZU0003 · dirichlet_signed_unit_inverse_iffZU0006 · dirichlet_signed_unit_multiply_involutionZU0007 · dirichlet_signed_unit_multiply_cancel_rightZU0008 · dirichlet_signed_unit_affine_solveZU0009 · dirichlet_signed_unit_affine_unique