PA009A

scaled_inverse_prefix_mate_predecessor

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

Every positive decoded mate has a predecessor inside the source bound.

Exact expanded PA statement

forall p a n b c i y. p = S n -> (forall esip_index_predecessor_prefix. (exists esip_gap_predecessor_prefix_prefix_bound. esip_gap_predecessor_prefix_prefix_bound + S (esip_index_predecessor_prefix) = n) -> exists esip_mate_predecessor_prefix. ((((exists ff_h_esip_predecessor_prefix_entry. ff_h_esip_predecessor_prefix_entry + S (esip_mate_predecessor_prefix) = S ((S (esip_index_predecessor_prefix)) * c)) /\ exists ff_q_esip_predecessor_prefix_entry. b = ff_q_esip_predecessor_prefix_entry * S ((S (esip_index_predecessor_prefix)) * c) + (esip_mate_predecessor_prefix))) /\ ((exists esip_gap_predecessor_prefix_relation_index_bound. esip_gap_predecessor_prefix_relation_index_bound + S (esip_index_predecessor_prefix) = n) /\ ((((~((S esip_index_predecessor_prefix) = 0) /\ (exists esip_gap_predecessor_prefix_relation_scaled_left_bound. esip_gap_predecessor_prefix_relation_scaled_left_bound + S (S esip_index_predecessor_prefix) = p))) /\ (((~(esip_mate_predecessor_prefix = 0) /\ (exists esip_gap_predecessor_prefix_relation_scaled_right_bound. esip_gap_predecessor_prefix_relation_scaled_right_bound + S (esip_mate_predecessor_prefix) = p))) /\ (exists esi_mod_left_predecessor_prefix_relation_scaled_mod esi_mod_right_predecessor_prefix_relation_scaled_mod. ((S esip_index_predecessor_prefix) * esip_mate_predecessor_prefix) + p * esi_mod_left_predecessor_prefix_relation_scaled_mod = (a) + p * esi_mod_right_predecessor_prefix_relation_scaled_mod))))))) -> (exists esip_gap_predecessor_source_bound. esip_gap_predecessor_source_bound + S (i) = n) -> (((exists ff_h_esipe_predecessor_at. ff_h_esipe_predecessor_at + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_predecessor_at. b = ff_q_esipe_predecessor_at * S ((S (i)) * c) + (y))) -> exists j. y = S j /\ (exists esip_gap_predecessor_result_bound. esip_gap_predecessor_result_bound + S (j) = n)

Structural proof guide

Generated structural guide

Every positive decoded mate has a predecessor inside the source bound.

Use the direct prerequisites scaled_inverse_prefix_entry_sound, nonzero_is_succ, le_of_succ_le_succ as previously established PA formulas.

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

Referenced ingredients

PA0099 scaled_inverse_prefix_entry_sound PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Proof neighborhood

Direct dependencies

PA0099 scaled_inverse_prefix_entry_sound PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Direct dependents

PA009E scaled_inverse_prefix_involutive

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 hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012have hrelation : (exists esip_gap_predecessor_relation_index_bound. esip_gap_predecessor_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_predecessor_relation_scaled_left_bound. esip_gap_predecessor_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_predecessor_relation_scaled_right_bound. esip_gap_predecessor_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_predecessor_relation_scaled_mod esi_mod_right_predecessor_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_predecessor_relation_scaled_mod = (a) + p * esi_mod_right_predecessor_relation_scaled_mod))))
  13. 0013specialize scaled_inverse_prefix_entry_sound p
  14. 0014specialize scaled_inverse_prefix_entry_sound a
  15. 0015specialize scaled_inverse_prefix_entry_sound n
  16. 0016specialize scaled_inverse_prefix_entry_sound b
  17. 0017specialize scaled_inverse_prefix_entry_sound c
  18. 0018specialize scaled_inverse_prefix_entry_sound n
  19. 0019specialize scaled_inverse_prefix_entry_sound i
  20. 0020specialize scaled_inverse_prefix_entry_sound y
  21. 0021apply scaled_inverse_prefix_entry_sound
  22. 0022exact hprefix
  23. 0023exact hi
  24. 0024exact hat
  25. 0025cases hrelation
  26. 0026cases hrelation_right
  27. 0027cases hrelation_right_right
  28. 0028cases hrelation_right_right_left
  29. 0029have hshape : exists j. y = S j
  30. 0030specialize nonzero_is_succ y
  31. 0031apply nonzero_is_succ
  32. 0032exact hrelation_right_right_left_left
  33. 0033cases hshape
  34. 0034have hjn : exists h. h + S x = n
  35. 0035rewrite hshape_witness at hrelation_right_right_left_right
  36. 0036rewrite hpn at hrelation_right_right_left_right
  37. 0037specialize le_of_succ_le_succ (S x)
  38. 0038specialize le_of_succ_le_succ n
  39. 0039apply le_of_succ_le_succ
  40. 0040exact hrelation_right_right_left_right
  41. 0041exists x
  42. 0042split
  43. 0043exact hshape_witness
  44. 0044exact hjn