matrix_lattice_identity_selected_signed

Exact expanded first-order arithmetic statement

forall ab ac bb bc d ib ic. ~(d = 0) -> (forall mdr_i_signed_identity. (exists mdr_gap_signed_identitybound. mdr_gap_signed_identitybound + S (mdr_i_signed_identity) = (d)) -> (((exists ff_h_mdr_signed_identityentry. ff_h_mdr_signed_identityentry + S (mdr_i_signed_identity) = S ((S (mdr_i_signed_identity)) * ic)) /\ exists ff_q_mdr_signed_identityentry. ib = ff_q_mdr_signed_identityentry * S ((S (mdr_i_signed_identity)) * ic) + (mdr_i_signed_identity)))) -> (((forall mdr_i_identity_selected_signedpositive. (exists mdr_gap_identity_selected_signedpositivebound. mdr_gap_identity_selected_signedpositivebound + S (mdr_i_identity_selected_signedpositive) = ((d) * (d))) -> exists mdr_a_identity_selected_signedpositive. (((exists mdr_r_identity_selected_signedpositivepoint mdr_s_identity_selected_signedpositivepoint mdr_u_identity_selected_signedpositivepoint mdr_v_identity_selected_signedpositivepoint. ((mdr_i_identity_selected_signedpositive = (d) * mdr_r_identity_selected_signedpositivepoint + mdr_s_identity_selected_signedpositivepoint) /\ ((exists mdr_gap_identity_selected_signedpositivepointcolumn. mdr_gap_identity_selected_signedpositivepointcolumn + S (mdr_s_identity_selected_signedpositivepoint) = (d)) /\ ((((exists ff_h_mdr_identity_selected_signedpositivepointrow_index. ff_h_mdr_identity_selected_signedpositivepointrow_index + S (mdr_u_identity_selected_signedpositivepoint) = S ((S (mdr_r_identity_selected_signedpositivepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signedpositivepointrow_index. ib = ff_q_mdr_identity_selected_signedpositivepointrow_index * S ((S (mdr_r_identity_selected_signedpositivepoint)) * ic) + (mdr_u_identity_selected_signedpositivepoint))) /\ ((((exists ff_h_mdr_identity_selected_signedpositivepointcolumn_index. ff_h_mdr_identity_selected_signedpositivepointcolumn_index + S (mdr_v_identity_selected_signedpositivepoint) = S ((S (mdr_s_identity_selected_signedpositivepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signedpositivepointcolumn_index. ib = ff_q_mdr_identity_selected_signedpositivepointcolumn_index * S ((S (mdr_s_identity_selected_signedpositivepoint)) * ic) + (mdr_v_identity_selected_signedpositivepoint))) /\ (((exists ff_h_mdr_identity_selected_signedpositivepointsource. ff_h_mdr_identity_selected_signedpositivepointsource + S (mdr_a_identity_selected_signedpositive) = S ((S ((mdr_u_identity_selected_signedpositivepoint) * (d) + (mdr_v_identity_selected_signedpositivepoint))) * ac)) /\ exists ff_q_mdr_identity_selected_signedpositivepointsource. ab = ff_q_mdr_identity_selected_signedpositivepointsource * S ((S ((mdr_u_identity_selected_signedpositivepoint) * (d) + (mdr_v_identity_selected_signedpositivepoint))) * ac) + (mdr_a_identity_selected_signedpositive)))))))) /\ (((exists ff_h_mdr_identity_selected_signedpositiveoutput. ff_h_mdr_identity_selected_signedpositiveoutput + S (mdr_a_identity_selected_signedpositive) = S ((S (mdr_i_identity_selected_signedpositive)) * ac)) /\ exists ff_q_mdr_identity_selected_signedpositiveoutput. ab = ff_q_mdr_identity_selected_signedpositiveoutput * S ((S (mdr_i_identity_selected_signedpositive)) * ac) + (mdr_a_identity_selected_signedpositive)))))) /\ (forall mdr_i_identity_selected_signednegative. (exists mdr_gap_identity_selected_signednegativebound. mdr_gap_identity_selected_signednegativebound + S (mdr_i_identity_selected_signednegative) = ((d) * (d))) -> exists mdr_a_identity_selected_signednegative. (((exists mdr_r_identity_selected_signednegativepoint mdr_s_identity_selected_signednegativepoint mdr_u_identity_selected_signednegativepoint mdr_v_identity_selected_signednegativepoint. ((mdr_i_identity_selected_signednegative = (d) * mdr_r_identity_selected_signednegativepoint + mdr_s_identity_selected_signednegativepoint) /\ ((exists mdr_gap_identity_selected_signednegativepointcolumn. mdr_gap_identity_selected_signednegativepointcolumn + S (mdr_s_identity_selected_signednegativepoint) = (d)) /\ ((((exists ff_h_mdr_identity_selected_signednegativepointrow_index. ff_h_mdr_identity_selected_signednegativepointrow_index + S (mdr_u_identity_selected_signednegativepoint) = S ((S (mdr_r_identity_selected_signednegativepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signednegativepointrow_index. ib = ff_q_mdr_identity_selected_signednegativepointrow_index * S ((S (mdr_r_identity_selected_signednegativepoint)) * ic) + (mdr_u_identity_selected_signednegativepoint))) /\ ((((exists ff_h_mdr_identity_selected_signednegativepointcolumn_index. ff_h_mdr_identity_selected_signednegativepointcolumn_index + S (mdr_v_identity_selected_signednegativepoint) = S ((S (mdr_s_identity_selected_signednegativepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signednegativepointcolumn_index. ib = ff_q_mdr_identity_selected_signednegativepointcolumn_index * S ((S (mdr_s_identity_selected_signednegativepoint)) * ic) + (mdr_v_identity_selected_signednegativepoint))) /\ (((exists ff_h_mdr_identity_selected_signednegativepointsource. ff_h_mdr_identity_selected_signednegativepointsource + S (mdr_a_identity_selected_signednegative) = S ((S ((mdr_u_identity_selected_signednegativepoint) * (d) + (mdr_v_identity_selected_signednegativepoint))) * bc)) /\ exists ff_q_mdr_identity_selected_signednegativepointsource. bb = ff_q_mdr_identity_selected_signednegativepointsource * S ((S ((mdr_u_identity_selected_signednegativepoint) * (d) + (mdr_v_identity_selected_signednegativepoint))) * bc) + (mdr_a_identity_selected_signednegative)))))))) /\ (((exists ff_h_mdr_identity_selected_signednegativeoutput. ff_h_mdr_identity_selected_signednegativeoutput + S (mdr_a_identity_selected_signednegative) = S ((S (mdr_i_identity_selected_signednegative)) * bc)) /\ exists ff_q_mdr_identity_selected_signednegativeoutput. bb = ff_q_mdr_identity_selected_signednegativeoutput * S ((S (mdr_i_identity_selected_signednegative)) * bc) + (mdr_a_identity_selected_signednegative))))))))