beta_sum_succ_last_zero

Exact expanded PA statement

forall b c l n. (exists fs_u_blrr_drop_successor fs_v_blrr_drop_successor. ((((exists fs_h_blrr_drop_successor_body_start. fs_h_blrr_drop_successor_body_start + S (0) = S ((S (0)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_start. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_start * S ((S (0)) * fs_v_blrr_drop_successor) + (0))) /\ ((((exists fs_h_blrr_drop_successor_body_terminal. fs_h_blrr_drop_successor_body_terminal + S (n) = S ((S (S l)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_terminal. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_terminal * S ((S (S l)) * fs_v_blrr_drop_successor) + (n))) /\ forall fs_i_blrr_drop_successor_body_steps. (exists fs_lt_blrr_drop_successor_body_steps_bound. fs_lt_blrr_drop_successor_body_steps_bound + S fs_i_blrr_drop_successor_body_steps = S l) -> exists fs_a_blrr_drop_successor_body_steps fs_r_blrr_drop_successor_body_steps fs_s_blrr_drop_successor_body_steps. ((((exists fs_h_blrr_drop_successor_body_steps_summand. fs_h_blrr_drop_successor_body_steps_summand + S (fs_a_blrr_drop_successor_body_steps) = S ((S (fs_i_blrr_drop_successor_body_steps)) * c)) /\ exists fs_q_blrr_drop_successor_body_steps_summand. b = fs_q_blrr_drop_successor_body_steps_summand * S ((S (fs_i_blrr_drop_successor_body_steps)) * c) + (fs_a_blrr_drop_successor_body_steps))) /\ ((((exists fs_h_blrr_drop_successor_body_steps_partial. fs_h_blrr_drop_successor_body_steps_partial + S (fs_r_blrr_drop_successor_body_steps) = S ((S (fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_steps_partial. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_steps_partial * S ((S (fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor) + (fs_r_blrr_drop_successor_body_steps))) /\ ((((exists fs_h_blrr_drop_successor_body_steps_successor. fs_h_blrr_drop_successor_body_steps_successor + S (fs_s_blrr_drop_successor_body_steps) = S ((S (S fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_steps_successor. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_steps_successor * S ((S (S fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor) + (fs_s_blrr_drop_successor_body_steps))) /\ fs_s_blrr_drop_successor_body_steps = fs_r_blrr_drop_successor_body_steps + fs_a_blrr_drop_successor_body_steps)))))) -> (((exists fs_h_blrr_drop_zero. fs_h_blrr_drop_zero + S (0) = S ((S (l)) * c)) /\ exists fs_q_blrr_drop_zero. b = fs_q_blrr_drop_zero * S ((S (l)) * c) + (0))) -> (exists ff_u_blrr_drop_predecessor ff_v_blrr_drop_predecessor. ((((exists ff_h_blrr_drop_predecessor_start. ff_h_blrr_drop_predecessor_start + S (0) = S ((S (0)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_start. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_start * S ((S (0)) * ff_v_blrr_drop_predecessor) + (0))) /\ ((((exists ff_h_blrr_drop_predecessor_terminal. ff_h_blrr_drop_predecessor_terminal + S (n) = S ((S (l)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_terminal. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_terminal * S ((S (l)) * ff_v_blrr_drop_predecessor) + (n))) /\ forall ff_i_blrr_drop_predecessor. (exists ff_lt_blrr_drop_predecessor_bound. ff_lt_blrr_drop_predecessor_bound + S ff_i_blrr_drop_predecessor = l) -> exists ff_a_blrr_drop_predecessor ff_r_blrr_drop_predecessor ff_s_blrr_drop_predecessor. ((((exists ff_h_blrr_drop_predecessor_summand. ff_h_blrr_drop_predecessor_summand + S (ff_a_blrr_drop_predecessor) = S ((S (ff_i_blrr_drop_predecessor)) * c)) /\ exists ff_q_blrr_drop_predecessor_summand. b = ff_q_blrr_drop_predecessor_summand * S ((S (ff_i_blrr_drop_predecessor)) * c) + (ff_a_blrr_drop_predecessor))) /\ ((((exists ff_h_blrr_drop_predecessor_partial. ff_h_blrr_drop_predecessor_partial + S (ff_r_blrr_drop_predecessor) = S ((S (ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_partial. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_partial * S ((S (ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor) + (ff_r_blrr_drop_predecessor))) /\ ((((exists ff_h_blrr_drop_predecessor_successor. ff_h_blrr_drop_predecessor_successor + S (ff_s_blrr_drop_predecessor) = S ((S (S ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_successor. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_successor * S ((S (S ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor) + (ff_s_blrr_drop_predecessor))) /\ ff_s_blrr_drop_predecessor = ff_r_blrr_drop_predecessor + ff_a_blrr_drop_predecessor))))))