euclidean_log_budget_successor_power

Exact expanded first-order arithmetic statement

forall a b n. (exists elb_list_doubled elb_history_doubled elb_scale_doubled elb_steps_doubled. ((exists cf_gcd_elb_doubled_budget. ((((exists ff_h_cf_elb_doubled_budget_initial_state. ff_h_cf_elb_doubled_budget_initial_state + S (((cf_gcd_elb_doubled_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_doubled_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_initial_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_initial_state * S ((S (0)) * elb_scale_doubled) + (((cf_gcd_elb_doubled_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_doubled_budget) + (((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_elb_doubled_budget_terminal_state. ff_h_cf_elb_doubled_budget_terminal_state + S (((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) * S ((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) + ((((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))))) = S ((S (elb_steps_doubled)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_terminal_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_terminal_state * S ((S (elb_steps_doubled)) * elb_scale_doubled) + (((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) * S ((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) + ((((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))))))) /\ forall cf_index_elb_doubled_budget. (exists ff_lt_cf_elb_doubled_budget_index. ff_lt_cf_elb_doubled_budget_index + S cf_index_elb_doubled_budget = elb_steps_doubled) -> exists cf_old_a_elb_doubled_budget cf_old_b_elb_doubled_budget cf_tail_elb_doubled_budget cf_new_a_elb_doubled_budget cf_new_b_elb_doubled_budget cf_head_elb_doubled_budget cf_quotient_elb_doubled_budget. ((((exists ff_h_cf_elb_doubled_budget_previous_state. ff_h_cf_elb_doubled_budget_previous_state + S (((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) * S ((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) + ((((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))))) = S ((S (cf_index_elb_doubled_budget)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_previous_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_previous_state * S ((S (cf_index_elb_doubled_budget)) * elb_scale_doubled) + (((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) * S ((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) + ((((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))))))) /\ ((((exists ff_h_cf_elb_doubled_budget_following_state. ff_h_cf_elb_doubled_budget_following_state + S (((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) * S ((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) + ((((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))))) = S ((S (S cf_index_elb_doubled_budget)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_following_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_following_state * S ((S (S cf_index_elb_doubled_budget)) * elb_scale_doubled) + (((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) * S ((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) + ((((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))))))) /\ (cf_new_b_elb_doubled_budget = cf_old_a_elb_doubled_budget /\ (cf_new_a_elb_doubled_budget = cf_new_b_elb_doubled_budget * cf_quotient_elb_doubled_budget + cf_old_b_elb_doubled_budget /\ ((exists ff_lt_cf_elb_doubled_budget_remainder. ff_lt_cf_elb_doubled_budget_remainder + S cf_old_b_elb_doubled_budget = cf_new_b_elb_doubled_budget) /\ (cf_head_elb_doubled_budget = S ((cf_quotient_elb_doubled_budget + cf_tail_elb_doubled_budget) * S (cf_quotient_elb_doubled_budget + cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget + cf_tail_elb_doubled_budget))))))))))) /\ exists elb_gap_doubled. elb_gap_doubled + elb_steps_doubled = (S (S (n + n))))) -> (exists elb_list_successor elb_history_successor elb_scale_successor elb_steps_successor. ((exists cf_gcd_elb_successor_budget. ((((exists ff_h_cf_elb_successor_budget_initial_state. ff_h_cf_elb_successor_budget_initial_state + S (((cf_gcd_elb_successor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_successor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_initial_state. elb_history_successor = ff_q_cf_elb_successor_budget_initial_state * S ((S (0)) * elb_scale_successor) + (((cf_gcd_elb_successor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_successor_budget) + (((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_elb_successor_budget_terminal_state. ff_h_cf_elb_successor_budget_terminal_state + S (((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) * S ((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) + ((((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))))) = S ((S (elb_steps_successor)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_terminal_state. elb_history_successor = ff_q_cf_elb_successor_budget_terminal_state * S ((S (elb_steps_successor)) * elb_scale_successor) + (((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) * S ((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) + ((((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))))))) /\ forall cf_index_elb_successor_budget. (exists ff_lt_cf_elb_successor_budget_index. ff_lt_cf_elb_successor_budget_index + S cf_index_elb_successor_budget = elb_steps_successor) -> exists cf_old_a_elb_successor_budget cf_old_b_elb_successor_budget cf_tail_elb_successor_budget cf_new_a_elb_successor_budget cf_new_b_elb_successor_budget cf_head_elb_successor_budget cf_quotient_elb_successor_budget. ((((exists ff_h_cf_elb_successor_budget_previous_state. ff_h_cf_elb_successor_budget_previous_state + S (((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) * S ((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) + ((((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))))) = S ((S (cf_index_elb_successor_budget)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_previous_state. elb_history_successor = ff_q_cf_elb_successor_budget_previous_state * S ((S (cf_index_elb_successor_budget)) * elb_scale_successor) + (((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) * S ((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) + ((((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))))))) /\ ((((exists ff_h_cf_elb_successor_budget_following_state. ff_h_cf_elb_successor_budget_following_state + S (((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) * S ((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) + ((((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))))) = S ((S (S cf_index_elb_successor_budget)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_following_state. elb_history_successor = ff_q_cf_elb_successor_budget_following_state * S ((S (S cf_index_elb_successor_budget)) * elb_scale_successor) + (((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) * S ((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) + ((((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))))))) /\ (cf_new_b_elb_successor_budget = cf_old_a_elb_successor_budget /\ (cf_new_a_elb_successor_budget = cf_new_b_elb_successor_budget * cf_quotient_elb_successor_budget + cf_old_b_elb_successor_budget /\ ((exists ff_lt_cf_elb_successor_budget_remainder. ff_lt_cf_elb_successor_budget_remainder + S cf_old_b_elb_successor_budget = cf_new_b_elb_successor_budget) /\ (cf_head_elb_successor_budget = S ((cf_quotient_elb_successor_budget + cf_tail_elb_successor_budget) * S (cf_quotient_elb_successor_budget + cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget + cf_tail_elb_successor_budget))))))))))) /\ exists elb_gap_successor. elb_gap_successor + elb_steps_successor = ((S n + S n))))