PA007J · theorem

beta_sign_factor_product_power_exists

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

For p=S r, the recoded sign product exists and equals the relational power r^e.

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. ∀ r. ∀ sb. ∀ sc. ∀ l. ∀ e. p = S r → BitCount(sb,sc,l,e) → ∃ x. ∃ y. ∃ z. ∃ n. (∀ m. ∀ k. Lt(m,l) → BetaAt(sb,sc,m,k) → k = 0 ∧ BetaAt(x,y,m,1) ∨ k = 1 ∧ BetaAt(x,y,m,r)) ∧ (Product(x,y,l,z) ∧ (Pow(r,e,n) ∧ z = n))

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 PD0014 Product PD0017 BitCount PD0020 Pow

7 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product PD0020 Pow

6 occurrences

Exact expanded native-PA statement
forall p r sb sc l e. p = S r -> (((exists ff_u_recode_count_sum ff_v_recode_count_sum. ((((exists ff_h_recode_count_sum_start. ff_h_recode_count_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_start. ff_u_recode_count_sum = ff_q_recode_count_sum_start * S ((S (0)) * ff_v_recode_count_sum) + (0))) /\ ((((exists ff_h_recode_count_sum_terminal. ff_h_recode_count_sum_terminal + S (e) = S ((S (l)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_terminal. ff_u_recode_count_sum = ff_q_recode_count_sum_terminal * S ((S (l)) * ff_v_recode_count_sum) + (e))) /\ forall ff_i_recode_count_sum. (exists ff_lt_recode_count_sum_bound. ff_lt_recode_count_sum_bound + S ff_i_recode_count_sum = l) -> exists ff_a_recode_count_sum ff_r_recode_count_sum ff_s_recode_count_sum. ((((exists ff_h_recode_count_sum_summand. ff_h_recode_count_sum_summand + S (ff_a_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * sc)) /\ exists ff_q_recode_count_sum_summand. sb = ff_q_recode_count_sum_summand * S ((S (ff_i_recode_count_sum)) * sc) + (ff_a_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_partial. ff_h_recode_count_sum_partial + S (ff_r_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_partial. ff_u_recode_count_sum = ff_q_recode_count_sum_partial * S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_r_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_successor. ff_h_recode_count_sum_successor + S (ff_s_recode_count_sum) = S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_successor. ff_u_recode_count_sum = ff_q_recode_count_sum_successor * S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_s_recode_count_sum))) /\ ff_s_recode_count_sum = ff_r_recode_count_sum + ff_a_recode_count_sum)))))) /\ (forall ff_i_recode_count_bits. (exists ff_lt_recode_count_bits_bound. ff_lt_recode_count_bits_bound + S ff_i_recode_count_bits = l) -> exists ff_bit_recode_count_bits. ((((exists ff_h_recode_count_bits_decoded. ff_h_recode_count_bits_decoded + S (ff_bit_recode_count_bits) = S ((S (ff_i_recode_count_bits)) * sc)) /\ exists ff_q_recode_count_bits_decoded. sb = ff_q_recode_count_bits_decoded * S ((S (ff_i_recode_count_bits)) * sc) + (ff_bit_recode_count_bits))) /\ (ff_bit_recode_count_bits = 0 \/ ff_bit_recode_count_bits = 1))))) -> (exists fb fc F R. ((forall gspf_index_recode_endpoint_signs gspf_bit_recode_endpoint_signs. (exists gsp_lt_gap_recode_endpoint_signs_bound. gsp_lt_gap_recode_endpoint_signs_bound + S gspf_index_recode_endpoint_signs = l) -> (((exists ff_h_gspf_recode_endpoint_signs_bit. ff_h_gspf_recode_endpoint_signs_bit + S (gspf_bit_recode_endpoint_signs) = S ((S (gspf_index_recode_endpoint_signs)) * sc)) /\ exists ff_q_gspf_recode_endpoint_signs_bit. sb = ff_q_gspf_recode_endpoint_signs_bit * S ((S (gspf_index_recode_endpoint_signs)) * sc) + (gspf_bit_recode_endpoint_signs))) -> (((gspf_bit_recode_endpoint_signs = 0) /\ (((exists gsp_beta_height_gspf_recode_endpoint_signs_one. gsp_beta_height_gspf_recode_endpoint_signs_one + S (1) = S ((S (gspf_index_recode_endpoint_signs)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_endpoint_signs_one. fb = gsp_beta_quotient_gspf_recode_endpoint_signs_one * S ((S (gspf_index_recode_endpoint_signs)) * fc) + (1)))) \/ ((gspf_bit_recode_endpoint_signs = 1) /\ (((exists ff_h_gspf_recode_endpoint_signs_predecessor. ff_h_gspf_recode_endpoint_signs_predecessor + S (r) = S ((S (gspf_index_recode_endpoint_signs)) * fc)) /\ exists ff_q_gspf_recode_endpoint_signs_predecessor. fb = ff_q_gspf_recode_endpoint_signs_predecessor * S ((S (gspf_index_recode_endpoint_signs)) * fc) + (r)))))) /\ ((exists ff_u_recode_endpoint_product ff_v_recode_endpoint_product. ((((exists ff_h_recode_endpoint_product_start. ff_h_recode_endpoint_product_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_start. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_start * S ((S (0)) * ff_v_recode_endpoint_product) + (1))) /\ ((((exists ff_h_recode_endpoint_product_terminal. ff_h_recode_endpoint_product_terminal + S (F) = S ((S (l)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_terminal. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_terminal * S ((S (l)) * ff_v_recode_endpoint_product) + (F))) /\ forall ff_i_recode_endpoint_product. (exists ff_lt_recode_endpoint_product_bound. ff_lt_recode_endpoint_product_bound + S ff_i_recode_endpoint_product = l) -> exists ff_p_recode_endpoint_product ff_r_recode_endpoint_product ff_s_recode_endpoint_product. ((((exists ff_h_recode_endpoint_product_factor. ff_h_recode_endpoint_product_factor + S (ff_p_recode_endpoint_product) = S ((S (ff_i_recode_endpoint_product)) * fc)) /\ exists ff_q_recode_endpoint_product_factor. fb = ff_q_recode_endpoint_product_factor * S ((S (ff_i_recode_endpoint_product)) * fc) + (ff_p_recode_endpoint_product))) /\ ((((exists ff_h_recode_endpoint_product_partial. ff_h_recode_endpoint_product_partial + S (ff_r_recode_endpoint_product) = S ((S (ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_partial. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_partial * S ((S (ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product) + (ff_r_recode_endpoint_product))) /\ ((((exists ff_h_recode_endpoint_product_successor. ff_h_recode_endpoint_product_successor + S (ff_s_recode_endpoint_product) = S ((S (S ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_successor. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_successor * S ((S (S ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product) + (ff_s_recode_endpoint_product))) /\ ff_s_recode_endpoint_product = ff_r_recode_endpoint_product * ff_p_recode_endpoint_product)))))) /\ ((exists ff_b_recode_endpoint_power ff_c_recode_endpoint_power. ((forall ff_i_recode_endpoint_power_repeat. (exists ff_lt_recode_endpoint_power_repeat_bound. ff_lt_recode_endpoint_power_repeat_bound + S ff_i_recode_endpoint_power_repeat = e) -> (((exists ff_h_recode_endpoint_power_repeat_decoded. ff_h_recode_endpoint_power_repeat_decoded + S (r) = S ((S (ff_i_recode_endpoint_power_repeat)) * ff_c_recode_endpoint_power)) /\ exists ff_q_recode_endpoint_power_repeat_decoded. ff_b_recode_endpoint_power = ff_q_recode_endpoint_power_repeat_decoded * S ((S (ff_i_recode_endpoint_power_repeat)) * ff_c_recode_endpoint_power) + (r)))) /\ (exists ff_u_recode_endpoint_power_product ff_v_recode_endpoint_power_product. ((((exists ff_h_recode_endpoint_power_product_start. ff_h_recode_endpoint_power_product_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_start. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_start * S ((S (0)) * ff_v_recode_endpoint_power_product) + (1))) /\ ((((exists ff_h_recode_endpoint_power_product_terminal. ff_h_recode_endpoint_power_product_terminal + S (R) = S ((S (e)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_terminal. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_terminal * S ((S (e)) * ff_v_recode_endpoint_power_product) + (R))) /\ forall ff_i_recode_endpoint_power_product. (exists ff_lt_recode_endpoint_power_product_bound. ff_lt_recode_endpoint_power_product_bound + S ff_i_recode_endpoint_power_product = e) -> exists ff_p_recode_endpoint_power_product ff_r_recode_endpoint_power_product ff_s_recode_endpoint_power_product. ((((exists ff_h_recode_endpoint_power_product_factor. ff_h_recode_endpoint_power_product_factor + S (ff_p_recode_endpoint_power_product) = S ((S (ff_i_recode_endpoint_power_product)) * ff_c_recode_endpoint_power)) /\ exists ff_q_recode_endpoint_power_product_factor. ff_b_recode_endpoint_power = ff_q_recode_endpoint_power_product_factor * S ((S (ff_i_recode_endpoint_power_product)) * ff_c_recode_endpoint_power) + (ff_p_recode_endpoint_power_product))) /\ ((((exists ff_h_recode_endpoint_power_product_partial. ff_h_recode_endpoint_power_product_partial + S (ff_r_recode_endpoint_power_product) = S ((S (ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_partial. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_partial * S ((S (ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product) + (ff_r_recode_endpoint_power_product))) /\ ((((exists ff_h_recode_endpoint_power_product_successor. ff_h_recode_endpoint_power_product_successor + S (ff_s_recode_endpoint_power_product) = S ((S (S ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_successor. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_successor * S ((S (S ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product) + (ff_s_recode_endpoint_power_product))) /\ ff_s_recode_endpoint_power_product = ff_r_recode_endpoint_power_product * ff_p_recode_endpoint_power_product)))))))) /\ F = R))))

Proof neighborhood

Direct theorem prerequisites

PA007G beta_sign_factor_prefix_exists PA003X beta_product_exists PA0046 pow_exists PA007I beta_sign_factor_product_power

Direct theorem dependents

PA0085 gauss_lemma_power_congruence_exists

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

55 script commands · 16 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)
beta sign factor prefix existsbeta product existspow existsbeta sign factor product power
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro l
  6. L6
    intro e
  7. L7
    intro hp
  8. L8
    intro hcount
02Establish hsigns_existsL9–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sign factor prefix exists.

  1. L9
    have hsigns_exists : ∃ fb. ∃ fc. ∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)Definitions: Lt(x,l)BetaAt(sb,sc,x,y)BetaAt(fb,fc,x,1)BetaAt(fb,fc,x,r)Original native command in the exact edition
  2. L10
    specialize beta_sign_factor_prefix_exists sb
  3. L11
    specialize beta_sign_factor_prefix_exists sc
  4. L12
    specialize beta_sign_factor_prefix_exists r
  5. L13
    specialize beta_sign_factor_prefix_exists l
  6. L14
    specialize beta_sign_factor_prefix_exists e
  7. L15
    apply beta_sign_factor_prefix_exists
  8. L16
    exact hcount
03Separate the logical casesL17–18

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

  1. L17
    cases hsigns_exists
  2. L18
    cases hsigns_exists_witness
04Establish hproduct_existsL19–23

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

  1. L19
    have hproduct_exists : ∃ F. Product(x,x1,l,F)Definitions: Product(x,x1,l,F)Original native command in the exact edition
  2. L20
    specialize beta_product_exists x
  3. L21
    specialize beta_product_exists x1
  4. L22
    specialize beta_product_exists l
  5. L23
    exact beta_product_exists
05Separate the logical casesL24–24

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

  1. L24
    cases hproduct_exists
06Establish hpower_existsL25–28

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

  1. L25
    have hpower_exists : ∃ R. Pow(r,e,R)Definitions: Pow(r,e,R)Original native command in the exact edition
  2. L26
    specialize pow_exists r
  3. L27
    specialize pow_exists e
  4. L28
    exact pow_exists
07Separate the logical casesL29–29

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

  1. L29
    cases hpower_exists
08Establish hequalL30–39

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

  1. L30
    have hequal : x2 = x3
  2. L31
    specialize beta_sign_factor_product_power sb
  3. L32
    specialize beta_sign_factor_product_power sc
  4. L33
    specialize beta_sign_factor_product_power x
  5. L34
    specialize beta_sign_factor_product_power x1
  6. L35
    specialize beta_sign_factor_product_power r
  7. L36
    specialize beta_sign_factor_product_power l
  8. L37
    specialize beta_sign_factor_product_power e
  9. L38
    specialize beta_sign_factor_product_power x2
  10. L39
    specialize beta_sign_factor_product_power x3
09Use earlier factsL40–44

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

  1. L40
    apply beta_sign_factor_product_power
  2. L41
    exact hcount
  3. L42
    exact hsigns_exists_witness_witness
  4. L43
    exact hproduct_exists_witness
  5. L44
    exact hpower_exists_witness
10Construct an explicit witnessL45–48

Supply the displayed value, then prove that it has the required property.

  1. L45
    exists x
  2. L46
    exists x1
  3. L47
    exists x2
  4. L48
    exists x3
11Separate the logical casesL49–49

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

  1. L49
    split
12Use earlier factsL50–50

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

  1. L50
    exact hsigns_exists_witness_witness
13Separate the logical casesL51–51

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

  1. L51
    split
14Use earlier factsL52–52

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

  1. L52
    exact hproduct_exists_witness
15Separate the logical casesL53–53

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

  1. L53
    split
16Use earlier factsL54–55

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

  1. L54
    exact hpower_exists_witness
  2. L55
    exact hequal

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro l
  6. 0006intro e
  7. 0007intro hp
  8. 0008intro hcount
  9. 0009have hsigns_exists : ∃ fb. ∃ fc. ∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)
    Exact native replay linehave hsigns_exists : exists fb fc. (forall gspf_index_recode_endpoint_signs_exists gspf_bit_recode_endpoint_signs_exists. (exists gsp_lt_gap_recode_endpoint_signs_exists_bound. gsp_lt_gap_recode_endpoint_signs_exists_bound + S gspf_index_recode_endpoint_signs_exists = l) -> (((exists ff_h_gspf_recode_endpoint_signs_exists_bit. ff_h_gspf_recode_endpoint_signs_exists_bit + S (gspf_bit_recode_endpoint_signs_exists) = S ((S (gspf_index_recode_endpoint_signs_exists)) * sc)) /\ exists ff_q_gspf_recode_endpoint_signs_exists_bit. sb = ff_q_gspf_recode_endpoint_signs_exists_bit * S ((S (gspf_index_recode_endpoint_signs_exists)) * sc) + (gspf_bit_recode_endpoint_signs_exists))) -> (((gspf_bit_recode_endpoint_signs_exists = 0) /\ (((exists gsp_beta_height_gspf_recode_endpoint_signs_exists_one. gsp_beta_height_gspf_recode_endpoint_signs_exists_one + S (1) = S ((S (gspf_index_recode_endpoint_signs_exists)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_endpoint_signs_exists_one. fb = gsp_beta_quotient_gspf_recode_endpoint_signs_exists_one * S ((S (gspf_index_recode_endpoint_signs_exists)) * fc) + (1)))) \/ ((gspf_bit_recode_endpoint_signs_exists = 1) /\ (((exists ff_h_gspf_recode_endpoint_signs_exists_predecessor. ff_h_gspf_recode_endpoint_signs_exists_predecessor + S (r) = S ((S (gspf_index_recode_endpoint_signs_exists)) * fc)) /\ exists ff_q_gspf_recode_endpoint_signs_exists_predecessor. fb = ff_q_gspf_recode_endpoint_signs_exists_predecessor * S ((S (gspf_index_recode_endpoint_signs_exists)) * fc) + (r))))))
  10. 0010specialize beta_sign_factor_prefix_exists sb
  11. 0011specialize beta_sign_factor_prefix_exists sc
  12. 0012specialize beta_sign_factor_prefix_exists r
  13. 0013specialize beta_sign_factor_prefix_exists l
  14. 0014specialize beta_sign_factor_prefix_exists e
  15. 0015apply beta_sign_factor_prefix_exists
  16. 0016exact hcount
  17. 0017cases hsigns_exists
  18. 0018cases hsigns_exists_witness
  19. 0019have hproduct_exists : ∃ F. Product(x,x1,l,F)
    Exact native replay linehave hproduct_exists : exists F. (exists ff_u_recode_endpoint_product_exists ff_v_recode_endpoint_product_exists. ((((exists ff_h_recode_endpoint_product_exists_start. ff_h_recode_endpoint_product_exists_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_product_exists)) /\ exists ff_q_recode_endpoint_product_exists_start. ff_u_recode_endpoint_product_exists = ff_q_recode_endpoint_product_exists_start * S ((S (0)) * ff_v_recode_endpoint_product_exists) + (1))) /\ ((((exists ff_h_recode_endpoint_product_exists_terminal. ff_h_recode_endpoint_product_exists_terminal + S (F) = S ((S (l)) * ff_v_recode_endpoint_product_exists)) /\ exists ff_q_recode_endpoint_product_exists_terminal. ff_u_recode_endpoint_product_exists = ff_q_recode_endpoint_product_exists_terminal * S ((S (l)) * ff_v_recode_endpoint_product_exists) + (F))) /\ forall ff_i_recode_endpoint_product_exists. (exists ff_lt_recode_endpoint_product_exists_bound. ff_lt_recode_endpoint_product_exists_bound + S ff_i_recode_endpoint_product_exists = l) -> exists ff_p_recode_endpoint_product_exists ff_r_recode_endpoint_product_exists ff_s_recode_endpoint_product_exists. ((((exists ff_h_recode_endpoint_product_exists_factor. ff_h_recode_endpoint_product_exists_factor + S (ff_p_recode_endpoint_product_exists) = S ((S (ff_i_recode_endpoint_product_exists)) * x1)) /\ exists ff_q_recode_endpoint_product_exists_factor. x = ff_q_recode_endpoint_product_exists_factor * S ((S (ff_i_recode_endpoint_product_exists)) * x1) + (ff_p_recode_endpoint_product_exists))) /\ ((((exists ff_h_recode_endpoint_product_exists_partial. ff_h_recode_endpoint_product_exists_partial + S (ff_r_recode_endpoint_product_exists) = S ((S (ff_i_recode_endpoint_product_exists)) * ff_v_recode_endpoint_product_exists)) /\ exists ff_q_recode_endpoint_product_exists_partial. ff_u_recode_endpoint_product_exists = ff_q_recode_endpoint_product_exists_partial * S ((S (ff_i_recode_endpoint_product_exists)) * ff_v_recode_endpoint_product_exists) + (ff_r_recode_endpoint_product_exists))) /\ ((((exists ff_h_recode_endpoint_product_exists_successor. ff_h_recode_endpoint_product_exists_successor + S (ff_s_recode_endpoint_product_exists) = S ((S (S ff_i_recode_endpoint_product_exists)) * ff_v_recode_endpoint_product_exists)) /\ exists ff_q_recode_endpoint_product_exists_successor. ff_u_recode_endpoint_product_exists = ff_q_recode_endpoint_product_exists_successor * S ((S (S ff_i_recode_endpoint_product_exists)) * ff_v_recode_endpoint_product_exists) + (ff_s_recode_endpoint_product_exists))) /\ ff_s_recode_endpoint_product_exists = ff_r_recode_endpoint_product_exists * ff_p_recode_endpoint_product_exists))))))
  20. 0020specialize beta_product_exists x
  21. 0021specialize beta_product_exists x1
  22. 0022specialize beta_product_exists l
  23. 0023exact beta_product_exists
  24. 0024cases hproduct_exists
  25. 0025have hpower_exists : ∃ R. Pow(r,e,R)
    Exact native replay linehave hpower_exists : exists R. (exists ff_b_recode_endpoint_power_exists ff_c_recode_endpoint_power_exists. ((forall ff_i_recode_endpoint_power_exists_repeat. (exists ff_lt_recode_endpoint_power_exists_repeat_bound. ff_lt_recode_endpoint_power_exists_repeat_bound + S ff_i_recode_endpoint_power_exists_repeat = e) -> (((exists ff_h_recode_endpoint_power_exists_repeat_decoded. ff_h_recode_endpoint_power_exists_repeat_decoded + S (r) = S ((S (ff_i_recode_endpoint_power_exists_repeat)) * ff_c_recode_endpoint_power_exists)) /\ exists ff_q_recode_endpoint_power_exists_repeat_decoded. ff_b_recode_endpoint_power_exists = ff_q_recode_endpoint_power_exists_repeat_decoded * S ((S (ff_i_recode_endpoint_power_exists_repeat)) * ff_c_recode_endpoint_power_exists) + (r)))) /\ (exists ff_u_recode_endpoint_power_exists_product ff_v_recode_endpoint_power_exists_product. ((((exists ff_h_recode_endpoint_power_exists_product_start. ff_h_recode_endpoint_power_exists_product_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_power_exists_product)) /\ exists ff_q_recode_endpoint_power_exists_product_start. ff_u_recode_endpoint_power_exists_product = ff_q_recode_endpoint_power_exists_product_start * S ((S (0)) * ff_v_recode_endpoint_power_exists_product) + (1))) /\ ((((exists ff_h_recode_endpoint_power_exists_product_terminal. ff_h_recode_endpoint_power_exists_product_terminal + S (R) = S ((S (e)) * ff_v_recode_endpoint_power_exists_product)) /\ exists ff_q_recode_endpoint_power_exists_product_terminal. ff_u_recode_endpoint_power_exists_product = ff_q_recode_endpoint_power_exists_product_terminal * S ((S (e)) * ff_v_recode_endpoint_power_exists_product) + (R))) /\ forall ff_i_recode_endpoint_power_exists_product. (exists ff_lt_recode_endpoint_power_exists_product_bound. ff_lt_recode_endpoint_power_exists_product_bound + S ff_i_recode_endpoint_power_exists_product = e) -> exists ff_p_recode_endpoint_power_exists_product ff_r_recode_endpoint_power_exists_product ff_s_recode_endpoint_power_exists_product. ((((exists ff_h_recode_endpoint_power_exists_product_factor. ff_h_recode_endpoint_power_exists_product_factor + S (ff_p_recode_endpoint_power_exists_product) = S ((S (ff_i_recode_endpoint_power_exists_product)) * ff_c_recode_endpoint_power_exists)) /\ exists ff_q_recode_endpoint_power_exists_product_factor. ff_b_recode_endpoint_power_exists = ff_q_recode_endpoint_power_exists_product_factor * S ((S (ff_i_recode_endpoint_power_exists_product)) * ff_c_recode_endpoint_power_exists) + (ff_p_recode_endpoint_power_exists_product))) /\ ((((exists ff_h_recode_endpoint_power_exists_product_partial. ff_h_recode_endpoint_power_exists_product_partial + S (ff_r_recode_endpoint_power_exists_product) = S ((S (ff_i_recode_endpoint_power_exists_product)) * ff_v_recode_endpoint_power_exists_product)) /\ exists ff_q_recode_endpoint_power_exists_product_partial. ff_u_recode_endpoint_power_exists_product = ff_q_recode_endpoint_power_exists_product_partial * S ((S (ff_i_recode_endpoint_power_exists_product)) * ff_v_recode_endpoint_power_exists_product) + (ff_r_recode_endpoint_power_exists_product))) /\ ((((exists ff_h_recode_endpoint_power_exists_product_successor. ff_h_recode_endpoint_power_exists_product_successor + S (ff_s_recode_endpoint_power_exists_product) = S ((S (S ff_i_recode_endpoint_power_exists_product)) * ff_v_recode_endpoint_power_exists_product)) /\ exists ff_q_recode_endpoint_power_exists_product_successor. ff_u_recode_endpoint_power_exists_product = ff_q_recode_endpoint_power_exists_product_successor * S ((S (S ff_i_recode_endpoint_power_exists_product)) * ff_v_recode_endpoint_power_exists_product) + (ff_s_recode_endpoint_power_exists_product))) /\ ff_s_recode_endpoint_power_exists_product = ff_r_recode_endpoint_power_exists_product * ff_p_recode_endpoint_power_exists_product))))))))
  26. 0026specialize pow_exists r
  27. 0027specialize pow_exists e
  28. 0028exact pow_exists
  29. 0029cases hpower_exists
  30. 0030have hequal : x2 = x3
  31. 0031specialize beta_sign_factor_product_power sb
  32. 0032specialize beta_sign_factor_product_power sc
  33. 0033specialize beta_sign_factor_product_power x
  34. 0034specialize beta_sign_factor_product_power x1
  35. 0035specialize beta_sign_factor_product_power r
  36. 0036specialize beta_sign_factor_product_power l
  37. 0037specialize beta_sign_factor_product_power e
  38. 0038specialize beta_sign_factor_product_power x2
  39. 0039specialize beta_sign_factor_product_power x3
  40. 0040apply beta_sign_factor_product_power
  41. 0041exact hcount
  42. 0042exact hsigns_exists_witness_witness
  43. 0043exact hproduct_exists_witness
  44. 0044exact hpower_exists_witness
  45. 0045exists x
  46. 0046exists x1
  47. 0047exists x2
  48. 0048exists x3
  49. 0049split
  50. 0050exact hsigns_exists_witness_witness
  51. 0051split
  52. 0052exact hproduct_exists_witness
  53. 0053split
  54. 0054exact hpower_exists_witness
  55. 0055exact hequal