PA002H

beta_exclusive_recode_invariant_step

Stable checked-use theorem · independently closed

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

Exact expanded PA statement

forall N c b e k P z. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

Structural proof guide

Generated structural guide

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

Use the direct prerequisites beta_exclusive_accumulated_product_step, beta_exclusive_recode_congruence_step as previously established PA formulas.

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

Referenced ingredients

PA001U beta_exclusive_accumulated_product_step PA002G beta_exclusive_recode_congruence_step

Proof neighborhood

Direct dependencies

PA001U beta_exclusive_accumulated_product_step PA002G beta_exclusive_recode_congruence_step

Direct dependents

PA002I bounded_beta_exclusive_recode_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro k
  6. 0006intro P
  7. 0007intro z
  8. 0008intro hcm
  9. 0009intro hkN
  10. 0010intro hP
  11. 0011intro hdiv
  12. 0012intro hcong
  13. 0013intro hfuture
  14. 0014have hproduct : (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))
  15. 0015specialize beta_exclusive_accumulated_product_step N
  16. 0016specialize beta_exclusive_accumulated_product_step c
  17. 0017specialize beta_exclusive_accumulated_product_step k
  18. 0018specialize beta_exclusive_accumulated_product_step P
  19. 0019apply beta_exclusive_accumulated_product_step
  20. 0020exact hcm
  21. 0021exact hkN
  22. 0022exact hP
  23. 0023exact hdiv
  24. 0024exact hfuture
  25. 0025have hcodes : exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v
  26. 0026specialize beta_exclusive_recode_congruence_step N
  27. 0027specialize beta_exclusive_recode_congruence_step c
  28. 0028specialize beta_exclusive_recode_congruence_step b
  29. 0029specialize beta_exclusive_recode_congruence_step e
  30. 0030specialize beta_exclusive_recode_congruence_step k
  31. 0031specialize beta_exclusive_recode_congruence_step P
  32. 0032specialize beta_exclusive_recode_congruence_step z
  33. 0033apply beta_exclusive_recode_congruence_step
  34. 0034exact hkN
  35. 0035exact hP
  36. 0036exact hdiv
  37. 0037exact hcong
  38. 0038exact hfuture
  39. 0039cases hcodes
  40. 0040cases hproduct
  41. 0041cases hproduct_right
  42. 0042exists x
  43. 0043split
  44. 0044exact hproduct_left
  45. 0045split
  46. 0046exact hproduct_right_left
  47. 0047split
  48. 0048exact hcodes_witness
  49. 0049exact hproduct_right_right