cf_convergent_matrix_entry_transport

Exact expanded first-order arithmetic statement

forall s h e k u U v V p P n N. u = p -> U = P -> v = n -> V = N -> (exists cfc_tail_entries_source. ((exists cfc_state_entries_sourceinitial. ((exists cfc_left_entries_sourceinitialcode cfc_right_entries_sourceinitialcode cfc_matrix_entries_sourceinitialcode. ((cfc_left_entries_sourceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_entries_sourceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_entries_sourceinitialcode = ((cfc_left_entries_sourceinitialcode) + (cfc_right_entries_sourceinitialcode)) * S ((cfc_left_entries_sourceinitialcode) + (cfc_right_entries_sourceinitialcode)) + ((cfc_right_entries_sourceinitialcode) + (cfc_right_entries_sourceinitialcode))) /\ ((cfc_state_entries_sourceinitial) = ((cfc_tail_entries_source) + (cfc_matrix_entries_sourceinitialcode)) * S ((cfc_tail_entries_source) + (cfc_matrix_entries_sourceinitialcode)) + ((cfc_matrix_entries_sourceinitialcode) + (cfc_matrix_entries_sourceinitialcode))))))) /\ (((exists ff_h_entries_sourceinitialentry. ff_h_entries_sourceinitialentry + S (cfc_state_entries_sourceinitial) = S ((S (0)) * e)) /\ exists ff_q_entries_sourceinitialentry. h = ff_q_entries_sourceinitialentry * S ((S (0)) * e) + (cfc_state_entries_sourceinitial))))) /\ ((exists cfc_state_entries_sourceterminal. ((exists cfc_left_entries_sourceterminalcode cfc_right_entries_sourceterminalcode cfc_matrix_entries_sourceterminalcode. ((cfc_left_entries_sourceterminalcode = ((p) + (P)) * S ((p) + (P)) + ((P) + (P))) /\ ((cfc_right_entries_sourceterminalcode = ((n) + (N)) * S ((n) + (N)) + ((N) + (N))) /\ ((cfc_matrix_entries_sourceterminalcode = ((cfc_left_entries_sourceterminalcode) + (cfc_right_entries_sourceterminalcode)) * S ((cfc_left_entries_sourceterminalcode) + (cfc_right_entries_sourceterminalcode)) + ((cfc_right_entries_sourceterminalcode) + (cfc_right_entries_sourceterminalcode))) /\ ((cfc_state_entries_sourceterminal) = ((s) + (cfc_matrix_entries_sourceterminalcode)) * S ((s) + (cfc_matrix_entries_sourceterminalcode)) + ((cfc_matrix_entries_sourceterminalcode) + (cfc_matrix_entries_sourceterminalcode))))))) /\ (((exists ff_h_entries_sourceterminalentry. ff_h_entries_sourceterminalentry + S (cfc_state_entries_sourceterminal) = S ((S (k)) * e)) /\ exists ff_q_entries_sourceterminalentry. h = ff_q_entries_sourceterminalentry * S ((S (k)) * e) + (cfc_state_entries_sourceterminal))))) /\ (forall cfc_index_entries_source. (exists cfba_gap_entries_sourcebound. cfba_gap_entries_sourcebound + S (cfc_index_entries_source) = (k)) -> exists cfc_old_entries_source cfc_a_entries_source cfc_b_entries_source cfc_c_entries_source cfc_d_entries_source cfc_new_entries_source cfc_quotient_entries_source. ((exists cfc_state_entries_sourceprevious. ((exists cfc_left_entries_sourcepreviouscode cfc_right_entries_sourcepreviouscode cfc_matrix_entries_sourcepreviouscode. ((cfc_left_entries_sourcepreviouscode = ((cfc_a_entries_source) + (cfc_b_entries_source)) * S ((cfc_a_entries_source) + (cfc_b_entries_source)) + ((cfc_b_entries_source) + (cfc_b_entries_source))) /\ ((cfc_right_entries_sourcepreviouscode = ((cfc_c_entries_source) + (cfc_d_entries_source)) * S ((cfc_c_entries_source) + (cfc_d_entries_source)) + ((cfc_d_entries_source) + (cfc_d_entries_source))) /\ ((cfc_matrix_entries_sourcepreviouscode = ((cfc_left_entries_sourcepreviouscode) + (cfc_right_entries_sourcepreviouscode)) * S ((cfc_left_entries_sourcepreviouscode) + (cfc_right_entries_sourcepreviouscode)) + ((cfc_right_entries_sourcepreviouscode) + (cfc_right_entries_sourcepreviouscode))) /\ ((cfc_state_entries_sourceprevious) = ((cfc_old_entries_source) + (cfc_matrix_entries_sourcepreviouscode)) * S ((cfc_old_entries_source) + (cfc_matrix_entries_sourcepreviouscode)) + ((cfc_matrix_entries_sourcepreviouscode) + (cfc_matrix_entries_sourcepreviouscode))))))) /\ (((exists ff_h_entries_sourcepreviousentry. ff_h_entries_sourcepreviousentry + S (cfc_state_entries_sourceprevious) = S ((S (cfc_index_entries_source)) * e)) /\ exists ff_q_entries_sourcepreviousentry. h = ff_q_entries_sourcepreviousentry * S ((S (cfc_index_entries_source)) * e) + (cfc_state_entries_sourceprevious))))) /\ ((exists cfc_state_entries_sourcefollowing. ((exists cfc_left_entries_sourcefollowingcode cfc_right_entries_sourcefollowingcode cfc_matrix_entries_sourcefollowingcode. ((cfc_left_entries_sourcefollowingcode = (((cfc_quotient_entries_source * cfc_a_entries_source + cfc_c_entries_source)) + ((cfc_quotient_entries_source * cfc_b_entries_source + cfc_d_entries_source))) * S (((cfc_quotient_entries_source * cfc_a_entries_source + cfc_c_entries_source)) + ((cfc_quotient_entries_source * cfc_b_entries_source + cfc_d_entries_source))) + (((cfc_quotient_entries_source * cfc_b_entries_source + cfc_d_entries_source)) + ((cfc_quotient_entries_source * cfc_b_entries_source + cfc_d_entries_source)))) /\ ((cfc_right_entries_sourcefollowingcode = ((cfc_a_entries_source) + (cfc_b_entries_source)) * S ((cfc_a_entries_source) + (cfc_b_entries_source)) + ((cfc_b_entries_source) + (cfc_b_entries_source))) /\ ((cfc_matrix_entries_sourcefollowingcode = ((cfc_left_entries_sourcefollowingcode) + (cfc_right_entries_sourcefollowingcode)) * S ((cfc_left_entries_sourcefollowingcode) + (cfc_right_entries_sourcefollowingcode)) + ((cfc_right_entries_sourcefollowingcode) + (cfc_right_entries_sourcefollowingcode))) /\ ((cfc_state_entries_sourcefollowing) = ((cfc_new_entries_source) + (cfc_matrix_entries_sourcefollowingcode)) * S ((cfc_new_entries_source) + (cfc_matrix_entries_sourcefollowingcode)) + ((cfc_matrix_entries_sourcefollowingcode) + (cfc_matrix_entries_sourcefollowingcode))))))) /\ (((exists ff_h_entries_sourcefollowingentry. ff_h_entries_sourcefollowingentry + S (cfc_state_entries_sourcefollowing) = S ((S (S cfc_index_entries_source)) * e)) /\ exists ff_q_entries_sourcefollowingentry. h = ff_q_entries_sourcefollowingentry * S ((S (S cfc_index_entries_source)) * e) + (cfc_state_entries_sourcefollowing))))) /\ (cfc_new_entries_source = S ((cfc_quotient_entries_source + cfc_old_entries_source) * S (cfc_quotient_entries_source + cfc_old_entries_source) + (cfc_old_entries_source + cfc_old_entries_source))))))))) -> (exists cfc_tail_entries_target. ((exists cfc_state_entries_targetinitial. ((exists cfc_left_entries_targetinitialcode cfc_right_entries_targetinitialcode cfc_matrix_entries_targetinitialcode. ((cfc_left_entries_targetinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_entries_targetinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_entries_targetinitialcode = ((cfc_left_entries_targetinitialcode) + (cfc_right_entries_targetinitialcode)) * S ((cfc_left_entries_targetinitialcode) + (cfc_right_entries_targetinitialcode)) + ((cfc_right_entries_targetinitialcode) + (cfc_right_entries_targetinitialcode))) /\ ((cfc_state_entries_targetinitial) = ((cfc_tail_entries_target) + (cfc_matrix_entries_targetinitialcode)) * S ((cfc_tail_entries_target) + (cfc_matrix_entries_targetinitialcode)) + ((cfc_matrix_entries_targetinitialcode) + (cfc_matrix_entries_targetinitialcode))))))) /\ (((exists ff_h_entries_targetinitialentry. ff_h_entries_targetinitialentry + S (cfc_state_entries_targetinitial) = S ((S (0)) * e)) /\ exists ff_q_entries_targetinitialentry. h = ff_q_entries_targetinitialentry * S ((S (0)) * e) + (cfc_state_entries_targetinitial))))) /\ ((exists cfc_state_entries_targetterminal. ((exists cfc_left_entries_targetterminalcode cfc_right_entries_targetterminalcode cfc_matrix_entries_targetterminalcode. ((cfc_left_entries_targetterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_entries_targetterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_entries_targetterminalcode = ((cfc_left_entries_targetterminalcode) + (cfc_right_entries_targetterminalcode)) * S ((cfc_left_entries_targetterminalcode) + (cfc_right_entries_targetterminalcode)) + ((cfc_right_entries_targetterminalcode) + (cfc_right_entries_targetterminalcode))) /\ ((cfc_state_entries_targetterminal) = ((s) + (cfc_matrix_entries_targetterminalcode)) * S ((s) + (cfc_matrix_entries_targetterminalcode)) + ((cfc_matrix_entries_targetterminalcode) + (cfc_matrix_entries_targetterminalcode))))))) /\ (((exists ff_h_entries_targetterminalentry. ff_h_entries_targetterminalentry + S (cfc_state_entries_targetterminal) = S ((S (k)) * e)) /\ exists ff_q_entries_targetterminalentry. h = ff_q_entries_targetterminalentry * S ((S (k)) * e) + (cfc_state_entries_targetterminal))))) /\ (forall cfc_index_entries_target. (exists cfba_gap_entries_targetbound. cfba_gap_entries_targetbound + S (cfc_index_entries_target) = (k)) -> exists cfc_old_entries_target cfc_a_entries_target cfc_b_entries_target cfc_c_entries_target cfc_d_entries_target cfc_new_entries_target cfc_quotient_entries_target. ((exists cfc_state_entries_targetprevious. ((exists cfc_left_entries_targetpreviouscode cfc_right_entries_targetpreviouscode cfc_matrix_entries_targetpreviouscode. ((cfc_left_entries_targetpreviouscode = ((cfc_a_entries_target) + (cfc_b_entries_target)) * S ((cfc_a_entries_target) + (cfc_b_entries_target)) + ((cfc_b_entries_target) + (cfc_b_entries_target))) /\ ((cfc_right_entries_targetpreviouscode = ((cfc_c_entries_target) + (cfc_d_entries_target)) * S ((cfc_c_entries_target) + (cfc_d_entries_target)) + ((cfc_d_entries_target) + (cfc_d_entries_target))) /\ ((cfc_matrix_entries_targetpreviouscode = ((cfc_left_entries_targetpreviouscode) + (cfc_right_entries_targetpreviouscode)) * S ((cfc_left_entries_targetpreviouscode) + (cfc_right_entries_targetpreviouscode)) + ((cfc_right_entries_targetpreviouscode) + (cfc_right_entries_targetpreviouscode))) /\ ((cfc_state_entries_targetprevious) = ((cfc_old_entries_target) + (cfc_matrix_entries_targetpreviouscode)) * S ((cfc_old_entries_target) + (cfc_matrix_entries_targetpreviouscode)) + ((cfc_matrix_entries_targetpreviouscode) + (cfc_matrix_entries_targetpreviouscode))))))) /\ (((exists ff_h_entries_targetpreviousentry. ff_h_entries_targetpreviousentry + S (cfc_state_entries_targetprevious) = S ((S (cfc_index_entries_target)) * e)) /\ exists ff_q_entries_targetpreviousentry. h = ff_q_entries_targetpreviousentry * S ((S (cfc_index_entries_target)) * e) + (cfc_state_entries_targetprevious))))) /\ ((exists cfc_state_entries_targetfollowing. ((exists cfc_left_entries_targetfollowingcode cfc_right_entries_targetfollowingcode cfc_matrix_entries_targetfollowingcode. ((cfc_left_entries_targetfollowingcode = (((cfc_quotient_entries_target * cfc_a_entries_target + cfc_c_entries_target)) + ((cfc_quotient_entries_target * cfc_b_entries_target + cfc_d_entries_target))) * S (((cfc_quotient_entries_target * cfc_a_entries_target + cfc_c_entries_target)) + ((cfc_quotient_entries_target * cfc_b_entries_target + cfc_d_entries_target))) + (((cfc_quotient_entries_target * cfc_b_entries_target + cfc_d_entries_target)) + ((cfc_quotient_entries_target * cfc_b_entries_target + cfc_d_entries_target)))) /\ ((cfc_right_entries_targetfollowingcode = ((cfc_a_entries_target) + (cfc_b_entries_target)) * S ((cfc_a_entries_target) + (cfc_b_entries_target)) + ((cfc_b_entries_target) + (cfc_b_entries_target))) /\ ((cfc_matrix_entries_targetfollowingcode = ((cfc_left_entries_targetfollowingcode) + (cfc_right_entries_targetfollowingcode)) * S ((cfc_left_entries_targetfollowingcode) + (cfc_right_entries_targetfollowingcode)) + ((cfc_right_entries_targetfollowingcode) + (cfc_right_entries_targetfollowingcode))) /\ ((cfc_state_entries_targetfollowing) = ((cfc_new_entries_target) + (cfc_matrix_entries_targetfollowingcode)) * S ((cfc_new_entries_target) + (cfc_matrix_entries_targetfollowingcode)) + ((cfc_matrix_entries_targetfollowingcode) + (cfc_matrix_entries_targetfollowingcode))))))) /\ (((exists ff_h_entries_targetfollowingentry. ff_h_entries_targetfollowingentry + S (cfc_state_entries_targetfollowing) = S ((S (S cfc_index_entries_target)) * e)) /\ exists ff_q_entries_targetfollowingentry. h = ff_q_entries_targetfollowingentry * S ((S (S cfc_index_entries_target)) * e) + (cfc_state_entries_targetfollowing))))) /\ (cfc_new_entries_target = S ((cfc_quotient_entries_target + cfc_old_entries_target) * S (cfc_quotient_entries_target + cfc_old_entries_target) + (cfc_old_entries_target + cfc_old_entries_target)))))))))