cf_convergent_every_valid_matrix_prefix_exists

forall L k a b s h e. (exists cf_gcd_complete_source. ((((exists ff_h_cf_complete_source_initial_state. ff_h_cf_complete_source_initial_state + S (((cf_gcd_complete_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_source) + (((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_complete_source_initial_state. h = ff_q_cf_complete_source_initial_state * S ((S (0)) * e) + (((cf_gcd_complete_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_source) + (((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_complete_source_terminal_state. ff_h_cf_complete_source_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_complete_source_terminal_state. h = ff_q_cf_complete_source_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_complete_source. (exists ff_lt_cf_complete_source_index. ff_lt_cf_complete_source_index + S cf_index_complete_source = L) -> exists cf_old_a_complete_source cf_old_b_complete_source cf_tail_complete_source cf_new_a_complete_source cf_new_b_complete_source cf_head_complete_source cf_quotient_complete_source. ((((exists ff_h_cf_complete_source_previous_state. ff_h_cf_complete_source_previous_state + S (((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) * S ((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) + ((((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))))) = S ((S (cf_index_complete_source)) * e)) /\ exists ff_q_cf_complete_source_previous_state. h = ff_q_cf_complete_source_previous_state * S ((S (cf_index_complete_source)) * e) + (((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) * S ((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) + ((((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))))))) /\ ((((exists ff_h_cf_complete_source_following_state. ff_h_cf_complete_source_following_state + S (((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) * S ((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) + ((((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))))) = S ((S (S cf_index_complete_source)) * e)) /\ exists ff_q_cf_complete_source_following_state. h = ff_q_cf_complete_source_following_state * S ((S (S cf_index_complete_source)) * e) + (((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) * S ((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) + ((((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))))))) /\ (cf_new_b_complete_source = cf_old_a_complete_source /\ (cf_new_a_complete_source = cf_new_b_complete_source * cf_quotient_complete_source + cf_old_b_complete_source /\ ((exists ff_lt_cf_complete_source_remainder. ff_lt_cf_complete_source_remainder + S cf_old_b_complete_source = cf_new_b_complete_source) /\ (cf_head_complete_source = S ((cf_quotient_complete_source + cf_tail_complete_source) * S (cf_quotient_complete_source + cf_tail_complete_source) + (cf_tail_complete_source + cf_tail_complete_source))))))))))) -> (exists cfba_bound_complete_index. cfba_bound_complete_index + (k) = (L)) -> (exists cfc_h_complete_result cfc_e_complete_result cfc_u_complete_result cfc_U_complete_result cfc_v_complete_result cfc_V_complete_result. exists cfc_tail_complete_resultbody. ((exists cfc_state_complete_resultbodyinitial. ((exists cfc_left_complete_resultbodyinitialcode cfc_right_complete_resultbodyinitialcode cfc_matrix_complete_resultbodyinitialcode. ((cfc_left_complete_resultbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_resultbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_resultbodyinitialcode = ((cfc_left_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode)) * S ((cfc_left_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode)) + ((cfc_right_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode))) /\ ((cfc_state_complete_resultbodyinitial) = ((cfc_tail_complete_resultbody) + (cfc_matrix_complete_resultbodyinitialcode)) * S ((cfc_tail_complete_resultbody) + (cfc_matrix_complete_resultbodyinitialcode)) + ((cfc_matrix_complete_resultbodyinitialcode) + (cfc_matrix_complete_resultbodyinitialcode))))))) /\ (((exists ff_h_complete_resultbodyinitialentry. ff_h_complete_resultbodyinitialentry + S (cfc_state_complete_resultbodyinitial) = S ((S (0)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyinitialentry. cfc_h_complete_result = ff_q_complete_resultbodyinitialentry * S ((S (0)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyinitial))))) /\ ((exists cfc_state_complete_resultbodyterminal. ((exists cfc_left_complete_resultbodyterminalcode cfc_right_complete_resultbodyterminalcode cfc_matrix_complete_resultbodyterminalcode. ((cfc_left_complete_resultbodyterminalcode = ((cfc_u_complete_result) + (cfc_U_complete_result)) * S ((cfc_u_complete_result) + (cfc_U_complete_result)) + ((cfc_U_complete_result) + (cfc_U_complete_result))) /\ ((cfc_right_complete_resultbodyterminalcode = ((cfc_v_complete_result) + (cfc_V_complete_result)) * S ((cfc_v_complete_result) + (cfc_V_complete_result)) + ((cfc_V_complete_result) + (cfc_V_complete_result))) /\ ((cfc_matrix_complete_resultbodyterminalcode = ((cfc_left_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode)) * S ((cfc_left_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode)) + ((cfc_right_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode))) /\ ((cfc_state_complete_resultbodyterminal) = ((s) + (cfc_matrix_complete_resultbodyterminalcode)) * S ((s) + (cfc_matrix_complete_resultbodyterminalcode)) + ((cfc_matrix_complete_resultbodyterminalcode) + (cfc_matrix_complete_resultbodyterminalcode))))))) /\ (((exists ff_h_complete_resultbodyterminalentry. ff_h_complete_resultbodyterminalentry + S (cfc_state_complete_resultbodyterminal) = S ((S (k)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyterminalentry. cfc_h_complete_result = ff_q_complete_resultbodyterminalentry * S ((S (k)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyterminal))))) /\ (forall cfc_index_complete_resultbody. (exists cfba_gap_complete_resultbodybound. cfba_gap_complete_resultbodybound + S (cfc_index_complete_resultbody) = (k)) -> exists cfc_old_complete_resultbody cfc_a_complete_resultbody cfc_b_complete_resultbody cfc_c_complete_resultbody cfc_d_complete_resultbody cfc_new_complete_resultbody cfc_quotient_complete_resultbody. ((exists cfc_state_complete_resultbodyprevious. ((exists cfc_left_complete_resultbodypreviouscode cfc_right_complete_resultbodypreviouscode cfc_matrix_complete_resultbodypreviouscode. ((cfc_left_complete_resultbodypreviouscode = ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) * S ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) + ((cfc_b_complete_resultbody) + (cfc_b_complete_resultbody))) /\ ((cfc_right_complete_resultbodypreviouscode = ((cfc_c_complete_resultbody) + (cfc_d_complete_resultbody)) * S ((cfc_c_complete_resultbody) + (cfc_d_complete_resultbody)) + ((cfc_d_complete_resultbody) + (cfc_d_complete_resultbody))) /\ ((cfc_matrix_complete_resultbodypreviouscode = ((cfc_left_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode)) * S ((cfc_left_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode)) + ((cfc_right_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode))) /\ ((cfc_state_complete_resultbodyprevious) = ((cfc_old_complete_resultbody) + (cfc_matrix_complete_resultbodypreviouscode)) * S ((cfc_old_complete_resultbody) + (cfc_matrix_complete_resultbodypreviouscode)) + ((cfc_matrix_complete_resultbodypreviouscode) + (cfc_matrix_complete_resultbodypreviouscode))))))) /\ (((exists ff_h_complete_resultbodypreviousentry. ff_h_complete_resultbodypreviousentry + S (cfc_state_complete_resultbodyprevious) = S ((S (cfc_index_complete_resultbody)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodypreviousentry. cfc_h_complete_result = ff_q_complete_resultbodypreviousentry * S ((S (cfc_index_complete_resultbody)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyprevious))))) /\ ((exists cfc_state_complete_resultbodyfollowing. ((exists cfc_left_complete_resultbodyfollowingcode cfc_right_complete_resultbodyfollowingcode cfc_matrix_complete_resultbodyfollowingcode. ((cfc_left_complete_resultbodyfollowingcode = (((cfc_quotient_complete_resultbody * cfc_a_complete_resultbody + cfc_c_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody))) * S (((cfc_quotient_complete_resultbody * cfc_a_complete_resultbody + cfc_c_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody))) + (((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody)))) /\ ((cfc_right_complete_resultbodyfollowingcode = ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) * S ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) + ((cfc_b_complete_resultbody) + (cfc_b_complete_resultbody))) /\ ((cfc_matrix_complete_resultbodyfollowingcode = ((cfc_left_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode)) * S ((cfc_left_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode)) + ((cfc_right_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode))) /\ ((cfc_state_complete_resultbodyfollowing) = ((cfc_new_complete_resultbody) + (cfc_matrix_complete_resultbodyfollowingcode)) * S ((cfc_new_complete_resultbody) + (cfc_matrix_complete_resultbodyfollowingcode)) + ((cfc_matrix_complete_resultbodyfollowingcode) + (cfc_matrix_complete_resultbodyfollowingcode))))))) /\ (((exists ff_h_complete_resultbodyfollowingentry. ff_h_complete_resultbodyfollowingentry + S (cfc_state_complete_resultbodyfollowing) = S ((S (S cfc_index_complete_resultbody)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyfollowingentry. cfc_h_complete_result = ff_q_complete_resultbodyfollowingentry * S ((S (S cfc_index_complete_resultbody)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyfollowing))))) /\ (cfc_new_complete_resultbody = S ((cfc_quotient_complete_resultbody + cfc_old_complete_resultbody) * S (cfc_quotient_complete_resultbody + cfc_old_complete_resultbody) + (cfc_old_complete_resultbody + cfc_old_complete_resultbody)))))))))