ND0145 — SignedMul(a,b,c)

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

SignedDecode(z,p,n)

Definitions depending on this notation

ArithScale(a,F,G,l)DirichletEntry(F,G,n,d,z)MultiplicativePrefix(N,F)SignedCartesianProduct(F,G,T,m,n)DirichletDivisorGridWitness(F,G,m,n,i,z,d,e,a,b)

Checked theorems using this definition