cf_convergent_matrix_extend_preserved_prefix

forall t h e k u U v V q s H E. (exists cfc_tail_extend_old. ((exists cfc_state_extend_oldinitial. ((exists cfc_left_extend_oldinitialcode cfc_right_extend_oldinitialcode cfc_matrix_extend_oldinitialcode. ((cfc_left_extend_oldinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_extend_oldinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_extend_oldinitialcode = ((cfc_left_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode)) * S ((cfc_left_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode)) + ((cfc_right_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode))) /\ ((cfc_state_extend_oldinitial) = ((cfc_tail_extend_old) + (cfc_matrix_extend_oldinitialcode)) * S ((cfc_tail_extend_old) + (cfc_matrix_extend_oldinitialcode)) + ((cfc_matrix_extend_oldinitialcode) + (cfc_matrix_extend_oldinitialcode))))))) /\ (((exists ff_h_extend_oldinitialentry. ff_h_extend_oldinitialentry + S (cfc_state_extend_oldinitial) = S ((S (0)) * e)) /\ exists ff_q_extend_oldinitialentry. h = ff_q_extend_oldinitialentry * S ((S (0)) * e) + (cfc_state_extend_oldinitial))))) /\ ((exists cfc_state_extend_oldterminal. ((exists cfc_left_extend_oldterminalcode cfc_right_extend_oldterminalcode cfc_matrix_extend_oldterminalcode. ((cfc_left_extend_oldterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_extend_oldterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_extend_oldterminalcode = ((cfc_left_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode)) * S ((cfc_left_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode)) + ((cfc_right_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode))) /\ ((cfc_state_extend_oldterminal) = ((t) + (cfc_matrix_extend_oldterminalcode)) * S ((t) + (cfc_matrix_extend_oldterminalcode)) + ((cfc_matrix_extend_oldterminalcode) + (cfc_matrix_extend_oldterminalcode))))))) /\ (((exists ff_h_extend_oldterminalentry. ff_h_extend_oldterminalentry + S (cfc_state_extend_oldterminal) = S ((S (k)) * e)) /\ exists ff_q_extend_oldterminalentry. h = ff_q_extend_oldterminalentry * S ((S (k)) * e) + (cfc_state_extend_oldterminal))))) /\ (forall cfc_index_extend_old. (exists cfba_gap_extend_oldbound. cfba_gap_extend_oldbound + S (cfc_index_extend_old) = (k)) -> exists cfc_old_extend_old cfc_a_extend_old cfc_b_extend_old cfc_c_extend_old cfc_d_extend_old cfc_new_extend_old cfc_quotient_extend_old. ((exists cfc_state_extend_oldprevious. ((exists cfc_left_extend_oldpreviouscode cfc_right_extend_oldpreviouscode cfc_matrix_extend_oldpreviouscode. ((cfc_left_extend_oldpreviouscode = ((cfc_a_extend_old) + (cfc_b_extend_old)) * S ((cfc_a_extend_old) + (cfc_b_extend_old)) + ((cfc_b_extend_old) + (cfc_b_extend_old))) /\ ((cfc_right_extend_oldpreviouscode = ((cfc_c_extend_old) + (cfc_d_extend_old)) * S ((cfc_c_extend_old) + (cfc_d_extend_old)) + ((cfc_d_extend_old) + (cfc_d_extend_old))) /\ ((cfc_matrix_extend_oldpreviouscode = ((cfc_left_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode)) * S ((cfc_left_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode)) + ((cfc_right_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode))) /\ ((cfc_state_extend_oldprevious) = ((cfc_old_extend_old) + (cfc_matrix_extend_oldpreviouscode)) * S ((cfc_old_extend_old) + (cfc_matrix_extend_oldpreviouscode)) + ((cfc_matrix_extend_oldpreviouscode) + (cfc_matrix_extend_oldpreviouscode))))))) /\ (((exists ff_h_extend_oldpreviousentry. ff_h_extend_oldpreviousentry + S (cfc_state_extend_oldprevious) = S ((S (cfc_index_extend_old)) * e)) /\ exists ff_q_extend_oldpreviousentry. h = ff_q_extend_oldpreviousentry * S ((S (cfc_index_extend_old)) * e) + (cfc_state_extend_oldprevious))))) /\ ((exists cfc_state_extend_oldfollowing. ((exists cfc_left_extend_oldfollowingcode cfc_right_extend_oldfollowingcode cfc_matrix_extend_oldfollowingcode. ((cfc_left_extend_oldfollowingcode = (((cfc_quotient_extend_old * cfc_a_extend_old + cfc_c_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old))) * S (((cfc_quotient_extend_old * cfc_a_extend_old + cfc_c_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old))) + (((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old)))) /\ ((cfc_right_extend_oldfollowingcode = ((cfc_a_extend_old) + (cfc_b_extend_old)) * S ((cfc_a_extend_old) + (cfc_b_extend_old)) + ((cfc_b_extend_old) + (cfc_b_extend_old))) /\ ((cfc_matrix_extend_oldfollowingcode = ((cfc_left_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode)) * S ((cfc_left_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode)) + ((cfc_right_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode))) /\ ((cfc_state_extend_oldfollowing) = ((cfc_new_extend_old) + (cfc_matrix_extend_oldfollowingcode)) * S ((cfc_new_extend_old) + (cfc_matrix_extend_oldfollowingcode)) + ((cfc_matrix_extend_oldfollowingcode) + (cfc_matrix_extend_oldfollowingcode))))))) /\ (((exists ff_h_extend_oldfollowingentry. ff_h_extend_oldfollowingentry + S (cfc_state_extend_oldfollowing) = S ((S (S cfc_index_extend_old)) * e)) /\ exists ff_q_extend_oldfollowingentry. h = ff_q_extend_oldfollowingentry * S ((S (S cfc_index_extend_old)) * e) + (cfc_state_extend_oldfollowing))))) /\ (cfc_new_extend_old = S ((cfc_quotient_extend_old + cfc_old_extend_old) * S (cfc_quotient_extend_old + cfc_old_extend_old) + (cfc_old_extend_old + cfc_old_extend_old))))))))) -> (s = S ((q + t) * S (q + t) + (t + t))) -> (exists cfc_state_extend_new_state. ((exists cfc_left_extend_new_statecode cfc_right_extend_new_statecode cfc_matrix_extend_new_statecode. ((cfc_left_extend_new_statecode = (((q * u + v)) + ((q * U + V))) * S (((q * u + v)) + ((q * U + V))) + (((q * U + V)) + ((q * U + V)))) /\ ((cfc_right_extend_new_statecode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_matrix_extend_new_statecode = ((cfc_left_extend_new_statecode) + (cfc_right_extend_new_statecode)) * S ((cfc_left_extend_new_statecode) + (cfc_right_extend_new_statecode)) + ((cfc_right_extend_new_statecode) + (cfc_right_extend_new_statecode))) /\ ((cfc_state_extend_new_state) = ((s) + (cfc_matrix_extend_new_statecode)) * S ((s) + (cfc_matrix_extend_new_statecode)) + ((cfc_matrix_extend_new_statecode) + (cfc_matrix_extend_new_statecode))))))) /\ (((exists ff_h_extend_new_stateentry. ff_h_extend_new_stateentry + S (cfc_state_extend_new_state) = S ((S (S k)) * E)) /\ exists ff_q_extend_new_stateentry. H = ff_q_extend_new_stateentry * S ((S (S k)) * E) + (cfc_state_extend_new_state))))) -> (forall cfc_index_extend_preserves cfc_value_extend_preserves. (exists cfba_gap_extend_preservesbound. cfba_gap_extend_preservesbound + S (cfc_index_extend_preserves) = (S k)) -> (((exists ff_h_extend_preservessource. ff_h_extend_preservessource + S (cfc_value_extend_preserves) = S ((S (cfc_index_extend_preserves)) * e)) /\ exists ff_q_extend_preservessource. h = ff_q_extend_preservessource * S ((S (cfc_index_extend_preserves)) * e) + (cfc_value_extend_preserves))) -> (((exists ff_h_extend_preservestarget. ff_h_extend_preservestarget + S (cfc_value_extend_preserves) = S ((S (cfc_index_extend_preserves)) * E)) /\ exists ff_q_extend_preservestarget. H = ff_q_extend_preservestarget * S ((S (cfc_index_extend_preserves)) * E) + (cfc_value_extend_preserves)))) -> (exists cfc_tail_extend_result. ((exists cfc_state_extend_resultinitial. ((exists cfc_left_extend_resultinitialcode cfc_right_extend_resultinitialcode cfc_matrix_extend_resultinitialcode. ((cfc_left_extend_resultinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_extend_resultinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_extend_resultinitialcode = ((cfc_left_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode)) * S ((cfc_left_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode)) + ((cfc_right_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode))) /\ ((cfc_state_extend_resultinitial) = ((cfc_tail_extend_result) + (cfc_matrix_extend_resultinitialcode)) * S ((cfc_tail_extend_result) + (cfc_matrix_extend_resultinitialcode)) + ((cfc_matrix_extend_resultinitialcode) + (cfc_matrix_extend_resultinitialcode))))))) /\ (((exists ff_h_extend_resultinitialentry. ff_h_extend_resultinitialentry + S (cfc_state_extend_resultinitial) = S ((S (0)) * E)) /\ exists ff_q_extend_resultinitialentry. H = ff_q_extend_resultinitialentry * S ((S (0)) * E) + (cfc_state_extend_resultinitial))))) /\ ((exists cfc_state_extend_resultterminal. ((exists cfc_left_extend_resultterminalcode cfc_right_extend_resultterminalcode cfc_matrix_extend_resultterminalcode. ((cfc_left_extend_resultterminalcode = (((q * u + v)) + ((q * U + V))) * S (((q * u + v)) + ((q * U + V))) + (((q * U + V)) + ((q * U + V)))) /\ ((cfc_right_extend_resultterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_matrix_extend_resultterminalcode = ((cfc_left_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode)) * S ((cfc_left_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode)) + ((cfc_right_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode))) /\ ((cfc_state_extend_resultterminal) = ((s) + (cfc_matrix_extend_resultterminalcode)) * S ((s) + (cfc_matrix_extend_resultterminalcode)) + ((cfc_matrix_extend_resultterminalcode) + (cfc_matrix_extend_resultterminalcode))))))) /\ (((exists ff_h_extend_resultterminalentry. ff_h_extend_resultterminalentry + S (cfc_state_extend_resultterminal) = S ((S (S k)) * E)) /\ exists ff_q_extend_resultterminalentry. H = ff_q_extend_resultterminalentry * S ((S (S k)) * E) + (cfc_state_extend_resultterminal))))) /\ (forall cfc_index_extend_result. (exists cfba_gap_extend_resultbound. cfba_gap_extend_resultbound + S (cfc_index_extend_result) = (S k)) -> exists cfc_old_extend_result cfc_a_extend_result cfc_b_extend_result cfc_c_extend_result cfc_d_extend_result cfc_new_extend_result cfc_quotient_extend_result. ((exists cfc_state_extend_resultprevious. ((exists cfc_left_extend_resultpreviouscode cfc_right_extend_resultpreviouscode cfc_matrix_extend_resultpreviouscode. ((cfc_left_extend_resultpreviouscode = ((cfc_a_extend_result) + (cfc_b_extend_result)) * S ((cfc_a_extend_result) + (cfc_b_extend_result)) + ((cfc_b_extend_result) + (cfc_b_extend_result))) /\ ((cfc_right_extend_resultpreviouscode = ((cfc_c_extend_result) + (cfc_d_extend_result)) * S ((cfc_c_extend_result) + (cfc_d_extend_result)) + ((cfc_d_extend_result) + (cfc_d_extend_result))) /\ ((cfc_matrix_extend_resultpreviouscode = ((cfc_left_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode)) * S ((cfc_left_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode)) + ((cfc_right_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode))) /\ ((cfc_state_extend_resultprevious) = ((cfc_old_extend_result) + (cfc_matrix_extend_resultpreviouscode)) * S ((cfc_old_extend_result) + (cfc_matrix_extend_resultpreviouscode)) + ((cfc_matrix_extend_resultpreviouscode) + (cfc_matrix_extend_resultpreviouscode))))))) /\ (((exists ff_h_extend_resultpreviousentry. ff_h_extend_resultpreviousentry + S (cfc_state_extend_resultprevious) = S ((S (cfc_index_extend_result)) * E)) /\ exists ff_q_extend_resultpreviousentry. H = ff_q_extend_resultpreviousentry * S ((S (cfc_index_extend_result)) * E) + (cfc_state_extend_resultprevious))))) /\ ((exists cfc_state_extend_resultfollowing. ((exists cfc_left_extend_resultfollowingcode cfc_right_extend_resultfollowingcode cfc_matrix_extend_resultfollowingcode. ((cfc_left_extend_resultfollowingcode = (((cfc_quotient_extend_result * cfc_a_extend_result + cfc_c_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result))) * S (((cfc_quotient_extend_result * cfc_a_extend_result + cfc_c_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result))) + (((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result)))) /\ ((cfc_right_extend_resultfollowingcode = ((cfc_a_extend_result) + (cfc_b_extend_result)) * S ((cfc_a_extend_result) + (cfc_b_extend_result)) + ((cfc_b_extend_result) + (cfc_b_extend_result))) /\ ((cfc_matrix_extend_resultfollowingcode = ((cfc_left_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode)) * S ((cfc_left_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode)) + ((cfc_right_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode))) /\ ((cfc_state_extend_resultfollowing) = ((cfc_new_extend_result) + (cfc_matrix_extend_resultfollowingcode)) * S ((cfc_new_extend_result) + (cfc_matrix_extend_resultfollowingcode)) + ((cfc_matrix_extend_resultfollowingcode) + (cfc_matrix_extend_resultfollowingcode))))))) /\ (((exists ff_h_extend_resultfollowingentry. ff_h_extend_resultfollowingentry + S (cfc_state_extend_resultfollowing) = S ((S (S cfc_index_extend_result)) * E)) /\ exists ff_q_extend_resultfollowingentry. H = ff_q_extend_resultfollowingentry * S ((S (S cfc_index_extend_result)) * E) + (cfc_state_extend_resultfollowing))))) /\ (cfc_new_extend_result = S ((cfc_quotient_extend_result + cfc_old_extend_result) * S (cfc_quotient_extend_result + cfc_old_extend_result) + (cfc_old_extend_result + cfc_old_extend_result)))))))))