PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H)

((exists pa_b_olte_prioritylayerA pa_c_olte_prioritylayerA. ((forall pa_i_olte_prioritylayerA_repeat. (exists pa_lt_olte_prioritylayerA_repeat_bound. pa_lt_olte_prioritylayerA_repeat_bound + S pa_i_olte_prioritylayerA_repeat = S (S (k))) -> (((exists pa_h_olte_prioritylayerA_repeat_decoded. pa_h_olte_prioritylayerA_repeat_decoded + S (a) = S ((S (pa_i_olte_prioritylayerA_repeat)) * pa_c_olte_prioritylayerA)) /\ exists pa_q_olte_prioritylayerA_repeat_decoded. pa_b_olte_prioritylayerA = pa_q_olte_prioritylayerA_repeat_decoded * S ((S (pa_i_olte_prioritylayerA_repeat)) * pa_c_olte_prioritylayerA) + (a)))) /\ (exists pa_u_olte_prioritylayerA_product pa_v_olte_prioritylayerA_product. ((((exists pa_h_olte_prioritylayerA_product_start. pa_h_olte_prioritylayerA_product_start + S (1) = S ((S (0)) * pa_v_olte_prioritylayerA_product)) /\ exists pa_q_olte_prioritylayerA_product_start. pa_u_olte_prioritylayerA_product = pa_q_olte_prioritylayerA_product_start * S ((S (0)) * pa_v_olte_prioritylayerA_product) + (1))) /\ ((((exists pa_h_olte_prioritylayerA_product_terminal. pa_h_olte_prioritylayerA_product_terminal + S (A) = S ((S (S (S (k)))) * pa_v_olte_prioritylayerA_product)) /\ exists pa_q_olte_prioritylayerA_product_terminal. pa_u_olte_prioritylayerA_product = pa_q_olte_prioritylayerA_product_terminal * S ((S (S (S (k)))) * pa_v_olte_prioritylayerA_product) + (A))) /\ forall pa_i_olte_prioritylayerA_product. (exists pa_lt_olte_prioritylayerA_product_bound. pa_lt_olte_prioritylayerA_product_bound + S pa_i_olte_prioritylayerA_product = S (S (k))) -> exists pa_p_olte_prioritylayerA_product pa_r_olte_prioritylayerA_product pa_s_olte_prioritylayerA_product. ((((exists pa_h_olte_prioritylayerA_product_factor. pa_h_olte_prioritylayerA_product_factor + S (pa_p_olte_prioritylayerA_product) = S ((S (pa_i_olte_prioritylayerA_product)) * pa_c_olte_prioritylayerA)) /\ exists pa_q_olte_prioritylayerA_product_factor. pa_b_olte_prioritylayerA = pa_q_olte_prioritylayerA_product_factor * S ((S (pa_i_olte_prioritylayerA_product)) * pa_c_olte_prioritylayerA) + (pa_p_olte_prioritylayerA_product))) /\ ((((exists pa_h_olte_prioritylayerA_product_partial. pa_h_olte_prioritylayerA_product_partial + S (pa_r_olte_prioritylayerA_product) = S ((S (pa_i_olte_prioritylayerA_product)) * pa_v_olte_prioritylayerA_product)) /\ exists pa_q_olte_prioritylayerA_product_partial. pa_u_olte_prioritylayerA_product = pa_q_olte_prioritylayerA_product_partial * S ((S (pa_i_olte_prioritylayerA_product)) * pa_v_olte_prioritylayerA_product) + (pa_r_olte_prioritylayerA_product))) /\ ((((exists pa_h_olte_prioritylayerA_product_successor. pa_h_olte_prioritylayerA_product_successor + S (pa_s_olte_prioritylayerA_product) = S ((S (S pa_i_olte_prioritylayerA_product)) * pa_v_olte_prioritylayerA_product)) /\ exists pa_q_olte_prioritylayerA_product_successor. pa_u_olte_prioritylayerA_product = pa_q_olte_prioritylayerA_product_successor * S ((S (S pa_i_olte_prioritylayerA_product)) * pa_v_olte_prioritylayerA_product) + (pa_s_olte_prioritylayerA_product))) /\ pa_s_olte_prioritylayerA_product = pa_r_olte_prioritylayerA_product * pa_p_olte_prioritylayerA_product)))))))) /\ (((exists pa_b_olte_prioritylayerB pa_c_olte_prioritylayerB. ((forall pa_i_olte_prioritylayerB_repeat. (exists pa_lt_olte_prioritylayerB_repeat_bound. pa_lt_olte_prioritylayerB_repeat_bound + S pa_i_olte_prioritylayerB_repeat = S (S (k))) -> (((exists pa_h_olte_prioritylayerB_repeat_decoded. pa_h_olte_prioritylayerB_repeat_decoded + S (b) = S ((S (pa_i_olte_prioritylayerB_repeat)) * pa_c_olte_prioritylayerB)) /\ exists pa_q_olte_prioritylayerB_repeat_decoded. pa_b_olte_prioritylayerB = pa_q_olte_prioritylayerB_repeat_decoded * S ((S (pa_i_olte_prioritylayerB_repeat)) * pa_c_olte_prioritylayerB) + (b)))) /\ (exists pa_u_olte_prioritylayerB_product pa_v_olte_prioritylayerB_product. ((((exists pa_h_olte_prioritylayerB_product_start. pa_h_olte_prioritylayerB_product_start + S (1) = S ((S (0)) * pa_v_olte_prioritylayerB_product)) /\ exists pa_q_olte_prioritylayerB_product_start. pa_u_olte_prioritylayerB_product = pa_q_olte_prioritylayerB_product_start * S ((S (0)) * pa_v_olte_prioritylayerB_product) + (1))) /\ ((((exists pa_h_olte_prioritylayerB_product_terminal. pa_h_olte_prioritylayerB_product_terminal + S (B) = S ((S (S (S (k)))) * pa_v_olte_prioritylayerB_product)) /\ exists pa_q_olte_prioritylayerB_product_terminal. pa_u_olte_prioritylayerB_product = pa_q_olte_prioritylayerB_product_terminal * S ((S (S (S (k)))) * pa_v_olte_prioritylayerB_product) + (B))) /\ forall pa_i_olte_prioritylayerB_product. (exists pa_lt_olte_prioritylayerB_product_bound. pa_lt_olte_prioritylayerB_product_bound + S pa_i_olte_prioritylayerB_product = S (S (k))) -> exists pa_p_olte_prioritylayerB_product pa_r_olte_prioritylayerB_product pa_s_olte_prioritylayerB_product. ((((exists pa_h_olte_prioritylayerB_product_factor. pa_h_olte_prioritylayerB_product_factor + S (pa_p_olte_prioritylayerB_product) = S ((S (pa_i_olte_prioritylayerB_product)) * pa_c_olte_prioritylayerB)) /\ exists pa_q_olte_prioritylayerB_product_factor. pa_b_olte_prioritylayerB = pa_q_olte_prioritylayerB_product_factor * S ((S (pa_i_olte_prioritylayerB_product)) * pa_c_olte_prioritylayerB) + (pa_p_olte_prioritylayerB_product))) /\ ((((exists pa_h_olte_prioritylayerB_product_partial. pa_h_olte_prioritylayerB_product_partial + S (pa_r_olte_prioritylayerB_product) = S ((S (pa_i_olte_prioritylayerB_product)) * pa_v_olte_prioritylayerB_product)) /\ exists pa_q_olte_prioritylayerB_product_partial. pa_u_olte_prioritylayerB_product = pa_q_olte_prioritylayerB_product_partial * S ((S (pa_i_olte_prioritylayerB_product)) * pa_v_olte_prioritylayerB_product) + (pa_r_olte_prioritylayerB_product))) /\ ((((exists pa_h_olte_prioritylayerB_product_successor. pa_h_olte_prioritylayerB_product_successor + S (pa_s_olte_prioritylayerB_product) = S ((S (S pa_i_olte_prioritylayerB_product)) * pa_v_olte_prioritylayerB_product)) /\ exists pa_q_olte_prioritylayerB_product_successor. pa_u_olte_prioritylayerB_product = pa_q_olte_prioritylayerB_product_successor * S ((S (S pa_i_olte_prioritylayerB_product)) * pa_v_olte_prioritylayerB_product) + (pa_s_olte_prioritylayerB_product))) /\ pa_s_olte_prioritylayerB_product = pa_r_olte_prioritylayerB_product * pa_p_olte_prioritylayerB_product)))))))) /\ (((exists pa_b_olte_prioritylayerR pa_c_olte_prioritylayerR. ((forall pa_i_olte_prioritylayerR_repeat. (exists pa_lt_olte_prioritylayerR_repeat_bound. pa_lt_olte_prioritylayerR_repeat_bound + S pa_i_olte_prioritylayerR_repeat = S (k)) -> (((exists pa_h_olte_prioritylayerR_repeat_decoded. pa_h_olte_prioritylayerR_repeat_decoded + S (b) = S ((S (pa_i_olte_prioritylayerR_repeat)) * pa_c_olte_prioritylayerR)) /\ exists pa_q_olte_prioritylayerR_repeat_decoded. pa_b_olte_prioritylayerR = pa_q_olte_prioritylayerR_repeat_decoded * S ((S (pa_i_olte_prioritylayerR_repeat)) * pa_c_olte_prioritylayerR) + (b)))) /\ (exists pa_u_olte_prioritylayerR_product pa_v_olte_prioritylayerR_product. ((((exists pa_h_olte_prioritylayerR_product_start. pa_h_olte_prioritylayerR_product_start + S (1) = S ((S (0)) * pa_v_olte_prioritylayerR_product)) /\ exists pa_q_olte_prioritylayerR_product_start. pa_u_olte_prioritylayerR_product = pa_q_olte_prioritylayerR_product_start * S ((S (0)) * pa_v_olte_prioritylayerR_product) + (1))) /\ ((((exists pa_h_olte_prioritylayerR_product_terminal. pa_h_olte_prioritylayerR_product_terminal + S (R) = S ((S (S (k))) * pa_v_olte_prioritylayerR_product)) /\ exists pa_q_olte_prioritylayerR_product_terminal. pa_u_olte_prioritylayerR_product = pa_q_olte_prioritylayerR_product_terminal * S ((S (S (k))) * pa_v_olte_prioritylayerR_product) + (R))) /\ forall pa_i_olte_prioritylayerR_product. (exists pa_lt_olte_prioritylayerR_product_bound. pa_lt_olte_prioritylayerR_product_bound + S pa_i_olte_prioritylayerR_product = S (k)) -> exists pa_p_olte_prioritylayerR_product pa_r_olte_prioritylayerR_product pa_s_olte_prioritylayerR_product. ((((exists pa_h_olte_prioritylayerR_product_factor. pa_h_olte_prioritylayerR_product_factor + S (pa_p_olte_prioritylayerR_product) = S ((S (pa_i_olte_prioritylayerR_product)) * pa_c_olte_prioritylayerR)) /\ exists pa_q_olte_prioritylayerR_product_factor. pa_b_olte_prioritylayerR = pa_q_olte_prioritylayerR_product_factor * S ((S (pa_i_olte_prioritylayerR_product)) * pa_c_olte_prioritylayerR) + (pa_p_olte_prioritylayerR_product))) /\ ((((exists pa_h_olte_prioritylayerR_product_partial. pa_h_olte_prioritylayerR_product_partial + S (pa_r_olte_prioritylayerR_product) = S ((S (pa_i_olte_prioritylayerR_product)) * pa_v_olte_prioritylayerR_product)) /\ exists pa_q_olte_prioritylayerR_product_partial. pa_u_olte_prioritylayerR_product = pa_q_olte_prioritylayerR_product_partial * S ((S (pa_i_olte_prioritylayerR_product)) * pa_v_olte_prioritylayerR_product) + (pa_r_olte_prioritylayerR_product))) /\ ((((exists pa_h_olte_prioritylayerR_product_successor. pa_h_olte_prioritylayerR_product_successor + S (pa_s_olte_prioritylayerR_product) = S ((S (S pa_i_olte_prioritylayerR_product)) * pa_v_olte_prioritylayerR_product)) /\ exists pa_q_olte_prioritylayerR_product_successor. pa_u_olte_prioritylayerR_product = pa_q_olte_prioritylayerR_product_successor * S ((S (S pa_i_olte_prioritylayerR_product)) * pa_v_olte_prioritylayerR_product) + (pa_s_olte_prioritylayerR_product))) /\ pa_s_olte_prioritylayerR_product = pa_r_olte_prioritylayerR_product * pa_p_olte_prioritylayerR_product)))))))) /\ (((exists pa_b_olte_prioritylayerT pa_c_olte_prioritylayerT. ((forall pa_i_olte_prioritylayerT_repeat. (exists pa_lt_olte_prioritylayerT_repeat_bound. pa_lt_olte_prioritylayerT_repeat_bound + S pa_i_olte_prioritylayerT_repeat = k) -> (((exists pa_h_olte_prioritylayerT_repeat_decoded. pa_h_olte_prioritylayerT_repeat_decoded + S (b) = S ((S (pa_i_olte_prioritylayerT_repeat)) * pa_c_olte_prioritylayerT)) /\ exists pa_q_olte_prioritylayerT_repeat_decoded. pa_b_olte_prioritylayerT = pa_q_olte_prioritylayerT_repeat_decoded * S ((S (pa_i_olte_prioritylayerT_repeat)) * pa_c_olte_prioritylayerT) + (b)))) /\ (exists pa_u_olte_prioritylayerT_product pa_v_olte_prioritylayerT_product. ((((exists pa_h_olte_prioritylayerT_product_start. pa_h_olte_prioritylayerT_product_start + S (1) = S ((S (0)) * pa_v_olte_prioritylayerT_product)) /\ exists pa_q_olte_prioritylayerT_product_start. pa_u_olte_prioritylayerT_product = pa_q_olte_prioritylayerT_product_start * S ((S (0)) * pa_v_olte_prioritylayerT_product) + (1))) /\ ((((exists pa_h_olte_prioritylayerT_product_terminal. pa_h_olte_prioritylayerT_product_terminal + S (T) = S ((S (k)) * pa_v_olte_prioritylayerT_product)) /\ exists pa_q_olte_prioritylayerT_product_terminal. pa_u_olte_prioritylayerT_product = pa_q_olte_prioritylayerT_product_terminal * S ((S (k)) * pa_v_olte_prioritylayerT_product) + (T))) /\ forall pa_i_olte_prioritylayerT_product. (exists pa_lt_olte_prioritylayerT_product_bound. pa_lt_olte_prioritylayerT_product_bound + S pa_i_olte_prioritylayerT_product = k) -> exists pa_p_olte_prioritylayerT_product pa_r_olte_prioritylayerT_product pa_s_olte_prioritylayerT_product. ((((exists pa_h_olte_prioritylayerT_product_factor. pa_h_olte_prioritylayerT_product_factor + S (pa_p_olte_prioritylayerT_product) = S ((S (pa_i_olte_prioritylayerT_product)) * pa_c_olte_prioritylayerT)) /\ exists pa_q_olte_prioritylayerT_product_factor. pa_b_olte_prioritylayerT = pa_q_olte_prioritylayerT_product_factor * S ((S (pa_i_olte_prioritylayerT_product)) * pa_c_olte_prioritylayerT) + (pa_p_olte_prioritylayerT_product))) /\ ((((exists pa_h_olte_prioritylayerT_product_partial. pa_h_olte_prioritylayerT_product_partial + S (pa_r_olte_prioritylayerT_product) = S ((S (pa_i_olte_prioritylayerT_product)) * pa_v_olte_prioritylayerT_product)) /\ exists pa_q_olte_prioritylayerT_product_partial. pa_u_olte_prioritylayerT_product = pa_q_olte_prioritylayerT_product_partial * S ((S (pa_i_olte_prioritylayerT_product)) * pa_v_olte_prioritylayerT_product) + (pa_r_olte_prioritylayerT_product))) /\ ((((exists pa_h_olte_prioritylayerT_product_successor. pa_h_olte_prioritylayerT_product_successor + S (pa_s_olte_prioritylayerT_product) = S ((S (S pa_i_olte_prioritylayerT_product)) * pa_v_olte_prioritylayerT_product)) /\ exists pa_q_olte_prioritylayerT_product_successor. pa_u_olte_prioritylayerT_product = pa_q_olte_prioritylayerT_product_successor * S ((S (S pa_i_olte_prioritylayerT_product)) * pa_v_olte_prioritylayerT_product) + (pa_s_olte_prioritylayerT_product))) /\ pa_s_olte_prioritylayerT_product = pa_r_olte_prioritylayerT_product * pa_p_olte_prioritylayerT_product)))))))) /\ ((((A) = (B) + (d) * (Q)) /\ ((((Q) = S (S (k)) * (R) + (d) * (C)) /\ (2 * (C) = (S (S (k)) * S (k)) * (T) + (d) * (H)))))))))))))

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