BT007W

beta_repeat_exists

Stable · empty-context checked

Every value and length admit a beta-coded constant prefix.

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) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_decoded. b = ff_q_r_decoded * S ((S (ff_i_r)) * c) + (a))))

Structural proof guide

Every value and length admit a beta-coded constant prefix.

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

Proof neighborhood

Direct dependencies

BT007U beta_repeat_empty BT007V beta_repeat_succ_extend

Direct dependents

BT0080 pow_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_repeat_empty 0
  6. 0006specialize beta_repeat_empty 0
  7. 0007specialize beta_repeat_empty a
  8. 0008specialize beta_repeat_empty 0
  9. 0009apply beta_repeat_empty
  10. 0010refl
  11. 0011cases IH
  12. 0012cases IH_witness
  13. 0013specialize beta_repeat_succ_extend x
  14. 0014specialize beta_repeat_succ_extend x1
  15. 0015specialize beta_repeat_succ_extend a
  16. 0016specialize beta_repeat_succ_extend l
  17. 0017specialize beta_repeat_succ_extend (S l)
  18. 0018apply beta_repeat_succ_extend
  19. 0019refl
  20. 0020exact IH_witness_witness