factor_permutation_empty_matching

Exact expanded first-order arithmetic statement

forall b c d e. (((((forall pfp_i_emptypermutationbounded. (exists pfp_gap_emptypermutationboundedindex. pfp_gap_emptypermutationboundedindex + S (pfp_i_emptypermutationbounded) = (0)) -> exists pfp_a_emptypermutationbounded. (((exists ff_h_pfp_emptypermutationboundedentry. ff_h_pfp_emptypermutationboundedentry + S (pfp_a_emptypermutationbounded) = S ((S (pfp_i_emptypermutationbounded)) * 0)) /\ exists ff_q_pfp_emptypermutationboundedentry. 0 = ff_q_pfp_emptypermutationboundedentry * S ((S (pfp_i_emptypermutationbounded)) * 0) + (pfp_a_emptypermutationbounded))) /\ (exists pfp_gap_emptypermutationboundedvalue. pfp_gap_emptypermutationboundedvalue + S (pfp_a_emptypermutationbounded) = (0))) /\ (((forall pfp_i_emptypermutationinjective pfp_j_emptypermutationinjective pfp_a_emptypermutationinjective. (exists pfp_gap_emptypermutationinjectivefirst. pfp_gap_emptypermutationinjectivefirst + S (pfp_i_emptypermutationinjective) = (0)) -> (exists pfp_gap_emptypermutationinjectivesecond. pfp_gap_emptypermutationinjectivesecond + S (pfp_j_emptypermutationinjective) = (0)) -> (((exists ff_h_pfp_emptypermutationinjectiveleft. ff_h_pfp_emptypermutationinjectiveleft + S (pfp_a_emptypermutationinjective) = S ((S (pfp_i_emptypermutationinjective)) * 0)) /\ exists ff_q_pfp_emptypermutationinjectiveleft. 0 = ff_q_pfp_emptypermutationinjectiveleft * S ((S (pfp_i_emptypermutationinjective)) * 0) + (pfp_a_emptypermutationinjective))) -> (((exists ff_h_pfp_emptypermutationinjectiveright. ff_h_pfp_emptypermutationinjectiveright + S (pfp_a_emptypermutationinjective) = S ((S (pfp_j_emptypermutationinjective)) * 0)) /\ exists ff_q_pfp_emptypermutationinjectiveright. 0 = ff_q_pfp_emptypermutationinjectiveright * S ((S (pfp_j_emptypermutationinjective)) * 0) + (pfp_a_emptypermutationinjective))) -> pfp_i_emptypermutationinjective = pfp_j_emptypermutationinjective) /\ (forall pfp_a_emptypermutationsurjective. (exists pfp_gap_emptypermutationsurjectivevalue. pfp_gap_emptypermutationsurjectivevalue + S (pfp_a_emptypermutationsurjective) = (0)) -> exists pfp_i_emptypermutationsurjective. (exists pfp_gap_emptypermutationsurjectiveindex. pfp_gap_emptypermutationsurjectiveindex + S (pfp_i_emptypermutationsurjective) = (0)) /\ (((exists ff_h_pfp_emptypermutationsurjectiveentry. ff_h_pfp_emptypermutationsurjectiveentry + S (pfp_a_emptypermutationsurjective) = S ((S (pfp_i_emptypermutationsurjective)) * 0)) /\ exists ff_q_pfp_emptypermutationsurjectiveentry. 0 = ff_q_pfp_emptypermutationsurjectiveentry * S ((S (pfp_i_emptypermutationsurjective)) * 0) + (pfp_a_emptypermutationsurjective)))))))) /\ (forall pfp_i_emptymatching pfp_j_emptymatching pfp_a_emptymatching. (exists pfp_gap_emptymatchingbound. pfp_gap_emptymatchingbound + S (pfp_i_emptymatching) = (0)) -> (((exists ff_h_pfp_emptymatchingmap. ff_h_pfp_emptymatchingmap + S (pfp_j_emptymatching) = S ((S (pfp_i_emptymatching)) * 0)) /\ exists ff_q_pfp_emptymatchingmap. 0 = ff_q_pfp_emptymatchingmap * S ((S (pfp_i_emptymatching)) * 0) + (pfp_j_emptymatching))) -> (((exists ff_h_pfp_emptymatchingsource. ff_h_pfp_emptymatchingsource + S (pfp_a_emptymatching) = S ((S (pfp_i_emptymatching)) * c)) /\ exists ff_q_pfp_emptymatchingsource. b = ff_q_pfp_emptymatchingsource * S ((S (pfp_i_emptymatching)) * c) + (pfp_a_emptymatching))) -> (((exists ff_h_pfp_emptymatchingtarget. ff_h_pfp_emptymatchingtarget + S (pfp_a_emptymatching) = S ((S (pfp_j_emptymatching)) * e)) /\ exists ff_q_pfp_emptymatchingtarget. d = ff_q_pfp_emptymatchingtarget * S ((S (pfp_j_emptymatching)) * e) + (pfp_a_emptymatching))))))