Convergent(s,i,u,v)

exists cfc_previous_numerator_prioritylayer cfc_previous_denominator_prioritylayer cfc_code_prioritylayer cfc_scale_prioritylayer. ((~(v = 0)) /\ (exists cfc_tail_prioritylayercomputation. ((exists cfc_state_prioritylayercomputationinitial. ((exists cfc_left_prioritylayercomputationinitialcode cfc_right_prioritylayercomputationinitialcode cfc_matrix_prioritylayercomputationinitialcode. ((cfc_left_prioritylayercomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_prioritylayercomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_prioritylayercomputationinitialcode = ((cfc_left_prioritylayercomputationinitialcode) + (cfc_right_prioritylayercomputationinitialcode)) * S ((cfc_left_prioritylayercomputationinitialcode) + (cfc_right_prioritylayercomputationinitialcode)) + ((cfc_right_prioritylayercomputationinitialcode) + (cfc_right_prioritylayercomputationinitialcode))) /\ ((cfc_state_prioritylayercomputationinitial) = ((cfc_tail_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationinitialcode)) * S ((cfc_tail_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationinitialcode)) + ((cfc_matrix_prioritylayercomputationinitialcode) + (cfc_matrix_prioritylayercomputationinitialcode))))))) /\ (((exists ff_h_prioritylayercomputationinitialentry. ff_h_prioritylayercomputationinitialentry + S (cfc_state_prioritylayercomputationinitial) = S ((S (0)) * cfc_scale_prioritylayer)) /\ exists ff_q_prioritylayercomputationinitialentry. cfc_code_prioritylayer = ff_q_prioritylayercomputationinitialentry * S ((S (0)) * cfc_scale_prioritylayer) + (cfc_state_prioritylayercomputationinitial))))) /\ ((exists cfc_state_prioritylayercomputationterminal. ((exists cfc_left_prioritylayercomputationterminalcode cfc_right_prioritylayercomputationterminalcode cfc_matrix_prioritylayercomputationterminalcode. ((cfc_left_prioritylayercomputationterminalcode = ((u) + (cfc_previous_numerator_prioritylayer)) * S ((u) + (cfc_previous_numerator_prioritylayer)) + ((cfc_previous_numerator_prioritylayer) + (cfc_previous_numerator_prioritylayer))) /\ ((cfc_right_prioritylayercomputationterminalcode = ((v) + (cfc_previous_denominator_prioritylayer)) * S ((v) + (cfc_previous_denominator_prioritylayer)) + ((cfc_previous_denominator_prioritylayer) + (cfc_previous_denominator_prioritylayer))) /\ ((cfc_matrix_prioritylayercomputationterminalcode = ((cfc_left_prioritylayercomputationterminalcode) + (cfc_right_prioritylayercomputationterminalcode)) * S ((cfc_left_prioritylayercomputationterminalcode) + (cfc_right_prioritylayercomputationterminalcode)) + ((cfc_right_prioritylayercomputationterminalcode) + (cfc_right_prioritylayercomputationterminalcode))) /\ ((cfc_state_prioritylayercomputationterminal) = ((s) + (cfc_matrix_prioritylayercomputationterminalcode)) * S ((s) + (cfc_matrix_prioritylayercomputationterminalcode)) + ((cfc_matrix_prioritylayercomputationterminalcode) + (cfc_matrix_prioritylayercomputationterminalcode))))))) /\ (((exists ff_h_prioritylayercomputationterminalentry. ff_h_prioritylayercomputationterminalentry + S (cfc_state_prioritylayercomputationterminal) = S ((S (S (i))) * cfc_scale_prioritylayer)) /\ exists ff_q_prioritylayercomputationterminalentry. cfc_code_prioritylayer = ff_q_prioritylayercomputationterminalentry * S ((S (S (i))) * cfc_scale_prioritylayer) + (cfc_state_prioritylayercomputationterminal))))) /\ (forall cfc_index_prioritylayercomputation. (exists cfba_gap_prioritylayercomputationbound. cfba_gap_prioritylayercomputationbound + S (cfc_index_prioritylayercomputation) = (S (i))) -> exists cfc_old_prioritylayercomputation cfc_a_prioritylayercomputation cfc_b_prioritylayercomputation cfc_c_prioritylayercomputation cfc_d_prioritylayercomputation cfc_new_prioritylayercomputation cfc_quotient_prioritylayercomputation. ((exists cfc_state_prioritylayercomputationprevious. ((exists cfc_left_prioritylayercomputationpreviouscode cfc_right_prioritylayercomputationpreviouscode cfc_matrix_prioritylayercomputationpreviouscode. ((cfc_left_prioritylayercomputationpreviouscode = ((cfc_a_prioritylayercomputation) + (cfc_b_prioritylayercomputation)) * S ((cfc_a_prioritylayercomputation) + (cfc_b_prioritylayercomputation)) + ((cfc_b_prioritylayercomputation) + (cfc_b_prioritylayercomputation))) /\ ((cfc_right_prioritylayercomputationpreviouscode = ((cfc_c_prioritylayercomputation) + (cfc_d_prioritylayercomputation)) * S ((cfc_c_prioritylayercomputation) + (cfc_d_prioritylayercomputation)) + ((cfc_d_prioritylayercomputation) + (cfc_d_prioritylayercomputation))) /\ ((cfc_matrix_prioritylayercomputationpreviouscode = ((cfc_left_prioritylayercomputationpreviouscode) + (cfc_right_prioritylayercomputationpreviouscode)) * S ((cfc_left_prioritylayercomputationpreviouscode) + (cfc_right_prioritylayercomputationpreviouscode)) + ((cfc_right_prioritylayercomputationpreviouscode) + (cfc_right_prioritylayercomputationpreviouscode))) /\ ((cfc_state_prioritylayercomputationprevious) = ((cfc_old_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationpreviouscode)) * S ((cfc_old_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationpreviouscode)) + ((cfc_matrix_prioritylayercomputationpreviouscode) + (cfc_matrix_prioritylayercomputationpreviouscode))))))) /\ (((exists ff_h_prioritylayercomputationpreviousentry. ff_h_prioritylayercomputationpreviousentry + S (cfc_state_prioritylayercomputationprevious) = S ((S (cfc_index_prioritylayercomputation)) * cfc_scale_prioritylayer)) /\ exists ff_q_prioritylayercomputationpreviousentry. cfc_code_prioritylayer = ff_q_prioritylayercomputationpreviousentry * S ((S (cfc_index_prioritylayercomputation)) * cfc_scale_prioritylayer) + (cfc_state_prioritylayercomputationprevious))))) /\ ((exists cfc_state_prioritylayercomputationfollowing. ((exists cfc_left_prioritylayercomputationfollowingcode cfc_right_prioritylayercomputationfollowingcode cfc_matrix_prioritylayercomputationfollowingcode. ((cfc_left_prioritylayercomputationfollowingcode = (((cfc_quotient_prioritylayercomputation * cfc_a_prioritylayercomputation + cfc_c_prioritylayercomputation)) + ((cfc_quotient_prioritylayercomputation * cfc_b_prioritylayercomputation + cfc_d_prioritylayercomputation))) * S (((cfc_quotient_prioritylayercomputation * cfc_a_prioritylayercomputation + cfc_c_prioritylayercomputation)) + ((cfc_quotient_prioritylayercomputation * cfc_b_prioritylayercomputation + cfc_d_prioritylayercomputation))) + (((cfc_quotient_prioritylayercomputation * cfc_b_prioritylayercomputation + cfc_d_prioritylayercomputation)) + ((cfc_quotient_prioritylayercomputation * cfc_b_prioritylayercomputation + cfc_d_prioritylayercomputation)))) /\ ((cfc_right_prioritylayercomputationfollowingcode = ((cfc_a_prioritylayercomputation) + (cfc_b_prioritylayercomputation)) * S ((cfc_a_prioritylayercomputation) + (cfc_b_prioritylayercomputation)) + ((cfc_b_prioritylayercomputation) + (cfc_b_prioritylayercomputation))) /\ ((cfc_matrix_prioritylayercomputationfollowingcode = ((cfc_left_prioritylayercomputationfollowingcode) + (cfc_right_prioritylayercomputationfollowingcode)) * S ((cfc_left_prioritylayercomputationfollowingcode) + (cfc_right_prioritylayercomputationfollowingcode)) + ((cfc_right_prioritylayercomputationfollowingcode) + (cfc_right_prioritylayercomputationfollowingcode))) /\ ((cfc_state_prioritylayercomputationfollowing) = ((cfc_new_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationfollowingcode)) * S ((cfc_new_prioritylayercomputation) + (cfc_matrix_prioritylayercomputationfollowingcode)) + ((cfc_matrix_prioritylayercomputationfollowingcode) + (cfc_matrix_prioritylayercomputationfollowingcode))))))) /\ (((exists ff_h_prioritylayercomputationfollowingentry. ff_h_prioritylayercomputationfollowingentry + S (cfc_state_prioritylayercomputationfollowing) = S ((S (S cfc_index_prioritylayercomputation)) * cfc_scale_prioritylayer)) /\ exists ff_q_prioritylayercomputationfollowingentry. cfc_code_prioritylayer = ff_q_prioritylayercomputationfollowingentry * S ((S (S cfc_index_prioritylayercomputation)) * cfc_scale_prioritylayer) + (cfc_state_prioritylayercomputationfollowing))))) /\ (cfc_new_prioritylayercomputation = S ((cfc_quotient_prioritylayercomputation + cfc_old_prioritylayercomputation) * S (cfc_quotient_prioritylayercomputation + cfc_old_prioritylayercomputation) + (cfc_old_prioritylayercomputation + cfc_old_prioritylayercomputation))))))))))

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