scaled_pair_order_successor_lift_product_is_factorial

Exact expanded PA statement

forall b c f g n Q F. (forall fom_index_enr_generic_bounded. (exists fom_gap_enr_generic_bounded_index_bound. fom_gap_enr_generic_bounded_index_bound + S (fom_index_enr_generic_bounded) = n) -> exists fom_value_enr_generic_bounded. ((((exists fom_beta_height_enr_generic_bounded_entry. fom_beta_height_enr_generic_bounded_entry + S (fom_value_enr_generic_bounded) = S ((S (fom_index_enr_generic_bounded)) * c)) /\ exists fom_beta_quotient_enr_generic_bounded_entry. b = fom_beta_quotient_enr_generic_bounded_entry * S ((S (fom_index_enr_generic_bounded)) * c) + (fom_value_enr_generic_bounded))) /\ (exists fom_gap_enr_generic_bounded_value_bound. fom_gap_enr_generic_bounded_value_bound + S (fom_value_enr_generic_bounded) = n))) -> (forall wpo_injective_left_enr_generic_injective wpo_injective_right_enr_generic_injective wpo_injective_value_enr_generic_injective. (exists wpo_gap_enr_generic_injective_left_bound. wpo_gap_enr_generic_injective_left_bound + S (wpo_injective_left_enr_generic_injective) = n) -> (exists wpo_gap_enr_generic_injective_right_bound. wpo_gap_enr_generic_injective_right_bound + S (wpo_injective_right_enr_generic_injective) = n) -> (((exists wpo_beta_height_enr_generic_injective_left_entry. wpo_beta_height_enr_generic_injective_left_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_left_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_left_entry. b = wpo_beta_quotient_enr_generic_injective_left_entry * S ((S (wpo_injective_left_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> (((exists wpo_beta_height_enr_generic_injective_right_entry. wpo_beta_height_enr_generic_injective_right_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_right_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_right_entry. b = wpo_beta_quotient_enr_generic_injective_right_entry * S ((S (wpo_injective_right_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> wpo_injective_left_enr_generic_injective = wpo_injective_right_enr_generic_injective) -> (forall wsl_index_enr_generic_lift wsl_value_enr_generic_lift. (exists wpo_gap_enr_generic_lift_bound. wpo_gap_enr_generic_lift_bound + S (wsl_index_enr_generic_lift) = n) -> (((exists wpo_beta_height_enr_generic_lift_source. wpo_beta_height_enr_generic_lift_source + S (wsl_value_enr_generic_lift) = S ((S (wsl_index_enr_generic_lift)) * c)) /\ exists wpo_beta_quotient_enr_generic_lift_source. b = wpo_beta_quotient_enr_generic_lift_source * S ((S (wsl_index_enr_generic_lift)) * c) + (wsl_value_enr_generic_lift))) -> (((exists wpo_beta_height_enr_generic_lift_target. wpo_beta_height_enr_generic_lift_target + S (S wsl_value_enr_generic_lift) = S ((S (wsl_index_enr_generic_lift)) * g)) /\ exists wpo_beta_quotient_enr_generic_lift_target. f = wpo_beta_quotient_enr_generic_lift_target * S ((S (wsl_index_enr_generic_lift)) * g) + (S wsl_value_enr_generic_lift)))) -> (exists ff_u_enr_lifted_product ff_v_enr_lifted_product. ((((exists ff_h_enr_lifted_product_start. ff_h_enr_lifted_product_start + S (1) = S ((S (0)) * ff_v_enr_lifted_product)) /\ exists ff_q_enr_lifted_product_start. ff_u_enr_lifted_product = ff_q_enr_lifted_product_start * S ((S (0)) * ff_v_enr_lifted_product) + (1))) /\ ((((exists ff_h_enr_lifted_product_terminal. ff_h_enr_lifted_product_terminal + S (Q) = S ((S (n)) * ff_v_enr_lifted_product)) /\ exists ff_q_enr_lifted_product_terminal. ff_u_enr_lifted_product = ff_q_enr_lifted_product_terminal * S ((S (n)) * ff_v_enr_lifted_product) + (Q))) /\ forall ff_i_enr_lifted_product. (exists ff_lt_enr_lifted_product_bound. ff_lt_enr_lifted_product_bound + S ff_i_enr_lifted_product = n) -> exists ff_p_enr_lifted_product ff_r_enr_lifted_product ff_s_enr_lifted_product. ((((exists ff_h_enr_lifted_product_factor. ff_h_enr_lifted_product_factor + S (ff_p_enr_lifted_product) = S ((S (ff_i_enr_lifted_product)) * g)) /\ exists ff_q_enr_lifted_product_factor. f = ff_q_enr_lifted_product_factor * S ((S (ff_i_enr_lifted_product)) * g) + (ff_p_enr_lifted_product))) /\ ((((exists ff_h_enr_lifted_product_partial. ff_h_enr_lifted_product_partial + S (ff_r_enr_lifted_product) = S ((S (ff_i_enr_lifted_product)) * ff_v_enr_lifted_product)) /\ exists ff_q_enr_lifted_product_partial. ff_u_enr_lifted_product = ff_q_enr_lifted_product_partial * S ((S (ff_i_enr_lifted_product)) * ff_v_enr_lifted_product) + (ff_r_enr_lifted_product))) /\ ((((exists ff_h_enr_lifted_product_successor. ff_h_enr_lifted_product_successor + S (ff_s_enr_lifted_product) = S ((S (S ff_i_enr_lifted_product)) * ff_v_enr_lifted_product)) /\ exists ff_q_enr_lifted_product_successor. ff_u_enr_lifted_product = ff_q_enr_lifted_product_successor * S ((S (S ff_i_enr_lifted_product)) * ff_v_enr_lifted_product) + (ff_s_enr_lifted_product))) /\ ff_s_enr_lifted_product = ff_r_enr_lifted_product * ff_p_enr_lifted_product)))))) -> (exists ff_b_enr_factorial ff_c_enr_factorial. ((forall ff_i_enr_factorial_range. (exists ff_lt_enr_factorial_range_bound. ff_lt_enr_factorial_range_bound + S ff_i_enr_factorial_range = n) -> (((exists ff_h_enr_factorial_range_decoded. ff_h_enr_factorial_range_decoded + S (1 + ff_i_enr_factorial_range) = S ((S (ff_i_enr_factorial_range)) * ff_c_enr_factorial)) /\ exists ff_q_enr_factorial_range_decoded. ff_b_enr_factorial = ff_q_enr_factorial_range_decoded * S ((S (ff_i_enr_factorial_range)) * ff_c_enr_factorial) + (1 + ff_i_enr_factorial_range)))) /\ (exists ff_u_enr_factorial_product ff_v_enr_factorial_product. ((((exists ff_h_enr_factorial_product_start. ff_h_enr_factorial_product_start + S (1) = S ((S (0)) * ff_v_enr_factorial_product)) /\ exists ff_q_enr_factorial_product_start. ff_u_enr_factorial_product = ff_q_enr_factorial_product_start * S ((S (0)) * ff_v_enr_factorial_product) + (1))) /\ ((((exists ff_h_enr_factorial_product_terminal. ff_h_enr_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_enr_factorial_product)) /\ exists ff_q_enr_factorial_product_terminal. ff_u_enr_factorial_product = ff_q_enr_factorial_product_terminal * S ((S (n)) * ff_v_enr_factorial_product) + (F))) /\ forall ff_i_enr_factorial_product. (exists ff_lt_enr_factorial_product_bound. ff_lt_enr_factorial_product_bound + S ff_i_enr_factorial_product = n) -> exists ff_p_enr_factorial_product ff_r_enr_factorial_product ff_s_enr_factorial_product. ((((exists ff_h_enr_factorial_product_factor. ff_h_enr_factorial_product_factor + S (ff_p_enr_factorial_product) = S ((S (ff_i_enr_factorial_product)) * ff_c_enr_factorial)) /\ exists ff_q_enr_factorial_product_factor. ff_b_enr_factorial = ff_q_enr_factorial_product_factor * S ((S (ff_i_enr_factorial_product)) * ff_c_enr_factorial) + (ff_p_enr_factorial_product))) /\ ((((exists ff_h_enr_factorial_product_partial. ff_h_enr_factorial_product_partial + S (ff_r_enr_factorial_product) = S ((S (ff_i_enr_factorial_product)) * ff_v_enr_factorial_product)) /\ exists ff_q_enr_factorial_product_partial. ff_u_enr_factorial_product = ff_q_enr_factorial_product_partial * S ((S (ff_i_enr_factorial_product)) * ff_v_enr_factorial_product) + (ff_r_enr_factorial_product))) /\ ((((exists ff_h_enr_factorial_product_successor. ff_h_enr_factorial_product_successor + S (ff_s_enr_factorial_product) = S ((S (S ff_i_enr_factorial_product)) * ff_v_enr_factorial_product)) /\ exists ff_q_enr_factorial_product_successor. ff_u_enr_factorial_product = ff_q_enr_factorial_product_successor * S ((S (S ff_i_enr_factorial_product)) * ff_v_enr_factorial_product) + (ff_s_enr_factorial_product))) /\ ff_s_enr_factorial_product = ff_r_enr_factorial_product * ff_p_enr_factorial_product)))))))) -> Q = F