factor_permutation_matched_append_exists

forall b c d e u v l p. (((((forall pfp_i_exists_append_oldpermutationbounded. (exists pfp_gap_exists_append_oldpermutationboundedindex. pfp_gap_exists_append_oldpermutationboundedindex + S (pfp_i_exists_append_oldpermutationbounded) = (l)) -> exists pfp_a_exists_append_oldpermutationbounded. (((exists ff_h_pfp_exists_append_oldpermutationboundedentry. ff_h_pfp_exists_append_oldpermutationboundedentry + S (pfp_a_exists_append_oldpermutationbounded) = S ((S (pfp_i_exists_append_oldpermutationbounded)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationboundedentry. u = ff_q_pfp_exists_append_oldpermutationboundedentry * S ((S (pfp_i_exists_append_oldpermutationbounded)) * v) + (pfp_a_exists_append_oldpermutationbounded))) /\ (exists pfp_gap_exists_append_oldpermutationboundedvalue. pfp_gap_exists_append_oldpermutationboundedvalue + S (pfp_a_exists_append_oldpermutationbounded) = (l))) /\ (((forall pfp_i_exists_append_oldpermutationinjective pfp_j_exists_append_oldpermutationinjective pfp_a_exists_append_oldpermutationinjective. (exists pfp_gap_exists_append_oldpermutationinjectivefirst. pfp_gap_exists_append_oldpermutationinjectivefirst + S (pfp_i_exists_append_oldpermutationinjective) = (l)) -> (exists pfp_gap_exists_append_oldpermutationinjectivesecond. pfp_gap_exists_append_oldpermutationinjectivesecond + S (pfp_j_exists_append_oldpermutationinjective) = (l)) -> (((exists ff_h_pfp_exists_append_oldpermutationinjectiveleft. ff_h_pfp_exists_append_oldpermutationinjectiveleft + S (pfp_a_exists_append_oldpermutationinjective) = S ((S (pfp_i_exists_append_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationinjectiveleft. u = ff_q_pfp_exists_append_oldpermutationinjectiveleft * S ((S (pfp_i_exists_append_oldpermutationinjective)) * v) + (pfp_a_exists_append_oldpermutationinjective))) -> (((exists ff_h_pfp_exists_append_oldpermutationinjectiveright. ff_h_pfp_exists_append_oldpermutationinjectiveright + S (pfp_a_exists_append_oldpermutationinjective) = S ((S (pfp_j_exists_append_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationinjectiveright. u = ff_q_pfp_exists_append_oldpermutationinjectiveright * S ((S (pfp_j_exists_append_oldpermutationinjective)) * v) + (pfp_a_exists_append_oldpermutationinjective))) -> pfp_i_exists_append_oldpermutationinjective = pfp_j_exists_append_oldpermutationinjective) /\ (forall pfp_a_exists_append_oldpermutationsurjective. (exists pfp_gap_exists_append_oldpermutationsurjectivevalue. pfp_gap_exists_append_oldpermutationsurjectivevalue + S (pfp_a_exists_append_oldpermutationsurjective) = (l)) -> exists pfp_i_exists_append_oldpermutationsurjective. (exists pfp_gap_exists_append_oldpermutationsurjectiveindex. pfp_gap_exists_append_oldpermutationsurjectiveindex + S (pfp_i_exists_append_oldpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_exists_append_oldpermutationsurjectiveentry. ff_h_pfp_exists_append_oldpermutationsurjectiveentry + S (pfp_a_exists_append_oldpermutationsurjective) = S ((S (pfp_i_exists_append_oldpermutationsurjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationsurjectiveentry. u = ff_q_pfp_exists_append_oldpermutationsurjectiveentry * S ((S (pfp_i_exists_append_oldpermutationsurjective)) * v) + (pfp_a_exists_append_oldpermutationsurjective)))))))) /\ (forall pfp_i_exists_append_oldmatching pfp_j_exists_append_oldmatching pfp_a_exists_append_oldmatching. (exists pfp_gap_exists_append_oldmatchingbound. pfp_gap_exists_append_oldmatchingbound + S (pfp_i_exists_append_oldmatching) = (l)) -> (((exists ff_h_pfp_exists_append_oldmatchingmap. ff_h_pfp_exists_append_oldmatchingmap + S (pfp_j_exists_append_oldmatching) = S ((S (pfp_i_exists_append_oldmatching)) * v)) /\ exists ff_q_pfp_exists_append_oldmatchingmap. u = ff_q_pfp_exists_append_oldmatchingmap * S ((S (pfp_i_exists_append_oldmatching)) * v) + (pfp_j_exists_append_oldmatching))) -> (((exists ff_h_pfp_exists_append_oldmatchingsource. ff_h_pfp_exists_append_oldmatchingsource + S (pfp_a_exists_append_oldmatching) = S ((S (pfp_i_exists_append_oldmatching)) * c)) /\ exists ff_q_pfp_exists_append_oldmatchingsource. b = ff_q_pfp_exists_append_oldmatchingsource * S ((S (pfp_i_exists_append_oldmatching)) * c) + (pfp_a_exists_append_oldmatching))) -> (((exists ff_h_pfp_exists_append_oldmatchingtarget. ff_h_pfp_exists_append_oldmatchingtarget + S (pfp_a_exists_append_oldmatching) = S ((S (pfp_j_exists_append_oldmatching)) * e)) /\ exists ff_q_pfp_exists_append_oldmatchingtarget. d = ff_q_pfp_exists_append_oldmatchingtarget * S ((S (pfp_j_exists_append_oldmatching)) * e) + (pfp_a_exists_append_oldmatching)))))) -> (((exists ff_h_pfp_exists_append_left. ff_h_pfp_exists_append_left + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_exists_append_left. b = ff_q_pfp_exists_append_left * S ((S (l)) * c) + (p))) -> (((exists ff_h_pfp_exists_append_right. ff_h_pfp_exists_append_right + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_exists_append_right. d = ff_q_pfp_exists_append_right * S ((S (l)) * e) + (p))) -> exists U V. (((((forall pfp_i_exists_append_newpermutationbounded. (exists pfp_gap_exists_append_newpermutationboundedindex. pfp_gap_exists_append_newpermutationboundedindex + S (pfp_i_exists_append_newpermutationbounded) = (S l)) -> exists pfp_a_exists_append_newpermutationbounded. (((exists ff_h_pfp_exists_append_newpermutationboundedentry. ff_h_pfp_exists_append_newpermutationboundedentry + S (pfp_a_exists_append_newpermutationbounded) = S ((S (pfp_i_exists_append_newpermutationbounded)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationboundedentry. U = ff_q_pfp_exists_append_newpermutationboundedentry * S ((S (pfp_i_exists_append_newpermutationbounded)) * V) + (pfp_a_exists_append_newpermutationbounded))) /\ (exists pfp_gap_exists_append_newpermutationboundedvalue. pfp_gap_exists_append_newpermutationboundedvalue + S (pfp_a_exists_append_newpermutationbounded) = (S l))) /\ (((forall pfp_i_exists_append_newpermutationinjective pfp_j_exists_append_newpermutationinjective pfp_a_exists_append_newpermutationinjective. (exists pfp_gap_exists_append_newpermutationinjectivefirst. pfp_gap_exists_append_newpermutationinjectivefirst + S (pfp_i_exists_append_newpermutationinjective) = (S l)) -> (exists pfp_gap_exists_append_newpermutationinjectivesecond. pfp_gap_exists_append_newpermutationinjectivesecond + S (pfp_j_exists_append_newpermutationinjective) = (S l)) -> (((exists ff_h_pfp_exists_append_newpermutationinjectiveleft. ff_h_pfp_exists_append_newpermutationinjectiveleft + S (pfp_a_exists_append_newpermutationinjective) = S ((S (pfp_i_exists_append_newpermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationinjectiveleft. U = ff_q_pfp_exists_append_newpermutationinjectiveleft * S ((S (pfp_i_exists_append_newpermutationinjective)) * V) + (pfp_a_exists_append_newpermutationinjective))) -> (((exists ff_h_pfp_exists_append_newpermutationinjectiveright. ff_h_pfp_exists_append_newpermutationinjectiveright + S (pfp_a_exists_append_newpermutationinjective) = S ((S (pfp_j_exists_append_newpermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationinjectiveright. U = ff_q_pfp_exists_append_newpermutationinjectiveright * S ((S (pfp_j_exists_append_newpermutationinjective)) * V) + (pfp_a_exists_append_newpermutationinjective))) -> pfp_i_exists_append_newpermutationinjective = pfp_j_exists_append_newpermutationinjective) /\ (forall pfp_a_exists_append_newpermutationsurjective. (exists pfp_gap_exists_append_newpermutationsurjectivevalue. pfp_gap_exists_append_newpermutationsurjectivevalue + S (pfp_a_exists_append_newpermutationsurjective) = (S l)) -> exists pfp_i_exists_append_newpermutationsurjective. (exists pfp_gap_exists_append_newpermutationsurjectiveindex. pfp_gap_exists_append_newpermutationsurjectiveindex + S (pfp_i_exists_append_newpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_exists_append_newpermutationsurjectiveentry. ff_h_pfp_exists_append_newpermutationsurjectiveentry + S (pfp_a_exists_append_newpermutationsurjective) = S ((S (pfp_i_exists_append_newpermutationsurjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationsurjectiveentry. U = ff_q_pfp_exists_append_newpermutationsurjectiveentry * S ((S (pfp_i_exists_append_newpermutationsurjective)) * V) + (pfp_a_exists_append_newpermutationsurjective)))))))) /\ (forall pfp_i_exists_append_newmatching pfp_j_exists_append_newmatching pfp_a_exists_append_newmatching. (exists pfp_gap_exists_append_newmatchingbound. pfp_gap_exists_append_newmatchingbound + S (pfp_i_exists_append_newmatching) = (S l)) -> (((exists ff_h_pfp_exists_append_newmatchingmap. ff_h_pfp_exists_append_newmatchingmap + S (pfp_j_exists_append_newmatching) = S ((S (pfp_i_exists_append_newmatching)) * V)) /\ exists ff_q_pfp_exists_append_newmatchingmap. U = ff_q_pfp_exists_append_newmatchingmap * S ((S (pfp_i_exists_append_newmatching)) * V) + (pfp_j_exists_append_newmatching))) -> (((exists ff_h_pfp_exists_append_newmatchingsource. ff_h_pfp_exists_append_newmatchingsource + S (pfp_a_exists_append_newmatching) = S ((S (pfp_i_exists_append_newmatching)) * c)) /\ exists ff_q_pfp_exists_append_newmatchingsource. b = ff_q_pfp_exists_append_newmatchingsource * S ((S (pfp_i_exists_append_newmatching)) * c) + (pfp_a_exists_append_newmatching))) -> (((exists ff_h_pfp_exists_append_newmatchingtarget. ff_h_pfp_exists_append_newmatchingtarget + S (pfp_a_exists_append_newmatching) = S ((S (pfp_j_exists_append_newmatching)) * e)) /\ exists ff_q_pfp_exists_append_newmatchingtarget. d = ff_q_pfp_exists_append_newmatchingtarget * S ((S (pfp_j_exists_append_newmatching)) * e) + (pfp_a_exists_append_newmatching))))))