ND0256

FpUnitSteps(p,b,c,n)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Each consecutive pair of actual history entries is related by addition of the canonical one. No modular-residue invariant is assumed.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

∀ pff_trace_index_bottomlayer. Lt(pff_trace_index_bottomlayer,n) → ∃ x. ∃ y. BetaAt(b,c,pff_trace_index_bottomlayer,x) ∧ (BetaAt(b,c,S pff_trace_index_bottomlayer,y) ∧ FpAdd(p,x,1,y))

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

Hygienic expanded first-order definition 
forall pff_trace_index_bottomlayer. (exists pfa_gap_bottomlayerindex. pfa_gap_bottomlayerindex + S (pff_trace_index_bottomlayer) = ((n))) -> exists pff_trace_before_bottomlayer pff_trace_after_bottomlayer. ((((exists ff_h_pft_bottomlayerbefore. ff_h_pft_bottomlayerbefore + S (pff_trace_before_bottomlayer) = S ((S (pff_trace_index_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerbefore. (b) = ff_q_pft_bottomlayerbefore * S ((S (pff_trace_index_bottomlayer)) * (c)) + (pff_trace_before_bottomlayer))) /\ (((((exists ff_h_pft_bottomlayerafter. ff_h_pft_bottomlayerafter + S (pff_trace_after_bottomlayer) = S ((S (S (pff_trace_index_bottomlayer))) * (c))) /\ exists ff_q_pft_bottomlayerafter. (b) = ff_q_pft_bottomlayerafter * S ((S (S (pff_trace_index_bottomlayer))) * (c)) + (pff_trace_after_bottomlayer))) /\ ((((exists pfa_gap_bottomlayeradditionleft. pfa_gap_bottomlayeradditionleft + S (pff_trace_before_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeradditionright. pfa_gap_bottomlayeradditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayeradditionresultbound. pfa_gap_bottomlayeradditionresultbound + S (pff_trace_after_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeradditionresultcongruence pfa_offset_right_bottomlayeradditionresultcongruence. ((pff_trace_before_bottomlayer) + (1)) + ((p)) * pfa_offset_left_bottomlayeradditionresultcongruence = (pff_trace_after_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeradditionresultcongruence)))))))))))))

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

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)FpAdd(p,a,b,c)

Definitions depending on this notation

FpUnitTrace(p,b,c,n,r)

Checked theorems using this definition

none directly; see definition consumers