beta_pointwise_mul_prefix_drop_last

Exact expanded PA statement

forall mb mc sb sc tb tc l. (forall fpmp_index_drop_successor fpmp_left_drop_successor fpmp_right_drop_successor fpmp_target_drop_successor. (exists fpmp_gap_drop_successor. fpmp_gap_drop_successor + S fpmp_index_drop_successor = S l) -> (((exists ff_h_fpmp_drop_successor_left. ff_h_fpmp_drop_successor_left + S (fpmp_left_drop_successor) = S ((S (fpmp_index_drop_successor)) * mc)) /\ exists ff_q_fpmp_drop_successor_left. mb = ff_q_fpmp_drop_successor_left * S ((S (fpmp_index_drop_successor)) * mc) + (fpmp_left_drop_successor))) -> (((exists ff_h_fpmp_drop_successor_right. ff_h_fpmp_drop_successor_right + S (fpmp_right_drop_successor) = S ((S (fpmp_index_drop_successor)) * sc)) /\ exists ff_q_fpmp_drop_successor_right. sb = ff_q_fpmp_drop_successor_right * S ((S (fpmp_index_drop_successor)) * sc) + (fpmp_right_drop_successor))) -> (((exists ff_h_fpmp_drop_successor_target. ff_h_fpmp_drop_successor_target + S (fpmp_target_drop_successor) = S ((S (fpmp_index_drop_successor)) * tc)) /\ exists ff_q_fpmp_drop_successor_target. tb = ff_q_fpmp_drop_successor_target * S ((S (fpmp_index_drop_successor)) * tc) + (fpmp_target_drop_successor))) -> fpmp_target_drop_successor = fpmp_left_drop_successor * fpmp_right_drop_successor) -> (forall fpmp_index_drop_prefix fpmp_left_drop_prefix fpmp_right_drop_prefix fpmp_target_drop_prefix. (exists fpmp_gap_drop_prefix. fpmp_gap_drop_prefix + S fpmp_index_drop_prefix = l) -> (((exists ff_h_fpmp_drop_prefix_left. ff_h_fpmp_drop_prefix_left + S (fpmp_left_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * mc)) /\ exists ff_q_fpmp_drop_prefix_left. mb = ff_q_fpmp_drop_prefix_left * S ((S (fpmp_index_drop_prefix)) * mc) + (fpmp_left_drop_prefix))) -> (((exists ff_h_fpmp_drop_prefix_right. ff_h_fpmp_drop_prefix_right + S (fpmp_right_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * sc)) /\ exists ff_q_fpmp_drop_prefix_right. sb = ff_q_fpmp_drop_prefix_right * S ((S (fpmp_index_drop_prefix)) * sc) + (fpmp_right_drop_prefix))) -> (((exists ff_h_fpmp_drop_prefix_target. ff_h_fpmp_drop_prefix_target + S (fpmp_target_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * tc)) /\ exists ff_q_fpmp_drop_prefix_target. tb = ff_q_fpmp_drop_prefix_target * S ((S (fpmp_index_drop_prefix)) * tc) + (fpmp_target_drop_prefix))) -> fpmp_target_drop_prefix = fpmp_left_drop_prefix * fpmp_right_drop_prefix)