continued_fraction_adjacent_convergent_determinant

forall a b s i u v p q. (exists cf_a_pred_adjacent_fraction cf_b_pred_adjacent_fraction cf_code_adjacent_fraction cf_scale_adjacent_fraction cf_length_pred_adjacent_fraction. (a = S cf_a_pred_adjacent_fraction /\ (b = S cf_b_pred_adjacent_fraction /\ (exists cf_gcd_adjacent_fraction_trace. ((((exists ff_h_cf_adjacent_fraction_trace_initial_state. ff_h_cf_adjacent_fraction_trace_initial_state + S (((cf_gcd_adjacent_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_adjacent_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * cf_scale_adjacent_fraction)) /\ exists ff_q_cf_adjacent_fraction_trace_initial_state. cf_code_adjacent_fraction = ff_q_cf_adjacent_fraction_trace_initial_state * S ((S (0)) * cf_scale_adjacent_fraction) + (((cf_gcd_adjacent_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_adjacent_fraction_trace) + (((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_adjacent_fraction_trace_terminal_state. ff_h_cf_adjacent_fraction_trace_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 (S cf_length_pred_adjacent_fraction)) * cf_scale_adjacent_fraction)) /\ exists ff_q_cf_adjacent_fraction_trace_terminal_state. cf_code_adjacent_fraction = ff_q_cf_adjacent_fraction_trace_terminal_state * S ((S (S cf_length_pred_adjacent_fraction)) * cf_scale_adjacent_fraction) + (((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_adjacent_fraction_trace. (exists ff_lt_cf_adjacent_fraction_trace_index. ff_lt_cf_adjacent_fraction_trace_index + S cf_index_adjacent_fraction_trace = S cf_length_pred_adjacent_fraction) -> exists cf_old_a_adjacent_fraction_trace cf_old_b_adjacent_fraction_trace cf_tail_adjacent_fraction_trace cf_new_a_adjacent_fraction_trace cf_new_b_adjacent_fraction_trace cf_head_adjacent_fraction_trace cf_quotient_adjacent_fraction_trace. ((((exists ff_h_cf_adjacent_fraction_trace_previous_state. ff_h_cf_adjacent_fraction_trace_previous_state + S (((cf_old_a_adjacent_fraction_trace) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)))) * S ((cf_old_a_adjacent_fraction_trace) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)))) + ((((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace))) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace))))) = S ((S (cf_index_adjacent_fraction_trace)) * cf_scale_adjacent_fraction)) /\ exists ff_q_cf_adjacent_fraction_trace_previous_state. cf_code_adjacent_fraction = ff_q_cf_adjacent_fraction_trace_previous_state * S ((S (cf_index_adjacent_fraction_trace)) * cf_scale_adjacent_fraction) + (((cf_old_a_adjacent_fraction_trace) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)))) * S ((cf_old_a_adjacent_fraction_trace) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)))) + ((((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace))) + (((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) * S ((cf_old_b_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace)) + ((cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace))))))) /\ ((((exists ff_h_cf_adjacent_fraction_trace_following_state. ff_h_cf_adjacent_fraction_trace_following_state + S (((cf_new_a_adjacent_fraction_trace) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)))) * S ((cf_new_a_adjacent_fraction_trace) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)))) + ((((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace))) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace))))) = S ((S (S cf_index_adjacent_fraction_trace)) * cf_scale_adjacent_fraction)) /\ exists ff_q_cf_adjacent_fraction_trace_following_state. cf_code_adjacent_fraction = ff_q_cf_adjacent_fraction_trace_following_state * S ((S (S cf_index_adjacent_fraction_trace)) * cf_scale_adjacent_fraction) + (((cf_new_a_adjacent_fraction_trace) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)))) * S ((cf_new_a_adjacent_fraction_trace) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)))) + ((((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace))) + (((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) * S ((cf_new_b_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace)) + ((cf_head_adjacent_fraction_trace) + (cf_head_adjacent_fraction_trace))))))) /\ (cf_new_b_adjacent_fraction_trace = cf_old_a_adjacent_fraction_trace /\ (cf_new_a_adjacent_fraction_trace = cf_new_b_adjacent_fraction_trace * cf_quotient_adjacent_fraction_trace + cf_old_b_adjacent_fraction_trace /\ ((exists ff_lt_cf_adjacent_fraction_trace_remainder. ff_lt_cf_adjacent_fraction_trace_remainder + S cf_old_b_adjacent_fraction_trace = cf_new_b_adjacent_fraction_trace) /\ (cf_head_adjacent_fraction_trace = S ((cf_quotient_adjacent_fraction_trace + cf_tail_adjacent_fraction_trace) * S (cf_quotient_adjacent_fraction_trace + cf_tail_adjacent_fraction_trace) + (cf_tail_adjacent_fraction_trace + cf_tail_adjacent_fraction_trace)))))))))))))) -> (exists cfc_previous_numerator_adjacent_current cfc_previous_denominator_adjacent_current cfc_code_adjacent_current cfc_scale_adjacent_current. ((~(v = 0)) /\ (exists cfc_tail_adjacent_currentcomputation. ((exists cfc_state_adjacent_currentcomputationinitial. ((exists cfc_left_adjacent_currentcomputationinitialcode cfc_right_adjacent_currentcomputationinitialcode cfc_matrix_adjacent_currentcomputationinitialcode. ((cfc_left_adjacent_currentcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_adjacent_currentcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_adjacent_currentcomputationinitialcode = ((cfc_left_adjacent_currentcomputationinitialcode) + (cfc_right_adjacent_currentcomputationinitialcode)) * S ((cfc_left_adjacent_currentcomputationinitialcode) + (cfc_right_adjacent_currentcomputationinitialcode)) + ((cfc_right_adjacent_currentcomputationinitialcode) + (cfc_right_adjacent_currentcomputationinitialcode))) /\ ((cfc_state_adjacent_currentcomputationinitial) = ((cfc_tail_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationinitialcode)) * S ((cfc_tail_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationinitialcode)) + ((cfc_matrix_adjacent_currentcomputationinitialcode) + (cfc_matrix_adjacent_currentcomputationinitialcode))))))) /\ (((exists ff_h_adjacent_currentcomputationinitialentry. ff_h_adjacent_currentcomputationinitialentry + S (cfc_state_adjacent_currentcomputationinitial) = S ((S (0)) * cfc_scale_adjacent_current)) /\ exists ff_q_adjacent_currentcomputationinitialentry. cfc_code_adjacent_current = ff_q_adjacent_currentcomputationinitialentry * S ((S (0)) * cfc_scale_adjacent_current) + (cfc_state_adjacent_currentcomputationinitial))))) /\ ((exists cfc_state_adjacent_currentcomputationterminal. ((exists cfc_left_adjacent_currentcomputationterminalcode cfc_right_adjacent_currentcomputationterminalcode cfc_matrix_adjacent_currentcomputationterminalcode. ((cfc_left_adjacent_currentcomputationterminalcode = ((u) + (cfc_previous_numerator_adjacent_current)) * S ((u) + (cfc_previous_numerator_adjacent_current)) + ((cfc_previous_numerator_adjacent_current) + (cfc_previous_numerator_adjacent_current))) /\ ((cfc_right_adjacent_currentcomputationterminalcode = ((v) + (cfc_previous_denominator_adjacent_current)) * S ((v) + (cfc_previous_denominator_adjacent_current)) + ((cfc_previous_denominator_adjacent_current) + (cfc_previous_denominator_adjacent_current))) /\ ((cfc_matrix_adjacent_currentcomputationterminalcode = ((cfc_left_adjacent_currentcomputationterminalcode) + (cfc_right_adjacent_currentcomputationterminalcode)) * S ((cfc_left_adjacent_currentcomputationterminalcode) + (cfc_right_adjacent_currentcomputationterminalcode)) + ((cfc_right_adjacent_currentcomputationterminalcode) + (cfc_right_adjacent_currentcomputationterminalcode))) /\ ((cfc_state_adjacent_currentcomputationterminal) = ((s) + (cfc_matrix_adjacent_currentcomputationterminalcode)) * S ((s) + (cfc_matrix_adjacent_currentcomputationterminalcode)) + ((cfc_matrix_adjacent_currentcomputationterminalcode) + (cfc_matrix_adjacent_currentcomputationterminalcode))))))) /\ (((exists ff_h_adjacent_currentcomputationterminalentry. ff_h_adjacent_currentcomputationterminalentry + S (cfc_state_adjacent_currentcomputationterminal) = S ((S (S ((S i)))) * cfc_scale_adjacent_current)) /\ exists ff_q_adjacent_currentcomputationterminalentry. cfc_code_adjacent_current = ff_q_adjacent_currentcomputationterminalentry * S ((S (S ((S i)))) * cfc_scale_adjacent_current) + (cfc_state_adjacent_currentcomputationterminal))))) /\ (forall cfc_index_adjacent_currentcomputation. (exists cfba_gap_adjacent_currentcomputationbound. cfba_gap_adjacent_currentcomputationbound + S (cfc_index_adjacent_currentcomputation) = (S ((S i)))) -> exists cfc_old_adjacent_currentcomputation cfc_a_adjacent_currentcomputation cfc_b_adjacent_currentcomputation cfc_c_adjacent_currentcomputation cfc_d_adjacent_currentcomputation cfc_new_adjacent_currentcomputation cfc_quotient_adjacent_currentcomputation. ((exists cfc_state_adjacent_currentcomputationprevious. ((exists cfc_left_adjacent_currentcomputationpreviouscode cfc_right_adjacent_currentcomputationpreviouscode cfc_matrix_adjacent_currentcomputationpreviouscode. ((cfc_left_adjacent_currentcomputationpreviouscode = ((cfc_a_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation)) * S ((cfc_a_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation)) + ((cfc_b_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation))) /\ ((cfc_right_adjacent_currentcomputationpreviouscode = ((cfc_c_adjacent_currentcomputation) + (cfc_d_adjacent_currentcomputation)) * S ((cfc_c_adjacent_currentcomputation) + (cfc_d_adjacent_currentcomputation)) + ((cfc_d_adjacent_currentcomputation) + (cfc_d_adjacent_currentcomputation))) /\ ((cfc_matrix_adjacent_currentcomputationpreviouscode = ((cfc_left_adjacent_currentcomputationpreviouscode) + (cfc_right_adjacent_currentcomputationpreviouscode)) * S ((cfc_left_adjacent_currentcomputationpreviouscode) + (cfc_right_adjacent_currentcomputationpreviouscode)) + ((cfc_right_adjacent_currentcomputationpreviouscode) + (cfc_right_adjacent_currentcomputationpreviouscode))) /\ ((cfc_state_adjacent_currentcomputationprevious) = ((cfc_old_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationpreviouscode)) * S ((cfc_old_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationpreviouscode)) + ((cfc_matrix_adjacent_currentcomputationpreviouscode) + (cfc_matrix_adjacent_currentcomputationpreviouscode))))))) /\ (((exists ff_h_adjacent_currentcomputationpreviousentry. ff_h_adjacent_currentcomputationpreviousentry + S (cfc_state_adjacent_currentcomputationprevious) = S ((S (cfc_index_adjacent_currentcomputation)) * cfc_scale_adjacent_current)) /\ exists ff_q_adjacent_currentcomputationpreviousentry. cfc_code_adjacent_current = ff_q_adjacent_currentcomputationpreviousentry * S ((S (cfc_index_adjacent_currentcomputation)) * cfc_scale_adjacent_current) + (cfc_state_adjacent_currentcomputationprevious))))) /\ ((exists cfc_state_adjacent_currentcomputationfollowing. ((exists cfc_left_adjacent_currentcomputationfollowingcode cfc_right_adjacent_currentcomputationfollowingcode cfc_matrix_adjacent_currentcomputationfollowingcode. ((cfc_left_adjacent_currentcomputationfollowingcode = (((cfc_quotient_adjacent_currentcomputation * cfc_a_adjacent_currentcomputation + cfc_c_adjacent_currentcomputation)) + ((cfc_quotient_adjacent_currentcomputation * cfc_b_adjacent_currentcomputation + cfc_d_adjacent_currentcomputation))) * S (((cfc_quotient_adjacent_currentcomputation * cfc_a_adjacent_currentcomputation + cfc_c_adjacent_currentcomputation)) + ((cfc_quotient_adjacent_currentcomputation * cfc_b_adjacent_currentcomputation + cfc_d_adjacent_currentcomputation))) + (((cfc_quotient_adjacent_currentcomputation * cfc_b_adjacent_currentcomputation + cfc_d_adjacent_currentcomputation)) + ((cfc_quotient_adjacent_currentcomputation * cfc_b_adjacent_currentcomputation + cfc_d_adjacent_currentcomputation)))) /\ ((cfc_right_adjacent_currentcomputationfollowingcode = ((cfc_a_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation)) * S ((cfc_a_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation)) + ((cfc_b_adjacent_currentcomputation) + (cfc_b_adjacent_currentcomputation))) /\ ((cfc_matrix_adjacent_currentcomputationfollowingcode = ((cfc_left_adjacent_currentcomputationfollowingcode) + (cfc_right_adjacent_currentcomputationfollowingcode)) * S ((cfc_left_adjacent_currentcomputationfollowingcode) + (cfc_right_adjacent_currentcomputationfollowingcode)) + ((cfc_right_adjacent_currentcomputationfollowingcode) + (cfc_right_adjacent_currentcomputationfollowingcode))) /\ ((cfc_state_adjacent_currentcomputationfollowing) = ((cfc_new_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationfollowingcode)) * S ((cfc_new_adjacent_currentcomputation) + (cfc_matrix_adjacent_currentcomputationfollowingcode)) + ((cfc_matrix_adjacent_currentcomputationfollowingcode) + (cfc_matrix_adjacent_currentcomputationfollowingcode))))))) /\ (((exists ff_h_adjacent_currentcomputationfollowingentry. ff_h_adjacent_currentcomputationfollowingentry + S (cfc_state_adjacent_currentcomputationfollowing) = S ((S (S cfc_index_adjacent_currentcomputation)) * cfc_scale_adjacent_current)) /\ exists ff_q_adjacent_currentcomputationfollowingentry. cfc_code_adjacent_current = ff_q_adjacent_currentcomputationfollowingentry * S ((S (S cfc_index_adjacent_currentcomputation)) * cfc_scale_adjacent_current) + (cfc_state_adjacent_currentcomputationfollowing))))) /\ (cfc_new_adjacent_currentcomputation = S ((cfc_quotient_adjacent_currentcomputation + cfc_old_adjacent_currentcomputation) * S (cfc_quotient_adjacent_currentcomputation + cfc_old_adjacent_currentcomputation) + (cfc_old_adjacent_currentcomputation + cfc_old_adjacent_currentcomputation))))))))))) -> (exists cfc_previous_numerator_adjacent_previous cfc_previous_denominator_adjacent_previous cfc_code_adjacent_previous cfc_scale_adjacent_previous. ((~(q = 0)) /\ (exists cfc_tail_adjacent_previouscomputation. ((exists cfc_state_adjacent_previouscomputationinitial. ((exists cfc_left_adjacent_previouscomputationinitialcode cfc_right_adjacent_previouscomputationinitialcode cfc_matrix_adjacent_previouscomputationinitialcode. ((cfc_left_adjacent_previouscomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_adjacent_previouscomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_adjacent_previouscomputationinitialcode = ((cfc_left_adjacent_previouscomputationinitialcode) + (cfc_right_adjacent_previouscomputationinitialcode)) * S ((cfc_left_adjacent_previouscomputationinitialcode) + (cfc_right_adjacent_previouscomputationinitialcode)) + ((cfc_right_adjacent_previouscomputationinitialcode) + (cfc_right_adjacent_previouscomputationinitialcode))) /\ ((cfc_state_adjacent_previouscomputationinitial) = ((cfc_tail_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationinitialcode)) * S ((cfc_tail_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationinitialcode)) + ((cfc_matrix_adjacent_previouscomputationinitialcode) + (cfc_matrix_adjacent_previouscomputationinitialcode))))))) /\ (((exists ff_h_adjacent_previouscomputationinitialentry. ff_h_adjacent_previouscomputationinitialentry + S (cfc_state_adjacent_previouscomputationinitial) = S ((S (0)) * cfc_scale_adjacent_previous)) /\ exists ff_q_adjacent_previouscomputationinitialentry. cfc_code_adjacent_previous = ff_q_adjacent_previouscomputationinitialentry * S ((S (0)) * cfc_scale_adjacent_previous) + (cfc_state_adjacent_previouscomputationinitial))))) /\ ((exists cfc_state_adjacent_previouscomputationterminal. ((exists cfc_left_adjacent_previouscomputationterminalcode cfc_right_adjacent_previouscomputationterminalcode cfc_matrix_adjacent_previouscomputationterminalcode. ((cfc_left_adjacent_previouscomputationterminalcode = ((p) + (cfc_previous_numerator_adjacent_previous)) * S ((p) + (cfc_previous_numerator_adjacent_previous)) + ((cfc_previous_numerator_adjacent_previous) + (cfc_previous_numerator_adjacent_previous))) /\ ((cfc_right_adjacent_previouscomputationterminalcode = ((q) + (cfc_previous_denominator_adjacent_previous)) * S ((q) + (cfc_previous_denominator_adjacent_previous)) + ((cfc_previous_denominator_adjacent_previous) + (cfc_previous_denominator_adjacent_previous))) /\ ((cfc_matrix_adjacent_previouscomputationterminalcode = ((cfc_left_adjacent_previouscomputationterminalcode) + (cfc_right_adjacent_previouscomputationterminalcode)) * S ((cfc_left_adjacent_previouscomputationterminalcode) + (cfc_right_adjacent_previouscomputationterminalcode)) + ((cfc_right_adjacent_previouscomputationterminalcode) + (cfc_right_adjacent_previouscomputationterminalcode))) /\ ((cfc_state_adjacent_previouscomputationterminal) = ((s) + (cfc_matrix_adjacent_previouscomputationterminalcode)) * S ((s) + (cfc_matrix_adjacent_previouscomputationterminalcode)) + ((cfc_matrix_adjacent_previouscomputationterminalcode) + (cfc_matrix_adjacent_previouscomputationterminalcode))))))) /\ (((exists ff_h_adjacent_previouscomputationterminalentry. ff_h_adjacent_previouscomputationterminalentry + S (cfc_state_adjacent_previouscomputationterminal) = S ((S (S (i))) * cfc_scale_adjacent_previous)) /\ exists ff_q_adjacent_previouscomputationterminalentry. cfc_code_adjacent_previous = ff_q_adjacent_previouscomputationterminalentry * S ((S (S (i))) * cfc_scale_adjacent_previous) + (cfc_state_adjacent_previouscomputationterminal))))) /\ (forall cfc_index_adjacent_previouscomputation. (exists cfba_gap_adjacent_previouscomputationbound. cfba_gap_adjacent_previouscomputationbound + S (cfc_index_adjacent_previouscomputation) = (S (i))) -> exists cfc_old_adjacent_previouscomputation cfc_a_adjacent_previouscomputation cfc_b_adjacent_previouscomputation cfc_c_adjacent_previouscomputation cfc_d_adjacent_previouscomputation cfc_new_adjacent_previouscomputation cfc_quotient_adjacent_previouscomputation. ((exists cfc_state_adjacent_previouscomputationprevious. ((exists cfc_left_adjacent_previouscomputationpreviouscode cfc_right_adjacent_previouscomputationpreviouscode cfc_matrix_adjacent_previouscomputationpreviouscode. ((cfc_left_adjacent_previouscomputationpreviouscode = ((cfc_a_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation)) * S ((cfc_a_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation)) + ((cfc_b_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation))) /\ ((cfc_right_adjacent_previouscomputationpreviouscode = ((cfc_c_adjacent_previouscomputation) + (cfc_d_adjacent_previouscomputation)) * S ((cfc_c_adjacent_previouscomputation) + (cfc_d_adjacent_previouscomputation)) + ((cfc_d_adjacent_previouscomputation) + (cfc_d_adjacent_previouscomputation))) /\ ((cfc_matrix_adjacent_previouscomputationpreviouscode = ((cfc_left_adjacent_previouscomputationpreviouscode) + (cfc_right_adjacent_previouscomputationpreviouscode)) * S ((cfc_left_adjacent_previouscomputationpreviouscode) + (cfc_right_adjacent_previouscomputationpreviouscode)) + ((cfc_right_adjacent_previouscomputationpreviouscode) + (cfc_right_adjacent_previouscomputationpreviouscode))) /\ ((cfc_state_adjacent_previouscomputationprevious) = ((cfc_old_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationpreviouscode)) * S ((cfc_old_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationpreviouscode)) + ((cfc_matrix_adjacent_previouscomputationpreviouscode) + (cfc_matrix_adjacent_previouscomputationpreviouscode))))))) /\ (((exists ff_h_adjacent_previouscomputationpreviousentry. ff_h_adjacent_previouscomputationpreviousentry + S (cfc_state_adjacent_previouscomputationprevious) = S ((S (cfc_index_adjacent_previouscomputation)) * cfc_scale_adjacent_previous)) /\ exists ff_q_adjacent_previouscomputationpreviousentry. cfc_code_adjacent_previous = ff_q_adjacent_previouscomputationpreviousentry * S ((S (cfc_index_adjacent_previouscomputation)) * cfc_scale_adjacent_previous) + (cfc_state_adjacent_previouscomputationprevious))))) /\ ((exists cfc_state_adjacent_previouscomputationfollowing. ((exists cfc_left_adjacent_previouscomputationfollowingcode cfc_right_adjacent_previouscomputationfollowingcode cfc_matrix_adjacent_previouscomputationfollowingcode. ((cfc_left_adjacent_previouscomputationfollowingcode = (((cfc_quotient_adjacent_previouscomputation * cfc_a_adjacent_previouscomputation + cfc_c_adjacent_previouscomputation)) + ((cfc_quotient_adjacent_previouscomputation * cfc_b_adjacent_previouscomputation + cfc_d_adjacent_previouscomputation))) * S (((cfc_quotient_adjacent_previouscomputation * cfc_a_adjacent_previouscomputation + cfc_c_adjacent_previouscomputation)) + ((cfc_quotient_adjacent_previouscomputation * cfc_b_adjacent_previouscomputation + cfc_d_adjacent_previouscomputation))) + (((cfc_quotient_adjacent_previouscomputation * cfc_b_adjacent_previouscomputation + cfc_d_adjacent_previouscomputation)) + ((cfc_quotient_adjacent_previouscomputation * cfc_b_adjacent_previouscomputation + cfc_d_adjacent_previouscomputation)))) /\ ((cfc_right_adjacent_previouscomputationfollowingcode = ((cfc_a_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation)) * S ((cfc_a_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation)) + ((cfc_b_adjacent_previouscomputation) + (cfc_b_adjacent_previouscomputation))) /\ ((cfc_matrix_adjacent_previouscomputationfollowingcode = ((cfc_left_adjacent_previouscomputationfollowingcode) + (cfc_right_adjacent_previouscomputationfollowingcode)) * S ((cfc_left_adjacent_previouscomputationfollowingcode) + (cfc_right_adjacent_previouscomputationfollowingcode)) + ((cfc_right_adjacent_previouscomputationfollowingcode) + (cfc_right_adjacent_previouscomputationfollowingcode))) /\ ((cfc_state_adjacent_previouscomputationfollowing) = ((cfc_new_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationfollowingcode)) * S ((cfc_new_adjacent_previouscomputation) + (cfc_matrix_adjacent_previouscomputationfollowingcode)) + ((cfc_matrix_adjacent_previouscomputationfollowingcode) + (cfc_matrix_adjacent_previouscomputationfollowingcode))))))) /\ (((exists ff_h_adjacent_previouscomputationfollowingentry. ff_h_adjacent_previouscomputationfollowingentry + S (cfc_state_adjacent_previouscomputationfollowing) = S ((S (S cfc_index_adjacent_previouscomputation)) * cfc_scale_adjacent_previous)) /\ exists ff_q_adjacent_previouscomputationfollowingentry. cfc_code_adjacent_previous = ff_q_adjacent_previouscomputationfollowingentry * S ((S (S cfc_index_adjacent_previouscomputation)) * cfc_scale_adjacent_previous) + (cfc_state_adjacent_previouscomputationfollowing))))) /\ (cfc_new_adjacent_previouscomputation = S ((cfc_quotient_adjacent_previouscomputation + cfc_old_adjacent_previouscomputation) * S (cfc_quotient_adjacent_previouscomputation + cfc_old_adjacent_previouscomputation) + (cfc_old_adjacent_previouscomputation + cfc_old_adjacent_previouscomputation))))))))))) -> (u * q + 1 = p * v \/ p * v + 1 = u * q)