PA007S

beta_magnitude_predecessor_recode_bounded

Alpha v16 checked-use theorem · independently closed; not Stable

Removing one successor turns the positive 1,...,l range bound into the finite 0,...,l-1 bound.

Exact expanded PA statement

forall mb mc rb rc l. (forall gmp_index_predecessor_transport_finite_range. (exists gsp_lt_gap_predecessor_transport_finite_range_index_bound. gsp_lt_gap_predecessor_transport_finite_range_index_bound + S gmp_index_predecessor_transport_finite_range = l) -> exists gmp_magnitude_predecessor_transport_finite_range. ((((exists ff_h_gmp_predecessor_transport_finite_range_decoded. ff_h_gmp_predecessor_transport_finite_range_decoded + S (gmp_magnitude_predecessor_transport_finite_range) = S ((S (gmp_index_predecessor_transport_finite_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_decoded. mb = ff_q_gmp_predecessor_transport_finite_range_decoded * S ((S (gmp_index_predecessor_transport_finite_range)) * mc) + (gmp_magnitude_predecessor_transport_finite_range))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_range_positive. gsp_lt_gap_predecessor_transport_finite_range_positive + S 0 = gmp_magnitude_predecessor_transport_finite_range) /\ (exists gsp_le_gap_predecessor_transport_finite_range_bounded. gsp_le_gap_predecessor_transport_finite_range_bounded + gmp_magnitude_predecessor_transport_finite_range = l)))) -> (forall gmp_index_predecessor_transport_recode gmp_predecessor_predecessor_transport_recode. (exists gsp_lt_gap_predecessor_transport_recode_index_bound. gsp_lt_gap_predecessor_transport_recode_index_bound + S gmp_index_predecessor_transport_recode = l) -> (((exists gsp_beta_height_gmp_predecessor_transport_recode_source. gsp_beta_height_gmp_predecessor_transport_recode_source + S (S gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_transport_recode_source. mb = gsp_beta_quotient_gmp_predecessor_transport_recode_source * S ((S (gmp_index_predecessor_transport_recode)) * mc) + (S gmp_predecessor_predecessor_transport_recode))) -> (((exists ff_h_gmp_predecessor_transport_recode_target. ff_h_gmp_predecessor_transport_recode_target + S (gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * rc)) /\ exists ff_q_gmp_predecessor_transport_recode_target. rb = ff_q_gmp_predecessor_transport_recode_target * S ((S (gmp_index_predecessor_transport_recode)) * rc) + (gmp_predecessor_predecessor_transport_recode)))) -> (forall fp_i_predecessor_transport_bounded_result. (exists fp_gap_predecessor_transport_bounded_result_index. fp_gap_predecessor_transport_bounded_result_index + S fp_i_predecessor_transport_bounded_result = l) -> exists fp_value_predecessor_transport_bounded_result. ((((exists ff_h_predecessor_transport_bounded_result_entry. ff_h_predecessor_transport_bounded_result_entry + S (fp_value_predecessor_transport_bounded_result) = S ((S (fp_i_predecessor_transport_bounded_result)) * rc)) /\ exists ff_q_predecessor_transport_bounded_result_entry. rb = ff_q_predecessor_transport_bounded_result_entry * S ((S (fp_i_predecessor_transport_bounded_result)) * rc) + (fp_value_predecessor_transport_bounded_result))) /\ (exists fp_gap_predecessor_transport_bounded_result_value. fp_gap_predecessor_transport_bounded_result_value + S fp_value_predecessor_transport_bounded_result = l)))

Structural proof guide

Generated structural guide

Removing one successor turns the positive 1,...,l range bound into the finite 0,...,l-1 bound.

Use the direct prerequisites ne_zero_of_one_le, nonzero_is_succ as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (3), equality transport (3).

Referenced ingredients

PA003U ne_zero_of_one_le PA001V nonzero_is_succ

Proof neighborhood

Direct dependencies

PA003U ne_zero_of_one_le PA001V nonzero_is_succ

Direct dependents

PA007V gauss_predecessor_half_range_aligned PA007Y gauss_magnitude_product_eq_half_range PA00B3 beta_magnitude_predecessor_recode_surjective PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BD pair_order_terminal_successor_product_eq_range_two PA00CY beta_magnitude_sum_permutation_exact

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro l
  6. 0006intro hrange
  7. 0007intro hrecode
  8. 0008intro i
  9. 0009intro hi
  10. 0010have hentry : exists m. (((exists ff_h_gmp_predecessor_transport_finite_range_entry. ff_h_gmp_predecessor_transport_finite_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_entry. mb = ff_q_gmp_predecessor_transport_finite_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_positive. gsp_lt_gap_predecessor_transport_finite_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_transport_finite_bounded. gsp_le_gap_predecessor_transport_finite_bounded + m = l))
  11. 0011specialize hrange i
  12. 0012apply hrange
  13. 0013exact hi
  14. 0014cases hentry
  15. 0015cases hentry_witness
  16. 0016cases hentry_witness_right
  17. 0017have hx0 : ~(x = 0)
  18. 0018intro hxzero
  19. 0019specialize ne_zero_of_one_le x
  20. 0020apply ne_zero_of_one_le
  21. 0021exact hentry_witness_right_left
  22. 0022exact hxzero
  23. 0023have hxpredecessor : exists q. x = S q
  24. 0024specialize nonzero_is_succ x
  25. 0025apply nonzero_is_succ
  26. 0026exact hx0
  27. 0027cases hxpredecessor
  28. 0028exists x1
  29. 0029split
  30. 0030specialize hrecode i
  31. 0031specialize hrecode x1
  32. 0032apply hrecode
  33. 0033exact hi
  34. 0034rewrite <- hxpredecessor_witness
  35. 0035rewrite <- hxpredecessor_witness
  36. 0036exact hentry_witness_left
  37. 0037rewrite hxpredecessor_witness at hentry_witness_right_right
  38. 0038exact hentry_witness_right_right