PA008J · theorem

prime_mul_residue_product_balance

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

Scaling the nonzero residues modulo a prime preserves their exact product modulo p.

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. ∀ a. ∀ b. ∀ c. ∀ F. ∀ A. p = S n → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,n) → Product(b,c,n,F) → Pow(a,n,A) → ModEq(p,A · F,F)

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

PD0003 Dvd PD0004 Prime PD0008 ModEq PD0014 Product PD0018 Range PD0020 Pow

6 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product PD0024 BoundedPrefix PD0025 InjectivePrefix

12 occurrences

Exact expanded native-PA statement
forall p n a b c F A. p = S n -> ((~(p = 1) /\ forall frm_prime_left_balance_prime frm_prime_right_balance_prime. p = frm_prime_left_balance_prime * frm_prime_right_balance_prime -> frm_prime_left_balance_prime = 1 \/ frm_prime_right_balance_prime = 1)) -> (~(exists frm_factor_balance_multiplier. a = p * frm_factor_balance_multiplier)) -> (forall ff_i_frp_range_balance_range. (exists ff_lt_frp_range_balance_range_bound. ff_lt_frp_range_balance_range_bound + S ff_i_frp_range_balance_range = n) -> (((exists ff_h_frp_range_balance_range_decoded. ff_h_frp_range_balance_range_decoded + S (1 + ff_i_frp_range_balance_range) = S ((S (ff_i_frp_range_balance_range)) * c)) /\ exists ff_q_frp_range_balance_range_decoded. b = ff_q_frp_range_balance_range_decoded * S ((S (ff_i_frp_range_balance_range)) * c) + (1 + ff_i_frp_range_balance_range)))) -> (exists ff_u_balance_source ff_v_balance_source. ((((exists ff_h_balance_source_start. ff_h_balance_source_start + S (1) = S ((S (0)) * ff_v_balance_source)) /\ exists ff_q_balance_source_start. ff_u_balance_source = ff_q_balance_source_start * S ((S (0)) * ff_v_balance_source) + (1))) /\ ((((exists ff_h_balance_source_terminal. ff_h_balance_source_terminal + S (F) = S ((S (n)) * ff_v_balance_source)) /\ exists ff_q_balance_source_terminal. ff_u_balance_source = ff_q_balance_source_terminal * S ((S (n)) * ff_v_balance_source) + (F))) /\ forall ff_i_balance_source. (exists ff_lt_balance_source_bound. ff_lt_balance_source_bound + S ff_i_balance_source = n) -> exists ff_p_balance_source ff_r_balance_source ff_s_balance_source. ((((exists ff_h_balance_source_factor. ff_h_balance_source_factor + S (ff_p_balance_source) = S ((S (ff_i_balance_source)) * c)) /\ exists ff_q_balance_source_factor. b = ff_q_balance_source_factor * S ((S (ff_i_balance_source)) * c) + (ff_p_balance_source))) /\ ((((exists ff_h_balance_source_partial. ff_h_balance_source_partial + S (ff_r_balance_source) = S ((S (ff_i_balance_source)) * ff_v_balance_source)) /\ exists ff_q_balance_source_partial. ff_u_balance_source = ff_q_balance_source_partial * S ((S (ff_i_balance_source)) * ff_v_balance_source) + (ff_r_balance_source))) /\ ((((exists ff_h_balance_source_successor. ff_h_balance_source_successor + S (ff_s_balance_source) = S ((S (S ff_i_balance_source)) * ff_v_balance_source)) /\ exists ff_q_balance_source_successor. ff_u_balance_source = ff_q_balance_source_successor * S ((S (S ff_i_balance_source)) * ff_v_balance_source) + (ff_s_balance_source))) /\ ff_s_balance_source = ff_r_balance_source * ff_p_balance_source)))))) -> (exists ff_b_balance_power ff_c_balance_power. ((forall ff_i_balance_power_repeat. (exists ff_lt_balance_power_repeat_bound. ff_lt_balance_power_repeat_bound + S ff_i_balance_power_repeat = n) -> (((exists ff_h_balance_power_repeat_decoded. ff_h_balance_power_repeat_decoded + S (a) = S ((S (ff_i_balance_power_repeat)) * ff_c_balance_power)) /\ exists ff_q_balance_power_repeat_decoded. ff_b_balance_power = ff_q_balance_power_repeat_decoded * S ((S (ff_i_balance_power_repeat)) * ff_c_balance_power) + (a)))) /\ (exists ff_u_balance_power_product ff_v_balance_power_product. ((((exists ff_h_balance_power_product_start. ff_h_balance_power_product_start + S (1) = S ((S (0)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_start. ff_u_balance_power_product = ff_q_balance_power_product_start * S ((S (0)) * ff_v_balance_power_product) + (1))) /\ ((((exists ff_h_balance_power_product_terminal. ff_h_balance_power_product_terminal + S (A) = S ((S (n)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_terminal. ff_u_balance_power_product = ff_q_balance_power_product_terminal * S ((S (n)) * ff_v_balance_power_product) + (A))) /\ forall ff_i_balance_power_product. (exists ff_lt_balance_power_product_bound. ff_lt_balance_power_product_bound + S ff_i_balance_power_product = n) -> exists ff_p_balance_power_product ff_r_balance_power_product ff_s_balance_power_product. ((((exists ff_h_balance_power_product_factor. ff_h_balance_power_product_factor + S (ff_p_balance_power_product) = S ((S (ff_i_balance_power_product)) * ff_c_balance_power)) /\ exists ff_q_balance_power_product_factor. ff_b_balance_power = ff_q_balance_power_product_factor * S ((S (ff_i_balance_power_product)) * ff_c_balance_power) + (ff_p_balance_power_product))) /\ ((((exists ff_h_balance_power_product_partial. ff_h_balance_power_product_partial + S (ff_r_balance_power_product) = S ((S (ff_i_balance_power_product)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_partial. ff_u_balance_power_product = ff_q_balance_power_product_partial * S ((S (ff_i_balance_power_product)) * ff_v_balance_power_product) + (ff_r_balance_power_product))) /\ ((((exists ff_h_balance_power_product_successor. ff_h_balance_power_product_successor + S (ff_s_balance_power_product) = S ((S (S ff_i_balance_power_product)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_successor. ff_u_balance_power_product = ff_q_balance_power_product_successor * S ((S (S ff_i_balance_power_product)) * ff_v_balance_power_product) + (ff_s_balance_power_product))) /\ ff_s_balance_power_product = ff_r_balance_power_product * ff_p_balance_power_product)))))))) -> (exists fsp_product_mod_left_balance_result fsp_product_mod_right_balance_result. (A * F) + p * fsp_product_mod_left_balance_result = F + p * fsp_product_mod_right_balance_result)

Proof neighborhood

Direct theorem prerequisites

PA008I prime_mul_residue_reindex_exists PA007Q beta_product_pointwise_scale_mod PA003X beta_product_exists PA007X beta_product_permutation_invariant

Direct theorem dependents

PA008L fermat_predecessor_exponent_mod_one

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

71 script commands · 13 reading checkpoints · 4 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 (4)
prime mul residue reindex existsbeta product pointwise scale modbeta product existsbeta product permutation invariant
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 a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro F
  7. L7
    intro A
  8. L8
    intro hpn
  9. L9
    intro hp
  10. L10
    intro hnotdiv
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hrange
  2. L12
    intro hF
  3. L13
    intro hA
03Establish hreindexL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mul residue reindex exists.

  1. L14
    have hreindex · expand full local formula (651 characters)have hreindex : ∃ fpb_map_code_balance_reindex. ∃ fpb_map_scale_balance_reindex. ∃ fpb_target_code_balance_reindex. ∃ fpb_target_scale_balance_reindex. BoundedPrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n) ∧ (InjectivePrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,n) → BetaAt(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,x,y) → BetaAt(b,c,y,z) → BetaAt(fpb_target_code_balance_reindex,fpb_target_scale_balance_reindex,x,z)) ∧ (∀ x. ∀ y. ∀ z. Lt(x,n) → BetaAt(b,c,x,y) → BetaAt(fpb_target_code_balance_reindex,fpb_target_scale_balance_reindex,x,z) → ModEq(p,a · y,z))))
    Definitions: BoundedPrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n)InjectivePrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n)Lt(x,n)BetaAt(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,x,y)BetaAt(b,c,y,z)BetaAt(fpb_target_code_balance_reindex,fpb_target_scale_balance_reindex,x,z)BetaAt(b,c,x,y)ModEq(p,a · y,z)Original native command in the exact edition
  2. L15
    specialize prime_mul_residue_reindex_exists p
  3. L16
    specialize prime_mul_residue_reindex_exists n
  4. L17
    specialize prime_mul_residue_reindex_exists a
  5. L18
    specialize prime_mul_residue_reindex_exists b
  6. L19
    specialize prime_mul_residue_reindex_exists c
  7. L20
    apply prime_mul_residue_reindex_exists
  8. L21
    exact hpn
  9. L22
    exact hp
  10. L23
    exact hnotdiv
04Use earlier factsL24–24

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

  1. L24
    exact hrange
05Separate the logical casesL25–31

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

  1. L25
    cases hreindex
  2. L26
    cases hreindex_witness
  3. L27
    cases hreindex_witness_witness
  4. L28
    cases hreindex_witness_witness_witness
  5. L29
    cases hreindex_witness_witness_witness_witness
  6. L30
    cases hreindex_witness_witness_witness_witness_right
  7. L31
    cases hreindex_witness_witness_witness_witness_right_right
06Establish htarget_product_existsL32–36

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have htarget_product_exists : ∃ Q. Product(x2,x3,n,Q)Definitions: Product(x2,x3,n,Q)Original native command in the exact edition
  2. L33
    specialize beta_product_exists x2
  3. L34
    specialize beta_product_exists x3
  4. L35
    specialize beta_product_exists n
  5. L36
    exact beta_product_exists
07Separate the logical casesL37–37

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

  1. L37
    cases htarget_product_exists
08Establish hFQL38–47

Establish this local claim before using it. It is not an additional assumption.

  1. L38
    have hFQ : F = x4
  2. L39
    specialize beta_product_permutation_invariant n
  3. L40
    specialize beta_product_permutation_invariant x
  4. L41
    specialize beta_product_permutation_invariant x1
  5. L42
    specialize beta_product_permutation_invariant b
  6. L43
    specialize beta_product_permutation_invariant c
  7. L44
    specialize beta_product_permutation_invariant x2
  8. L45
    specialize beta_product_permutation_invariant x3
  9. L46
    specialize beta_product_permutation_invariant F
  10. L47
    specialize beta_product_permutation_invariant x4
09Use earlier factsL48–53

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

  1. L48
    apply beta_product_permutation_invariant
  2. L49
    exact hreindex_witness_witness_witness_witness_left
  3. L50
    exact hreindex_witness_witness_witness_witness_right_left
  4. L51
    exact hreindex_witness_witness_witness_witness_right_right_left
  5. L52
    exact hF
  6. L53
    exact htarget_product_exists_witness
10Establish hscaleL54–63

Establish this local claim before using it. It is not an additional assumption.

  1. L54
    have hscale : ModEq(p,A · F,x4)Definitions: ModEq(p,A · F,x4)Original native command in the exact edition
  2. L55
    specialize beta_product_pointwise_scale_mod p
  3. L56
    specialize beta_product_pointwise_scale_mod a
  4. L57
    specialize beta_product_pointwise_scale_mod b
  5. L58
    specialize beta_product_pointwise_scale_mod c
  6. L59
    specialize beta_product_pointwise_scale_mod x2
  7. L60
    specialize beta_product_pointwise_scale_mod x3
  8. L61
    specialize beta_product_pointwise_scale_mod n
  9. L62
    specialize beta_product_pointwise_scale_mod F
  10. L63
    specialize beta_product_pointwise_scale_mod x4
11Use earlier factsL64–69

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

  1. L64
    specialize beta_product_pointwise_scale_mod A
  2. L65
    apply beta_product_pointwise_scale_mod
  3. L66
    exact hreindex_witness_witness_witness_witness_right_right_right
  4. L67
    exact hF
  5. L68
    exact htarget_product_exists_witness
  6. L69
    exact hA
12Calculate and transport equalitiesL70–70

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L70
    rewrite <- hFQ at hscale
13Use earlier factsL71–71

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

  1. L71
    exact hscale

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro F
  7. 0007intro A
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hnotdiv
  11. 0011intro hrange
  12. 0012intro hF
  13. 0013intro hA
  14. 0014have hreindex : ∃ fpb_map_code_balance_reindex. ∃ fpb_map_scale_balance_reindex. ∃ fpb_target_code_balance_reindex. ∃ fpb_target_scale_balance_reindex. BoundedPrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n) ∧ (InjectivePrefix(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,n) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,n) → BetaAt(fpb_map_code_balance_reindex,fpb_map_scale_balance_reindex,x,y) → BetaAt(b,c,y,z) → BetaAt(fpb_target_code_balance_reindex,fpb_target_scale_balance_reindex,x,z)) ∧ (∀ x. ∀ y. ∀ z. Lt(x,n) → BetaAt(b,c,x,y) → BetaAt(fpb_target_code_balance_reindex,fpb_target_scale_balance_reindex,x,z) → ModEq(p,a · y,z))))
    Exact native replay linehave hreindex : exists fpb_map_code_balance_reindex fpb_map_scale_balance_reindex fpb_target_code_balance_reindex fpb_target_scale_balance_reindex. ((forall fp_i_fpb_balance_reindex_data_bounded. (exists fp_gap_fpb_balance_reindex_data_bounded_index. fp_gap_fpb_balance_reindex_data_bounded_index + S fp_i_fpb_balance_reindex_data_bounded = n) -> exists fp_value_fpb_balance_reindex_data_bounded. ((((exists ff_h_fpb_balance_reindex_data_bounded_entry. ff_h_fpb_balance_reindex_data_bounded_entry + S (fp_value_fpb_balance_reindex_data_bounded) = S ((S (fp_i_fpb_balance_reindex_data_bounded)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_bounded_entry. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_bounded_entry * S ((S (fp_i_fpb_balance_reindex_data_bounded)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_bounded))) /\ (exists fp_gap_fpb_balance_reindex_data_bounded_value. fp_gap_fpb_balance_reindex_data_bounded_value + S fp_value_fpb_balance_reindex_data_bounded = n))) /\ ((forall fp_i_fpb_balance_reindex_data_injective fp_j_fpb_balance_reindex_data_injective fp_value_fpb_balance_reindex_data_injective. (exists fp_gap_fpb_balance_reindex_data_injective_i. fp_gap_fpb_balance_reindex_data_injective_i + S fp_i_fpb_balance_reindex_data_injective = n) -> (exists fp_gap_fpb_balance_reindex_data_injective_j. fp_gap_fpb_balance_reindex_data_injective_j + S fp_j_fpb_balance_reindex_data_injective = n) -> (((exists ff_h_fpb_balance_reindex_data_injective_left. ff_h_fpb_balance_reindex_data_injective_left + S (fp_value_fpb_balance_reindex_data_injective) = S ((S (fp_i_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_injective_left. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_injective_left * S ((S (fp_i_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_injective))) -> (((exists ff_h_fpb_balance_reindex_data_injective_right. ff_h_fpb_balance_reindex_data_injective_right + S (fp_value_fpb_balance_reindex_data_injective) = S ((S (fp_j_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_injective_right. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_injective_right * S ((S (fp_j_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_injective))) -> fp_i_fpb_balance_reindex_data_injective = fp_j_fpb_balance_reindex_data_injective) /\ ((forall fpr_i_fpb_balance_reindex_data_aligned fpr_j_fpb_balance_reindex_data_aligned fpr_x_fpb_balance_reindex_data_aligned. (exists fpr_h_fpb_balance_reindex_data_aligned. fpr_h_fpb_balance_reindex_data_aligned + S fpr_i_fpb_balance_reindex_data_aligned = n) -> (((exists ff_h_fpb_balance_reindex_data_aligned_map. ff_h_fpb_balance_reindex_data_aligned_map + S (fpr_j_fpb_balance_reindex_data_aligned) = S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_aligned_map. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_aligned_map * S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_map_scale_balance_reindex) + (fpr_j_fpb_balance_reindex_data_aligned))) -> (((exists ff_h_fpb_balance_reindex_data_aligned_source. ff_h_fpb_balance_reindex_data_aligned_source + S (fpr_x_fpb_balance_reindex_data_aligned) = S ((S (fpr_j_fpb_balance_reindex_data_aligned)) * c)) /\ exists ff_q_fpb_balance_reindex_data_aligned_source. b = ff_q_fpb_balance_reindex_data_aligned_source * S ((S (fpr_j_fpb_balance_reindex_data_aligned)) * c) + (fpr_x_fpb_balance_reindex_data_aligned))) -> (((exists ff_h_fpb_balance_reindex_data_aligned_target. ff_h_fpb_balance_reindex_data_aligned_target + S (fpr_x_fpb_balance_reindex_data_aligned) = S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_target_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_aligned_target. fpb_target_code_balance_reindex = ff_q_fpb_balance_reindex_data_aligned_target * S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_target_scale_balance_reindex) + (fpr_x_fpb_balance_reindex_data_aligned)))) /\ (forall fsp_index_fpb_balance_reindex_data_scaled fsp_source_fpb_balance_reindex_data_scaled fsp_target_fpb_balance_reindex_data_scaled. (exists fsp_gap_fpb_balance_reindex_data_scaled. fsp_gap_fpb_balance_reindex_data_scaled + S fsp_index_fpb_balance_reindex_data_scaled = n) -> (((exists fsp_source_height_fpb_balance_reindex_data_scaled. fsp_source_height_fpb_balance_reindex_data_scaled + S (fsp_source_fpb_balance_reindex_data_scaled) = S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * c)) /\ exists fsp_source_quotient_fpb_balance_reindex_data_scaled. b = fsp_source_quotient_fpb_balance_reindex_data_scaled * S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * c) + (fsp_source_fpb_balance_reindex_data_scaled))) -> (((exists fsp_target_height_fpb_balance_reindex_data_scaled. fsp_target_height_fpb_balance_reindex_data_scaled + S (fsp_target_fpb_balance_reindex_data_scaled) = S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * fpb_target_scale_balance_reindex)) /\ exists fsp_target_quotient_fpb_balance_reindex_data_scaled. fpb_target_code_balance_reindex = fsp_target_quotient_fpb_balance_reindex_data_scaled * S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * fpb_target_scale_balance_reindex) + (fsp_target_fpb_balance_reindex_data_scaled))) -> (exists fsp_mod_left_fpb_balance_reindex_data_scaled fsp_mod_right_fpb_balance_reindex_data_scaled. a * fsp_source_fpb_balance_reindex_data_scaled + p * fsp_mod_left_fpb_balance_reindex_data_scaled = fsp_target_fpb_balance_reindex_data_scaled + p * fsp_mod_right_fpb_balance_reindex_data_scaled)))))
  15. 0015specialize prime_mul_residue_reindex_exists p
  16. 0016specialize prime_mul_residue_reindex_exists n
  17. 0017specialize prime_mul_residue_reindex_exists a
  18. 0018specialize prime_mul_residue_reindex_exists b
  19. 0019specialize prime_mul_residue_reindex_exists c
  20. 0020apply prime_mul_residue_reindex_exists
  21. 0021exact hpn
  22. 0022exact hp
  23. 0023exact hnotdiv
  24. 0024exact hrange
  25. 0025cases hreindex
  26. 0026cases hreindex_witness
  27. 0027cases hreindex_witness_witness
  28. 0028cases hreindex_witness_witness_witness
  29. 0029cases hreindex_witness_witness_witness_witness
  30. 0030cases hreindex_witness_witness_witness_witness_right
  31. 0031cases hreindex_witness_witness_witness_witness_right_right
  32. 0032have htarget_product_exists : ∃ Q. Product(x2,x3,n,Q)
    Exact native replay linehave htarget_product_exists : exists Q. (exists ff_u_balance_target_exists ff_v_balance_target_exists. ((((exists ff_h_balance_target_exists_start. ff_h_balance_target_exists_start + S (1) = S ((S (0)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_start. ff_u_balance_target_exists = ff_q_balance_target_exists_start * S ((S (0)) * ff_v_balance_target_exists) + (1))) /\ ((((exists ff_h_balance_target_exists_terminal. ff_h_balance_target_exists_terminal + S (Q) = S ((S (n)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_terminal. ff_u_balance_target_exists = ff_q_balance_target_exists_terminal * S ((S (n)) * ff_v_balance_target_exists) + (Q))) /\ forall ff_i_balance_target_exists. (exists ff_lt_balance_target_exists_bound. ff_lt_balance_target_exists_bound + S ff_i_balance_target_exists = n) -> exists ff_p_balance_target_exists ff_r_balance_target_exists ff_s_balance_target_exists. ((((exists ff_h_balance_target_exists_factor. ff_h_balance_target_exists_factor + S (ff_p_balance_target_exists) = S ((S (ff_i_balance_target_exists)) * x3)) /\ exists ff_q_balance_target_exists_factor. x2 = ff_q_balance_target_exists_factor * S ((S (ff_i_balance_target_exists)) * x3) + (ff_p_balance_target_exists))) /\ ((((exists ff_h_balance_target_exists_partial. ff_h_balance_target_exists_partial + S (ff_r_balance_target_exists) = S ((S (ff_i_balance_target_exists)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_partial. ff_u_balance_target_exists = ff_q_balance_target_exists_partial * S ((S (ff_i_balance_target_exists)) * ff_v_balance_target_exists) + (ff_r_balance_target_exists))) /\ ((((exists ff_h_balance_target_exists_successor. ff_h_balance_target_exists_successor + S (ff_s_balance_target_exists) = S ((S (S ff_i_balance_target_exists)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_successor. ff_u_balance_target_exists = ff_q_balance_target_exists_successor * S ((S (S ff_i_balance_target_exists)) * ff_v_balance_target_exists) + (ff_s_balance_target_exists))) /\ ff_s_balance_target_exists = ff_r_balance_target_exists * ff_p_balance_target_exists))))))
  33. 0033specialize beta_product_exists x2
  34. 0034specialize beta_product_exists x3
  35. 0035specialize beta_product_exists n
  36. 0036exact beta_product_exists
  37. 0037cases htarget_product_exists
  38. 0038have hFQ : F = x4
  39. 0039specialize beta_product_permutation_invariant n
  40. 0040specialize beta_product_permutation_invariant x
  41. 0041specialize beta_product_permutation_invariant x1
  42. 0042specialize beta_product_permutation_invariant b
  43. 0043specialize beta_product_permutation_invariant c
  44. 0044specialize beta_product_permutation_invariant x2
  45. 0045specialize beta_product_permutation_invariant x3
  46. 0046specialize beta_product_permutation_invariant F
  47. 0047specialize beta_product_permutation_invariant x4
  48. 0048apply beta_product_permutation_invariant
  49. 0049exact hreindex_witness_witness_witness_witness_left
  50. 0050exact hreindex_witness_witness_witness_witness_right_left
  51. 0051exact hreindex_witness_witness_witness_witness_right_right_left
  52. 0052exact hF
  53. 0053exact htarget_product_exists_witness
  54. 0054have hscale : ModEq(p,A · F,x4)
    Exact native replay linehave hscale : exists fsp_product_mod_left_balance_scaled_product fsp_product_mod_right_balance_scaled_product. (A * F) + p * fsp_product_mod_left_balance_scaled_product = x4 + p * fsp_product_mod_right_balance_scaled_product
  55. 0055specialize beta_product_pointwise_scale_mod p
  56. 0056specialize beta_product_pointwise_scale_mod a
  57. 0057specialize beta_product_pointwise_scale_mod b
  58. 0058specialize beta_product_pointwise_scale_mod c
  59. 0059specialize beta_product_pointwise_scale_mod x2
  60. 0060specialize beta_product_pointwise_scale_mod x3
  61. 0061specialize beta_product_pointwise_scale_mod n
  62. 0062specialize beta_product_pointwise_scale_mod F
  63. 0063specialize beta_product_pointwise_scale_mod x4
  64. 0064specialize beta_product_pointwise_scale_mod A
  65. 0065apply beta_product_pointwise_scale_mod
  66. 0066exact hreindex_witness_witness_witness_witness_right_right_right
  67. 0067exact hF
  68. 0068exact htarget_product_exists_witness
  69. 0069exact hA
  70. 0070rewrite <- hFQ at hscale
  71. 0071exact hscale