BE0010

binary_modular_execution_power_correct

Every genuine coded square-and-multiply execution is the canonical modular power of the exact base-two Horner exponent represented by its digit prefix.

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. ∀ e. ∀ r. BinaryModulus(m) → Horner(b,c,2,l,e) → BinaryModularExecution(b,c,a,m,l,r) → BinaryModularPower(a,e,m,r)

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) · 1BinaryModularExecution(d,s,a,m,n,r) · 1

Actual proof prerequisites

beta_horner_eval_empty · checked external prerequisitebinary_modular_execution_emptybinary_execution_power_zerobeta_horner_eval_successor_decompose · checked external prerequisitebinary_modular_execution_successor_decomposebeta_at_unique · checked external prerequisitebinary_execution_step_digitbinary_execution_horner_digit_splitbinary_execution_step_power_invariant
Original expanded first-order statement 
forall b c a m l e r. (exists ff_modulus_gap_binary_execution_guard. ff_modulus_gap_binary_execution_guard + S 1 = m) -> (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 106 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

106 script commands · 15 reading checkpoints · 8 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 (6)
binary modular execution emptybinary execution power zerobinary modular execution successor decomposebinary execution step digitbinary execution horner digit splitbinary execution step power invariant

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–4

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
02Induction on lL5–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction l
  2. L6
    intro e
  3. L7
    intro r
  4. L8
    intro hmodulus
  5. L9
    intro hhorner
  6. L10
    intro hexecution
03Establish hzeroL11–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval empty.

  1. L11
    have hzero : e = 0
  2. L12
    specialize beta_horner_eval_empty b
  3. L13
    specialize beta_horner_eval_empty c
  4. L14
    specialize beta_horner_eval_empty 2
  5. L15
    specialize beta_horner_eval_empty e
  6. L16
    apply beta_horner_eval_empty
  7. L17
    exact hhorner
04Establish honeL18–27

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

  1. L18
    have hone : r = 1
  2. L19
    specialize binary_modular_execution_empty b
  3. L20
    specialize binary_modular_execution_empty c
  4. L21
    specialize binary_modular_execution_empty a
  5. L22
    specialize binary_modular_execution_empty m
  6. L23
    specialize binary_modular_execution_empty r
  7. L24
    apply binary_modular_execution_empty
  8. L25
    exact hexecution
  9. L26
    specialize binary_execution_power_zero a
  10. L27
    specialize binary_execution_power_zero e
05Use earlier factsL28–33

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

  1. L28
    specialize binary_execution_power_zero m
  2. L29
    specialize binary_execution_power_zero r
  3. L30
    apply binary_execution_power_zero
  4. L31
    exact hmodulus
  5. L32
    exact hzero
  6. L33
    exact hone
06Fix variables and assumptionsL34–38

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

  1. L34
    intro e
  2. L35
    intro r
  3. L36
    intro hmodulus
  4. L37
    intro hhorner
  5. L38
    intro hexecution
07Establish hhstepL39–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval successor decompose.

  1. L39
    have hhstep : ∃ digit. ∃ half. Beta(b,c,l,digit) ∧ (Horner(b,c,2,l,half) ∧ e = half · 2 + digit)Definitions: BetaHornerOriginal native command in the exact edition
  2. L40
    specialize beta_horner_eval_successor_decompose b
  3. L41
    specialize beta_horner_eval_successor_decompose c
  4. L42
    specialize beta_horner_eval_successor_decompose 2
  5. L43
    specialize beta_horner_eval_successor_decompose l
  6. L44
    specialize beta_horner_eval_successor_decompose e
  7. L45
    apply beta_horner_eval_successor_decompose
  8. L46
    exact hhorner
08Separate the logical casesL47–50

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

  1. L47
    cases hhstep
  2. L48
    cases hhstep_witness
  3. L49
    cases hhstep_witness_witness
  4. L50
    cases hhstep_witness_witness_right
09Establish hxstepL51–59

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

  1. L51
    have hxstep : ∃ digit. ∃ previous. Beta(b,c,l,digit) ∧ (BinaryModularExecution(b,c,a,m,l,previous) ∧ BinaryModularStep(m,previous,a,digit,r))Definitions: BetaBinaryModularStepBinaryModularExecutionOriginal native command in the exact edition
  2. L52
    specialize binary_modular_execution_successor_decompose b
  3. L53
    specialize binary_modular_execution_successor_decompose c
  4. L54
    specialize binary_modular_execution_successor_decompose a
  5. L55
    specialize binary_modular_execution_successor_decompose m
  6. L56
    specialize binary_modular_execution_successor_decompose l
  7. L57
    specialize binary_modular_execution_successor_decompose r
  8. L58
    apply binary_modular_execution_successor_decompose
  9. L59
    exact hexecution
10Separate the logical casesL60–63

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

  1. L60
    cases hxstep
  2. L61
    cases hxstep_witness
  3. L62
    cases hxstep_witness_witness
  4. L63
    cases hxstep_witness_witness_right
11Establish hdigitL64–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L64
    have hdigit : x = x2
  2. L65
    specialize beta_at_unique b
  3. L66
    specialize beta_at_unique c
  4. L67
    specialize beta_at_unique l
  5. L68
    specialize beta_at_unique x
  6. L69
    specialize beta_at_unique x2
  7. L70
    apply beta_at_unique
  8. L71
    exact hhstep_witness_witness_left
  9. L72
    exact hxstep_witness_witness_left
  10. L73
    rewrite hdigit at hhstep_witness_witness_right_right
12Establish hbitL74–81

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

  1. L74
    have hbit : x2 = 0 \/ x2 = 1
  2. L75
    specialize binary_execution_step_digit m
  3. L76
    specialize binary_execution_step_digit x3
  4. L77
    specialize binary_execution_step_digit a
  5. L78
    specialize binary_execution_step_digit x2
  6. L79
    specialize binary_execution_step_digit r
  7. L80
    apply binary_execution_step_digit
  8. L81
    exact hxstep_witness_witness_right_right
13Establish hsplitL82–88

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

  1. L82
    have hsplit : ((((x2 = 0) \/ (x2 = 1)) /\ e = (x1 + x1) + x2))
  2. L83
    specialize binary_execution_horner_digit_split x1
  3. L84
    specialize binary_execution_horner_digit_split e
  4. L85
    specialize binary_execution_horner_digit_split x2
  5. L86
    apply binary_execution_horner_digit_split
  6. L87
    exact hbit
  7. L88
    exact hhstep_witness_witness_right_right
14Establish hpreviousL89–98

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L89
    have hprevious : BinaryModularPower(a,x1,m,x3)Definitions: BinaryModularPowerOriginal native command in the exact edition
  2. L90
    specialize IH x1
  3. L91
    specialize IH x3
  4. L92
    apply IH
  5. L93
    exact hmodulus
  6. L94
    exact hhstep_witness_witness_right_left
  7. L95
    exact hxstep_witness_witness_right_left
  8. L96
    specialize binary_execution_step_power_invariant a
  9. L97
    specialize binary_execution_step_power_invariant x1
  10. L98
    specialize binary_execution_step_power_invariant e
15Use earlier factsL99–106

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

  1. L99
    specialize binary_execution_step_power_invariant m
  2. L100
    specialize binary_execution_step_power_invariant x3
  3. L101
    specialize binary_execution_step_power_invariant x2
  4. L102
    specialize binary_execution_step_power_invariant r
  5. L103
    apply binary_execution_step_power_invariant
  6. L104
    exact hprevious
  7. L105
    exact hsplit
  8. L106
    exact hxstep_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 106 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005induction l
  6. 0006intro e
  7. 0007intro r
  8. 0008intro hmodulus
  9. 0009intro hhorner
  10. 0010intro hexecution
  11. 0011have hzero : e = 0
  12. 0012specialize beta_horner_eval_empty b
  13. 0013specialize beta_horner_eval_empty c
  14. 0014specialize beta_horner_eval_empty 2
  15. 0015specialize beta_horner_eval_empty e
  16. 0016apply beta_horner_eval_empty
  17. 0017exact hhorner
  18. 0018have hone : r = 1
  19. 0019specialize binary_modular_execution_empty b
  20. 0020specialize binary_modular_execution_empty c
  21. 0021specialize binary_modular_execution_empty a
  22. 0022specialize binary_modular_execution_empty m
  23. 0023specialize binary_modular_execution_empty r
  24. 0024apply binary_modular_execution_empty
  25. 0025exact hexecution
  26. 0026specialize binary_execution_power_zero a
  27. 0027specialize binary_execution_power_zero e
  28. 0028specialize binary_execution_power_zero m
  29. 0029specialize binary_execution_power_zero r
  30. 0030apply binary_execution_power_zero
  31. 0031exact hmodulus
  32. 0032exact hzero
  33. 0033exact hone
  34. 0034intro e
  35. 0035intro r
  36. 0036intro hmodulus
  37. 0037intro hhorner
  38. 0038intro hexecution
  39. 0039have hhstep : exists digit half. ((((exists ff_h_be_power_horner_digit. ff_h_be_power_horner_digit + S (digit) = S ((S (l)) * c)) /\ exists ff_q_be_power_horner_digit. b = ff_q_be_power_horner_digit * S ((S (l)) * c) + (digit))) /\ ((exists ff_u_ph_be_power_horner_prefix ff_v_ph_be_power_horner_prefix. ((((exists fs_h_ph_be_power_horner_prefix_body_start. fs_h_ph_be_power_horner_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_be_power_horner_prefix)) /\ exists fs_q_ph_be_power_horner_prefix_body_start. ff_u_ph_be_power_horner_prefix = fs_q_ph_be_power_horner_prefix_body_start * S ((S (0)) * ff_v_ph_be_power_horner_prefix) + (0))) /\ ((((exists fs_h_ph_be_power_horner_prefix_body_terminal. fs_h_ph_be_power_horner_prefix_body_terminal + S (half) = S ((S (l)) * ff_v_ph_be_power_horner_prefix)) /\ exists fs_q_ph_be_power_horner_prefix_body_terminal. ff_u_ph_be_power_horner_prefix = fs_q_ph_be_power_horner_prefix_body_terminal * S ((S (l)) * ff_v_ph_be_power_horner_prefix) + (half))) /\ forall ff_i_ph_be_power_horner_prefix_body_steps. (exists ph_bound_be_power_horner_prefix_body_steps. ph_bound_be_power_horner_prefix_body_steps + S ff_i_ph_be_power_horner_prefix_body_steps = l) -> exists ff_coefficient_ph_be_power_horner_prefix_body_steps ff_previous_ph_be_power_horner_prefix_body_steps ff_current_ph_be_power_horner_prefix_body_steps. ((((exists fs_h_ph_be_power_horner_prefix_body_steps_coefficient. fs_h_ph_be_power_horner_prefix_body_steps_coefficient + S (ff_coefficient_ph_be_power_horner_prefix_body_steps) = S ((S (ff_i_ph_be_power_horner_prefix_body_steps)) * c)) /\ exists fs_q_ph_be_power_horner_prefix_body_steps_coefficient. b = fs_q_ph_be_power_horner_prefix_body_steps_coefficient * S ((S (ff_i_ph_be_power_horner_prefix_body_steps)) * c) + (ff_coefficient_ph_be_power_horner_prefix_body_steps))) /\ ((((exists fs_h_ph_be_power_horner_prefix_body_steps_before. fs_h_ph_be_power_horner_prefix_body_steps_before + S (ff_previous_ph_be_power_horner_prefix_body_steps) = S ((S (ff_i_ph_be_power_horner_prefix_body_steps)) * ff_v_ph_be_power_horner_prefix)) /\ exists fs_q_ph_be_power_horner_prefix_body_steps_before. ff_u_ph_be_power_horner_prefix = fs_q_ph_be_power_horner_prefix_body_steps_before * S ((S (ff_i_ph_be_power_horner_prefix_body_steps)) * ff_v_ph_be_power_horner_prefix) + (ff_previous_ph_be_power_horner_prefix_body_steps))) /\ ((((exists fs_h_ph_be_power_horner_prefix_body_steps_after. fs_h_ph_be_power_horner_prefix_body_steps_after + S (ff_current_ph_be_power_horner_prefix_body_steps) = S ((S (S ff_i_ph_be_power_horner_prefix_body_steps)) * ff_v_ph_be_power_horner_prefix)) /\ exists fs_q_ph_be_power_horner_prefix_body_steps_after. ff_u_ph_be_power_horner_prefix = fs_q_ph_be_power_horner_prefix_body_steps_after * S ((S (S ff_i_ph_be_power_horner_prefix_body_steps)) * ff_v_ph_be_power_horner_prefix) + (ff_current_ph_be_power_horner_prefix_body_steps))) /\ ff_current_ph_be_power_horner_prefix_body_steps = ff_previous_ph_be_power_horner_prefix_body_steps * 2 + ff_coefficient_ph_be_power_horner_prefix_body_steps)))))) /\ e = half * 2 + digit))
  40. 0040specialize beta_horner_eval_successor_decompose b
  41. 0041specialize beta_horner_eval_successor_decompose c
  42. 0042specialize beta_horner_eval_successor_decompose 2
  43. 0043specialize beta_horner_eval_successor_decompose l
  44. 0044specialize beta_horner_eval_successor_decompose e
  45. 0045apply beta_horner_eval_successor_decompose
  46. 0046exact hhorner
  47. 0047cases hhstep
  48. 0048cases hhstep_witness
  49. 0049cases hhstep_witness_witness
  50. 0050cases hhstep_witness_witness_right
  51. 0051have hxstep : exists digit previous. ((((exists ff_h_be_power_execution_digit. ff_h_be_power_execution_digit + S (digit) = S ((S (l)) * c)) /\ exists ff_q_be_power_execution_digit. b = ff_q_be_power_execution_digit * S ((S (l)) * c) + (digit))) /\ ((exists ff_trace_code_be_power_execution_prefix ff_trace_scale_be_power_execution_prefix. ((((((exists ff_h_be_power_execution_prefix_trace_start. ff_h_be_power_execution_prefix_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_power_execution_prefix)) /\ exists ff_q_be_power_execution_prefix_trace_start. ff_trace_code_be_power_execution_prefix = ff_q_be_power_execution_prefix_trace_start * S ((S (0)) * ff_trace_scale_be_power_execution_prefix) + (1))) /\ forall ff_index_be_power_execution_prefix_trace. (exists ff_lt_be_power_execution_prefix_trace_bound. ff_lt_be_power_execution_prefix_trace_bound + S ff_index_be_power_execution_prefix_trace = l) -> exists ff_digit_be_power_execution_prefix_trace ff_previous_be_power_execution_prefix_trace ff_current_be_power_execution_prefix_trace. ((((exists ff_h_be_power_execution_prefix_trace_source. ff_h_be_power_execution_prefix_trace_source + S (ff_digit_be_power_execution_prefix_trace) = S ((S (ff_index_be_power_execution_prefix_trace)) * c)) /\ exists ff_q_be_power_execution_prefix_trace_source. b = ff_q_be_power_execution_prefix_trace_source * S ((S (ff_index_be_power_execution_prefix_trace)) * c) + (ff_digit_be_power_execution_prefix_trace))) /\ ((((exists ff_h_be_power_execution_prefix_trace_before. ff_h_be_power_execution_prefix_trace_before + S (ff_previous_be_power_execution_prefix_trace) = S ((S (ff_index_be_power_execution_prefix_trace)) * ff_trace_scale_be_power_execution_prefix)) /\ exists ff_q_be_power_execution_prefix_trace_before. ff_trace_code_be_power_execution_prefix = ff_q_be_power_execution_prefix_trace_before * S ((S (ff_index_be_power_execution_prefix_trace)) * ff_trace_scale_be_power_execution_prefix) + (ff_previous_be_power_execution_prefix_trace))) /\ ((((exists ff_h_be_power_execution_prefix_trace_after. ff_h_be_power_execution_prefix_trace_after + S (ff_current_be_power_execution_prefix_trace) = S ((S (S ff_index_be_power_execution_prefix_trace)) * ff_trace_scale_be_power_execution_prefix)) /\ exists ff_q_be_power_execution_prefix_trace_after. ff_trace_code_be_power_execution_prefix = ff_q_be_power_execution_prefix_trace_after * S ((S (S ff_index_be_power_execution_prefix_trace)) * ff_trace_scale_be_power_execution_prefix) + (ff_current_be_power_execution_prefix_trace))) /\ ((((ff_digit_be_power_execution_prefix_trace = 0) /\ (((exists ff_gap_binary_be_power_execution_prefix_trace_transition_square. ff_gap_binary_be_power_execution_prefix_trace_transition_square + S (ff_current_be_power_execution_prefix_trace) = m) /\ (exists ff_left_binary_be_power_execution_prefix_trace_transition_square_congruence ff_right_binary_be_power_execution_prefix_trace_transition_square_congruence. (ff_previous_be_power_execution_prefix_trace * ff_previous_be_power_execution_prefix_trace) + m * ff_left_binary_be_power_execution_prefix_trace_transition_square_congruence = (ff_current_be_power_execution_prefix_trace) + m * ff_right_binary_be_power_execution_prefix_trace_transition_square_congruence)))) \/ ((ff_digit_be_power_execution_prefix_trace = 1) /\ (((exists ff_gap_binary_be_power_execution_prefix_trace_transition_multiply. ff_gap_binary_be_power_execution_prefix_trace_transition_multiply + S (ff_current_be_power_execution_prefix_trace) = m) /\ (exists ff_left_binary_be_power_execution_prefix_trace_transition_multiply_congruence ff_right_binary_be_power_execution_prefix_trace_transition_multiply_congruence. ((ff_previous_be_power_execution_prefix_trace * ff_previous_be_power_execution_prefix_trace) * a) + m * ff_left_binary_be_power_execution_prefix_trace_transition_multiply_congruence = (ff_current_be_power_execution_prefix_trace) + m * ff_right_binary_be_power_execution_prefix_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_power_execution_prefix_terminal. ff_h_be_power_execution_prefix_terminal + S (previous) = S ((S (l)) * ff_trace_scale_be_power_execution_prefix)) /\ exists ff_q_be_power_execution_prefix_terminal. ff_trace_code_be_power_execution_prefix = ff_q_be_power_execution_prefix_terminal * S ((S (l)) * ff_trace_scale_be_power_execution_prefix) + (previous))))) /\ ((((digit = 0) /\ (((exists ff_gap_binary_power_execution_step_square. ff_gap_binary_power_execution_step_square + S (r) = m) /\ (exists ff_left_binary_power_execution_step_square_congruence ff_right_binary_power_execution_step_square_congruence. (previous * previous) + m * ff_left_binary_power_execution_step_square_congruence = (r) + m * ff_right_binary_power_execution_step_square_congruence)))) \/ ((digit = 1) /\ (((exists ff_gap_binary_power_execution_step_multiply. ff_gap_binary_power_execution_step_multiply + S (r) = m) /\ (exists ff_left_binary_power_execution_step_multiply_congruence ff_right_binary_power_execution_step_multiply_congruence. ((previous * previous) * a) + m * ff_left_binary_power_execution_step_multiply_congruence = (r) + m * ff_right_binary_power_execution_step_multiply_congruence))))))))
  52. 0052specialize binary_modular_execution_successor_decompose b
  53. 0053specialize binary_modular_execution_successor_decompose c
  54. 0054specialize binary_modular_execution_successor_decompose a
  55. 0055specialize binary_modular_execution_successor_decompose m
  56. 0056specialize binary_modular_execution_successor_decompose l
  57. 0057specialize binary_modular_execution_successor_decompose r
  58. 0058apply binary_modular_execution_successor_decompose
  59. 0059exact hexecution
  60. 0060cases hxstep
  61. 0061cases hxstep_witness
  62. 0062cases hxstep_witness_witness
  63. 0063cases hxstep_witness_witness_right
  64. 0064have hdigit : x = x2
  65. 0065specialize beta_at_unique b
  66. 0066specialize beta_at_unique c
  67. 0067specialize beta_at_unique l
  68. 0068specialize beta_at_unique x
  69. 0069specialize beta_at_unique x2
  70. 0070apply beta_at_unique
  71. 0071exact hhstep_witness_witness_left
  72. 0072exact hxstep_witness_witness_left
  73. 0073rewrite hdigit at hhstep_witness_witness_right_right
  74. 0074have hbit : x2 = 0 \/ x2 = 1
  75. 0075specialize binary_execution_step_digit m
  76. 0076specialize binary_execution_step_digit x3
  77. 0077specialize binary_execution_step_digit a
  78. 0078specialize binary_execution_step_digit x2
  79. 0079specialize binary_execution_step_digit r
  80. 0080apply binary_execution_step_digit
  81. 0081exact hxstep_witness_witness_right_right
  82. 0082have hsplit : ((((x2 = 0) \/ (x2 = 1)) /\ e = (x1 + x1) + x2))
  83. 0083specialize binary_execution_horner_digit_split x1
  84. 0084specialize binary_execution_horner_digit_split e
  85. 0085specialize binary_execution_horner_digit_split x2
  86. 0086apply binary_execution_horner_digit_split
  87. 0087exact hbit
  88. 0088exact hhstep_witness_witness_right_right
  89. 0089have hprevious : (exists ff_power_binary_correctness_previous. ((exists ff_b_binary_correctness_previous_value ff_c_binary_correctness_previous_value. ((forall ff_i_binary_correctness_previous_value_repeat. (exists ff_lt_binary_correctness_previous_value_repeat_bound. ff_lt_binary_correctness_previous_value_repeat_bound + S ff_i_binary_correctness_previous_value_repeat = x1) -> (((exists ff_h_binary_correctness_previous_value_repeat_decoded. ff_h_binary_correctness_previous_value_repeat_decoded + S (a) = S ((S (ff_i_binary_correctness_previous_value_repeat)) * ff_c_binary_correctness_previous_value)) /\ exists ff_q_binary_correctness_previous_value_repeat_decoded. ff_b_binary_correctness_previous_value = ff_q_binary_correctness_previous_value_repeat_decoded * S ((S (ff_i_binary_correctness_previous_value_repeat)) * ff_c_binary_correctness_previous_value) + (a)))) /\ (exists ff_u_binary_correctness_previous_value_product ff_v_binary_correctness_previous_value_product. ((((exists ff_h_binary_correctness_previous_value_product_start. ff_h_binary_correctness_previous_value_product_start + S (1) = S ((S (0)) * ff_v_binary_correctness_previous_value_product)) /\ exists ff_q_binary_correctness_previous_value_product_start. ff_u_binary_correctness_previous_value_product = ff_q_binary_correctness_previous_value_product_start * S ((S (0)) * ff_v_binary_correctness_previous_value_product) + (1))) /\ ((((exists ff_h_binary_correctness_previous_value_product_terminal. ff_h_binary_correctness_previous_value_product_terminal + S (ff_power_binary_correctness_previous) = S ((S (x1)) * ff_v_binary_correctness_previous_value_product)) /\ exists ff_q_binary_correctness_previous_value_product_terminal. ff_u_binary_correctness_previous_value_product = ff_q_binary_correctness_previous_value_product_terminal * S ((S (x1)) * ff_v_binary_correctness_previous_value_product) + (ff_power_binary_correctness_previous))) /\ forall ff_i_binary_correctness_previous_value_product. (exists ff_lt_binary_correctness_previous_value_product_bound. ff_lt_binary_correctness_previous_value_product_bound + S ff_i_binary_correctness_previous_value_product = x1) -> exists ff_p_binary_correctness_previous_value_product ff_r_binary_correctness_previous_value_product ff_s_binary_correctness_previous_value_product. ((((exists ff_h_binary_correctness_previous_value_product_factor. ff_h_binary_correctness_previous_value_product_factor + S (ff_p_binary_correctness_previous_value_product) = S ((S (ff_i_binary_correctness_previous_value_product)) * ff_c_binary_correctness_previous_value)) /\ exists ff_q_binary_correctness_previous_value_product_factor. ff_b_binary_correctness_previous_value = ff_q_binary_correctness_previous_value_product_factor * S ((S (ff_i_binary_correctness_previous_value_product)) * ff_c_binary_correctness_previous_value) + (ff_p_binary_correctness_previous_value_product))) /\ ((((exists ff_h_binary_correctness_previous_value_product_partial. ff_h_binary_correctness_previous_value_product_partial + S (ff_r_binary_correctness_previous_value_product) = S ((S (ff_i_binary_correctness_previous_value_product)) * ff_v_binary_correctness_previous_value_product)) /\ exists ff_q_binary_correctness_previous_value_product_partial. ff_u_binary_correctness_previous_value_product = ff_q_binary_correctness_previous_value_product_partial * S ((S (ff_i_binary_correctness_previous_value_product)) * ff_v_binary_correctness_previous_value_product) + (ff_r_binary_correctness_previous_value_product))) /\ ((((exists ff_h_binary_correctness_previous_value_product_successor. ff_h_binary_correctness_previous_value_product_successor + S (ff_s_binary_correctness_previous_value_product) = S ((S (S ff_i_binary_correctness_previous_value_product)) * ff_v_binary_correctness_previous_value_product)) /\ exists ff_q_binary_correctness_previous_value_product_successor. ff_u_binary_correctness_previous_value_product = ff_q_binary_correctness_previous_value_product_successor * S ((S (S ff_i_binary_correctness_previous_value_product)) * ff_v_binary_correctness_previous_value_product) + (ff_s_binary_correctness_previous_value_product))) /\ ff_s_binary_correctness_previous_value_product = ff_r_binary_correctness_previous_value_product * ff_p_binary_correctness_previous_value_product)))))))) /\ (((exists ff_gap_binary_correctness_previous_residue. ff_gap_binary_correctness_previous_residue + S (x3) = m) /\ (exists ff_left_binary_correctness_previous_residue_congruence ff_right_binary_correctness_previous_residue_congruence. (ff_power_binary_correctness_previous) + m * ff_left_binary_correctness_previous_residue_congruence = (x3) + m * ff_right_binary_correctness_previous_residue_congruence)))))
  90. 0090specialize IH x1
  91. 0091specialize IH x3
  92. 0092apply IH
  93. 0093exact hmodulus
  94. 0094exact hhstep_witness_witness_right_left
  95. 0095exact hxstep_witness_witness_right_left
  96. 0096specialize binary_execution_step_power_invariant a
  97. 0097specialize binary_execution_step_power_invariant x1
  98. 0098specialize binary_execution_step_power_invariant e
  99. 0099specialize binary_execution_step_power_invariant m
  100. 0100specialize binary_execution_step_power_invariant x3
  101. 0101specialize binary_execution_step_power_invariant x2
  102. 0102specialize binary_execution_step_power_invariant r
  103. 0103apply binary_execution_step_power_invariant
  104. 0104exact hprevious
  105. 0105exact hsplit
  106. 0106exact hxstep_witness_witness_right_right