prime_field_polynomial_scale_distributes_over_add

forall p k ab ac bb bc sb sc xb xc yb yc ub uc vb vc l. (forall pfp_index_distribute_sum. (exists pfa_gap_distribute_sumindex. pfa_gap_distribute_sumindex + S (pfp_index_distribute_sum) = (l)) -> exists pfp_left_distribute_sum pfp_right_distribute_sum pfp_value_distribute_sum. ((((exists ff_h_pfp_distribute_sumleft. ff_h_pfp_distribute_sumleft + S (pfp_left_distribute_sum) = S ((S (pfp_index_distribute_sum)) * ac)) /\ exists ff_q_pfp_distribute_sumleft. ab = ff_q_pfp_distribute_sumleft * S ((S (pfp_index_distribute_sum)) * ac) + (pfp_left_distribute_sum))) /\ (((((exists ff_h_pfp_distribute_sumright. ff_h_pfp_distribute_sumright + S (pfp_right_distribute_sum) = S ((S (pfp_index_distribute_sum)) * bc)) /\ exists ff_q_pfp_distribute_sumright. bb = ff_q_pfp_distribute_sumright * S ((S (pfp_index_distribute_sum)) * bc) + (pfp_right_distribute_sum))) /\ (((((exists ff_h_pfp_distribute_sumtarget. ff_h_pfp_distribute_sumtarget + S (pfp_value_distribute_sum) = S ((S (pfp_index_distribute_sum)) * sc)) /\ exists ff_q_pfp_distribute_sumtarget. sb = ff_q_pfp_distribute_sumtarget * S ((S (pfp_index_distribute_sum)) * sc) + (pfp_value_distribute_sum))) /\ ((((exists pfa_gap_distribute_sumoperationleft. pfa_gap_distribute_sumoperationleft + S (pfp_left_distribute_sum) = (p)) /\ (((exists pfa_gap_distribute_sumoperationright. pfa_gap_distribute_sumoperationright + S (pfp_right_distribute_sum) = (p)) /\ ((((exists pfa_gap_distribute_sumoperationresultbound. pfa_gap_distribute_sumoperationresultbound + S (pfp_value_distribute_sum) = (p)) /\ ((exists pfa_offset_left_distribute_sumoperationresultcongruence pfa_offset_right_distribute_sumoperationresultcongruence. ((pfp_left_distribute_sum) + (pfp_right_distribute_sum)) + (p) * pfa_offset_left_distribute_sumoperationresultcongruence = (pfp_value_distribute_sum) + (p) * pfa_offset_right_distribute_sumoperationresultcongruence)))))))))))))))) -> (((exists pfa_gap_distribute_leftscalar. pfa_gap_distribute_leftscalar + S (k) = (p)) /\ ((forall pfp_index_distribute_left. (exists pfa_gap_distribute_leftindex. pfa_gap_distribute_leftindex + S (pfp_index_distribute_left) = (l)) -> exists pfp_source_distribute_left pfp_value_distribute_left. ((((exists ff_h_pfp_distribute_leftsource. ff_h_pfp_distribute_leftsource + S (pfp_source_distribute_left) = S ((S (pfp_index_distribute_left)) * sc)) /\ exists ff_q_pfp_distribute_leftsource. sb = ff_q_pfp_distribute_leftsource * S ((S (pfp_index_distribute_left)) * sc) + (pfp_source_distribute_left))) /\ (((((exists ff_h_pfp_distribute_lefttarget. ff_h_pfp_distribute_lefttarget + S (pfp_value_distribute_left) = S ((S (pfp_index_distribute_left)) * uc)) /\ exists ff_q_pfp_distribute_lefttarget. ub = ff_q_pfp_distribute_lefttarget * S ((S (pfp_index_distribute_left)) * uc) + (pfp_value_distribute_left))) /\ ((((exists pfa_gap_distribute_leftoperationleft. pfa_gap_distribute_leftoperationleft + S (k) = (p)) /\ (((exists pfa_gap_distribute_leftoperationright. pfa_gap_distribute_leftoperationright + S (pfp_source_distribute_left) = (p)) /\ ((((exists pfa_gap_distribute_leftoperationresultbound. pfa_gap_distribute_leftoperationresultbound + S (pfp_value_distribute_left) = (p)) /\ ((exists pfa_offset_left_distribute_leftoperationresultcongruence pfa_offset_right_distribute_leftoperationresultcongruence. ((k) * (pfp_source_distribute_left)) + (p) * pfa_offset_left_distribute_leftoperationresultcongruence = (pfp_value_distribute_left) + (p) * pfa_offset_right_distribute_leftoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_distribute_ascalar. pfa_gap_distribute_ascalar + S (k) = (p)) /\ ((forall pfp_index_distribute_a. (exists pfa_gap_distribute_aindex. pfa_gap_distribute_aindex + S (pfp_index_distribute_a) = (l)) -> exists pfp_source_distribute_a pfp_value_distribute_a. ((((exists ff_h_pfp_distribute_asource. ff_h_pfp_distribute_asource + S (pfp_source_distribute_a) = S ((S (pfp_index_distribute_a)) * ac)) /\ exists ff_q_pfp_distribute_asource. ab = ff_q_pfp_distribute_asource * S ((S (pfp_index_distribute_a)) * ac) + (pfp_source_distribute_a))) /\ (((((exists ff_h_pfp_distribute_atarget. ff_h_pfp_distribute_atarget + S (pfp_value_distribute_a) = S ((S (pfp_index_distribute_a)) * xc)) /\ exists ff_q_pfp_distribute_atarget. xb = ff_q_pfp_distribute_atarget * S ((S (pfp_index_distribute_a)) * xc) + (pfp_value_distribute_a))) /\ ((((exists pfa_gap_distribute_aoperationleft. pfa_gap_distribute_aoperationleft + S (k) = (p)) /\ (((exists pfa_gap_distribute_aoperationright. pfa_gap_distribute_aoperationright + S (pfp_source_distribute_a) = (p)) /\ ((((exists pfa_gap_distribute_aoperationresultbound. pfa_gap_distribute_aoperationresultbound + S (pfp_value_distribute_a) = (p)) /\ ((exists pfa_offset_left_distribute_aoperationresultcongruence pfa_offset_right_distribute_aoperationresultcongruence. ((k) * (pfp_source_distribute_a)) + (p) * pfa_offset_left_distribute_aoperationresultcongruence = (pfp_value_distribute_a) + (p) * pfa_offset_right_distribute_aoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_distribute_bscalar. pfa_gap_distribute_bscalar + S (k) = (p)) /\ ((forall pfp_index_distribute_b. (exists pfa_gap_distribute_bindex. pfa_gap_distribute_bindex + S (pfp_index_distribute_b) = (l)) -> exists pfp_source_distribute_b pfp_value_distribute_b. ((((exists ff_h_pfp_distribute_bsource. ff_h_pfp_distribute_bsource + S (pfp_source_distribute_b) = S ((S (pfp_index_distribute_b)) * bc)) /\ exists ff_q_pfp_distribute_bsource. bb = ff_q_pfp_distribute_bsource * S ((S (pfp_index_distribute_b)) * bc) + (pfp_source_distribute_b))) /\ (((((exists ff_h_pfp_distribute_btarget. ff_h_pfp_distribute_btarget + S (pfp_value_distribute_b) = S ((S (pfp_index_distribute_b)) * yc)) /\ exists ff_q_pfp_distribute_btarget. yb = ff_q_pfp_distribute_btarget * S ((S (pfp_index_distribute_b)) * yc) + (pfp_value_distribute_b))) /\ ((((exists pfa_gap_distribute_boperationleft. pfa_gap_distribute_boperationleft + S (k) = (p)) /\ (((exists pfa_gap_distribute_boperationright. pfa_gap_distribute_boperationright + S (pfp_source_distribute_b) = (p)) /\ ((((exists pfa_gap_distribute_boperationresultbound. pfa_gap_distribute_boperationresultbound + S (pfp_value_distribute_b) = (p)) /\ ((exists pfa_offset_left_distribute_boperationresultcongruence pfa_offset_right_distribute_boperationresultcongruence. ((k) * (pfp_source_distribute_b)) + (p) * pfa_offset_left_distribute_boperationresultcongruence = (pfp_value_distribute_b) + (p) * pfa_offset_right_distribute_boperationresultcongruence))))))))))))))))) -> (forall pfp_index_distribute_right. (exists pfa_gap_distribute_rightindex. pfa_gap_distribute_rightindex + S (pfp_index_distribute_right) = (l)) -> exists pfp_left_distribute_right pfp_right_distribute_right pfp_value_distribute_right. ((((exists ff_h_pfp_distribute_rightleft. ff_h_pfp_distribute_rightleft + S (pfp_left_distribute_right) = S ((S (pfp_index_distribute_right)) * xc)) /\ exists ff_q_pfp_distribute_rightleft. xb = ff_q_pfp_distribute_rightleft * S ((S (pfp_index_distribute_right)) * xc) + (pfp_left_distribute_right))) /\ (((((exists ff_h_pfp_distribute_rightright. ff_h_pfp_distribute_rightright + S (pfp_right_distribute_right) = S ((S (pfp_index_distribute_right)) * yc)) /\ exists ff_q_pfp_distribute_rightright. yb = ff_q_pfp_distribute_rightright * S ((S (pfp_index_distribute_right)) * yc) + (pfp_right_distribute_right))) /\ (((((exists ff_h_pfp_distribute_righttarget. ff_h_pfp_distribute_righttarget + S (pfp_value_distribute_right) = S ((S (pfp_index_distribute_right)) * vc)) /\ exists ff_q_pfp_distribute_righttarget. vb = ff_q_pfp_distribute_righttarget * S ((S (pfp_index_distribute_right)) * vc) + (pfp_value_distribute_right))) /\ ((((exists pfa_gap_distribute_rightoperationleft. pfa_gap_distribute_rightoperationleft + S (pfp_left_distribute_right) = (p)) /\ (((exists pfa_gap_distribute_rightoperationright. pfa_gap_distribute_rightoperationright + S (pfp_right_distribute_right) = (p)) /\ ((((exists pfa_gap_distribute_rightoperationresultbound. pfa_gap_distribute_rightoperationresultbound + S (pfp_value_distribute_right) = (p)) /\ ((exists pfa_offset_left_distribute_rightoperationresultcongruence pfa_offset_right_distribute_rightoperationresultcongruence. ((pfp_left_distribute_right) + (pfp_right_distribute_right)) + (p) * pfa_offset_left_distribute_rightoperationresultcongruence = (pfp_value_distribute_right) + (p) * pfa_offset_right_distribute_rightoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_distribute_result mdr_a_pfp_distribute_result. (exists mdr_gap_pfp_distribute_resultb. mdr_gap_pfp_distribute_resultb + S (mdr_i_pfp_distribute_result) = (l)) -> (((exists ff_h_mdr_pfp_distribute_resulto. ff_h_mdr_pfp_distribute_resulto + S (mdr_a_pfp_distribute_result) = S ((S (mdr_i_pfp_distribute_result)) * uc)) /\ exists ff_q_mdr_pfp_distribute_resulto. ub = ff_q_mdr_pfp_distribute_resulto * S ((S (mdr_i_pfp_distribute_result)) * uc) + (mdr_a_pfp_distribute_result))) -> (((exists ff_h_mdr_pfp_distribute_resultn. ff_h_mdr_pfp_distribute_resultn + S (mdr_a_pfp_distribute_result) = S ((S (mdr_i_pfp_distribute_result)) * vc)) /\ exists ff_q_mdr_pfp_distribute_resultn. vb = ff_q_mdr_pfp_distribute_resultn * S ((S (mdr_i_pfp_distribute_result)) * vc) + (mdr_a_pfp_distribute_result))))