Reused convolution definition DAG

exists h. h + a = b

exists h. h + S a = b

((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))

exists ff_u_defined_sum ff_v_defined_sum. ((((exists ff_h_defined_sum_start. ff_h_defined_sum_start + S (0) = S ((S (0)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_start. ff_u_defined_sum = ff_q_defined_sum_start * S ((S (0)) * ff_v_defined_sum) + (0))) /\ ((((exists ff_h_defined_sum_terminal. ff_h_defined_sum_terminal + S (z) = S ((S (l)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_terminal. ff_u_defined_sum = ff_q_defined_sum_terminal * S ((S (l)) * ff_v_defined_sum) + (z))) /\ forall ff_i_defined_sum. (exists ff_lt_defined_sum_bound. ff_lt_defined_sum_bound + S ff_i_defined_sum = l) -> exists ff_a_defined_sum ff_r_defined_sum ff_s_defined_sum. ((((exists ff_h_defined_sum_summand. ff_h_defined_sum_summand + S (ff_a_defined_sum) = S ((S (ff_i_defined_sum)) * c)) /\ exists ff_q_defined_sum_summand. b = ff_q_defined_sum_summand * S ((S (ff_i_defined_sum)) * c) + (ff_a_defined_sum))) /\ ((((exists ff_h_defined_sum_partial. ff_h_defined_sum_partial + S (ff_r_defined_sum) = S ((S (ff_i_defined_sum)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_partial. ff_u_defined_sum = ff_q_defined_sum_partial * S ((S (ff_i_defined_sum)) * ff_v_defined_sum) + (ff_r_defined_sum))) /\ ((((exists ff_h_defined_sum_successor. ff_h_defined_sum_successor + S (ff_s_defined_sum) = S ((S (S ff_i_defined_sum)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_successor. ff_u_defined_sum = ff_q_defined_sum_successor * S ((S (S ff_i_defined_sum)) * ff_v_defined_sum) + (ff_s_defined_sum))) /\ ff_s_defined_sum = ff_r_defined_sum + ff_a_defined_sum)))))

forall ff_i_defined_repeat. (exists ff_lt_defined_repeat_bound. ff_lt_defined_repeat_bound + S ff_i_defined_repeat = l) -> (((exists ff_h_defined_repeat_decoded. ff_h_defined_repeat_decoded + S (a) = S ((S (ff_i_defined_repeat)) * c)) /\ exists ff_q_defined_repeat_decoded. b = ff_q_defined_repeat_decoded * S ((S (ff_i_defined_repeat)) * c) + (a)))

(((exists pfa_gap_lowercontinuationinside. pfa_gap_lowercontinuationinside + S ((i)) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S ((a)) = S ((S ((i))) * (c))) /\ exists ff_q_pfp_lowercontinuationentry. (b) = ff_q_pfp_lowercontinuationentry * S ((S ((i))) * (c)) + ((a))))))) \/ (((exists pfc_gap_lowercontinuationoutside. pfc_gap_lowercontinuationoutside+((L))=((i))) /\ ((((a))=0))))

exists pfc_complement_lowercontinuation pfc_left_lowercontinuation pfc_right_lowercontinuation. ((((j))+pfc_complement_lowercontinuation=((i))) /\ ((((((exists pfa_gap_lowercontinuationleftinside. pfa_gap_lowercontinuationleftinside + S ((j)) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationleftentry. ff_h_pfp_lowercontinuationleftentry + S (pfc_left_lowercontinuation) = S ((S ((j))) * (ac))) /\ exists ff_q_pfp_lowercontinuationleftentry. (ab) = ff_q_pfp_lowercontinuationleftentry * S ((S ((j))) * (ac)) + (pfc_left_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationleftoutside. pfc_gap_lowercontinuationleftoutside+((L))=((j))) /\ (((pfc_left_lowercontinuation)=0))))) /\ ((((((exists pfa_gap_lowercontinuationrightinside. pfa_gap_lowercontinuationrightinside + S (pfc_complement_lowercontinuation) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationrightentry. ff_h_pfp_lowercontinuationrightentry + S (pfc_right_lowercontinuation) = S ((S (pfc_complement_lowercontinuation)) * (bc))) /\ exists ff_q_pfp_lowercontinuationrightentry. (bb) = ff_q_pfp_lowercontinuationrightentry * S ((S (pfc_complement_lowercontinuation)) * (bc)) + (pfc_right_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationrightoutside. pfc_gap_lowercontinuationrightoutside+((M))=(pfc_complement_lowercontinuation)) /\ (((pfc_right_lowercontinuation)=0))))) /\ ((((t))=pfc_left_lowercontinuation*pfc_right_lowercontinuation)))))))

forall pfc_index_lowercontinuation. (exists pfa_gap_lowercontinuationbound. pfa_gap_lowercontinuationbound + S (pfc_index_lowercontinuation) = ((l))) -> exists pfc_value_lowercontinuation. ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S (pfc_value_lowercontinuation) = S ((S (pfc_index_lowercontinuation)) * (dc))) /\ exists ff_q_pfp_lowercontinuationentry. (db) = ff_q_pfp_lowercontinuationentry * S ((S (pfc_index_lowercontinuation)) * (dc)) + (pfc_value_lowercontinuation))) /\ ((exists pfc_complement_lowercontinuationterm pfc_left_lowercontinuationterm pfc_right_lowercontinuationterm. (((pfc_index_lowercontinuation)+pfc_complement_lowercontinuationterm=((i))) /\ ((((((exists pfa_gap_lowercontinuationtermleftinside. pfa_gap_lowercontinuationtermleftinside + S (pfc_index_lowercontinuation) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationtermleftentry. ff_h_pfp_lowercontinuationtermleftentry + S (pfc_left_lowercontinuationterm) = S ((S (pfc_index_lowercontinuation)) * (ac))) /\ exists ff_q_pfp_lowercontinuationtermleftentry. (ab) = ff_q_pfp_lowercontinuationtermleftentry * S ((S (pfc_index_lowercontinuation)) * (ac)) + (pfc_left_lowercontinuationterm)))))) \/ (((exists pfc_gap_lowercontinuationtermleftoutside. pfc_gap_lowercontinuationtermleftoutside+((L))=(pfc_index_lowercontinuation)) /\ (((pfc_left_lowercontinuationterm)=0))))) /\ ((((((exists pfa_gap_lowercontinuationtermrightinside. pfa_gap_lowercontinuationtermrightinside + S (pfc_complement_lowercontinuationterm) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationtermrightentry. ff_h_pfp_lowercontinuationtermrightentry + S (pfc_right_lowercontinuationterm) = S ((S (pfc_complement_lowercontinuationterm)) * (bc))) /\ exists ff_q_pfp_lowercontinuationtermrightentry. (bb) = ff_q_pfp_lowercontinuationtermrightentry * S ((S (pfc_complement_lowercontinuationterm)) * (bc)) + (pfc_right_lowercontinuationterm)))))) \/ (((exists pfc_gap_lowercontinuationtermrightoutside. pfc_gap_lowercontinuationtermrightoutside+((M))=(pfc_complement_lowercontinuationterm)) /\ (((pfc_right_lowercontinuationterm)=0))))) /\ (((pfc_value_lowercontinuation)=pfc_left_lowercontinuationterm*pfc_right_lowercontinuationterm))))))))))