PA00AH

prime_inverse_prefix_fixed_cases

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

A fixed zero-based inverse index is zero or the last index.

Exact expanded PA statement

forall p n b c i. p = S n -> ((~(p = 1) /\ forall wip_prime_left_fixed_prime wip_prime_right_fixed_prime. p = wip_prime_left_fixed_prime * wip_prime_right_fixed_prime -> wip_prime_left_fixed_prime = 1 \/ wip_prime_right_fixed_prime = 1)) -> (forall wip_index_fixed_prefix. (exists wip_gap_fixed_prefix_prefix_bound. wip_gap_fixed_prefix_prefix_bound + S wip_index_fixed_prefix = n) -> exists wip_mate_fixed_prefix. ((((exists wip_beta_height_fixed_prefix_decoded. wip_beta_height_fixed_prefix_decoded + S (wip_mate_fixed_prefix) = S ((S (wip_index_fixed_prefix)) * c)) /\ exists wip_beta_quotient_fixed_prefix_decoded. b = wip_beta_quotient_fixed_prefix_decoded * S ((S (wip_index_fixed_prefix)) * c) + (wip_mate_fixed_prefix))) /\ ((exists wip_gap_fixed_prefix_inverse_index_bound. wip_gap_fixed_prefix_inverse_index_bound + S wip_index_fixed_prefix = n) /\ ((exists wip_gap_fixed_prefix_inverse_mate_bound. wip_gap_fixed_prefix_inverse_mate_bound + S wip_mate_fixed_prefix = n) /\ (exists wip_mod_left_fixed_prefix_inverse_mod wip_mod_right_fixed_prefix_inverse_mod. ((S wip_index_fixed_prefix) * S wip_mate_fixed_prefix) + p * wip_mod_left_fixed_prefix_inverse_mod = 1 + p * wip_mod_right_fixed_prefix_inverse_mod))))) -> (exists wip_gap_fixed_index_bound. wip_gap_fixed_index_bound + S i = n) -> (((exists wip_beta_height_fixed_entry. wip_beta_height_fixed_entry + S (i) = S ((S (i)) * c)) /\ exists wip_beta_quotient_fixed_entry. b = wip_beta_quotient_fixed_entry * S ((S (i)) * c) + (i))) -> i = 0 \/ S i = n

Structural proof guide

Generated structural guide

A fixed zero-based inverse index is zero or the last index.

Use the direct prerequisites inverse_prefix_entry_sound, succ_le_succ, prime_bounded_square_one_cases, succ_injective as previously established PA formulas.

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

Referenced ingredients

PA00AF inverse_prefix_entry_sound PA002K succ_le_succ PA00AG prime_bounded_square_one_cases PA003V succ_injective

Proof neighborhood

Direct dependencies

PA00AF inverse_prefix_entry_sound PA002K succ_le_succ PA00AG prime_bounded_square_one_cases PA003V succ_injective

Direct dependents

PA00AI prime_inverse_prefix_nonendpoint_not_fixed

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. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hprefix
  9. 0009intro hi
  10. 0010intro hfixed
  11. 0011have hidx : (exists wip_gap_fixed_inverse_index_bound. wip_gap_fixed_inverse_index_bound + S i = n) /\ ((exists wip_gap_fixed_inverse_mate_bound. wip_gap_fixed_inverse_mate_bound + S i = n) /\ (exists wip_mod_left_fixed_inverse_mod wip_mod_right_fixed_inverse_mod. ((S i) * S i) + p * wip_mod_left_fixed_inverse_mod = 1 + p * wip_mod_right_fixed_inverse_mod))
  12. 0012specialize inverse_prefix_entry_sound p
  13. 0013specialize inverse_prefix_entry_sound n
  14. 0014specialize inverse_prefix_entry_sound b
  15. 0015specialize inverse_prefix_entry_sound c
  16. 0016specialize inverse_prefix_entry_sound n
  17. 0017specialize inverse_prefix_entry_sound i
  18. 0018specialize inverse_prefix_entry_sound i
  19. 0019apply inverse_prefix_entry_sound
  20. 0020exact hprefix
  21. 0021exact hi
  22. 0022exact hfixed
  23. 0023cases hidx
  24. 0024cases hidx_right
  25. 0025have hpositive : exists wii_positive_gap_fixed_positive. wii_positive_gap_fixed_positive + 1 = S i
  26. 0026exists i
  27. 0027rewrite PA4
  28. 0028rewrite PA3
  29. 0029refl
  30. 0030have hbounded : exists wii_successor_gap_fixed_residue_bound. wii_successor_gap_fixed_residue_bound + S (S i) = p
  31. 0031rewrite hpn
  32. 0032specialize succ_le_succ (S i)
  33. 0033specialize succ_le_succ n
  34. 0034apply succ_le_succ
  35. 0035exact hidx_left
  36. 0036have hcases : S i = 1 \/ S i = n
  37. 0037specialize prime_bounded_square_one_cases p
  38. 0038specialize prime_bounded_square_one_cases n
  39. 0039specialize prime_bounded_square_one_cases (S i)
  40. 0040apply prime_bounded_square_one_cases
  41. 0041exact hpn
  42. 0042exact hp
  43. 0043exact hpositive
  44. 0044exact hbounded
  45. 0045exact hidx_right_right
  46. 0046cases hcases
  47. 0047left
  48. 0048specialize succ_injective i
  49. 0049specialize succ_injective 0
  50. 0050apply succ_injective
  51. 0051exact hcases_left
  52. 0052right
  53. 0053exact hcases_right