PermutationPrefix(b,c,l)

((forall fp_i_lowerlayer_bounded. (exists fp_gap_lowerlayer_bounded_index. fp_gap_lowerlayer_bounded_index + S fp_i_lowerlayer_bounded = l) -> exists fp_value_lowerlayer_bounded. ((((exists ff_h_lowerlayer_bounded_entry. ff_h_lowerlayer_bounded_entry + S (fp_value_lowerlayer_bounded) = S ((S (fp_i_lowerlayer_bounded)) * c)) /\ exists ff_q_lowerlayer_bounded_entry. b = ff_q_lowerlayer_bounded_entry * S ((S (fp_i_lowerlayer_bounded)) * c) + (fp_value_lowerlayer_bounded))) /\ (exists fp_gap_lowerlayer_bounded_value. fp_gap_lowerlayer_bounded_value + S fp_value_lowerlayer_bounded = l))) /\ ((forall fp_i_lowerlayer_injective fp_j_lowerlayer_injective fp_value_lowerlayer_injective. (exists fp_gap_lowerlayer_injective_i. fp_gap_lowerlayer_injective_i + S fp_i_lowerlayer_injective = l) -> (exists fp_gap_lowerlayer_injective_j. fp_gap_lowerlayer_injective_j + S fp_j_lowerlayer_injective = l) -> (((exists ff_h_lowerlayer_injective_left. ff_h_lowerlayer_injective_left + S (fp_value_lowerlayer_injective) = S ((S (fp_i_lowerlayer_injective)) * c)) /\ exists ff_q_lowerlayer_injective_left. b = ff_q_lowerlayer_injective_left * S ((S (fp_i_lowerlayer_injective)) * c) + (fp_value_lowerlayer_injective))) -> (((exists ff_h_lowerlayer_injective_right. ff_h_lowerlayer_injective_right + S (fp_value_lowerlayer_injective) = S ((S (fp_j_lowerlayer_injective)) * c)) /\ exists ff_q_lowerlayer_injective_right. b = ff_q_lowerlayer_injective_right * S ((S (fp_j_lowerlayer_injective)) * c) + (fp_value_lowerlayer_injective))) -> fp_i_lowerlayer_injective = fp_j_lowerlayer_injective) /\ (forall fp_value_lowerlayer_surjective. (exists fp_gap_lowerlayer_surjective_value. fp_gap_lowerlayer_surjective_value + S fp_value_lowerlayer_surjective = l) -> exists fp_i_lowerlayer_surjective. ((exists fp_gap_lowerlayer_surjective_index. fp_gap_lowerlayer_surjective_index + S fp_i_lowerlayer_surjective = l) /\ (((exists ff_h_lowerlayer_surjective_entry. ff_h_lowerlayer_surjective_entry + S (fp_value_lowerlayer_surjective) = S ((S (fp_i_lowerlayer_surjective)) * c)) /\ exists ff_q_lowerlayer_surjective_entry. b = ff_q_lowerlayer_surjective_entry * S ((S (fp_i_lowerlayer_surjective)) * c) + (fp_value_lowerlayer_surjective)))))))

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