PA00AN

inverse_prefix_involutive

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

Decoding an inverse mate and decoding again returns the source index.

Exact expanded PA statement

forall p n b c i j. p = S n -> (forall wip_index_involutive_prefix. (exists wip_gap_involutive_prefix_prefix_bound. wip_gap_involutive_prefix_prefix_bound + S wip_index_involutive_prefix = n) -> exists wip_mate_involutive_prefix. ((((exists wip_beta_height_involutive_prefix_decoded. wip_beta_height_involutive_prefix_decoded + S (wip_mate_involutive_prefix) = S ((S (wip_index_involutive_prefix)) * c)) /\ exists wip_beta_quotient_involutive_prefix_decoded. b = wip_beta_quotient_involutive_prefix_decoded * S ((S (wip_index_involutive_prefix)) * c) + (wip_mate_involutive_prefix))) /\ ((exists wip_gap_involutive_prefix_inverse_index_bound. wip_gap_involutive_prefix_inverse_index_bound + S wip_index_involutive_prefix = n) /\ ((exists wip_gap_involutive_prefix_inverse_mate_bound. wip_gap_involutive_prefix_inverse_mate_bound + S wip_mate_involutive_prefix = n) /\ (exists wip_mod_left_involutive_prefix_inverse_mod wip_mod_right_involutive_prefix_inverse_mod. ((S wip_index_involutive_prefix) * S wip_mate_involutive_prefix) + p * wip_mod_left_involutive_prefix_inverse_mod = 1 + p * wip_mod_right_involutive_prefix_inverse_mod))))) -> (exists wip_gap_involutive_index_bound. wip_gap_involutive_index_bound + S i = n) -> (((exists wip_beta_height_involutive_source. wip_beta_height_involutive_source + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_involutive_source. b = wip_beta_quotient_involutive_source * S ((S (i)) * c) + (j))) -> ((exists wip_gap_involutive_mate_bound. wip_gap_involutive_mate_bound + S j = n) /\ (((exists wip_beta_height_involutive_back. wip_beta_height_involutive_back + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_involutive_back. b = wip_beta_quotient_involutive_back * S ((S (j)) * c) + (i))))

Structural proof guide

Generated structural guide

Decoding an inverse mate and decoding again returns the source index.

Use the direct prerequisites inverse_prefix_entry_sound, inverse_index_symmetric, inverse_prefix_extensional as previously established PA formulas.

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

Referenced ingredients

PA00AF inverse_prefix_entry_sound PA00AJ inverse_index_symmetric PA00AM inverse_prefix_extensional

Proof neighborhood

Direct dependencies

PA00AF inverse_prefix_entry_sound PA00AJ inverse_index_symmetric PA00AM inverse_prefix_extensional

Direct dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_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 n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpn
  8. 0008intro hprefix
  9. 0009intro hi
  10. 0010intro hat
  11. 0011have hforward : (exists wip_gap_involutive_forward_index_bound. wip_gap_involutive_forward_index_bound + S i = n) /\ ((exists wip_gap_involutive_forward_mate_bound. wip_gap_involutive_forward_mate_bound + S j = n) /\ (exists wip_mod_left_involutive_forward_mod wip_mod_right_involutive_forward_mod. ((S i) * S j) + p * wip_mod_left_involutive_forward_mod = 1 + p * wip_mod_right_involutive_forward_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 j
  19. 0019apply inverse_prefix_entry_sound
  20. 0020exact hprefix
  21. 0021exact hi
  22. 0022exact hat
  23. 0023have hreverse : (exists wip_gap_involutive_reverse_index_bound. wip_gap_involutive_reverse_index_bound + S j = n) /\ ((exists wip_gap_involutive_reverse_mate_bound. wip_gap_involutive_reverse_mate_bound + S i = n) /\ (exists wip_mod_left_involutive_reverse_mod wip_mod_right_involutive_reverse_mod. ((S j) * S i) + p * wip_mod_left_involutive_reverse_mod = 1 + p * wip_mod_right_involutive_reverse_mod))
  24. 0024specialize inverse_index_symmetric p
  25. 0025specialize inverse_index_symmetric n
  26. 0026specialize inverse_index_symmetric i
  27. 0027specialize inverse_index_symmetric j
  28. 0028apply inverse_index_symmetric
  29. 0029exact hforward
  30. 0030cases hforward
  31. 0031cases hforward_right
  32. 0032split
  33. 0033exact hforward_right_left
  34. 0034specialize inverse_prefix_extensional p
  35. 0035specialize inverse_prefix_extensional n
  36. 0036specialize inverse_prefix_extensional b
  37. 0037specialize inverse_prefix_extensional c
  38. 0038specialize inverse_prefix_extensional n
  39. 0039specialize inverse_prefix_extensional j
  40. 0040specialize inverse_prefix_extensional i
  41. 0041apply inverse_prefix_extensional
  42. 0042exact hpn
  43. 0043exact hprefix
  44. 0044exact hforward_right_left
  45. 0045exact hreverse