BT0086

beta_range_exists

Stable · empty-context checked

Every start and length admit a beta-coded consecutive range.

Exact expanded PA statement

forall a l. exists b c. (forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> (((exists ff_h_r_decoded. ff_h_r_decoded + S (a + ff_i_r) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_decoded. b = ff_q_r_decoded * S ((S (ff_i_r)) * c) + (a + ff_i_r))))

Structural proof guide

Every start and length admit a beta-coded consecutive range.

Direct prerequisites: beta_range_empty, beta_range_succ_extend. The authored body proceeds by structural induction (1), case analysis (2).

Proof neighborhood

Direct dependencies

BT0084 beta_range_empty BT0085 beta_range_succ_extend

Direct dependents

BT008Y factorial_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 a
  2. 0002induction l
  3. 0003exists 0
  4. 0004exists 0
  5. 0005specialize beta_range_empty 0
  6. 0006specialize beta_range_empty 0
  7. 0007specialize beta_range_empty a
  8. 0008specialize beta_range_empty 0
  9. 0009apply beta_range_empty
  10. 0010refl
  11. 0011cases IH
  12. 0012cases IH_witness
  13. 0013specialize beta_range_succ_extend x
  14. 0014specialize beta_range_succ_extend x1
  15. 0015specialize beta_range_succ_extend a
  16. 0016specialize beta_range_succ_extend l
  17. 0017specialize beta_range_succ_extend (S l)
  18. 0018apply beta_range_succ_extend
  19. 0019refl
  20. 0020exact IH_witness_witness