BT00Y3 · Bertrand theorem

beta_sum_double_carry_exact

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

The doubled quotient sum is twice the source sum plus its carries.

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.

Statement with defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ l. ∀ B. ∀ A. ∀ E. Sum(b,c,l,B) → Sum(d,e,l,A) → (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(d,e,x,z) ∧ (BetaAt(f,g,x,n) ∧ (n = 0 ∧ z = y + y ∨ n = 1 ∧ z = S (y + y))))) → BitCount(f,g,l,E) → A = B + B + E

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount

7 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount

13 occurrences

Exact expanded native-PA statement
forall b c d e f g l B A E. (exists ff_u_b5ccsdce_left_sum ff_v_b5ccsdce_left_sum. ((((exists ff_h_b5ccsdce_left_sum_start. ff_h_b5ccsdce_left_sum_start + S (0) = S ((S (0)) * ff_v_b5ccsdce_left_sum)) /\ exists ff_q_b5ccsdce_left_sum_start. ff_u_b5ccsdce_left_sum = ff_q_b5ccsdce_left_sum_start * S ((S (0)) * ff_v_b5ccsdce_left_sum) + (0))) /\ ((((exists ff_h_b5ccsdce_left_sum_terminal. ff_h_b5ccsdce_left_sum_terminal + S (B) = S ((S (l)) * ff_v_b5ccsdce_left_sum)) /\ exists ff_q_b5ccsdce_left_sum_terminal. ff_u_b5ccsdce_left_sum = ff_q_b5ccsdce_left_sum_terminal * S ((S (l)) * ff_v_b5ccsdce_left_sum) + (B))) /\ forall ff_i_b5ccsdce_left_sum. (exists ff_lt_b5ccsdce_left_sum_bound. ff_lt_b5ccsdce_left_sum_bound + S ff_i_b5ccsdce_left_sum = l) -> exists ff_a_b5ccsdce_left_sum ff_r_b5ccsdce_left_sum ff_s_b5ccsdce_left_sum. ((((exists ff_h_b5ccsdce_left_sum_summand. ff_h_b5ccsdce_left_sum_summand + S (ff_a_b5ccsdce_left_sum) = S ((S (ff_i_b5ccsdce_left_sum)) * c)) /\ exists ff_q_b5ccsdce_left_sum_summand. b = ff_q_b5ccsdce_left_sum_summand * S ((S (ff_i_b5ccsdce_left_sum)) * c) + (ff_a_b5ccsdce_left_sum))) /\ ((((exists ff_h_b5ccsdce_left_sum_partial. ff_h_b5ccsdce_left_sum_partial + S (ff_r_b5ccsdce_left_sum) = S ((S (ff_i_b5ccsdce_left_sum)) * ff_v_b5ccsdce_left_sum)) /\ exists ff_q_b5ccsdce_left_sum_partial. ff_u_b5ccsdce_left_sum = ff_q_b5ccsdce_left_sum_partial * S ((S (ff_i_b5ccsdce_left_sum)) * ff_v_b5ccsdce_left_sum) + (ff_r_b5ccsdce_left_sum))) /\ ((((exists ff_h_b5ccsdce_left_sum_successor. ff_h_b5ccsdce_left_sum_successor + S (ff_s_b5ccsdce_left_sum) = S ((S (S ff_i_b5ccsdce_left_sum)) * ff_v_b5ccsdce_left_sum)) /\ exists ff_q_b5ccsdce_left_sum_successor. ff_u_b5ccsdce_left_sum = ff_q_b5ccsdce_left_sum_successor * S ((S (S ff_i_b5ccsdce_left_sum)) * ff_v_b5ccsdce_left_sum) + (ff_s_b5ccsdce_left_sum))) /\ ff_s_b5ccsdce_left_sum = ff_r_b5ccsdce_left_sum + ff_a_b5ccsdce_left_sum)))))) -> (exists ff_u_b5ccsdce_right_sum ff_v_b5ccsdce_right_sum. ((((exists ff_h_b5ccsdce_right_sum_start. ff_h_b5ccsdce_right_sum_start + S (0) = S ((S (0)) * ff_v_b5ccsdce_right_sum)) /\ exists ff_q_b5ccsdce_right_sum_start. ff_u_b5ccsdce_right_sum = ff_q_b5ccsdce_right_sum_start * S ((S (0)) * ff_v_b5ccsdce_right_sum) + (0))) /\ ((((exists ff_h_b5ccsdce_right_sum_terminal. ff_h_b5ccsdce_right_sum_terminal + S (A) = S ((S (l)) * ff_v_b5ccsdce_right_sum)) /\ exists ff_q_b5ccsdce_right_sum_terminal. ff_u_b5ccsdce_right_sum = ff_q_b5ccsdce_right_sum_terminal * S ((S (l)) * ff_v_b5ccsdce_right_sum) + (A))) /\ forall ff_i_b5ccsdce_right_sum. (exists ff_lt_b5ccsdce_right_sum_bound. ff_lt_b5ccsdce_right_sum_bound + S ff_i_b5ccsdce_right_sum = l) -> exists ff_a_b5ccsdce_right_sum ff_r_b5ccsdce_right_sum ff_s_b5ccsdce_right_sum. ((((exists ff_h_b5ccsdce_right_sum_summand. ff_h_b5ccsdce_right_sum_summand + S (ff_a_b5ccsdce_right_sum) = S ((S (ff_i_b5ccsdce_right_sum)) * e)) /\ exists ff_q_b5ccsdce_right_sum_summand. d = ff_q_b5ccsdce_right_sum_summand * S ((S (ff_i_b5ccsdce_right_sum)) * e) + (ff_a_b5ccsdce_right_sum))) /\ ((((exists ff_h_b5ccsdce_right_sum_partial. ff_h_b5ccsdce_right_sum_partial + S (ff_r_b5ccsdce_right_sum) = S ((S (ff_i_b5ccsdce_right_sum)) * ff_v_b5ccsdce_right_sum)) /\ exists ff_q_b5ccsdce_right_sum_partial. ff_u_b5ccsdce_right_sum = ff_q_b5ccsdce_right_sum_partial * S ((S (ff_i_b5ccsdce_right_sum)) * ff_v_b5ccsdce_right_sum) + (ff_r_b5ccsdce_right_sum))) /\ ((((exists ff_h_b5ccsdce_right_sum_successor. ff_h_b5ccsdce_right_sum_successor + S (ff_s_b5ccsdce_right_sum) = S ((S (S ff_i_b5ccsdce_right_sum)) * ff_v_b5ccsdce_right_sum)) /\ exists ff_q_b5ccsdce_right_sum_successor. ff_u_b5ccsdce_right_sum = ff_q_b5ccsdce_right_sum_successor * S ((S (S ff_i_b5ccsdce_right_sum)) * ff_v_b5ccsdce_right_sum) + (ff_s_b5ccsdce_right_sum))) /\ ff_s_b5ccsdce_right_sum = ff_r_b5ccsdce_right_sum + ff_a_b5ccsdce_right_sum)))))) -> (forall b5cc_index_b5ccsdce_prefix. (exists bcf_lt_gap_b5ccsdce_prefix_bound. bcf_lt_gap_b5ccsdce_prefix_bound + S (b5cc_index_b5ccsdce_prefix) = l) -> exists b5cc_left_b5ccsdce_prefix b5cc_right_b5ccsdce_prefix b5cc_bit_b5ccsdce_prefix. (((exists fs_h_b5cc_b5ccsdce_prefix_left. fs_h_b5cc_b5ccsdce_prefix_left + S (b5cc_left_b5ccsdce_prefix) = S ((S (b5cc_index_b5ccsdce_prefix)) * c)) /\ exists fs_q_b5cc_b5ccsdce_prefix_left. b = fs_q_b5cc_b5ccsdce_prefix_left * S ((S (b5cc_index_b5ccsdce_prefix)) * c) + (b5cc_left_b5ccsdce_prefix))) /\ ((((exists fs_h_b5cc_b5ccsdce_prefix_right. fs_h_b5cc_b5ccsdce_prefix_right + S (b5cc_right_b5ccsdce_prefix) = S ((S (b5cc_index_b5ccsdce_prefix)) * e)) /\ exists fs_q_b5cc_b5ccsdce_prefix_right. d = fs_q_b5cc_b5ccsdce_prefix_right * S ((S (b5cc_index_b5ccsdce_prefix)) * e) + (b5cc_right_b5ccsdce_prefix))) /\ ((((exists fs_h_b5cc_b5ccsdce_prefix_bit. fs_h_b5cc_b5ccsdce_prefix_bit + S (b5cc_bit_b5ccsdce_prefix) = S ((S (b5cc_index_b5ccsdce_prefix)) * g)) /\ exists fs_q_b5cc_b5ccsdce_prefix_bit. f = fs_q_b5cc_b5ccsdce_prefix_bit * S ((S (b5cc_index_b5ccsdce_prefix)) * g) + (b5cc_bit_b5ccsdce_prefix))) /\ (((b5cc_bit_b5ccsdce_prefix = 0 /\ b5cc_right_b5ccsdce_prefix = b5cc_left_b5ccsdce_prefix + b5cc_left_b5ccsdce_prefix) \/ (b5cc_bit_b5ccsdce_prefix = 1 /\ b5cc_right_b5ccsdce_prefix = S (b5cc_left_b5ccsdce_prefix + b5cc_left_b5ccsdce_prefix))))))) -> (((exists ff_u_b5ccsdce_count_sum ff_v_b5ccsdce_count_sum. ((((exists ff_h_b5ccsdce_count_sum_start. ff_h_b5ccsdce_count_sum_start + S (0) = S ((S (0)) * ff_v_b5ccsdce_count_sum)) /\ exists ff_q_b5ccsdce_count_sum_start. ff_u_b5ccsdce_count_sum = ff_q_b5ccsdce_count_sum_start * S ((S (0)) * ff_v_b5ccsdce_count_sum) + (0))) /\ ((((exists ff_h_b5ccsdce_count_sum_terminal. ff_h_b5ccsdce_count_sum_terminal + S (E) = S ((S (l)) * ff_v_b5ccsdce_count_sum)) /\ exists ff_q_b5ccsdce_count_sum_terminal. ff_u_b5ccsdce_count_sum = ff_q_b5ccsdce_count_sum_terminal * S ((S (l)) * ff_v_b5ccsdce_count_sum) + (E))) /\ forall ff_i_b5ccsdce_count_sum. (exists ff_lt_b5ccsdce_count_sum_bound. ff_lt_b5ccsdce_count_sum_bound + S ff_i_b5ccsdce_count_sum = l) -> exists ff_a_b5ccsdce_count_sum ff_r_b5ccsdce_count_sum ff_s_b5ccsdce_count_sum. ((((exists ff_h_b5ccsdce_count_sum_summand. ff_h_b5ccsdce_count_sum_summand + S (ff_a_b5ccsdce_count_sum) = S ((S (ff_i_b5ccsdce_count_sum)) * g)) /\ exists ff_q_b5ccsdce_count_sum_summand. f = ff_q_b5ccsdce_count_sum_summand * S ((S (ff_i_b5ccsdce_count_sum)) * g) + (ff_a_b5ccsdce_count_sum))) /\ ((((exists ff_h_b5ccsdce_count_sum_partial. ff_h_b5ccsdce_count_sum_partial + S (ff_r_b5ccsdce_count_sum) = S ((S (ff_i_b5ccsdce_count_sum)) * ff_v_b5ccsdce_count_sum)) /\ exists ff_q_b5ccsdce_count_sum_partial. ff_u_b5ccsdce_count_sum = ff_q_b5ccsdce_count_sum_partial * S ((S (ff_i_b5ccsdce_count_sum)) * ff_v_b5ccsdce_count_sum) + (ff_r_b5ccsdce_count_sum))) /\ ((((exists ff_h_b5ccsdce_count_sum_successor. ff_h_b5ccsdce_count_sum_successor + S (ff_s_b5ccsdce_count_sum) = S ((S (S ff_i_b5ccsdce_count_sum)) * ff_v_b5ccsdce_count_sum)) /\ exists ff_q_b5ccsdce_count_sum_successor. ff_u_b5ccsdce_count_sum = ff_q_b5ccsdce_count_sum_successor * S ((S (S ff_i_b5ccsdce_count_sum)) * ff_v_b5ccsdce_count_sum) + (ff_s_b5ccsdce_count_sum))) /\ ff_s_b5ccsdce_count_sum = ff_r_b5ccsdce_count_sum + ff_a_b5ccsdce_count_sum)))))) /\ (forall ff_i_b5ccsdce_count_bits. (exists ff_lt_b5ccsdce_count_bits_bound. ff_lt_b5ccsdce_count_bits_bound + S ff_i_b5ccsdce_count_bits = l) -> exists ff_bit_b5ccsdce_count_bits. ((((exists ff_h_b5ccsdce_count_bits_decoded. ff_h_b5ccsdce_count_bits_decoded + S (ff_bit_b5ccsdce_count_bits) = S ((S (ff_i_b5ccsdce_count_bits)) * g)) /\ exists ff_q_b5ccsdce_count_bits_decoded. f = ff_q_b5ccsdce_count_bits_decoded * S ((S (ff_i_b5ccsdce_count_bits)) * g) + (ff_bit_b5ccsdce_count_bits))) /\ (ff_bit_b5ccsdce_count_bits = 0 \/ ff_bit_b5ccsdce_count_bits = 1))))) -> A = (B + B) + E

Proof neighborhood

Direct theorem prerequisites

BT008E beta_sum_zero BT008F beta_sum_succ_decompose BT008N bit_count_zero BT008O bit_count_succ_decompose BT0042 beta_at_unique BT000E le_refl BT00Y0 double_quotient_carry_prefix_restrict BT0003 add_assoc BT0032 add_permute_outer BT0002 add_comm

Direct theorem dependents

BT00Y4 central_binom_carry_bit_count

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

174 script commands · 29 reading checkpoints · 16 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (9)
beta sum zerobeta sum succ decomposebit count zerobit count succ decomposebeta at uniquele refldouble quotient carry prefix restrictadd assocadd permute outer
01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro f
  6. L6
    intro g
02Induction on lL7–14

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

  1. L7
    induction l
  2. L8
    intro B
  3. L9
    intro A
  4. L10
    intro E
  5. L11
    intro hleft
  6. L12
    intro hright
  7. L13
    intro hcarry
  8. L14
    intro hcount
03Establish hBL15–20

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

  1. L15
    have hB : B = 0
  2. L16
    specialize beta_sum_zero b
  3. L17
    specialize beta_sum_zero c
  4. L18
    specialize beta_sum_zero B
  5. L19
    apply beta_sum_zero
  6. L20
    exact hleft
04Establish hAL21–26

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

  1. L21
    have hA : A = 0
  2. L22
    specialize beta_sum_zero d
  3. L23
    specialize beta_sum_zero e
  4. L24
    specialize beta_sum_zero A
  5. L25
    apply beta_sum_zero
  6. L26
    exact hright
05Establish hEL27–36

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

  1. L27
    have hE : E = 0
  2. L28
    specialize bit_count_zero f
  3. L29
    specialize bit_count_zero g
  4. L30
    specialize bit_count_zero 0
  5. L31
    specialize bit_count_zero E
  6. L32
    apply bit_count_zero
  7. L33
    refl
  8. L34
    exact hcount
  9. L35
    rewrite hA
  10. L36
    rewrite hB
06Calculate and transport equalitiesL37–39

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

  1. L37
    rewrite hB
  2. L38
    rewrite hE
  3. L39
    simp
07Fix variables and assumptionsL40–46

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

  1. L40
    intro B
  2. L41
    intro A
  3. L42
    intro E
  4. L43
    intro hleft
  5. L44
    intro hright
  6. L45
    intro hcarry
  7. L46
    intro hcount
08Establish hleft_decompL47–53

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

  1. L47
    have hleft_decomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ B = r + a)Definitions: BetaAt(b,c,l,a)Sum(b,c,l,r)Original native command in the exact edition
  2. L48
    specialize beta_sum_succ_decompose b
  3. L49
    specialize beta_sum_succ_decompose c
  4. L50
    specialize beta_sum_succ_decompose l
  5. L51
    specialize beta_sum_succ_decompose B
  6. L52
    apply beta_sum_succ_decompose
  7. L53
    exact hleft
09Separate the logical casesL54–57

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

  1. L54
    cases hleft_decomp
  2. L55
    cases hleft_decomp_witness
  3. L56
    cases hleft_decomp_witness_witness
  4. L57
    cases hleft_decomp_witness_witness_right
10Establish hright_decompL58–64

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

  1. L58
    have hright_decomp : ∃ a. ∃ r. BetaAt(d,e,l,a) ∧ (Sum(d,e,l,r) ∧ A = r + a)Definitions: BetaAt(d,e,l,a)Sum(d,e,l,r)Original native command in the exact edition
  2. L59
    specialize beta_sum_succ_decompose d
  3. L60
    specialize beta_sum_succ_decompose e
  4. L61
    specialize beta_sum_succ_decompose l
  5. L62
    specialize beta_sum_succ_decompose A
  6. L63
    apply beta_sum_succ_decompose
  7. L64
    exact hright
11Separate the logical casesL65–68

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

  1. L65
    cases hright_decomp
  2. L66
    cases hright_decomp_witness
  3. L67
    cases hright_decomp_witness_witness
  4. L68
    cases hright_decomp_witness_witness_right
12Establish hcount_decompL69–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count succ decompose.

  1. L69
    have hcount_decomp : ∃ bit. ∃ r. BetaAt(f,g,l,bit) ∧ (BitCount(f,g,l,r) ∧ ((bit = 0 ∨ bit = 1) ∧ E = r + bit))Definitions: BetaAt(f,g,l,bit)BitCount(f,g,l,r)Original native command in the exact edition
  2. L70
    specialize bit_count_succ_decompose f
  3. L71
    specialize bit_count_succ_decompose g
  4. L72
    specialize bit_count_succ_decompose l
  5. L73
    specialize bit_count_succ_decompose (S l)
  6. L74
    specialize bit_count_succ_decompose E
  7. L75
    apply bit_count_succ_decompose
  8. L76
    refl
  9. L77
    exact hcount
13Separate the logical casesL78–82

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

  1. L78
    cases hcount_decomp
  2. L79
    cases hcount_decomp_witness
  3. L80
    cases hcount_decomp_witness_witness
  4. L81
    cases hcount_decomp_witness_witness_right
  5. L82
    cases hcount_decomp_witness_witness_right_right
14Establish hterminalL83–87

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

  1. L83
    have hterminal : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,l,q) ∧ (BetaAt(d,e,l,Q) ∧ (BetaAt(f,g,l,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))Definitions: BetaAt(b,c,l,q)BetaAt(d,e,l,Q)BetaAt(f,g,l,bit)Original native command in the exact edition
  2. L84
    specialize hcarry l
  3. L85
    apply hcarry
  4. L86
    specialize le_refl (S l)
  5. L87
    exact le_refl
15Separate the logical casesL88–93

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

  1. L88
    cases hterminal
  2. L89
    cases hterminal_witness
  3. L90
    cases hterminal_witness_witness
  4. L91
    cases hterminal_witness_witness_witness
  5. L92
    cases hterminal_witness_witness_witness_right
  6. L93
    cases hterminal_witness_witness_witness_right_right
16Establish hqL94–102

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

  1. L94
    have hq : x = x6
  2. L95
    specialize beta_at_unique b
  3. L96
    specialize beta_at_unique c
  4. L97
    specialize beta_at_unique l
  5. L98
    specialize beta_at_unique x
  6. L99
    specialize beta_at_unique x6
  7. L100
    apply beta_at_unique
  8. L101
    exact hleft_decomp_witness_witness_left
  9. L102
    exact hterminal_witness_witness_witness_left
17Establish hQL103–111

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

  1. L103
    have hQ : x2 = x7
  2. L104
    specialize beta_at_unique d
  3. L105
    specialize beta_at_unique e
  4. L106
    specialize beta_at_unique l
  5. L107
    specialize beta_at_unique x2
  6. L108
    specialize beta_at_unique x7
  7. L109
    apply beta_at_unique
  8. L110
    exact hright_decomp_witness_witness_left
  9. L111
    exact hterminal_witness_witness_witness_right_left
18Establish hbitL112–121

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

  1. L112
    have hbit : x4 = x8
  2. L113
    specialize beta_at_unique f
  3. L114
    specialize beta_at_unique g
  4. L115
    specialize beta_at_unique l
  5. L116
    specialize beta_at_unique x4
  6. L117
    specialize beta_at_unique x8
  7. L118
    apply beta_at_unique
  8. L119
    exact hcount_decomp_witness_witness_left
  9. L120
    exact hterminal_witness_witness_witness_right_right_left
  10. L121
    rewrite hq at hleft_decomp_witness_witness_right_right
19Calculate and transport equalitiesL122–123

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

  1. L122
    rewrite hQ at hright_decomp_witness_witness_right_right
  2. L123
    rewrite hbit at hcount_decomp_witness_witness_right_right_right
20Establish hprefixL124–133

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply double quotient carry prefix restrict.

  1. L124
    have hprefix : ∀ b5cc_index_b5ccsdce_restricted. Lt(b5cc_index_b5ccsdce_restricted,l) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,b5cc_index_b5ccsdce_restricted,x) ∧ (BetaAt(d,e,b5cc_index_b5ccsdce_restricted,y) ∧ (BetaAt(f,g,b5cc_index_b5ccsdce_restricted,z) ∧ (z = 0 ∧ y = x + x ∨ z = 1 ∧ y = S (x + x))))Definitions: Lt(b5cc_index_b5ccsdce_restricted,l)BetaAt(b,c,b5cc_index_b5ccsdce_restricted,x)BetaAt(d,e,b5cc_index_b5ccsdce_restricted,y)BetaAt(f,g,b5cc_index_b5ccsdce_restricted,z)Original native command in the exact edition
  2. L125
    specialize double_quotient_carry_prefix_restrict b
  3. L126
    specialize double_quotient_carry_prefix_restrict c
  4. L127
    specialize double_quotient_carry_prefix_restrict d
  5. L128
    specialize double_quotient_carry_prefix_restrict e
  6. L129
    specialize double_quotient_carry_prefix_restrict f
  7. L130
    specialize double_quotient_carry_prefix_restrict g
  8. L131
    specialize double_quotient_carry_prefix_restrict l
  9. L132
    apply double_quotient_carry_prefix_restrict
  10. L133
    exact hcarry
21Establish hbalanceL134–142

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

  1. L134
    have hbalance : x3 = (x1 + x1) + x5
  2. L135
    specialize IH x1
  3. L136
    specialize IH x3
  4. L137
    specialize IH x5
  5. L138
    apply IH
  6. L139
    exact hleft_decomp_witness_witness_right_left
  7. L140
    exact hright_decomp_witness_witness_right_left
  8. L141
    exact hprefix
  9. L142
    exact hcount_decomp_witness_witness_right_left
22Establish hinnerL143–143

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

  1. L143
    have hinner : x5 + (x6 + (x6 + x1)) = x6 + (x6 + (x5 + x1))
23Establish hleft_assocL144–146

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

  1. L144
    have hleft_assoc : x5 + (x6 + (x6 + x1)) = (x5 + x6) + (x6 + x1)
  2. L145
    symm
  3. L146
    apply add_assoc
24Establish hpermuteL147–148

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

  1. L147
    have hpermute : (x5 + x6) + (x6 + x1) = (x6 + x6) + (x5 + x1)
  2. L148
    apply add_permute_outer
25Establish hright_assocL149–155

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

  1. L149
    have hright_assoc : (x6 + x6) + (x5 + x1) = x6 + (x6 + (x5 + x1))
  2. L150
    apply add_assoc
  3. L151
    trans (x5 + x6) + (x6 + x1)
  4. L152
    exact hleft_assoc
  5. L153
    trans (x6 + x6) + (x5 + x1)
  6. L154
    exact hpermute
  7. L155
    exact hright_assoc
26Separate the logical casesL156–157

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

  1. L156
    cases hterminal_witness_witness_witness_right_right_right
  2. L157
    cases hterminal_witness_witness_witness_right_right_right_left
27Calculate and transport equalitiesL158–165

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

  1. L158
    rewrite hright_decomp_witness_witness_right_right
  2. L159
    rewrite hleft_decomp_witness_witness_right_right
  3. L160
    rewrite hleft_decomp_witness_witness_right_right
  4. L161
    rewrite hcount_decomp_witness_witness_right_right_right
  5. L162
    rewrite hbalance
  6. L163
    rewrite hterminal_witness_witness_witness_right_right_right_left_left
  7. L164
    rewrite hterminal_witness_witness_witness_right_right_right_left_right
  8. L165
    simp [add_assoc, add_comm]
28Separate the logical casesL166–166

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

  1. L166
    cases hterminal_witness_witness_witness_right_right_right_right
29Calculate and transport equalitiesL167–174

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

  1. L167
    rewrite hright_decomp_witness_witness_right_right
  2. L168
    rewrite hleft_decomp_witness_witness_right_right
  3. L169
    rewrite hleft_decomp_witness_witness_right_right
  4. L170
    rewrite hcount_decomp_witness_witness_right_right_right
  5. L171
    rewrite hbalance
  6. L172
    rewrite hterminal_witness_witness_witness_right_right_right_right_left
  7. L173
    rewrite hterminal_witness_witness_witness_right_right_right_right_right
  8. L174
    simp [add_assoc, add_comm]

Library-wide reading audit

Original defined command ledger · 174 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007induction l
  8. 0008intro B
  9. 0009intro A
  10. 0010intro E
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013intro hcarry
  14. 0014intro hcount
  15. 0015have hB : B = 0
  16. 0016specialize beta_sum_zero b
  17. 0017specialize beta_sum_zero c
  18. 0018specialize beta_sum_zero B
  19. 0019apply beta_sum_zero
  20. 0020exact hleft
  21. 0021have hA : A = 0
  22. 0022specialize beta_sum_zero d
  23. 0023specialize beta_sum_zero e
  24. 0024specialize beta_sum_zero A
  25. 0025apply beta_sum_zero
  26. 0026exact hright
  27. 0027have hE : E = 0
  28. 0028specialize bit_count_zero f
  29. 0029specialize bit_count_zero g
  30. 0030specialize bit_count_zero 0
  31. 0031specialize bit_count_zero E
  32. 0032apply bit_count_zero
  33. 0033refl
  34. 0034exact hcount
  35. 0035rewrite hA
  36. 0036rewrite hB
  37. 0037rewrite hB
  38. 0038rewrite hE
  39. 0039simp
  40. 0040intro B
  41. 0041intro A
  42. 0042intro E
  43. 0043intro hleft
  44. 0044intro hright
  45. 0045intro hcarry
  46. 0046intro hcount
  47. 0047have hleft_decomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ B = r + a)
    Exact native replay linehave hleft_decomp : exists a r. (((exists fs_h_b5ccsdce_left_decomp_entry. fs_h_b5ccsdce_left_decomp_entry + S (a) = S ((S (l)) * c)) /\ exists fs_q_b5ccsdce_left_decomp_entry. b = fs_q_b5ccsdce_left_decomp_entry * S ((S (l)) * c) + (a))) /\ ((exists fs_u_b5ccsdce_left_decomp_prefix fs_v_b5ccsdce_left_decomp_prefix. ((((exists fs_h_b5ccsdce_left_decomp_prefix_body_start. fs_h_b5ccsdce_left_decomp_prefix_body_start + S (0) = S ((S (0)) * fs_v_b5ccsdce_left_decomp_prefix)) /\ exists fs_q_b5ccsdce_left_decomp_prefix_body_start. fs_u_b5ccsdce_left_decomp_prefix = fs_q_b5ccsdce_left_decomp_prefix_body_start * S ((S (0)) * fs_v_b5ccsdce_left_decomp_prefix) + (0))) /\ ((((exists fs_h_b5ccsdce_left_decomp_prefix_body_terminal. fs_h_b5ccsdce_left_decomp_prefix_body_terminal + S (r) = S ((S (l)) * fs_v_b5ccsdce_left_decomp_prefix)) /\ exists fs_q_b5ccsdce_left_decomp_prefix_body_terminal. fs_u_b5ccsdce_left_decomp_prefix = fs_q_b5ccsdce_left_decomp_prefix_body_terminal * S ((S (l)) * fs_v_b5ccsdce_left_decomp_prefix) + (r))) /\ forall fs_i_b5ccsdce_left_decomp_prefix_body_steps. (exists fs_lt_b5ccsdce_left_decomp_prefix_body_steps_bound. fs_lt_b5ccsdce_left_decomp_prefix_body_steps_bound + S fs_i_b5ccsdce_left_decomp_prefix_body_steps = l) -> exists fs_a_b5ccsdce_left_decomp_prefix_body_steps fs_r_b5ccsdce_left_decomp_prefix_body_steps fs_s_b5ccsdce_left_decomp_prefix_body_steps. ((((exists fs_h_b5ccsdce_left_decomp_prefix_body_steps_summand. fs_h_b5ccsdce_left_decomp_prefix_body_steps_summand + S (fs_a_b5ccsdce_left_decomp_prefix_body_steps) = S ((S (fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * c)) /\ exists fs_q_b5ccsdce_left_decomp_prefix_body_steps_summand. b = fs_q_b5ccsdce_left_decomp_prefix_body_steps_summand * S ((S (fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * c) + (fs_a_b5ccsdce_left_decomp_prefix_body_steps))) /\ ((((exists fs_h_b5ccsdce_left_decomp_prefix_body_steps_partial. fs_h_b5ccsdce_left_decomp_prefix_body_steps_partial + S (fs_r_b5ccsdce_left_decomp_prefix_body_steps) = S ((S (fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * fs_v_b5ccsdce_left_decomp_prefix)) /\ exists fs_q_b5ccsdce_left_decomp_prefix_body_steps_partial. fs_u_b5ccsdce_left_decomp_prefix = fs_q_b5ccsdce_left_decomp_prefix_body_steps_partial * S ((S (fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * fs_v_b5ccsdce_left_decomp_prefix) + (fs_r_b5ccsdce_left_decomp_prefix_body_steps))) /\ ((((exists fs_h_b5ccsdce_left_decomp_prefix_body_steps_successor. fs_h_b5ccsdce_left_decomp_prefix_body_steps_successor + S (fs_s_b5ccsdce_left_decomp_prefix_body_steps) = S ((S (S fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * fs_v_b5ccsdce_left_decomp_prefix)) /\ exists fs_q_b5ccsdce_left_decomp_prefix_body_steps_successor. fs_u_b5ccsdce_left_decomp_prefix = fs_q_b5ccsdce_left_decomp_prefix_body_steps_successor * S ((S (S fs_i_b5ccsdce_left_decomp_prefix_body_steps)) * fs_v_b5ccsdce_left_decomp_prefix) + (fs_s_b5ccsdce_left_decomp_prefix_body_steps))) /\ fs_s_b5ccsdce_left_decomp_prefix_body_steps = fs_r_b5ccsdce_left_decomp_prefix_body_steps + fs_a_b5ccsdce_left_decomp_prefix_body_steps)))))) /\ B = r + a)
  48. 0048specialize beta_sum_succ_decompose b
  49. 0049specialize beta_sum_succ_decompose c
  50. 0050specialize beta_sum_succ_decompose l
  51. 0051specialize beta_sum_succ_decompose B
  52. 0052apply beta_sum_succ_decompose
  53. 0053exact hleft
  54. 0054cases hleft_decomp
  55. 0055cases hleft_decomp_witness
  56. 0056cases hleft_decomp_witness_witness
  57. 0057cases hleft_decomp_witness_witness_right
  58. 0058have hright_decomp : ∃ a. ∃ r. BetaAt(d,e,l,a) ∧ (Sum(d,e,l,r) ∧ A = r + a)
    Exact native replay linehave hright_decomp : exists a r. (((exists fs_h_b5ccsdce_right_decomp_entry. fs_h_b5ccsdce_right_decomp_entry + S (a) = S ((S (l)) * e)) /\ exists fs_q_b5ccsdce_right_decomp_entry. d = fs_q_b5ccsdce_right_decomp_entry * S ((S (l)) * e) + (a))) /\ ((exists fs_u_b5ccsdce_right_decomp_prefix fs_v_b5ccsdce_right_decomp_prefix. ((((exists fs_h_b5ccsdce_right_decomp_prefix_body_start. fs_h_b5ccsdce_right_decomp_prefix_body_start + S (0) = S ((S (0)) * fs_v_b5ccsdce_right_decomp_prefix)) /\ exists fs_q_b5ccsdce_right_decomp_prefix_body_start. fs_u_b5ccsdce_right_decomp_prefix = fs_q_b5ccsdce_right_decomp_prefix_body_start * S ((S (0)) * fs_v_b5ccsdce_right_decomp_prefix) + (0))) /\ ((((exists fs_h_b5ccsdce_right_decomp_prefix_body_terminal. fs_h_b5ccsdce_right_decomp_prefix_body_terminal + S (r) = S ((S (l)) * fs_v_b5ccsdce_right_decomp_prefix)) /\ exists fs_q_b5ccsdce_right_decomp_prefix_body_terminal. fs_u_b5ccsdce_right_decomp_prefix = fs_q_b5ccsdce_right_decomp_prefix_body_terminal * S ((S (l)) * fs_v_b5ccsdce_right_decomp_prefix) + (r))) /\ forall fs_i_b5ccsdce_right_decomp_prefix_body_steps. (exists fs_lt_b5ccsdce_right_decomp_prefix_body_steps_bound. fs_lt_b5ccsdce_right_decomp_prefix_body_steps_bound + S fs_i_b5ccsdce_right_decomp_prefix_body_steps = l) -> exists fs_a_b5ccsdce_right_decomp_prefix_body_steps fs_r_b5ccsdce_right_decomp_prefix_body_steps fs_s_b5ccsdce_right_decomp_prefix_body_steps. ((((exists fs_h_b5ccsdce_right_decomp_prefix_body_steps_summand. fs_h_b5ccsdce_right_decomp_prefix_body_steps_summand + S (fs_a_b5ccsdce_right_decomp_prefix_body_steps) = S ((S (fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * e)) /\ exists fs_q_b5ccsdce_right_decomp_prefix_body_steps_summand. d = fs_q_b5ccsdce_right_decomp_prefix_body_steps_summand * S ((S (fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * e) + (fs_a_b5ccsdce_right_decomp_prefix_body_steps))) /\ ((((exists fs_h_b5ccsdce_right_decomp_prefix_body_steps_partial. fs_h_b5ccsdce_right_decomp_prefix_body_steps_partial + S (fs_r_b5ccsdce_right_decomp_prefix_body_steps) = S ((S (fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * fs_v_b5ccsdce_right_decomp_prefix)) /\ exists fs_q_b5ccsdce_right_decomp_prefix_body_steps_partial. fs_u_b5ccsdce_right_decomp_prefix = fs_q_b5ccsdce_right_decomp_prefix_body_steps_partial * S ((S (fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * fs_v_b5ccsdce_right_decomp_prefix) + (fs_r_b5ccsdce_right_decomp_prefix_body_steps))) /\ ((((exists fs_h_b5ccsdce_right_decomp_prefix_body_steps_successor. fs_h_b5ccsdce_right_decomp_prefix_body_steps_successor + S (fs_s_b5ccsdce_right_decomp_prefix_body_steps) = S ((S (S fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * fs_v_b5ccsdce_right_decomp_prefix)) /\ exists fs_q_b5ccsdce_right_decomp_prefix_body_steps_successor. fs_u_b5ccsdce_right_decomp_prefix = fs_q_b5ccsdce_right_decomp_prefix_body_steps_successor * S ((S (S fs_i_b5ccsdce_right_decomp_prefix_body_steps)) * fs_v_b5ccsdce_right_decomp_prefix) + (fs_s_b5ccsdce_right_decomp_prefix_body_steps))) /\ fs_s_b5ccsdce_right_decomp_prefix_body_steps = fs_r_b5ccsdce_right_decomp_prefix_body_steps + fs_a_b5ccsdce_right_decomp_prefix_body_steps)))))) /\ A = r + a)
  59. 0059specialize beta_sum_succ_decompose d
  60. 0060specialize beta_sum_succ_decompose e
  61. 0061specialize beta_sum_succ_decompose l
  62. 0062specialize beta_sum_succ_decompose A
  63. 0063apply beta_sum_succ_decompose
  64. 0064exact hright
  65. 0065cases hright_decomp
  66. 0066cases hright_decomp_witness
  67. 0067cases hright_decomp_witness_witness
  68. 0068cases hright_decomp_witness_witness_right
  69. 0069have hcount_decomp : ∃ bit. ∃ r. BetaAt(f,g,l,bit) ∧ (BitCount(f,g,l,r) ∧ ((bit = 0 ∨ bit = 1) ∧ E = r + bit))
    Exact native replay linehave hcount_decomp : exists bit r. (((exists fs_h_b5ccsdce_count_last. fs_h_b5ccsdce_count_last + S (bit) = S ((S (l)) * g)) /\ exists fs_q_b5ccsdce_count_last. f = fs_q_b5ccsdce_count_last * S ((S (l)) * g) + (bit))) /\ ((((exists ff_u_b5ccsdce_count_prefix_sum ff_v_b5ccsdce_count_prefix_sum. ((((exists ff_h_b5ccsdce_count_prefix_sum_start. ff_h_b5ccsdce_count_prefix_sum_start + S (0) = S ((S (0)) * ff_v_b5ccsdce_count_prefix_sum)) /\ exists ff_q_b5ccsdce_count_prefix_sum_start. ff_u_b5ccsdce_count_prefix_sum = ff_q_b5ccsdce_count_prefix_sum_start * S ((S (0)) * ff_v_b5ccsdce_count_prefix_sum) + (0))) /\ ((((exists ff_h_b5ccsdce_count_prefix_sum_terminal. ff_h_b5ccsdce_count_prefix_sum_terminal + S (r) = S ((S (l)) * ff_v_b5ccsdce_count_prefix_sum)) /\ exists ff_q_b5ccsdce_count_prefix_sum_terminal. ff_u_b5ccsdce_count_prefix_sum = ff_q_b5ccsdce_count_prefix_sum_terminal * S ((S (l)) * ff_v_b5ccsdce_count_prefix_sum) + (r))) /\ forall ff_i_b5ccsdce_count_prefix_sum. (exists ff_lt_b5ccsdce_count_prefix_sum_bound. ff_lt_b5ccsdce_count_prefix_sum_bound + S ff_i_b5ccsdce_count_prefix_sum = l) -> exists ff_a_b5ccsdce_count_prefix_sum ff_r_b5ccsdce_count_prefix_sum ff_s_b5ccsdce_count_prefix_sum. ((((exists ff_h_b5ccsdce_count_prefix_sum_summand. ff_h_b5ccsdce_count_prefix_sum_summand + S (ff_a_b5ccsdce_count_prefix_sum) = S ((S (ff_i_b5ccsdce_count_prefix_sum)) * g)) /\ exists ff_q_b5ccsdce_count_prefix_sum_summand. f = ff_q_b5ccsdce_count_prefix_sum_summand * S ((S (ff_i_b5ccsdce_count_prefix_sum)) * g) + (ff_a_b5ccsdce_count_prefix_sum))) /\ ((((exists ff_h_b5ccsdce_count_prefix_sum_partial. ff_h_b5ccsdce_count_prefix_sum_partial + S (ff_r_b5ccsdce_count_prefix_sum) = S ((S (ff_i_b5ccsdce_count_prefix_sum)) * ff_v_b5ccsdce_count_prefix_sum)) /\ exists ff_q_b5ccsdce_count_prefix_sum_partial. ff_u_b5ccsdce_count_prefix_sum = ff_q_b5ccsdce_count_prefix_sum_partial * S ((S (ff_i_b5ccsdce_count_prefix_sum)) * ff_v_b5ccsdce_count_prefix_sum) + (ff_r_b5ccsdce_count_prefix_sum))) /\ ((((exists ff_h_b5ccsdce_count_prefix_sum_successor. ff_h_b5ccsdce_count_prefix_sum_successor + S (ff_s_b5ccsdce_count_prefix_sum) = S ((S (S ff_i_b5ccsdce_count_prefix_sum)) * ff_v_b5ccsdce_count_prefix_sum)) /\ exists ff_q_b5ccsdce_count_prefix_sum_successor. ff_u_b5ccsdce_count_prefix_sum = ff_q_b5ccsdce_count_prefix_sum_successor * S ((S (S ff_i_b5ccsdce_count_prefix_sum)) * ff_v_b5ccsdce_count_prefix_sum) + (ff_s_b5ccsdce_count_prefix_sum))) /\ ff_s_b5ccsdce_count_prefix_sum = ff_r_b5ccsdce_count_prefix_sum + ff_a_b5ccsdce_count_prefix_sum)))))) /\ (forall ff_i_b5ccsdce_count_prefix_bits. (exists ff_lt_b5ccsdce_count_prefix_bits_bound. ff_lt_b5ccsdce_count_prefix_bits_bound + S ff_i_b5ccsdce_count_prefix_bits = l) -> exists ff_bit_b5ccsdce_count_prefix_bits. ((((exists ff_h_b5ccsdce_count_prefix_bits_decoded. ff_h_b5ccsdce_count_prefix_bits_decoded + S (ff_bit_b5ccsdce_count_prefix_bits) = S ((S (ff_i_b5ccsdce_count_prefix_bits)) * g)) /\ exists ff_q_b5ccsdce_count_prefix_bits_decoded. f = ff_q_b5ccsdce_count_prefix_bits_decoded * S ((S (ff_i_b5ccsdce_count_prefix_bits)) * g) + (ff_bit_b5ccsdce_count_prefix_bits))) /\ (ff_bit_b5ccsdce_count_prefix_bits = 0 \/ ff_bit_b5ccsdce_count_prefix_bits = 1))))) /\ ((bit = 0 \/ bit = 1) /\ E = r + bit))
  70. 0070specialize bit_count_succ_decompose f
  71. 0071specialize bit_count_succ_decompose g
  72. 0072specialize bit_count_succ_decompose l
  73. 0073specialize bit_count_succ_decompose (S l)
  74. 0074specialize bit_count_succ_decompose E
  75. 0075apply bit_count_succ_decompose
  76. 0076refl
  77. 0077exact hcount
  78. 0078cases hcount_decomp
  79. 0079cases hcount_decomp_witness
  80. 0080cases hcount_decomp_witness_witness
  81. 0081cases hcount_decomp_witness_witness_right
  82. 0082cases hcount_decomp_witness_witness_right_right
  83. 0083have hterminal : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,l,q) ∧ (BetaAt(d,e,l,Q) ∧ (BetaAt(f,g,l,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))
    Exact native replay linehave hterminal : exists q Q bit. (((exists fs_h_b5ccsdce_terminal_left. fs_h_b5ccsdce_terminal_left + S (q) = S ((S (l)) * c)) /\ exists fs_q_b5ccsdce_terminal_left. b = fs_q_b5ccsdce_terminal_left * S ((S (l)) * c) + (q))) /\ ((((exists fs_h_b5ccsdce_terminal_right. fs_h_b5ccsdce_terminal_right + S (Q) = S ((S (l)) * e)) /\ exists fs_q_b5ccsdce_terminal_right. d = fs_q_b5ccsdce_terminal_right * S ((S (l)) * e) + (Q))) /\ ((((exists fs_h_b5ccsdce_terminal_bit. fs_h_b5ccsdce_terminal_bit + S (bit) = S ((S (l)) * g)) /\ exists fs_q_b5ccsdce_terminal_bit. f = fs_q_b5ccsdce_terminal_bit * S ((S (l)) * g) + (bit))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q))))))
  84. 0084specialize hcarry l
  85. 0085apply hcarry
  86. 0086specialize le_refl (S l)
  87. 0087exact le_refl
  88. 0088cases hterminal
  89. 0089cases hterminal_witness
  90. 0090cases hterminal_witness_witness
  91. 0091cases hterminal_witness_witness_witness
  92. 0092cases hterminal_witness_witness_witness_right
  93. 0093cases hterminal_witness_witness_witness_right_right
  94. 0094have hq : x = x6
  95. 0095specialize beta_at_unique b
  96. 0096specialize beta_at_unique c
  97. 0097specialize beta_at_unique l
  98. 0098specialize beta_at_unique x
  99. 0099specialize beta_at_unique x6
  100. 0100apply beta_at_unique
  101. 0101exact hleft_decomp_witness_witness_left
  102. 0102exact hterminal_witness_witness_witness_left
  103. 0103have hQ : x2 = x7
  104. 0104specialize beta_at_unique d
  105. 0105specialize beta_at_unique e
  106. 0106specialize beta_at_unique l
  107. 0107specialize beta_at_unique x2
  108. 0108specialize beta_at_unique x7
  109. 0109apply beta_at_unique
  110. 0110exact hright_decomp_witness_witness_left
  111. 0111exact hterminal_witness_witness_witness_right_left
  112. 0112have hbit : x4 = x8
  113. 0113specialize beta_at_unique f
  114. 0114specialize beta_at_unique g
  115. 0115specialize beta_at_unique l
  116. 0116specialize beta_at_unique x4
  117. 0117specialize beta_at_unique x8
  118. 0118apply beta_at_unique
  119. 0119exact hcount_decomp_witness_witness_left
  120. 0120exact hterminal_witness_witness_witness_right_right_left
  121. 0121rewrite hq at hleft_decomp_witness_witness_right_right
  122. 0122rewrite hQ at hright_decomp_witness_witness_right_right
  123. 0123rewrite hbit at hcount_decomp_witness_witness_right_right_right
  124. 0124have hprefix : ∀ b5cc_index_b5ccsdce_restricted. Lt(b5cc_index_b5ccsdce_restricted,l) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,b5cc_index_b5ccsdce_restricted,x) ∧ (BetaAt(d,e,b5cc_index_b5ccsdce_restricted,y) ∧ (BetaAt(f,g,b5cc_index_b5ccsdce_restricted,z) ∧ (z = 0 ∧ y = x + x ∨ z = 1 ∧ y = S (x + x))))
    Exact native replay linehave hprefix : forall b5cc_index_b5ccsdce_restricted. (exists bcf_lt_gap_b5ccsdce_restricted_bound. bcf_lt_gap_b5ccsdce_restricted_bound + S (b5cc_index_b5ccsdce_restricted) = l) -> exists b5cc_left_b5ccsdce_restricted b5cc_right_b5ccsdce_restricted b5cc_bit_b5ccsdce_restricted. (((exists fs_h_b5cc_b5ccsdce_restricted_left. fs_h_b5cc_b5ccsdce_restricted_left + S (b5cc_left_b5ccsdce_restricted) = S ((S (b5cc_index_b5ccsdce_restricted)) * c)) /\ exists fs_q_b5cc_b5ccsdce_restricted_left. b = fs_q_b5cc_b5ccsdce_restricted_left * S ((S (b5cc_index_b5ccsdce_restricted)) * c) + (b5cc_left_b5ccsdce_restricted))) /\ ((((exists fs_h_b5cc_b5ccsdce_restricted_right. fs_h_b5cc_b5ccsdce_restricted_right + S (b5cc_right_b5ccsdce_restricted) = S ((S (b5cc_index_b5ccsdce_restricted)) * e)) /\ exists fs_q_b5cc_b5ccsdce_restricted_right. d = fs_q_b5cc_b5ccsdce_restricted_right * S ((S (b5cc_index_b5ccsdce_restricted)) * e) + (b5cc_right_b5ccsdce_restricted))) /\ ((((exists fs_h_b5cc_b5ccsdce_restricted_bit. fs_h_b5cc_b5ccsdce_restricted_bit + S (b5cc_bit_b5ccsdce_restricted) = S ((S (b5cc_index_b5ccsdce_restricted)) * g)) /\ exists fs_q_b5cc_b5ccsdce_restricted_bit. f = fs_q_b5cc_b5ccsdce_restricted_bit * S ((S (b5cc_index_b5ccsdce_restricted)) * g) + (b5cc_bit_b5ccsdce_restricted))) /\ (((b5cc_bit_b5ccsdce_restricted = 0 /\ b5cc_right_b5ccsdce_restricted = b5cc_left_b5ccsdce_restricted + b5cc_left_b5ccsdce_restricted) \/ (b5cc_bit_b5ccsdce_restricted = 1 /\ b5cc_right_b5ccsdce_restricted = S (b5cc_left_b5ccsdce_restricted + b5cc_left_b5ccsdce_restricted))))))
  125. 0125specialize double_quotient_carry_prefix_restrict b
  126. 0126specialize double_quotient_carry_prefix_restrict c
  127. 0127specialize double_quotient_carry_prefix_restrict d
  128. 0128specialize double_quotient_carry_prefix_restrict e
  129. 0129specialize double_quotient_carry_prefix_restrict f
  130. 0130specialize double_quotient_carry_prefix_restrict g
  131. 0131specialize double_quotient_carry_prefix_restrict l
  132. 0132apply double_quotient_carry_prefix_restrict
  133. 0133exact hcarry
  134. 0134have hbalance : x3 = (x1 + x1) + x5
  135. 0135specialize IH x1
  136. 0136specialize IH x3
  137. 0137specialize IH x5
  138. 0138apply IH
  139. 0139exact hleft_decomp_witness_witness_right_left
  140. 0140exact hright_decomp_witness_witness_right_left
  141. 0141exact hprefix
  142. 0142exact hcount_decomp_witness_witness_right_left
  143. 0143have hinner : x5 + (x6 + (x6 + x1)) = x6 + (x6 + (x5 + x1))
  144. 0144have hleft_assoc : x5 + (x6 + (x6 + x1)) = (x5 + x6) + (x6 + x1)
  145. 0145symm
  146. 0146apply add_assoc
  147. 0147have hpermute : (x5 + x6) + (x6 + x1) = (x6 + x6) + (x5 + x1)
  148. 0148apply add_permute_outer
  149. 0149have hright_assoc : (x6 + x6) + (x5 + x1) = x6 + (x6 + (x5 + x1))
  150. 0150apply add_assoc
  151. 0151trans (x5 + x6) + (x6 + x1)
  152. 0152exact hleft_assoc
  153. 0153trans (x6 + x6) + (x5 + x1)
  154. 0154exact hpermute
  155. 0155exact hright_assoc
  156. 0156cases hterminal_witness_witness_witness_right_right_right
  157. 0157cases hterminal_witness_witness_witness_right_right_right_left
  158. 0158rewrite hright_decomp_witness_witness_right_right
  159. 0159rewrite hleft_decomp_witness_witness_right_right
  160. 0160rewrite hleft_decomp_witness_witness_right_right
  161. 0161rewrite hcount_decomp_witness_witness_right_right_right
  162. 0162rewrite hbalance
  163. 0163rewrite hterminal_witness_witness_witness_right_right_right_left_left
  164. 0164rewrite hterminal_witness_witness_witness_right_right_right_left_right
  165. 0165simp [add_assoc, add_comm]
  166. 0166cases hterminal_witness_witness_witness_right_right_right_right
  167. 0167rewrite hright_decomp_witness_witness_right_right
  168. 0168rewrite hleft_decomp_witness_witness_right_right
  169. 0169rewrite hleft_decomp_witness_witness_right_right
  170. 0170rewrite hcount_decomp_witness_witness_right_right_right
  171. 0171rewrite hbalance
  172. 0172rewrite hterminal_witness_witness_witness_right_right_right_right_left
  173. 0173rewrite hterminal_witness_witness_witness_right_right_right_right_right
  174. 0174simp [add_assoc, add_comm]