factor_permutation_matched_unswap_exists

forall b c d e D E u v l j p q. (exists pfp_gap_unswap_exists_index. pfp_gap_unswap_exists_index + S (j) = (l)) -> (((((forall pfp_i_unswap_exists_prefixpermutationbounded. (exists pfp_gap_unswap_exists_prefixpermutationboundedindex. pfp_gap_unswap_exists_prefixpermutationboundedindex + S (pfp_i_unswap_exists_prefixpermutationbounded) = (l)) -> exists pfp_a_unswap_exists_prefixpermutationbounded. (((exists ff_h_pfp_unswap_exists_prefixpermutationboundedentry. ff_h_pfp_unswap_exists_prefixpermutationboundedentry + S (pfp_a_unswap_exists_prefixpermutationbounded) = S ((S (pfp_i_unswap_exists_prefixpermutationbounded)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationboundedentry. u = ff_q_pfp_unswap_exists_prefixpermutationboundedentry * S ((S (pfp_i_unswap_exists_prefixpermutationbounded)) * v) + (pfp_a_unswap_exists_prefixpermutationbounded))) /\ (exists pfp_gap_unswap_exists_prefixpermutationboundedvalue. pfp_gap_unswap_exists_prefixpermutationboundedvalue + S (pfp_a_unswap_exists_prefixpermutationbounded) = (l))) /\ (((forall pfp_i_unswap_exists_prefixpermutationinjective pfp_j_unswap_exists_prefixpermutationinjective pfp_a_unswap_exists_prefixpermutationinjective. (exists pfp_gap_unswap_exists_prefixpermutationinjectivefirst. pfp_gap_unswap_exists_prefixpermutationinjectivefirst + S (pfp_i_unswap_exists_prefixpermutationinjective) = (l)) -> (exists pfp_gap_unswap_exists_prefixpermutationinjectivesecond. pfp_gap_unswap_exists_prefixpermutationinjectivesecond + S (pfp_j_unswap_exists_prefixpermutationinjective) = (l)) -> (((exists ff_h_pfp_unswap_exists_prefixpermutationinjectiveleft. ff_h_pfp_unswap_exists_prefixpermutationinjectiveleft + S (pfp_a_unswap_exists_prefixpermutationinjective) = S ((S (pfp_i_unswap_exists_prefixpermutationinjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationinjectiveleft. u = ff_q_pfp_unswap_exists_prefixpermutationinjectiveleft * S ((S (pfp_i_unswap_exists_prefixpermutationinjective)) * v) + (pfp_a_unswap_exists_prefixpermutationinjective))) -> (((exists ff_h_pfp_unswap_exists_prefixpermutationinjectiveright. ff_h_pfp_unswap_exists_prefixpermutationinjectiveright + S (pfp_a_unswap_exists_prefixpermutationinjective) = S ((S (pfp_j_unswap_exists_prefixpermutationinjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationinjectiveright. u = ff_q_pfp_unswap_exists_prefixpermutationinjectiveright * S ((S (pfp_j_unswap_exists_prefixpermutationinjective)) * v) + (pfp_a_unswap_exists_prefixpermutationinjective))) -> pfp_i_unswap_exists_prefixpermutationinjective = pfp_j_unswap_exists_prefixpermutationinjective) /\ (forall pfp_a_unswap_exists_prefixpermutationsurjective. (exists pfp_gap_unswap_exists_prefixpermutationsurjectivevalue. pfp_gap_unswap_exists_prefixpermutationsurjectivevalue + S (pfp_a_unswap_exists_prefixpermutationsurjective) = (l)) -> exists pfp_i_unswap_exists_prefixpermutationsurjective. (exists pfp_gap_unswap_exists_prefixpermutationsurjectiveindex. pfp_gap_unswap_exists_prefixpermutationsurjectiveindex + S (pfp_i_unswap_exists_prefixpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_unswap_exists_prefixpermutationsurjectiveentry. ff_h_pfp_unswap_exists_prefixpermutationsurjectiveentry + S (pfp_a_unswap_exists_prefixpermutationsurjective) = S ((S (pfp_i_unswap_exists_prefixpermutationsurjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationsurjectiveentry. u = ff_q_pfp_unswap_exists_prefixpermutationsurjectiveentry * S ((S (pfp_i_unswap_exists_prefixpermutationsurjective)) * v) + (pfp_a_unswap_exists_prefixpermutationsurjective)))))))) /\ (forall pfp_i_unswap_exists_prefixmatching pfp_j_unswap_exists_prefixmatching pfp_a_unswap_exists_prefixmatching. (exists pfp_gap_unswap_exists_prefixmatchingbound. pfp_gap_unswap_exists_prefixmatchingbound + S (pfp_i_unswap_exists_prefixmatching) = (l)) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingmap. ff_h_pfp_unswap_exists_prefixmatchingmap + S (pfp_j_unswap_exists_prefixmatching) = S ((S (pfp_i_unswap_exists_prefixmatching)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingmap. u = ff_q_pfp_unswap_exists_prefixmatchingmap * S ((S (pfp_i_unswap_exists_prefixmatching)) * v) + (pfp_j_unswap_exists_prefixmatching))) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingsource. ff_h_pfp_unswap_exists_prefixmatchingsource + S (pfp_a_unswap_exists_prefixmatching) = S ((S (pfp_i_unswap_exists_prefixmatching)) * c)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingsource. b = ff_q_pfp_unswap_exists_prefixmatchingsource * S ((S (pfp_i_unswap_exists_prefixmatching)) * c) + (pfp_a_unswap_exists_prefixmatching))) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingtarget. ff_h_pfp_unswap_exists_prefixmatchingtarget + S (pfp_a_unswap_exists_prefixmatching) = S ((S (pfp_j_unswap_exists_prefixmatching)) * E)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingtarget. D = ff_q_pfp_unswap_exists_prefixmatchingtarget * S ((S (pfp_j_unswap_exists_prefixmatching)) * E) + (pfp_a_unswap_exists_prefixmatching)))))) -> (((exists ff_h_pfp_unswap_exists_last. ff_h_pfp_unswap_exists_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_unswap_exists_last. b = ff_q_pfp_unswap_exists_last * S ((S (l)) * c) + (p))) -> (((((exists ff_h_pfp_target_swapoldi. ff_h_pfp_target_swapoldi + S (p) = S ((S (j)) * e)) /\ exists ff_q_pfp_target_swapoldi. d = ff_q_pfp_target_swapoldi * S ((S (j)) * e) + (p))) /\ (((((exists ff_h_pfp_target_swapoldlast. ff_h_pfp_target_swapoldlast + S (q) = S ((S (l)) * e)) /\ exists ff_q_pfp_target_swapoldlast. d = ff_q_pfp_target_swapoldlast * S ((S (l)) * e) + (q))) /\ (((((exists ff_h_pfp_target_swapnewi. ff_h_pfp_target_swapnewi + S (q) = S ((S (j)) * E)) /\ exists ff_q_pfp_target_swapnewi. D = ff_q_pfp_target_swapnewi * S ((S (j)) * E) + (q))) /\ (((((exists ff_h_pfp_target_swapnewlast. ff_h_pfp_target_swapnewlast + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_target_swapnewlast. D = ff_q_pfp_target_swapnewlast * S ((S (l)) * E) + (p))) /\ (forall pfp_j_target_swap pfp_a_target_swap. (exists pfp_gap_target_swapbound. pfp_gap_target_swapbound + S (pfp_j_target_swap) = (S (l))) -> ~(pfp_j_target_swap = j) -> ~(pfp_j_target_swap = l) -> (((exists ff_h_pfp_target_swapold. ff_h_pfp_target_swapold + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * e)) /\ exists ff_q_pfp_target_swapold. d = ff_q_pfp_target_swapold * S ((S (pfp_j_target_swap)) * e) + (pfp_a_target_swap))) -> (((exists ff_h_pfp_target_swapnew. ff_h_pfp_target_swapnew + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * E)) /\ exists ff_q_pfp_target_swapnew. D = ff_q_pfp_target_swapnew * S ((S (pfp_j_target_swap)) * E) + (pfp_a_target_swap)))))))))))) -> exists U V. (((((forall pfp_i_unswap_exists_resultpermutationbounded. (exists pfp_gap_unswap_exists_resultpermutationboundedindex. pfp_gap_unswap_exists_resultpermutationboundedindex + S (pfp_i_unswap_exists_resultpermutationbounded) = (S l)) -> exists pfp_a_unswap_exists_resultpermutationbounded. (((exists ff_h_pfp_unswap_exists_resultpermutationboundedentry. ff_h_pfp_unswap_exists_resultpermutationboundedentry + S (pfp_a_unswap_exists_resultpermutationbounded) = S ((S (pfp_i_unswap_exists_resultpermutationbounded)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationboundedentry. U = ff_q_pfp_unswap_exists_resultpermutationboundedentry * S ((S (pfp_i_unswap_exists_resultpermutationbounded)) * V) + (pfp_a_unswap_exists_resultpermutationbounded))) /\ (exists pfp_gap_unswap_exists_resultpermutationboundedvalue. pfp_gap_unswap_exists_resultpermutationboundedvalue + S (pfp_a_unswap_exists_resultpermutationbounded) = (S l))) /\ (((forall pfp_i_unswap_exists_resultpermutationinjective pfp_j_unswap_exists_resultpermutationinjective pfp_a_unswap_exists_resultpermutationinjective. (exists pfp_gap_unswap_exists_resultpermutationinjectivefirst. pfp_gap_unswap_exists_resultpermutationinjectivefirst + S (pfp_i_unswap_exists_resultpermutationinjective) = (S l)) -> (exists pfp_gap_unswap_exists_resultpermutationinjectivesecond. pfp_gap_unswap_exists_resultpermutationinjectivesecond + S (pfp_j_unswap_exists_resultpermutationinjective) = (S l)) -> (((exists ff_h_pfp_unswap_exists_resultpermutationinjectiveleft. ff_h_pfp_unswap_exists_resultpermutationinjectiveleft + S (pfp_a_unswap_exists_resultpermutationinjective) = S ((S (pfp_i_unswap_exists_resultpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationinjectiveleft. U = ff_q_pfp_unswap_exists_resultpermutationinjectiveleft * S ((S (pfp_i_unswap_exists_resultpermutationinjective)) * V) + (pfp_a_unswap_exists_resultpermutationinjective))) -> (((exists ff_h_pfp_unswap_exists_resultpermutationinjectiveright. ff_h_pfp_unswap_exists_resultpermutationinjectiveright + S (pfp_a_unswap_exists_resultpermutationinjective) = S ((S (pfp_j_unswap_exists_resultpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationinjectiveright. U = ff_q_pfp_unswap_exists_resultpermutationinjectiveright * S ((S (pfp_j_unswap_exists_resultpermutationinjective)) * V) + (pfp_a_unswap_exists_resultpermutationinjective))) -> pfp_i_unswap_exists_resultpermutationinjective = pfp_j_unswap_exists_resultpermutationinjective) /\ (forall pfp_a_unswap_exists_resultpermutationsurjective. (exists pfp_gap_unswap_exists_resultpermutationsurjectivevalue. pfp_gap_unswap_exists_resultpermutationsurjectivevalue + S (pfp_a_unswap_exists_resultpermutationsurjective) = (S l)) -> exists pfp_i_unswap_exists_resultpermutationsurjective. (exists pfp_gap_unswap_exists_resultpermutationsurjectiveindex. pfp_gap_unswap_exists_resultpermutationsurjectiveindex + S (pfp_i_unswap_exists_resultpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_exists_resultpermutationsurjectiveentry. ff_h_pfp_unswap_exists_resultpermutationsurjectiveentry + S (pfp_a_unswap_exists_resultpermutationsurjective) = S ((S (pfp_i_unswap_exists_resultpermutationsurjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationsurjectiveentry. U = ff_q_pfp_unswap_exists_resultpermutationsurjectiveentry * S ((S (pfp_i_unswap_exists_resultpermutationsurjective)) * V) + (pfp_a_unswap_exists_resultpermutationsurjective)))))))) /\ (forall pfp_i_unswap_exists_resultmatching pfp_j_unswap_exists_resultmatching pfp_a_unswap_exists_resultmatching. (exists pfp_gap_unswap_exists_resultmatchingbound. pfp_gap_unswap_exists_resultmatchingbound + S (pfp_i_unswap_exists_resultmatching) = (S l)) -> (((exists ff_h_pfp_unswap_exists_resultmatchingmap. ff_h_pfp_unswap_exists_resultmatchingmap + S (pfp_j_unswap_exists_resultmatching) = S ((S (pfp_i_unswap_exists_resultmatching)) * V)) /\ exists ff_q_pfp_unswap_exists_resultmatchingmap. U = ff_q_pfp_unswap_exists_resultmatchingmap * S ((S (pfp_i_unswap_exists_resultmatching)) * V) + (pfp_j_unswap_exists_resultmatching))) -> (((exists ff_h_pfp_unswap_exists_resultmatchingsource. ff_h_pfp_unswap_exists_resultmatchingsource + S (pfp_a_unswap_exists_resultmatching) = S ((S (pfp_i_unswap_exists_resultmatching)) * c)) /\ exists ff_q_pfp_unswap_exists_resultmatchingsource. b = ff_q_pfp_unswap_exists_resultmatchingsource * S ((S (pfp_i_unswap_exists_resultmatching)) * c) + (pfp_a_unswap_exists_resultmatching))) -> (((exists ff_h_pfp_unswap_exists_resultmatchingtarget. ff_h_pfp_unswap_exists_resultmatchingtarget + S (pfp_a_unswap_exists_resultmatching) = S ((S (pfp_j_unswap_exists_resultmatching)) * e)) /\ exists ff_q_pfp_unswap_exists_resultmatchingtarget. d = ff_q_pfp_unswap_exists_resultmatchingtarget * S ((S (pfp_j_unswap_exists_resultmatching)) * e) + (pfp_a_unswap_exists_resultmatching))))))