PA00AM

inverse_prefix_extensional

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

A full inverse relation at a covered index is decoded by the prefix.

Exact expanded PA statement

forall p n b c l i j. p = S n -> (forall wip_index_extensional_prefix. (exists wip_gap_extensional_prefix_prefix_bound. wip_gap_extensional_prefix_prefix_bound + S wip_index_extensional_prefix = l) -> exists wip_mate_extensional_prefix. ((((exists wip_beta_height_extensional_prefix_decoded. wip_beta_height_extensional_prefix_decoded + S (wip_mate_extensional_prefix) = S ((S (wip_index_extensional_prefix)) * c)) /\ exists wip_beta_quotient_extensional_prefix_decoded. b = wip_beta_quotient_extensional_prefix_decoded * S ((S (wip_index_extensional_prefix)) * c) + (wip_mate_extensional_prefix))) /\ ((exists wip_gap_extensional_prefix_inverse_index_bound. wip_gap_extensional_prefix_inverse_index_bound + S wip_index_extensional_prefix = n) /\ ((exists wip_gap_extensional_prefix_inverse_mate_bound. wip_gap_extensional_prefix_inverse_mate_bound + S wip_mate_extensional_prefix = n) /\ (exists wip_mod_left_extensional_prefix_inverse_mod wip_mod_right_extensional_prefix_inverse_mod. ((S wip_index_extensional_prefix) * S wip_mate_extensional_prefix) + p * wip_mod_left_extensional_prefix_inverse_mod = 1 + p * wip_mod_right_extensional_prefix_inverse_mod))))) -> (exists wip_gap_extensional_index_bound. wip_gap_extensional_index_bound + S i = l) -> ((exists wip_gap_extensional_source_index_bound. wip_gap_extensional_source_index_bound + S i = n) /\ ((exists wip_gap_extensional_source_mate_bound. wip_gap_extensional_source_mate_bound + S j = n) /\ (exists wip_mod_left_extensional_source_mod wip_mod_right_extensional_source_mod. ((S i) * S j) + p * wip_mod_left_extensional_source_mod = 1 + p * wip_mod_right_extensional_source_mod))) -> (((exists wip_beta_height_extensional_result. wip_beta_height_extensional_result + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_extensional_result. b = wip_beta_quotient_extensional_result * S ((S (i)) * c) + (j)))

Structural proof guide

Generated structural guide

A full inverse relation at a covered index is decoded by the prefix.

Use the direct prerequisites bounded_inverse_index_unique as previously established PA formulas.

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

Referenced ingredients

PA00AL bounded_inverse_index_unique

Proof neighborhood

Direct dependencies

PA00AL bounded_inverse_index_unique

Direct dependents

PA00AN inverse_prefix_involutive PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed

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 l
  6. 0006intro i
  7. 0007intro j
  8. 0008intro hpn
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hidx
  12. 0012have hstored : exists k. ((((exists wip_beta_height_extensional_stored_at. wip_beta_height_extensional_stored_at + S (k) = S ((S (i)) * c)) /\ exists wip_beta_quotient_extensional_stored_at. b = wip_beta_quotient_extensional_stored_at * S ((S (i)) * c) + (k))) /\ ((exists wip_gap_extensional_stored_inverse_index_bound. wip_gap_extensional_stored_inverse_index_bound + S i = n) /\ ((exists wip_gap_extensional_stored_inverse_mate_bound. wip_gap_extensional_stored_inverse_mate_bound + S k = n) /\ (exists wip_mod_left_extensional_stored_inverse_mod wip_mod_right_extensional_stored_inverse_mod. ((S i) * S k) + p * wip_mod_left_extensional_stored_inverse_mod = 1 + p * wip_mod_right_extensional_stored_inverse_mod))))
  13. 0013specialize hprefix i
  14. 0014apply hprefix
  15. 0015exact hi
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have heq : j = x
  19. 0019specialize bounded_inverse_index_unique p
  20. 0020specialize bounded_inverse_index_unique n
  21. 0021specialize bounded_inverse_index_unique i
  22. 0022specialize bounded_inverse_index_unique j
  23. 0023specialize bounded_inverse_index_unique x
  24. 0024apply bounded_inverse_index_unique
  25. 0025exact hpn
  26. 0026exact hidx
  27. 0027exact hstored_witness_right
  28. 0028rewrite heq
  29. 0029rewrite heq
  30. 0030exact hstored_witness_left