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
Checked theorems using this definition
WS0007 · signed_table_multiply_lookupWS000B · signed_table_scalar_lookupWS0012 · signed_table_multiply_extendWS0013 · signed_table_multiply_existsWS0015 · signed_table_scalar_extendWS0016 · signed_table_scalar_existsWS001A · signed_table_scalar_add_introWS001C · signed_prefix_sum_scalar_multiplyWS001E · signed_prefix_sum_scalar_multiply_values_existWS0025 · signed_weighted_scalar_commuteWS0028 · signed_weighted_sum_scalar_linearity