BE0012

binary_modular_execution_result_functional

Any two complete actual coded square-and-multiply executions of the same guarded binary prefix have identical terminal residues.

Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not Stable

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.

G102 was OPEN at this family's Alpha-v22 first admission: complete execution was proved only for a supplied valid beta-coded digit prefix. G102 is now CLOSED in Alpha v23 for every arbitrary exponent, with actual canonical digits and operations≤3*BitLen(e)+2.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ a. ∀ m. ∀ l. ∀ r. ∀ s. BinaryModulus(m) → BinaryModularExecution(b,c,a,m,l,r) → BinaryModularExecution(b,c,a,m,l,s) → r = s

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BinaryModulus(m) · 1BinaryModularExecution(d,s,a,m,n,r) · 2

Actual proof prerequisites

beta_horner_eval_exists · checked external prerequisitebinary_modular_execution_power_correctbinary_modular_exponentiation_result_functional · checked external prerequisite
Original expanded first-order statement 
forall b c a m l r s. (exists ff_modulus_gap_binary_execution_guard. ff_modulus_gap_binary_execution_guard + S 1 = m) -> (exists ff_trace_code_be_execution ff_trace_scale_be_execution. ((((((exists ff_h_be_execution_trace_start. ff_h_be_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_start. ff_trace_code_be_execution = ff_q_be_execution_trace_start * S ((S (0)) * ff_trace_scale_be_execution) + (1))) /\ forall ff_index_be_execution_trace. (exists ff_lt_be_execution_trace_bound. ff_lt_be_execution_trace_bound + S ff_index_be_execution_trace = l) -> exists ff_digit_be_execution_trace ff_previous_be_execution_trace ff_current_be_execution_trace. ((((exists ff_h_be_execution_trace_source. ff_h_be_execution_trace_source + S (ff_digit_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * c)) /\ exists ff_q_be_execution_trace_source. b = ff_q_be_execution_trace_source * S ((S (ff_index_be_execution_trace)) * c) + (ff_digit_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_before. ff_h_be_execution_trace_before + S (ff_previous_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_before. ff_trace_code_be_execution = ff_q_be_execution_trace_before * S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_previous_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_after. ff_h_be_execution_trace_after + S (ff_current_be_execution_trace) = S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_after. ff_trace_code_be_execution = ff_q_be_execution_trace_after * S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_current_be_execution_trace))) /\ ((((ff_digit_be_execution_trace = 0) /\ (((exists ff_gap_binary_be_execution_trace_transition_square. ff_gap_binary_be_execution_trace_transition_square + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_square_congruence ff_right_binary_be_execution_trace_transition_square_congruence. (ff_previous_be_execution_trace * ff_previous_be_execution_trace) + m * ff_left_binary_be_execution_trace_transition_square_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_execution_trace = 1) /\ (((exists ff_gap_binary_be_execution_trace_transition_multiply. ff_gap_binary_be_execution_trace_transition_multiply + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_multiply_congruence ff_right_binary_be_execution_trace_transition_multiply_congruence. ((ff_previous_be_execution_trace * ff_previous_be_execution_trace) * a) + m * ff_left_binary_be_execution_trace_transition_multiply_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_execution_terminal. ff_h_be_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_terminal. ff_trace_code_be_execution = ff_q_be_execution_terminal * S ((S (l)) * ff_trace_scale_be_execution) + (r))))) -> (exists ff_trace_code_be_other_execution ff_trace_scale_be_other_execution. ((((((exists ff_h_be_other_execution_trace_start. ff_h_be_other_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_start. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_start * S ((S (0)) * ff_trace_scale_be_other_execution) + (1))) /\ forall ff_index_be_other_execution_trace. (exists ff_lt_be_other_execution_trace_bound. ff_lt_be_other_execution_trace_bound + S ff_index_be_other_execution_trace = l) -> exists ff_digit_be_other_execution_trace ff_previous_be_other_execution_trace ff_current_be_other_execution_trace. ((((exists ff_h_be_other_execution_trace_source. ff_h_be_other_execution_trace_source + S (ff_digit_be_other_execution_trace) = S ((S (ff_index_be_other_execution_trace)) * c)) /\ exists ff_q_be_other_execution_trace_source. b = ff_q_be_other_execution_trace_source * S ((S (ff_index_be_other_execution_trace)) * c) + (ff_digit_be_other_execution_trace))) /\ ((((exists ff_h_be_other_execution_trace_before. ff_h_be_other_execution_trace_before + S (ff_previous_be_other_execution_trace) = S ((S (ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_before. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_before * S ((S (ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution) + (ff_previous_be_other_execution_trace))) /\ ((((exists ff_h_be_other_execution_trace_after. ff_h_be_other_execution_trace_after + S (ff_current_be_other_execution_trace) = S ((S (S ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_after. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_after * S ((S (S ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution) + (ff_current_be_other_execution_trace))) /\ ((((ff_digit_be_other_execution_trace = 0) /\ (((exists ff_gap_binary_be_other_execution_trace_transition_square. ff_gap_binary_be_other_execution_trace_transition_square + S (ff_current_be_other_execution_trace) = m) /\ (exists ff_left_binary_be_other_execution_trace_transition_square_congruence ff_right_binary_be_other_execution_trace_transition_square_congruence. (ff_previous_be_other_execution_trace * ff_previous_be_other_execution_trace) + m * ff_left_binary_be_other_execution_trace_transition_square_congruence = (ff_current_be_other_execution_trace) + m * ff_right_binary_be_other_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_other_execution_trace = 1) /\ (((exists ff_gap_binary_be_other_execution_trace_transition_multiply. ff_gap_binary_be_other_execution_trace_transition_multiply + S (ff_current_be_other_execution_trace) = m) /\ (exists ff_left_binary_be_other_execution_trace_transition_multiply_congruence ff_right_binary_be_other_execution_trace_transition_multiply_congruence. ((ff_previous_be_other_execution_trace * ff_previous_be_other_execution_trace) * a) + m * ff_left_binary_be_other_execution_trace_transition_multiply_congruence = (ff_current_be_other_execution_trace) + m * ff_right_binary_be_other_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_other_execution_terminal. ff_h_be_other_execution_terminal + S (s) = S ((S (l)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_terminal. ff_trace_code_be_other_execution = ff_q_be_other_execution_terminal * S ((S (l)) * ff_trace_scale_be_other_execution) + (s))))) -> r = s

Complete unchanged native tactic proof

All 49 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

49 script commands · 7 reading checkpoints · 3 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 (1)
binary modular execution power correct

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro m
  5. L5
    intro l
  6. L6
    intro r
  7. L7
    intro s
  8. L8
    intro hmodulus
  9. L9
    intro hleft
  10. L10
    intro hright
02Establish hhornerL11–16

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

  1. L11
    have hhorner : ∃ e. Horner(b,c,2,l,e)Definitions: HornerOriginal native command in the exact edition
  2. L12
    specialize beta_horner_eval_exists b
  3. L13
    specialize beta_horner_eval_exists c
  4. L14
    specialize beta_horner_eval_exists 2
  5. L15
    specialize beta_horner_eval_exists l
  6. L16
    exact beta_horner_eval_exists
03Separate the logical casesL17–17

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

  1. L17
    cases hhorner
04Establish hfirstL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modular execution power correct.

  1. L18
    have hfirst : BinaryModularPower(a,x,m,r)Definitions: BinaryModularPowerOriginal native command in the exact edition
  2. L19
    specialize binary_modular_execution_power_correct b
  3. L20
    specialize binary_modular_execution_power_correct c
  4. L21
    specialize binary_modular_execution_power_correct a
  5. L22
    specialize binary_modular_execution_power_correct m
  6. L23
    specialize binary_modular_execution_power_correct l
  7. L24
    specialize binary_modular_execution_power_correct x
  8. L25
    specialize binary_modular_execution_power_correct r
  9. L26
    apply binary_modular_execution_power_correct
  10. L27
    exact hmodulus
05Use earlier factsL28–29

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

  1. L28
    exact hhorner_witness
  2. L29
    exact hleft
06Establish hsecondL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modular execution power correct.

  1. L30
    have hsecond : BinaryModularPower(a,x,m,s)Definitions: BinaryModularPowerOriginal native command in the exact edition
  2. L31
    specialize binary_modular_execution_power_correct b
  3. L32
    specialize binary_modular_execution_power_correct c
  4. L33
    specialize binary_modular_execution_power_correct a
  5. L34
    specialize binary_modular_execution_power_correct m
  6. L35
    specialize binary_modular_execution_power_correct l
  7. L36
    specialize binary_modular_execution_power_correct x
  8. L37
    specialize binary_modular_execution_power_correct s
  9. L38
    apply binary_modular_execution_power_correct
  10. L39
    exact hmodulus
07Use earlier factsL40–49

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

  1. L40
    exact hhorner_witness
  2. L41
    exact hright
  3. L42
    specialize binary_modular_exponentiation_result_functional a
  4. L43
    specialize binary_modular_exponentiation_result_functional x
  5. L44
    specialize binary_modular_exponentiation_result_functional m
  6. L45
    specialize binary_modular_exponentiation_result_functional r
  7. L46
    specialize binary_modular_exponentiation_result_functional s
  8. L47
    apply binary_modular_exponentiation_result_functional
  9. L48
    exact hfirst
  10. L49
    exact hsecond

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro r
  7. 0007intro s
  8. 0008intro hmodulus
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011have hhorner : exists e. (exists ff_u_ph_be_exponent ff_v_ph_be_exponent. ((((exists fs_h_ph_be_exponent_body_start. fs_h_ph_be_exponent_body_start + S (0) = S ((S (0)) * ff_v_ph_be_exponent)) /\ exists fs_q_ph_be_exponent_body_start. ff_u_ph_be_exponent = fs_q_ph_be_exponent_body_start * S ((S (0)) * ff_v_ph_be_exponent) + (0))) /\ ((((exists fs_h_ph_be_exponent_body_terminal. fs_h_ph_be_exponent_body_terminal + S (e) = S ((S (l)) * ff_v_ph_be_exponent)) /\ exists fs_q_ph_be_exponent_body_terminal. ff_u_ph_be_exponent = fs_q_ph_be_exponent_body_terminal * S ((S (l)) * ff_v_ph_be_exponent) + (e))) /\ forall ff_i_ph_be_exponent_body_steps. (exists ph_bound_be_exponent_body_steps. ph_bound_be_exponent_body_steps + S ff_i_ph_be_exponent_body_steps = l) -> exists ff_coefficient_ph_be_exponent_body_steps ff_previous_ph_be_exponent_body_steps ff_current_ph_be_exponent_body_steps. ((((exists fs_h_ph_be_exponent_body_steps_coefficient. fs_h_ph_be_exponent_body_steps_coefficient + S (ff_coefficient_ph_be_exponent_body_steps) = S ((S (ff_i_ph_be_exponent_body_steps)) * c)) /\ exists fs_q_ph_be_exponent_body_steps_coefficient. b = fs_q_ph_be_exponent_body_steps_coefficient * S ((S (ff_i_ph_be_exponent_body_steps)) * c) + (ff_coefficient_ph_be_exponent_body_steps))) /\ ((((exists fs_h_ph_be_exponent_body_steps_before. fs_h_ph_be_exponent_body_steps_before + S (ff_previous_ph_be_exponent_body_steps) = S ((S (ff_i_ph_be_exponent_body_steps)) * ff_v_ph_be_exponent)) /\ exists fs_q_ph_be_exponent_body_steps_before. ff_u_ph_be_exponent = fs_q_ph_be_exponent_body_steps_before * S ((S (ff_i_ph_be_exponent_body_steps)) * ff_v_ph_be_exponent) + (ff_previous_ph_be_exponent_body_steps))) /\ ((((exists fs_h_ph_be_exponent_body_steps_after. fs_h_ph_be_exponent_body_steps_after + S (ff_current_ph_be_exponent_body_steps) = S ((S (S ff_i_ph_be_exponent_body_steps)) * ff_v_ph_be_exponent)) /\ exists fs_q_ph_be_exponent_body_steps_after. ff_u_ph_be_exponent = fs_q_ph_be_exponent_body_steps_after * S ((S (S ff_i_ph_be_exponent_body_steps)) * ff_v_ph_be_exponent) + (ff_current_ph_be_exponent_body_steps))) /\ ff_current_ph_be_exponent_body_steps = ff_previous_ph_be_exponent_body_steps * 2 + ff_coefficient_ph_be_exponent_body_steps))))))
  12. 0012specialize beta_horner_eval_exists b
  13. 0013specialize beta_horner_eval_exists c
  14. 0014specialize beta_horner_eval_exists 2
  15. 0015specialize beta_horner_eval_exists l
  16. 0016exact beta_horner_eval_exists
  17. 0017cases hhorner
  18. 0018have hfirst : (exists ff_power_binary_functional_left. ((exists ff_b_binary_functional_left_value ff_c_binary_functional_left_value. ((forall ff_i_binary_functional_left_value_repeat. (exists ff_lt_binary_functional_left_value_repeat_bound. ff_lt_binary_functional_left_value_repeat_bound + S ff_i_binary_functional_left_value_repeat = x) -> (((exists ff_h_binary_functional_left_value_repeat_decoded. ff_h_binary_functional_left_value_repeat_decoded + S (a) = S ((S (ff_i_binary_functional_left_value_repeat)) * ff_c_binary_functional_left_value)) /\ exists ff_q_binary_functional_left_value_repeat_decoded. ff_b_binary_functional_left_value = ff_q_binary_functional_left_value_repeat_decoded * S ((S (ff_i_binary_functional_left_value_repeat)) * ff_c_binary_functional_left_value) + (a)))) /\ (exists ff_u_binary_functional_left_value_product ff_v_binary_functional_left_value_product. ((((exists ff_h_binary_functional_left_value_product_start. ff_h_binary_functional_left_value_product_start + S (1) = S ((S (0)) * ff_v_binary_functional_left_value_product)) /\ exists ff_q_binary_functional_left_value_product_start. ff_u_binary_functional_left_value_product = ff_q_binary_functional_left_value_product_start * S ((S (0)) * ff_v_binary_functional_left_value_product) + (1))) /\ ((((exists ff_h_binary_functional_left_value_product_terminal. ff_h_binary_functional_left_value_product_terminal + S (ff_power_binary_functional_left) = S ((S (x)) * ff_v_binary_functional_left_value_product)) /\ exists ff_q_binary_functional_left_value_product_terminal. ff_u_binary_functional_left_value_product = ff_q_binary_functional_left_value_product_terminal * S ((S (x)) * ff_v_binary_functional_left_value_product) + (ff_power_binary_functional_left))) /\ forall ff_i_binary_functional_left_value_product. (exists ff_lt_binary_functional_left_value_product_bound. ff_lt_binary_functional_left_value_product_bound + S ff_i_binary_functional_left_value_product = x) -> exists ff_p_binary_functional_left_value_product ff_r_binary_functional_left_value_product ff_s_binary_functional_left_value_product. ((((exists ff_h_binary_functional_left_value_product_factor. ff_h_binary_functional_left_value_product_factor + S (ff_p_binary_functional_left_value_product) = S ((S (ff_i_binary_functional_left_value_product)) * ff_c_binary_functional_left_value)) /\ exists ff_q_binary_functional_left_value_product_factor. ff_b_binary_functional_left_value = ff_q_binary_functional_left_value_product_factor * S ((S (ff_i_binary_functional_left_value_product)) * ff_c_binary_functional_left_value) + (ff_p_binary_functional_left_value_product))) /\ ((((exists ff_h_binary_functional_left_value_product_partial. ff_h_binary_functional_left_value_product_partial + S (ff_r_binary_functional_left_value_product) = S ((S (ff_i_binary_functional_left_value_product)) * ff_v_binary_functional_left_value_product)) /\ exists ff_q_binary_functional_left_value_product_partial. ff_u_binary_functional_left_value_product = ff_q_binary_functional_left_value_product_partial * S ((S (ff_i_binary_functional_left_value_product)) * ff_v_binary_functional_left_value_product) + (ff_r_binary_functional_left_value_product))) /\ ((((exists ff_h_binary_functional_left_value_product_successor. ff_h_binary_functional_left_value_product_successor + S (ff_s_binary_functional_left_value_product) = S ((S (S ff_i_binary_functional_left_value_product)) * ff_v_binary_functional_left_value_product)) /\ exists ff_q_binary_functional_left_value_product_successor. ff_u_binary_functional_left_value_product = ff_q_binary_functional_left_value_product_successor * S ((S (S ff_i_binary_functional_left_value_product)) * ff_v_binary_functional_left_value_product) + (ff_s_binary_functional_left_value_product))) /\ ff_s_binary_functional_left_value_product = ff_r_binary_functional_left_value_product * ff_p_binary_functional_left_value_product)))))))) /\ (((exists ff_gap_binary_functional_left_residue. ff_gap_binary_functional_left_residue + S (r) = m) /\ (exists ff_left_binary_functional_left_residue_congruence ff_right_binary_functional_left_residue_congruence. (ff_power_binary_functional_left) + m * ff_left_binary_functional_left_residue_congruence = (r) + m * ff_right_binary_functional_left_residue_congruence)))))
  19. 0019specialize binary_modular_execution_power_correct b
  20. 0020specialize binary_modular_execution_power_correct c
  21. 0021specialize binary_modular_execution_power_correct a
  22. 0022specialize binary_modular_execution_power_correct m
  23. 0023specialize binary_modular_execution_power_correct l
  24. 0024specialize binary_modular_execution_power_correct x
  25. 0025specialize binary_modular_execution_power_correct r
  26. 0026apply binary_modular_execution_power_correct
  27. 0027exact hmodulus
  28. 0028exact hhorner_witness
  29. 0029exact hleft
  30. 0030have hsecond : (exists ff_power_binary_functional_right. ((exists ff_b_binary_functional_right_value ff_c_binary_functional_right_value. ((forall ff_i_binary_functional_right_value_repeat. (exists ff_lt_binary_functional_right_value_repeat_bound. ff_lt_binary_functional_right_value_repeat_bound + S ff_i_binary_functional_right_value_repeat = x) -> (((exists ff_h_binary_functional_right_value_repeat_decoded. ff_h_binary_functional_right_value_repeat_decoded + S (a) = S ((S (ff_i_binary_functional_right_value_repeat)) * ff_c_binary_functional_right_value)) /\ exists ff_q_binary_functional_right_value_repeat_decoded. ff_b_binary_functional_right_value = ff_q_binary_functional_right_value_repeat_decoded * S ((S (ff_i_binary_functional_right_value_repeat)) * ff_c_binary_functional_right_value) + (a)))) /\ (exists ff_u_binary_functional_right_value_product ff_v_binary_functional_right_value_product. ((((exists ff_h_binary_functional_right_value_product_start. ff_h_binary_functional_right_value_product_start + S (1) = S ((S (0)) * ff_v_binary_functional_right_value_product)) /\ exists ff_q_binary_functional_right_value_product_start. ff_u_binary_functional_right_value_product = ff_q_binary_functional_right_value_product_start * S ((S (0)) * ff_v_binary_functional_right_value_product) + (1))) /\ ((((exists ff_h_binary_functional_right_value_product_terminal. ff_h_binary_functional_right_value_product_terminal + S (ff_power_binary_functional_right) = S ((S (x)) * ff_v_binary_functional_right_value_product)) /\ exists ff_q_binary_functional_right_value_product_terminal. ff_u_binary_functional_right_value_product = ff_q_binary_functional_right_value_product_terminal * S ((S (x)) * ff_v_binary_functional_right_value_product) + (ff_power_binary_functional_right))) /\ forall ff_i_binary_functional_right_value_product. (exists ff_lt_binary_functional_right_value_product_bound. ff_lt_binary_functional_right_value_product_bound + S ff_i_binary_functional_right_value_product = x) -> exists ff_p_binary_functional_right_value_product ff_r_binary_functional_right_value_product ff_s_binary_functional_right_value_product. ((((exists ff_h_binary_functional_right_value_product_factor. ff_h_binary_functional_right_value_product_factor + S (ff_p_binary_functional_right_value_product) = S ((S (ff_i_binary_functional_right_value_product)) * ff_c_binary_functional_right_value)) /\ exists ff_q_binary_functional_right_value_product_factor. ff_b_binary_functional_right_value = ff_q_binary_functional_right_value_product_factor * S ((S (ff_i_binary_functional_right_value_product)) * ff_c_binary_functional_right_value) + (ff_p_binary_functional_right_value_product))) /\ ((((exists ff_h_binary_functional_right_value_product_partial. ff_h_binary_functional_right_value_product_partial + S (ff_r_binary_functional_right_value_product) = S ((S (ff_i_binary_functional_right_value_product)) * ff_v_binary_functional_right_value_product)) /\ exists ff_q_binary_functional_right_value_product_partial. ff_u_binary_functional_right_value_product = ff_q_binary_functional_right_value_product_partial * S ((S (ff_i_binary_functional_right_value_product)) * ff_v_binary_functional_right_value_product) + (ff_r_binary_functional_right_value_product))) /\ ((((exists ff_h_binary_functional_right_value_product_successor. ff_h_binary_functional_right_value_product_successor + S (ff_s_binary_functional_right_value_product) = S ((S (S ff_i_binary_functional_right_value_product)) * ff_v_binary_functional_right_value_product)) /\ exists ff_q_binary_functional_right_value_product_successor. ff_u_binary_functional_right_value_product = ff_q_binary_functional_right_value_product_successor * S ((S (S ff_i_binary_functional_right_value_product)) * ff_v_binary_functional_right_value_product) + (ff_s_binary_functional_right_value_product))) /\ ff_s_binary_functional_right_value_product = ff_r_binary_functional_right_value_product * ff_p_binary_functional_right_value_product)))))))) /\ (((exists ff_gap_binary_functional_right_residue. ff_gap_binary_functional_right_residue + S (s) = m) /\ (exists ff_left_binary_functional_right_residue_congruence ff_right_binary_functional_right_residue_congruence. (ff_power_binary_functional_right) + m * ff_left_binary_functional_right_residue_congruence = (s) + m * ff_right_binary_functional_right_residue_congruence)))))
  31. 0031specialize binary_modular_execution_power_correct b
  32. 0032specialize binary_modular_execution_power_correct c
  33. 0033specialize binary_modular_execution_power_correct a
  34. 0034specialize binary_modular_execution_power_correct m
  35. 0035specialize binary_modular_execution_power_correct l
  36. 0036specialize binary_modular_execution_power_correct x
  37. 0037specialize binary_modular_execution_power_correct s
  38. 0038apply binary_modular_execution_power_correct
  39. 0039exact hmodulus
  40. 0040exact hhorner_witness
  41. 0041exact hright
  42. 0042specialize binary_modular_exponentiation_result_functional a
  43. 0043specialize binary_modular_exponentiation_result_functional x
  44. 0044specialize binary_modular_exponentiation_result_functional m
  45. 0045specialize binary_modular_exponentiation_result_functional r
  46. 0046specialize binary_modular_exponentiation_result_functional s
  47. 0047apply binary_modular_exponentiation_result_functional
  48. 0048exact hfirst
  49. 0049exact hsecond