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

((l = m) /\ (((((forall pfp_i_lowerlayerpermutationbounded. (exists pfp_gap_lowerlayerpermutationboundedindex. pfp_gap_lowerlayerpermutationboundedindex + S (pfp_i_lowerlayerpermutationbounded) = (l)) -> exists pfp_a_lowerlayerpermutationbounded. (((exists ff_h_pfp_lowerlayerpermutationboundedentry. ff_h_pfp_lowerlayerpermutationboundedentry + S (pfp_a_lowerlayerpermutationbounded) = S ((S (pfp_i_lowerlayerpermutationbounded)) * v)) /\ exists ff_q_pfp_lowerlayerpermutationboundedentry. u = ff_q_pfp_lowerlayerpermutationboundedentry * S ((S (pfp_i_lowerlayerpermutationbounded)) * v) + (pfp_a_lowerlayerpermutationbounded))) /\ (exists pfp_gap_lowerlayerpermutationboundedvalue. pfp_gap_lowerlayerpermutationboundedvalue + S (pfp_a_lowerlayerpermutationbounded) = (l))) /\ (((forall pfp_i_lowerlayerpermutationinjective pfp_j_lowerlayerpermutationinjective pfp_a_lowerlayerpermutationinjective. (exists pfp_gap_lowerlayerpermutationinjectivefirst. pfp_gap_lowerlayerpermutationinjectivefirst + S (pfp_i_lowerlayerpermutationinjective) = (l)) -> (exists pfp_gap_lowerlayerpermutationinjectivesecond. pfp_gap_lowerlayerpermutationinjectivesecond + S (pfp_j_lowerlayerpermutationinjective) = (l)) -> (((exists ff_h_pfp_lowerlayerpermutationinjectiveleft. ff_h_pfp_lowerlayerpermutationinjectiveleft + S (pfp_a_lowerlayerpermutationinjective) = S ((S (pfp_i_lowerlayerpermutationinjective)) * v)) /\ exists ff_q_pfp_lowerlayerpermutationinjectiveleft. u = ff_q_pfp_lowerlayerpermutationinjectiveleft * S ((S (pfp_i_lowerlayerpermutationinjective)) * v) + (pfp_a_lowerlayerpermutationinjective))) -> (((exists ff_h_pfp_lowerlayerpermutationinjectiveright. ff_h_pfp_lowerlayerpermutationinjectiveright + S (pfp_a_lowerlayerpermutationinjective) = S ((S (pfp_j_lowerlayerpermutationinjective)) * v)) /\ exists ff_q_pfp_lowerlayerpermutationinjectiveright. u = ff_q_pfp_lowerlayerpermutationinjectiveright * S ((S (pfp_j_lowerlayerpermutationinjective)) * v) + (pfp_a_lowerlayerpermutationinjective))) -> pfp_i_lowerlayerpermutationinjective = pfp_j_lowerlayerpermutationinjective) /\ (forall pfp_a_lowerlayerpermutationsurjective. (exists pfp_gap_lowerlayerpermutationsurjectivevalue. pfp_gap_lowerlayerpermutationsurjectivevalue + S (pfp_a_lowerlayerpermutationsurjective) = (l)) -> exists pfp_i_lowerlayerpermutationsurjective. (exists pfp_gap_lowerlayerpermutationsurjectiveindex. pfp_gap_lowerlayerpermutationsurjectiveindex + S (pfp_i_lowerlayerpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_lowerlayerpermutationsurjectiveentry. ff_h_pfp_lowerlayerpermutationsurjectiveentry + S (pfp_a_lowerlayerpermutationsurjective) = S ((S (pfp_i_lowerlayerpermutationsurjective)) * v)) /\ exists ff_q_pfp_lowerlayerpermutationsurjectiveentry. u = ff_q_pfp_lowerlayerpermutationsurjectiveentry * S ((S (pfp_i_lowerlayerpermutationsurjective)) * v) + (pfp_a_lowerlayerpermutationsurjective)))))))) /\ (forall pfp_i_lowerlayermatching pfp_j_lowerlayermatching pfp_a_lowerlayermatching. (exists pfp_gap_lowerlayermatchingbound. pfp_gap_lowerlayermatchingbound + S (pfp_i_lowerlayermatching) = (l)) -> (((exists ff_h_pfp_lowerlayermatchingmap. ff_h_pfp_lowerlayermatchingmap + S (pfp_j_lowerlayermatching) = S ((S (pfp_i_lowerlayermatching)) * v)) /\ exists ff_q_pfp_lowerlayermatchingmap. u = ff_q_pfp_lowerlayermatchingmap * S ((S (pfp_i_lowerlayermatching)) * v) + (pfp_j_lowerlayermatching))) -> (((exists ff_h_pfp_lowerlayermatchingsource. ff_h_pfp_lowerlayermatchingsource + S (pfp_a_lowerlayermatching) = S ((S (pfp_i_lowerlayermatching)) * c)) /\ exists ff_q_pfp_lowerlayermatchingsource. b = ff_q_pfp_lowerlayermatchingsource * S ((S (pfp_i_lowerlayermatching)) * c) + (pfp_a_lowerlayermatching))) -> (((exists ff_h_pfp_lowerlayermatchingtarget. ff_h_pfp_lowerlayermatchingtarget + S (pfp_a_lowerlayermatching) = S ((S (pfp_j_lowerlayermatching)) * e)) /\ exists ff_q_pfp_lowerlayermatchingtarget. d = ff_q_pfp_lowerlayermatchingtarget * S ((S (pfp_j_lowerlayermatching)) * e) + (pfp_a_lowerlayermatching)))))))

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