PA0078

gauss_signed_half_magnitude_range

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

Every decoded signed-prefix magnitude lies constructively in 1,...,h.

Exact expanded PA statement

forall p h a b c mb mc sb sc l. (forall gsp_index_magnitude_range_source. (exists gsp_lt_gap_magnitude_range_source_index_bound. gsp_lt_gap_magnitude_range_source_index_bound + S gsp_index_magnitude_range_source = l) -> (exists gsp_value_magnitude_range_source_entry gsp_magnitude_magnitude_range_source_entry gsp_sign_magnitude_range_source_entry. (((exists ff_h_gsp_magnitude_range_source_entry_source. ff_h_gsp_magnitude_range_source_entry_source + S (gsp_value_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * c)) /\ exists ff_q_gsp_magnitude_range_source_entry_source. b = ff_q_gsp_magnitude_range_source_entry_source * S ((S (gsp_index_magnitude_range_source)) * c) + (gsp_value_magnitude_range_source_entry))) /\ ((((exists ff_h_gsp_magnitude_range_source_entry_magnitude. ff_h_gsp_magnitude_range_source_entry_magnitude + S (gsp_magnitude_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * mc)) /\ exists ff_q_gsp_magnitude_range_source_entry_magnitude. mb = ff_q_gsp_magnitude_range_source_entry_magnitude * S ((S (gsp_index_magnitude_range_source)) * mc) + (gsp_magnitude_magnitude_range_source_entry))) /\ ((((exists ff_h_gsp_magnitude_range_source_entry_sign. ff_h_gsp_magnitude_range_source_entry_sign + S (gsp_sign_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * sc)) /\ exists ff_q_gsp_magnitude_range_source_entry_sign. sb = ff_q_gsp_magnitude_range_source_entry_sign * S ((S (gsp_index_magnitude_range_source)) * sc) + (gsp_sign_magnitude_range_source_entry))) /\ ((exists gsp_lt_gap_magnitude_range_source_entry_positive. gsp_lt_gap_magnitude_range_source_entry_positive + S 0 = gsp_magnitude_magnitude_range_source_entry) /\ ((exists gsp_le_gap_magnitude_range_source_entry_bounded. gsp_le_gap_magnitude_range_source_entry_bounded + gsp_magnitude_magnitude_range_source_entry = h) /\ ((gsp_sign_magnitude_range_source_entry = 0 \/ gsp_sign_magnitude_range_source_entry = 1) /\ (((gsp_sign_magnitude_range_source_entry = 0 /\ (exists gsp_mod_left_magnitude_range_source_entry_lower gsp_mod_right_magnitude_range_source_entry_lower. (a * gsp_value_magnitude_range_source_entry) + p * gsp_mod_left_magnitude_range_source_entry_lower = (gsp_magnitude_magnitude_range_source_entry) + p * gsp_mod_right_magnitude_range_source_entry_lower)) \/ (gsp_sign_magnitude_range_source_entry = 1 /\ (exists gsp_mod_left_magnitude_range_source_entry_reflected gsp_mod_right_magnitude_range_source_entry_reflected. (a * gsp_value_magnitude_range_source_entry) + p * gsp_mod_left_magnitude_range_source_entry_reflected = ((2 * h) * gsp_magnitude_magnitude_range_source_entry) + p * gsp_mod_right_magnitude_range_source_entry_reflected))))))))))) -> (forall gmp_index_magnitude_range_result. (exists gsp_lt_gap_magnitude_range_result_index_bound. gsp_lt_gap_magnitude_range_result_index_bound + S gmp_index_magnitude_range_result = l) -> exists gmp_magnitude_magnitude_range_result. ((((exists ff_h_gmp_magnitude_range_result_decoded. ff_h_gmp_magnitude_range_result_decoded + S (gmp_magnitude_magnitude_range_result) = S ((S (gmp_index_magnitude_range_result)) * mc)) /\ exists ff_q_gmp_magnitude_range_result_decoded. mb = ff_q_gmp_magnitude_range_result_decoded * S ((S (gmp_index_magnitude_range_result)) * mc) + (gmp_magnitude_magnitude_range_result))) /\ ((exists gsp_lt_gap_magnitude_range_result_positive. gsp_lt_gap_magnitude_range_result_positive + S 0 = gmp_magnitude_magnitude_range_result) /\ (exists gsp_le_gap_magnitude_range_result_bounded. gsp_le_gap_magnitude_range_result_bounded + gmp_magnitude_magnitude_range_result = h))))

Structural proof guide

Generated structural guide

Every decoded signed-prefix magnitude lies constructively in 1,...,h.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (8), intermediate claims (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA007E gauss_signed_half_predecessor_recode_exists PA0085 gauss_lemma_power_congruence_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

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 p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro l
  11. 0011intro hprefix
  12. 0012intro i
  13. 0013intro hi
  14. 0014have hentry : exists gsp_value_magnitude_range_entry gsp_magnitude_magnitude_range_entry gsp_sign_magnitude_range_entry. (((exists ff_h_gsp_magnitude_range_entry_source. ff_h_gsp_magnitude_range_entry_source + S (gsp_value_magnitude_range_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_magnitude_range_entry_source. b = ff_q_gsp_magnitude_range_entry_source * S ((S (i)) * c) + (gsp_value_magnitude_range_entry))) /\ ((((exists ff_h_gsp_magnitude_range_entry_magnitude. ff_h_gsp_magnitude_range_entry_magnitude + S (gsp_magnitude_magnitude_range_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_magnitude_range_entry_magnitude. mb = ff_q_gsp_magnitude_range_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_magnitude_range_entry))) /\ ((((exists ff_h_gsp_magnitude_range_entry_sign. ff_h_gsp_magnitude_range_entry_sign + S (gsp_sign_magnitude_range_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_magnitude_range_entry_sign. sb = ff_q_gsp_magnitude_range_entry_sign * S ((S (i)) * sc) + (gsp_sign_magnitude_range_entry))) /\ ((exists gsp_lt_gap_magnitude_range_entry_positive. gsp_lt_gap_magnitude_range_entry_positive + S 0 = gsp_magnitude_magnitude_range_entry) /\ ((exists gsp_le_gap_magnitude_range_entry_bounded. gsp_le_gap_magnitude_range_entry_bounded + gsp_magnitude_magnitude_range_entry = h) /\ ((gsp_sign_magnitude_range_entry = 0 \/ gsp_sign_magnitude_range_entry = 1) /\ (((gsp_sign_magnitude_range_entry = 0 /\ (exists gsp_mod_left_magnitude_range_entry_lower gsp_mod_right_magnitude_range_entry_lower. (a * gsp_value_magnitude_range_entry) + p * gsp_mod_left_magnitude_range_entry_lower = (gsp_magnitude_magnitude_range_entry) + p * gsp_mod_right_magnitude_range_entry_lower)) \/ (gsp_sign_magnitude_range_entry = 1 /\ (exists gsp_mod_left_magnitude_range_entry_reflected gsp_mod_right_magnitude_range_entry_reflected. (a * gsp_value_magnitude_range_entry) + p * gsp_mod_left_magnitude_range_entry_reflected = ((2 * h) * gsp_magnitude_magnitude_range_entry) + p * gsp_mod_right_magnitude_range_entry_reflected)))))))))
  15. 0015specialize hprefix i
  16. 0016apply hprefix
  17. 0017exact hi
  18. 0018cases hentry
  19. 0019cases hentry_witness
  20. 0020cases hentry_witness_witness
  21. 0021cases hentry_witness_witness_witness
  22. 0022cases hentry_witness_witness_witness_right
  23. 0023cases hentry_witness_witness_witness_right_right
  24. 0024cases hentry_witness_witness_witness_right_right_right
  25. 0025cases hentry_witness_witness_witness_right_right_right_right
  26. 0026exists x1
  27. 0027split
  28. 0028exact hentry_witness_witness_witness_right_left
  29. 0029split
  30. 0030exact hentry_witness_witness_witness_right_right_right_left
  31. 0031exact hentry_witness_witness_witness_right_right_right_right_left