finite_injective_prefix_succ

Exact expanded PA statement

forall b c n sn. sn = S n -> (forall fp_i_inj_succ fp_j_inj_succ fp_value_inj_succ. (exists fp_gap_inj_succ_i. fp_gap_inj_succ_i + S fp_i_inj_succ = sn) -> (exists fp_gap_inj_succ_j. fp_gap_inj_succ_j + S fp_j_inj_succ = sn) -> (((exists ff_h_inj_succ_left. ff_h_inj_succ_left + S (fp_value_inj_succ) = S ((S (fp_i_inj_succ)) * c)) /\ exists ff_q_inj_succ_left. b = ff_q_inj_succ_left * S ((S (fp_i_inj_succ)) * c) + (fp_value_inj_succ))) -> (((exists ff_h_inj_succ_right. ff_h_inj_succ_right + S (fp_value_inj_succ) = S ((S (fp_j_inj_succ)) * c)) /\ exists ff_q_inj_succ_right. b = ff_q_inj_succ_right * S ((S (fp_j_inj_succ)) * c) + (fp_value_inj_succ))) -> fp_i_inj_succ = fp_j_inj_succ) -> (forall fp_i_inj_prefix fp_j_inj_prefix fp_value_inj_prefix. (exists fp_gap_inj_prefix_i. fp_gap_inj_prefix_i + S fp_i_inj_prefix = n) -> (exists fp_gap_inj_prefix_j. fp_gap_inj_prefix_j + S fp_j_inj_prefix = n) -> (((exists ff_h_inj_prefix_left. ff_h_inj_prefix_left + S (fp_value_inj_prefix) = S ((S (fp_i_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_left. b = ff_q_inj_prefix_left * S ((S (fp_i_inj_prefix)) * c) + (fp_value_inj_prefix))) -> (((exists ff_h_inj_prefix_right. ff_h_inj_prefix_right + S (fp_value_inj_prefix) = S ((S (fp_j_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_right. b = ff_q_inj_prefix_right * S ((S (fp_j_inj_prefix)) * c) + (fp_value_inj_prefix))) -> fp_i_inj_prefix = fp_j_inj_prefix)