SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l)

Hygienic expanded first-order definition

forall ff_index_mce_alternating_breakthrough. (exists ff_gap_mce_breakthrough_index. ff_gap_mce_breakthrough_index + S (ff_index_mce_alternating_breakthrough) = (l)) -> exists ff_ap_mce_alternating_breakthrough ff_an_mce_alternating_breakthrough ff_bp_mce_alternating_breakthrough ff_bn_mce_alternating_breakthrough ff_p_mce_alternating_breakthrough ff_n_mce_alternating_breakthrough. ((((exists ff_h_mce_breakthrough_ap. ff_h_mce_breakthrough_ap + S (ff_ap_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * ac)) /\ exists ff_q_mce_breakthrough_ap. ab = ff_q_mce_breakthrough_ap * S ((S (ff_index_mce_alternating_breakthrough)) * ac) + (ff_ap_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_an. ff_h_mce_breakthrough_an + S (ff_an_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * dc)) /\ exists ff_q_mce_breakthrough_an. db = ff_q_mce_breakthrough_an * S ((S (ff_index_mce_alternating_breakthrough)) * dc) + (ff_an_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_bp. ff_h_mce_breakthrough_bp + S (ff_bp_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * ec)) /\ exists ff_q_mce_breakthrough_bp. eb = ff_q_mce_breakthrough_bp * S ((S (ff_index_mce_alternating_breakthrough)) * ec) + (ff_bp_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_bn. ff_h_mce_breakthrough_bn + S (ff_bn_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * fc)) /\ exists ff_q_mce_breakthrough_bn. fb = ff_q_mce_breakthrough_bn * S ((S (ff_index_mce_alternating_breakthrough)) * fc) + (ff_bn_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_positive. ff_h_mce_breakthrough_positive + S (ff_p_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * uc)) /\ exists ff_q_mce_breakthrough_positive. ub = ff_q_mce_breakthrough_positive * S ((S (ff_index_mce_alternating_breakthrough)) * uc) + (ff_p_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_negative. ff_h_mce_breakthrough_negative + S (ff_n_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * vc)) /\ exists ff_q_mce_breakthrough_negative. vb = ff_q_mce_breakthrough_negative * S ((S (ff_index_mce_alternating_breakthrough)) * vc) + (ff_n_mce_alternating_breakthrough))) /\ (((exists ff_even_mce_term_breakthrough_term. ff_index_mce_alternating_breakthrough = 2 * ff_even_mce_term_breakthrough_term) /\ (ff_p_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) /\ ff_n_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough))) \/ ((exists ff_odd_mce_term_breakthrough_term. ff_index_mce_alternating_breakthrough = 2 * ff_odd_mce_term_breakthrough_term + 1) /\ (ff_p_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) /\ ff_n_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough))))))))))

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