PA004P

finite_bounded_prefix_without_top

Stable checked-use theorem · independently closed

If a successor prefix omits its top value, its old prefix is bounded by the predecessor.

Exact expanded PA statement

forall b c n sn. sn = S n -> (forall fp_i_bounded_succ. (exists fp_gap_bounded_succ_index. fp_gap_bounded_succ_index + S fp_i_bounded_succ = sn) -> exists fp_value_bounded_succ. ((((exists ff_h_bounded_succ_entry. ff_h_bounded_succ_entry + S (fp_value_bounded_succ) = S ((S (fp_i_bounded_succ)) * c)) /\ exists ff_q_bounded_succ_entry. b = ff_q_bounded_succ_entry * S ((S (fp_i_bounded_succ)) * c) + (fp_value_bounded_succ))) /\ (exists fp_gap_bounded_succ_value. fp_gap_bounded_succ_value + S fp_value_bounded_succ = sn))) -> (forall i. (exists h. h + S i = n) -> ~(((exists ff_h_top_i. ff_h_top_i + S (n) = S ((S (i)) * c)) /\ exists ff_q_top_i. b = ff_q_top_i * S ((S (i)) * c) + (n)))) -> (forall fp_i_bounded_prefix. (exists fp_gap_bounded_prefix_index. fp_gap_bounded_prefix_index + S fp_i_bounded_prefix = n) -> exists fp_value_bounded_prefix. ((((exists ff_h_bounded_prefix_entry. ff_h_bounded_prefix_entry + S (fp_value_bounded_prefix) = S ((S (fp_i_bounded_prefix)) * c)) /\ exists ff_q_bounded_prefix_entry. b = ff_q_bounded_prefix_entry * S ((S (fp_i_bounded_prefix)) * c) + (fp_value_bounded_prefix))) /\ (exists fp_gap_bounded_prefix_value. fp_gap_bounded_prefix_value + S fp_value_bounded_prefix = n)))

Structural proof guide

Generated structural guide

If a successor prefix omits its top value, its old prefix is bounded by the predecessor.

Use the direct prerequisites le_succ, finite_lt_succ_eq_or_lt as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (2), equality transport (4).

Referenced ingredients

PA002O le_succ PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002O le_succ PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded

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 sn
  5. 0005intro hsn
  6. 0006intro hbounded
  7. 0007intro hnotop
  8. 0008rewrite hsn at hbounded
  9. 0009rewrite hsn at hbounded
  10. 0010intro i
  11. 0011intro hi
  12. 0012specialize hbounded i
  13. 0013have hfull : exists x. (((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) /\ exists h. h + S x = S n)
  14. 0014apply hbounded
  15. 0015specialize le_succ (S i)
  16. 0016specialize le_succ n
  17. 0017apply le_succ
  18. 0018exact hi
  19. 0019cases hfull
  20. 0020cases hfull_witness
  21. 0021have hsplit : x = n \/ exists h. h + S x = n
  22. 0022specialize finite_lt_succ_eq_or_lt n
  23. 0023specialize finite_lt_succ_eq_or_lt x
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hfull_witness_right
  26. 0026cases hsplit
  27. 0027exfalso
  28. 0028specialize hnotop i
  29. 0029apply hnotop
  30. 0030exact hi
  31. 0031rewrite <- hsplit_left
  32. 0032rewrite <- hsplit_left
  33. 0033exact hfull_witness_left
  34. 0034exists x
  35. 0035split
  36. 0036exact hfull_witness_left
  37. 0037exact hsplit_right