ND0292 — PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)

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

∃ pfc_complement_lowercontinuation. ∃ pfc_left_lowercontinuation. ∃ pfc_right_lowercontinuation. j + pfc_complement_lowercontinuation = i ∧ (BetaZeroExtend(ab,ac,L,j,pfc_left_lowercontinuation) ∧ (BetaZeroExtend(bb,bc,M,pfc_complement_lowercontinuation,pfc_right_lowercontinuation) ∧ t = pfc_left_lowercontinuation · pfc_right_lowercontinuation))

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition

exists pfc_complement_lowercontinuation pfc_left_lowercontinuation pfc_right_lowercontinuation. ((((j))+pfc_complement_lowercontinuation=((i))) /\ ((((((exists pfa_gap_lowercontinuationleftinside. pfa_gap_lowercontinuationleftinside + S ((j)) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationleftentry. ff_h_pfp_lowercontinuationleftentry + S (pfc_left_lowercontinuation) = S ((S ((j))) * (ac))) /\ exists ff_q_pfp_lowercontinuationleftentry. (ab) = ff_q_pfp_lowercontinuationleftentry * S ((S ((j))) * (ac)) + (pfc_left_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationleftoutside. pfc_gap_lowercontinuationleftoutside+((L))=((j))) /\ (((pfc_left_lowercontinuation)=0))))) /\ ((((((exists pfa_gap_lowercontinuationrightinside. pfa_gap_lowercontinuationrightinside + S (pfc_complement_lowercontinuation) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationrightentry. ff_h_pfp_lowercontinuationrightentry + S (pfc_right_lowercontinuation) = S ((S (pfc_complement_lowercontinuation)) * (bc))) /\ exists ff_q_pfp_lowercontinuationrightentry. (bb) = ff_q_pfp_lowercontinuationrightentry * S ((S (pfc_complement_lowercontinuation)) * (bc)) + (pfc_right_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationrightoutside. pfc_gap_lowercontinuationrightoutside+((M))=(pfc_complement_lowercontinuation)) /\ (((pfc_right_lowercontinuation)=0))))) /\ ((((t))=pfc_left_lowercontinuation*pfc_right_lowercontinuation)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

BetaZeroExtend(b,c,L,i,a)

Definitions depending on this notation

PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)

Checked theorems using this definition