power_quotient_prefix_transport

Exact expanded PA statement

forall p n b c z d l. (forall bls_index_bls_transport_source. (exists bls_gap_bls_transport_source_bound. bls_gap_bls_transport_source_bound + S (bls_index_bls_transport_source) = (l)) -> exists bls_power_bls_transport_source bls_quotient_bls_transport_source bls_remainder_bls_transport_source. ((exists bpvi_b_bls_bls_transport_source_power bpvi_c_bls_bls_transport_source_power. ((forall bpvi_i_bls_bls_transport_source_power. (exists bpvi_repeat_gap_bls_bls_transport_source_power. bpvi_repeat_gap_bls_bls_transport_source_power + S bpvi_i_bls_bls_transport_source_power = S bls_index_bls_transport_source) -> (((exists bpvi_h_bls_bls_transport_source_power_repeat. bpvi_h_bls_bls_transport_source_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_repeat. bpvi_b_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_repeat * S ((S (bpvi_i_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power) + (p)))) /\ (exists bpvi_u_bls_bls_transport_source_power bpvi_v_bls_bls_transport_source_power. ((((exists bpvi_h_bls_bls_transport_source_power_start. bpvi_h_bls_bls_transport_source_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_start. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_start * S ((S (0)) * bpvi_v_bls_bls_transport_source_power) + (1))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_terminal. bpvi_h_bls_bls_transport_source_power_terminal + S (bls_power_bls_transport_source) = S ((S (S bls_index_bls_transport_source)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_terminal. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_terminal * S ((S (S bls_index_bls_transport_source)) * bpvi_v_bls_bls_transport_source_power) + (bls_power_bls_transport_source))) /\ forall bpvi_j_bls_bls_transport_source_power. (exists bpvi_product_gap_bls_bls_transport_source_power. bpvi_product_gap_bls_bls_transport_source_power + S bpvi_j_bls_bls_transport_source_power = S bls_index_bls_transport_source) -> exists bpvi_factor_bls_bls_transport_source_power bpvi_partial_bls_bls_transport_source_power bpvi_successor_bls_bls_transport_source_power. ((((exists bpvi_h_bls_bls_transport_source_power_factor. bpvi_h_bls_bls_transport_source_power_factor + S (bpvi_factor_bls_bls_transport_source_power) = S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_factor. bpvi_b_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_factor * S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power) + (bpvi_factor_bls_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_partial. bpvi_h_bls_bls_transport_source_power_partial + S (bpvi_partial_bls_bls_transport_source_power) = S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_partial. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_partial * S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power) + (bpvi_partial_bls_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_successor. bpvi_h_bls_bls_transport_source_power_successor + S (bpvi_successor_bls_bls_transport_source_power) = S ((S (S bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_successor. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_successor * S ((S (S bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power) + (bpvi_successor_bls_bls_transport_source_power))) /\ bpvi_successor_bls_bls_transport_source_power = bpvi_partial_bls_bls_transport_source_power * bpvi_factor_bls_bls_transport_source_power)))))))) /\ ((((exists ff_h_bls_bls_transport_source_quotient_entry. ff_h_bls_bls_transport_source_quotient_entry + S (bls_quotient_bls_transport_source) = S ((S (bls_index_bls_transport_source)) * c)) /\ exists ff_q_bls_bls_transport_source_quotient_entry. b = ff_q_bls_bls_transport_source_quotient_entry * S ((S (bls_index_bls_transport_source)) * c) + (bls_quotient_bls_transport_source))) /\ ((n = bls_power_bls_transport_source * bls_quotient_bls_transport_source + bls_remainder_bls_transport_source /\ exists bls_remainder_gap_bls_transport_source_division. bls_remainder_gap_bls_transport_source_division + S (bls_remainder_bls_transport_source) = bls_power_bls_transport_source))))) -> (forall bls_index_bls_transport_target. (exists bls_gap_bls_transport_target_bound. bls_gap_bls_transport_target_bound + S (bls_index_bls_transport_target) = (l)) -> exists bls_power_bls_transport_target bls_quotient_bls_transport_target bls_remainder_bls_transport_target. ((exists bpvi_b_bls_bls_transport_target_power bpvi_c_bls_bls_transport_target_power. ((forall bpvi_i_bls_bls_transport_target_power. (exists bpvi_repeat_gap_bls_bls_transport_target_power. bpvi_repeat_gap_bls_bls_transport_target_power + S bpvi_i_bls_bls_transport_target_power = S bls_index_bls_transport_target) -> (((exists bpvi_h_bls_bls_transport_target_power_repeat. bpvi_h_bls_bls_transport_target_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_repeat. bpvi_b_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_repeat * S ((S (bpvi_i_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power) + (p)))) /\ (exists bpvi_u_bls_bls_transport_target_power bpvi_v_bls_bls_transport_target_power. ((((exists bpvi_h_bls_bls_transport_target_power_start. bpvi_h_bls_bls_transport_target_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_start. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_start * S ((S (0)) * bpvi_v_bls_bls_transport_target_power) + (1))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_terminal. bpvi_h_bls_bls_transport_target_power_terminal + S (bls_power_bls_transport_target) = S ((S (S bls_index_bls_transport_target)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_terminal. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_terminal * S ((S (S bls_index_bls_transport_target)) * bpvi_v_bls_bls_transport_target_power) + (bls_power_bls_transport_target))) /\ forall bpvi_j_bls_bls_transport_target_power. (exists bpvi_product_gap_bls_bls_transport_target_power. bpvi_product_gap_bls_bls_transport_target_power + S bpvi_j_bls_bls_transport_target_power = S bls_index_bls_transport_target) -> exists bpvi_factor_bls_bls_transport_target_power bpvi_partial_bls_bls_transport_target_power bpvi_successor_bls_bls_transport_target_power. ((((exists bpvi_h_bls_bls_transport_target_power_factor. bpvi_h_bls_bls_transport_target_power_factor + S (bpvi_factor_bls_bls_transport_target_power) = S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_factor. bpvi_b_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_factor * S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power) + (bpvi_factor_bls_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_partial. bpvi_h_bls_bls_transport_target_power_partial + S (bpvi_partial_bls_bls_transport_target_power) = S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_partial. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_partial * S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power) + (bpvi_partial_bls_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_successor. bpvi_h_bls_bls_transport_target_power_successor + S (bpvi_successor_bls_bls_transport_target_power) = S ((S (S bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_successor. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_successor * S ((S (S bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power) + (bpvi_successor_bls_bls_transport_target_power))) /\ bpvi_successor_bls_bls_transport_target_power = bpvi_partial_bls_bls_transport_target_power * bpvi_factor_bls_bls_transport_target_power)))))))) /\ ((((exists ff_h_bls_bls_transport_target_quotient_entry. ff_h_bls_bls_transport_target_quotient_entry + S (bls_quotient_bls_transport_target) = S ((S (bls_index_bls_transport_target)) * d)) /\ exists ff_q_bls_bls_transport_target_quotient_entry. z = ff_q_bls_bls_transport_target_quotient_entry * S ((S (bls_index_bls_transport_target)) * d) + (bls_quotient_bls_transport_target))) /\ ((n = bls_power_bls_transport_target * bls_quotient_bls_transport_target + bls_remainder_bls_transport_target /\ exists bls_remainder_gap_bls_transport_target_division. bls_remainder_gap_bls_transport_target_division + S (bls_remainder_bls_transport_target) = bls_power_bls_transport_target))))) -> forall i q. (exists bls_gap_bls_transport_bound. bls_gap_bls_transport_bound + S (i) = (l)) -> (((exists ff_h_bls_transport_given. ff_h_bls_transport_given + S (q) = S ((S (i)) * c)) /\ exists ff_q_bls_transport_given. b = ff_q_bls_transport_given * S ((S (i)) * c) + (q))) -> (((exists ff_h_bls_transport_result. ff_h_bls_transport_result + S (q) = S ((S (i)) * d)) /\ exists ff_q_bls_transport_result. z = ff_q_bls_transport_result * S ((S (i)) * d) + (q)))