PA0006

beta_range_empty

Stable checked-use theorem · independently closed

Every consecutive beta range of length zero is vacuous.

Exact expanded PA statement

forall b c a l. l = 0 -> (forall ff_i_empty. (exists ff_lt_empty_bound. ff_lt_empty_bound + S ff_i_empty = l) -> (((exists ff_h_empty_decoded. ff_h_empty_decoded + S (a + ff_i_empty) = S ((S (ff_i_empty)) * c)) /\ exists ff_q_empty_decoded. b = ff_q_empty_decoded * S ((S (ff_i_empty)) * c) + (a + ff_i_empty))))

Structural proof guide

Generated structural guide

Every consecutive beta range of length zero is vacuous.

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

PA0030 beta_range_exists

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 a
  4. 0004intro l
  5. 0005intro hl
  6. 0006intro i
  7. 0007intro hi
  8. 0008rewrite hl at hi
  9. 0009exfalso
  10. 0010cases hi
  11. 0011have hsi : S i = 0
  12. 0012specialize add_eq_zero_right x
  13. 0013specialize add_eq_zero_right (S i)
  14. 0014apply add_eq_zero_right
  15. 0015exact hi_witness
  16. 0016specialize succ_ne_zero i
  17. 0017apply succ_ne_zero
  18. 0018exact hsi