BE0011

binary_modular_execution_horner_exists

Every valid beta-coded binary prefix has a witnessed Horner exponent, complete actual modular execution, and independently proved canonical power invariant.

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. BinaryModulus(m) → BinaryDigitPrefix(b,c,l) → ∃ x. ∃ y. Horner(b,c,2,l,x) ∧ (BinaryModularExecution(b,c,a,m,l,y) ∧ BinaryModularPower(a,x,m,y))

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

Definition DAG

Horner(b,c,x,ell,z) · 1BinaryModulus(m) · 1BinaryModularPower(a,e,m,r) · 1BinaryDigitPrefix(d,s,n) · 1BinaryModularExecution(d,s,a,m,n,r) · 1

Actual proof prerequisites

beta_horner_eval_exists · checked external prerequisitebinary_modular_execution_existsbinary_modular_execution_power_correct
Original expanded first-order statement 
forall b c a m l. (exists ff_modulus_gap_binary_execution_guard. ff_modulus_gap_binary_execution_guard + S 1 = m) -> (forall ff_index_be_prefix ff_digit_be_prefix. (exists ff_lt_be_prefix_bound. ff_lt_be_prefix_bound + S ff_index_be_prefix = l) -> (((exists ff_h_be_prefix_digit. ff_h_be_prefix_digit + S (ff_digit_be_prefix) = S ((S (ff_index_be_prefix)) * c)) /\ exists ff_q_be_prefix_digit. b = ff_q_be_prefix_digit * S ((S (ff_index_be_prefix)) * c) + (ff_digit_be_prefix))) -> (ff_digit_be_prefix = 0 \/ ff_digit_be_prefix = 1)) -> exists e r. ((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)))))) /\ ((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_power_binary_terminal_power. ((exists ff_b_binary_terminal_power_value ff_c_binary_terminal_power_value. ((forall ff_i_binary_terminal_power_value_repeat. (exists ff_lt_binary_terminal_power_value_repeat_bound. ff_lt_binary_terminal_power_value_repeat_bound + S ff_i_binary_terminal_power_value_repeat = e) -> (((exists ff_h_binary_terminal_power_value_repeat_decoded. ff_h_binary_terminal_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_terminal_power_value_repeat)) * ff_c_binary_terminal_power_value)) /\ exists ff_q_binary_terminal_power_value_repeat_decoded. ff_b_binary_terminal_power_value = ff_q_binary_terminal_power_value_repeat_decoded * S ((S (ff_i_binary_terminal_power_value_repeat)) * ff_c_binary_terminal_power_value) + (a)))) /\ (exists ff_u_binary_terminal_power_value_product ff_v_binary_terminal_power_value_product. ((((exists ff_h_binary_terminal_power_value_product_start. ff_h_binary_terminal_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_terminal_power_value_product)) /\ exists ff_q_binary_terminal_power_value_product_start. ff_u_binary_terminal_power_value_product = ff_q_binary_terminal_power_value_product_start * S ((S (0)) * ff_v_binary_terminal_power_value_product) + (1))) /\ ((((exists ff_h_binary_terminal_power_value_product_terminal. ff_h_binary_terminal_power_value_product_terminal + S (ff_power_binary_terminal_power) = S ((S (e)) * ff_v_binary_terminal_power_value_product)) /\ exists ff_q_binary_terminal_power_value_product_terminal. ff_u_binary_terminal_power_value_product = ff_q_binary_terminal_power_value_product_terminal * S ((S (e)) * ff_v_binary_terminal_power_value_product) + (ff_power_binary_terminal_power))) /\ forall ff_i_binary_terminal_power_value_product. (exists ff_lt_binary_terminal_power_value_product_bound. ff_lt_binary_terminal_power_value_product_bound + S ff_i_binary_terminal_power_value_product = e) -> exists ff_p_binary_terminal_power_value_product ff_r_binary_terminal_power_value_product ff_s_binary_terminal_power_value_product. ((((exists ff_h_binary_terminal_power_value_product_factor. ff_h_binary_terminal_power_value_product_factor + S (ff_p_binary_terminal_power_value_product) = S ((S (ff_i_binary_terminal_power_value_product)) * ff_c_binary_terminal_power_value)) /\ exists ff_q_binary_terminal_power_value_product_factor. ff_b_binary_terminal_power_value = ff_q_binary_terminal_power_value_product_factor * S ((S (ff_i_binary_terminal_power_value_product)) * ff_c_binary_terminal_power_value) + (ff_p_binary_terminal_power_value_product))) /\ ((((exists ff_h_binary_terminal_power_value_product_partial. ff_h_binary_terminal_power_value_product_partial + S (ff_r_binary_terminal_power_value_product) = S ((S (ff_i_binary_terminal_power_value_product)) * ff_v_binary_terminal_power_value_product)) /\ exists ff_q_binary_terminal_power_value_product_partial. ff_u_binary_terminal_power_value_product = ff_q_binary_terminal_power_value_product_partial * S ((S (ff_i_binary_terminal_power_value_product)) * ff_v_binary_terminal_power_value_product) + (ff_r_binary_terminal_power_value_product))) /\ ((((exists ff_h_binary_terminal_power_value_product_successor. ff_h_binary_terminal_power_value_product_successor + S (ff_s_binary_terminal_power_value_product) = S ((S (S ff_i_binary_terminal_power_value_product)) * ff_v_binary_terminal_power_value_product)) /\ exists ff_q_binary_terminal_power_value_product_successor. ff_u_binary_terminal_power_value_product = ff_q_binary_terminal_power_value_product_successor * S ((S (S ff_i_binary_terminal_power_value_product)) * ff_v_binary_terminal_power_value_product) + (ff_s_binary_terminal_power_value_product))) /\ ff_s_binary_terminal_power_value_product = ff_r_binary_terminal_power_value_product * ff_p_binary_terminal_power_value_product)))))))) /\ (((exists ff_gap_binary_terminal_power_residue. ff_gap_binary_terminal_power_residue + S (r) = m) /\ (exists ff_left_binary_terminal_power_residue_congruence ff_right_binary_terminal_power_residue_congruence. (ff_power_binary_terminal_power) + m * ff_left_binary_terminal_power_residue_congruence = (r) + m * ff_right_binary_terminal_power_residue_congruence)))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

41 script commands · 11 reading checkpoints · 2 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 (2)
binary modular execution existsbinary 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–7

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 hmodulus
  7. L7
    intro hdigits
02Establish hhornerL8–13

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

  1. L8
    have hhorner : ∃ e. Horner(b,c,2,l,e)Definitions: HornerOriginal native command in the exact edition
  2. L9
    specialize beta_horner_eval_exists b
  3. L10
    specialize beta_horner_eval_exists c
  4. L11
    specialize beta_horner_eval_exists 2
  5. L12
    specialize beta_horner_eval_exists l
  6. L13
    exact beta_horner_eval_exists
03Separate the logical casesL14–14

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

  1. L14
    cases hhorner
04Establish hexecutionL15–23

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

  1. L15
    have hexecution : ∃ r. BinaryModularExecution(b,c,a,m,l,r)Definitions: BinaryModularExecutionOriginal native command in the exact edition
  2. L16
    specialize binary_modular_execution_exists b
  3. L17
    specialize binary_modular_execution_exists c
  4. L18
    specialize binary_modular_execution_exists a
  5. L19
    specialize binary_modular_execution_exists m
  6. L20
    specialize binary_modular_execution_exists l
  7. L21
    apply binary_modular_execution_exists
  8. L22
    exact hmodulus
  9. L23
    exact hdigits
05Separate the logical casesL24–24

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

  1. L24
    cases hexecution
06Construct an explicit witnessL25–26

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

  1. L25
    exists x
  2. L26
    exists x1
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–28

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

  1. L28
    exact hhorner_witness
09Separate the logical casesL29–29

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

  1. L29
    split
10Use earlier factsL30–39

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

  1. L30
    exact hexecution_witness
  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 x1
  9. L38
    apply binary_modular_execution_power_correct
  10. L39
    exact hmodulus
11Use earlier factsL40–41

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

  1. L40
    exact hhorner_witness
  2. L41
    exact hexecution_witness

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro hmodulus
  7. 0007intro hdigits
  8. 0008have 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))))))
  9. 0009specialize beta_horner_eval_exists b
  10. 0010specialize beta_horner_eval_exists c
  11. 0011specialize beta_horner_eval_exists 2
  12. 0012specialize beta_horner_eval_exists l
  13. 0013exact beta_horner_eval_exists
  14. 0014cases hhorner
  15. 0015have hexecution : exists r. (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)))))
  16. 0016specialize binary_modular_execution_exists b
  17. 0017specialize binary_modular_execution_exists c
  18. 0018specialize binary_modular_execution_exists a
  19. 0019specialize binary_modular_execution_exists m
  20. 0020specialize binary_modular_execution_exists l
  21. 0021apply binary_modular_execution_exists
  22. 0022exact hmodulus
  23. 0023exact hdigits
  24. 0024cases hexecution
  25. 0025exists x
  26. 0026exists x1
  27. 0027split
  28. 0028exact hhorner_witness
  29. 0029split
  30. 0030exact hexecution_witness
  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 x1
  38. 0038apply binary_modular_execution_power_correct
  39. 0039exact hmodulus
  40. 0040exact hhorner_witness
  41. 0041exact hexecution_witness