PA009D

scaled_inverse_prefix_extensional

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

A valid scaled inverse at a covered source is decoded by the prefix.

Exact expanded PA statement

forall p a n b c l i y. ((~(p = 1) /\ forall esi_prime_left_esipe_ext_prime esi_prime_right_esipe_ext_prime. p = esi_prime_left_esipe_ext_prime * esi_prime_right_esipe_ext_prime -> esi_prime_left_esipe_ext_prime = 1 \/ esi_prime_right_esipe_ext_prime = 1)) -> (forall esip_index_extensional_prefix. (exists esip_gap_extensional_prefix_prefix_bound. esip_gap_extensional_prefix_prefix_bound + S (esip_index_extensional_prefix) = l) -> exists esip_mate_extensional_prefix. ((((exists ff_h_esip_extensional_prefix_entry. ff_h_esip_extensional_prefix_entry + S (esip_mate_extensional_prefix) = S ((S (esip_index_extensional_prefix)) * c)) /\ exists ff_q_esip_extensional_prefix_entry. b = ff_q_esip_extensional_prefix_entry * S ((S (esip_index_extensional_prefix)) * c) + (esip_mate_extensional_prefix))) /\ ((exists esip_gap_extensional_prefix_relation_index_bound. esip_gap_extensional_prefix_relation_index_bound + S (esip_index_extensional_prefix) = n) /\ ((((~((S esip_index_extensional_prefix) = 0) /\ (exists esip_gap_extensional_prefix_relation_scaled_left_bound. esip_gap_extensional_prefix_relation_scaled_left_bound + S (S esip_index_extensional_prefix) = p))) /\ (((~(esip_mate_extensional_prefix = 0) /\ (exists esip_gap_extensional_prefix_relation_scaled_right_bound. esip_gap_extensional_prefix_relation_scaled_right_bound + S (esip_mate_extensional_prefix) = p))) /\ (exists esi_mod_left_extensional_prefix_relation_scaled_mod esi_mod_right_extensional_prefix_relation_scaled_mod. ((S esip_index_extensional_prefix) * esip_mate_extensional_prefix) + p * esi_mod_left_extensional_prefix_relation_scaled_mod = (a) + p * esi_mod_right_extensional_prefix_relation_scaled_mod))))))) -> (exists esip_gap_extensional_bound. esip_gap_extensional_bound + S (i) = l) -> ((exists esip_gap_extensional_relation_index_bound. esip_gap_extensional_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_extensional_relation_scaled_left_bound. esip_gap_extensional_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_extensional_relation_scaled_right_bound. esip_gap_extensional_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_extensional_relation_scaled_mod esi_mod_right_extensional_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_extensional_relation_scaled_mod = (a) + p * esi_mod_right_extensional_relation_scaled_mod))))) -> (((exists ff_h_esipe_extensional_result. ff_h_esipe_extensional_result + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_extensional_result. b = ff_q_esipe_extensional_result * S ((S (i)) * c) + (y)))

Structural proof guide

Generated structural guide

A valid scaled inverse at a covered source is decoded by the prefix.

Use the direct prerequisites prime_scaled_inverse_unique as previously established PA formulas.

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

Referenced ingredients

PA009C prime_scaled_inverse_unique

Proof neighborhood

Direct dependencies

PA009C prime_scaled_inverse_unique

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 l
  7. 0007intro i
  8. 0008intro y
  9. 0009intro hp
  10. 0010intro hprefix
  11. 0011intro hi
  12. 0012intro hrelation
  13. 0013have hstored : exists z. ((((exists ff_h_esipe_extensional_stored_at. ff_h_esipe_extensional_stored_at + S (z) = S ((S (i)) * c)) /\ exists ff_q_esipe_extensional_stored_at. b = ff_q_esipe_extensional_stored_at * S ((S (i)) * c) + (z))) /\ ((exists esip_gap_extensional_stored_relation_index_bound. esip_gap_extensional_stored_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_extensional_stored_relation_scaled_left_bound. esip_gap_extensional_stored_relation_scaled_left_bound + S (S i) = p))) /\ (((~(z = 0) /\ (exists esip_gap_extensional_stored_relation_scaled_right_bound. esip_gap_extensional_stored_relation_scaled_right_bound + S (z) = p))) /\ (exists esi_mod_left_extensional_stored_relation_scaled_mod esi_mod_right_extensional_stored_relation_scaled_mod. ((S i) * z) + p * esi_mod_left_extensional_stored_relation_scaled_mod = (a) + p * esi_mod_right_extensional_stored_relation_scaled_mod))))))
  14. 0014specialize hprefix i
  15. 0015apply hprefix
  16. 0016exact hi
  17. 0017cases hstored
  18. 0018cases hstored_witness
  19. 0019cases hrelation
  20. 0020cases hstored_witness_right
  21. 0021have heq : y = x
  22. 0022specialize prime_scaled_inverse_unique p
  23. 0023specialize prime_scaled_inverse_unique a
  24. 0024specialize prime_scaled_inverse_unique (S i)
  25. 0025specialize prime_scaled_inverse_unique y
  26. 0026specialize prime_scaled_inverse_unique x
  27. 0027apply prime_scaled_inverse_unique
  28. 0028exact hp
  29. 0029exact hrelation_right
  30. 0030exact hstored_witness_right_right
  31. 0031rewrite heq
  32. 0032rewrite heq
  33. 0033exact hstored_witness_left