BT00XX

double_quotient_carry_prefix_exists

Alpha body-checked · checked-use disabled

Doubled quotient prefixes admit a beta-coded carry prefix.

Exact expanded PA statement

forall p n b c d e l. (forall bls_index_b5ccpx_left. (exists bls_gap_b5ccpx_left_bound. bls_gap_b5ccpx_left_bound + S (bls_index_b5ccpx_left) = (l)) -> exists bls_power_b5ccpx_left bls_quotient_b5ccpx_left bls_remainder_b5ccpx_left. ((exists bpvi_b_bls_b5ccpx_left_power bpvi_c_bls_b5ccpx_left_power. ((forall bpvi_i_bls_b5ccpx_left_power. (exists bpvi_repeat_gap_bls_b5ccpx_left_power. bpvi_repeat_gap_bls_b5ccpx_left_power + S bpvi_i_bls_b5ccpx_left_power = S bls_index_b5ccpx_left) -> (((exists bpvi_h_bls_b5ccpx_left_power_repeat. bpvi_h_bls_b5ccpx_left_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccpx_left_power)) * bpvi_c_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_repeat. bpvi_b_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_repeat * S ((S (bpvi_i_bls_b5ccpx_left_power)) * bpvi_c_bls_b5ccpx_left_power) + (p)))) /\ (exists bpvi_u_bls_b5ccpx_left_power bpvi_v_bls_b5ccpx_left_power. ((((exists bpvi_h_bls_b5ccpx_left_power_start. bpvi_h_bls_b5ccpx_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_start. bpvi_u_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_start * S ((S (0)) * bpvi_v_bls_b5ccpx_left_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccpx_left_power_terminal. bpvi_h_bls_b5ccpx_left_power_terminal + S (bls_power_b5ccpx_left) = S ((S (S bls_index_b5ccpx_left)) * bpvi_v_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_terminal. bpvi_u_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_terminal * S ((S (S bls_index_b5ccpx_left)) * bpvi_v_bls_b5ccpx_left_power) + (bls_power_b5ccpx_left))) /\ forall bpvi_j_bls_b5ccpx_left_power. (exists bpvi_product_gap_bls_b5ccpx_left_power. bpvi_product_gap_bls_b5ccpx_left_power + S bpvi_j_bls_b5ccpx_left_power = S bls_index_b5ccpx_left) -> exists bpvi_factor_bls_b5ccpx_left_power bpvi_partial_bls_b5ccpx_left_power bpvi_successor_bls_b5ccpx_left_power. ((((exists bpvi_h_bls_b5ccpx_left_power_factor. bpvi_h_bls_b5ccpx_left_power_factor + S (bpvi_factor_bls_b5ccpx_left_power) = S ((S (bpvi_j_bls_b5ccpx_left_power)) * bpvi_c_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_factor. bpvi_b_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_factor * S ((S (bpvi_j_bls_b5ccpx_left_power)) * bpvi_c_bls_b5ccpx_left_power) + (bpvi_factor_bls_b5ccpx_left_power))) /\ ((((exists bpvi_h_bls_b5ccpx_left_power_partial. bpvi_h_bls_b5ccpx_left_power_partial + S (bpvi_partial_bls_b5ccpx_left_power) = S ((S (bpvi_j_bls_b5ccpx_left_power)) * bpvi_v_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_partial. bpvi_u_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_partial * S ((S (bpvi_j_bls_b5ccpx_left_power)) * bpvi_v_bls_b5ccpx_left_power) + (bpvi_partial_bls_b5ccpx_left_power))) /\ ((((exists bpvi_h_bls_b5ccpx_left_power_successor. bpvi_h_bls_b5ccpx_left_power_successor + S (bpvi_successor_bls_b5ccpx_left_power) = S ((S (S bpvi_j_bls_b5ccpx_left_power)) * bpvi_v_bls_b5ccpx_left_power)) /\ exists bpvi_q_bls_b5ccpx_left_power_successor. bpvi_u_bls_b5ccpx_left_power = bpvi_q_bls_b5ccpx_left_power_successor * S ((S (S bpvi_j_bls_b5ccpx_left_power)) * bpvi_v_bls_b5ccpx_left_power) + (bpvi_successor_bls_b5ccpx_left_power))) /\ bpvi_successor_bls_b5ccpx_left_power = bpvi_partial_bls_b5ccpx_left_power * bpvi_factor_bls_b5ccpx_left_power)))))))) /\ ((((exists ff_h_bls_b5ccpx_left_quotient_entry. ff_h_bls_b5ccpx_left_quotient_entry + S (bls_quotient_b5ccpx_left) = S ((S (bls_index_b5ccpx_left)) * c)) /\ exists ff_q_bls_b5ccpx_left_quotient_entry. b = ff_q_bls_b5ccpx_left_quotient_entry * S ((S (bls_index_b5ccpx_left)) * c) + (bls_quotient_b5ccpx_left))) /\ ((n = bls_power_b5ccpx_left * bls_quotient_b5ccpx_left + bls_remainder_b5ccpx_left /\ exists bls_remainder_gap_b5ccpx_left_division. bls_remainder_gap_b5ccpx_left_division + S (bls_remainder_b5ccpx_left) = bls_power_b5ccpx_left))))) -> (forall bls_index_b5ccpx_right. (exists bls_gap_b5ccpx_right_bound. bls_gap_b5ccpx_right_bound + S (bls_index_b5ccpx_right) = (l)) -> exists bls_power_b5ccpx_right bls_quotient_b5ccpx_right bls_remainder_b5ccpx_right. ((exists bpvi_b_bls_b5ccpx_right_power bpvi_c_bls_b5ccpx_right_power. ((forall bpvi_i_bls_b5ccpx_right_power. (exists bpvi_repeat_gap_bls_b5ccpx_right_power. bpvi_repeat_gap_bls_b5ccpx_right_power + S bpvi_i_bls_b5ccpx_right_power = S bls_index_b5ccpx_right) -> (((exists bpvi_h_bls_b5ccpx_right_power_repeat. bpvi_h_bls_b5ccpx_right_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccpx_right_power)) * bpvi_c_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_repeat. bpvi_b_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_repeat * S ((S (bpvi_i_bls_b5ccpx_right_power)) * bpvi_c_bls_b5ccpx_right_power) + (p)))) /\ (exists bpvi_u_bls_b5ccpx_right_power bpvi_v_bls_b5ccpx_right_power. ((((exists bpvi_h_bls_b5ccpx_right_power_start. bpvi_h_bls_b5ccpx_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_start. bpvi_u_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_start * S ((S (0)) * bpvi_v_bls_b5ccpx_right_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccpx_right_power_terminal. bpvi_h_bls_b5ccpx_right_power_terminal + S (bls_power_b5ccpx_right) = S ((S (S bls_index_b5ccpx_right)) * bpvi_v_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_terminal. bpvi_u_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_terminal * S ((S (S bls_index_b5ccpx_right)) * bpvi_v_bls_b5ccpx_right_power) + (bls_power_b5ccpx_right))) /\ forall bpvi_j_bls_b5ccpx_right_power. (exists bpvi_product_gap_bls_b5ccpx_right_power. bpvi_product_gap_bls_b5ccpx_right_power + S bpvi_j_bls_b5ccpx_right_power = S bls_index_b5ccpx_right) -> exists bpvi_factor_bls_b5ccpx_right_power bpvi_partial_bls_b5ccpx_right_power bpvi_successor_bls_b5ccpx_right_power. ((((exists bpvi_h_bls_b5ccpx_right_power_factor. bpvi_h_bls_b5ccpx_right_power_factor + S (bpvi_factor_bls_b5ccpx_right_power) = S ((S (bpvi_j_bls_b5ccpx_right_power)) * bpvi_c_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_factor. bpvi_b_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_factor * S ((S (bpvi_j_bls_b5ccpx_right_power)) * bpvi_c_bls_b5ccpx_right_power) + (bpvi_factor_bls_b5ccpx_right_power))) /\ ((((exists bpvi_h_bls_b5ccpx_right_power_partial. bpvi_h_bls_b5ccpx_right_power_partial + S (bpvi_partial_bls_b5ccpx_right_power) = S ((S (bpvi_j_bls_b5ccpx_right_power)) * bpvi_v_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_partial. bpvi_u_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_partial * S ((S (bpvi_j_bls_b5ccpx_right_power)) * bpvi_v_bls_b5ccpx_right_power) + (bpvi_partial_bls_b5ccpx_right_power))) /\ ((((exists bpvi_h_bls_b5ccpx_right_power_successor. bpvi_h_bls_b5ccpx_right_power_successor + S (bpvi_successor_bls_b5ccpx_right_power) = S ((S (S bpvi_j_bls_b5ccpx_right_power)) * bpvi_v_bls_b5ccpx_right_power)) /\ exists bpvi_q_bls_b5ccpx_right_power_successor. bpvi_u_bls_b5ccpx_right_power = bpvi_q_bls_b5ccpx_right_power_successor * S ((S (S bpvi_j_bls_b5ccpx_right_power)) * bpvi_v_bls_b5ccpx_right_power) + (bpvi_successor_bls_b5ccpx_right_power))) /\ bpvi_successor_bls_b5ccpx_right_power = bpvi_partial_bls_b5ccpx_right_power * bpvi_factor_bls_b5ccpx_right_power)))))))) /\ ((((exists ff_h_bls_b5ccpx_right_quotient_entry. ff_h_bls_b5ccpx_right_quotient_entry + S (bls_quotient_b5ccpx_right) = S ((S (bls_index_b5ccpx_right)) * e)) /\ exists ff_q_bls_b5ccpx_right_quotient_entry. d = ff_q_bls_b5ccpx_right_quotient_entry * S ((S (bls_index_b5ccpx_right)) * e) + (bls_quotient_b5ccpx_right))) /\ ((n + n = bls_power_b5ccpx_right * bls_quotient_b5ccpx_right + bls_remainder_b5ccpx_right /\ exists bls_remainder_gap_b5ccpx_right_division. bls_remainder_gap_b5ccpx_right_division + S (bls_remainder_b5ccpx_right) = bls_power_b5ccpx_right))))) -> exists f g. (forall b5cc_index_b5ccpx_result. (exists bcf_lt_gap_b5ccpx_result_bound. bcf_lt_gap_b5ccpx_result_bound + S (b5cc_index_b5ccpx_result) = l) -> exists b5cc_left_b5ccpx_result b5cc_right_b5ccpx_result b5cc_bit_b5ccpx_result. (((exists fs_h_b5cc_b5ccpx_result_left. fs_h_b5cc_b5ccpx_result_left + S (b5cc_left_b5ccpx_result) = S ((S (b5cc_index_b5ccpx_result)) * c)) /\ exists fs_q_b5cc_b5ccpx_result_left. b = fs_q_b5cc_b5ccpx_result_left * S ((S (b5cc_index_b5ccpx_result)) * c) + (b5cc_left_b5ccpx_result))) /\ ((((exists fs_h_b5cc_b5ccpx_result_right. fs_h_b5cc_b5ccpx_result_right + S (b5cc_right_b5ccpx_result) = S ((S (b5cc_index_b5ccpx_result)) * e)) /\ exists fs_q_b5cc_b5ccpx_result_right. d = fs_q_b5cc_b5ccpx_result_right * S ((S (b5cc_index_b5ccpx_result)) * e) + (b5cc_right_b5ccpx_result))) /\ ((((exists fs_h_b5cc_b5ccpx_result_bit. fs_h_b5cc_b5ccpx_result_bit + S (b5cc_bit_b5ccpx_result) = S ((S (b5cc_index_b5ccpx_result)) * g)) /\ exists fs_q_b5cc_b5ccpx_result_bit. f = fs_q_b5cc_b5ccpx_result_bit * S ((S (b5cc_index_b5ccpx_result)) * g) + (b5cc_bit_b5ccpx_result))) /\ (((b5cc_bit_b5ccpx_result = 0 /\ b5cc_right_b5ccpx_result = b5cc_left_b5ccpx_result + b5cc_left_b5ccpx_result) \/ (b5cc_bit_b5ccpx_result = 1 /\ b5cc_right_b5ccpx_result = S (b5cc_left_b5ccpx_result + b5cc_left_b5ccpx_result)))))))

Structural proof guide

Doubled quotient prefixes admit a beta-coded carry prefix.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, le_succ, le_refl, double_quotient_carry_choice, double_quotient_carry_prefix_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT0018 le_succ BT000E le_refl BT00XV double_quotient_carry_choice BT00XW double_quotient_carry_prefix_extend

Direct dependents

BT00Y4 central_binom_carry_bit_count

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007induction l
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010exists 0
  11. 0011exists 0
  12. 0012intro i
  13. 0013intro hi
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hzero : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hzero
  24. 0024intro hleft
  25. 0025intro hright
  26. 0026have hleft_prefix : forall bls_index_b5ccpx_left_prefix. (exists bls_gap_b5ccpx_left_prefix_bound. bls_gap_b5ccpx_left_prefix_bound + S (bls_index_b5ccpx_left_prefix) = (l)) -> exists bls_power_b5ccpx_left_prefix bls_quotient_b5ccpx_left_prefix bls_remainder_b5ccpx_left_prefix. ((exists bpvi_b_bls_b5ccpx_left_prefix_power bpvi_c_bls_b5ccpx_left_prefix_power. ((forall bpvi_i_bls_b5ccpx_left_prefix_power. (exists bpvi_repeat_gap_bls_b5ccpx_left_prefix_power. bpvi_repeat_gap_bls_b5ccpx_left_prefix_power + S bpvi_i_bls_b5ccpx_left_prefix_power = S bls_index_b5ccpx_left_prefix) -> (((exists bpvi_h_bls_b5ccpx_left_prefix_power_repeat. bpvi_h_bls_b5ccpx_left_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccpx_left_prefix_power)) * bpvi_c_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_repeat. bpvi_b_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_repeat * S ((S (bpvi_i_bls_b5ccpx_left_prefix_power)) * bpvi_c_bls_b5ccpx_left_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5ccpx_left_prefix_power bpvi_v_bls_b5ccpx_left_prefix_power. ((((exists bpvi_h_bls_b5ccpx_left_prefix_power_start. bpvi_h_bls_b5ccpx_left_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_start. bpvi_u_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5ccpx_left_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccpx_left_prefix_power_terminal. bpvi_h_bls_b5ccpx_left_prefix_power_terminal + S (bls_power_b5ccpx_left_prefix) = S ((S (S bls_index_b5ccpx_left_prefix)) * bpvi_v_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_terminal. bpvi_u_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_terminal * S ((S (S bls_index_b5ccpx_left_prefix)) * bpvi_v_bls_b5ccpx_left_prefix_power) + (bls_power_b5ccpx_left_prefix))) /\ forall bpvi_j_bls_b5ccpx_left_prefix_power. (exists bpvi_product_gap_bls_b5ccpx_left_prefix_power. bpvi_product_gap_bls_b5ccpx_left_prefix_power + S bpvi_j_bls_b5ccpx_left_prefix_power = S bls_index_b5ccpx_left_prefix) -> exists bpvi_factor_bls_b5ccpx_left_prefix_power bpvi_partial_bls_b5ccpx_left_prefix_power bpvi_successor_bls_b5ccpx_left_prefix_power. ((((exists bpvi_h_bls_b5ccpx_left_prefix_power_factor. bpvi_h_bls_b5ccpx_left_prefix_power_factor + S (bpvi_factor_bls_b5ccpx_left_prefix_power) = S ((S (bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_c_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_factor. bpvi_b_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_factor * S ((S (bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_c_bls_b5ccpx_left_prefix_power) + (bpvi_factor_bls_b5ccpx_left_prefix_power))) /\ ((((exists bpvi_h_bls_b5ccpx_left_prefix_power_partial. bpvi_h_bls_b5ccpx_left_prefix_power_partial + S (bpvi_partial_bls_b5ccpx_left_prefix_power) = S ((S (bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_v_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_partial. bpvi_u_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_partial * S ((S (bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_v_bls_b5ccpx_left_prefix_power) + (bpvi_partial_bls_b5ccpx_left_prefix_power))) /\ ((((exists bpvi_h_bls_b5ccpx_left_prefix_power_successor. bpvi_h_bls_b5ccpx_left_prefix_power_successor + S (bpvi_successor_bls_b5ccpx_left_prefix_power) = S ((S (S bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_v_bls_b5ccpx_left_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_left_prefix_power_successor. bpvi_u_bls_b5ccpx_left_prefix_power = bpvi_q_bls_b5ccpx_left_prefix_power_successor * S ((S (S bpvi_j_bls_b5ccpx_left_prefix_power)) * bpvi_v_bls_b5ccpx_left_prefix_power) + (bpvi_successor_bls_b5ccpx_left_prefix_power))) /\ bpvi_successor_bls_b5ccpx_left_prefix_power = bpvi_partial_bls_b5ccpx_left_prefix_power * bpvi_factor_bls_b5ccpx_left_prefix_power)))))))) /\ ((((exists ff_h_bls_b5ccpx_left_prefix_quotient_entry. ff_h_bls_b5ccpx_left_prefix_quotient_entry + S (bls_quotient_b5ccpx_left_prefix) = S ((S (bls_index_b5ccpx_left_prefix)) * c)) /\ exists ff_q_bls_b5ccpx_left_prefix_quotient_entry. b = ff_q_bls_b5ccpx_left_prefix_quotient_entry * S ((S (bls_index_b5ccpx_left_prefix)) * c) + (bls_quotient_b5ccpx_left_prefix))) /\ ((n = bls_power_b5ccpx_left_prefix * bls_quotient_b5ccpx_left_prefix + bls_remainder_b5ccpx_left_prefix /\ exists bls_remainder_gap_b5ccpx_left_prefix_division. bls_remainder_gap_b5ccpx_left_prefix_division + S (bls_remainder_b5ccpx_left_prefix) = bls_power_b5ccpx_left_prefix))))
  27. 0027intro i
  28. 0028intro hi
  29. 0029specialize hleft i
  30. 0030apply hleft
  31. 0031specialize le_succ (S i)
  32. 0032specialize le_succ l
  33. 0033apply le_succ
  34. 0034exact hi
  35. 0035have hright_prefix : forall bls_index_b5ccpx_right_prefix. (exists bls_gap_b5ccpx_right_prefix_bound. bls_gap_b5ccpx_right_prefix_bound + S (bls_index_b5ccpx_right_prefix) = (l)) -> exists bls_power_b5ccpx_right_prefix bls_quotient_b5ccpx_right_prefix bls_remainder_b5ccpx_right_prefix. ((exists bpvi_b_bls_b5ccpx_right_prefix_power bpvi_c_bls_b5ccpx_right_prefix_power. ((forall bpvi_i_bls_b5ccpx_right_prefix_power. (exists bpvi_repeat_gap_bls_b5ccpx_right_prefix_power. bpvi_repeat_gap_bls_b5ccpx_right_prefix_power + S bpvi_i_bls_b5ccpx_right_prefix_power = S bls_index_b5ccpx_right_prefix) -> (((exists bpvi_h_bls_b5ccpx_right_prefix_power_repeat. bpvi_h_bls_b5ccpx_right_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccpx_right_prefix_power)) * bpvi_c_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_repeat. bpvi_b_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_repeat * S ((S (bpvi_i_bls_b5ccpx_right_prefix_power)) * bpvi_c_bls_b5ccpx_right_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5ccpx_right_prefix_power bpvi_v_bls_b5ccpx_right_prefix_power. ((((exists bpvi_h_bls_b5ccpx_right_prefix_power_start. bpvi_h_bls_b5ccpx_right_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_start. bpvi_u_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5ccpx_right_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccpx_right_prefix_power_terminal. bpvi_h_bls_b5ccpx_right_prefix_power_terminal + S (bls_power_b5ccpx_right_prefix) = S ((S (S bls_index_b5ccpx_right_prefix)) * bpvi_v_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_terminal. bpvi_u_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_terminal * S ((S (S bls_index_b5ccpx_right_prefix)) * bpvi_v_bls_b5ccpx_right_prefix_power) + (bls_power_b5ccpx_right_prefix))) /\ forall bpvi_j_bls_b5ccpx_right_prefix_power. (exists bpvi_product_gap_bls_b5ccpx_right_prefix_power. bpvi_product_gap_bls_b5ccpx_right_prefix_power + S bpvi_j_bls_b5ccpx_right_prefix_power = S bls_index_b5ccpx_right_prefix) -> exists bpvi_factor_bls_b5ccpx_right_prefix_power bpvi_partial_bls_b5ccpx_right_prefix_power bpvi_successor_bls_b5ccpx_right_prefix_power. ((((exists bpvi_h_bls_b5ccpx_right_prefix_power_factor. bpvi_h_bls_b5ccpx_right_prefix_power_factor + S (bpvi_factor_bls_b5ccpx_right_prefix_power) = S ((S (bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_c_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_factor. bpvi_b_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_factor * S ((S (bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_c_bls_b5ccpx_right_prefix_power) + (bpvi_factor_bls_b5ccpx_right_prefix_power))) /\ ((((exists bpvi_h_bls_b5ccpx_right_prefix_power_partial. bpvi_h_bls_b5ccpx_right_prefix_power_partial + S (bpvi_partial_bls_b5ccpx_right_prefix_power) = S ((S (bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_v_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_partial. bpvi_u_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_partial * S ((S (bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_v_bls_b5ccpx_right_prefix_power) + (bpvi_partial_bls_b5ccpx_right_prefix_power))) /\ ((((exists bpvi_h_bls_b5ccpx_right_prefix_power_successor. bpvi_h_bls_b5ccpx_right_prefix_power_successor + S (bpvi_successor_bls_b5ccpx_right_prefix_power) = S ((S (S bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_v_bls_b5ccpx_right_prefix_power)) /\ exists bpvi_q_bls_b5ccpx_right_prefix_power_successor. bpvi_u_bls_b5ccpx_right_prefix_power = bpvi_q_bls_b5ccpx_right_prefix_power_successor * S ((S (S bpvi_j_bls_b5ccpx_right_prefix_power)) * bpvi_v_bls_b5ccpx_right_prefix_power) + (bpvi_successor_bls_b5ccpx_right_prefix_power))) /\ bpvi_successor_bls_b5ccpx_right_prefix_power = bpvi_partial_bls_b5ccpx_right_prefix_power * bpvi_factor_bls_b5ccpx_right_prefix_power)))))))) /\ ((((exists ff_h_bls_b5ccpx_right_prefix_quotient_entry. ff_h_bls_b5ccpx_right_prefix_quotient_entry + S (bls_quotient_b5ccpx_right_prefix) = S ((S (bls_index_b5ccpx_right_prefix)) * e)) /\ exists ff_q_bls_b5ccpx_right_prefix_quotient_entry. d = ff_q_bls_b5ccpx_right_prefix_quotient_entry * S ((S (bls_index_b5ccpx_right_prefix)) * e) + (bls_quotient_b5ccpx_right_prefix))) /\ ((n + n = bls_power_b5ccpx_right_prefix * bls_quotient_b5ccpx_right_prefix + bls_remainder_b5ccpx_right_prefix /\ exists bls_remainder_gap_b5ccpx_right_prefix_division. bls_remainder_gap_b5ccpx_right_prefix_division + S (bls_remainder_b5ccpx_right_prefix) = bls_power_b5ccpx_right_prefix))))
  36. 0036intro i
  37. 0037intro hi
  38. 0038specialize hright i
  39. 0039apply hright
  40. 0040specialize le_succ (S i)
  41. 0041specialize le_succ l
  42. 0042apply le_succ
  43. 0043exact hi
  44. 0044have hprefix : exists f g. forall b5cc_index_b5ccpx_previous. (exists bcf_lt_gap_b5ccpx_previous_bound. bcf_lt_gap_b5ccpx_previous_bound + S (b5cc_index_b5ccpx_previous) = l) -> exists b5cc_left_b5ccpx_previous b5cc_right_b5ccpx_previous b5cc_bit_b5ccpx_previous. (((exists fs_h_b5cc_b5ccpx_previous_left. fs_h_b5cc_b5ccpx_previous_left + S (b5cc_left_b5ccpx_previous) = S ((S (b5cc_index_b5ccpx_previous)) * c)) /\ exists fs_q_b5cc_b5ccpx_previous_left. b = fs_q_b5cc_b5ccpx_previous_left * S ((S (b5cc_index_b5ccpx_previous)) * c) + (b5cc_left_b5ccpx_previous))) /\ ((((exists fs_h_b5cc_b5ccpx_previous_right. fs_h_b5cc_b5ccpx_previous_right + S (b5cc_right_b5ccpx_previous) = S ((S (b5cc_index_b5ccpx_previous)) * e)) /\ exists fs_q_b5cc_b5ccpx_previous_right. d = fs_q_b5cc_b5ccpx_previous_right * S ((S (b5cc_index_b5ccpx_previous)) * e) + (b5cc_right_b5ccpx_previous))) /\ ((((exists fs_h_b5cc_b5ccpx_previous_bit. fs_h_b5cc_b5ccpx_previous_bit + S (b5cc_bit_b5ccpx_previous) = S ((S (b5cc_index_b5ccpx_previous)) * g)) /\ exists fs_q_b5cc_b5ccpx_previous_bit. f = fs_q_b5cc_b5ccpx_previous_bit * S ((S (b5cc_index_b5ccpx_previous)) * g) + (b5cc_bit_b5ccpx_previous))) /\ (((b5cc_bit_b5ccpx_previous = 0 /\ b5cc_right_b5ccpx_previous = b5cc_left_b5ccpx_previous + b5cc_left_b5ccpx_previous) \/ (b5cc_bit_b5ccpx_previous = 1 /\ b5cc_right_b5ccpx_previous = S (b5cc_left_b5ccpx_previous + b5cc_left_b5ccpx_previous))))))
  45. 0045apply IH
  46. 0046exact hleft_prefix
  47. 0047exact hright_prefix
  48. 0048cases hprefix
  49. 0049cases hprefix_witness
  50. 0050have hlast : exists q Q bit. (((exists fs_h_b5ccpx_last_left. fs_h_b5ccpx_last_left + S (q) = S ((S (l)) * c)) /\ exists fs_q_b5ccpx_last_left. b = fs_q_b5ccpx_last_left * S ((S (l)) * c) + (q))) /\ ((((exists fs_h_b5ccpx_last_right. fs_h_b5ccpx_last_right + S (Q) = S ((S (l)) * e)) /\ exists fs_q_b5ccpx_last_right. d = fs_q_b5ccpx_last_right * S ((S (l)) * e) + (Q))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q)))))
  51. 0051specialize double_quotient_carry_choice p
  52. 0052specialize double_quotient_carry_choice n
  53. 0053specialize double_quotient_carry_choice b
  54. 0054specialize double_quotient_carry_choice c
  55. 0055specialize double_quotient_carry_choice d
  56. 0056specialize double_quotient_carry_choice e
  57. 0057specialize double_quotient_carry_choice (S l)
  58. 0058specialize double_quotient_carry_choice l
  59. 0059apply double_quotient_carry_choice
  60. 0060exact hleft
  61. 0061exact hright
  62. 0062specialize le_refl (S l)
  63. 0063exact le_refl
  64. 0064specialize double_quotient_carry_prefix_extend b
  65. 0065specialize double_quotient_carry_prefix_extend c
  66. 0066specialize double_quotient_carry_prefix_extend d
  67. 0067specialize double_quotient_carry_prefix_extend e
  68. 0068specialize double_quotient_carry_prefix_extend x
  69. 0069specialize double_quotient_carry_prefix_extend x1
  70. 0070specialize double_quotient_carry_prefix_extend l
  71. 0071apply double_quotient_carry_prefix_extend
  72. 0072exact hprefix_witness_witness
  73. 0073exact hlast