prime_field_polynomial_horner_successor_decompose

Exact expanded first-order arithmetic statement

forall p b c t l r. (exists pfh_trace_code_successor_execution pfh_trace_scale_successor_execution. (((exists pfa_gap_successor_executiontracebase. pfa_gap_successor_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_executiontraceinitial. ff_h_pfp_successor_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontraceinitial. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontraceinitial * S ((S (0)) * pfh_trace_scale_successor_execution) + (0))) /\ (((((exists ff_h_pfp_successor_executiontraceterminal. ff_h_pfp_successor_executiontraceterminal + S (r) = S ((S (S l)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontraceterminal. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontraceterminal * S ((S (S l)) * pfh_trace_scale_successor_execution) + (r))) /\ ((forall pfh_index_successor_executiontracesteps. (exists pfa_gap_successor_executiontracestepsindex. pfa_gap_successor_executiontracestepsindex + S (pfh_index_successor_executiontracesteps) = (S l)) -> (exists pfh_coefficient_successor_executiontracestepsstep pfh_before_successor_executiontracestepsstep pfh_after_successor_executiontracestepsstep pfh_product_successor_executiontracestepsstep. ((((exists ff_h_pfp_successor_executiontracestepsstepcoefficient. ff_h_pfp_successor_executiontracestepsstepcoefficient + S (pfh_coefficient_successor_executiontracestepsstep) = S ((S (pfh_index_successor_executiontracesteps)) * c)) /\ exists ff_q_pfp_successor_executiontracestepsstepcoefficient. b = ff_q_pfp_successor_executiontracestepsstepcoefficient * S ((S (pfh_index_successor_executiontracesteps)) * c) + (pfh_coefficient_successor_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_executiontracestepsstepbefore. ff_h_pfp_successor_executiontracestepsstepbefore + S (pfh_before_successor_executiontracestepsstep) = S ((S (pfh_index_successor_executiontracesteps)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontracestepsstepbefore. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontracestepsstepbefore * S ((S (pfh_index_successor_executiontracesteps)) * pfh_trace_scale_successor_execution) + (pfh_before_successor_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_executiontracestepsstepafter. ff_h_pfp_successor_executiontracestepsstepafter + S (pfh_after_successor_executiontracestepsstep) = S ((S (S (pfh_index_successor_executiontracesteps))) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontracestepsstepafter. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontracestepsstepafter * S ((S (S (pfh_index_successor_executiontracesteps))) * pfh_trace_scale_successor_execution) + (pfh_after_successor_executiontracestepsstep))) /\ (((((exists pfa_gap_successor_executiontracestepsstepmultiplyleft. pfa_gap_successor_executiontracestepsstepmultiplyleft + S (pfh_before_successor_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_executiontracestepsstepmultiplyright. pfa_gap_successor_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_executiontracestepsstepmultiplyresultbound. pfa_gap_successor_executiontracestepsstepmultiplyresultbound + S (pfh_product_successor_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_successor_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_successor_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_successor_executiontracestepsstepmultiplyresultcongruence = (pfh_product_successor_executiontracestepsstep) + (p) * pfa_offset_right_successor_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_executiontracestepsstepaddleft. pfa_gap_successor_executiontracestepsstepaddleft + S (pfh_product_successor_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_executiontracestepsstepaddright. pfa_gap_successor_executiontracestepsstepaddright + S (pfh_coefficient_successor_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_executiontracestepsstepaddresultbound. pfa_gap_successor_executiontracestepsstepaddresultbound + S (pfh_after_successor_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_executiontracestepsstepaddresultcongruence pfa_offset_right_successor_executiontracestepsstepaddresultcongruence. ((pfh_product_successor_executiontracestepsstep) + (pfh_coefficient_successor_executiontracestepsstep)) + (p) * pfa_offset_left_successor_executiontracestepsstepaddresultcongruence = (pfh_after_successor_executiontracestepsstep) + (p) * pfa_offset_right_successor_executiontracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> exists a h k. ((((exists ff_h_pfp_successor_coefficient. ff_h_pfp_successor_coefficient + S (a) = S ((S (l)) * c)) /\ exists ff_q_pfp_successor_coefficient. b = ff_q_pfp_successor_coefficient * S ((S (l)) * c) + (a))) /\ (((exists pfh_trace_code_successor_prefix pfh_trace_scale_successor_prefix. (((exists pfa_gap_successor_prefixtracebase. pfa_gap_successor_prefixtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_prefixtraceinitial. ff_h_pfp_successor_prefixtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtraceinitial. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtraceinitial * S ((S (0)) * pfh_trace_scale_successor_prefix) + (0))) /\ (((((exists ff_h_pfp_successor_prefixtraceterminal. ff_h_pfp_successor_prefixtraceterminal + S (h) = S ((S (l)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtraceterminal. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtraceterminal * S ((S (l)) * pfh_trace_scale_successor_prefix) + (h))) /\ ((forall pfh_index_successor_prefixtracesteps. (exists pfa_gap_successor_prefixtracestepsindex. pfa_gap_successor_prefixtracestepsindex + S (pfh_index_successor_prefixtracesteps) = (l)) -> (exists pfh_coefficient_successor_prefixtracestepsstep pfh_before_successor_prefixtracestepsstep pfh_after_successor_prefixtracestepsstep pfh_product_successor_prefixtracestepsstep. ((((exists ff_h_pfp_successor_prefixtracestepsstepcoefficient. ff_h_pfp_successor_prefixtracestepsstepcoefficient + S (pfh_coefficient_successor_prefixtracestepsstep) = S ((S (pfh_index_successor_prefixtracesteps)) * c)) /\ exists ff_q_pfp_successor_prefixtracestepsstepcoefficient. b = ff_q_pfp_successor_prefixtracestepsstepcoefficient * S ((S (pfh_index_successor_prefixtracesteps)) * c) + (pfh_coefficient_successor_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_prefixtracestepsstepbefore. ff_h_pfp_successor_prefixtracestepsstepbefore + S (pfh_before_successor_prefixtracestepsstep) = S ((S (pfh_index_successor_prefixtracesteps)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtracestepsstepbefore. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtracestepsstepbefore * S ((S (pfh_index_successor_prefixtracesteps)) * pfh_trace_scale_successor_prefix) + (pfh_before_successor_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_prefixtracestepsstepafter. ff_h_pfp_successor_prefixtracestepsstepafter + S (pfh_after_successor_prefixtracestepsstep) = S ((S (S (pfh_index_successor_prefixtracesteps))) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtracestepsstepafter. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtracestepsstepafter * S ((S (S (pfh_index_successor_prefixtracesteps))) * pfh_trace_scale_successor_prefix) + (pfh_after_successor_prefixtracestepsstep))) /\ (((((exists pfa_gap_successor_prefixtracestepsstepmultiplyleft. pfa_gap_successor_prefixtracestepsstepmultiplyleft + S (pfh_before_successor_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_prefixtracestepsstepmultiplyright. pfa_gap_successor_prefixtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_prefixtracestepsstepmultiplyresultbound. pfa_gap_successor_prefixtracestepsstepmultiplyresultbound + S (pfh_product_successor_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_prefixtracestepsstepmultiplyresultcongruence pfa_offset_right_successor_prefixtracestepsstepmultiplyresultcongruence. ((pfh_before_successor_prefixtracestepsstep) * (t)) + (p) * pfa_offset_left_successor_prefixtracestepsstepmultiplyresultcongruence = (pfh_product_successor_prefixtracestepsstep) + (p) * pfa_offset_right_successor_prefixtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_prefixtracestepsstepaddleft. pfa_gap_successor_prefixtracestepsstepaddleft + S (pfh_product_successor_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_prefixtracestepsstepaddright. pfa_gap_successor_prefixtracestepsstepaddright + S (pfh_coefficient_successor_prefixtracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_prefixtracestepsstepaddresultbound. pfa_gap_successor_prefixtracestepsstepaddresultbound + S (pfh_after_successor_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_prefixtracestepsstepaddresultcongruence pfa_offset_right_successor_prefixtracestepsstepaddresultcongruence. ((pfh_product_successor_prefixtracestepsstep) + (pfh_coefficient_successor_prefixtracestepsstep)) + (p) * pfa_offset_left_successor_prefixtracestepsstepaddresultcongruence = (pfh_after_successor_prefixtracestepsstep) + (p) * pfa_offset_right_successor_prefixtracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ (((((exists pfa_gap_successor_multiplyleft. pfa_gap_successor_multiplyleft + S (h) = (p)) /\ (((exists pfa_gap_successor_multiplyright. pfa_gap_successor_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_multiplyresultbound. pfa_gap_successor_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_successor_multiplyresultcongruence pfa_offset_right_successor_multiplyresultcongruence. ((h) * (t)) + (p) * pfa_offset_left_successor_multiplyresultcongruence = (k) + (p) * pfa_offset_right_successor_multiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_addleft. pfa_gap_successor_addleft + S (k) = (p)) /\ (((exists pfa_gap_successor_addright. pfa_gap_successor_addright + S (a) = (p)) /\ ((((exists pfa_gap_successor_addresultbound. pfa_gap_successor_addresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_successor_addresultcongruence pfa_offset_right_successor_addresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_successor_addresultcongruence = (r) + (p) * pfa_offset_right_successor_addresultcongruence)))))))))))))))