cf_convergent_numerator_transport

forall s i u p v. u = p -> (exists cfc_previous_numerator_numerator_source cfc_previous_denominator_numerator_source cfc_code_numerator_source cfc_scale_numerator_source. ((~(v = 0)) /\ (exists cfc_tail_numerator_sourcecomputation. ((exists cfc_state_numerator_sourcecomputationinitial. ((exists cfc_left_numerator_sourcecomputationinitialcode cfc_right_numerator_sourcecomputationinitialcode cfc_matrix_numerator_sourcecomputationinitialcode. ((cfc_left_numerator_sourcecomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_numerator_sourcecomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_numerator_sourcecomputationinitialcode = ((cfc_left_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode)) * S ((cfc_left_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode)) + ((cfc_right_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode))) /\ ((cfc_state_numerator_sourcecomputationinitial) = ((cfc_tail_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationinitialcode)) * S ((cfc_tail_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationinitialcode)) + ((cfc_matrix_numerator_sourcecomputationinitialcode) + (cfc_matrix_numerator_sourcecomputationinitialcode))))))) /\ (((exists ff_h_numerator_sourcecomputationinitialentry. ff_h_numerator_sourcecomputationinitialentry + S (cfc_state_numerator_sourcecomputationinitial) = S ((S (0)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationinitialentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationinitialentry * S ((S (0)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationinitial))))) /\ ((exists cfc_state_numerator_sourcecomputationterminal. ((exists cfc_left_numerator_sourcecomputationterminalcode cfc_right_numerator_sourcecomputationterminalcode cfc_matrix_numerator_sourcecomputationterminalcode. ((cfc_left_numerator_sourcecomputationterminalcode = ((u) + (cfc_previous_numerator_numerator_source)) * S ((u) + (cfc_previous_numerator_numerator_source)) + ((cfc_previous_numerator_numerator_source) + (cfc_previous_numerator_numerator_source))) /\ ((cfc_right_numerator_sourcecomputationterminalcode = ((v) + (cfc_previous_denominator_numerator_source)) * S ((v) + (cfc_previous_denominator_numerator_source)) + ((cfc_previous_denominator_numerator_source) + (cfc_previous_denominator_numerator_source))) /\ ((cfc_matrix_numerator_sourcecomputationterminalcode = ((cfc_left_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode)) * S ((cfc_left_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode)) + ((cfc_right_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode))) /\ ((cfc_state_numerator_sourcecomputationterminal) = ((s) + (cfc_matrix_numerator_sourcecomputationterminalcode)) * S ((s) + (cfc_matrix_numerator_sourcecomputationterminalcode)) + ((cfc_matrix_numerator_sourcecomputationterminalcode) + (cfc_matrix_numerator_sourcecomputationterminalcode))))))) /\ (((exists ff_h_numerator_sourcecomputationterminalentry. ff_h_numerator_sourcecomputationterminalentry + S (cfc_state_numerator_sourcecomputationterminal) = S ((S (S (i))) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationterminalentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationterminalentry * S ((S (S (i))) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationterminal))))) /\ (forall cfc_index_numerator_sourcecomputation. (exists cfba_gap_numerator_sourcecomputationbound. cfba_gap_numerator_sourcecomputationbound + S (cfc_index_numerator_sourcecomputation) = (S (i))) -> exists cfc_old_numerator_sourcecomputation cfc_a_numerator_sourcecomputation cfc_b_numerator_sourcecomputation cfc_c_numerator_sourcecomputation cfc_d_numerator_sourcecomputation cfc_new_numerator_sourcecomputation cfc_quotient_numerator_sourcecomputation. ((exists cfc_state_numerator_sourcecomputationprevious. ((exists cfc_left_numerator_sourcecomputationpreviouscode cfc_right_numerator_sourcecomputationpreviouscode cfc_matrix_numerator_sourcecomputationpreviouscode. ((cfc_left_numerator_sourcecomputationpreviouscode = ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) * S ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) + ((cfc_b_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation))) /\ ((cfc_right_numerator_sourcecomputationpreviouscode = ((cfc_c_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation)) * S ((cfc_c_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation)) + ((cfc_d_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation))) /\ ((cfc_matrix_numerator_sourcecomputationpreviouscode = ((cfc_left_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode)) * S ((cfc_left_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode)) + ((cfc_right_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode))) /\ ((cfc_state_numerator_sourcecomputationprevious) = ((cfc_old_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationpreviouscode)) * S ((cfc_old_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationpreviouscode)) + ((cfc_matrix_numerator_sourcecomputationpreviouscode) + (cfc_matrix_numerator_sourcecomputationpreviouscode))))))) /\ (((exists ff_h_numerator_sourcecomputationpreviousentry. ff_h_numerator_sourcecomputationpreviousentry + S (cfc_state_numerator_sourcecomputationprevious) = S ((S (cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationpreviousentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationpreviousentry * S ((S (cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationprevious))))) /\ ((exists cfc_state_numerator_sourcecomputationfollowing. ((exists cfc_left_numerator_sourcecomputationfollowingcode cfc_right_numerator_sourcecomputationfollowingcode cfc_matrix_numerator_sourcecomputationfollowingcode. ((cfc_left_numerator_sourcecomputationfollowingcode = (((cfc_quotient_numerator_sourcecomputation * cfc_a_numerator_sourcecomputation + cfc_c_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation))) * S (((cfc_quotient_numerator_sourcecomputation * cfc_a_numerator_sourcecomputation + cfc_c_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation))) + (((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation)))) /\ ((cfc_right_numerator_sourcecomputationfollowingcode = ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) * S ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) + ((cfc_b_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation))) /\ ((cfc_matrix_numerator_sourcecomputationfollowingcode = ((cfc_left_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode)) * S ((cfc_left_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode)) + ((cfc_right_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode))) /\ ((cfc_state_numerator_sourcecomputationfollowing) = ((cfc_new_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationfollowingcode)) * S ((cfc_new_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationfollowingcode)) + ((cfc_matrix_numerator_sourcecomputationfollowingcode) + (cfc_matrix_numerator_sourcecomputationfollowingcode))))))) /\ (((exists ff_h_numerator_sourcecomputationfollowingentry. ff_h_numerator_sourcecomputationfollowingentry + S (cfc_state_numerator_sourcecomputationfollowing) = S ((S (S cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationfollowingentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationfollowingentry * S ((S (S cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationfollowing))))) /\ (cfc_new_numerator_sourcecomputation = S ((cfc_quotient_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation) * S (cfc_quotient_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation) + (cfc_old_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation))))))))))) -> (exists cfc_previous_numerator_numerator_target cfc_previous_denominator_numerator_target cfc_code_numerator_target cfc_scale_numerator_target. ((~(v = 0)) /\ (exists cfc_tail_numerator_targetcomputation. ((exists cfc_state_numerator_targetcomputationinitial. ((exists cfc_left_numerator_targetcomputationinitialcode cfc_right_numerator_targetcomputationinitialcode cfc_matrix_numerator_targetcomputationinitialcode. ((cfc_left_numerator_targetcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_numerator_targetcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_numerator_targetcomputationinitialcode = ((cfc_left_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode)) * S ((cfc_left_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode)) + ((cfc_right_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode))) /\ ((cfc_state_numerator_targetcomputationinitial) = ((cfc_tail_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationinitialcode)) * S ((cfc_tail_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationinitialcode)) + ((cfc_matrix_numerator_targetcomputationinitialcode) + (cfc_matrix_numerator_targetcomputationinitialcode))))))) /\ (((exists ff_h_numerator_targetcomputationinitialentry. ff_h_numerator_targetcomputationinitialentry + S (cfc_state_numerator_targetcomputationinitial) = S ((S (0)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationinitialentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationinitialentry * S ((S (0)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationinitial))))) /\ ((exists cfc_state_numerator_targetcomputationterminal. ((exists cfc_left_numerator_targetcomputationterminalcode cfc_right_numerator_targetcomputationterminalcode cfc_matrix_numerator_targetcomputationterminalcode. ((cfc_left_numerator_targetcomputationterminalcode = ((p) + (cfc_previous_numerator_numerator_target)) * S ((p) + (cfc_previous_numerator_numerator_target)) + ((cfc_previous_numerator_numerator_target) + (cfc_previous_numerator_numerator_target))) /\ ((cfc_right_numerator_targetcomputationterminalcode = ((v) + (cfc_previous_denominator_numerator_target)) * S ((v) + (cfc_previous_denominator_numerator_target)) + ((cfc_previous_denominator_numerator_target) + (cfc_previous_denominator_numerator_target))) /\ ((cfc_matrix_numerator_targetcomputationterminalcode = ((cfc_left_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode)) * S ((cfc_left_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode)) + ((cfc_right_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode))) /\ ((cfc_state_numerator_targetcomputationterminal) = ((s) + (cfc_matrix_numerator_targetcomputationterminalcode)) * S ((s) + (cfc_matrix_numerator_targetcomputationterminalcode)) + ((cfc_matrix_numerator_targetcomputationterminalcode) + (cfc_matrix_numerator_targetcomputationterminalcode))))))) /\ (((exists ff_h_numerator_targetcomputationterminalentry. ff_h_numerator_targetcomputationterminalentry + S (cfc_state_numerator_targetcomputationterminal) = S ((S (S (i))) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationterminalentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationterminalentry * S ((S (S (i))) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationterminal))))) /\ (forall cfc_index_numerator_targetcomputation. (exists cfba_gap_numerator_targetcomputationbound. cfba_gap_numerator_targetcomputationbound + S (cfc_index_numerator_targetcomputation) = (S (i))) -> exists cfc_old_numerator_targetcomputation cfc_a_numerator_targetcomputation cfc_b_numerator_targetcomputation cfc_c_numerator_targetcomputation cfc_d_numerator_targetcomputation cfc_new_numerator_targetcomputation cfc_quotient_numerator_targetcomputation. ((exists cfc_state_numerator_targetcomputationprevious. ((exists cfc_left_numerator_targetcomputationpreviouscode cfc_right_numerator_targetcomputationpreviouscode cfc_matrix_numerator_targetcomputationpreviouscode. ((cfc_left_numerator_targetcomputationpreviouscode = ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) * S ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) + ((cfc_b_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation))) /\ ((cfc_right_numerator_targetcomputationpreviouscode = ((cfc_c_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation)) * S ((cfc_c_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation)) + ((cfc_d_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation))) /\ ((cfc_matrix_numerator_targetcomputationpreviouscode = ((cfc_left_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode)) * S ((cfc_left_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode)) + ((cfc_right_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode))) /\ ((cfc_state_numerator_targetcomputationprevious) = ((cfc_old_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationpreviouscode)) * S ((cfc_old_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationpreviouscode)) + ((cfc_matrix_numerator_targetcomputationpreviouscode) + (cfc_matrix_numerator_targetcomputationpreviouscode))))))) /\ (((exists ff_h_numerator_targetcomputationpreviousentry. ff_h_numerator_targetcomputationpreviousentry + S (cfc_state_numerator_targetcomputationprevious) = S ((S (cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationpreviousentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationpreviousentry * S ((S (cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationprevious))))) /\ ((exists cfc_state_numerator_targetcomputationfollowing. ((exists cfc_left_numerator_targetcomputationfollowingcode cfc_right_numerator_targetcomputationfollowingcode cfc_matrix_numerator_targetcomputationfollowingcode. ((cfc_left_numerator_targetcomputationfollowingcode = (((cfc_quotient_numerator_targetcomputation * cfc_a_numerator_targetcomputation + cfc_c_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation))) * S (((cfc_quotient_numerator_targetcomputation * cfc_a_numerator_targetcomputation + cfc_c_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation))) + (((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation)))) /\ ((cfc_right_numerator_targetcomputationfollowingcode = ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) * S ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) + ((cfc_b_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation))) /\ ((cfc_matrix_numerator_targetcomputationfollowingcode = ((cfc_left_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode)) * S ((cfc_left_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode)) + ((cfc_right_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode))) /\ ((cfc_state_numerator_targetcomputationfollowing) = ((cfc_new_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationfollowingcode)) * S ((cfc_new_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationfollowingcode)) + ((cfc_matrix_numerator_targetcomputationfollowingcode) + (cfc_matrix_numerator_targetcomputationfollowingcode))))))) /\ (((exists ff_h_numerator_targetcomputationfollowingentry. ff_h_numerator_targetcomputationfollowingentry + S (cfc_state_numerator_targetcomputationfollowing) = S ((S (S cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationfollowingentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationfollowingentry * S ((S (S cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationfollowing))))) /\ (cfc_new_numerator_targetcomputation = S ((cfc_quotient_numerator_targetcomputation + cfc_old_numerator_targetcomputation) * S (cfc_quotient_numerator_targetcomputation + cfc_old_numerator_targetcomputation) + (cfc_old_numerator_targetcomputation + cfc_old_numerator_targetcomputation)))))))))))