PA00AP

inverse_prefix_last_fixed

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

The last index, representing the predecessor of p, is fixed by the full inverse prefix.

Exact expanded PA statement

forall p n k b c. p = S n -> n = S k -> (forall wip_index_last_prefix. (exists wip_gap_last_prefix_prefix_bound. wip_gap_last_prefix_prefix_bound + S wip_index_last_prefix = n) -> exists wip_mate_last_prefix. ((((exists wip_beta_height_last_prefix_decoded. wip_beta_height_last_prefix_decoded + S (wip_mate_last_prefix) = S ((S (wip_index_last_prefix)) * c)) /\ exists wip_beta_quotient_last_prefix_decoded. b = wip_beta_quotient_last_prefix_decoded * S ((S (wip_index_last_prefix)) * c) + (wip_mate_last_prefix))) /\ ((exists wip_gap_last_prefix_inverse_index_bound. wip_gap_last_prefix_inverse_index_bound + S wip_index_last_prefix = n) /\ ((exists wip_gap_last_prefix_inverse_mate_bound. wip_gap_last_prefix_inverse_mate_bound + S wip_mate_last_prefix = n) /\ (exists wip_mod_left_last_prefix_inverse_mod wip_mod_right_last_prefix_inverse_mod. ((S wip_index_last_prefix) * S wip_mate_last_prefix) + p * wip_mod_left_last_prefix_inverse_mod = 1 + p * wip_mod_right_last_prefix_inverse_mod))))) -> (((exists wip_beta_height_last_result. wip_beta_height_last_result + S (k) = S ((S (k)) * c)) /\ exists wip_beta_quotient_last_result. b = wip_beta_quotient_last_result * S ((S (k)) * c) + (k)))

Structural proof guide

Generated structural guide

The last index, representing the predecessor of p, is fixed by the full inverse prefix.

Use the direct prerequisites zero_add, predecessor_square_mod_one, inverse_prefix_extensional as previously established PA formulas.

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

Referenced ingredients

PA0001 zero_add PA005D predecessor_square_mod_one PA00AM inverse_prefix_extensional

Proof neighborhood

Direct dependencies

PA0001 zero_add PA005D predecessor_square_mod_one PA00AM inverse_prefix_extensional

Direct dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate

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 k
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpn
  7. 0007intro hnk
  8. 0008intro hprefix
  9. 0009have hlast_bound : exists wip_gap_last_bound. wip_gap_last_bound + S k = n
  10. 0010rewrite hnk
  11. 0011exists 0
  12. 0012specialize zero_add (S k)
  13. 0013exact zero_add
  14. 0014have hpredecessor_mod : exists wie_mod_left_predecessor wie_mod_right_predecessor. (n * n) + p * wie_mod_left_predecessor = (1) + p * wie_mod_right_predecessor
  15. 0015specialize predecessor_square_mod_one p
  16. 0016specialize predecessor_square_mod_one n
  17. 0017apply predecessor_square_mod_one
  18. 0018exact hpn
  19. 0019have hlast_mod : exists wie_mod_left_last wie_mod_right_last. ((S k) * S k) + p * wie_mod_left_last = (1) + p * wie_mod_right_last
  20. 0020rewrite <- hnk
  21. 0021rewrite <- hnk
  22. 0022exact hpredecessor_mod
  23. 0023have hlast_relation : (exists wip_gap_last_relation_index_bound. wip_gap_last_relation_index_bound + S k = n) /\ ((exists wip_gap_last_relation_mate_bound. wip_gap_last_relation_mate_bound + S k = n) /\ (exists wip_mod_left_last_relation_mod wip_mod_right_last_relation_mod. ((S k) * S k) + p * wip_mod_left_last_relation_mod = 1 + p * wip_mod_right_last_relation_mod))
  24. 0024split
  25. 0025exact hlast_bound
  26. 0026split
  27. 0027exact hlast_bound
  28. 0028exact hlast_mod
  29. 0029specialize inverse_prefix_extensional p
  30. 0030specialize inverse_prefix_extensional n
  31. 0031specialize inverse_prefix_extensional b
  32. 0032specialize inverse_prefix_extensional c
  33. 0033specialize inverse_prefix_extensional n
  34. 0034specialize inverse_prefix_extensional k
  35. 0035specialize inverse_prefix_extensional k
  36. 0036apply inverse_prefix_extensional
  37. 0037exact hpn
  38. 0038exact hprefix
  39. 0039exact hlast_bound
  40. 0040exact hlast_relation