PA00AN · theorem

inverse_prefix_involutive

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ b. ∀ c. ∀ i. ∀ j. p = S n → InversePrefix(p,n,b,c,n) → Lt(i,n) → BetaAt(b,c,i,j) → Lt(j,n) ∧ BetaAt(b,c,j,i)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0037 InversePrefix

5 occurrences

In local proof propositions

PD0036 InverseIndex

2 occurrences

Exact expanded native-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))))

Proof neighborhood

Direct theorem prerequisites

PA00AF inverse_prefix_entry_sound PA00AJ inverse_index_symmetric PA00AM inverse_prefix_extensional

Direct theorem dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_orbit

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

45 script commands · 7 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
inverse prefix entry soundinverse index symmetricinverse prefix extensional
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro hpn
  8. L8
    intro hprefix
  9. L9
    intro hi
  10. L10
    intro hat
02Establish hforwardL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply inverse prefix entry sound.

  1. L11
    have hforward : InverseIndex(p,n,i,j)Definitions: InverseIndex(p,n,i,j)Original native command in the exact edition
  2. L12
    specialize inverse_prefix_entry_sound p
  3. L13
    specialize inverse_prefix_entry_sound n
  4. L14
    specialize inverse_prefix_entry_sound b
  5. L15
    specialize inverse_prefix_entry_sound c
  6. L16
    specialize inverse_prefix_entry_sound n
  7. L17
    specialize inverse_prefix_entry_sound i
  8. L18
    specialize inverse_prefix_entry_sound j
  9. L19
    apply inverse_prefix_entry_sound
  10. L20
    exact hprefix
03Use earlier factsL21–22

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    exact hi
  2. L22
    exact hat
04Establish hreverseL23–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply inverse index symmetric.

  1. L23
    have hreverse : InverseIndex(p,n,j,i)Definitions: InverseIndex(p,n,j,i)Original native command in the exact edition
  2. L24
    specialize inverse_index_symmetric p
  3. L25
    specialize inverse_index_symmetric n
  4. L26
    specialize inverse_index_symmetric i
  5. L27
    specialize inverse_index_symmetric j
  6. L28
    apply inverse_index_symmetric
  7. L29
    exact hforward
05Separate the logical casesL30–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hforward
  2. L31
    cases hforward_right
  3. L32
    split
06Use earlier factsL33–42

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    exact hforward_right_left
  2. L34
    specialize inverse_prefix_extensional p
  3. L35
    specialize inverse_prefix_extensional n
  4. L36
    specialize inverse_prefix_extensional b
  5. L37
    specialize inverse_prefix_extensional c
  6. L38
    specialize inverse_prefix_extensional n
  7. L39
    specialize inverse_prefix_extensional j
  8. L40
    specialize inverse_prefix_extensional i
  9. L41
    apply inverse_prefix_extensional
  10. L42
    exact hpn
07Use earlier factsL43–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L43
    exact hprefix
  2. L44
    exact hforward_right_left
  3. L45
    exact hreverse

Library-wide reading audit

Original defined command ledger · 45 lines
  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 : InverseIndex(p,n,i,j)
    Exact native replay linehave 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 : InverseIndex(p,n,j,i)
    Exact native replay linehave 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