EuclideanBoundedTrace(a,b,B)

Hygienic expanded first-order definition

exists elb_list_milestone elb_history_milestone elb_scale_milestone elb_steps_milestone. ((exists cf_gcd_elb_milestone_budget. ((((exists ff_h_cf_elb_milestone_budget_initial_state. ff_h_cf_elb_milestone_budget_initial_state + S (((cf_gcd_elb_milestone_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_milestone_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_milestone)) /\ exists ff_q_cf_elb_milestone_budget_initial_state. elb_history_milestone = ff_q_cf_elb_milestone_budget_initial_state * S ((S (0)) * elb_scale_milestone) + (((cf_gcd_elb_milestone_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_milestone_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_milestone_budget_terminal_state. ff_h_cf_elb_milestone_budget_terminal_state + S (((a) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone)))) * S ((a) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone)))) + ((((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone))) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone))))) = S ((S (elb_steps_milestone)) * elb_scale_milestone)) /\ exists ff_q_cf_elb_milestone_budget_terminal_state. elb_history_milestone = ff_q_cf_elb_milestone_budget_terminal_state * S ((S (elb_steps_milestone)) * elb_scale_milestone) + (((a) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone)))) * S ((a) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone)))) + ((((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone))) + (((b) + (elb_list_milestone)) * S ((b) + (elb_list_milestone)) + ((elb_list_milestone) + (elb_list_milestone))))))) /\ forall cf_index_elb_milestone_budget. (exists ff_lt_cf_elb_milestone_budget_index. ff_lt_cf_elb_milestone_budget_index + S cf_index_elb_milestone_budget = elb_steps_milestone) -> exists cf_old_a_elb_milestone_budget cf_old_b_elb_milestone_budget cf_tail_elb_milestone_budget cf_new_a_elb_milestone_budget cf_new_b_elb_milestone_budget cf_head_elb_milestone_budget cf_quotient_elb_milestone_budget. ((((exists ff_h_cf_elb_milestone_budget_previous_state. ff_h_cf_elb_milestone_budget_previous_state + S (((cf_old_a_elb_milestone_budget) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget)))) * S ((cf_old_a_elb_milestone_budget) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget)))) + ((((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget))) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget))))) = S ((S (cf_index_elb_milestone_budget)) * elb_scale_milestone)) /\ exists ff_q_cf_elb_milestone_budget_previous_state. elb_history_milestone = ff_q_cf_elb_milestone_budget_previous_state * S ((S (cf_index_elb_milestone_budget)) * elb_scale_milestone) + (((cf_old_a_elb_milestone_budget) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget)))) * S ((cf_old_a_elb_milestone_budget) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget)))) + ((((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget))) + (((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) * S ((cf_old_b_elb_milestone_budget) + (cf_tail_elb_milestone_budget)) + ((cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget))))))) /\ ((((exists ff_h_cf_elb_milestone_budget_following_state. ff_h_cf_elb_milestone_budget_following_state + S (((cf_new_a_elb_milestone_budget) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget)))) * S ((cf_new_a_elb_milestone_budget) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget)))) + ((((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget))) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget))))) = S ((S (S cf_index_elb_milestone_budget)) * elb_scale_milestone)) /\ exists ff_q_cf_elb_milestone_budget_following_state. elb_history_milestone = ff_q_cf_elb_milestone_budget_following_state * S ((S (S cf_index_elb_milestone_budget)) * elb_scale_milestone) + (((cf_new_a_elb_milestone_budget) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget)))) * S ((cf_new_a_elb_milestone_budget) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget)))) + ((((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget))) + (((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) * S ((cf_new_b_elb_milestone_budget) + (cf_head_elb_milestone_budget)) + ((cf_head_elb_milestone_budget) + (cf_head_elb_milestone_budget))))))) /\ (cf_new_b_elb_milestone_budget = cf_old_a_elb_milestone_budget /\ (cf_new_a_elb_milestone_budget = cf_new_b_elb_milestone_budget * cf_quotient_elb_milestone_budget + cf_old_b_elb_milestone_budget /\ ((exists ff_lt_cf_elb_milestone_budget_remainder. ff_lt_cf_elb_milestone_budget_remainder + S cf_old_b_elb_milestone_budget = cf_new_b_elb_milestone_budget) /\ (cf_head_elb_milestone_budget = S ((cf_quotient_elb_milestone_budget + cf_tail_elb_milestone_budget) * S (cf_quotient_elb_milestone_budget + cf_tail_elb_milestone_budget) + (cf_tail_elb_milestone_budget + cf_tail_elb_milestone_budget))))))))))) /\ exists elb_gap_milestone. elb_gap_milestone + elb_steps_milestone = (B))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition