ND0150

FactorListMatching(b,c,d,e,u,v,l)

Each actual source factor equals the factor at the index decoded from its image under the witnessed map.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Definition in prerequisite notation

∀ pfp_i_lowerlayer. ∀ pfp_j_lowerlayer. ∀ pfp_a_lowerlayer. Lt(pfp_i_lowerlayer,l) → BetaAt(u,v,pfp_i_lowerlayer,pfp_j_lowerlayer) → BetaAt(b,c,pfp_i_lowerlayer,pfp_a_lowerlayer) → BetaAt(d,e,pfp_j_lowerlayer,pfp_a_lowerlayer)

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

Hygienic expanded first-order definition 
forall pfp_i_lowerlayer pfp_j_lowerlayer pfp_a_lowerlayer. (exists pfp_gap_lowerlayerbound. pfp_gap_lowerlayerbound + S (pfp_i_lowerlayer) = (l)) -> (((exists ff_h_pfp_lowerlayermap. ff_h_pfp_lowerlayermap + S (pfp_j_lowerlayer) = S ((S (pfp_i_lowerlayer)) * v)) /\ exists ff_q_pfp_lowerlayermap. u = ff_q_pfp_lowerlayermap * S ((S (pfp_i_lowerlayer)) * v) + (pfp_j_lowerlayer))) -> (((exists ff_h_pfp_lowerlayersource. ff_h_pfp_lowerlayersource + S (pfp_a_lowerlayer) = S ((S (pfp_i_lowerlayer)) * c)) /\ exists ff_q_pfp_lowerlayersource. b = ff_q_pfp_lowerlayersource * S ((S (pfp_i_lowerlayer)) * c) + (pfp_a_lowerlayer))) -> (((exists ff_h_pfp_lowerlayertarget. ff_h_pfp_lowerlayertarget + S (pfp_a_lowerlayer) = S ((S (pfp_j_lowerlayer)) * e)) /\ exists ff_q_pfp_lowerlayertarget. d = ff_q_pfp_lowerlayertarget * S ((S (pfp_j_lowerlayer)) * e) + (pfp_a_lowerlayer)))

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)

Definitions depending on this notation

PrimeFactorListPermutation(b,c,l,d,e,m,u,v)

Checked theorems using this definition

AF000D · factor_permutation_empty_matchingAF000F · factor_permutation_matching_appendAF0010 · factor_permutation_matched_appendAF0011 · factor_permutation_matched_append_existsAF0017 · factor_permutation_matching_unswapAF0018 · factor_permutation_matched_unswap_existsAF0019 · prime_factor_lists_matching_by_lengthAF001A · prime_factor_lists_permutation_exists