KU0006

add_quotient_carry_choice

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

Three arbitrary power-quotient prefixes admit a constructive pointwise carry bit.

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 i. (forall bls_index_kmcqc_left. (exists bls_gap_kmcqc_left_bound. bls_gap_kmcqc_left_bound + S (bls_index_kmcqc_left) = (l)) -> exists bls_power_kmcqc_left bls_quotient_kmcqc_left bls_remainder_kmcqc_left. ((exists bpvi_b_bls_kmcqc_left_power bpvi_c_bls_kmcqc_left_power. ((forall bpvi_i_bls_kmcqc_left_power. (exists bpvi_repeat_gap_bls_kmcqc_left_power. bpvi_repeat_gap_bls_kmcqc_left_power + S bpvi_i_bls_kmcqc_left_power = S bls_index_kmcqc_left) -> (((exists bpvi_h_bls_kmcqc_left_power_repeat. bpvi_h_bls_kmcqc_left_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcqc_left_power)) * bpvi_c_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_repeat. bpvi_b_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_repeat * S ((S (bpvi_i_bls_kmcqc_left_power)) * bpvi_c_bls_kmcqc_left_power) + (p)))) /\ (exists bpvi_u_bls_kmcqc_left_power bpvi_v_bls_kmcqc_left_power. ((((exists bpvi_h_bls_kmcqc_left_power_start. bpvi_h_bls_kmcqc_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_start. bpvi_u_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_start * S ((S (0)) * bpvi_v_bls_kmcqc_left_power) + (1))) /\ ((((exists bpvi_h_bls_kmcqc_left_power_terminal. bpvi_h_bls_kmcqc_left_power_terminal + S (bls_power_kmcqc_left) = S ((S (S bls_index_kmcqc_left)) * bpvi_v_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_terminal. bpvi_u_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_terminal * S ((S (S bls_index_kmcqc_left)) * bpvi_v_bls_kmcqc_left_power) + (bls_power_kmcqc_left))) /\ forall bpvi_j_bls_kmcqc_left_power. (exists bpvi_product_gap_bls_kmcqc_left_power. bpvi_product_gap_bls_kmcqc_left_power + S bpvi_j_bls_kmcqc_left_power = S bls_index_kmcqc_left) -> exists bpvi_factor_bls_kmcqc_left_power bpvi_partial_bls_kmcqc_left_power bpvi_successor_bls_kmcqc_left_power. ((((exists bpvi_h_bls_kmcqc_left_power_factor. bpvi_h_bls_kmcqc_left_power_factor + S (bpvi_factor_bls_kmcqc_left_power) = S ((S (bpvi_j_bls_kmcqc_left_power)) * bpvi_c_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_factor. bpvi_b_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_factor * S ((S (bpvi_j_bls_kmcqc_left_power)) * bpvi_c_bls_kmcqc_left_power) + (bpvi_factor_bls_kmcqc_left_power))) /\ ((((exists bpvi_h_bls_kmcqc_left_power_partial. bpvi_h_bls_kmcqc_left_power_partial + S (bpvi_partial_bls_kmcqc_left_power) = S ((S (bpvi_j_bls_kmcqc_left_power)) * bpvi_v_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_partial. bpvi_u_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_partial * S ((S (bpvi_j_bls_kmcqc_left_power)) * bpvi_v_bls_kmcqc_left_power) + (bpvi_partial_bls_kmcqc_left_power))) /\ ((((exists bpvi_h_bls_kmcqc_left_power_successor. bpvi_h_bls_kmcqc_left_power_successor + S (bpvi_successor_bls_kmcqc_left_power) = S ((S (S bpvi_j_bls_kmcqc_left_power)) * bpvi_v_bls_kmcqc_left_power)) /\ exists bpvi_q_bls_kmcqc_left_power_successor. bpvi_u_bls_kmcqc_left_power = bpvi_q_bls_kmcqc_left_power_successor * S ((S (S bpvi_j_bls_kmcqc_left_power)) * bpvi_v_bls_kmcqc_left_power) + (bpvi_successor_bls_kmcqc_left_power))) /\ bpvi_successor_bls_kmcqc_left_power = bpvi_partial_bls_kmcqc_left_power * bpvi_factor_bls_kmcqc_left_power)))))))) /\ ((((exists ff_h_bls_kmcqc_left_quotient_entry. ff_h_bls_kmcqc_left_quotient_entry + S (bls_quotient_kmcqc_left) = S ((S (bls_index_kmcqc_left)) * lc)) /\ exists ff_q_bls_kmcqc_left_quotient_entry. lb = ff_q_bls_kmcqc_left_quotient_entry * S ((S (bls_index_kmcqc_left)) * lc) + (bls_quotient_kmcqc_left))) /\ ((a = bls_power_kmcqc_left * bls_quotient_kmcqc_left + bls_remainder_kmcqc_left /\ exists bls_remainder_gap_kmcqc_left_division. bls_remainder_gap_kmcqc_left_division + S (bls_remainder_kmcqc_left) = bls_power_kmcqc_left))))) -> (forall bls_index_kmcqc_right. (exists bls_gap_kmcqc_right_bound. bls_gap_kmcqc_right_bound + S (bls_index_kmcqc_right) = (l)) -> exists bls_power_kmcqc_right bls_quotient_kmcqc_right bls_remainder_kmcqc_right. ((exists bpvi_b_bls_kmcqc_right_power bpvi_c_bls_kmcqc_right_power. ((forall bpvi_i_bls_kmcqc_right_power. (exists bpvi_repeat_gap_bls_kmcqc_right_power. bpvi_repeat_gap_bls_kmcqc_right_power + S bpvi_i_bls_kmcqc_right_power = S bls_index_kmcqc_right) -> (((exists bpvi_h_bls_kmcqc_right_power_repeat. bpvi_h_bls_kmcqc_right_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcqc_right_power)) * bpvi_c_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_repeat. bpvi_b_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_repeat * S ((S (bpvi_i_bls_kmcqc_right_power)) * bpvi_c_bls_kmcqc_right_power) + (p)))) /\ (exists bpvi_u_bls_kmcqc_right_power bpvi_v_bls_kmcqc_right_power. ((((exists bpvi_h_bls_kmcqc_right_power_start. bpvi_h_bls_kmcqc_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_start. bpvi_u_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_start * S ((S (0)) * bpvi_v_bls_kmcqc_right_power) + (1))) /\ ((((exists bpvi_h_bls_kmcqc_right_power_terminal. bpvi_h_bls_kmcqc_right_power_terminal + S (bls_power_kmcqc_right) = S ((S (S bls_index_kmcqc_right)) * bpvi_v_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_terminal. bpvi_u_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_terminal * S ((S (S bls_index_kmcqc_right)) * bpvi_v_bls_kmcqc_right_power) + (bls_power_kmcqc_right))) /\ forall bpvi_j_bls_kmcqc_right_power. (exists bpvi_product_gap_bls_kmcqc_right_power. bpvi_product_gap_bls_kmcqc_right_power + S bpvi_j_bls_kmcqc_right_power = S bls_index_kmcqc_right) -> exists bpvi_factor_bls_kmcqc_right_power bpvi_partial_bls_kmcqc_right_power bpvi_successor_bls_kmcqc_right_power. ((((exists bpvi_h_bls_kmcqc_right_power_factor. bpvi_h_bls_kmcqc_right_power_factor + S (bpvi_factor_bls_kmcqc_right_power) = S ((S (bpvi_j_bls_kmcqc_right_power)) * bpvi_c_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_factor. bpvi_b_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_factor * S ((S (bpvi_j_bls_kmcqc_right_power)) * bpvi_c_bls_kmcqc_right_power) + (bpvi_factor_bls_kmcqc_right_power))) /\ ((((exists bpvi_h_bls_kmcqc_right_power_partial. bpvi_h_bls_kmcqc_right_power_partial + S (bpvi_partial_bls_kmcqc_right_power) = S ((S (bpvi_j_bls_kmcqc_right_power)) * bpvi_v_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_partial. bpvi_u_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_partial * S ((S (bpvi_j_bls_kmcqc_right_power)) * bpvi_v_bls_kmcqc_right_power) + (bpvi_partial_bls_kmcqc_right_power))) /\ ((((exists bpvi_h_bls_kmcqc_right_power_successor. bpvi_h_bls_kmcqc_right_power_successor + S (bpvi_successor_bls_kmcqc_right_power) = S ((S (S bpvi_j_bls_kmcqc_right_power)) * bpvi_v_bls_kmcqc_right_power)) /\ exists bpvi_q_bls_kmcqc_right_power_successor. bpvi_u_bls_kmcqc_right_power = bpvi_q_bls_kmcqc_right_power_successor * S ((S (S bpvi_j_bls_kmcqc_right_power)) * bpvi_v_bls_kmcqc_right_power) + (bpvi_successor_bls_kmcqc_right_power))) /\ bpvi_successor_bls_kmcqc_right_power = bpvi_partial_bls_kmcqc_right_power * bpvi_factor_bls_kmcqc_right_power)))))))) /\ ((((exists ff_h_bls_kmcqc_right_quotient_entry. ff_h_bls_kmcqc_right_quotient_entry + S (bls_quotient_kmcqc_right) = S ((S (bls_index_kmcqc_right)) * rc)) /\ exists ff_q_bls_kmcqc_right_quotient_entry. rb = ff_q_bls_kmcqc_right_quotient_entry * S ((S (bls_index_kmcqc_right)) * rc) + (bls_quotient_kmcqc_right))) /\ ((b = bls_power_kmcqc_right * bls_quotient_kmcqc_right + bls_remainder_kmcqc_right /\ exists bls_remainder_gap_kmcqc_right_division. bls_remainder_gap_kmcqc_right_division + S (bls_remainder_kmcqc_right) = bls_power_kmcqc_right))))) -> (forall bls_index_kmcqc_total. (exists bls_gap_kmcqc_total_bound. bls_gap_kmcqc_total_bound + S (bls_index_kmcqc_total) = (l)) -> exists bls_power_kmcqc_total bls_quotient_kmcqc_total bls_remainder_kmcqc_total. ((exists bpvi_b_bls_kmcqc_total_power bpvi_c_bls_kmcqc_total_power. ((forall bpvi_i_bls_kmcqc_total_power. (exists bpvi_repeat_gap_bls_kmcqc_total_power. bpvi_repeat_gap_bls_kmcqc_total_power + S bpvi_i_bls_kmcqc_total_power = S bls_index_kmcqc_total) -> (((exists bpvi_h_bls_kmcqc_total_power_repeat. bpvi_h_bls_kmcqc_total_power_repeat + S (p) = S ((S (bpvi_i_bls_kmcqc_total_power)) * bpvi_c_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_repeat. bpvi_b_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_repeat * S ((S (bpvi_i_bls_kmcqc_total_power)) * bpvi_c_bls_kmcqc_total_power) + (p)))) /\ (exists bpvi_u_bls_kmcqc_total_power bpvi_v_bls_kmcqc_total_power. ((((exists bpvi_h_bls_kmcqc_total_power_start. bpvi_h_bls_kmcqc_total_power_start + S (1) = S ((S (0)) * bpvi_v_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_start. bpvi_u_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_start * S ((S (0)) * bpvi_v_bls_kmcqc_total_power) + (1))) /\ ((((exists bpvi_h_bls_kmcqc_total_power_terminal. bpvi_h_bls_kmcqc_total_power_terminal + S (bls_power_kmcqc_total) = S ((S (S bls_index_kmcqc_total)) * bpvi_v_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_terminal. bpvi_u_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_terminal * S ((S (S bls_index_kmcqc_total)) * bpvi_v_bls_kmcqc_total_power) + (bls_power_kmcqc_total))) /\ forall bpvi_j_bls_kmcqc_total_power. (exists bpvi_product_gap_bls_kmcqc_total_power. bpvi_product_gap_bls_kmcqc_total_power + S bpvi_j_bls_kmcqc_total_power = S bls_index_kmcqc_total) -> exists bpvi_factor_bls_kmcqc_total_power bpvi_partial_bls_kmcqc_total_power bpvi_successor_bls_kmcqc_total_power. ((((exists bpvi_h_bls_kmcqc_total_power_factor. bpvi_h_bls_kmcqc_total_power_factor + S (bpvi_factor_bls_kmcqc_total_power) = S ((S (bpvi_j_bls_kmcqc_total_power)) * bpvi_c_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_factor. bpvi_b_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_factor * S ((S (bpvi_j_bls_kmcqc_total_power)) * bpvi_c_bls_kmcqc_total_power) + (bpvi_factor_bls_kmcqc_total_power))) /\ ((((exists bpvi_h_bls_kmcqc_total_power_partial. bpvi_h_bls_kmcqc_total_power_partial + S (bpvi_partial_bls_kmcqc_total_power) = S ((S (bpvi_j_bls_kmcqc_total_power)) * bpvi_v_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_partial. bpvi_u_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_partial * S ((S (bpvi_j_bls_kmcqc_total_power)) * bpvi_v_bls_kmcqc_total_power) + (bpvi_partial_bls_kmcqc_total_power))) /\ ((((exists bpvi_h_bls_kmcqc_total_power_successor. bpvi_h_bls_kmcqc_total_power_successor + S (bpvi_successor_bls_kmcqc_total_power) = S ((S (S bpvi_j_bls_kmcqc_total_power)) * bpvi_v_bls_kmcqc_total_power)) /\ exists bpvi_q_bls_kmcqc_total_power_successor. bpvi_u_bls_kmcqc_total_power = bpvi_q_bls_kmcqc_total_power_successor * S ((S (S bpvi_j_bls_kmcqc_total_power)) * bpvi_v_bls_kmcqc_total_power) + (bpvi_successor_bls_kmcqc_total_power))) /\ bpvi_successor_bls_kmcqc_total_power = bpvi_partial_bls_kmcqc_total_power * bpvi_factor_bls_kmcqc_total_power)))))))) /\ ((((exists ff_h_bls_kmcqc_total_quotient_entry. ff_h_bls_kmcqc_total_quotient_entry + S (bls_quotient_kmcqc_total) = S ((S (bls_index_kmcqc_total)) * tc)) /\ exists ff_q_bls_kmcqc_total_quotient_entry. tb = ff_q_bls_kmcqc_total_quotient_entry * S ((S (bls_index_kmcqc_total)) * tc) + (bls_quotient_kmcqc_total))) /\ ((a + b = bls_power_kmcqc_total * bls_quotient_kmcqc_total + bls_remainder_kmcqc_total /\ exists bls_remainder_gap_kmcqc_total_division. bls_remainder_gap_kmcqc_total_division + S (bls_remainder_kmcqc_total) = bls_power_kmcqc_total))))) -> (exists bcf_lt_gap_kmcqc_bound. bcf_lt_gap_kmcqc_bound + S (i) = l) -> (exists q s Q bit. (((exists fs_h_kmcqc_result_left. fs_h_kmcqc_result_left + S (q) = S ((S (i)) * lc)) /\ exists fs_q_kmcqc_result_left. lb = fs_q_kmcqc_result_left * S ((S (i)) * lc) + (q))) /\ ((((exists fs_h_kmcqc_result_right. fs_h_kmcqc_result_right + S (s) = S ((S (i)) * rc)) /\ exists fs_q_kmcqc_result_right. rb = fs_q_kmcqc_result_right * S ((S (i)) * rc) + (s))) /\ ((((exists fs_h_kmcqc_result_total. fs_h_kmcqc_result_total + S (Q) = S ((S (i)) * tc)) /\ exists fs_q_kmcqc_result_total. tb = fs_q_kmcqc_result_total * S ((S (i)) * tc) + (Q))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s)))))))

Constructive proof overview

Generated structural guide

Three arbitrary power-quotient prefixes admit a constructive pointwise carry bit.

The unchanged tactic script uses 2 declared prerequisites and contains 105 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

pow_functional Stable theorem; checked-use authorized KU0000 division_add_quotient_bit

Direct dependents

KU0008 add_quotient_carry_prefix_exists

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

105 script commands · 33 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 (1)
division add quotient bit

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro 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
  10. L10
    intro l
02Fix variables and assumptionsL11–15

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

  1. L11
    intro i
  2. L12
    intro hleft
  3. L13
    intro hright
  4. L14
    intro htotal
  5. L15
    intro hi
03Establish hleft_dataL16–19

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

  1. L16
    have hleft_data : ∃ P. ∃ q. ∃ r. Pow(p,S i,P) ∧ (BetaAt(lb,lc,i,q) ∧ DivRem(a,P,q,r))Definitions: DivRemBetaAtPow
  2. L17
    specialize hleft i
  3. L18
    apply hleft
  4. L19
    exact hi
04Separate the logical casesL20–24

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

  1. L20
    cases hleft_data
  2. L21
    cases hleft_data_witness
  3. L22
    cases hleft_data_witness_witness
  4. L23
    cases hleft_data_witness_witness_witness
  5. L24
    cases hleft_data_witness_witness_witness_right
05Establish hright_dataL25–28

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

  1. L25
    have hright_data : ∃ P. ∃ q. ∃ r. Pow(p,S i,P) ∧ (BetaAt(rb,rc,i,q) ∧ DivRem(b,P,q,r))Definitions: DivRemBetaAtPow
  2. L26
    specialize hright i
  3. L27
    apply hright
  4. L28
    exact hi
06Separate the logical casesL29–33

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

  1. L29
    cases hright_data
  2. L30
    cases hright_data_witness
  3. L31
    cases hright_data_witness_witness
  4. L32
    cases hright_data_witness_witness_witness
  5. L33
    cases hright_data_witness_witness_witness_right
07Establish htotal_dataL34–37

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

  1. L34
    have htotal_data : ∃ P. ∃ q. ∃ r. Pow(p,S i,P) ∧ (BetaAt(tb,tc,i,q) ∧ DivRem(a + b,P,q,r))Definitions: DivRemBetaAtPow
  2. L35
    specialize htotal i
  3. L36
    apply htotal
  4. L37
    exact hi
08Separate the logical casesL38–42

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

  1. L38
    cases htotal_data
  2. L39
    cases htotal_data_witness
  3. L40
    cases htotal_data_witness_witness
  4. L41
    cases htotal_data_witness_witness_witness
  5. L42
    cases htotal_data_witness_witness_witness_right
09Establish hright_powerL43–52

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

  1. L43
    have hright_power : x = x3
  2. L44
    specialize pow_functional p
  3. L45
    specialize pow_functional (S i)
  4. L46
    specialize pow_functional x
  5. L47
    specialize pow_functional x3
  6. L48
    apply pow_functional
  7. L49
    exact hleft_data_witness_witness_witness_left
  8. L50
    exact hright_data_witness_witness_witness_left
  9. L51
    rewrite <- hright_power at hright_data_witness_witness_witness_right_right
  10. L52
    rewrite <- hright_power at hright_data_witness_witness_witness_right_right
10Establish htotal_powerL53–62

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

  1. L53
    have htotal_power : x = x6
  2. L54
    specialize pow_functional p
  3. L55
    specialize pow_functional (S i)
  4. L56
    specialize pow_functional x
  5. L57
    specialize pow_functional x6
  6. L58
    apply pow_functional
  7. L59
    exact hleft_data_witness_witness_witness_left
  8. L60
    exact htotal_data_witness_witness_witness_left
  9. L61
    rewrite <- htotal_power at htotal_data_witness_witness_witness_right_right
  10. L62
    rewrite <- htotal_power at htotal_data_witness_witness_witness_right_right
11Establish hcarryL63–72

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

  1. L63
    have hcarry : x7 = x1 + x4 \/ x7 = S (x1 + x4)
  2. L64
    specialize division_add_quotient_bit x
  3. L65
    specialize division_add_quotient_bit a
  4. L66
    specialize division_add_quotient_bit b
  5. L67
    specialize division_add_quotient_bit x1
  6. L68
    specialize division_add_quotient_bit x2
  7. L69
    specialize division_add_quotient_bit x4
  8. L70
    specialize division_add_quotient_bit x5
  9. L71
    specialize division_add_quotient_bit x7
  10. L72
    specialize division_add_quotient_bit x8
12Use earlier factsL73–76

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

  1. L73
    apply division_add_quotient_bit
  2. L74
    exact hleft_data_witness_witness_witness_right_right
  3. L75
    exact hright_data_witness_witness_witness_right_right
  4. L76
    exact htotal_data_witness_witness_witness_right_right
13Separate the logical casesL77–77

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

  1. L77
    cases hcarry
14Construct an explicit witnessL78–81

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

  1. L78
    exists x1
  2. L79
    exists x4
  3. L80
    exists x7
  4. L81
    exists 0
15Separate the logical casesL82–82

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

  1. L82
    split
16Use earlier factsL83–83

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

  1. L83
    exact hleft_data_witness_witness_witness_right_left
17Separate the logical casesL84–84

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

  1. L84
    split
18Use earlier factsL85–85

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

  1. L85
    exact hright_data_witness_witness_witness_right_left
19Separate the logical casesL86–86

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

  1. L86
    split
20Use earlier factsL87–87

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

  1. L87
    exact htotal_data_witness_witness_witness_right_left
21Separate the logical casesL88–89

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

  1. L88
    left
  2. L89
    split
22Calculate and transport equalitiesL90–90

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L90
    refl
23Use earlier factsL91–91

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

  1. L91
    exact hcarry_left
24Construct an explicit witnessL92–95

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

  1. L92
    exists x1
  2. L93
    exists x4
  3. L94
    exists x7
  4. L95
    exists 1
25Separate the logical casesL96–96

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

  1. L96
    split
26Use earlier factsL97–97

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

  1. L97
    exact hleft_data_witness_witness_witness_right_left
27Separate the logical casesL98–98

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

  1. L98
    split
28Use earlier factsL99–99

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

  1. L99
    exact hright_data_witness_witness_witness_right_left
29Separate the logical casesL100–100

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

  1. L100
    split
30Use earlier factsL101–101

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

  1. L101
    exact htotal_data_witness_witness_witness_right_left
31Separate the logical casesL102–103

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

  1. L102
    right
  2. L103
    split
32Calculate and transport equalitiesL104–104

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L104
    refl
33Use earlier factsL105–105

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

  1. L105
    exact hcarry_right

Library-wide reading audit

Original exact command ledger · 105 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. 0010intro l
  11. 0011intro i
  12. 0012intro hleft
  13. 0013intro hright
  14. 0014intro htotal
  15. 0015intro hi
  16. 0016have hleft_data : exists P q r. (exists bpvi_b_kmcqc_left_data_power bpvi_c_kmcqc_left_data_power. ((forall bpvi_i_kmcqc_left_data_power. (exists bpvi_repeat_gap_kmcqc_left_data_power. bpvi_repeat_gap_kmcqc_left_data_power + S bpvi_i_kmcqc_left_data_power = S i) -> (((exists bpvi_h_kmcqc_left_data_power_repeat. bpvi_h_kmcqc_left_data_power_repeat + S (p) = S ((S (bpvi_i_kmcqc_left_data_power)) * bpvi_c_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_repeat. bpvi_b_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_repeat * S ((S (bpvi_i_kmcqc_left_data_power)) * bpvi_c_kmcqc_left_data_power) + (p)))) /\ (exists bpvi_u_kmcqc_left_data_power bpvi_v_kmcqc_left_data_power. ((((exists bpvi_h_kmcqc_left_data_power_start. bpvi_h_kmcqc_left_data_power_start + S (1) = S ((S (0)) * bpvi_v_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_start. bpvi_u_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_start * S ((S (0)) * bpvi_v_kmcqc_left_data_power) + (1))) /\ ((((exists bpvi_h_kmcqc_left_data_power_terminal. bpvi_h_kmcqc_left_data_power_terminal + S (P) = S ((S (S i)) * bpvi_v_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_terminal. bpvi_u_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_terminal * S ((S (S i)) * bpvi_v_kmcqc_left_data_power) + (P))) /\ forall bpvi_j_kmcqc_left_data_power. (exists bpvi_product_gap_kmcqc_left_data_power. bpvi_product_gap_kmcqc_left_data_power + S bpvi_j_kmcqc_left_data_power = S i) -> exists bpvi_factor_kmcqc_left_data_power bpvi_partial_kmcqc_left_data_power bpvi_successor_kmcqc_left_data_power. ((((exists bpvi_h_kmcqc_left_data_power_factor. bpvi_h_kmcqc_left_data_power_factor + S (bpvi_factor_kmcqc_left_data_power) = S ((S (bpvi_j_kmcqc_left_data_power)) * bpvi_c_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_factor. bpvi_b_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_factor * S ((S (bpvi_j_kmcqc_left_data_power)) * bpvi_c_kmcqc_left_data_power) + (bpvi_factor_kmcqc_left_data_power))) /\ ((((exists bpvi_h_kmcqc_left_data_power_partial. bpvi_h_kmcqc_left_data_power_partial + S (bpvi_partial_kmcqc_left_data_power) = S ((S (bpvi_j_kmcqc_left_data_power)) * bpvi_v_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_partial. bpvi_u_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_partial * S ((S (bpvi_j_kmcqc_left_data_power)) * bpvi_v_kmcqc_left_data_power) + (bpvi_partial_kmcqc_left_data_power))) /\ ((((exists bpvi_h_kmcqc_left_data_power_successor. bpvi_h_kmcqc_left_data_power_successor + S (bpvi_successor_kmcqc_left_data_power) = S ((S (S bpvi_j_kmcqc_left_data_power)) * bpvi_v_kmcqc_left_data_power)) /\ exists bpvi_q_kmcqc_left_data_power_successor. bpvi_u_kmcqc_left_data_power = bpvi_q_kmcqc_left_data_power_successor * S ((S (S bpvi_j_kmcqc_left_data_power)) * bpvi_v_kmcqc_left_data_power) + (bpvi_successor_kmcqc_left_data_power))) /\ bpvi_successor_kmcqc_left_data_power = bpvi_partial_kmcqc_left_data_power * bpvi_factor_kmcqc_left_data_power)))))))) /\ ((((exists fs_h_kmcqc_left_data_entry. fs_h_kmcqc_left_data_entry + S (q) = S ((S (i)) * lc)) /\ exists fs_q_kmcqc_left_data_entry. lb = fs_q_kmcqc_left_data_entry * S ((S (i)) * lc) + (q))) /\ (((a) = (P) * (q) + (r) /\ (exists bcf_lt_gap_kmcqc_left_data_division_bound. bcf_lt_gap_kmcqc_left_data_division_bound + S (r) = P))))
  17. 0017specialize hleft i
  18. 0018apply hleft
  19. 0019exact hi
  20. 0020cases hleft_data
  21. 0021cases hleft_data_witness
  22. 0022cases hleft_data_witness_witness
  23. 0023cases hleft_data_witness_witness_witness
  24. 0024cases hleft_data_witness_witness_witness_right
  25. 0025have hright_data : exists P q r. (exists bpvi_b_kmcqc_right_data_power bpvi_c_kmcqc_right_data_power. ((forall bpvi_i_kmcqc_right_data_power. (exists bpvi_repeat_gap_kmcqc_right_data_power. bpvi_repeat_gap_kmcqc_right_data_power + S bpvi_i_kmcqc_right_data_power = S i) -> (((exists bpvi_h_kmcqc_right_data_power_repeat. bpvi_h_kmcqc_right_data_power_repeat + S (p) = S ((S (bpvi_i_kmcqc_right_data_power)) * bpvi_c_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_repeat. bpvi_b_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_repeat * S ((S (bpvi_i_kmcqc_right_data_power)) * bpvi_c_kmcqc_right_data_power) + (p)))) /\ (exists bpvi_u_kmcqc_right_data_power bpvi_v_kmcqc_right_data_power. ((((exists bpvi_h_kmcqc_right_data_power_start. bpvi_h_kmcqc_right_data_power_start + S (1) = S ((S (0)) * bpvi_v_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_start. bpvi_u_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_start * S ((S (0)) * bpvi_v_kmcqc_right_data_power) + (1))) /\ ((((exists bpvi_h_kmcqc_right_data_power_terminal. bpvi_h_kmcqc_right_data_power_terminal + S (P) = S ((S (S i)) * bpvi_v_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_terminal. bpvi_u_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_terminal * S ((S (S i)) * bpvi_v_kmcqc_right_data_power) + (P))) /\ forall bpvi_j_kmcqc_right_data_power. (exists bpvi_product_gap_kmcqc_right_data_power. bpvi_product_gap_kmcqc_right_data_power + S bpvi_j_kmcqc_right_data_power = S i) -> exists bpvi_factor_kmcqc_right_data_power bpvi_partial_kmcqc_right_data_power bpvi_successor_kmcqc_right_data_power. ((((exists bpvi_h_kmcqc_right_data_power_factor. bpvi_h_kmcqc_right_data_power_factor + S (bpvi_factor_kmcqc_right_data_power) = S ((S (bpvi_j_kmcqc_right_data_power)) * bpvi_c_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_factor. bpvi_b_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_factor * S ((S (bpvi_j_kmcqc_right_data_power)) * bpvi_c_kmcqc_right_data_power) + (bpvi_factor_kmcqc_right_data_power))) /\ ((((exists bpvi_h_kmcqc_right_data_power_partial. bpvi_h_kmcqc_right_data_power_partial + S (bpvi_partial_kmcqc_right_data_power) = S ((S (bpvi_j_kmcqc_right_data_power)) * bpvi_v_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_partial. bpvi_u_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_partial * S ((S (bpvi_j_kmcqc_right_data_power)) * bpvi_v_kmcqc_right_data_power) + (bpvi_partial_kmcqc_right_data_power))) /\ ((((exists bpvi_h_kmcqc_right_data_power_successor. bpvi_h_kmcqc_right_data_power_successor + S (bpvi_successor_kmcqc_right_data_power) = S ((S (S bpvi_j_kmcqc_right_data_power)) * bpvi_v_kmcqc_right_data_power)) /\ exists bpvi_q_kmcqc_right_data_power_successor. bpvi_u_kmcqc_right_data_power = bpvi_q_kmcqc_right_data_power_successor * S ((S (S bpvi_j_kmcqc_right_data_power)) * bpvi_v_kmcqc_right_data_power) + (bpvi_successor_kmcqc_right_data_power))) /\ bpvi_successor_kmcqc_right_data_power = bpvi_partial_kmcqc_right_data_power * bpvi_factor_kmcqc_right_data_power)))))))) /\ ((((exists fs_h_kmcqc_right_data_entry. fs_h_kmcqc_right_data_entry + S (q) = S ((S (i)) * rc)) /\ exists fs_q_kmcqc_right_data_entry. rb = fs_q_kmcqc_right_data_entry * S ((S (i)) * rc) + (q))) /\ (((b) = (P) * (q) + (r) /\ (exists bcf_lt_gap_kmcqc_right_data_division_bound. bcf_lt_gap_kmcqc_right_data_division_bound + S (r) = P))))
  26. 0026specialize hright i
  27. 0027apply hright
  28. 0028exact hi
  29. 0029cases hright_data
  30. 0030cases hright_data_witness
  31. 0031cases hright_data_witness_witness
  32. 0032cases hright_data_witness_witness_witness
  33. 0033cases hright_data_witness_witness_witness_right
  34. 0034have htotal_data : exists P q r. (exists bpvi_b_kmcqc_total_data_power bpvi_c_kmcqc_total_data_power. ((forall bpvi_i_kmcqc_total_data_power. (exists bpvi_repeat_gap_kmcqc_total_data_power. bpvi_repeat_gap_kmcqc_total_data_power + S bpvi_i_kmcqc_total_data_power = S i) -> (((exists bpvi_h_kmcqc_total_data_power_repeat. bpvi_h_kmcqc_total_data_power_repeat + S (p) = S ((S (bpvi_i_kmcqc_total_data_power)) * bpvi_c_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_repeat. bpvi_b_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_repeat * S ((S (bpvi_i_kmcqc_total_data_power)) * bpvi_c_kmcqc_total_data_power) + (p)))) /\ (exists bpvi_u_kmcqc_total_data_power bpvi_v_kmcqc_total_data_power. ((((exists bpvi_h_kmcqc_total_data_power_start. bpvi_h_kmcqc_total_data_power_start + S (1) = S ((S (0)) * bpvi_v_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_start. bpvi_u_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_start * S ((S (0)) * bpvi_v_kmcqc_total_data_power) + (1))) /\ ((((exists bpvi_h_kmcqc_total_data_power_terminal. bpvi_h_kmcqc_total_data_power_terminal + S (P) = S ((S (S i)) * bpvi_v_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_terminal. bpvi_u_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_terminal * S ((S (S i)) * bpvi_v_kmcqc_total_data_power) + (P))) /\ forall bpvi_j_kmcqc_total_data_power. (exists bpvi_product_gap_kmcqc_total_data_power. bpvi_product_gap_kmcqc_total_data_power + S bpvi_j_kmcqc_total_data_power = S i) -> exists bpvi_factor_kmcqc_total_data_power bpvi_partial_kmcqc_total_data_power bpvi_successor_kmcqc_total_data_power. ((((exists bpvi_h_kmcqc_total_data_power_factor. bpvi_h_kmcqc_total_data_power_factor + S (bpvi_factor_kmcqc_total_data_power) = S ((S (bpvi_j_kmcqc_total_data_power)) * bpvi_c_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_factor. bpvi_b_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_factor * S ((S (bpvi_j_kmcqc_total_data_power)) * bpvi_c_kmcqc_total_data_power) + (bpvi_factor_kmcqc_total_data_power))) /\ ((((exists bpvi_h_kmcqc_total_data_power_partial. bpvi_h_kmcqc_total_data_power_partial + S (bpvi_partial_kmcqc_total_data_power) = S ((S (bpvi_j_kmcqc_total_data_power)) * bpvi_v_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_partial. bpvi_u_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_partial * S ((S (bpvi_j_kmcqc_total_data_power)) * bpvi_v_kmcqc_total_data_power) + (bpvi_partial_kmcqc_total_data_power))) /\ ((((exists bpvi_h_kmcqc_total_data_power_successor. bpvi_h_kmcqc_total_data_power_successor + S (bpvi_successor_kmcqc_total_data_power) = S ((S (S bpvi_j_kmcqc_total_data_power)) * bpvi_v_kmcqc_total_data_power)) /\ exists bpvi_q_kmcqc_total_data_power_successor. bpvi_u_kmcqc_total_data_power = bpvi_q_kmcqc_total_data_power_successor * S ((S (S bpvi_j_kmcqc_total_data_power)) * bpvi_v_kmcqc_total_data_power) + (bpvi_successor_kmcqc_total_data_power))) /\ bpvi_successor_kmcqc_total_data_power = bpvi_partial_kmcqc_total_data_power * bpvi_factor_kmcqc_total_data_power)))))))) /\ ((((exists fs_h_kmcqc_total_data_entry. fs_h_kmcqc_total_data_entry + S (q) = S ((S (i)) * tc)) /\ exists fs_q_kmcqc_total_data_entry. tb = fs_q_kmcqc_total_data_entry * S ((S (i)) * tc) + (q))) /\ (((a + b) = (P) * (q) + (r) /\ (exists bcf_lt_gap_kmcqc_total_data_division_bound. bcf_lt_gap_kmcqc_total_data_division_bound + S (r) = P))))
  35. 0035specialize htotal i
  36. 0036apply htotal
  37. 0037exact hi
  38. 0038cases htotal_data
  39. 0039cases htotal_data_witness
  40. 0040cases htotal_data_witness_witness
  41. 0041cases htotal_data_witness_witness_witness
  42. 0042cases htotal_data_witness_witness_witness_right
  43. 0043have hright_power : x = x3
  44. 0044specialize pow_functional p
  45. 0045specialize pow_functional (S i)
  46. 0046specialize pow_functional x
  47. 0047specialize pow_functional x3
  48. 0048apply pow_functional
  49. 0049exact hleft_data_witness_witness_witness_left
  50. 0050exact hright_data_witness_witness_witness_left
  51. 0051rewrite <- hright_power at hright_data_witness_witness_witness_right_right
  52. 0052rewrite <- hright_power at hright_data_witness_witness_witness_right_right
  53. 0053have htotal_power : x = x6
  54. 0054specialize pow_functional p
  55. 0055specialize pow_functional (S i)
  56. 0056specialize pow_functional x
  57. 0057specialize pow_functional x6
  58. 0058apply pow_functional
  59. 0059exact hleft_data_witness_witness_witness_left
  60. 0060exact htotal_data_witness_witness_witness_left
  61. 0061rewrite <- htotal_power at htotal_data_witness_witness_witness_right_right
  62. 0062rewrite <- htotal_power at htotal_data_witness_witness_witness_right_right
  63. 0063have hcarry : x7 = x1 + x4 \/ x7 = S (x1 + x4)
  64. 0064specialize division_add_quotient_bit x
  65. 0065specialize division_add_quotient_bit a
  66. 0066specialize division_add_quotient_bit b
  67. 0067specialize division_add_quotient_bit x1
  68. 0068specialize division_add_quotient_bit x2
  69. 0069specialize division_add_quotient_bit x4
  70. 0070specialize division_add_quotient_bit x5
  71. 0071specialize division_add_quotient_bit x7
  72. 0072specialize division_add_quotient_bit x8
  73. 0073apply division_add_quotient_bit
  74. 0074exact hleft_data_witness_witness_witness_right_right
  75. 0075exact hright_data_witness_witness_witness_right_right
  76. 0076exact htotal_data_witness_witness_witness_right_right
  77. 0077cases hcarry
  78. 0078exists x1
  79. 0079exists x4
  80. 0080exists x7
  81. 0081exists 0
  82. 0082split
  83. 0083exact hleft_data_witness_witness_witness_right_left
  84. 0084split
  85. 0085exact hright_data_witness_witness_witness_right_left
  86. 0086split
  87. 0087exact htotal_data_witness_witness_witness_right_left
  88. 0088left
  89. 0089split
  90. 0090refl
  91. 0091exact hcarry_left
  92. 0092exists x1
  93. 0093exists x4
  94. 0094exists x7
  95. 0095exists 1
  96. 0096split
  97. 0097exact hleft_data_witness_witness_witness_right_left
  98. 0098split
  99. 0099exact hright_data_witness_witness_witness_right_left
  100. 0100split
  101. 0101exact htotal_data_witness_witness_witness_right_left
  102. 0102right
  103. 0103split
  104. 0104refl
  105. 0105exact hcarry_right