PA009E

scaled_inverse_prefix_involutive

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

Decoding a scaled-inverse mate and decoding its predecessor returns the source residue.

Exact expanded PA statement

forall p a n b c i y. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esipe_involutive_prime esi_prime_right_esipe_involutive_prime. p = esi_prime_left_esipe_involutive_prime * esi_prime_right_esipe_involutive_prime -> esi_prime_left_esipe_involutive_prime = 1 \/ esi_prime_right_esipe_involutive_prime = 1)) -> (forall esip_index_involutive_prefix. (exists esip_gap_involutive_prefix_prefix_bound. esip_gap_involutive_prefix_prefix_bound + S (esip_index_involutive_prefix) = n) -> exists esip_mate_involutive_prefix. ((((exists ff_h_esip_involutive_prefix_entry. ff_h_esip_involutive_prefix_entry + S (esip_mate_involutive_prefix) = S ((S (esip_index_involutive_prefix)) * c)) /\ exists ff_q_esip_involutive_prefix_entry. b = ff_q_esip_involutive_prefix_entry * S ((S (esip_index_involutive_prefix)) * c) + (esip_mate_involutive_prefix))) /\ ((exists esip_gap_involutive_prefix_relation_index_bound. esip_gap_involutive_prefix_relation_index_bound + S (esip_index_involutive_prefix) = n) /\ ((((~((S esip_index_involutive_prefix) = 0) /\ (exists esip_gap_involutive_prefix_relation_scaled_left_bound. esip_gap_involutive_prefix_relation_scaled_left_bound + S (S esip_index_involutive_prefix) = p))) /\ (((~(esip_mate_involutive_prefix = 0) /\ (exists esip_gap_involutive_prefix_relation_scaled_right_bound. esip_gap_involutive_prefix_relation_scaled_right_bound + S (esip_mate_involutive_prefix) = p))) /\ (exists esi_mod_left_involutive_prefix_relation_scaled_mod esi_mod_right_involutive_prefix_relation_scaled_mod. ((S esip_index_involutive_prefix) * esip_mate_involutive_prefix) + p * esi_mod_left_involutive_prefix_relation_scaled_mod = (a) + p * esi_mod_right_involutive_prefix_relation_scaled_mod))))))) -> (exists esip_gap_involutive_bound. esip_gap_involutive_bound + S (i) = n) -> (((exists ff_h_esipe_involutive_at. ff_h_esipe_involutive_at + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_involutive_at. b = ff_q_esipe_involutive_at * S ((S (i)) * c) + (y))) -> exists j. y = S j /\ ((exists esip_gap_involutive_mate_bound. esip_gap_involutive_mate_bound + S (j) = n) /\ (((exists ff_h_esipe_involutive_back. ff_h_esipe_involutive_back + S (S i) = S ((S (j)) * c)) /\ exists ff_q_esipe_involutive_back. b = ff_q_esipe_involutive_back * S ((S (j)) * c) + (S i))))

Structural proof guide

Generated structural guide

Decoding a scaled-inverse mate and decoding its predecessor returns the source residue.

Use the direct prerequisites scaled_inverse_prefix_mate_predecessor, scaled_inverse_prefix_entry_sound, scaled_inverse_symmetric, scaled_inverse_prefix_extensional as previously established PA formulas.

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

Referenced ingredients

PA009A scaled_inverse_prefix_mate_predecessor PA0099 scaled_inverse_prefix_entry_sound PA009B scaled_inverse_symmetric PA009D scaled_inverse_prefix_extensional

Proof neighborhood

Direct dependencies

PA009A scaled_inverse_prefix_mate_predecessor PA0099 scaled_inverse_prefix_entry_sound PA009B scaled_inverse_symmetric PA009D scaled_inverse_prefix_extensional

Direct dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit

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 a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro i
  7. 0007intro y
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hprefix
  11. 0011intro hi
  12. 0012intro hat
  13. 0013have hpredecessor : exists j. y = S j /\ (exists esip_gap_involutive_mate_bound. esip_gap_involutive_mate_bound + S (j) = n)
  14. 0014specialize scaled_inverse_prefix_mate_predecessor p
  15. 0015specialize scaled_inverse_prefix_mate_predecessor a
  16. 0016specialize scaled_inverse_prefix_mate_predecessor n
  17. 0017specialize scaled_inverse_prefix_mate_predecessor b
  18. 0018specialize scaled_inverse_prefix_mate_predecessor c
  19. 0019specialize scaled_inverse_prefix_mate_predecessor i
  20. 0020specialize scaled_inverse_prefix_mate_predecessor y
  21. 0021apply scaled_inverse_prefix_mate_predecessor
  22. 0022exact hpn
  23. 0023exact hprefix
  24. 0024exact hi
  25. 0025exact hat
  26. 0026cases hpredecessor
  27. 0027cases hpredecessor_witness
  28. 0028have hforward_relation : (exists esip_gap_involutive_forward_relation_index_bound. esip_gap_involutive_forward_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_involutive_forward_relation_scaled_left_bound. esip_gap_involutive_forward_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_involutive_forward_relation_scaled_right_bound. esip_gap_involutive_forward_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_involutive_forward_relation_scaled_mod esi_mod_right_involutive_forward_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_involutive_forward_relation_scaled_mod = (a) + p * esi_mod_right_involutive_forward_relation_scaled_mod))))
  29. 0029specialize scaled_inverse_prefix_entry_sound p
  30. 0030specialize scaled_inverse_prefix_entry_sound a
  31. 0031specialize scaled_inverse_prefix_entry_sound n
  32. 0032specialize scaled_inverse_prefix_entry_sound b
  33. 0033specialize scaled_inverse_prefix_entry_sound c
  34. 0034specialize scaled_inverse_prefix_entry_sound n
  35. 0035specialize scaled_inverse_prefix_entry_sound i
  36. 0036specialize scaled_inverse_prefix_entry_sound y
  37. 0037apply scaled_inverse_prefix_entry_sound
  38. 0038exact hprefix
  39. 0039exact hi
  40. 0040exact hat
  41. 0041cases hforward_relation
  42. 0042have hforward : (((~((S i) = 0) /\ (exists esip_gap_involutive_forward_scaled_left_bound. esip_gap_involutive_forward_scaled_left_bound + S (S i) = p))) /\ (((~(S x = 0) /\ (exists esip_gap_involutive_forward_scaled_right_bound. esip_gap_involutive_forward_scaled_right_bound + S (S x) = p))) /\ (exists esi_mod_left_involutive_forward_scaled_mod esi_mod_right_involutive_forward_scaled_mod. ((S i) * S x) + p * esi_mod_left_involutive_forward_scaled_mod = (a) + p * esi_mod_right_involutive_forward_scaled_mod)))
  43. 0043rewrite hpredecessor_witness_left at hforward_relation_right
  44. 0044rewrite hpredecessor_witness_left at hforward_relation_right
  45. 0045rewrite hpredecessor_witness_left at hforward_relation_right
  46. 0046exact hforward_relation_right
  47. 0047have hreverse : (((~((S x) = 0) /\ (exists esip_gap_involutive_reverse_scaled_left_bound. esip_gap_involutive_reverse_scaled_left_bound + S (S x) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_involutive_reverse_scaled_right_bound. esip_gap_involutive_reverse_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_involutive_reverse_scaled_mod esi_mod_right_involutive_reverse_scaled_mod. ((S x) * S i) + p * esi_mod_left_involutive_reverse_scaled_mod = (a) + p * esi_mod_right_involutive_reverse_scaled_mod)))
  48. 0048specialize scaled_inverse_symmetric p
  49. 0049specialize scaled_inverse_symmetric a
  50. 0050specialize scaled_inverse_symmetric (S i)
  51. 0051specialize scaled_inverse_symmetric (S x)
  52. 0052apply scaled_inverse_symmetric
  53. 0053exact hforward
  54. 0054have hreverse_relation : (exists esip_gap_involutive_reverse_relation_index_bound. esip_gap_involutive_reverse_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_involutive_reverse_relation_scaled_left_bound. esip_gap_involutive_reverse_relation_scaled_left_bound + S (S x) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_involutive_reverse_relation_scaled_right_bound. esip_gap_involutive_reverse_relation_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_involutive_reverse_relation_scaled_mod esi_mod_right_involutive_reverse_relation_scaled_mod. ((S x) * S i) + p * esi_mod_left_involutive_reverse_relation_scaled_mod = (a) + p * esi_mod_right_involutive_reverse_relation_scaled_mod))))
  55. 0055split
  56. 0056exact hpredecessor_witness_right
  57. 0057exact hreverse
  58. 0058have hback : ((exists ff_h_esipe_involutive_back. ff_h_esipe_involutive_back + S (S i) = S ((S (x)) * c)) /\ exists ff_q_esipe_involutive_back. b = ff_q_esipe_involutive_back * S ((S (x)) * c) + (S i))
  59. 0059specialize scaled_inverse_prefix_extensional p
  60. 0060specialize scaled_inverse_prefix_extensional a
  61. 0061specialize scaled_inverse_prefix_extensional n
  62. 0062specialize scaled_inverse_prefix_extensional b
  63. 0063specialize scaled_inverse_prefix_extensional c
  64. 0064specialize scaled_inverse_prefix_extensional n
  65. 0065specialize scaled_inverse_prefix_extensional x
  66. 0066specialize scaled_inverse_prefix_extensional (S i)
  67. 0067apply scaled_inverse_prefix_extensional
  68. 0068exact hp
  69. 0069exact hprefix
  70. 0070exact hpredecessor_witness_right
  71. 0071exact hreverse_relation
  72. 0072exists x
  73. 0073split
  74. 0074exact hpredecessor_witness_left
  75. 0075split
  76. 0076exact hpredecessor_witness_right
  77. 0077exact hback