PA004Q — finite_injective_prefix

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)

Structural proof guide

Generated structural guide

Injectivity of a successor prefix restricts to its old prefix.

Use the direct prerequisites le_succ as previously established PA formulas.

The proof proceeds by equality transport (2).

Referenced ingredients

PA002O le_succ

Proof neighborhood

Direct dependencies

PA002O le_succ

Direct dependents

PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.