polynomial_diagonal_sum_left_add_congruent

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L db dc M i N ub uc vb vc wb wc u v w. (forall pfp_index_diagonal_add_left_source. (exists pfa_gap_diagonal_add_left_sourceindex. pfa_gap_diagonal_add_left_sourceindex + S (pfp_index_diagonal_add_left_source) = (L)) -> exists pfp_left_diagonal_add_left_source pfp_right_diagonal_add_left_source pfp_value_diagonal_add_left_source. ((((exists ff_h_pfp_diagonal_add_left_sourceleft. ff_h_pfp_diagonal_add_left_sourceleft + S (pfp_left_diagonal_add_left_source) = S ((S (pfp_index_diagonal_add_left_source)) * ac)) /\ exists ff_q_pfp_diagonal_add_left_sourceleft. ab = ff_q_pfp_diagonal_add_left_sourceleft * S ((S (pfp_index_diagonal_add_left_source)) * ac) + (pfp_left_diagonal_add_left_source))) /\ (((((exists ff_h_pfp_diagonal_add_left_sourceright. ff_h_pfp_diagonal_add_left_sourceright + S (pfp_right_diagonal_add_left_source) = S ((S (pfp_index_diagonal_add_left_source)) * bc)) /\ exists ff_q_pfp_diagonal_add_left_sourceright. bb = ff_q_pfp_diagonal_add_left_sourceright * S ((S (pfp_index_diagonal_add_left_source)) * bc) + (pfp_right_diagonal_add_left_source))) /\ (((((exists ff_h_pfp_diagonal_add_left_sourcetarget. ff_h_pfp_diagonal_add_left_sourcetarget + S (pfp_value_diagonal_add_left_source) = S ((S (pfp_index_diagonal_add_left_source)) * cc)) /\ exists ff_q_pfp_diagonal_add_left_sourcetarget. cb = ff_q_pfp_diagonal_add_left_sourcetarget * S ((S (pfp_index_diagonal_add_left_source)) * cc) + (pfp_value_diagonal_add_left_source))) /\ ((((exists pfa_gap_diagonal_add_left_sourceoperationleft. pfa_gap_diagonal_add_left_sourceoperationleft + S (pfp_left_diagonal_add_left_source) = (p)) /\ (((exists pfa_gap_diagonal_add_left_sourceoperationright. pfa_gap_diagonal_add_left_sourceoperationright + S (pfp_right_diagonal_add_left_source) = (p)) /\ ((((exists pfa_gap_diagonal_add_left_sourceoperationresultbound. pfa_gap_diagonal_add_left_sourceoperationresultbound + S (pfp_value_diagonal_add_left_source) = (p)) /\ ((exists pfa_offset_left_diagonal_add_left_sourceoperationresultcongruence pfa_offset_right_diagonal_add_left_sourceoperationresultcongruence. ((pfp_left_diagonal_add_left_source) + (pfp_right_diagonal_add_left_source)) + (p) * pfa_offset_left_diagonal_add_left_sourceoperationresultcongruence = (pfp_value_diagonal_add_left_source) + (p) * pfa_offset_right_diagonal_add_left_sourceoperationresultcongruence)))))))))))))))) -> (forall pfc_index_diagonal_add_left_u. (exists pfa_gap_diagonal_add_left_ubound. pfa_gap_diagonal_add_left_ubound + S (pfc_index_diagonal_add_left_u) = (N)) -> exists pfc_value_diagonal_add_left_u. ((((exists ff_h_pfp_diagonal_add_left_uentry. ff_h_pfp_diagonal_add_left_uentry + S (pfc_value_diagonal_add_left_u) = S ((S (pfc_index_diagonal_add_left_u)) * uc)) /\ exists ff_q_pfp_diagonal_add_left_uentry. ub = ff_q_pfp_diagonal_add_left_uentry * S ((S (pfc_index_diagonal_add_left_u)) * uc) + (pfc_value_diagonal_add_left_u))) /\ ((exists pfc_complement_diagonal_add_left_uterm pfc_left_diagonal_add_left_uterm pfc_right_diagonal_add_left_uterm. (((pfc_index_diagonal_add_left_u)+pfc_complement_diagonal_add_left_uterm=(i)) /\ ((((((exists pfa_gap_diagonal_add_left_utermleftinside. pfa_gap_diagonal_add_left_utermleftinside + S (pfc_index_diagonal_add_left_u) = (M)) /\ ((((exists ff_h_pfp_diagonal_add_left_utermleftentry. ff_h_pfp_diagonal_add_left_utermleftentry + S (pfc_left_diagonal_add_left_uterm) = S ((S (pfc_index_diagonal_add_left_u)) * dc)) /\ exists ff_q_pfp_diagonal_add_left_utermleftentry. db = ff_q_pfp_diagonal_add_left_utermleftentry * S ((S (pfc_index_diagonal_add_left_u)) * dc) + (pfc_left_diagonal_add_left_uterm)))))) \/ (((exists pfc_gap_diagonal_add_left_utermleftoutside. pfc_gap_diagonal_add_left_utermleftoutside+(M)=(pfc_index_diagonal_add_left_u)) /\ (((pfc_left_diagonal_add_left_uterm)=0))))) /\ ((((((exists pfa_gap_diagonal_add_left_utermrightinside. pfa_gap_diagonal_add_left_utermrightinside + S (pfc_complement_diagonal_add_left_uterm) = (L)) /\ ((((exists ff_h_pfp_diagonal_add_left_utermrightentry. ff_h_pfp_diagonal_add_left_utermrightentry + S (pfc_right_diagonal_add_left_uterm) = S ((S (pfc_complement_diagonal_add_left_uterm)) * ac)) /\ exists ff_q_pfp_diagonal_add_left_utermrightentry. ab = ff_q_pfp_diagonal_add_left_utermrightentry * S ((S (pfc_complement_diagonal_add_left_uterm)) * ac) + (pfc_right_diagonal_add_left_uterm)))))) \/ (((exists pfc_gap_diagonal_add_left_utermrightoutside. pfc_gap_diagonal_add_left_utermrightoutside+(L)=(pfc_complement_diagonal_add_left_uterm)) /\ (((pfc_right_diagonal_add_left_uterm)=0))))) /\ (((pfc_value_diagonal_add_left_u)=pfc_left_diagonal_add_left_uterm*pfc_right_diagonal_add_left_uterm))))))))))) -> (exists fs_u_pfc_diagonal_add_left_sum_u fs_v_pfc_diagonal_add_left_sum_u. ((((exists fs_h_pfc_diagonal_add_left_sum_u_body_start. fs_h_pfc_diagonal_add_left_sum_u_body_start + S (0) = S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_u)) /\ exists fs_q_pfc_diagonal_add_left_sum_u_body_start. fs_u_pfc_diagonal_add_left_sum_u = fs_q_pfc_diagonal_add_left_sum_u_body_start * S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_u) + (0))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_u_body_terminal. fs_h_pfc_diagonal_add_left_sum_u_body_terminal + S (u) = S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_u)) /\ exists fs_q_pfc_diagonal_add_left_sum_u_body_terminal. fs_u_pfc_diagonal_add_left_sum_u = fs_q_pfc_diagonal_add_left_sum_u_body_terminal * S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_u) + (u))) /\ forall fs_i_pfc_diagonal_add_left_sum_u_body_steps. (exists fs_lt_pfc_diagonal_add_left_sum_u_body_steps_bound. fs_lt_pfc_diagonal_add_left_sum_u_body_steps_bound + S fs_i_pfc_diagonal_add_left_sum_u_body_steps = N) -> exists fs_a_pfc_diagonal_add_left_sum_u_body_steps fs_r_pfc_diagonal_add_left_sum_u_body_steps fs_s_pfc_diagonal_add_left_sum_u_body_steps. ((((exists fs_h_pfc_diagonal_add_left_sum_u_body_steps_summand. fs_h_pfc_diagonal_add_left_sum_u_body_steps_summand + S (fs_a_pfc_diagonal_add_left_sum_u_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * uc)) /\ exists fs_q_pfc_diagonal_add_left_sum_u_body_steps_summand. ub = fs_q_pfc_diagonal_add_left_sum_u_body_steps_summand * S ((S (fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * uc) + (fs_a_pfc_diagonal_add_left_sum_u_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_u_body_steps_partial. fs_h_pfc_diagonal_add_left_sum_u_body_steps_partial + S (fs_r_pfc_diagonal_add_left_sum_u_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * fs_v_pfc_diagonal_add_left_sum_u)) /\ exists fs_q_pfc_diagonal_add_left_sum_u_body_steps_partial. fs_u_pfc_diagonal_add_left_sum_u = fs_q_pfc_diagonal_add_left_sum_u_body_steps_partial * S ((S (fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * fs_v_pfc_diagonal_add_left_sum_u) + (fs_r_pfc_diagonal_add_left_sum_u_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_u_body_steps_successor. fs_h_pfc_diagonal_add_left_sum_u_body_steps_successor + S (fs_s_pfc_diagonal_add_left_sum_u_body_steps) = S ((S (S fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * fs_v_pfc_diagonal_add_left_sum_u)) /\ exists fs_q_pfc_diagonal_add_left_sum_u_body_steps_successor. fs_u_pfc_diagonal_add_left_sum_u = fs_q_pfc_diagonal_add_left_sum_u_body_steps_successor * S ((S (S fs_i_pfc_diagonal_add_left_sum_u_body_steps)) * fs_v_pfc_diagonal_add_left_sum_u) + (fs_s_pfc_diagonal_add_left_sum_u_body_steps))) /\ fs_s_pfc_diagonal_add_left_sum_u_body_steps = fs_r_pfc_diagonal_add_left_sum_u_body_steps + fs_a_pfc_diagonal_add_left_sum_u_body_steps)))))) -> (forall pfc_index_diagonal_add_left_v. (exists pfa_gap_diagonal_add_left_vbound. pfa_gap_diagonal_add_left_vbound + S (pfc_index_diagonal_add_left_v) = (N)) -> exists pfc_value_diagonal_add_left_v. ((((exists ff_h_pfp_diagonal_add_left_ventry. ff_h_pfp_diagonal_add_left_ventry + S (pfc_value_diagonal_add_left_v) = S ((S (pfc_index_diagonal_add_left_v)) * vc)) /\ exists ff_q_pfp_diagonal_add_left_ventry. vb = ff_q_pfp_diagonal_add_left_ventry * S ((S (pfc_index_diagonal_add_left_v)) * vc) + (pfc_value_diagonal_add_left_v))) /\ ((exists pfc_complement_diagonal_add_left_vterm pfc_left_diagonal_add_left_vterm pfc_right_diagonal_add_left_vterm. (((pfc_index_diagonal_add_left_v)+pfc_complement_diagonal_add_left_vterm=(i)) /\ ((((((exists pfa_gap_diagonal_add_left_vtermleftinside. pfa_gap_diagonal_add_left_vtermleftinside + S (pfc_index_diagonal_add_left_v) = (M)) /\ ((((exists ff_h_pfp_diagonal_add_left_vtermleftentry. ff_h_pfp_diagonal_add_left_vtermleftentry + S (pfc_left_diagonal_add_left_vterm) = S ((S (pfc_index_diagonal_add_left_v)) * dc)) /\ exists ff_q_pfp_diagonal_add_left_vtermleftentry. db = ff_q_pfp_diagonal_add_left_vtermleftentry * S ((S (pfc_index_diagonal_add_left_v)) * dc) + (pfc_left_diagonal_add_left_vterm)))))) \/ (((exists pfc_gap_diagonal_add_left_vtermleftoutside. pfc_gap_diagonal_add_left_vtermleftoutside+(M)=(pfc_index_diagonal_add_left_v)) /\ (((pfc_left_diagonal_add_left_vterm)=0))))) /\ ((((((exists pfa_gap_diagonal_add_left_vtermrightinside. pfa_gap_diagonal_add_left_vtermrightinside + S (pfc_complement_diagonal_add_left_vterm) = (L)) /\ ((((exists ff_h_pfp_diagonal_add_left_vtermrightentry. ff_h_pfp_diagonal_add_left_vtermrightentry + S (pfc_right_diagonal_add_left_vterm) = S ((S (pfc_complement_diagonal_add_left_vterm)) * bc)) /\ exists ff_q_pfp_diagonal_add_left_vtermrightentry. bb = ff_q_pfp_diagonal_add_left_vtermrightentry * S ((S (pfc_complement_diagonal_add_left_vterm)) * bc) + (pfc_right_diagonal_add_left_vterm)))))) \/ (((exists pfc_gap_diagonal_add_left_vtermrightoutside. pfc_gap_diagonal_add_left_vtermrightoutside+(L)=(pfc_complement_diagonal_add_left_vterm)) /\ (((pfc_right_diagonal_add_left_vterm)=0))))) /\ (((pfc_value_diagonal_add_left_v)=pfc_left_diagonal_add_left_vterm*pfc_right_diagonal_add_left_vterm))))))))))) -> (exists fs_u_pfc_diagonal_add_left_sum_v fs_v_pfc_diagonal_add_left_sum_v. ((((exists fs_h_pfc_diagonal_add_left_sum_v_body_start. fs_h_pfc_diagonal_add_left_sum_v_body_start + S (0) = S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_v)) /\ exists fs_q_pfc_diagonal_add_left_sum_v_body_start. fs_u_pfc_diagonal_add_left_sum_v = fs_q_pfc_diagonal_add_left_sum_v_body_start * S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_v) + (0))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_v_body_terminal. fs_h_pfc_diagonal_add_left_sum_v_body_terminal + S (v) = S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_v)) /\ exists fs_q_pfc_diagonal_add_left_sum_v_body_terminal. fs_u_pfc_diagonal_add_left_sum_v = fs_q_pfc_diagonal_add_left_sum_v_body_terminal * S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_v) + (v))) /\ forall fs_i_pfc_diagonal_add_left_sum_v_body_steps. (exists fs_lt_pfc_diagonal_add_left_sum_v_body_steps_bound. fs_lt_pfc_diagonal_add_left_sum_v_body_steps_bound + S fs_i_pfc_diagonal_add_left_sum_v_body_steps = N) -> exists fs_a_pfc_diagonal_add_left_sum_v_body_steps fs_r_pfc_diagonal_add_left_sum_v_body_steps fs_s_pfc_diagonal_add_left_sum_v_body_steps. ((((exists fs_h_pfc_diagonal_add_left_sum_v_body_steps_summand. fs_h_pfc_diagonal_add_left_sum_v_body_steps_summand + S (fs_a_pfc_diagonal_add_left_sum_v_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * vc)) /\ exists fs_q_pfc_diagonal_add_left_sum_v_body_steps_summand. vb = fs_q_pfc_diagonal_add_left_sum_v_body_steps_summand * S ((S (fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * vc) + (fs_a_pfc_diagonal_add_left_sum_v_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_v_body_steps_partial. fs_h_pfc_diagonal_add_left_sum_v_body_steps_partial + S (fs_r_pfc_diagonal_add_left_sum_v_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * fs_v_pfc_diagonal_add_left_sum_v)) /\ exists fs_q_pfc_diagonal_add_left_sum_v_body_steps_partial. fs_u_pfc_diagonal_add_left_sum_v = fs_q_pfc_diagonal_add_left_sum_v_body_steps_partial * S ((S (fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * fs_v_pfc_diagonal_add_left_sum_v) + (fs_r_pfc_diagonal_add_left_sum_v_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_v_body_steps_successor. fs_h_pfc_diagonal_add_left_sum_v_body_steps_successor + S (fs_s_pfc_diagonal_add_left_sum_v_body_steps) = S ((S (S fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * fs_v_pfc_diagonal_add_left_sum_v)) /\ exists fs_q_pfc_diagonal_add_left_sum_v_body_steps_successor. fs_u_pfc_diagonal_add_left_sum_v = fs_q_pfc_diagonal_add_left_sum_v_body_steps_successor * S ((S (S fs_i_pfc_diagonal_add_left_sum_v_body_steps)) * fs_v_pfc_diagonal_add_left_sum_v) + (fs_s_pfc_diagonal_add_left_sum_v_body_steps))) /\ fs_s_pfc_diagonal_add_left_sum_v_body_steps = fs_r_pfc_diagonal_add_left_sum_v_body_steps + fs_a_pfc_diagonal_add_left_sum_v_body_steps)))))) -> (forall pfc_index_diagonal_add_left_w. (exists pfa_gap_diagonal_add_left_wbound. pfa_gap_diagonal_add_left_wbound + S (pfc_index_diagonal_add_left_w) = (N)) -> exists pfc_value_diagonal_add_left_w. ((((exists ff_h_pfp_diagonal_add_left_wentry. ff_h_pfp_diagonal_add_left_wentry + S (pfc_value_diagonal_add_left_w) = S ((S (pfc_index_diagonal_add_left_w)) * wc)) /\ exists ff_q_pfp_diagonal_add_left_wentry. wb = ff_q_pfp_diagonal_add_left_wentry * S ((S (pfc_index_diagonal_add_left_w)) * wc) + (pfc_value_diagonal_add_left_w))) /\ ((exists pfc_complement_diagonal_add_left_wterm pfc_left_diagonal_add_left_wterm pfc_right_diagonal_add_left_wterm. (((pfc_index_diagonal_add_left_w)+pfc_complement_diagonal_add_left_wterm=(i)) /\ ((((((exists pfa_gap_diagonal_add_left_wtermleftinside. pfa_gap_diagonal_add_left_wtermleftinside + S (pfc_index_diagonal_add_left_w) = (M)) /\ ((((exists ff_h_pfp_diagonal_add_left_wtermleftentry. ff_h_pfp_diagonal_add_left_wtermleftentry + S (pfc_left_diagonal_add_left_wterm) = S ((S (pfc_index_diagonal_add_left_w)) * dc)) /\ exists ff_q_pfp_diagonal_add_left_wtermleftentry. db = ff_q_pfp_diagonal_add_left_wtermleftentry * S ((S (pfc_index_diagonal_add_left_w)) * dc) + (pfc_left_diagonal_add_left_wterm)))))) \/ (((exists pfc_gap_diagonal_add_left_wtermleftoutside. pfc_gap_diagonal_add_left_wtermleftoutside+(M)=(pfc_index_diagonal_add_left_w)) /\ (((pfc_left_diagonal_add_left_wterm)=0))))) /\ ((((((exists pfa_gap_diagonal_add_left_wtermrightinside. pfa_gap_diagonal_add_left_wtermrightinside + S (pfc_complement_diagonal_add_left_wterm) = (L)) /\ ((((exists ff_h_pfp_diagonal_add_left_wtermrightentry. ff_h_pfp_diagonal_add_left_wtermrightentry + S (pfc_right_diagonal_add_left_wterm) = S ((S (pfc_complement_diagonal_add_left_wterm)) * cc)) /\ exists ff_q_pfp_diagonal_add_left_wtermrightentry. cb = ff_q_pfp_diagonal_add_left_wtermrightentry * S ((S (pfc_complement_diagonal_add_left_wterm)) * cc) + (pfc_right_diagonal_add_left_wterm)))))) \/ (((exists pfc_gap_diagonal_add_left_wtermrightoutside. pfc_gap_diagonal_add_left_wtermrightoutside+(L)=(pfc_complement_diagonal_add_left_wterm)) /\ (((pfc_right_diagonal_add_left_wterm)=0))))) /\ (((pfc_value_diagonal_add_left_w)=pfc_left_diagonal_add_left_wterm*pfc_right_diagonal_add_left_wterm))))))))))) -> (exists fs_u_pfc_diagonal_add_left_sum_w fs_v_pfc_diagonal_add_left_sum_w. ((((exists fs_h_pfc_diagonal_add_left_sum_w_body_start. fs_h_pfc_diagonal_add_left_sum_w_body_start + S (0) = S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_w)) /\ exists fs_q_pfc_diagonal_add_left_sum_w_body_start. fs_u_pfc_diagonal_add_left_sum_w = fs_q_pfc_diagonal_add_left_sum_w_body_start * S ((S (0)) * fs_v_pfc_diagonal_add_left_sum_w) + (0))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_w_body_terminal. fs_h_pfc_diagonal_add_left_sum_w_body_terminal + S (w) = S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_w)) /\ exists fs_q_pfc_diagonal_add_left_sum_w_body_terminal. fs_u_pfc_diagonal_add_left_sum_w = fs_q_pfc_diagonal_add_left_sum_w_body_terminal * S ((S (N)) * fs_v_pfc_diagonal_add_left_sum_w) + (w))) /\ forall fs_i_pfc_diagonal_add_left_sum_w_body_steps. (exists fs_lt_pfc_diagonal_add_left_sum_w_body_steps_bound. fs_lt_pfc_diagonal_add_left_sum_w_body_steps_bound + S fs_i_pfc_diagonal_add_left_sum_w_body_steps = N) -> exists fs_a_pfc_diagonal_add_left_sum_w_body_steps fs_r_pfc_diagonal_add_left_sum_w_body_steps fs_s_pfc_diagonal_add_left_sum_w_body_steps. ((((exists fs_h_pfc_diagonal_add_left_sum_w_body_steps_summand. fs_h_pfc_diagonal_add_left_sum_w_body_steps_summand + S (fs_a_pfc_diagonal_add_left_sum_w_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * wc)) /\ exists fs_q_pfc_diagonal_add_left_sum_w_body_steps_summand. wb = fs_q_pfc_diagonal_add_left_sum_w_body_steps_summand * S ((S (fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * wc) + (fs_a_pfc_diagonal_add_left_sum_w_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_w_body_steps_partial. fs_h_pfc_diagonal_add_left_sum_w_body_steps_partial + S (fs_r_pfc_diagonal_add_left_sum_w_body_steps) = S ((S (fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * fs_v_pfc_diagonal_add_left_sum_w)) /\ exists fs_q_pfc_diagonal_add_left_sum_w_body_steps_partial. fs_u_pfc_diagonal_add_left_sum_w = fs_q_pfc_diagonal_add_left_sum_w_body_steps_partial * S ((S (fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * fs_v_pfc_diagonal_add_left_sum_w) + (fs_r_pfc_diagonal_add_left_sum_w_body_steps))) /\ ((((exists fs_h_pfc_diagonal_add_left_sum_w_body_steps_successor. fs_h_pfc_diagonal_add_left_sum_w_body_steps_successor + S (fs_s_pfc_diagonal_add_left_sum_w_body_steps) = S ((S (S fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * fs_v_pfc_diagonal_add_left_sum_w)) /\ exists fs_q_pfc_diagonal_add_left_sum_w_body_steps_successor. fs_u_pfc_diagonal_add_left_sum_w = fs_q_pfc_diagonal_add_left_sum_w_body_steps_successor * S ((S (S fs_i_pfc_diagonal_add_left_sum_w_body_steps)) * fs_v_pfc_diagonal_add_left_sum_w) + (fs_s_pfc_diagonal_add_left_sum_w_body_steps))) /\ fs_s_pfc_diagonal_add_left_sum_w_body_steps = fs_r_pfc_diagonal_add_left_sum_w_body_steps + fs_a_pfc_diagonal_add_left_sum_w_body_steps)))))) -> (exists pfa_offset_left_diagonal_add_left_result pfa_offset_right_diagonal_add_left_result. (u+v) + (p) * pfa_offset_left_diagonal_add_left_result = (w) + (p) * pfa_offset_right_diagonal_add_left_result)