Conservative definition
Parameters: ab, ac, L, bb, bc, M, i, db, dc, l
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))))))))))