BT0084

beta_range_empty

Stable · empty-context checked

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

Every consecutive beta range of length zero is vacuous.

Direct prerequisites: add_eq_zero_right, succ_ne_zero. The authored body proceeds by case analysis (1), intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero

Direct dependents

BT0086 beta_range_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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