ConvergentMatrixTrace(s,h,e,k,u,U,v,V)

exists cfc_tail_prioritylayer. ((exists cfc_state_prioritylayerinitial. ((exists cfc_left_prioritylayerinitialcode cfc_right_prioritylayerinitialcode cfc_matrix_prioritylayerinitialcode. ((cfc_left_prioritylayerinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_prioritylayerinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_prioritylayerinitialcode = ((cfc_left_prioritylayerinitialcode) + (cfc_right_prioritylayerinitialcode)) * S ((cfc_left_prioritylayerinitialcode) + (cfc_right_prioritylayerinitialcode)) + ((cfc_right_prioritylayerinitialcode) + (cfc_right_prioritylayerinitialcode))) /\ ((cfc_state_prioritylayerinitial) = ((cfc_tail_prioritylayer) + (cfc_matrix_prioritylayerinitialcode)) * S ((cfc_tail_prioritylayer) + (cfc_matrix_prioritylayerinitialcode)) + ((cfc_matrix_prioritylayerinitialcode) + (cfc_matrix_prioritylayerinitialcode))))))) /\ (((exists ff_h_prioritylayerinitialentry. ff_h_prioritylayerinitialentry + S (cfc_state_prioritylayerinitial) = S ((S (0)) * e)) /\ exists ff_q_prioritylayerinitialentry. h = ff_q_prioritylayerinitialentry * S ((S (0)) * e) + (cfc_state_prioritylayerinitial))))) /\ ((exists cfc_state_prioritylayerterminal. ((exists cfc_left_prioritylayerterminalcode cfc_right_prioritylayerterminalcode cfc_matrix_prioritylayerterminalcode. ((cfc_left_prioritylayerterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_prioritylayerterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_prioritylayerterminalcode = ((cfc_left_prioritylayerterminalcode) + (cfc_right_prioritylayerterminalcode)) * S ((cfc_left_prioritylayerterminalcode) + (cfc_right_prioritylayerterminalcode)) + ((cfc_right_prioritylayerterminalcode) + (cfc_right_prioritylayerterminalcode))) /\ ((cfc_state_prioritylayerterminal) = ((s) + (cfc_matrix_prioritylayerterminalcode)) * S ((s) + (cfc_matrix_prioritylayerterminalcode)) + ((cfc_matrix_prioritylayerterminalcode) + (cfc_matrix_prioritylayerterminalcode))))))) /\ (((exists ff_h_prioritylayerterminalentry. ff_h_prioritylayerterminalentry + S (cfc_state_prioritylayerterminal) = S ((S (k)) * e)) /\ exists ff_q_prioritylayerterminalentry. h = ff_q_prioritylayerterminalentry * S ((S (k)) * e) + (cfc_state_prioritylayerterminal))))) /\ (forall cfc_index_prioritylayer. (exists cfba_gap_prioritylayerbound. cfba_gap_prioritylayerbound + S (cfc_index_prioritylayer) = (k)) -> exists cfc_old_prioritylayer cfc_a_prioritylayer cfc_b_prioritylayer cfc_c_prioritylayer cfc_d_prioritylayer cfc_new_prioritylayer cfc_quotient_prioritylayer. ((exists cfc_state_prioritylayerprevious. ((exists cfc_left_prioritylayerpreviouscode cfc_right_prioritylayerpreviouscode cfc_matrix_prioritylayerpreviouscode. ((cfc_left_prioritylayerpreviouscode = ((cfc_a_prioritylayer) + (cfc_b_prioritylayer)) * S ((cfc_a_prioritylayer) + (cfc_b_prioritylayer)) + ((cfc_b_prioritylayer) + (cfc_b_prioritylayer))) /\ ((cfc_right_prioritylayerpreviouscode = ((cfc_c_prioritylayer) + (cfc_d_prioritylayer)) * S ((cfc_c_prioritylayer) + (cfc_d_prioritylayer)) + ((cfc_d_prioritylayer) + (cfc_d_prioritylayer))) /\ ((cfc_matrix_prioritylayerpreviouscode = ((cfc_left_prioritylayerpreviouscode) + (cfc_right_prioritylayerpreviouscode)) * S ((cfc_left_prioritylayerpreviouscode) + (cfc_right_prioritylayerpreviouscode)) + ((cfc_right_prioritylayerpreviouscode) + (cfc_right_prioritylayerpreviouscode))) /\ ((cfc_state_prioritylayerprevious) = ((cfc_old_prioritylayer) + (cfc_matrix_prioritylayerpreviouscode)) * S ((cfc_old_prioritylayer) + (cfc_matrix_prioritylayerpreviouscode)) + ((cfc_matrix_prioritylayerpreviouscode) + (cfc_matrix_prioritylayerpreviouscode))))))) /\ (((exists ff_h_prioritylayerpreviousentry. ff_h_prioritylayerpreviousentry + S (cfc_state_prioritylayerprevious) = S ((S (cfc_index_prioritylayer)) * e)) /\ exists ff_q_prioritylayerpreviousentry. h = ff_q_prioritylayerpreviousentry * S ((S (cfc_index_prioritylayer)) * e) + (cfc_state_prioritylayerprevious))))) /\ ((exists cfc_state_prioritylayerfollowing. ((exists cfc_left_prioritylayerfollowingcode cfc_right_prioritylayerfollowingcode cfc_matrix_prioritylayerfollowingcode. ((cfc_left_prioritylayerfollowingcode = (((cfc_quotient_prioritylayer * cfc_a_prioritylayer + cfc_c_prioritylayer)) + ((cfc_quotient_prioritylayer * cfc_b_prioritylayer + cfc_d_prioritylayer))) * S (((cfc_quotient_prioritylayer * cfc_a_prioritylayer + cfc_c_prioritylayer)) + ((cfc_quotient_prioritylayer * cfc_b_prioritylayer + cfc_d_prioritylayer))) + (((cfc_quotient_prioritylayer * cfc_b_prioritylayer + cfc_d_prioritylayer)) + ((cfc_quotient_prioritylayer * cfc_b_prioritylayer + cfc_d_prioritylayer)))) /\ ((cfc_right_prioritylayerfollowingcode = ((cfc_a_prioritylayer) + (cfc_b_prioritylayer)) * S ((cfc_a_prioritylayer) + (cfc_b_prioritylayer)) + ((cfc_b_prioritylayer) + (cfc_b_prioritylayer))) /\ ((cfc_matrix_prioritylayerfollowingcode = ((cfc_left_prioritylayerfollowingcode) + (cfc_right_prioritylayerfollowingcode)) * S ((cfc_left_prioritylayerfollowingcode) + (cfc_right_prioritylayerfollowingcode)) + ((cfc_right_prioritylayerfollowingcode) + (cfc_right_prioritylayerfollowingcode))) /\ ((cfc_state_prioritylayerfollowing) = ((cfc_new_prioritylayer) + (cfc_matrix_prioritylayerfollowingcode)) * S ((cfc_new_prioritylayer) + (cfc_matrix_prioritylayerfollowingcode)) + ((cfc_matrix_prioritylayerfollowingcode) + (cfc_matrix_prioritylayerfollowingcode))))))) /\ (((exists ff_h_prioritylayerfollowingentry. ff_h_prioritylayerfollowingentry + S (cfc_state_prioritylayerfollowing) = S ((S (S cfc_index_prioritylayer)) * e)) /\ exists ff_q_prioritylayerfollowingentry. h = ff_q_prioritylayerfollowingentry * S ((S (S cfc_index_prioritylayer)) * e) + (cfc_state_prioritylayerfollowing))))) /\ (cfc_new_prioritylayer = S ((cfc_quotient_prioritylayer + cfc_old_prioritylayer) * S (cfc_quotient_prioritylayer + cfc_old_prioritylayer) + (cfc_old_prioritylayer + cfc_old_prioritylayer))))))))

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