cf_convergent_euclidean_matrix_step_alignment

forall a b s h e L H E k u U v V. (exists cf_gcd_alignment_old. ((((exists ff_h_cf_alignment_old_initial_state. ff_h_cf_alignment_old_initial_state + S (((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_alignment_old_initial_state. h = ff_q_cf_alignment_old_initial_state * S ((S (0)) * e) + (((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_alignment_old_terminal_state. ff_h_cf_alignment_old_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (L)) * e)) /\ exists ff_q_cf_alignment_old_terminal_state. h = ff_q_cf_alignment_old_terminal_state * S ((S (L)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_alignment_old. (exists ff_lt_cf_alignment_old_index. ff_lt_cf_alignment_old_index + S cf_index_alignment_old = L) -> exists cf_old_a_alignment_old cf_old_b_alignment_old cf_tail_alignment_old cf_new_a_alignment_old cf_new_b_alignment_old cf_head_alignment_old cf_quotient_alignment_old. ((((exists ff_h_cf_alignment_old_previous_state. ff_h_cf_alignment_old_previous_state + S (((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) * S ((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) + ((((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))))) = S ((S (cf_index_alignment_old)) * e)) /\ exists ff_q_cf_alignment_old_previous_state. h = ff_q_cf_alignment_old_previous_state * S ((S (cf_index_alignment_old)) * e) + (((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) * S ((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) + ((((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))))))) /\ ((((exists ff_h_cf_alignment_old_following_state. ff_h_cf_alignment_old_following_state + S (((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) * S ((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) + ((((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))))) = S ((S (S cf_index_alignment_old)) * e)) /\ exists ff_q_cf_alignment_old_following_state. h = ff_q_cf_alignment_old_following_state * S ((S (S cf_index_alignment_old)) * e) + (((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) * S ((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) + ((((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))))))) /\ (cf_new_b_alignment_old = cf_old_a_alignment_old /\ (cf_new_a_alignment_old = cf_new_b_alignment_old * cf_quotient_alignment_old + cf_old_b_alignment_old /\ ((exists ff_lt_cf_alignment_old_remainder. ff_lt_cf_alignment_old_remainder + S cf_old_b_alignment_old = cf_new_b_alignment_old) /\ (cf_head_alignment_old = S ((cf_quotient_alignment_old + cf_tail_alignment_old) * S (cf_quotient_alignment_old + cf_tail_alignment_old) + (cf_tail_alignment_old + cf_tail_alignment_old))))))))))) -> (exists cfc_tail_alignment_new. ((exists cfc_state_alignment_newinitial. ((exists cfc_left_alignment_newinitialcode cfc_right_alignment_newinitialcode cfc_matrix_alignment_newinitialcode. ((cfc_left_alignment_newinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_alignment_newinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_alignment_newinitialcode = ((cfc_left_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode)) * S ((cfc_left_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode)) + ((cfc_right_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode))) /\ ((cfc_state_alignment_newinitial) = ((cfc_tail_alignment_new) + (cfc_matrix_alignment_newinitialcode)) * S ((cfc_tail_alignment_new) + (cfc_matrix_alignment_newinitialcode)) + ((cfc_matrix_alignment_newinitialcode) + (cfc_matrix_alignment_newinitialcode))))))) /\ (((exists ff_h_alignment_newinitialentry. ff_h_alignment_newinitialentry + S (cfc_state_alignment_newinitial) = S ((S (0)) * E)) /\ exists ff_q_alignment_newinitialentry. H = ff_q_alignment_newinitialentry * S ((S (0)) * E) + (cfc_state_alignment_newinitial))))) /\ ((exists cfc_state_alignment_newterminal. ((exists cfc_left_alignment_newterminalcode cfc_right_alignment_newterminalcode cfc_matrix_alignment_newterminalcode. ((cfc_left_alignment_newterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_alignment_newterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_alignment_newterminalcode = ((cfc_left_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode)) * S ((cfc_left_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode)) + ((cfc_right_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode))) /\ ((cfc_state_alignment_newterminal) = ((s) + (cfc_matrix_alignment_newterminalcode)) * S ((s) + (cfc_matrix_alignment_newterminalcode)) + ((cfc_matrix_alignment_newterminalcode) + (cfc_matrix_alignment_newterminalcode))))))) /\ (((exists ff_h_alignment_newterminalentry. ff_h_alignment_newterminalentry + S (cfc_state_alignment_newterminal) = S ((S (S k)) * E)) /\ exists ff_q_alignment_newterminalentry. H = ff_q_alignment_newterminalentry * S ((S (S k)) * E) + (cfc_state_alignment_newterminal))))) /\ (forall cfc_index_alignment_new. (exists cfba_gap_alignment_newbound. cfba_gap_alignment_newbound + S (cfc_index_alignment_new) = (S k)) -> exists cfc_old_alignment_new cfc_a_alignment_new cfc_b_alignment_new cfc_c_alignment_new cfc_d_alignment_new cfc_new_alignment_new cfc_quotient_alignment_new. ((exists cfc_state_alignment_newprevious. ((exists cfc_left_alignment_newpreviouscode cfc_right_alignment_newpreviouscode cfc_matrix_alignment_newpreviouscode. ((cfc_left_alignment_newpreviouscode = ((cfc_a_alignment_new) + (cfc_b_alignment_new)) * S ((cfc_a_alignment_new) + (cfc_b_alignment_new)) + ((cfc_b_alignment_new) + (cfc_b_alignment_new))) /\ ((cfc_right_alignment_newpreviouscode = ((cfc_c_alignment_new) + (cfc_d_alignment_new)) * S ((cfc_c_alignment_new) + (cfc_d_alignment_new)) + ((cfc_d_alignment_new) + (cfc_d_alignment_new))) /\ ((cfc_matrix_alignment_newpreviouscode = ((cfc_left_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode)) * S ((cfc_left_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode)) + ((cfc_right_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode))) /\ ((cfc_state_alignment_newprevious) = ((cfc_old_alignment_new) + (cfc_matrix_alignment_newpreviouscode)) * S ((cfc_old_alignment_new) + (cfc_matrix_alignment_newpreviouscode)) + ((cfc_matrix_alignment_newpreviouscode) + (cfc_matrix_alignment_newpreviouscode))))))) /\ (((exists ff_h_alignment_newpreviousentry. ff_h_alignment_newpreviousentry + S (cfc_state_alignment_newprevious) = S ((S (cfc_index_alignment_new)) * E)) /\ exists ff_q_alignment_newpreviousentry. H = ff_q_alignment_newpreviousentry * S ((S (cfc_index_alignment_new)) * E) + (cfc_state_alignment_newprevious))))) /\ ((exists cfc_state_alignment_newfollowing. ((exists cfc_left_alignment_newfollowingcode cfc_right_alignment_newfollowingcode cfc_matrix_alignment_newfollowingcode. ((cfc_left_alignment_newfollowingcode = (((cfc_quotient_alignment_new * cfc_a_alignment_new + cfc_c_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new))) * S (((cfc_quotient_alignment_new * cfc_a_alignment_new + cfc_c_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new))) + (((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new)))) /\ ((cfc_right_alignment_newfollowingcode = ((cfc_a_alignment_new) + (cfc_b_alignment_new)) * S ((cfc_a_alignment_new) + (cfc_b_alignment_new)) + ((cfc_b_alignment_new) + (cfc_b_alignment_new))) /\ ((cfc_matrix_alignment_newfollowingcode = ((cfc_left_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode)) * S ((cfc_left_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode)) + ((cfc_right_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode))) /\ ((cfc_state_alignment_newfollowing) = ((cfc_new_alignment_new) + (cfc_matrix_alignment_newfollowingcode)) * S ((cfc_new_alignment_new) + (cfc_matrix_alignment_newfollowingcode)) + ((cfc_matrix_alignment_newfollowingcode) + (cfc_matrix_alignment_newfollowingcode))))))) /\ (((exists ff_h_alignment_newfollowingentry. ff_h_alignment_newfollowingentry + S (cfc_state_alignment_newfollowing) = S ((S (S cfc_index_alignment_new)) * E)) /\ exists ff_q_alignment_newfollowingentry. H = ff_q_alignment_newfollowingentry * S ((S (S cfc_index_alignment_new)) * E) + (cfc_state_alignment_newfollowing))))) /\ (cfc_new_alignment_new = S ((cfc_quotient_alignment_new + cfc_old_alignment_new) * S (cfc_quotient_alignment_new + cfc_old_alignment_new) + (cfc_old_alignment_new + cfc_old_alignment_new))))))))) -> (exists cfc_r_alignment_result cfc_tail_alignment_result cfc_length_alignment_result cfc_q_alignment_result cfc_p_alignment_result cfc_P_alignment_result cfc_n_alignment_result cfc_N_alignment_result. (((L) = S cfc_length_alignment_result) /\ (((a) = (b) * cfc_q_alignment_result + cfc_r_alignment_result) /\ ((exists cfba_gap_alignment_resultbound. cfba_gap_alignment_resultbound + S (cfc_r_alignment_result) = (b)) /\ ((exists cf_gcd_alignment_resulteuclidean. ((((exists ff_h_cf_alignment_resulteuclidean_initial_state. ff_h_cf_alignment_resulteuclidean_initial_state + S (((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_initial_state. h = ff_q_cf_alignment_resulteuclidean_initial_state * S ((S (0)) * e) + (((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_alignment_resulteuclidean_terminal_state. ff_h_cf_alignment_resulteuclidean_terminal_state + S (((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) * S ((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) + ((((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))))) = S ((S (cfc_length_alignment_result)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_terminal_state. h = ff_q_cf_alignment_resulteuclidean_terminal_state * S ((S (cfc_length_alignment_result)) * e) + (((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) * S ((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) + ((((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))))))) /\ forall cf_index_alignment_resulteuclidean. (exists ff_lt_cf_alignment_resulteuclidean_index. ff_lt_cf_alignment_resulteuclidean_index + S cf_index_alignment_resulteuclidean = cfc_length_alignment_result) -> exists cf_old_a_alignment_resulteuclidean cf_old_b_alignment_resulteuclidean cf_tail_alignment_resulteuclidean cf_new_a_alignment_resulteuclidean cf_new_b_alignment_resulteuclidean cf_head_alignment_resulteuclidean cf_quotient_alignment_resulteuclidean. ((((exists ff_h_cf_alignment_resulteuclidean_previous_state. ff_h_cf_alignment_resulteuclidean_previous_state + S (((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) * S ((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) + ((((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))))) = S ((S (cf_index_alignment_resulteuclidean)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_previous_state. h = ff_q_cf_alignment_resulteuclidean_previous_state * S ((S (cf_index_alignment_resulteuclidean)) * e) + (((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) * S ((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) + ((((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))))))) /\ ((((exists ff_h_cf_alignment_resulteuclidean_following_state. ff_h_cf_alignment_resulteuclidean_following_state + S (((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) * S ((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) + ((((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))))) = S ((S (S cf_index_alignment_resulteuclidean)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_following_state. h = ff_q_cf_alignment_resulteuclidean_following_state * S ((S (S cf_index_alignment_resulteuclidean)) * e) + (((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) * S ((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) + ((((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))))))) /\ (cf_new_b_alignment_resulteuclidean = cf_old_a_alignment_resulteuclidean /\ (cf_new_a_alignment_resulteuclidean = cf_new_b_alignment_resulteuclidean * cf_quotient_alignment_resulteuclidean + cf_old_b_alignment_resulteuclidean /\ ((exists ff_lt_cf_alignment_resulteuclidean_remainder. ff_lt_cf_alignment_resulteuclidean_remainder + S cf_old_b_alignment_resulteuclidean = cf_new_b_alignment_resulteuclidean) /\ (cf_head_alignment_resulteuclidean = S ((cf_quotient_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean) * S (cf_quotient_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean))))))))))) /\ ((exists cfc_tail_alignment_resultmatrix. ((exists cfc_state_alignment_resultmatrixinitial. ((exists cfc_left_alignment_resultmatrixinitialcode cfc_right_alignment_resultmatrixinitialcode cfc_matrix_alignment_resultmatrixinitialcode. ((cfc_left_alignment_resultmatrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_alignment_resultmatrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_alignment_resultmatrixinitialcode = ((cfc_left_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode)) * S ((cfc_left_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode)) + ((cfc_right_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode))) /\ ((cfc_state_alignment_resultmatrixinitial) = ((cfc_tail_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixinitialcode)) * S ((cfc_tail_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixinitialcode)) + ((cfc_matrix_alignment_resultmatrixinitialcode) + (cfc_matrix_alignment_resultmatrixinitialcode))))))) /\ (((exists ff_h_alignment_resultmatrixinitialentry. ff_h_alignment_resultmatrixinitialentry + S (cfc_state_alignment_resultmatrixinitial) = S ((S (0)) * E)) /\ exists ff_q_alignment_resultmatrixinitialentry. H = ff_q_alignment_resultmatrixinitialentry * S ((S (0)) * E) + (cfc_state_alignment_resultmatrixinitial))))) /\ ((exists cfc_state_alignment_resultmatrixterminal. ((exists cfc_left_alignment_resultmatrixterminalcode cfc_right_alignment_resultmatrixterminalcode cfc_matrix_alignment_resultmatrixterminalcode. ((cfc_left_alignment_resultmatrixterminalcode = ((cfc_p_alignment_result) + (cfc_P_alignment_result)) * S ((cfc_p_alignment_result) + (cfc_P_alignment_result)) + ((cfc_P_alignment_result) + (cfc_P_alignment_result))) /\ ((cfc_right_alignment_resultmatrixterminalcode = ((cfc_n_alignment_result) + (cfc_N_alignment_result)) * S ((cfc_n_alignment_result) + (cfc_N_alignment_result)) + ((cfc_N_alignment_result) + (cfc_N_alignment_result))) /\ ((cfc_matrix_alignment_resultmatrixterminalcode = ((cfc_left_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode)) * S ((cfc_left_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode)) + ((cfc_right_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode))) /\ ((cfc_state_alignment_resultmatrixterminal) = ((cfc_tail_alignment_result) + (cfc_matrix_alignment_resultmatrixterminalcode)) * S ((cfc_tail_alignment_result) + (cfc_matrix_alignment_resultmatrixterminalcode)) + ((cfc_matrix_alignment_resultmatrixterminalcode) + (cfc_matrix_alignment_resultmatrixterminalcode))))))) /\ (((exists ff_h_alignment_resultmatrixterminalentry. ff_h_alignment_resultmatrixterminalentry + S (cfc_state_alignment_resultmatrixterminal) = S ((S (k)) * E)) /\ exists ff_q_alignment_resultmatrixterminalentry. H = ff_q_alignment_resultmatrixterminalentry * S ((S (k)) * E) + (cfc_state_alignment_resultmatrixterminal))))) /\ (forall cfc_index_alignment_resultmatrix. (exists cfba_gap_alignment_resultmatrixbound. cfba_gap_alignment_resultmatrixbound + S (cfc_index_alignment_resultmatrix) = (k)) -> exists cfc_old_alignment_resultmatrix cfc_a_alignment_resultmatrix cfc_b_alignment_resultmatrix cfc_c_alignment_resultmatrix cfc_d_alignment_resultmatrix cfc_new_alignment_resultmatrix cfc_quotient_alignment_resultmatrix. ((exists cfc_state_alignment_resultmatrixprevious. ((exists cfc_left_alignment_resultmatrixpreviouscode cfc_right_alignment_resultmatrixpreviouscode cfc_matrix_alignment_resultmatrixpreviouscode. ((cfc_left_alignment_resultmatrixpreviouscode = ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) * S ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) + ((cfc_b_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix))) /\ ((cfc_right_alignment_resultmatrixpreviouscode = ((cfc_c_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix)) * S ((cfc_c_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix)) + ((cfc_d_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix))) /\ ((cfc_matrix_alignment_resultmatrixpreviouscode = ((cfc_left_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode)) * S ((cfc_left_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode)) + ((cfc_right_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode))) /\ ((cfc_state_alignment_resultmatrixprevious) = ((cfc_old_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixpreviouscode)) * S ((cfc_old_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixpreviouscode)) + ((cfc_matrix_alignment_resultmatrixpreviouscode) + (cfc_matrix_alignment_resultmatrixpreviouscode))))))) /\ (((exists ff_h_alignment_resultmatrixpreviousentry. ff_h_alignment_resultmatrixpreviousentry + S (cfc_state_alignment_resultmatrixprevious) = S ((S (cfc_index_alignment_resultmatrix)) * E)) /\ exists ff_q_alignment_resultmatrixpreviousentry. H = ff_q_alignment_resultmatrixpreviousentry * S ((S (cfc_index_alignment_resultmatrix)) * E) + (cfc_state_alignment_resultmatrixprevious))))) /\ ((exists cfc_state_alignment_resultmatrixfollowing. ((exists cfc_left_alignment_resultmatrixfollowingcode cfc_right_alignment_resultmatrixfollowingcode cfc_matrix_alignment_resultmatrixfollowingcode. ((cfc_left_alignment_resultmatrixfollowingcode = (((cfc_quotient_alignment_resultmatrix * cfc_a_alignment_resultmatrix + cfc_c_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix))) * S (((cfc_quotient_alignment_resultmatrix * cfc_a_alignment_resultmatrix + cfc_c_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix))) + (((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix)))) /\ ((cfc_right_alignment_resultmatrixfollowingcode = ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) * S ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) + ((cfc_b_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix))) /\ ((cfc_matrix_alignment_resultmatrixfollowingcode = ((cfc_left_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode)) * S ((cfc_left_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode)) + ((cfc_right_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode))) /\ ((cfc_state_alignment_resultmatrixfollowing) = ((cfc_new_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixfollowingcode)) * S ((cfc_new_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixfollowingcode)) + ((cfc_matrix_alignment_resultmatrixfollowingcode) + (cfc_matrix_alignment_resultmatrixfollowingcode))))))) /\ (((exists ff_h_alignment_resultmatrixfollowingentry. ff_h_alignment_resultmatrixfollowingentry + S (cfc_state_alignment_resultmatrixfollowing) = S ((S (S cfc_index_alignment_resultmatrix)) * E)) /\ exists ff_q_alignment_resultmatrixfollowingentry. H = ff_q_alignment_resultmatrixfollowingentry * S ((S (S cfc_index_alignment_resultmatrix)) * E) + (cfc_state_alignment_resultmatrixfollowing))))) /\ (cfc_new_alignment_resultmatrix = S ((cfc_quotient_alignment_resultmatrix + cfc_old_alignment_resultmatrix) * S (cfc_quotient_alignment_resultmatrix + cfc_old_alignment_resultmatrix) + (cfc_old_alignment_resultmatrix + cfc_old_alignment_resultmatrix))))))))) /\ (((u) = cfc_q_alignment_result * cfc_p_alignment_result + cfc_n_alignment_result) /\ (((U) = cfc_q_alignment_result * cfc_P_alignment_result + cfc_N_alignment_result) /\ (((v) = cfc_p_alignment_result) /\ ((V) = cfc_P_alignment_result))))))))))