SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n)

Hygienic expanded first-order definition

exists ff_ab_mce_row_breakthrough ff_ac_mce_row_breakthrough ff_db_mce_row_breakthrough ff_dc_mce_row_breakthrough. ((forall ff_index_mcp_mce_breakthrough_positive ff_source_mcp_mce_breakthrough_positive ff_target_mcp_mce_breakthrough_positive. (exists mcp_gap_mce_breakthrough_positive_bound. mcp_gap_mce_breakthrough_positive_bound + S (ff_index_mcp_mce_breakthrough_positive) = (S (q))) -> (((exists fs_h_mcp_mce_breakthrough_positive_source. fs_h_mcp_mce_breakthrough_positive_source + S (ff_source_mcp_mce_breakthrough_positive) = S ((S ((0) + (1) * ff_index_mcp_mce_breakthrough_positive)) * pc)) /\ exists fs_q_mcp_mce_breakthrough_positive_source. pb = fs_q_mcp_mce_breakthrough_positive_source * S ((S ((0) + (1) * ff_index_mcp_mce_breakthrough_positive)) * pc) + (ff_source_mcp_mce_breakthrough_positive))) -> (((exists fs_h_mcp_mce_breakthrough_positive_target. fs_h_mcp_mce_breakthrough_positive_target + S (ff_target_mcp_mce_breakthrough_positive) = S ((S (ff_index_mcp_mce_breakthrough_positive)) * ff_ac_mce_row_breakthrough)) /\ exists fs_q_mcp_mce_breakthrough_positive_target. ff_ab_mce_row_breakthrough = fs_q_mcp_mce_breakthrough_positive_target * S ((S (ff_index_mcp_mce_breakthrough_positive)) * ff_ac_mce_row_breakthrough) + (ff_target_mcp_mce_breakthrough_positive))) -> ff_target_mcp_mce_breakthrough_positive = ff_source_mcp_mce_breakthrough_positive) /\ ((forall ff_index_mcp_mce_breakthrough_negative ff_source_mcp_mce_breakthrough_negative ff_target_mcp_mce_breakthrough_negative. (exists mcp_gap_mce_breakthrough_negative_bound. mcp_gap_mce_breakthrough_negative_bound + S (ff_index_mcp_mce_breakthrough_negative) = (S (q))) -> (((exists fs_h_mcp_mce_breakthrough_negative_source. fs_h_mcp_mce_breakthrough_negative_source + S (ff_source_mcp_mce_breakthrough_negative) = S ((S ((0) + (1) * ff_index_mcp_mce_breakthrough_negative)) * nc)) /\ exists fs_q_mcp_mce_breakthrough_negative_source. nb = fs_q_mcp_mce_breakthrough_negative_source * S ((S ((0) + (1) * ff_index_mcp_mce_breakthrough_negative)) * nc) + (ff_source_mcp_mce_breakthrough_negative))) -> (((exists fs_h_mcp_mce_breakthrough_negative_target. fs_h_mcp_mce_breakthrough_negative_target + S (ff_target_mcp_mce_breakthrough_negative) = S ((S (ff_index_mcp_mce_breakthrough_negative)) * ff_dc_mce_row_breakthrough)) /\ exists fs_q_mcp_mce_breakthrough_negative_target. ff_db_mce_row_breakthrough = fs_q_mcp_mce_breakthrough_negative_target * S ((S (ff_index_mcp_mce_breakthrough_negative)) * ff_dc_mce_row_breakthrough) + (ff_target_mcp_mce_breakthrough_negative))) -> ff_target_mcp_mce_breakthrough_negative = ff_source_mcp_mce_breakthrough_negative) /\ (exists ff_ub_mce_fold_breakthrough_fold ff_uc_mce_fold_breakthrough_fold ff_vb_mce_fold_breakthrough_fold ff_vc_mce_fold_breakthrough_fold. ((forall ff_index_mce_alternating_breakthrough_fold_prefix. (exists ff_gap_mce_breakthrough_fold_prefix_index. ff_gap_mce_breakthrough_fold_prefix_index + S (ff_index_mce_alternating_breakthrough_fold_prefix) = (S (q))) -> exists ff_ap_mce_alternating_breakthrough_fold_prefix ff_an_mce_alternating_breakthrough_fold_prefix ff_bp_mce_alternating_breakthrough_fold_prefix ff_bn_mce_alternating_breakthrough_fold_prefix ff_p_mce_alternating_breakthrough_fold_prefix ff_n_mce_alternating_breakthrough_fold_prefix. ((((exists ff_h_mce_breakthrough_fold_prefix_ap. ff_h_mce_breakthrough_fold_prefix_ap + S (ff_ap_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_ac_mce_row_breakthrough)) /\ exists ff_q_mce_breakthrough_fold_prefix_ap. ff_ab_mce_row_breakthrough = ff_q_mce_breakthrough_fold_prefix_ap * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_ac_mce_row_breakthrough) + (ff_ap_mce_alternating_breakthrough_fold_prefix))) /\ ((((exists ff_h_mce_breakthrough_fold_prefix_an. ff_h_mce_breakthrough_fold_prefix_an + S (ff_an_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_dc_mce_row_breakthrough)) /\ exists ff_q_mce_breakthrough_fold_prefix_an. ff_db_mce_row_breakthrough = ff_q_mce_breakthrough_fold_prefix_an * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_dc_mce_row_breakthrough) + (ff_an_mce_alternating_breakthrough_fold_prefix))) /\ ((((exists ff_h_mce_breakthrough_fold_prefix_bp. ff_h_mce_breakthrough_fold_prefix_bp + S (ff_bp_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ec)) /\ exists ff_q_mce_breakthrough_fold_prefix_bp. eb = ff_q_mce_breakthrough_fold_prefix_bp * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ec) + (ff_bp_mce_alternating_breakthrough_fold_prefix))) /\ ((((exists ff_h_mce_breakthrough_fold_prefix_bn. ff_h_mce_breakthrough_fold_prefix_bn + S (ff_bn_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * fc)) /\ exists ff_q_mce_breakthrough_fold_prefix_bn. fb = ff_q_mce_breakthrough_fold_prefix_bn * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * fc) + (ff_bn_mce_alternating_breakthrough_fold_prefix))) /\ ((((exists ff_h_mce_breakthrough_fold_prefix_positive. ff_h_mce_breakthrough_fold_prefix_positive + S (ff_p_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_uc_mce_fold_breakthrough_fold)) /\ exists ff_q_mce_breakthrough_fold_prefix_positive. ff_ub_mce_fold_breakthrough_fold = ff_q_mce_breakthrough_fold_prefix_positive * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_uc_mce_fold_breakthrough_fold) + (ff_p_mce_alternating_breakthrough_fold_prefix))) /\ ((((exists ff_h_mce_breakthrough_fold_prefix_negative. ff_h_mce_breakthrough_fold_prefix_negative + S (ff_n_mce_alternating_breakthrough_fold_prefix) = S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_vc_mce_fold_breakthrough_fold)) /\ exists ff_q_mce_breakthrough_fold_prefix_negative. ff_vb_mce_fold_breakthrough_fold = ff_q_mce_breakthrough_fold_prefix_negative * S ((S (ff_index_mce_alternating_breakthrough_fold_prefix)) * ff_vc_mce_fold_breakthrough_fold) + (ff_n_mce_alternating_breakthrough_fold_prefix))) /\ (((exists ff_even_mce_term_breakthrough_fold_prefix_term. ff_index_mce_alternating_breakthrough_fold_prefix = 2 * ff_even_mce_term_breakthrough_fold_prefix_term) /\ (ff_p_mce_alternating_breakthrough_fold_prefix = (ff_ap_mce_alternating_breakthrough_fold_prefix) * (ff_bp_mce_alternating_breakthrough_fold_prefix) + (ff_an_mce_alternating_breakthrough_fold_prefix) * (ff_bn_mce_alternating_breakthrough_fold_prefix) /\ ff_n_mce_alternating_breakthrough_fold_prefix = (ff_ap_mce_alternating_breakthrough_fold_prefix) * (ff_bn_mce_alternating_breakthrough_fold_prefix) + (ff_an_mce_alternating_breakthrough_fold_prefix) * (ff_bp_mce_alternating_breakthrough_fold_prefix))) \/ ((exists ff_odd_mce_term_breakthrough_fold_prefix_term. ff_index_mce_alternating_breakthrough_fold_prefix = 2 * ff_odd_mce_term_breakthrough_fold_prefix_term + 1) /\ (ff_p_mce_alternating_breakthrough_fold_prefix = (ff_ap_mce_alternating_breakthrough_fold_prefix) * (ff_bn_mce_alternating_breakthrough_fold_prefix) + (ff_an_mce_alternating_breakthrough_fold_prefix) * (ff_bp_mce_alternating_breakthrough_fold_prefix) /\ ff_n_mce_alternating_breakthrough_fold_prefix = (ff_ap_mce_alternating_breakthrough_fold_prefix) * (ff_bp_mce_alternating_breakthrough_fold_prefix) + (ff_an_mce_alternating_breakthrough_fold_prefix) * (ff_bn_mce_alternating_breakthrough_fold_prefix))))))))))) /\ ((exists ff_u_mce_breakthrough_fold_positive ff_v_mce_breakthrough_fold_positive. ((((exists ff_h_mce_breakthrough_fold_positive_start. ff_h_mce_breakthrough_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_breakthrough_fold_positive)) /\ exists ff_q_mce_breakthrough_fold_positive_start. ff_u_mce_breakthrough_fold_positive = ff_q_mce_breakthrough_fold_positive_start * S ((S (0)) * ff_v_mce_breakthrough_fold_positive) + (0))) /\ ((((exists ff_h_mce_breakthrough_fold_positive_terminal. ff_h_mce_breakthrough_fold_positive_terminal + S (p) = S ((S ((S (q)))) * ff_v_mce_breakthrough_fold_positive)) /\ exists ff_q_mce_breakthrough_fold_positive_terminal. ff_u_mce_breakthrough_fold_positive = ff_q_mce_breakthrough_fold_positive_terminal * S ((S ((S (q)))) * ff_v_mce_breakthrough_fold_positive) + (p))) /\ forall ff_i_mce_breakthrough_fold_positive. (exists ff_lt_mce_breakthrough_fold_positive_bound. ff_lt_mce_breakthrough_fold_positive_bound + S ff_i_mce_breakthrough_fold_positive = (S (q))) -> exists ff_a_mce_breakthrough_fold_positive ff_r_mce_breakthrough_fold_positive ff_s_mce_breakthrough_fold_positive. ((((exists ff_h_mce_breakthrough_fold_positive_summand. ff_h_mce_breakthrough_fold_positive_summand + S (ff_a_mce_breakthrough_fold_positive) = S ((S (ff_i_mce_breakthrough_fold_positive)) * ff_uc_mce_fold_breakthrough_fold)) /\ exists ff_q_mce_breakthrough_fold_positive_summand. ff_ub_mce_fold_breakthrough_fold = ff_q_mce_breakthrough_fold_positive_summand * S ((S (ff_i_mce_breakthrough_fold_positive)) * ff_uc_mce_fold_breakthrough_fold) + (ff_a_mce_breakthrough_fold_positive))) /\ ((((exists ff_h_mce_breakthrough_fold_positive_partial. ff_h_mce_breakthrough_fold_positive_partial + S (ff_r_mce_breakthrough_fold_positive) = S ((S (ff_i_mce_breakthrough_fold_positive)) * ff_v_mce_breakthrough_fold_positive)) /\ exists ff_q_mce_breakthrough_fold_positive_partial. ff_u_mce_breakthrough_fold_positive = ff_q_mce_breakthrough_fold_positive_partial * S ((S (ff_i_mce_breakthrough_fold_positive)) * ff_v_mce_breakthrough_fold_positive) + (ff_r_mce_breakthrough_fold_positive))) /\ ((((exists ff_h_mce_breakthrough_fold_positive_successor. ff_h_mce_breakthrough_fold_positive_successor + S (ff_s_mce_breakthrough_fold_positive) = S ((S (S ff_i_mce_breakthrough_fold_positive)) * ff_v_mce_breakthrough_fold_positive)) /\ exists ff_q_mce_breakthrough_fold_positive_successor. ff_u_mce_breakthrough_fold_positive = ff_q_mce_breakthrough_fold_positive_successor * S ((S (S ff_i_mce_breakthrough_fold_positive)) * ff_v_mce_breakthrough_fold_positive) + (ff_s_mce_breakthrough_fold_positive))) /\ ff_s_mce_breakthrough_fold_positive = ff_r_mce_breakthrough_fold_positive + ff_a_mce_breakthrough_fold_positive)))))) /\ (exists ff_u_mce_breakthrough_fold_negative ff_v_mce_breakthrough_fold_negative. ((((exists ff_h_mce_breakthrough_fold_negative_start. ff_h_mce_breakthrough_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_breakthrough_fold_negative)) /\ exists ff_q_mce_breakthrough_fold_negative_start. ff_u_mce_breakthrough_fold_negative = ff_q_mce_breakthrough_fold_negative_start * S ((S (0)) * ff_v_mce_breakthrough_fold_negative) + (0))) /\ ((((exists ff_h_mce_breakthrough_fold_negative_terminal. ff_h_mce_breakthrough_fold_negative_terminal + S (n) = S ((S ((S (q)))) * ff_v_mce_breakthrough_fold_negative)) /\ exists ff_q_mce_breakthrough_fold_negative_terminal. ff_u_mce_breakthrough_fold_negative = ff_q_mce_breakthrough_fold_negative_terminal * S ((S ((S (q)))) * ff_v_mce_breakthrough_fold_negative) + (n))) /\ forall ff_i_mce_breakthrough_fold_negative. (exists ff_lt_mce_breakthrough_fold_negative_bound. ff_lt_mce_breakthrough_fold_negative_bound + S ff_i_mce_breakthrough_fold_negative = (S (q))) -> exists ff_a_mce_breakthrough_fold_negative ff_r_mce_breakthrough_fold_negative ff_s_mce_breakthrough_fold_negative. ((((exists ff_h_mce_breakthrough_fold_negative_summand. ff_h_mce_breakthrough_fold_negative_summand + S (ff_a_mce_breakthrough_fold_negative) = S ((S (ff_i_mce_breakthrough_fold_negative)) * ff_vc_mce_fold_breakthrough_fold)) /\ exists ff_q_mce_breakthrough_fold_negative_summand. ff_vb_mce_fold_breakthrough_fold = ff_q_mce_breakthrough_fold_negative_summand * S ((S (ff_i_mce_breakthrough_fold_negative)) * ff_vc_mce_fold_breakthrough_fold) + (ff_a_mce_breakthrough_fold_negative))) /\ ((((exists ff_h_mce_breakthrough_fold_negative_partial. ff_h_mce_breakthrough_fold_negative_partial + S (ff_r_mce_breakthrough_fold_negative) = S ((S (ff_i_mce_breakthrough_fold_negative)) * ff_v_mce_breakthrough_fold_negative)) /\ exists ff_q_mce_breakthrough_fold_negative_partial. ff_u_mce_breakthrough_fold_negative = ff_q_mce_breakthrough_fold_negative_partial * S ((S (ff_i_mce_breakthrough_fold_negative)) * ff_v_mce_breakthrough_fold_negative) + (ff_r_mce_breakthrough_fold_negative))) /\ ((((exists ff_h_mce_breakthrough_fold_negative_successor. ff_h_mce_breakthrough_fold_negative_successor + S (ff_s_mce_breakthrough_fold_negative) = S ((S (S ff_i_mce_breakthrough_fold_negative)) * ff_v_mce_breakthrough_fold_negative)) /\ exists ff_q_mce_breakthrough_fold_negative_successor. ff_u_mce_breakthrough_fold_negative = ff_q_mce_breakthrough_fold_negative_successor * S ((S (S ff_i_mce_breakthrough_fold_negative)) * ff_v_mce_breakthrough_fold_negative) + (ff_s_mce_breakthrough_fold_negative))) /\ ff_s_mce_breakthrough_fold_negative = ff_r_mce_breakthrough_fold_negative + ff_a_mce_breakthrough_fold_negative)))))))))))

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