prime_field_right_table_distributive

forall p A D M E a b c s x y u v. (forall pft_index_righttable_distributive_add. (exists pfa_gap_righttable_distributive_addprefix. pfa_gap_righttable_distributive_addprefix + S (pft_index_righttable_distributive_add) = ((p) * (p))) -> exists pft_value_righttable_distributive_add. (((((exists ff_h_pft_righttable_distributive_addpointentry. ff_h_pft_righttable_distributive_addpointentry + S (pft_value_righttable_distributive_add) = S ((S (pft_index_righttable_distributive_add)) * D)) /\ exists ff_q_pft_righttable_distributive_addpointentry. A = ff_q_pft_righttable_distributive_addpointentry * S ((S (pft_index_righttable_distributive_add)) * D) + (pft_value_righttable_distributive_add))) /\ ((exists pft_row_righttable_distributive_addpointvalue pft_column_righttable_distributive_addpointvalue. (((pft_index_righttable_distributive_add) = pft_row_righttable_distributive_addpointvalue * (p) + pft_column_righttable_distributive_addpointvalue) /\ ((((exists pfa_gap_righttable_distributive_addpointvalueoperationleft. pfa_gap_righttable_distributive_addpointvalueoperationleft + S (pft_row_righttable_distributive_addpointvalue) = (p)) /\ (((exists pfa_gap_righttable_distributive_addpointvalueoperationright. pfa_gap_righttable_distributive_addpointvalueoperationright + S (pft_column_righttable_distributive_addpointvalue) = (p)) /\ ((((exists pfa_gap_righttable_distributive_addpointvalueoperationresultbound. pfa_gap_righttable_distributive_addpointvalueoperationresultbound + S (pft_value_righttable_distributive_add) = (p)) /\ ((exists pfa_offset_left_righttable_distributive_addpointvalueoperationresultcongruence pfa_offset_right_righttable_distributive_addpointvalueoperationresultcongruence. ((pft_row_righttable_distributive_addpointvalue) + (pft_column_righttable_distributive_addpointvalue)) + (p) * pfa_offset_left_righttable_distributive_addpointvalueoperationresultcongruence = (pft_value_righttable_distributive_add) + (p) * pfa_offset_right_righttable_distributive_addpointvalueoperationresultcongruence)))))))))))))))) -> (forall pft_index_righttable_distributive_mul. (exists pfa_gap_righttable_distributive_mulprefix. pfa_gap_righttable_distributive_mulprefix + S (pft_index_righttable_distributive_mul) = ((p) * (p))) -> exists pft_value_righttable_distributive_mul. (((((exists ff_h_pft_righttable_distributive_mulpointentry. ff_h_pft_righttable_distributive_mulpointentry + S (pft_value_righttable_distributive_mul) = S ((S (pft_index_righttable_distributive_mul)) * E)) /\ exists ff_q_pft_righttable_distributive_mulpointentry. M = ff_q_pft_righttable_distributive_mulpointentry * S ((S (pft_index_righttable_distributive_mul)) * E) + (pft_value_righttable_distributive_mul))) /\ ((exists pft_row_righttable_distributive_mulpointvalue pft_column_righttable_distributive_mulpointvalue. (((pft_index_righttable_distributive_mul) = pft_row_righttable_distributive_mulpointvalue * (p) + pft_column_righttable_distributive_mulpointvalue) /\ ((((exists pfa_gap_righttable_distributive_mulpointvalueoperationleft. pfa_gap_righttable_distributive_mulpointvalueoperationleft + S (pft_row_righttable_distributive_mulpointvalue) = (p)) /\ (((exists pfa_gap_righttable_distributive_mulpointvalueoperationright. pfa_gap_righttable_distributive_mulpointvalueoperationright + S (pft_column_righttable_distributive_mulpointvalue) = (p)) /\ ((((exists pfa_gap_righttable_distributive_mulpointvalueoperationresultbound. pfa_gap_righttable_distributive_mulpointvalueoperationresultbound + S (pft_value_righttable_distributive_mul) = (p)) /\ ((exists pfa_offset_left_righttable_distributive_mulpointvalueoperationresultcongruence pfa_offset_right_righttable_distributive_mulpointvalueoperationresultcongruence. ((pft_row_righttable_distributive_mulpointvalue) * (pft_column_righttable_distributive_mulpointvalue)) + (p) * pfa_offset_left_righttable_distributive_mulpointvalueoperationresultcongruence = (pft_value_righttable_distributive_mul) + (p) * pfa_offset_right_righttable_distributive_mulpointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_righttable_distributive_a. pfa_gap_righttable_distributive_a + S (a) = (p)) -> (exists pfa_gap_righttable_distributive_b. pfa_gap_righttable_distributive_b + S (b) = (p)) -> (exists pfa_gap_righttable_distributive_c. pfa_gap_righttable_distributive_c + S (c) = (p)) -> (((exists ff_h_pft_righttable_distributive_sum. ff_h_pft_righttable_distributive_sum + S (s) = S ((S (b*p+c)) * D)) /\ exists ff_q_pft_righttable_distributive_sum. A = ff_q_pft_righttable_distributive_sum * S ((S (b*p+c)) * D) + (s))) -> (((exists ff_h_pft_righttable_distributive_left. ff_h_pft_righttable_distributive_left + S (u) = S ((S (s*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_left. M = ff_q_pft_righttable_distributive_left * S ((S (s*p+a)) * E) + (u))) -> (((exists ff_h_pft_righttable_distributive_first. ff_h_pft_righttable_distributive_first + S (x) = S ((S (b*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_first. M = ff_q_pft_righttable_distributive_first * S ((S (b*p+a)) * E) + (x))) -> (((exists ff_h_pft_righttable_distributive_second. ff_h_pft_righttable_distributive_second + S (y) = S ((S (c*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_second. M = ff_q_pft_righttable_distributive_second * S ((S (c*p+a)) * E) + (y))) -> (((exists ff_h_pft_righttable_distributive_right. ff_h_pft_righttable_distributive_right + S (v) = S ((S (x*p+y)) * D)) /\ exists ff_q_pft_righttable_distributive_right. A = ff_q_pft_righttable_distributive_right * S ((S (x*p+y)) * D) + (v))) -> u = v