PA00A6

prime_inverse_prefix_exists_bounded

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

Every length bounded by p-1 has a beta-coded inverse prefix.

Exact expanded PA statement

forall p n l. p = S n -> ((~(p = 1) /\ forall wip_prime_left_bounded_prime wip_prime_right_bounded_prime. p = wip_prime_left_bounded_prime * wip_prime_right_bounded_prime -> wip_prime_left_bounded_prime = 1 \/ wip_prime_right_bounded_prime = 1)) -> (exists wip_weak_gap_bounded_length. wip_weak_gap_bounded_length + l = n) -> exists b c. (forall wip_index_bounded_result. (exists wip_gap_bounded_result_prefix_bound. wip_gap_bounded_result_prefix_bound + S wip_index_bounded_result = l) -> exists wip_mate_bounded_result. ((((exists wip_beta_height_bounded_result_decoded. wip_beta_height_bounded_result_decoded + S (wip_mate_bounded_result) = S ((S (wip_index_bounded_result)) * c)) /\ exists wip_beta_quotient_bounded_result_decoded. b = wip_beta_quotient_bounded_result_decoded * S ((S (wip_index_bounded_result)) * c) + (wip_mate_bounded_result))) /\ ((exists wip_gap_bounded_result_inverse_index_bound. wip_gap_bounded_result_inverse_index_bound + S wip_index_bounded_result = n) /\ ((exists wip_gap_bounded_result_inverse_mate_bound. wip_gap_bounded_result_inverse_mate_bound + S wip_mate_bounded_result = n) /\ (exists wip_mod_left_bounded_result_inverse_mod wip_mod_right_bounded_result_inverse_mod. ((S wip_index_bounded_result) * S wip_mate_bounded_result) + p * wip_mod_left_bounded_result_inverse_mod = 1 + p * wip_mod_right_bounded_result_inverse_mod)))))

Structural proof guide

Generated structural guide

Every length bounded by p-1 has a beta-coded inverse prefix.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, lt_to_le, prime_inverse_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (4).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA00A5 prime_inverse_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA00A5 prime_inverse_prefix_extend

Direct dependents

PA00A7 prime_inverse_prefix_exists

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 n
  3. 0003induction l
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hln
  7. 0007exists 0
  8. 0008exists 0
  9. 0009intro i
  10. 0010intro hi
  11. 0011exfalso
  12. 0012cases hi
  13. 0013have hsi : S i = 0
  14. 0014specialize add_eq_zero_right x
  15. 0015specialize add_eq_zero_right (S i)
  16. 0016apply add_eq_zero_right
  17. 0017exact hi_witness
  18. 0018specialize succ_ne_zero i
  19. 0019apply succ_ne_zero
  20. 0020exact hsi
  21. 0021intro hpn
  22. 0022intro hp
  23. 0023intro hln
  24. 0024have hprev_bound : exists h. h + l = n
  25. 0025specialize lt_to_le l
  26. 0026specialize lt_to_le n
  27. 0027apply lt_to_le
  28. 0028exact hln
  29. 0029have hprev : exists b c. (forall wip_index_bounded_previous. (exists wip_gap_bounded_previous_prefix_bound. wip_gap_bounded_previous_prefix_bound + S wip_index_bounded_previous = l) -> exists wip_mate_bounded_previous. ((((exists wip_beta_height_bounded_previous_decoded. wip_beta_height_bounded_previous_decoded + S (wip_mate_bounded_previous) = S ((S (wip_index_bounded_previous)) * c)) /\ exists wip_beta_quotient_bounded_previous_decoded. b = wip_beta_quotient_bounded_previous_decoded * S ((S (wip_index_bounded_previous)) * c) + (wip_mate_bounded_previous))) /\ ((exists wip_gap_bounded_previous_inverse_index_bound. wip_gap_bounded_previous_inverse_index_bound + S wip_index_bounded_previous = n) /\ ((exists wip_gap_bounded_previous_inverse_mate_bound. wip_gap_bounded_previous_inverse_mate_bound + S wip_mate_bounded_previous = n) /\ (exists wip_mod_left_bounded_previous_inverse_mod wip_mod_right_bounded_previous_inverse_mod. ((S wip_index_bounded_previous) * S wip_mate_bounded_previous) + p * wip_mod_left_bounded_previous_inverse_mod = 1 + p * wip_mod_right_bounded_previous_inverse_mod)))))
  30. 0030apply IH
  31. 0031exact hpn
  32. 0032exact hp
  33. 0033exact hprev_bound
  34. 0034cases hprev
  35. 0035cases hprev_witness
  36. 0036have hnext : exists z d. (forall wip_index_bounded_successor. (exists wip_gap_bounded_successor_prefix_bound. wip_gap_bounded_successor_prefix_bound + S wip_index_bounded_successor = S l) -> exists wip_mate_bounded_successor. ((((exists wip_beta_height_bounded_successor_decoded. wip_beta_height_bounded_successor_decoded + S (wip_mate_bounded_successor) = S ((S (wip_index_bounded_successor)) * d)) /\ exists wip_beta_quotient_bounded_successor_decoded. z = wip_beta_quotient_bounded_successor_decoded * S ((S (wip_index_bounded_successor)) * d) + (wip_mate_bounded_successor))) /\ ((exists wip_gap_bounded_successor_inverse_index_bound. wip_gap_bounded_successor_inverse_index_bound + S wip_index_bounded_successor = n) /\ ((exists wip_gap_bounded_successor_inverse_mate_bound. wip_gap_bounded_successor_inverse_mate_bound + S wip_mate_bounded_successor = n) /\ (exists wip_mod_left_bounded_successor_inverse_mod wip_mod_right_bounded_successor_inverse_mod. ((S wip_index_bounded_successor) * S wip_mate_bounded_successor) + p * wip_mod_left_bounded_successor_inverse_mod = 1 + p * wip_mod_right_bounded_successor_inverse_mod)))))
  37. 0037specialize prime_inverse_prefix_extend p
  38. 0038specialize prime_inverse_prefix_extend n
  39. 0039specialize prime_inverse_prefix_extend x
  40. 0040specialize prime_inverse_prefix_extend x1
  41. 0041specialize prime_inverse_prefix_extend l
  42. 0042apply prime_inverse_prefix_extend
  43. 0043exact hpn
  44. 0044exact hp
  45. 0045exact hln
  46. 0046exact hprev_witness_witness
  47. 0047cases hnext
  48. 0048cases hnext_witness
  49. 0049exists x2
  50. 0050exists x3
  51. 0051exact hnext_witness_witness