SignedDotProduct(ab,ac,db,dc,eb,ec,fb,fc,l,p,n)

Hygienic expanded first-order definition

exists ff_pp_mcp_signed_advanced ff_nn_mcp_signed_advanced ff_pn_mcp_signed_advanced ff_np_mcp_signed_advanced. ((exists ff_code_dot_mcp_advanced_pp ff_scale_dot_mcp_advanced_pp. ((forall fpmp_index_dot_mcp_advanced_pp_pointwise fpmp_left_dot_mcp_advanced_pp_pointwise fpmp_right_dot_mcp_advanced_pp_pointwise fpmp_target_dot_mcp_advanced_pp_pointwise. (exists fpmp_gap_dot_mcp_advanced_pp_pointwise. fpmp_gap_dot_mcp_advanced_pp_pointwise + S fpmp_index_dot_mcp_advanced_pp_pointwise = l) -> (((exists ff_h_fpmp_dot_mcp_advanced_pp_pointwise_left. ff_h_fpmp_dot_mcp_advanced_pp_pointwise_left + S (fpmp_left_dot_mcp_advanced_pp_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ac)) /\ exists ff_q_fpmp_dot_mcp_advanced_pp_pointwise_left. ab = ff_q_fpmp_dot_mcp_advanced_pp_pointwise_left * S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ac) + (fpmp_left_dot_mcp_advanced_pp_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_pp_pointwise_right. ff_h_fpmp_dot_mcp_advanced_pp_pointwise_right + S (fpmp_right_dot_mcp_advanced_pp_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ec)) /\ exists ff_q_fpmp_dot_mcp_advanced_pp_pointwise_right. eb = ff_q_fpmp_dot_mcp_advanced_pp_pointwise_right * S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ec) + (fpmp_right_dot_mcp_advanced_pp_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_pp_pointwise_target. ff_h_fpmp_dot_mcp_advanced_pp_pointwise_target + S (fpmp_target_dot_mcp_advanced_pp_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ff_scale_dot_mcp_advanced_pp)) /\ exists ff_q_fpmp_dot_mcp_advanced_pp_pointwise_target. ff_code_dot_mcp_advanced_pp = ff_q_fpmp_dot_mcp_advanced_pp_pointwise_target * S ((S (fpmp_index_dot_mcp_advanced_pp_pointwise)) * ff_scale_dot_mcp_advanced_pp) + (fpmp_target_dot_mcp_advanced_pp_pointwise))) -> fpmp_target_dot_mcp_advanced_pp_pointwise = fpmp_left_dot_mcp_advanced_pp_pointwise * fpmp_right_dot_mcp_advanced_pp_pointwise) /\ (exists ff_u_dot_mcp_advanced_pp_sum ff_v_dot_mcp_advanced_pp_sum. ((((exists ff_h_dot_mcp_advanced_pp_sum_start. ff_h_dot_mcp_advanced_pp_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_advanced_pp_sum)) /\ exists ff_q_dot_mcp_advanced_pp_sum_start. ff_u_dot_mcp_advanced_pp_sum = ff_q_dot_mcp_advanced_pp_sum_start * S ((S (0)) * ff_v_dot_mcp_advanced_pp_sum) + (0))) /\ ((((exists ff_h_dot_mcp_advanced_pp_sum_terminal. ff_h_dot_mcp_advanced_pp_sum_terminal + S (ff_pp_mcp_signed_advanced) = S ((S (l)) * ff_v_dot_mcp_advanced_pp_sum)) /\ exists ff_q_dot_mcp_advanced_pp_sum_terminal. ff_u_dot_mcp_advanced_pp_sum = ff_q_dot_mcp_advanced_pp_sum_terminal * S ((S (l)) * ff_v_dot_mcp_advanced_pp_sum) + (ff_pp_mcp_signed_advanced))) /\ forall ff_i_dot_mcp_advanced_pp_sum. (exists ff_lt_dot_mcp_advanced_pp_sum_bound. ff_lt_dot_mcp_advanced_pp_sum_bound + S ff_i_dot_mcp_advanced_pp_sum = l) -> exists ff_a_dot_mcp_advanced_pp_sum ff_r_dot_mcp_advanced_pp_sum ff_s_dot_mcp_advanced_pp_sum. ((((exists ff_h_dot_mcp_advanced_pp_sum_summand. ff_h_dot_mcp_advanced_pp_sum_summand + S (ff_a_dot_mcp_advanced_pp_sum) = S ((S (ff_i_dot_mcp_advanced_pp_sum)) * ff_scale_dot_mcp_advanced_pp)) /\ exists ff_q_dot_mcp_advanced_pp_sum_summand. ff_code_dot_mcp_advanced_pp = ff_q_dot_mcp_advanced_pp_sum_summand * S ((S (ff_i_dot_mcp_advanced_pp_sum)) * ff_scale_dot_mcp_advanced_pp) + (ff_a_dot_mcp_advanced_pp_sum))) /\ ((((exists ff_h_dot_mcp_advanced_pp_sum_partial. ff_h_dot_mcp_advanced_pp_sum_partial + S (ff_r_dot_mcp_advanced_pp_sum) = S ((S (ff_i_dot_mcp_advanced_pp_sum)) * ff_v_dot_mcp_advanced_pp_sum)) /\ exists ff_q_dot_mcp_advanced_pp_sum_partial. ff_u_dot_mcp_advanced_pp_sum = ff_q_dot_mcp_advanced_pp_sum_partial * S ((S (ff_i_dot_mcp_advanced_pp_sum)) * ff_v_dot_mcp_advanced_pp_sum) + (ff_r_dot_mcp_advanced_pp_sum))) /\ ((((exists ff_h_dot_mcp_advanced_pp_sum_successor. ff_h_dot_mcp_advanced_pp_sum_successor + S (ff_s_dot_mcp_advanced_pp_sum) = S ((S (S ff_i_dot_mcp_advanced_pp_sum)) * ff_v_dot_mcp_advanced_pp_sum)) /\ exists ff_q_dot_mcp_advanced_pp_sum_successor. ff_u_dot_mcp_advanced_pp_sum = ff_q_dot_mcp_advanced_pp_sum_successor * S ((S (S ff_i_dot_mcp_advanced_pp_sum)) * ff_v_dot_mcp_advanced_pp_sum) + (ff_s_dot_mcp_advanced_pp_sum))) /\ ff_s_dot_mcp_advanced_pp_sum = ff_r_dot_mcp_advanced_pp_sum + ff_a_dot_mcp_advanced_pp_sum)))))))) /\ ((exists ff_code_dot_mcp_advanced_nn ff_scale_dot_mcp_advanced_nn. ((forall fpmp_index_dot_mcp_advanced_nn_pointwise fpmp_left_dot_mcp_advanced_nn_pointwise fpmp_right_dot_mcp_advanced_nn_pointwise fpmp_target_dot_mcp_advanced_nn_pointwise. (exists fpmp_gap_dot_mcp_advanced_nn_pointwise. fpmp_gap_dot_mcp_advanced_nn_pointwise + S fpmp_index_dot_mcp_advanced_nn_pointwise = l) -> (((exists ff_h_fpmp_dot_mcp_advanced_nn_pointwise_left. ff_h_fpmp_dot_mcp_advanced_nn_pointwise_left + S (fpmp_left_dot_mcp_advanced_nn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * dc)) /\ exists ff_q_fpmp_dot_mcp_advanced_nn_pointwise_left. db = ff_q_fpmp_dot_mcp_advanced_nn_pointwise_left * S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * dc) + (fpmp_left_dot_mcp_advanced_nn_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_nn_pointwise_right. ff_h_fpmp_dot_mcp_advanced_nn_pointwise_right + S (fpmp_right_dot_mcp_advanced_nn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * fc)) /\ exists ff_q_fpmp_dot_mcp_advanced_nn_pointwise_right. fb = ff_q_fpmp_dot_mcp_advanced_nn_pointwise_right * S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * fc) + (fpmp_right_dot_mcp_advanced_nn_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_nn_pointwise_target. ff_h_fpmp_dot_mcp_advanced_nn_pointwise_target + S (fpmp_target_dot_mcp_advanced_nn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * ff_scale_dot_mcp_advanced_nn)) /\ exists ff_q_fpmp_dot_mcp_advanced_nn_pointwise_target. ff_code_dot_mcp_advanced_nn = ff_q_fpmp_dot_mcp_advanced_nn_pointwise_target * S ((S (fpmp_index_dot_mcp_advanced_nn_pointwise)) * ff_scale_dot_mcp_advanced_nn) + (fpmp_target_dot_mcp_advanced_nn_pointwise))) -> fpmp_target_dot_mcp_advanced_nn_pointwise = fpmp_left_dot_mcp_advanced_nn_pointwise * fpmp_right_dot_mcp_advanced_nn_pointwise) /\ (exists ff_u_dot_mcp_advanced_nn_sum ff_v_dot_mcp_advanced_nn_sum. ((((exists ff_h_dot_mcp_advanced_nn_sum_start. ff_h_dot_mcp_advanced_nn_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_advanced_nn_sum)) /\ exists ff_q_dot_mcp_advanced_nn_sum_start. ff_u_dot_mcp_advanced_nn_sum = ff_q_dot_mcp_advanced_nn_sum_start * S ((S (0)) * ff_v_dot_mcp_advanced_nn_sum) + (0))) /\ ((((exists ff_h_dot_mcp_advanced_nn_sum_terminal. ff_h_dot_mcp_advanced_nn_sum_terminal + S (ff_nn_mcp_signed_advanced) = S ((S (l)) * ff_v_dot_mcp_advanced_nn_sum)) /\ exists ff_q_dot_mcp_advanced_nn_sum_terminal. ff_u_dot_mcp_advanced_nn_sum = ff_q_dot_mcp_advanced_nn_sum_terminal * S ((S (l)) * ff_v_dot_mcp_advanced_nn_sum) + (ff_nn_mcp_signed_advanced))) /\ forall ff_i_dot_mcp_advanced_nn_sum. (exists ff_lt_dot_mcp_advanced_nn_sum_bound. ff_lt_dot_mcp_advanced_nn_sum_bound + S ff_i_dot_mcp_advanced_nn_sum = l) -> exists ff_a_dot_mcp_advanced_nn_sum ff_r_dot_mcp_advanced_nn_sum ff_s_dot_mcp_advanced_nn_sum. ((((exists ff_h_dot_mcp_advanced_nn_sum_summand. ff_h_dot_mcp_advanced_nn_sum_summand + S (ff_a_dot_mcp_advanced_nn_sum) = S ((S (ff_i_dot_mcp_advanced_nn_sum)) * ff_scale_dot_mcp_advanced_nn)) /\ exists ff_q_dot_mcp_advanced_nn_sum_summand. ff_code_dot_mcp_advanced_nn = ff_q_dot_mcp_advanced_nn_sum_summand * S ((S (ff_i_dot_mcp_advanced_nn_sum)) * ff_scale_dot_mcp_advanced_nn) + (ff_a_dot_mcp_advanced_nn_sum))) /\ ((((exists ff_h_dot_mcp_advanced_nn_sum_partial. ff_h_dot_mcp_advanced_nn_sum_partial + S (ff_r_dot_mcp_advanced_nn_sum) = S ((S (ff_i_dot_mcp_advanced_nn_sum)) * ff_v_dot_mcp_advanced_nn_sum)) /\ exists ff_q_dot_mcp_advanced_nn_sum_partial. ff_u_dot_mcp_advanced_nn_sum = ff_q_dot_mcp_advanced_nn_sum_partial * S ((S (ff_i_dot_mcp_advanced_nn_sum)) * ff_v_dot_mcp_advanced_nn_sum) + (ff_r_dot_mcp_advanced_nn_sum))) /\ ((((exists ff_h_dot_mcp_advanced_nn_sum_successor. ff_h_dot_mcp_advanced_nn_sum_successor + S (ff_s_dot_mcp_advanced_nn_sum) = S ((S (S ff_i_dot_mcp_advanced_nn_sum)) * ff_v_dot_mcp_advanced_nn_sum)) /\ exists ff_q_dot_mcp_advanced_nn_sum_successor. ff_u_dot_mcp_advanced_nn_sum = ff_q_dot_mcp_advanced_nn_sum_successor * S ((S (S ff_i_dot_mcp_advanced_nn_sum)) * ff_v_dot_mcp_advanced_nn_sum) + (ff_s_dot_mcp_advanced_nn_sum))) /\ ff_s_dot_mcp_advanced_nn_sum = ff_r_dot_mcp_advanced_nn_sum + ff_a_dot_mcp_advanced_nn_sum)))))))) /\ ((exists ff_code_dot_mcp_advanced_pn ff_scale_dot_mcp_advanced_pn. ((forall fpmp_index_dot_mcp_advanced_pn_pointwise fpmp_left_dot_mcp_advanced_pn_pointwise fpmp_right_dot_mcp_advanced_pn_pointwise fpmp_target_dot_mcp_advanced_pn_pointwise. (exists fpmp_gap_dot_mcp_advanced_pn_pointwise. fpmp_gap_dot_mcp_advanced_pn_pointwise + S fpmp_index_dot_mcp_advanced_pn_pointwise = l) -> (((exists ff_h_fpmp_dot_mcp_advanced_pn_pointwise_left. ff_h_fpmp_dot_mcp_advanced_pn_pointwise_left + S (fpmp_left_dot_mcp_advanced_pn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * ac)) /\ exists ff_q_fpmp_dot_mcp_advanced_pn_pointwise_left. ab = ff_q_fpmp_dot_mcp_advanced_pn_pointwise_left * S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * ac) + (fpmp_left_dot_mcp_advanced_pn_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_pn_pointwise_right. ff_h_fpmp_dot_mcp_advanced_pn_pointwise_right + S (fpmp_right_dot_mcp_advanced_pn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * fc)) /\ exists ff_q_fpmp_dot_mcp_advanced_pn_pointwise_right. fb = ff_q_fpmp_dot_mcp_advanced_pn_pointwise_right * S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * fc) + (fpmp_right_dot_mcp_advanced_pn_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_pn_pointwise_target. ff_h_fpmp_dot_mcp_advanced_pn_pointwise_target + S (fpmp_target_dot_mcp_advanced_pn_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * ff_scale_dot_mcp_advanced_pn)) /\ exists ff_q_fpmp_dot_mcp_advanced_pn_pointwise_target. ff_code_dot_mcp_advanced_pn = ff_q_fpmp_dot_mcp_advanced_pn_pointwise_target * S ((S (fpmp_index_dot_mcp_advanced_pn_pointwise)) * ff_scale_dot_mcp_advanced_pn) + (fpmp_target_dot_mcp_advanced_pn_pointwise))) -> fpmp_target_dot_mcp_advanced_pn_pointwise = fpmp_left_dot_mcp_advanced_pn_pointwise * fpmp_right_dot_mcp_advanced_pn_pointwise) /\ (exists ff_u_dot_mcp_advanced_pn_sum ff_v_dot_mcp_advanced_pn_sum. ((((exists ff_h_dot_mcp_advanced_pn_sum_start. ff_h_dot_mcp_advanced_pn_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_advanced_pn_sum)) /\ exists ff_q_dot_mcp_advanced_pn_sum_start. ff_u_dot_mcp_advanced_pn_sum = ff_q_dot_mcp_advanced_pn_sum_start * S ((S (0)) * ff_v_dot_mcp_advanced_pn_sum) + (0))) /\ ((((exists ff_h_dot_mcp_advanced_pn_sum_terminal. ff_h_dot_mcp_advanced_pn_sum_terminal + S (ff_pn_mcp_signed_advanced) = S ((S (l)) * ff_v_dot_mcp_advanced_pn_sum)) /\ exists ff_q_dot_mcp_advanced_pn_sum_terminal. ff_u_dot_mcp_advanced_pn_sum = ff_q_dot_mcp_advanced_pn_sum_terminal * S ((S (l)) * ff_v_dot_mcp_advanced_pn_sum) + (ff_pn_mcp_signed_advanced))) /\ forall ff_i_dot_mcp_advanced_pn_sum. (exists ff_lt_dot_mcp_advanced_pn_sum_bound. ff_lt_dot_mcp_advanced_pn_sum_bound + S ff_i_dot_mcp_advanced_pn_sum = l) -> exists ff_a_dot_mcp_advanced_pn_sum ff_r_dot_mcp_advanced_pn_sum ff_s_dot_mcp_advanced_pn_sum. ((((exists ff_h_dot_mcp_advanced_pn_sum_summand. ff_h_dot_mcp_advanced_pn_sum_summand + S (ff_a_dot_mcp_advanced_pn_sum) = S ((S (ff_i_dot_mcp_advanced_pn_sum)) * ff_scale_dot_mcp_advanced_pn)) /\ exists ff_q_dot_mcp_advanced_pn_sum_summand. ff_code_dot_mcp_advanced_pn = ff_q_dot_mcp_advanced_pn_sum_summand * S ((S (ff_i_dot_mcp_advanced_pn_sum)) * ff_scale_dot_mcp_advanced_pn) + (ff_a_dot_mcp_advanced_pn_sum))) /\ ((((exists ff_h_dot_mcp_advanced_pn_sum_partial. ff_h_dot_mcp_advanced_pn_sum_partial + S (ff_r_dot_mcp_advanced_pn_sum) = S ((S (ff_i_dot_mcp_advanced_pn_sum)) * ff_v_dot_mcp_advanced_pn_sum)) /\ exists ff_q_dot_mcp_advanced_pn_sum_partial. ff_u_dot_mcp_advanced_pn_sum = ff_q_dot_mcp_advanced_pn_sum_partial * S ((S (ff_i_dot_mcp_advanced_pn_sum)) * ff_v_dot_mcp_advanced_pn_sum) + (ff_r_dot_mcp_advanced_pn_sum))) /\ ((((exists ff_h_dot_mcp_advanced_pn_sum_successor. ff_h_dot_mcp_advanced_pn_sum_successor + S (ff_s_dot_mcp_advanced_pn_sum) = S ((S (S ff_i_dot_mcp_advanced_pn_sum)) * ff_v_dot_mcp_advanced_pn_sum)) /\ exists ff_q_dot_mcp_advanced_pn_sum_successor. ff_u_dot_mcp_advanced_pn_sum = ff_q_dot_mcp_advanced_pn_sum_successor * S ((S (S ff_i_dot_mcp_advanced_pn_sum)) * ff_v_dot_mcp_advanced_pn_sum) + (ff_s_dot_mcp_advanced_pn_sum))) /\ ff_s_dot_mcp_advanced_pn_sum = ff_r_dot_mcp_advanced_pn_sum + ff_a_dot_mcp_advanced_pn_sum)))))))) /\ ((exists ff_code_dot_mcp_advanced_np ff_scale_dot_mcp_advanced_np. ((forall fpmp_index_dot_mcp_advanced_np_pointwise fpmp_left_dot_mcp_advanced_np_pointwise fpmp_right_dot_mcp_advanced_np_pointwise fpmp_target_dot_mcp_advanced_np_pointwise. (exists fpmp_gap_dot_mcp_advanced_np_pointwise. fpmp_gap_dot_mcp_advanced_np_pointwise + S fpmp_index_dot_mcp_advanced_np_pointwise = l) -> (((exists ff_h_fpmp_dot_mcp_advanced_np_pointwise_left. ff_h_fpmp_dot_mcp_advanced_np_pointwise_left + S (fpmp_left_dot_mcp_advanced_np_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * dc)) /\ exists ff_q_fpmp_dot_mcp_advanced_np_pointwise_left. db = ff_q_fpmp_dot_mcp_advanced_np_pointwise_left * S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * dc) + (fpmp_left_dot_mcp_advanced_np_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_np_pointwise_right. ff_h_fpmp_dot_mcp_advanced_np_pointwise_right + S (fpmp_right_dot_mcp_advanced_np_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * ec)) /\ exists ff_q_fpmp_dot_mcp_advanced_np_pointwise_right. eb = ff_q_fpmp_dot_mcp_advanced_np_pointwise_right * S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * ec) + (fpmp_right_dot_mcp_advanced_np_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_np_pointwise_target. ff_h_fpmp_dot_mcp_advanced_np_pointwise_target + S (fpmp_target_dot_mcp_advanced_np_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * ff_scale_dot_mcp_advanced_np)) /\ exists ff_q_fpmp_dot_mcp_advanced_np_pointwise_target. ff_code_dot_mcp_advanced_np = ff_q_fpmp_dot_mcp_advanced_np_pointwise_target * S ((S (fpmp_index_dot_mcp_advanced_np_pointwise)) * ff_scale_dot_mcp_advanced_np) + (fpmp_target_dot_mcp_advanced_np_pointwise))) -> fpmp_target_dot_mcp_advanced_np_pointwise = fpmp_left_dot_mcp_advanced_np_pointwise * fpmp_right_dot_mcp_advanced_np_pointwise) /\ (exists ff_u_dot_mcp_advanced_np_sum ff_v_dot_mcp_advanced_np_sum. ((((exists ff_h_dot_mcp_advanced_np_sum_start. ff_h_dot_mcp_advanced_np_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_advanced_np_sum)) /\ exists ff_q_dot_mcp_advanced_np_sum_start. ff_u_dot_mcp_advanced_np_sum = ff_q_dot_mcp_advanced_np_sum_start * S ((S (0)) * ff_v_dot_mcp_advanced_np_sum) + (0))) /\ ((((exists ff_h_dot_mcp_advanced_np_sum_terminal. ff_h_dot_mcp_advanced_np_sum_terminal + S (ff_np_mcp_signed_advanced) = S ((S (l)) * ff_v_dot_mcp_advanced_np_sum)) /\ exists ff_q_dot_mcp_advanced_np_sum_terminal. ff_u_dot_mcp_advanced_np_sum = ff_q_dot_mcp_advanced_np_sum_terminal * S ((S (l)) * ff_v_dot_mcp_advanced_np_sum) + (ff_np_mcp_signed_advanced))) /\ forall ff_i_dot_mcp_advanced_np_sum. (exists ff_lt_dot_mcp_advanced_np_sum_bound. ff_lt_dot_mcp_advanced_np_sum_bound + S ff_i_dot_mcp_advanced_np_sum = l) -> exists ff_a_dot_mcp_advanced_np_sum ff_r_dot_mcp_advanced_np_sum ff_s_dot_mcp_advanced_np_sum. ((((exists ff_h_dot_mcp_advanced_np_sum_summand. ff_h_dot_mcp_advanced_np_sum_summand + S (ff_a_dot_mcp_advanced_np_sum) = S ((S (ff_i_dot_mcp_advanced_np_sum)) * ff_scale_dot_mcp_advanced_np)) /\ exists ff_q_dot_mcp_advanced_np_sum_summand. ff_code_dot_mcp_advanced_np = ff_q_dot_mcp_advanced_np_sum_summand * S ((S (ff_i_dot_mcp_advanced_np_sum)) * ff_scale_dot_mcp_advanced_np) + (ff_a_dot_mcp_advanced_np_sum))) /\ ((((exists ff_h_dot_mcp_advanced_np_sum_partial. ff_h_dot_mcp_advanced_np_sum_partial + S (ff_r_dot_mcp_advanced_np_sum) = S ((S (ff_i_dot_mcp_advanced_np_sum)) * ff_v_dot_mcp_advanced_np_sum)) /\ exists ff_q_dot_mcp_advanced_np_sum_partial. ff_u_dot_mcp_advanced_np_sum = ff_q_dot_mcp_advanced_np_sum_partial * S ((S (ff_i_dot_mcp_advanced_np_sum)) * ff_v_dot_mcp_advanced_np_sum) + (ff_r_dot_mcp_advanced_np_sum))) /\ ((((exists ff_h_dot_mcp_advanced_np_sum_successor. ff_h_dot_mcp_advanced_np_sum_successor + S (ff_s_dot_mcp_advanced_np_sum) = S ((S (S ff_i_dot_mcp_advanced_np_sum)) * ff_v_dot_mcp_advanced_np_sum)) /\ exists ff_q_dot_mcp_advanced_np_sum_successor. ff_u_dot_mcp_advanced_np_sum = ff_q_dot_mcp_advanced_np_sum_successor * S ((S (S ff_i_dot_mcp_advanced_np_sum)) * ff_v_dot_mcp_advanced_np_sum) + (ff_s_dot_mcp_advanced_np_sum))) /\ ff_s_dot_mcp_advanced_np_sum = ff_r_dot_mcp_advanced_np_sum + ff_a_dot_mcp_advanced_np_sum)))))))) /\ (p = ff_pp_mcp_signed_advanced + ff_nn_mcp_signed_advanced /\ n = ff_pn_mcp_signed_advanced + ff_np_mcp_signed_advanced)))))

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

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition