jordan_prime_power_tuple_primitivity_invariant

Exact expanded first-order arithmetic statement

forall p h j m n b c k. (~((p) = 1) /\ forall pvs_left_jordan_base pvs_right_jordan_base. (p) = pvs_left_jordan_base * pvs_right_jordan_base -> pvs_left_jordan_base = 1 \/ pvs_right_jordan_base = 1) -> (exists pa_b_pvs_jordan_first_power pa_c_pvs_jordan_first_power. ((forall pa_i_pvs_jordan_first_power_repeat. (exists pa_lt_pvs_jordan_first_power_repeat_bound. pa_lt_pvs_jordan_first_power_repeat_bound + S pa_i_pvs_jordan_first_power_repeat = S h) -> (((exists pa_h_pvs_jordan_first_power_repeat_decoded. pa_h_pvs_jordan_first_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_first_power_repeat)) * pa_c_pvs_jordan_first_power)) /\ exists pa_q_pvs_jordan_first_power_repeat_decoded. pa_b_pvs_jordan_first_power = pa_q_pvs_jordan_first_power_repeat_decoded * S ((S (pa_i_pvs_jordan_first_power_repeat)) * pa_c_pvs_jordan_first_power) + (p)))) /\ (exists pa_u_pvs_jordan_first_power_product pa_v_pvs_jordan_first_power_product. ((((exists pa_h_pvs_jordan_first_power_product_start. pa_h_pvs_jordan_first_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_start. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_start * S ((S (0)) * pa_v_pvs_jordan_first_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_first_power_product_terminal. pa_h_pvs_jordan_first_power_product_terminal + S (m) = S ((S (S h)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_terminal. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_terminal * S ((S (S h)) * pa_v_pvs_jordan_first_power_product) + (m))) /\ forall pa_i_pvs_jordan_first_power_product. (exists pa_lt_pvs_jordan_first_power_product_bound. pa_lt_pvs_jordan_first_power_product_bound + S pa_i_pvs_jordan_first_power_product = S h) -> exists pa_p_pvs_jordan_first_power_product pa_r_pvs_jordan_first_power_product pa_s_pvs_jordan_first_power_product. ((((exists pa_h_pvs_jordan_first_power_product_factor. pa_h_pvs_jordan_first_power_product_factor + S (pa_p_pvs_jordan_first_power_product) = S ((S (pa_i_pvs_jordan_first_power_product)) * pa_c_pvs_jordan_first_power)) /\ exists pa_q_pvs_jordan_first_power_product_factor. pa_b_pvs_jordan_first_power = pa_q_pvs_jordan_first_power_product_factor * S ((S (pa_i_pvs_jordan_first_power_product)) * pa_c_pvs_jordan_first_power) + (pa_p_pvs_jordan_first_power_product))) /\ ((((exists pa_h_pvs_jordan_first_power_product_partial. pa_h_pvs_jordan_first_power_product_partial + S (pa_r_pvs_jordan_first_power_product) = S ((S (pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_partial. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_partial * S ((S (pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product) + (pa_r_pvs_jordan_first_power_product))) /\ ((((exists pa_h_pvs_jordan_first_power_product_successor. pa_h_pvs_jordan_first_power_product_successor + S (pa_s_pvs_jordan_first_power_product) = S ((S (S pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_successor. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_successor * S ((S (S pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product) + (pa_s_pvs_jordan_first_power_product))) /\ pa_s_pvs_jordan_first_power_product = pa_r_pvs_jordan_first_power_product * pa_p_pvs_jordan_first_power_product)))))))) -> (exists pa_b_pvs_jordan_second_power pa_c_pvs_jordan_second_power. ((forall pa_i_pvs_jordan_second_power_repeat. (exists pa_lt_pvs_jordan_second_power_repeat_bound. pa_lt_pvs_jordan_second_power_repeat_bound + S pa_i_pvs_jordan_second_power_repeat = S j) -> (((exists pa_h_pvs_jordan_second_power_repeat_decoded. pa_h_pvs_jordan_second_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_second_power_repeat)) * pa_c_pvs_jordan_second_power)) /\ exists pa_q_pvs_jordan_second_power_repeat_decoded. pa_b_pvs_jordan_second_power = pa_q_pvs_jordan_second_power_repeat_decoded * S ((S (pa_i_pvs_jordan_second_power_repeat)) * pa_c_pvs_jordan_second_power) + (p)))) /\ (exists pa_u_pvs_jordan_second_power_product pa_v_pvs_jordan_second_power_product. ((((exists pa_h_pvs_jordan_second_power_product_start. pa_h_pvs_jordan_second_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_start. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_start * S ((S (0)) * pa_v_pvs_jordan_second_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_second_power_product_terminal. pa_h_pvs_jordan_second_power_product_terminal + S (n) = S ((S (S j)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_terminal. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_terminal * S ((S (S j)) * pa_v_pvs_jordan_second_power_product) + (n))) /\ forall pa_i_pvs_jordan_second_power_product. (exists pa_lt_pvs_jordan_second_power_product_bound. pa_lt_pvs_jordan_second_power_product_bound + S pa_i_pvs_jordan_second_power_product = S j) -> exists pa_p_pvs_jordan_second_power_product pa_r_pvs_jordan_second_power_product pa_s_pvs_jordan_second_power_product. ((((exists pa_h_pvs_jordan_second_power_product_factor. pa_h_pvs_jordan_second_power_product_factor + S (pa_p_pvs_jordan_second_power_product) = S ((S (pa_i_pvs_jordan_second_power_product)) * pa_c_pvs_jordan_second_power)) /\ exists pa_q_pvs_jordan_second_power_product_factor. pa_b_pvs_jordan_second_power = pa_q_pvs_jordan_second_power_product_factor * S ((S (pa_i_pvs_jordan_second_power_product)) * pa_c_pvs_jordan_second_power) + (pa_p_pvs_jordan_second_power_product))) /\ ((((exists pa_h_pvs_jordan_second_power_product_partial. pa_h_pvs_jordan_second_power_product_partial + S (pa_r_pvs_jordan_second_power_product) = S ((S (pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_partial. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_partial * S ((S (pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product) + (pa_r_pvs_jordan_second_power_product))) /\ ((((exists pa_h_pvs_jordan_second_power_product_successor. pa_h_pvs_jordan_second_power_product_successor + S (pa_s_pvs_jordan_second_power_product) = S ((S (S pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_successor. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_successor * S ((S (S pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product) + (pa_s_pvs_jordan_second_power_product))) /\ pa_s_pvs_jordan_second_power_product = pa_r_pvs_jordan_second_power_product * pa_p_pvs_jordan_second_power_product)))))))) -> (forall jt_divisor_jordan_first_primitive. (exists jt_factor_jordan_first_primitivemodulus. (m)=(jt_divisor_jordan_first_primitive)*jt_factor_jordan_first_primitivemodulus) -> (forall jt_index_jordan_first_primitivecoordinates jt_value_jordan_first_primitivecoordinates. (exists jt_gap_jordan_first_primitivecoordinatesindex. jt_gap_jordan_first_primitivecoordinatesindex+S (jt_index_jordan_first_primitivecoordinates)=(k)) -> (((exists fs_h_jt_jordan_first_primitivecoordinatesat. fs_h_jt_jordan_first_primitivecoordinatesat + S (jt_value_jordan_first_primitivecoordinates) = S ((S (jt_index_jordan_first_primitivecoordinates)) * c)) /\ exists fs_q_jt_jordan_first_primitivecoordinatesat. b = fs_q_jt_jordan_first_primitivecoordinatesat * S ((S (jt_index_jordan_first_primitivecoordinates)) * c) + (jt_value_jordan_first_primitivecoordinates))) -> (exists jt_factor_jordan_first_primitivecoordinatesdivides. (jt_value_jordan_first_primitivecoordinates)=(jt_divisor_jordan_first_primitive)*jt_factor_jordan_first_primitivecoordinatesdivides)) -> jt_divisor_jordan_first_primitive=1) -> forall jt_divisor_power_primitive. (exists jt_factor_power_primitivemodulus. (n)=(jt_divisor_power_primitive)*jt_factor_power_primitivemodulus) -> (forall jt_index_power_primitivecoordinates jt_value_power_primitivecoordinates. (exists jt_gap_power_primitivecoordinatesindex. jt_gap_power_primitivecoordinatesindex+S (jt_index_power_primitivecoordinates)=(k)) -> (((exists fs_h_jt_power_primitivecoordinatesat. fs_h_jt_power_primitivecoordinatesat + S (jt_value_power_primitivecoordinates) = S ((S (jt_index_power_primitivecoordinates)) * c)) /\ exists fs_q_jt_power_primitivecoordinatesat. b = fs_q_jt_power_primitivecoordinatesat * S ((S (jt_index_power_primitivecoordinates)) * c) + (jt_value_power_primitivecoordinates))) -> (exists jt_factor_power_primitivecoordinatesdivides. (jt_value_power_primitivecoordinates)=(jt_divisor_power_primitive)*jt_factor_power_primitivecoordinatesdivides)) -> jt_divisor_power_primitive=1