factor_permutation_matched_append

Exact expanded first-order arithmetic statement

forall b c d e u v l p. (((((forall pfp_i_matched_oldpermutationbounded. (exists pfp_gap_matched_oldpermutationboundedindex. pfp_gap_matched_oldpermutationboundedindex + S (pfp_i_matched_oldpermutationbounded) = (l)) -> exists pfp_a_matched_oldpermutationbounded. (((exists ff_h_pfp_matched_oldpermutationboundedentry. ff_h_pfp_matched_oldpermutationboundedentry + S (pfp_a_matched_oldpermutationbounded) = S ((S (pfp_i_matched_oldpermutationbounded)) * v)) /\ exists ff_q_pfp_matched_oldpermutationboundedentry. u = ff_q_pfp_matched_oldpermutationboundedentry * S ((S (pfp_i_matched_oldpermutationbounded)) * v) + (pfp_a_matched_oldpermutationbounded))) /\ (exists pfp_gap_matched_oldpermutationboundedvalue. pfp_gap_matched_oldpermutationboundedvalue + S (pfp_a_matched_oldpermutationbounded) = (l))) /\ (((forall pfp_i_matched_oldpermutationinjective pfp_j_matched_oldpermutationinjective pfp_a_matched_oldpermutationinjective. (exists pfp_gap_matched_oldpermutationinjectivefirst. pfp_gap_matched_oldpermutationinjectivefirst + S (pfp_i_matched_oldpermutationinjective) = (l)) -> (exists pfp_gap_matched_oldpermutationinjectivesecond. pfp_gap_matched_oldpermutationinjectivesecond + S (pfp_j_matched_oldpermutationinjective) = (l)) -> (((exists ff_h_pfp_matched_oldpermutationinjectiveleft. ff_h_pfp_matched_oldpermutationinjectiveleft + S (pfp_a_matched_oldpermutationinjective) = S ((S (pfp_i_matched_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_matched_oldpermutationinjectiveleft. u = ff_q_pfp_matched_oldpermutationinjectiveleft * S ((S (pfp_i_matched_oldpermutationinjective)) * v) + (pfp_a_matched_oldpermutationinjective))) -> (((exists ff_h_pfp_matched_oldpermutationinjectiveright. ff_h_pfp_matched_oldpermutationinjectiveright + S (pfp_a_matched_oldpermutationinjective) = S ((S (pfp_j_matched_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_matched_oldpermutationinjectiveright. u = ff_q_pfp_matched_oldpermutationinjectiveright * S ((S (pfp_j_matched_oldpermutationinjective)) * v) + (pfp_a_matched_oldpermutationinjective))) -> pfp_i_matched_oldpermutationinjective = pfp_j_matched_oldpermutationinjective) /\ (forall pfp_a_matched_oldpermutationsurjective. (exists pfp_gap_matched_oldpermutationsurjectivevalue. pfp_gap_matched_oldpermutationsurjectivevalue + S (pfp_a_matched_oldpermutationsurjective) = (l)) -> exists pfp_i_matched_oldpermutationsurjective. (exists pfp_gap_matched_oldpermutationsurjectiveindex. pfp_gap_matched_oldpermutationsurjectiveindex + S (pfp_i_matched_oldpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_matched_oldpermutationsurjectiveentry. ff_h_pfp_matched_oldpermutationsurjectiveentry + S (pfp_a_matched_oldpermutationsurjective) = S ((S (pfp_i_matched_oldpermutationsurjective)) * v)) /\ exists ff_q_pfp_matched_oldpermutationsurjectiveentry. u = ff_q_pfp_matched_oldpermutationsurjectiveentry * S ((S (pfp_i_matched_oldpermutationsurjective)) * v) + (pfp_a_matched_oldpermutationsurjective)))))))) /\ (forall pfp_i_matched_oldmatching pfp_j_matched_oldmatching pfp_a_matched_oldmatching. (exists pfp_gap_matched_oldmatchingbound. pfp_gap_matched_oldmatchingbound + S (pfp_i_matched_oldmatching) = (l)) -> (((exists ff_h_pfp_matched_oldmatchingmap. ff_h_pfp_matched_oldmatchingmap + S (pfp_j_matched_oldmatching) = S ((S (pfp_i_matched_oldmatching)) * v)) /\ exists ff_q_pfp_matched_oldmatchingmap. u = ff_q_pfp_matched_oldmatchingmap * S ((S (pfp_i_matched_oldmatching)) * v) + (pfp_j_matched_oldmatching))) -> (((exists ff_h_pfp_matched_oldmatchingsource. ff_h_pfp_matched_oldmatchingsource + S (pfp_a_matched_oldmatching) = S ((S (pfp_i_matched_oldmatching)) * c)) /\ exists ff_q_pfp_matched_oldmatchingsource. b = ff_q_pfp_matched_oldmatchingsource * S ((S (pfp_i_matched_oldmatching)) * c) + (pfp_a_matched_oldmatching))) -> (((exists ff_h_pfp_matched_oldmatchingtarget. ff_h_pfp_matched_oldmatchingtarget + S (pfp_a_matched_oldmatching) = S ((S (pfp_j_matched_oldmatching)) * e)) /\ exists ff_q_pfp_matched_oldmatchingtarget. d = ff_q_pfp_matched_oldmatchingtarget * S ((S (pfp_j_matched_oldmatching)) * e) + (pfp_a_matched_oldmatching)))))) -> (((exists ff_h_pfp_matched_left. ff_h_pfp_matched_left + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_matched_left. b = ff_q_pfp_matched_left * S ((S (l)) * c) + (p))) -> (((exists ff_h_pfp_matched_right. ff_h_pfp_matched_right + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_matched_right. d = ff_q_pfp_matched_right * S ((S (l)) * e) + (p))) -> exists U V. ((((((forall pfp_i_matched_newpermutationbounded. (exists pfp_gap_matched_newpermutationboundedindex. pfp_gap_matched_newpermutationboundedindex + S (pfp_i_matched_newpermutationbounded) = (S l)) -> exists pfp_a_matched_newpermutationbounded. (((exists ff_h_pfp_matched_newpermutationboundedentry. ff_h_pfp_matched_newpermutationboundedentry + S (pfp_a_matched_newpermutationbounded) = S ((S (pfp_i_matched_newpermutationbounded)) * V)) /\ exists ff_q_pfp_matched_newpermutationboundedentry. U = ff_q_pfp_matched_newpermutationboundedentry * S ((S (pfp_i_matched_newpermutationbounded)) * V) + (pfp_a_matched_newpermutationbounded))) /\ (exists pfp_gap_matched_newpermutationboundedvalue. pfp_gap_matched_newpermutationboundedvalue + S (pfp_a_matched_newpermutationbounded) = (S l))) /\ (((forall pfp_i_matched_newpermutationinjective pfp_j_matched_newpermutationinjective pfp_a_matched_newpermutationinjective. (exists pfp_gap_matched_newpermutationinjectivefirst. pfp_gap_matched_newpermutationinjectivefirst + S (pfp_i_matched_newpermutationinjective) = (S l)) -> (exists pfp_gap_matched_newpermutationinjectivesecond. pfp_gap_matched_newpermutationinjectivesecond + S (pfp_j_matched_newpermutationinjective) = (S l)) -> (((exists ff_h_pfp_matched_newpermutationinjectiveleft. ff_h_pfp_matched_newpermutationinjectiveleft + S (pfp_a_matched_newpermutationinjective) = S ((S (pfp_i_matched_newpermutationinjective)) * V)) /\ exists ff_q_pfp_matched_newpermutationinjectiveleft. U = ff_q_pfp_matched_newpermutationinjectiveleft * S ((S (pfp_i_matched_newpermutationinjective)) * V) + (pfp_a_matched_newpermutationinjective))) -> (((exists ff_h_pfp_matched_newpermutationinjectiveright. ff_h_pfp_matched_newpermutationinjectiveright + S (pfp_a_matched_newpermutationinjective) = S ((S (pfp_j_matched_newpermutationinjective)) * V)) /\ exists ff_q_pfp_matched_newpermutationinjectiveright. U = ff_q_pfp_matched_newpermutationinjectiveright * S ((S (pfp_j_matched_newpermutationinjective)) * V) + (pfp_a_matched_newpermutationinjective))) -> pfp_i_matched_newpermutationinjective = pfp_j_matched_newpermutationinjective) /\ (forall pfp_a_matched_newpermutationsurjective. (exists pfp_gap_matched_newpermutationsurjectivevalue. pfp_gap_matched_newpermutationsurjectivevalue + S (pfp_a_matched_newpermutationsurjective) = (S l)) -> exists pfp_i_matched_newpermutationsurjective. (exists pfp_gap_matched_newpermutationsurjectiveindex. pfp_gap_matched_newpermutationsurjectiveindex + S (pfp_i_matched_newpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_matched_newpermutationsurjectiveentry. ff_h_pfp_matched_newpermutationsurjectiveentry + S (pfp_a_matched_newpermutationsurjective) = S ((S (pfp_i_matched_newpermutationsurjective)) * V)) /\ exists ff_q_pfp_matched_newpermutationsurjectiveentry. U = ff_q_pfp_matched_newpermutationsurjectiveentry * S ((S (pfp_i_matched_newpermutationsurjective)) * V) + (pfp_a_matched_newpermutationsurjective)))))))) /\ (forall pfp_i_matched_newmatching pfp_j_matched_newmatching pfp_a_matched_newmatching. (exists pfp_gap_matched_newmatchingbound. pfp_gap_matched_newmatchingbound + S (pfp_i_matched_newmatching) = (S l)) -> (((exists ff_h_pfp_matched_newmatchingmap. ff_h_pfp_matched_newmatchingmap + S (pfp_j_matched_newmatching) = S ((S (pfp_i_matched_newmatching)) * V)) /\ exists ff_q_pfp_matched_newmatchingmap. U = ff_q_pfp_matched_newmatchingmap * S ((S (pfp_i_matched_newmatching)) * V) + (pfp_j_matched_newmatching))) -> (((exists ff_h_pfp_matched_newmatchingsource. ff_h_pfp_matched_newmatchingsource + S (pfp_a_matched_newmatching) = S ((S (pfp_i_matched_newmatching)) * c)) /\ exists ff_q_pfp_matched_newmatchingsource. b = ff_q_pfp_matched_newmatchingsource * S ((S (pfp_i_matched_newmatching)) * c) + (pfp_a_matched_newmatching))) -> (((exists ff_h_pfp_matched_newmatchingtarget. ff_h_pfp_matched_newmatchingtarget + S (pfp_a_matched_newmatching) = S ((S (pfp_j_matched_newmatching)) * e)) /\ exists ff_q_pfp_matched_newmatchingtarget. d = ff_q_pfp_matched_newmatchingtarget * S ((S (pfp_j_matched_newmatching)) * e) + (pfp_a_matched_newmatching)))))) /\ (((((exists ff_h_pfp_matched_extensionlast. ff_h_pfp_matched_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_matched_extensionlast. U = ff_q_pfp_matched_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_matched_extensionprefix pfp_a_matched_extensionprefix. (exists pfp_gap_matched_extensionprefixbound. pfp_gap_matched_extensionprefixbound + S (pfp_i_matched_extensionprefix) = (l)) -> (((exists ff_h_pfp_matched_extensionprefixold. ff_h_pfp_matched_extensionprefixold + S (pfp_a_matched_extensionprefix) = S ((S (pfp_i_matched_extensionprefix)) * v)) /\ exists ff_q_pfp_matched_extensionprefixold. u = ff_q_pfp_matched_extensionprefixold * S ((S (pfp_i_matched_extensionprefix)) * v) + (pfp_a_matched_extensionprefix))) -> (((exists ff_h_pfp_matched_extensionprefixnew. ff_h_pfp_matched_extensionprefixnew + S (pfp_a_matched_extensionprefix) = S ((S (pfp_i_matched_extensionprefix)) * V)) /\ exists ff_q_pfp_matched_extensionprefixnew. U = ff_q_pfp_matched_extensionprefixnew * S ((S (pfp_i_matched_extensionprefix)) * V) + (pfp_a_matched_extensionprefix)))))))