KU0008

add_quotient_carry_prefix_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Three arbitrary power-quotient prefixes admit a beta-coded additive carry prefix.

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.

Exact expanded first-order arithmetic statement

forall p a b lb lc rb rc tb tc l. (forall bls_index_kmcpx_left. (exists bls_gap_kmcpx_left_bound. bls_gap_kmcpx_left_bound + S (bls_index_kmcpx_left) = (l)) -> exists bls_power_kmcpx_left bls_quotient_kmcpx_left bls_remainder_kmcpx_left. ((exists bpvi_b_bls_kmcpx_left_power bpvi_c_bls_kmcpx_left_power. ((forall bpvi_i_bls_kmcpx_left_power. (exists bpvi_repeat_gap_bls_kmcpx_left_power. bpvi_repeat_gap_bls_kmcpx_left_power + S bpvi_i_bls_kmcpx_left_power = S bls_index_kmcpx_left) -> (((exists bpvi_h_bls_kmcpx_left_power_repeat. bpvi_h_bls_kmcpx_left_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_left_power)) * bpvi_c_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_repeat. bpvi_b_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_repeat * S ((S (bpvi_i_bls_kmcpx_left_power)) * bpvi_c_bls_kmcpx_left_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_left_power bpvi_v_bls_kmcpx_left_power. ((((exists bpvi_h_bls_kmcpx_left_power_start. bpvi_h_bls_kmcpx_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_start. bpvi_u_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_left_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_left_power_terminal. bpvi_h_bls_kmcpx_left_power_terminal + S (bls_power_kmcpx_left) = S ((S (S bls_index_kmcpx_left)) * bpvi_v_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_terminal. bpvi_u_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_terminal * S ((S (S bls_index_kmcpx_left)) * bpvi_v_bls_kmcpx_left_power) + (bls_power_kmcpx_left))) /\ forall bpvi_j_bls_kmcpx_left_power. (exists bpvi_product_gap_bls_kmcpx_left_power. bpvi_product_gap_bls_kmcpx_left_power + S bpvi_j_bls_kmcpx_left_power = S bls_index_kmcpx_left) -> exists bpvi_factor_bls_kmcpx_left_power bpvi_partial_bls_kmcpx_left_power bpvi_successor_bls_kmcpx_left_power. ((((exists bpvi_h_bls_kmcpx_left_power_factor. bpvi_h_bls_kmcpx_left_power_factor + S (bpvi_factor_bls_kmcpx_left_power) = S ((S (bpvi_j_bls_kmcpx_left_power)) * bpvi_c_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_factor. bpvi_b_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_factor * S ((S (bpvi_j_bls_kmcpx_left_power)) * bpvi_c_bls_kmcpx_left_power) + (bpvi_factor_bls_kmcpx_left_power))) /\ ((((exists bpvi_h_bls_kmcpx_left_power_partial. bpvi_h_bls_kmcpx_left_power_partial + S (bpvi_partial_bls_kmcpx_left_power) = S ((S (bpvi_j_bls_kmcpx_left_power)) * bpvi_v_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_partial. bpvi_u_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_partial * S ((S (bpvi_j_bls_kmcpx_left_power)) * bpvi_v_bls_kmcpx_left_power) + (bpvi_partial_bls_kmcpx_left_power))) /\ ((((exists bpvi_h_bls_kmcpx_left_power_successor. bpvi_h_bls_kmcpx_left_power_successor + S (bpvi_successor_bls_kmcpx_left_power) = S ((S (S bpvi_j_bls_kmcpx_left_power)) * bpvi_v_bls_kmcpx_left_power)) /\ exists bpvi_q_bls_kmcpx_left_power_successor. bpvi_u_bls_kmcpx_left_power = bpvi_q_bls_kmcpx_left_power_successor * S ((S (S bpvi_j_bls_kmcpx_left_power)) * bpvi_v_bls_kmcpx_left_power) + (bpvi_successor_bls_kmcpx_left_power))) /\ bpvi_successor_bls_kmcpx_left_power = bpvi_partial_bls_kmcpx_left_power * bpvi_factor_bls_kmcpx_left_power)))))))) /\ ((((exists ff_h_bls_kmcpx_left_quotient_entry. ff_h_bls_kmcpx_left_quotient_entry + S (bls_quotient_kmcpx_left) = S ((S (bls_index_kmcpx_left)) * lc)) /\ exists ff_q_bls_kmcpx_left_quotient_entry. lb = ff_q_bls_kmcpx_left_quotient_entry * S ((S (bls_index_kmcpx_left)) * lc) + (bls_quotient_kmcpx_left))) /\ ((a = bls_power_kmcpx_left * bls_quotient_kmcpx_left + bls_remainder_kmcpx_left /\ exists bls_remainder_gap_kmcpx_left_division. bls_remainder_gap_kmcpx_left_division + S (bls_remainder_kmcpx_left) = bls_power_kmcpx_left))))) -> (forall bls_index_kmcpx_right. (exists bls_gap_kmcpx_right_bound. bls_gap_kmcpx_right_bound + S (bls_index_kmcpx_right) = (l)) -> exists bls_power_kmcpx_right bls_quotient_kmcpx_right bls_remainder_kmcpx_right. ((exists bpvi_b_bls_kmcpx_right_power bpvi_c_bls_kmcpx_right_power. ((forall bpvi_i_bls_kmcpx_right_power. (exists bpvi_repeat_gap_bls_kmcpx_right_power. bpvi_repeat_gap_bls_kmcpx_right_power + S bpvi_i_bls_kmcpx_right_power = S bls_index_kmcpx_right) -> (((exists bpvi_h_bls_kmcpx_right_power_repeat. bpvi_h_bls_kmcpx_right_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_right_power)) * bpvi_c_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_repeat. bpvi_b_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_repeat * S ((S (bpvi_i_bls_kmcpx_right_power)) * bpvi_c_bls_kmcpx_right_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_right_power bpvi_v_bls_kmcpx_right_power. ((((exists bpvi_h_bls_kmcpx_right_power_start. bpvi_h_bls_kmcpx_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_start. bpvi_u_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_right_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_right_power_terminal. bpvi_h_bls_kmcpx_right_power_terminal + S (bls_power_kmcpx_right) = S ((S (S bls_index_kmcpx_right)) * bpvi_v_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_terminal. bpvi_u_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_terminal * S ((S (S bls_index_kmcpx_right)) * bpvi_v_bls_kmcpx_right_power) + (bls_power_kmcpx_right))) /\ forall bpvi_j_bls_kmcpx_right_power. (exists bpvi_product_gap_bls_kmcpx_right_power. bpvi_product_gap_bls_kmcpx_right_power + S bpvi_j_bls_kmcpx_right_power = S bls_index_kmcpx_right) -> exists bpvi_factor_bls_kmcpx_right_power bpvi_partial_bls_kmcpx_right_power bpvi_successor_bls_kmcpx_right_power. ((((exists bpvi_h_bls_kmcpx_right_power_factor. bpvi_h_bls_kmcpx_right_power_factor + S (bpvi_factor_bls_kmcpx_right_power) = S ((S (bpvi_j_bls_kmcpx_right_power)) * bpvi_c_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_factor. bpvi_b_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_factor * S ((S (bpvi_j_bls_kmcpx_right_power)) * bpvi_c_bls_kmcpx_right_power) + (bpvi_factor_bls_kmcpx_right_power))) /\ ((((exists bpvi_h_bls_kmcpx_right_power_partial. bpvi_h_bls_kmcpx_right_power_partial + S (bpvi_partial_bls_kmcpx_right_power) = S ((S (bpvi_j_bls_kmcpx_right_power)) * bpvi_v_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_partial. bpvi_u_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_partial * S ((S (bpvi_j_bls_kmcpx_right_power)) * bpvi_v_bls_kmcpx_right_power) + (bpvi_partial_bls_kmcpx_right_power))) /\ ((((exists bpvi_h_bls_kmcpx_right_power_successor. bpvi_h_bls_kmcpx_right_power_successor + S (bpvi_successor_bls_kmcpx_right_power) = S ((S (S bpvi_j_bls_kmcpx_right_power)) * bpvi_v_bls_kmcpx_right_power)) /\ exists bpvi_q_bls_kmcpx_right_power_successor. bpvi_u_bls_kmcpx_right_power = bpvi_q_bls_kmcpx_right_power_successor * S ((S (S bpvi_j_bls_kmcpx_right_power)) * bpvi_v_bls_kmcpx_right_power) + (bpvi_successor_bls_kmcpx_right_power))) /\ bpvi_successor_bls_kmcpx_right_power = bpvi_partial_bls_kmcpx_right_power * bpvi_factor_bls_kmcpx_right_power)))))))) /\ ((((exists ff_h_bls_kmcpx_right_quotient_entry. ff_h_bls_kmcpx_right_quotient_entry + S (bls_quotient_kmcpx_right) = S ((S (bls_index_kmcpx_right)) * rc)) /\ exists ff_q_bls_kmcpx_right_quotient_entry. rb = ff_q_bls_kmcpx_right_quotient_entry * S ((S (bls_index_kmcpx_right)) * rc) + (bls_quotient_kmcpx_right))) /\ ((b = bls_power_kmcpx_right * bls_quotient_kmcpx_right + bls_remainder_kmcpx_right /\ exists bls_remainder_gap_kmcpx_right_division. bls_remainder_gap_kmcpx_right_division + S (bls_remainder_kmcpx_right) = bls_power_kmcpx_right))))) -> (forall bls_index_kmcpx_total. (exists bls_gap_kmcpx_total_bound. bls_gap_kmcpx_total_bound + S (bls_index_kmcpx_total) = (l)) -> exists bls_power_kmcpx_total bls_quotient_kmcpx_total bls_remainder_kmcpx_total. ((exists bpvi_b_bls_kmcpx_total_power bpvi_c_bls_kmcpx_total_power. ((forall bpvi_i_bls_kmcpx_total_power. (exists bpvi_repeat_gap_bls_kmcpx_total_power. bpvi_repeat_gap_bls_kmcpx_total_power + S bpvi_i_bls_kmcpx_total_power = S bls_index_kmcpx_total) -> (((exists bpvi_h_bls_kmcpx_total_power_repeat. bpvi_h_bls_kmcpx_total_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_total_power)) * bpvi_c_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_repeat. bpvi_b_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_repeat * S ((S (bpvi_i_bls_kmcpx_total_power)) * bpvi_c_bls_kmcpx_total_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_total_power bpvi_v_bls_kmcpx_total_power. ((((exists bpvi_h_bls_kmcpx_total_power_start. bpvi_h_bls_kmcpx_total_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_start. bpvi_u_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_total_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_total_power_terminal. bpvi_h_bls_kmcpx_total_power_terminal + S (bls_power_kmcpx_total) = S ((S (S bls_index_kmcpx_total)) * bpvi_v_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_terminal. bpvi_u_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_terminal * S ((S (S bls_index_kmcpx_total)) * bpvi_v_bls_kmcpx_total_power) + (bls_power_kmcpx_total))) /\ forall bpvi_j_bls_kmcpx_total_power. (exists bpvi_product_gap_bls_kmcpx_total_power. bpvi_product_gap_bls_kmcpx_total_power + S bpvi_j_bls_kmcpx_total_power = S bls_index_kmcpx_total) -> exists bpvi_factor_bls_kmcpx_total_power bpvi_partial_bls_kmcpx_total_power bpvi_successor_bls_kmcpx_total_power. ((((exists bpvi_h_bls_kmcpx_total_power_factor. bpvi_h_bls_kmcpx_total_power_factor + S (bpvi_factor_bls_kmcpx_total_power) = S ((S (bpvi_j_bls_kmcpx_total_power)) * bpvi_c_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_factor. bpvi_b_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_factor * S ((S (bpvi_j_bls_kmcpx_total_power)) * bpvi_c_bls_kmcpx_total_power) + (bpvi_factor_bls_kmcpx_total_power))) /\ ((((exists bpvi_h_bls_kmcpx_total_power_partial. bpvi_h_bls_kmcpx_total_power_partial + S (bpvi_partial_bls_kmcpx_total_power) = S ((S (bpvi_j_bls_kmcpx_total_power)) * bpvi_v_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_partial. bpvi_u_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_partial * S ((S (bpvi_j_bls_kmcpx_total_power)) * bpvi_v_bls_kmcpx_total_power) + (bpvi_partial_bls_kmcpx_total_power))) /\ ((((exists bpvi_h_bls_kmcpx_total_power_successor. bpvi_h_bls_kmcpx_total_power_successor + S (bpvi_successor_bls_kmcpx_total_power) = S ((S (S bpvi_j_bls_kmcpx_total_power)) * bpvi_v_bls_kmcpx_total_power)) /\ exists bpvi_q_bls_kmcpx_total_power_successor. bpvi_u_bls_kmcpx_total_power = bpvi_q_bls_kmcpx_total_power_successor * S ((S (S bpvi_j_bls_kmcpx_total_power)) * bpvi_v_bls_kmcpx_total_power) + (bpvi_successor_bls_kmcpx_total_power))) /\ bpvi_successor_bls_kmcpx_total_power = bpvi_partial_bls_kmcpx_total_power * bpvi_factor_bls_kmcpx_total_power)))))))) /\ ((((exists ff_h_bls_kmcpx_total_quotient_entry. ff_h_bls_kmcpx_total_quotient_entry + S (bls_quotient_kmcpx_total) = S ((S (bls_index_kmcpx_total)) * tc)) /\ exists ff_q_bls_kmcpx_total_quotient_entry. tb = ff_q_bls_kmcpx_total_quotient_entry * S ((S (bls_index_kmcpx_total)) * tc) + (bls_quotient_kmcpx_total))) /\ ((a + b = bls_power_kmcpx_total * bls_quotient_kmcpx_total + bls_remainder_kmcpx_total /\ exists bls_remainder_gap_kmcpx_total_division. bls_remainder_gap_kmcpx_total_division + S (bls_remainder_kmcpx_total) = bls_power_kmcpx_total))))) -> exists cb cc. (forall kmc_index_kmcpx_result. (exists bcf_lt_gap_kmcpx_result_bound. bcf_lt_gap_kmcpx_result_bound + S (kmc_index_kmcpx_result) = l) -> exists kmc_left_kmcpx_result kmc_right_kmcpx_result kmc_total_kmcpx_result kmc_bit_kmcpx_result. (((exists fs_h_kmcpx_result_left. fs_h_kmcpx_result_left + S (kmc_left_kmcpx_result) = S ((S (kmc_index_kmcpx_result)) * lc)) /\ exists fs_q_kmcpx_result_left. lb = fs_q_kmcpx_result_left * S ((S (kmc_index_kmcpx_result)) * lc) + (kmc_left_kmcpx_result))) /\ ((((exists fs_h_kmcpx_result_right. fs_h_kmcpx_result_right + S (kmc_right_kmcpx_result) = S ((S (kmc_index_kmcpx_result)) * rc)) /\ exists fs_q_kmcpx_result_right. rb = fs_q_kmcpx_result_right * S ((S (kmc_index_kmcpx_result)) * rc) + (kmc_right_kmcpx_result))) /\ ((((exists fs_h_kmcpx_result_total. fs_h_kmcpx_result_total + S (kmc_total_kmcpx_result) = S ((S (kmc_index_kmcpx_result)) * tc)) /\ exists fs_q_kmcpx_result_total. tb = fs_q_kmcpx_result_total * S ((S (kmc_index_kmcpx_result)) * tc) + (kmc_total_kmcpx_result))) /\ ((((exists fs_h_kmcpx_result_bit. fs_h_kmcpx_result_bit + S (kmc_bit_kmcpx_result) = S ((S (kmc_index_kmcpx_result)) * cc)) /\ exists fs_q_kmcpx_result_bit. cb = fs_q_kmcpx_result_bit * S ((S (kmc_index_kmcpx_result)) * cc) + (kmc_bit_kmcpx_result))) /\ (((kmc_bit_kmcpx_result = 0 /\ kmc_total_kmcpx_result = kmc_left_kmcpx_result + kmc_right_kmcpx_result) \/ (kmc_bit_kmcpx_result = 1 /\ kmc_total_kmcpx_result = S (kmc_left_kmcpx_result + kmc_right_kmcpx_result))))))))

Constructive proof overview

Generated structural guide

Three arbitrary power-quotient prefixes admit a beta-coded additive carry prefix.

The unchanged tactic script uses 6 declared prerequisites and contains 94 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

add_eq_zero_right Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized KU0006 add_quotient_carry_choice KU0007 add_quotient_carry_prefix_extend

Direct dependents

KU000C kummer_binomial_carry_bit_count

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

94 script commands · 15 reading checkpoints · 6 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.

Named ingredients (2)
add quotient carry choiceadd quotient carry prefix extend

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

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro lb
  5. L5
    intro lc
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro tb
  9. L9
    intro tc
02Induction on lL10–13

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

  1. L10
    induction l
  2. L11
    intro hleft
  3. L12
    intro hright
  4. L13
    intro htotal
03Construct an explicit witnessL14–15

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

  1. L14
    exists 0
  2. L15
    exists 0
04Fix variables and assumptionsL16–17

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

  1. L16
    intro i
  2. L17
    intro hi
05Separate the logical casesL18–19

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

  1. L18
    exfalso
  2. L19
    cases hi
06Establish hzeroL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L20
    have hzero : S i = 0
  2. L21
    specialize add_eq_zero_right x
  3. L22
    specialize add_eq_zero_right (S i)
  4. L23
    apply add_eq_zero_right
  5. L24
    exact hi_witness
  6. L25
    specialize succ_ne_zero i
  7. L26
    apply succ_ne_zero
  8. L27
    exact hzero
  9. L28
    intro hleft
  10. L29
    intro hright
07Fix variables and assumptionsL30–30

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

  1. L30
    intro htotal
08Establish hleft_prefixL31–39

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

  1. L31
    have hleft_prefix : PowerQuotPrefix(p,a,lb,lc,l)Definitions: PowerQuotPrefix
  2. L32
    intro i
  3. L33
    intro hi
  4. L34
    specialize hleft i
  5. L35
    apply hleft
  6. L36
    specialize le_succ (S i)
  7. L37
    specialize le_succ l
  8. L38
    apply le_succ
  9. L39
    exact hi
09Establish hright_prefixL40–48

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

  1. L40
    have hright_prefix : PowerQuotPrefix(p,b,rb,rc,l)Definitions: PowerQuotPrefix
  2. L41
    intro i
  3. L42
    intro hi
  4. L43
    specialize hright i
  5. L44
    apply hright
  6. L45
    specialize le_succ (S i)
  7. L46
    specialize le_succ l
  8. L47
    apply le_succ
  9. L48
    exact hi
10Establish htotal_prefixL49–57

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

  1. L49
    have htotal_prefix : PowerQuotPrefix(p,a + b,tb,tc,l)Definitions: PowerQuotPrefix
  2. L50
    intro i
  3. L51
    intro hi
  4. L52
    specialize htotal i
  5. L53
    apply htotal
  6. L54
    specialize le_succ (S i)
  7. L55
    specialize le_succ l
  8. L56
    apply le_succ
  9. L57
    exact hi
11Establish hprefixL58–62

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

  1. L58
    have hprefix : ∃ cb. ∃ cc. ∀ kmc_index_kmcpx_previous. Lt(kmc_index_kmcpx_previous,l) → ∃ x. ∃ y. ∃ z. ∃ n. BetaAt(lb,lc,kmc_index_kmcpx_previous,x) ∧ (BetaAt(rb,rc,kmc_index_kmcpx_previous,y) ∧ (BetaAt(tb,tc,kmc_index_kmcpx_previous,z) ∧ (BetaAt(cb,cc,kmc_index_kmcpx_previous,n) ∧ (n = 0 ∧ z = x + y ∨ n = 1 ∧ z = S (x + y)))))Definitions: LtBetaAt
  2. L59
    apply IH
  3. L60
    exact hleft_prefix
  4. L61
    exact hright_prefix
  5. L62
    exact htotal_prefix
12Separate the logical casesL63–64

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

  1. L63
    cases hprefix
  2. L64
    cases hprefix_witness
13Establish hlastL65–74

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

  1. L65
    have hlast : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,l,q) ∧ (BetaAt(rb,rc,l,s) ∧ (BetaAt(tb,tc,l,Q) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s))))Definitions: BetaAt
  2. L66
    specialize add_quotient_carry_choice p
  3. L67
    specialize add_quotient_carry_choice a
  4. L68
    specialize add_quotient_carry_choice b
  5. L69
    specialize add_quotient_carry_choice lb
  6. L70
    specialize add_quotient_carry_choice lc
  7. L71
    specialize add_quotient_carry_choice rb
  8. L72
    specialize add_quotient_carry_choice rc
  9. L73
    specialize add_quotient_carry_choice tb
  10. L74
    specialize add_quotient_carry_choice tc
14Use earlier factsL75–84

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

  1. L75
    specialize add_quotient_carry_choice (S l)
  2. L76
    specialize add_quotient_carry_choice l
  3. L77
    apply add_quotient_carry_choice
  4. L78
    exact hleft
  5. L79
    exact hright
  6. L80
    exact htotal
  7. L81
    specialize le_refl (S l)
  8. L82
    exact le_refl
  9. L83
    specialize add_quotient_carry_prefix_extend lb
  10. L84
    specialize add_quotient_carry_prefix_extend lc
15Use earlier factsL85–94

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

  1. L85
    specialize add_quotient_carry_prefix_extend rb
  2. L86
    specialize add_quotient_carry_prefix_extend rc
  3. L87
    specialize add_quotient_carry_prefix_extend tb
  4. L88
    specialize add_quotient_carry_prefix_extend tc
  5. L89
    specialize add_quotient_carry_prefix_extend x
  6. L90
    specialize add_quotient_carry_prefix_extend x1
  7. L91
    specialize add_quotient_carry_prefix_extend l
  8. L92
    apply add_quotient_carry_prefix_extend
  9. L93
    exact hprefix_witness_witness
  10. L94
    exact hlast

Library-wide reading audit

Original exact command ledger · 94 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro lb
  5. 0005intro lc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro tb
  9. 0009intro tc
  10. 0010induction l
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013intro htotal
  14. 0014exists 0
  15. 0015exists 0
  16. 0016intro i
  17. 0017intro hi
  18. 0018exfalso
  19. 0019cases hi
  20. 0020have hzero : S i = 0
  21. 0021specialize add_eq_zero_right x
  22. 0022specialize add_eq_zero_right (S i)
  23. 0023apply add_eq_zero_right
  24. 0024exact hi_witness
  25. 0025specialize succ_ne_zero i
  26. 0026apply succ_ne_zero
  27. 0027exact hzero
  28. 0028intro hleft
  29. 0029intro hright
  30. 0030intro htotal
  31. 0031have hleft_prefix : forall bls_index_kmcpx_left_previous. (exists bls_gap_kmcpx_left_previous_bound. bls_gap_kmcpx_left_previous_bound + S (bls_index_kmcpx_left_previous) = (l)) -> exists bls_power_kmcpx_left_previous bls_quotient_kmcpx_left_previous bls_remainder_kmcpx_left_previous. ((exists bpvi_b_bls_kmcpx_left_previous_power bpvi_c_bls_kmcpx_left_previous_power. ((forall bpvi_i_bls_kmcpx_left_previous_power. (exists bpvi_repeat_gap_bls_kmcpx_left_previous_power. bpvi_repeat_gap_bls_kmcpx_left_previous_power + S bpvi_i_bls_kmcpx_left_previous_power = S bls_index_kmcpx_left_previous) -> (((exists bpvi_h_bls_kmcpx_left_previous_power_repeat. bpvi_h_bls_kmcpx_left_previous_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_left_previous_power)) * bpvi_c_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_repeat. bpvi_b_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_repeat * S ((S (bpvi_i_bls_kmcpx_left_previous_power)) * bpvi_c_bls_kmcpx_left_previous_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_left_previous_power bpvi_v_bls_kmcpx_left_previous_power. ((((exists bpvi_h_bls_kmcpx_left_previous_power_start. bpvi_h_bls_kmcpx_left_previous_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_start. bpvi_u_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_left_previous_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_left_previous_power_terminal. bpvi_h_bls_kmcpx_left_previous_power_terminal + S (bls_power_kmcpx_left_previous) = S ((S (S bls_index_kmcpx_left_previous)) * bpvi_v_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_terminal. bpvi_u_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_terminal * S ((S (S bls_index_kmcpx_left_previous)) * bpvi_v_bls_kmcpx_left_previous_power) + (bls_power_kmcpx_left_previous))) /\ forall bpvi_j_bls_kmcpx_left_previous_power. (exists bpvi_product_gap_bls_kmcpx_left_previous_power. bpvi_product_gap_bls_kmcpx_left_previous_power + S bpvi_j_bls_kmcpx_left_previous_power = S bls_index_kmcpx_left_previous) -> exists bpvi_factor_bls_kmcpx_left_previous_power bpvi_partial_bls_kmcpx_left_previous_power bpvi_successor_bls_kmcpx_left_previous_power. ((((exists bpvi_h_bls_kmcpx_left_previous_power_factor. bpvi_h_bls_kmcpx_left_previous_power_factor + S (bpvi_factor_bls_kmcpx_left_previous_power) = S ((S (bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_c_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_factor. bpvi_b_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_factor * S ((S (bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_c_bls_kmcpx_left_previous_power) + (bpvi_factor_bls_kmcpx_left_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_left_previous_power_partial. bpvi_h_bls_kmcpx_left_previous_power_partial + S (bpvi_partial_bls_kmcpx_left_previous_power) = S ((S (bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_v_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_partial. bpvi_u_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_partial * S ((S (bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_v_bls_kmcpx_left_previous_power) + (bpvi_partial_bls_kmcpx_left_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_left_previous_power_successor. bpvi_h_bls_kmcpx_left_previous_power_successor + S (bpvi_successor_bls_kmcpx_left_previous_power) = S ((S (S bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_v_bls_kmcpx_left_previous_power)) /\ exists bpvi_q_bls_kmcpx_left_previous_power_successor. bpvi_u_bls_kmcpx_left_previous_power = bpvi_q_bls_kmcpx_left_previous_power_successor * S ((S (S bpvi_j_bls_kmcpx_left_previous_power)) * bpvi_v_bls_kmcpx_left_previous_power) + (bpvi_successor_bls_kmcpx_left_previous_power))) /\ bpvi_successor_bls_kmcpx_left_previous_power = bpvi_partial_bls_kmcpx_left_previous_power * bpvi_factor_bls_kmcpx_left_previous_power)))))))) /\ ((((exists ff_h_bls_kmcpx_left_previous_quotient_entry. ff_h_bls_kmcpx_left_previous_quotient_entry + S (bls_quotient_kmcpx_left_previous) = S ((S (bls_index_kmcpx_left_previous)) * lc)) /\ exists ff_q_bls_kmcpx_left_previous_quotient_entry. lb = ff_q_bls_kmcpx_left_previous_quotient_entry * S ((S (bls_index_kmcpx_left_previous)) * lc) + (bls_quotient_kmcpx_left_previous))) /\ ((a = bls_power_kmcpx_left_previous * bls_quotient_kmcpx_left_previous + bls_remainder_kmcpx_left_previous /\ exists bls_remainder_gap_kmcpx_left_previous_division. bls_remainder_gap_kmcpx_left_previous_division + S (bls_remainder_kmcpx_left_previous) = bls_power_kmcpx_left_previous))))
  32. 0032intro i
  33. 0033intro hi
  34. 0034specialize hleft i
  35. 0035apply hleft
  36. 0036specialize le_succ (S i)
  37. 0037specialize le_succ l
  38. 0038apply le_succ
  39. 0039exact hi
  40. 0040have hright_prefix : forall bls_index_kmcpx_right_previous. (exists bls_gap_kmcpx_right_previous_bound. bls_gap_kmcpx_right_previous_bound + S (bls_index_kmcpx_right_previous) = (l)) -> exists bls_power_kmcpx_right_previous bls_quotient_kmcpx_right_previous bls_remainder_kmcpx_right_previous. ((exists bpvi_b_bls_kmcpx_right_previous_power bpvi_c_bls_kmcpx_right_previous_power. ((forall bpvi_i_bls_kmcpx_right_previous_power. (exists bpvi_repeat_gap_bls_kmcpx_right_previous_power. bpvi_repeat_gap_bls_kmcpx_right_previous_power + S bpvi_i_bls_kmcpx_right_previous_power = S bls_index_kmcpx_right_previous) -> (((exists bpvi_h_bls_kmcpx_right_previous_power_repeat. bpvi_h_bls_kmcpx_right_previous_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_right_previous_power)) * bpvi_c_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_repeat. bpvi_b_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_repeat * S ((S (bpvi_i_bls_kmcpx_right_previous_power)) * bpvi_c_bls_kmcpx_right_previous_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_right_previous_power bpvi_v_bls_kmcpx_right_previous_power. ((((exists bpvi_h_bls_kmcpx_right_previous_power_start. bpvi_h_bls_kmcpx_right_previous_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_start. bpvi_u_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_right_previous_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_right_previous_power_terminal. bpvi_h_bls_kmcpx_right_previous_power_terminal + S (bls_power_kmcpx_right_previous) = S ((S (S bls_index_kmcpx_right_previous)) * bpvi_v_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_terminal. bpvi_u_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_terminal * S ((S (S bls_index_kmcpx_right_previous)) * bpvi_v_bls_kmcpx_right_previous_power) + (bls_power_kmcpx_right_previous))) /\ forall bpvi_j_bls_kmcpx_right_previous_power. (exists bpvi_product_gap_bls_kmcpx_right_previous_power. bpvi_product_gap_bls_kmcpx_right_previous_power + S bpvi_j_bls_kmcpx_right_previous_power = S bls_index_kmcpx_right_previous) -> exists bpvi_factor_bls_kmcpx_right_previous_power bpvi_partial_bls_kmcpx_right_previous_power bpvi_successor_bls_kmcpx_right_previous_power. ((((exists bpvi_h_bls_kmcpx_right_previous_power_factor. bpvi_h_bls_kmcpx_right_previous_power_factor + S (bpvi_factor_bls_kmcpx_right_previous_power) = S ((S (bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_c_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_factor. bpvi_b_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_factor * S ((S (bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_c_bls_kmcpx_right_previous_power) + (bpvi_factor_bls_kmcpx_right_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_right_previous_power_partial. bpvi_h_bls_kmcpx_right_previous_power_partial + S (bpvi_partial_bls_kmcpx_right_previous_power) = S ((S (bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_v_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_partial. bpvi_u_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_partial * S ((S (bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_v_bls_kmcpx_right_previous_power) + (bpvi_partial_bls_kmcpx_right_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_right_previous_power_successor. bpvi_h_bls_kmcpx_right_previous_power_successor + S (bpvi_successor_bls_kmcpx_right_previous_power) = S ((S (S bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_v_bls_kmcpx_right_previous_power)) /\ exists bpvi_q_bls_kmcpx_right_previous_power_successor. bpvi_u_bls_kmcpx_right_previous_power = bpvi_q_bls_kmcpx_right_previous_power_successor * S ((S (S bpvi_j_bls_kmcpx_right_previous_power)) * bpvi_v_bls_kmcpx_right_previous_power) + (bpvi_successor_bls_kmcpx_right_previous_power))) /\ bpvi_successor_bls_kmcpx_right_previous_power = bpvi_partial_bls_kmcpx_right_previous_power * bpvi_factor_bls_kmcpx_right_previous_power)))))))) /\ ((((exists ff_h_bls_kmcpx_right_previous_quotient_entry. ff_h_bls_kmcpx_right_previous_quotient_entry + S (bls_quotient_kmcpx_right_previous) = S ((S (bls_index_kmcpx_right_previous)) * rc)) /\ exists ff_q_bls_kmcpx_right_previous_quotient_entry. rb = ff_q_bls_kmcpx_right_previous_quotient_entry * S ((S (bls_index_kmcpx_right_previous)) * rc) + (bls_quotient_kmcpx_right_previous))) /\ ((b = bls_power_kmcpx_right_previous * bls_quotient_kmcpx_right_previous + bls_remainder_kmcpx_right_previous /\ exists bls_remainder_gap_kmcpx_right_previous_division. bls_remainder_gap_kmcpx_right_previous_division + S (bls_remainder_kmcpx_right_previous) = bls_power_kmcpx_right_previous))))
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hright i
  44. 0044apply hright
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ l
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049have htotal_prefix : forall bls_index_kmcpx_total_previous. (exists bls_gap_kmcpx_total_previous_bound. bls_gap_kmcpx_total_previous_bound + S (bls_index_kmcpx_total_previous) = (l)) -> exists bls_power_kmcpx_total_previous bls_quotient_kmcpx_total_previous bls_remainder_kmcpx_total_previous. ((exists bpvi_b_bls_kmcpx_total_previous_power bpvi_c_bls_kmcpx_total_previous_power. ((forall bpvi_i_bls_kmcpx_total_previous_power. (exists bpvi_repeat_gap_bls_kmcpx_total_previous_power. bpvi_repeat_gap_bls_kmcpx_total_previous_power + S bpvi_i_bls_kmcpx_total_previous_power = S bls_index_kmcpx_total_previous) -> (((exists bpvi_h_bls_kmcpx_total_previous_power_repeat. bpvi_h_bls_kmcpx_total_previous_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcpx_total_previous_power)) * bpvi_c_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_repeat. bpvi_b_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_repeat * S ((S (bpvi_i_bls_kmcpx_total_previous_power)) * bpvi_c_bls_kmcpx_total_previous_power) + (p)))) /\ (exists bpvi_u_bls_kmcpx_total_previous_power bpvi_v_bls_kmcpx_total_previous_power. ((((exists bpvi_h_bls_kmcpx_total_previous_power_start. bpvi_h_bls_kmcpx_total_previous_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_start. bpvi_u_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_start * S ((S (0)) * bpvi_v_bls_kmcpx_total_previous_power) + (1))) /\ ((((exists bpvi_h_bls_kmcpx_total_previous_power_terminal. bpvi_h_bls_kmcpx_total_previous_power_terminal + S (bls_power_kmcpx_total_previous) = S ((S (S bls_index_kmcpx_total_previous)) * bpvi_v_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_terminal. bpvi_u_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_terminal * S ((S (S bls_index_kmcpx_total_previous)) * bpvi_v_bls_kmcpx_total_previous_power) + (bls_power_kmcpx_total_previous))) /\ forall bpvi_j_bls_kmcpx_total_previous_power. (exists bpvi_product_gap_bls_kmcpx_total_previous_power. bpvi_product_gap_bls_kmcpx_total_previous_power + S bpvi_j_bls_kmcpx_total_previous_power = S bls_index_kmcpx_total_previous) -> exists bpvi_factor_bls_kmcpx_total_previous_power bpvi_partial_bls_kmcpx_total_previous_power bpvi_successor_bls_kmcpx_total_previous_power. ((((exists bpvi_h_bls_kmcpx_total_previous_power_factor. bpvi_h_bls_kmcpx_total_previous_power_factor + S (bpvi_factor_bls_kmcpx_total_previous_power) = S ((S (bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_c_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_factor. bpvi_b_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_factor * S ((S (bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_c_bls_kmcpx_total_previous_power) + (bpvi_factor_bls_kmcpx_total_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_total_previous_power_partial. bpvi_h_bls_kmcpx_total_previous_power_partial + S (bpvi_partial_bls_kmcpx_total_previous_power) = S ((S (bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_v_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_partial. bpvi_u_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_partial * S ((S (bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_v_bls_kmcpx_total_previous_power) + (bpvi_partial_bls_kmcpx_total_previous_power))) /\ ((((exists bpvi_h_bls_kmcpx_total_previous_power_successor. bpvi_h_bls_kmcpx_total_previous_power_successor + S (bpvi_successor_bls_kmcpx_total_previous_power) = S ((S (S bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_v_bls_kmcpx_total_previous_power)) /\ exists bpvi_q_bls_kmcpx_total_previous_power_successor. bpvi_u_bls_kmcpx_total_previous_power = bpvi_q_bls_kmcpx_total_previous_power_successor * S ((S (S bpvi_j_bls_kmcpx_total_previous_power)) * bpvi_v_bls_kmcpx_total_previous_power) + (bpvi_successor_bls_kmcpx_total_previous_power))) /\ bpvi_successor_bls_kmcpx_total_previous_power = bpvi_partial_bls_kmcpx_total_previous_power * bpvi_factor_bls_kmcpx_total_previous_power)))))))) /\ ((((exists ff_h_bls_kmcpx_total_previous_quotient_entry. ff_h_bls_kmcpx_total_previous_quotient_entry + S (bls_quotient_kmcpx_total_previous) = S ((S (bls_index_kmcpx_total_previous)) * tc)) /\ exists ff_q_bls_kmcpx_total_previous_quotient_entry. tb = ff_q_bls_kmcpx_total_previous_quotient_entry * S ((S (bls_index_kmcpx_total_previous)) * tc) + (bls_quotient_kmcpx_total_previous))) /\ ((a + b = bls_power_kmcpx_total_previous * bls_quotient_kmcpx_total_previous + bls_remainder_kmcpx_total_previous /\ exists bls_remainder_gap_kmcpx_total_previous_division. bls_remainder_gap_kmcpx_total_previous_division + S (bls_remainder_kmcpx_total_previous) = bls_power_kmcpx_total_previous))))
  50. 0050intro i
  51. 0051intro hi
  52. 0052specialize htotal i
  53. 0053apply htotal
  54. 0054specialize le_succ (S i)
  55. 0055specialize le_succ l
  56. 0056apply le_succ
  57. 0057exact hi
  58. 0058have hprefix : exists cb cc. forall kmc_index_kmcpx_previous. (exists bcf_lt_gap_kmcpx_previous_bound. bcf_lt_gap_kmcpx_previous_bound + S (kmc_index_kmcpx_previous) = l) -> exists kmc_left_kmcpx_previous kmc_right_kmcpx_previous kmc_total_kmcpx_previous kmc_bit_kmcpx_previous. (((exists fs_h_kmcpx_previous_left. fs_h_kmcpx_previous_left + S (kmc_left_kmcpx_previous) = S ((S (kmc_index_kmcpx_previous)) * lc)) /\ exists fs_q_kmcpx_previous_left. lb = fs_q_kmcpx_previous_left * S ((S (kmc_index_kmcpx_previous)) * lc) + (kmc_left_kmcpx_previous))) /\ ((((exists fs_h_kmcpx_previous_right. fs_h_kmcpx_previous_right + S (kmc_right_kmcpx_previous) = S ((S (kmc_index_kmcpx_previous)) * rc)) /\ exists fs_q_kmcpx_previous_right. rb = fs_q_kmcpx_previous_right * S ((S (kmc_index_kmcpx_previous)) * rc) + (kmc_right_kmcpx_previous))) /\ ((((exists fs_h_kmcpx_previous_total. fs_h_kmcpx_previous_total + S (kmc_total_kmcpx_previous) = S ((S (kmc_index_kmcpx_previous)) * tc)) /\ exists fs_q_kmcpx_previous_total. tb = fs_q_kmcpx_previous_total * S ((S (kmc_index_kmcpx_previous)) * tc) + (kmc_total_kmcpx_previous))) /\ ((((exists fs_h_kmcpx_previous_bit. fs_h_kmcpx_previous_bit + S (kmc_bit_kmcpx_previous) = S ((S (kmc_index_kmcpx_previous)) * cc)) /\ exists fs_q_kmcpx_previous_bit. cb = fs_q_kmcpx_previous_bit * S ((S (kmc_index_kmcpx_previous)) * cc) + (kmc_bit_kmcpx_previous))) /\ (((kmc_bit_kmcpx_previous = 0 /\ kmc_total_kmcpx_previous = kmc_left_kmcpx_previous + kmc_right_kmcpx_previous) \/ (kmc_bit_kmcpx_previous = 1 /\ kmc_total_kmcpx_previous = S (kmc_left_kmcpx_previous + kmc_right_kmcpx_previous)))))))
  59. 0059apply IH
  60. 0060exact hleft_prefix
  61. 0061exact hright_prefix
  62. 0062exact htotal_prefix
  63. 0063cases hprefix
  64. 0064cases hprefix_witness
  65. 0065have hlast : exists q s Q bit. (((exists fs_h_kmcpx_last_left. fs_h_kmcpx_last_left + S (q) = S ((S (l)) * lc)) /\ exists fs_q_kmcpx_last_left. lb = fs_q_kmcpx_last_left * S ((S (l)) * lc) + (q))) /\ ((((exists fs_h_kmcpx_last_right. fs_h_kmcpx_last_right + S (s) = S ((S (l)) * rc)) /\ exists fs_q_kmcpx_last_right. rb = fs_q_kmcpx_last_right * S ((S (l)) * rc) + (s))) /\ ((((exists fs_h_kmcpx_last_total. fs_h_kmcpx_last_total + S (Q) = S ((S (l)) * tc)) /\ exists fs_q_kmcpx_last_total. tb = fs_q_kmcpx_last_total * S ((S (l)) * tc) + (Q))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s))))))
  66. 0066specialize add_quotient_carry_choice p
  67. 0067specialize add_quotient_carry_choice a
  68. 0068specialize add_quotient_carry_choice b
  69. 0069specialize add_quotient_carry_choice lb
  70. 0070specialize add_quotient_carry_choice lc
  71. 0071specialize add_quotient_carry_choice rb
  72. 0072specialize add_quotient_carry_choice rc
  73. 0073specialize add_quotient_carry_choice tb
  74. 0074specialize add_quotient_carry_choice tc
  75. 0075specialize add_quotient_carry_choice (S l)
  76. 0076specialize add_quotient_carry_choice l
  77. 0077apply add_quotient_carry_choice
  78. 0078exact hleft
  79. 0079exact hright
  80. 0080exact htotal
  81. 0081specialize le_refl (S l)
  82. 0082exact le_refl
  83. 0083specialize add_quotient_carry_prefix_extend lb
  84. 0084specialize add_quotient_carry_prefix_extend lc
  85. 0085specialize add_quotient_carry_prefix_extend rb
  86. 0086specialize add_quotient_carry_prefix_extend rc
  87. 0087specialize add_quotient_carry_prefix_extend tb
  88. 0088specialize add_quotient_carry_prefix_extend tc
  89. 0089specialize add_quotient_carry_prefix_extend x
  90. 0090specialize add_quotient_carry_prefix_extend x1
  91. 0091specialize add_quotient_carry_prefix_extend l
  92. 0092apply add_quotient_carry_prefix_extend
  93. 0093exact hprefix_witness_witness
  94. 0094exact hlast