BT007V

beta_repeat_succ_extend

Stable · empty-context checked

Recode a constant prefix and append one more copy of its value.

Exact expanded PA statement

forall b c a l sl. sl = S l -> (forall ff_i_before. (exists ff_lt_before_bound. ff_lt_before_bound + S ff_i_before = l) -> (((exists ff_h_before_decoded. ff_h_before_decoded + S (a) = S ((S (ff_i_before)) * c)) /\ exists ff_q_before_decoded. b = ff_q_before_decoded * S ((S (ff_i_before)) * c) + (a)))) -> exists z d. (forall ff_i_after. (exists ff_lt_after_bound. ff_lt_after_bound + S ff_i_after = sl) -> (((exists ff_h_after_decoded. ff_h_after_decoded + S (a) = S ((S (ff_i_after)) * d)) /\ exists ff_q_after_decoded. z = ff_q_after_decoded * S ((S (ff_i_after)) * d) + (a))))

Structural proof guide

Recode a constant prefix and append one more copy of its value.

Direct prerequisites: beta_prefix_extend, le_of_succ_le_succ, le_eq_or_lt. The authored body proceeds by case analysis (4), intermediate claims (2), equality transport (3).

Proof neighborhood

Direct dependencies

BT005D beta_prefix_extend BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct dependents

BT007W beta_repeat_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 sl
  6. 0006intro hsl
  7. 0007intro hrepeat
  8. 0008specialize beta_prefix_extend l
  9. 0009specialize beta_prefix_extend b
  10. 0010specialize beta_prefix_extend c
  11. 0011specialize beta_prefix_extend a
  12. 0012cases beta_prefix_extend
  13. 0013cases beta_prefix_extend_witness
  14. 0014cases beta_prefix_extend_witness_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017intro i
  18. 0018intro hi
  19. 0019rewrite hsl at hi
  20. 0020have hil : exists h. h + i = l
  21. 0021specialize le_of_succ_le_succ i
  22. 0022specialize le_of_succ_le_succ l
  23. 0023apply le_of_succ_le_succ
  24. 0024exact hi
  25. 0025have hsplit : i = l \/ exists h. h + S i = l
  26. 0026specialize le_eq_or_lt i
  27. 0027specialize le_eq_or_lt l
  28. 0028apply le_eq_or_lt
  29. 0029exact hil
  30. 0030cases hsplit
  31. 0031rewrite hsplit_left
  32. 0032rewrite hsplit_left
  33. 0033exact beta_prefix_extend_witness_witness_left
  34. 0034specialize beta_prefix_extend_witness_witness_right i
  35. 0035specialize beta_prefix_extend_witness_witness_right a
  36. 0036apply beta_prefix_extend_witness_witness_right
  37. 0037exact hsplit_right
  38. 0038specialize hrepeat i
  39. 0039apply hrepeat
  40. 0040exact hsplit_right