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