PA00AI

prime_inverse_prefix_nonendpoint_not_fixed

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

A decoded inverse entry from a nonendpoint source is not fixed.

Exact expanded PA statement

forall p n b c i j. p = S n -> ((~(p = 1) /\ forall wip_prime_left_orbit_prime wip_prime_right_orbit_prime. p = wip_prime_left_orbit_prime * wip_prime_right_orbit_prime -> wip_prime_left_orbit_prime = 1 \/ wip_prime_right_orbit_prime = 1)) -> (forall wip_index_orbit_prefix. (exists wip_gap_orbit_prefix_prefix_bound. wip_gap_orbit_prefix_prefix_bound + S wip_index_orbit_prefix = n) -> exists wip_mate_orbit_prefix. ((((exists wip_beta_height_orbit_prefix_decoded. wip_beta_height_orbit_prefix_decoded + S (wip_mate_orbit_prefix) = S ((S (wip_index_orbit_prefix)) * c)) /\ exists wip_beta_quotient_orbit_prefix_decoded. b = wip_beta_quotient_orbit_prefix_decoded * S ((S (wip_index_orbit_prefix)) * c) + (wip_mate_orbit_prefix))) /\ ((exists wip_gap_orbit_prefix_inverse_index_bound. wip_gap_orbit_prefix_inverse_index_bound + S wip_index_orbit_prefix = n) /\ ((exists wip_gap_orbit_prefix_inverse_mate_bound. wip_gap_orbit_prefix_inverse_mate_bound + S wip_mate_orbit_prefix = n) /\ (exists wip_mod_left_orbit_prefix_inverse_mod wip_mod_right_orbit_prefix_inverse_mod. ((S wip_index_orbit_prefix) * S wip_mate_orbit_prefix) + p * wip_mod_left_orbit_prefix_inverse_mod = 1 + p * wip_mod_right_orbit_prefix_inverse_mod))))) -> (exists wip_gap_orbit_source_bound. wip_gap_orbit_source_bound + S i = n) -> (((exists wip_beta_height_orbit_source_entry. wip_beta_height_orbit_source_entry + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_orbit_source_entry. b = wip_beta_quotient_orbit_source_entry * S ((S (i)) * c) + (j))) -> ((~(i = 0) /\ ~((S i) = n))) -> ~(i = j)

Structural proof guide

Generated structural guide

A decoded inverse entry from a nonendpoint source is not fixed.

Use the direct prerequisites prime_inverse_prefix_fixed_cases as previously established PA formulas.

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

Referenced ingredients

PA00AH prime_inverse_prefix_fixed_cases

Proof neighborhood

Direct dependencies

PA00AH prime_inverse_prefix_fixed_cases

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 hp
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012intro hnonendpoint
  13. 0013cases hnonendpoint
  14. 0014intro heq
  15. 0015have hfixed : ((exists wip_beta_height_orbit_source_fixed. wip_beta_height_orbit_source_fixed + S (i) = S ((S (i)) * c)) /\ exists wip_beta_quotient_orbit_source_fixed. b = wip_beta_quotient_orbit_source_fixed * S ((S (i)) * c) + (i))
  16. 0016rewrite <- heq at hat
  17. 0017rewrite <- heq at hat
  18. 0018exact hat
  19. 0019have hcases : i = 0 \/ S i = n
  20. 0020specialize prime_inverse_prefix_fixed_cases p
  21. 0021specialize prime_inverse_prefix_fixed_cases n
  22. 0022specialize prime_inverse_prefix_fixed_cases b
  23. 0023specialize prime_inverse_prefix_fixed_cases c
  24. 0024specialize prime_inverse_prefix_fixed_cases i
  25. 0025apply prime_inverse_prefix_fixed_cases
  26. 0026exact hpn
  27. 0027exact hp
  28. 0028exact hprefix
  29. 0029exact hi
  30. 0030exact hfixed
  31. 0031cases hcases
  32. 0032apply hnonendpoint_left
  33. 0033exact hcases_left
  34. 0034apply hnonendpoint_right
  35. 0035exact hcases_right