PA004F

finite_surjective_zero

Stable checked-use theorem · independently closed

The empty decoded prefix is surjective onto the empty interval.

Exact expanded PA statement

forall b c n. n = 0 -> (forall fp_value_zero. (exists fp_gap_zero_value. fp_gap_zero_value + S fp_value_zero = n) -> exists fp_i_zero. ((exists fp_gap_zero_index. fp_gap_zero_index + S fp_i_zero = n) /\ (((exists ff_h_zero_entry. ff_h_zero_entry + S (fp_value_zero) = S ((S (fp_i_zero)) * c)) /\ exists ff_q_zero_entry. b = ff_q_zero_entry * S ((S (fp_i_zero)) * c) + (fp_value_zero)))))

Structural proof guide

Generated structural guide

The empty decoded prefix is surjective onto the empty interval.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1), equality transport (1).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Direct dependents

PA004W finite_bounded_injective_surjective

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.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro hn
  5. 0005intro y
  6. 0006intro hy
  7. 0007rewrite hn at hy
  8. 0008exfalso
  9. 0009cases hy
  10. 0010have hsy : S y = 0
  11. 0011specialize add_eq_zero_right x
  12. 0012specialize add_eq_zero_right (S y)
  13. 0013apply add_eq_zero_right
  14. 0014exact hy_witness
  15. 0015specialize succ_ne_zero y
  16. 0016apply succ_ne_zero
  17. 0017exact hsy