floor_sqrt_above_root_power_two_strict

Exact expanded PA statement

forall x s p t. (((exists bcs_sqrt_lower_gap_bfsarpts_source. bcs_sqrt_lower_gap_bfsarpts_source + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_bfsarpts_source. bcs_sqrt_upper_gap_bfsarpts_source + S (x) = S (s) * S (s))) -> (exists bcf_lt_gap_bfsarpts_above. bcf_lt_gap_bfsarpts_above + S (s) = p) -> (exists bpvi_b_bfsarpts_power bpvi_c_bfsarpts_power. ((forall bpvi_i_bfsarpts_power. (exists bpvi_repeat_gap_bfsarpts_power. bpvi_repeat_gap_bfsarpts_power + S bpvi_i_bfsarpts_power = 2) -> (((exists bpvi_h_bfsarpts_power_repeat. bpvi_h_bfsarpts_power_repeat + S (p) = S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_repeat. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_repeat * S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (p)))) /\ (exists bpvi_u_bfsarpts_power bpvi_v_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_start. bpvi_h_bfsarpts_power_start + S (1) = S ((S (0)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_start. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_start * S ((S (0)) * bpvi_v_bfsarpts_power) + (1))) /\ ((((exists bpvi_h_bfsarpts_power_terminal. bpvi_h_bfsarpts_power_terminal + S (t) = S ((S (2)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_terminal. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_terminal * S ((S (2)) * bpvi_v_bfsarpts_power) + (t))) /\ forall bpvi_j_bfsarpts_power. (exists bpvi_product_gap_bfsarpts_power. bpvi_product_gap_bfsarpts_power + S bpvi_j_bfsarpts_power = 2) -> exists bpvi_factor_bfsarpts_power bpvi_partial_bfsarpts_power bpvi_successor_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_factor. bpvi_h_bfsarpts_power_factor + S (bpvi_factor_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_factor. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_factor * S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (bpvi_factor_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_partial. bpvi_h_bfsarpts_power_partial + S (bpvi_partial_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_partial. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_partial * S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_partial_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_successor. bpvi_h_bfsarpts_power_successor + S (bpvi_successor_bfsarpts_power) = S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_successor. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_successor * S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_successor_bfsarpts_power))) /\ bpvi_successor_bfsarpts_power = bpvi_partial_bfsarpts_power * bpvi_factor_bfsarpts_power)))))))) -> (exists bcf_lt_gap_bfsarpts_result. bcf_lt_gap_bfsarpts_result + S (x) = t)