PA00B3

beta_magnitude_predecessor_recode_surjective

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

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

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 fp_i_predecessor_transport_magnitude_injective fp_j_predecessor_transport_magnitude_injective fp_value_predecessor_transport_magnitude_injective. (exists fp_gap_predecessor_transport_magnitude_injective_i. fp_gap_predecessor_transport_magnitude_injective_i + S fp_i_predecessor_transport_magnitude_injective = l) -> (exists fp_gap_predecessor_transport_magnitude_injective_j. fp_gap_predecessor_transport_magnitude_injective_j + S fp_j_predecessor_transport_magnitude_injective = l) -> (((exists ff_h_predecessor_transport_magnitude_injective_left. ff_h_predecessor_transport_magnitude_injective_left + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_left. mb = ff_q_predecessor_transport_magnitude_injective_left * S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> (((exists ff_h_predecessor_transport_magnitude_injective_right. ff_h_predecessor_transport_magnitude_injective_right + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_right. mb = ff_q_predecessor_transport_magnitude_injective_right * S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> fp_i_predecessor_transport_magnitude_injective = fp_j_predecessor_transport_magnitude_injective) -> (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_value_predecessor_transport_target_surjective. (exists fp_gap_predecessor_transport_target_surjective_value. fp_gap_predecessor_transport_target_surjective_value + S fp_value_predecessor_transport_target_surjective = l) -> exists fp_i_predecessor_transport_target_surjective. ((exists fp_gap_predecessor_transport_target_surjective_index. fp_gap_predecessor_transport_target_surjective_index + S fp_i_predecessor_transport_target_surjective = l) /\ (((exists ff_h_predecessor_transport_target_surjective_entry. ff_h_predecessor_transport_target_surjective_entry + S (fp_value_predecessor_transport_target_surjective) = S ((S (fp_i_predecessor_transport_target_surjective)) * rc)) /\ exists ff_q_predecessor_transport_target_surjective_entry. rb = ff_q_predecessor_transport_target_surjective_entry * S ((S (fp_i_predecessor_transport_target_surjective)) * rc) + (fp_value_predecessor_transport_target_surjective)))))

Structural proof guide

Generated structural guide

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

Use the direct prerequisites beta_magnitude_predecessor_recode_bounded, beta_magnitude_predecessor_recode_injective, finite_bounded_injective_surjective as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA004W finite_bounded_injective_surjective

Proof neighborhood

Direct dependencies

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA004W finite_bounded_injective_surjective

Direct dependents

PA00B4 finite_bounded_nonendpoint_injective_coverage

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 hsource_injective
  8. 0008intro hrecode
  9. 0009have hbounded : 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))
  10. 0010specialize beta_magnitude_predecessor_recode_bounded mb
  11. 0011specialize beta_magnitude_predecessor_recode_bounded mc
  12. 0012specialize beta_magnitude_predecessor_recode_bounded rb
  13. 0013specialize beta_magnitude_predecessor_recode_bounded rc
  14. 0014specialize beta_magnitude_predecessor_recode_bounded l
  15. 0015apply beta_magnitude_predecessor_recode_bounded
  16. 0016exact hrange
  17. 0017exact hrecode
  18. 0018have hinjective : forall fp_i_predecessor_transport_target_injective fp_j_predecessor_transport_target_injective fp_value_predecessor_transport_target_injective. (exists fp_gap_predecessor_transport_target_injective_i. fp_gap_predecessor_transport_target_injective_i + S fp_i_predecessor_transport_target_injective = l) -> (exists fp_gap_predecessor_transport_target_injective_j. fp_gap_predecessor_transport_target_injective_j + S fp_j_predecessor_transport_target_injective = l) -> (((exists ff_h_predecessor_transport_target_injective_left. ff_h_predecessor_transport_target_injective_left + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_i_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_left. rb = ff_q_predecessor_transport_target_injective_left * S ((S (fp_i_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> (((exists ff_h_predecessor_transport_target_injective_right. ff_h_predecessor_transport_target_injective_right + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_j_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_right. rb = ff_q_predecessor_transport_target_injective_right * S ((S (fp_j_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> fp_i_predecessor_transport_target_injective = fp_j_predecessor_transport_target_injective
  19. 0019specialize beta_magnitude_predecessor_recode_injective mb
  20. 0020specialize beta_magnitude_predecessor_recode_injective mc
  21. 0021specialize beta_magnitude_predecessor_recode_injective rb
  22. 0022specialize beta_magnitude_predecessor_recode_injective rc
  23. 0023specialize beta_magnitude_predecessor_recode_injective l
  24. 0024apply beta_magnitude_predecessor_recode_injective
  25. 0025exact hrange
  26. 0026exact hsource_injective
  27. 0027exact hrecode
  28. 0028specialize finite_bounded_injective_surjective l
  29. 0029specialize finite_bounded_injective_surjective rb
  30. 0030specialize finite_bounded_injective_surjective rc
  31. 0031apply finite_bounded_injective_surjective
  32. 0032exact hbounded
  33. 0033exact hinjective