KU000B · theorem body

beta_sum_add_carry_exact

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

The sum-prefix quotient total equals both addend totals plus the exact carry count.

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

∀ lb. ∀ lc. ∀ rb. ∀ rc. ∀ tb. ∀ tc. ∀ cb. ∀ cc. ∀ l. ∀ L. ∀ M. ∀ T. ∀ E. Sum(lb,lc,l,L) → Sum(rb,rc,l,M) → Sum(tb,tc,l,T) → (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. BetaAt(lb,lc,x,y) ∧ (BetaAt(rb,rc,x,z) ∧ (BetaAt(tb,tc,x,n) ∧ (BetaAt(cb,cc,x,m) ∧ (m = 0 ∧ n = y + z ∨ m = 1 ∧ n = S (y + z)))))) → BitCount(cb,cc,l,E) → T = L + M + E

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount
Exact expanded first-order statement
forall lb lc rb rc tb tc cb cc l L M T E. (exists ff_u_kmcsace_left ff_v_kmcsace_left. ((((exists ff_h_kmcsace_left_start. ff_h_kmcsace_left_start + S (0) = S ((S (0)) * ff_v_kmcsace_left)) /\ exists ff_q_kmcsace_left_start. ff_u_kmcsace_left = ff_q_kmcsace_left_start * S ((S (0)) * ff_v_kmcsace_left) + (0))) /\ ((((exists ff_h_kmcsace_left_terminal. ff_h_kmcsace_left_terminal + S (L) = S ((S (l)) * ff_v_kmcsace_left)) /\ exists ff_q_kmcsace_left_terminal. ff_u_kmcsace_left = ff_q_kmcsace_left_terminal * S ((S (l)) * ff_v_kmcsace_left) + (L))) /\ forall ff_i_kmcsace_left. (exists ff_lt_kmcsace_left_bound. ff_lt_kmcsace_left_bound + S ff_i_kmcsace_left = l) -> exists ff_a_kmcsace_left ff_r_kmcsace_left ff_s_kmcsace_left. ((((exists ff_h_kmcsace_left_summand. ff_h_kmcsace_left_summand + S (ff_a_kmcsace_left) = S ((S (ff_i_kmcsace_left)) * lc)) /\ exists ff_q_kmcsace_left_summand. lb = ff_q_kmcsace_left_summand * S ((S (ff_i_kmcsace_left)) * lc) + (ff_a_kmcsace_left))) /\ ((((exists ff_h_kmcsace_left_partial. ff_h_kmcsace_left_partial + S (ff_r_kmcsace_left) = S ((S (ff_i_kmcsace_left)) * ff_v_kmcsace_left)) /\ exists ff_q_kmcsace_left_partial. ff_u_kmcsace_left = ff_q_kmcsace_left_partial * S ((S (ff_i_kmcsace_left)) * ff_v_kmcsace_left) + (ff_r_kmcsace_left))) /\ ((((exists ff_h_kmcsace_left_successor. ff_h_kmcsace_left_successor + S (ff_s_kmcsace_left) = S ((S (S ff_i_kmcsace_left)) * ff_v_kmcsace_left)) /\ exists ff_q_kmcsace_left_successor. ff_u_kmcsace_left = ff_q_kmcsace_left_successor * S ((S (S ff_i_kmcsace_left)) * ff_v_kmcsace_left) + (ff_s_kmcsace_left))) /\ ff_s_kmcsace_left = ff_r_kmcsace_left + ff_a_kmcsace_left)))))) -> (exists ff_u_kmcsace_right ff_v_kmcsace_right. ((((exists ff_h_kmcsace_right_start. ff_h_kmcsace_right_start + S (0) = S ((S (0)) * ff_v_kmcsace_right)) /\ exists ff_q_kmcsace_right_start. ff_u_kmcsace_right = ff_q_kmcsace_right_start * S ((S (0)) * ff_v_kmcsace_right) + (0))) /\ ((((exists ff_h_kmcsace_right_terminal. ff_h_kmcsace_right_terminal + S (M) = S ((S (l)) * ff_v_kmcsace_right)) /\ exists ff_q_kmcsace_right_terminal. ff_u_kmcsace_right = ff_q_kmcsace_right_terminal * S ((S (l)) * ff_v_kmcsace_right) + (M))) /\ forall ff_i_kmcsace_right. (exists ff_lt_kmcsace_right_bound. ff_lt_kmcsace_right_bound + S ff_i_kmcsace_right = l) -> exists ff_a_kmcsace_right ff_r_kmcsace_right ff_s_kmcsace_right. ((((exists ff_h_kmcsace_right_summand. ff_h_kmcsace_right_summand + S (ff_a_kmcsace_right) = S ((S (ff_i_kmcsace_right)) * rc)) /\ exists ff_q_kmcsace_right_summand. rb = ff_q_kmcsace_right_summand * S ((S (ff_i_kmcsace_right)) * rc) + (ff_a_kmcsace_right))) /\ ((((exists ff_h_kmcsace_right_partial. ff_h_kmcsace_right_partial + S (ff_r_kmcsace_right) = S ((S (ff_i_kmcsace_right)) * ff_v_kmcsace_right)) /\ exists ff_q_kmcsace_right_partial. ff_u_kmcsace_right = ff_q_kmcsace_right_partial * S ((S (ff_i_kmcsace_right)) * ff_v_kmcsace_right) + (ff_r_kmcsace_right))) /\ ((((exists ff_h_kmcsace_right_successor. ff_h_kmcsace_right_successor + S (ff_s_kmcsace_right) = S ((S (S ff_i_kmcsace_right)) * ff_v_kmcsace_right)) /\ exists ff_q_kmcsace_right_successor. ff_u_kmcsace_right = ff_q_kmcsace_right_successor * S ((S (S ff_i_kmcsace_right)) * ff_v_kmcsace_right) + (ff_s_kmcsace_right))) /\ ff_s_kmcsace_right = ff_r_kmcsace_right + ff_a_kmcsace_right)))))) -> (exists ff_u_kmcsace_total ff_v_kmcsace_total. ((((exists ff_h_kmcsace_total_start. ff_h_kmcsace_total_start + S (0) = S ((S (0)) * ff_v_kmcsace_total)) /\ exists ff_q_kmcsace_total_start. ff_u_kmcsace_total = ff_q_kmcsace_total_start * S ((S (0)) * ff_v_kmcsace_total) + (0))) /\ ((((exists ff_h_kmcsace_total_terminal. ff_h_kmcsace_total_terminal + S (T) = S ((S (l)) * ff_v_kmcsace_total)) /\ exists ff_q_kmcsace_total_terminal. ff_u_kmcsace_total = ff_q_kmcsace_total_terminal * S ((S (l)) * ff_v_kmcsace_total) + (T))) /\ forall ff_i_kmcsace_total. (exists ff_lt_kmcsace_total_bound. ff_lt_kmcsace_total_bound + S ff_i_kmcsace_total = l) -> exists ff_a_kmcsace_total ff_r_kmcsace_total ff_s_kmcsace_total. ((((exists ff_h_kmcsace_total_summand. ff_h_kmcsace_total_summand + S (ff_a_kmcsace_total) = S ((S (ff_i_kmcsace_total)) * tc)) /\ exists ff_q_kmcsace_total_summand. tb = ff_q_kmcsace_total_summand * S ((S (ff_i_kmcsace_total)) * tc) + (ff_a_kmcsace_total))) /\ ((((exists ff_h_kmcsace_total_partial. ff_h_kmcsace_total_partial + S (ff_r_kmcsace_total) = S ((S (ff_i_kmcsace_total)) * ff_v_kmcsace_total)) /\ exists ff_q_kmcsace_total_partial. ff_u_kmcsace_total = ff_q_kmcsace_total_partial * S ((S (ff_i_kmcsace_total)) * ff_v_kmcsace_total) + (ff_r_kmcsace_total))) /\ ((((exists ff_h_kmcsace_total_successor. ff_h_kmcsace_total_successor + S (ff_s_kmcsace_total) = S ((S (S ff_i_kmcsace_total)) * ff_v_kmcsace_total)) /\ exists ff_q_kmcsace_total_successor. ff_u_kmcsace_total = ff_q_kmcsace_total_successor * S ((S (S ff_i_kmcsace_total)) * ff_v_kmcsace_total) + (ff_s_kmcsace_total))) /\ ff_s_kmcsace_total = ff_r_kmcsace_total + ff_a_kmcsace_total)))))) -> (forall kmc_index_kmcsace_carry. (exists bcf_lt_gap_kmcsace_carry_bound. bcf_lt_gap_kmcsace_carry_bound + S (kmc_index_kmcsace_carry) = l) -> exists kmc_left_kmcsace_carry kmc_right_kmcsace_carry kmc_total_kmcsace_carry kmc_bit_kmcsace_carry. (((exists fs_h_kmcsace_carry_left. fs_h_kmcsace_carry_left + S (kmc_left_kmcsace_carry) = S ((S (kmc_index_kmcsace_carry)) * lc)) /\ exists fs_q_kmcsace_carry_left. lb = fs_q_kmcsace_carry_left * S ((S (kmc_index_kmcsace_carry)) * lc) + (kmc_left_kmcsace_carry))) /\ ((((exists fs_h_kmcsace_carry_right. fs_h_kmcsace_carry_right + S (kmc_right_kmcsace_carry) = S ((S (kmc_index_kmcsace_carry)) * rc)) /\ exists fs_q_kmcsace_carry_right. rb = fs_q_kmcsace_carry_right * S ((S (kmc_index_kmcsace_carry)) * rc) + (kmc_right_kmcsace_carry))) /\ ((((exists fs_h_kmcsace_carry_total. fs_h_kmcsace_carry_total + S (kmc_total_kmcsace_carry) = S ((S (kmc_index_kmcsace_carry)) * tc)) /\ exists fs_q_kmcsace_carry_total. tb = fs_q_kmcsace_carry_total * S ((S (kmc_index_kmcsace_carry)) * tc) + (kmc_total_kmcsace_carry))) /\ ((((exists fs_h_kmcsace_carry_bit. fs_h_kmcsace_carry_bit + S (kmc_bit_kmcsace_carry) = S ((S (kmc_index_kmcsace_carry)) * cc)) /\ exists fs_q_kmcsace_carry_bit. cb = fs_q_kmcsace_carry_bit * S ((S (kmc_index_kmcsace_carry)) * cc) + (kmc_bit_kmcsace_carry))) /\ (((kmc_bit_kmcsace_carry = 0 /\ kmc_total_kmcsace_carry = kmc_left_kmcsace_carry + kmc_right_kmcsace_carry) \/ (kmc_bit_kmcsace_carry = 1 /\ kmc_total_kmcsace_carry = S (kmc_left_kmcsace_carry + kmc_right_kmcsace_carry)))))))) -> (((exists ff_u_kmcsace_count_sum ff_v_kmcsace_count_sum. ((((exists ff_h_kmcsace_count_sum_start. ff_h_kmcsace_count_sum_start + S (0) = S ((S (0)) * ff_v_kmcsace_count_sum)) /\ exists ff_q_kmcsace_count_sum_start. ff_u_kmcsace_count_sum = ff_q_kmcsace_count_sum_start * S ((S (0)) * ff_v_kmcsace_count_sum) + (0))) /\ ((((exists ff_h_kmcsace_count_sum_terminal. ff_h_kmcsace_count_sum_terminal + S (E) = S ((S (l)) * ff_v_kmcsace_count_sum)) /\ exists ff_q_kmcsace_count_sum_terminal. ff_u_kmcsace_count_sum = ff_q_kmcsace_count_sum_terminal * S ((S (l)) * ff_v_kmcsace_count_sum) + (E))) /\ forall ff_i_kmcsace_count_sum. (exists ff_lt_kmcsace_count_sum_bound. ff_lt_kmcsace_count_sum_bound + S ff_i_kmcsace_count_sum = l) -> exists ff_a_kmcsace_count_sum ff_r_kmcsace_count_sum ff_s_kmcsace_count_sum. ((((exists ff_h_kmcsace_count_sum_summand. ff_h_kmcsace_count_sum_summand + S (ff_a_kmcsace_count_sum) = S ((S (ff_i_kmcsace_count_sum)) * cc)) /\ exists ff_q_kmcsace_count_sum_summand. cb = ff_q_kmcsace_count_sum_summand * S ((S (ff_i_kmcsace_count_sum)) * cc) + (ff_a_kmcsace_count_sum))) /\ ((((exists ff_h_kmcsace_count_sum_partial. ff_h_kmcsace_count_sum_partial + S (ff_r_kmcsace_count_sum) = S ((S (ff_i_kmcsace_count_sum)) * ff_v_kmcsace_count_sum)) /\ exists ff_q_kmcsace_count_sum_partial. ff_u_kmcsace_count_sum = ff_q_kmcsace_count_sum_partial * S ((S (ff_i_kmcsace_count_sum)) * ff_v_kmcsace_count_sum) + (ff_r_kmcsace_count_sum))) /\ ((((exists ff_h_kmcsace_count_sum_successor. ff_h_kmcsace_count_sum_successor + S (ff_s_kmcsace_count_sum) = S ((S (S ff_i_kmcsace_count_sum)) * ff_v_kmcsace_count_sum)) /\ exists ff_q_kmcsace_count_sum_successor. ff_u_kmcsace_count_sum = ff_q_kmcsace_count_sum_successor * S ((S (S ff_i_kmcsace_count_sum)) * ff_v_kmcsace_count_sum) + (ff_s_kmcsace_count_sum))) /\ ff_s_kmcsace_count_sum = ff_r_kmcsace_count_sum + ff_a_kmcsace_count_sum)))))) /\ (forall ff_i_kmcsace_count_bits. (exists ff_lt_kmcsace_count_bits_bound. ff_lt_kmcsace_count_bits_bound + S ff_i_kmcsace_count_bits = l) -> exists ff_bit_kmcsace_count_bits. ((((exists ff_h_kmcsace_count_bits_decoded. ff_h_kmcsace_count_bits_decoded + S (ff_bit_kmcsace_count_bits) = S ((S (ff_i_kmcsace_count_bits)) * cc)) /\ exists ff_q_kmcsace_count_bits_decoded. cb = ff_q_kmcsace_count_bits_decoded * S ((S (ff_i_kmcsace_count_bits)) * cc) + (ff_bit_kmcsace_count_bits))) /\ (ff_bit_kmcsace_count_bits = 0 \/ ff_bit_kmcsace_count_bits = 1))))) -> T = (L + M) + E

Proof neighborhood

Direct theorem prerequisites

beta_sum_zero · Stable closed beta_sum_succ_decompose · Stable closed bit_count_zero · Stable closed bit_count_succ_decompose · Stable closed beta_at_unique · Stable closed le_refl · Stable closed KU000A add_quotient_carry_prefix_restrict add_assoc · Stable closed add_comm · Stable closed add_shuffle_middle · Alpha closed

Direct theorem dependents

KU000C kummer_binomial_carry_bit_count

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

228 script commands · 37 reading checkpoints · 21 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 (1)
add quotient carry prefix restrict
01Fix variables and assumptionsL1–8

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

  1. L1
    intro lb
  2. L2
    intro lc
  3. L3
    intro rb
  4. L4
    intro rc
  5. L5
    intro tb
  6. L6
    intro tc
  7. L7
    intro cb
  8. L8
    intro cc
02Induction on lL9–18

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

  1. L9
    induction l
  2. L10
    intro L
  3. L11
    intro M
  4. L12
    intro T
  5. L13
    intro E
  6. L14
    intro hleft
  7. L15
    intro hright
  8. L16
    intro htotal
  9. L17
    intro hcarry
  10. L18
    intro hcount
03Establish hLL19–24

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

  1. L19
    have hL : L = 0
  2. L20
    specialize beta_sum_zero lb
  3. L21
    specialize beta_sum_zero lc
  4. L22
    specialize beta_sum_zero L
  5. L23
    apply beta_sum_zero
  6. L24
    exact hleft
04Establish hML25–30

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

  1. L25
    have hM : M = 0
  2. L26
    specialize beta_sum_zero rb
  3. L27
    specialize beta_sum_zero rc
  4. L28
    specialize beta_sum_zero M
  5. L29
    apply beta_sum_zero
  6. L30
    exact hright
05Establish hTL31–36

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

  1. L31
    have hT : T = 0
  2. L32
    specialize beta_sum_zero tb
  3. L33
    specialize beta_sum_zero tc
  4. L34
    specialize beta_sum_zero T
  5. L35
    apply beta_sum_zero
  6. L36
    exact htotal
06Establish hEL37–46

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

  1. L37
    have hE : E = 0
  2. L38
    specialize bit_count_zero cb
  3. L39
    specialize bit_count_zero cc
  4. L40
    specialize bit_count_zero 0
  5. L41
    specialize bit_count_zero E
  6. L42
    apply bit_count_zero
  7. L43
    refl
  8. L44
    exact hcount
  9. L45
    rewrite hT
  10. L46
    rewrite hL
07Calculate and transport equalitiesL47–49

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

  1. L47
    rewrite hM
  2. L48
    rewrite hE
  3. L49
    simp
08Fix variables and assumptionsL50–58

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

  1. L50
    intro L
  2. L51
    intro M
  3. L52
    intro T
  4. L53
    intro E
  5. L54
    intro hleft
  6. L55
    intro hright
  7. L56
    intro htotal
  8. L57
    intro hcarry
  9. L58
    intro hcount
09Establish hleft_decompL59–65

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

  1. L59
    have hleft_decomp : ∃ z. ∃ u. BetaAt(lb,lc,l,z) ∧ (Sum(lb,lc,l,u) ∧ L = u + z)Definitions: BetaAt(lb,lc,l,z)Sum(lb,lc,l,u)Original native command in the exact edition
  2. L60
    specialize beta_sum_succ_decompose lb
  3. L61
    specialize beta_sum_succ_decompose lc
  4. L62
    specialize beta_sum_succ_decompose l
  5. L63
    specialize beta_sum_succ_decompose L
  6. L64
    apply beta_sum_succ_decompose
  7. L65
    exact hleft
10Separate the logical casesL66–69

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

  1. L66
    cases hleft_decomp
  2. L67
    cases hleft_decomp_witness
  3. L68
    cases hleft_decomp_witness_witness
  4. L69
    cases hleft_decomp_witness_witness_right
11Establish hright_decompL70–76

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

  1. L70
    have hright_decomp : ∃ z. ∃ u. BetaAt(rb,rc,l,z) ∧ (Sum(rb,rc,l,u) ∧ M = u + z)Definitions: BetaAt(rb,rc,l,z)Sum(rb,rc,l,u)Original native command in the exact edition
  2. L71
    specialize beta_sum_succ_decompose rb
  3. L72
    specialize beta_sum_succ_decompose rc
  4. L73
    specialize beta_sum_succ_decompose l
  5. L74
    specialize beta_sum_succ_decompose M
  6. L75
    apply beta_sum_succ_decompose
  7. L76
    exact hright
12Separate the logical casesL77–80

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

  1. L77
    cases hright_decomp
  2. L78
    cases hright_decomp_witness
  3. L79
    cases hright_decomp_witness_witness
  4. L80
    cases hright_decomp_witness_witness_right
13Establish htotal_decompL81–87

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

  1. L81
    have htotal_decomp : ∃ z. ∃ u. BetaAt(tb,tc,l,z) ∧ (Sum(tb,tc,l,u) ∧ T = u + z)Definitions: BetaAt(tb,tc,l,z)Sum(tb,tc,l,u)Original native command in the exact edition
  2. L82
    specialize beta_sum_succ_decompose tb
  3. L83
    specialize beta_sum_succ_decompose tc
  4. L84
    specialize beta_sum_succ_decompose l
  5. L85
    specialize beta_sum_succ_decompose T
  6. L86
    apply beta_sum_succ_decompose
  7. L87
    exact htotal
14Separate the logical casesL88–91

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

  1. L88
    cases htotal_decomp
  2. L89
    cases htotal_decomp_witness
  3. L90
    cases htotal_decomp_witness_witness
  4. L91
    cases htotal_decomp_witness_witness_right
15Establish hcount_decompL92–100

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

  1. L92
    have hcount_decomp : ∃ bit. ∃ z. BetaAt(cb,cc,l,bit) ∧ (BitCount(cb,cc,l,z) ∧ ((bit = 0 ∨ bit = 1) ∧ E = z + bit))Definitions: BetaAt(cb,cc,l,bit)BitCount(cb,cc,l,z)Original native command in the exact edition
  2. L93
    specialize bit_count_succ_decompose cb
  3. L94
    specialize bit_count_succ_decompose cc
  4. L95
    specialize bit_count_succ_decompose l
  5. L96
    specialize bit_count_succ_decompose (S l)
  6. L97
    specialize bit_count_succ_decompose E
  7. L98
    apply bit_count_succ_decompose
  8. L99
    refl
  9. L100
    exact hcount
16Separate the logical casesL101–105

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

  1. L101
    cases hcount_decomp
  2. L102
    cases hcount_decomp_witness
  3. L103
    cases hcount_decomp_witness_witness
  4. L104
    cases hcount_decomp_witness_witness_right
  5. L105
    cases hcount_decomp_witness_witness_right_right
17Establish hterminalL106–110

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

  1. L106
    have hterminal : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,l,q) ∧ (BetaAt(rb,rc,l,s) ∧ (BetaAt(tb,tc,l,Q) ∧ (BetaAt(cb,cc,l,bit) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s)))))Definitions: BetaAt(lb,lc,l,q)BetaAt(rb,rc,l,s)BetaAt(tb,tc,l,Q)BetaAt(cb,cc,l,bit)Original native command in the exact edition
  2. L107
    specialize hcarry l
  3. L108
    apply hcarry
  4. L109
    specialize le_refl (S l)
  5. L110
    exact le_refl
18Separate the logical casesL111–118

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

  1. L111
    cases hterminal
  2. L112
    cases hterminal_witness
  3. L113
    cases hterminal_witness_witness
  4. L114
    cases hterminal_witness_witness_witness
  5. L115
    cases hterminal_witness_witness_witness_witness
  6. L116
    cases hterminal_witness_witness_witness_witness_right
  7. L117
    cases hterminal_witness_witness_witness_witness_right_right
  8. L118
    cases hterminal_witness_witness_witness_witness_right_right_right
19Establish hqL119–127

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

  1. L119
    have hq : x = x8
  2. L120
    specialize beta_at_unique lb
  3. L121
    specialize beta_at_unique lc
  4. L122
    specialize beta_at_unique l
  5. L123
    specialize beta_at_unique x
  6. L124
    specialize beta_at_unique x8
  7. L125
    apply beta_at_unique
  8. L126
    exact hleft_decomp_witness_witness_left
  9. L127
    exact hterminal_witness_witness_witness_witness_left
20Establish hsL128–136

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

  1. L128
    have hs : x2 = x9
  2. L129
    specialize beta_at_unique rb
  3. L130
    specialize beta_at_unique rc
  4. L131
    specialize beta_at_unique l
  5. L132
    specialize beta_at_unique x2
  6. L133
    specialize beta_at_unique x9
  7. L134
    apply beta_at_unique
  8. L135
    exact hright_decomp_witness_witness_left
  9. L136
    exact hterminal_witness_witness_witness_witness_right_left
21Establish hQL137–145

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

  1. L137
    have hQ : x4 = x10
  2. L138
    specialize beta_at_unique tb
  3. L139
    specialize beta_at_unique tc
  4. L140
    specialize beta_at_unique l
  5. L141
    specialize beta_at_unique x4
  6. L142
    specialize beta_at_unique x10
  7. L143
    apply beta_at_unique
  8. L144
    exact htotal_decomp_witness_witness_left
  9. L145
    exact hterminal_witness_witness_witness_witness_right_right_left
22Establish hbitL146–155

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

  1. L146
    have hbit : x6 = x11
  2. L147
    specialize beta_at_unique cb
  3. L148
    specialize beta_at_unique cc
  4. L149
    specialize beta_at_unique l
  5. L150
    specialize beta_at_unique x6
  6. L151
    specialize beta_at_unique x11
  7. L152
    apply beta_at_unique
  8. L153
    exact hcount_decomp_witness_witness_left
  9. L154
    exact hterminal_witness_witness_witness_witness_right_right_right_left
  10. L155
    rewrite hq at hleft_decomp_witness_witness_right_right
23Calculate and transport equalitiesL156–158

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

  1. L156
    rewrite hs at hright_decomp_witness_witness_right_right
  2. L157
    rewrite hQ at htotal_decomp_witness_witness_right_right
  3. L158
    rewrite hbit at hcount_decomp_witness_witness_right_right_right
24Establish hprefixL159–168

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

  1. L159
    have hprefix : ∀ kmc_index_kmcsace_restricted. Lt(kmc_index_kmcsace_restricted,l) → ∃ x. ∃ y. ∃ z. ∃ n. BetaAt(lb,lc,kmc_index_kmcsace_restricted,x) ∧ (BetaAt(rb,rc,kmc_index_kmcsace_restricted,y) ∧ (BetaAt(tb,tc,kmc_index_kmcsace_restricted,z) ∧ (BetaAt(cb,cc,kmc_index_kmcsace_restricted,n) ∧ (n = 0 ∧ z = x + y ∨ n = 1 ∧ z = S (x + y)))))Definitions: Lt(kmc_index_kmcsace_restricted,l)BetaAt(lb,lc,kmc_index_kmcsace_restricted,x)BetaAt(rb,rc,kmc_index_kmcsace_restricted,y)BetaAt(tb,tc,kmc_index_kmcsace_restricted,z)BetaAt(cb,cc,kmc_index_kmcsace_restricted,n)Original native command in the exact edition
  2. L160
    specialize add_quotient_carry_prefix_restrict lb
  3. L161
    specialize add_quotient_carry_prefix_restrict lc
  4. L162
    specialize add_quotient_carry_prefix_restrict rb
  5. L163
    specialize add_quotient_carry_prefix_restrict rc
  6. L164
    specialize add_quotient_carry_prefix_restrict tb
  7. L165
    specialize add_quotient_carry_prefix_restrict tc
  8. L166
    specialize add_quotient_carry_prefix_restrict cb
  9. L167
    specialize add_quotient_carry_prefix_restrict cc
  10. L168
    specialize add_quotient_carry_prefix_restrict l
25Use earlier factsL169–170

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

  1. L169
    apply add_quotient_carry_prefix_restrict
  2. L170
    exact hcarry
26Establish hbalanceL171–180

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

  1. L171
    have hbalance : x5 = (x1 + x3) + x7
  2. L172
    specialize IH x1
  3. L173
    specialize IH x3
  4. L174
    specialize IH x5
  5. L175
    specialize IH x7
  6. L176
    apply IH
  7. L177
    exact hleft_decomp_witness_witness_right_left
  8. L178
    exact hright_decomp_witness_witness_right_left
  9. L179
    exact htotal_decomp_witness_witness_right_left
  10. L180
    exact hprefix
27Use earlier factsL181–181

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

  1. L181
    exact hcount_decomp_witness_witness_right_left
28Establish hinnerL182–182

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

  1. L182
    have hinner : x3 + (x7 + (x8 + (x9 + x1))) = x8 + (x3 + (x9 + (x7 + x1)))
29Establish hleft_assocL183–185

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

  1. L183
    have hleft_assoc : x3 + (x7 + (x8 + (x9 + x1))) = (x3 + x7) + (x8 + (x9 + x1))
  2. L184
    symm
  3. L185
    apply add_assoc
30Establish hshuffleL186–187

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

  1. L186
    have hshuffle : (x3 + x7) + (x8 + (x9 + x1)) = (x3 + x8) + (x7 + (x9 + x1))
  2. L187
    apply add_shuffle_middle
31Establish hswapL188–196

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

  1. L188
    have hswap : x7 + (x9 + x1) = x9 + (x7 + x1)
  2. L189
    trans (x7 + x9) + x1
  3. L190
    symm
  4. L191
    apply add_assoc
  5. L192
    trans (x9 + x7) + x1
  6. L193
    congr
  7. L194
    apply add_comm
  8. L195
    refl
  9. L196
    apply add_assoc
32Establish hpermuteL197–200

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

  1. L197
    have hpermute : (x3 + x8) + (x7 + (x9 + x1)) = (x8 + x3) + (x9 + (x7 + x1))
  2. L198
    congr
  3. L199
    apply add_comm
  4. L200
    exact hswap
33Establish hright_assocL201–209

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

  1. L201
    have hright_assoc : (x8 + x3) + (x9 + (x7 + x1)) = x8 + (x3 + (x9 + (x7 + x1)))
  2. L202
    apply add_assoc
  3. L203
    trans (x3 + x7) + (x8 + (x9 + x1))
  4. L204
    exact hleft_assoc
  5. L205
    trans (x3 + x8) + (x7 + (x9 + x1))
  6. L206
    exact hshuffle
  7. L207
    trans (x8 + x3) + (x9 + (x7 + x1))
  8. L208
    exact hpermute
  9. L209
    exact hright_assoc
34Separate the logical casesL210–211

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

  1. L210
    cases hterminal_witness_witness_witness_witness_right_right_right_right
  2. L211
    cases hterminal_witness_witness_witness_witness_right_right_right_right_left
35Calculate and transport equalitiesL212–219

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

  1. L212
    rewrite htotal_decomp_witness_witness_right_right
  2. L213
    rewrite hleft_decomp_witness_witness_right_right
  3. L214
    rewrite hright_decomp_witness_witness_right_right
  4. L215
    rewrite hcount_decomp_witness_witness_right_right_right
  5. L216
    rewrite hbalance
  6. L217
    rewrite hterminal_witness_witness_witness_witness_right_right_right_right_left_left
  7. L218
    rewrite hterminal_witness_witness_witness_witness_right_right_right_right_left_right
  8. L219
    simp [add_assoc, add_comm]
36Separate the logical casesL220–220

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

  1. L220
    cases hterminal_witness_witness_witness_witness_right_right_right_right_right
37Calculate and transport equalitiesL221–228

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

  1. L221
    rewrite htotal_decomp_witness_witness_right_right
  2. L222
    rewrite hleft_decomp_witness_witness_right_right
  3. L223
    rewrite hright_decomp_witness_witness_right_right
  4. L224
    rewrite hcount_decomp_witness_witness_right_right_right
  5. L225
    rewrite hbalance
  6. L226
    rewrite hterminal_witness_witness_witness_witness_right_right_right_right_right_left
  7. L227
    rewrite hterminal_witness_witness_witness_witness_right_right_right_right_right_right
  8. L228
    simp [add_assoc, add_comm]

Library-wide reading audit

Original defined command ledger · 228 lines
  1. 0001intro lb
  2. 0002intro lc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro cb
  8. 0008intro cc
  9. 0009induction l
  10. 0010intro L
  11. 0011intro M
  12. 0012intro T
  13. 0013intro E
  14. 0014intro hleft
  15. 0015intro hright
  16. 0016intro htotal
  17. 0017intro hcarry
  18. 0018intro hcount
  19. 0019have hL : L = 0
  20. 0020specialize beta_sum_zero lb
  21. 0021specialize beta_sum_zero lc
  22. 0022specialize beta_sum_zero L
  23. 0023apply beta_sum_zero
  24. 0024exact hleft
  25. 0025have hM : M = 0
  26. 0026specialize beta_sum_zero rb
  27. 0027specialize beta_sum_zero rc
  28. 0028specialize beta_sum_zero M
  29. 0029apply beta_sum_zero
  30. 0030exact hright
  31. 0031have hT : T = 0
  32. 0032specialize beta_sum_zero tb
  33. 0033specialize beta_sum_zero tc
  34. 0034specialize beta_sum_zero T
  35. 0035apply beta_sum_zero
  36. 0036exact htotal
  37. 0037have hE : E = 0
  38. 0038specialize bit_count_zero cb
  39. 0039specialize bit_count_zero cc
  40. 0040specialize bit_count_zero 0
  41. 0041specialize bit_count_zero E
  42. 0042apply bit_count_zero
  43. 0043refl
  44. 0044exact hcount
  45. 0045rewrite hT
  46. 0046rewrite hL
  47. 0047rewrite hM
  48. 0048rewrite hE
  49. 0049simp
  50. 0050intro L
  51. 0051intro M
  52. 0052intro T
  53. 0053intro E
  54. 0054intro hleft
  55. 0055intro hright
  56. 0056intro htotal
  57. 0057intro hcarry
  58. 0058intro hcount
  59. 0059have hleft_decomp : ∃ z. ∃ u. BetaAt(lb,lc,l,z) ∧ (Sum(lb,lc,l,u) ∧ L = u + z)
    Exact native replay linehave hleft_decomp : exists z u. (((exists fs_h_kmcsace_left_decomp_entry. fs_h_kmcsace_left_decomp_entry + S (z) = S ((S (l)) * lc)) /\ exists fs_q_kmcsace_left_decomp_entry. lb = fs_q_kmcsace_left_decomp_entry * S ((S (l)) * lc) + (z))) /\ ((exists fs_u_kmcsace_left_decomp_prefix fs_v_kmcsace_left_decomp_prefix. ((((exists fs_h_kmcsace_left_decomp_prefix_body_start. fs_h_kmcsace_left_decomp_prefix_body_start + S (0) = S ((S (0)) * fs_v_kmcsace_left_decomp_prefix)) /\ exists fs_q_kmcsace_left_decomp_prefix_body_start. fs_u_kmcsace_left_decomp_prefix = fs_q_kmcsace_left_decomp_prefix_body_start * S ((S (0)) * fs_v_kmcsace_left_decomp_prefix) + (0))) /\ ((((exists fs_h_kmcsace_left_decomp_prefix_body_terminal. fs_h_kmcsace_left_decomp_prefix_body_terminal + S (u) = S ((S (l)) * fs_v_kmcsace_left_decomp_prefix)) /\ exists fs_q_kmcsace_left_decomp_prefix_body_terminal. fs_u_kmcsace_left_decomp_prefix = fs_q_kmcsace_left_decomp_prefix_body_terminal * S ((S (l)) * fs_v_kmcsace_left_decomp_prefix) + (u))) /\ forall fs_i_kmcsace_left_decomp_prefix_body_steps. (exists fs_lt_kmcsace_left_decomp_prefix_body_steps_bound. fs_lt_kmcsace_left_decomp_prefix_body_steps_bound + S fs_i_kmcsace_left_decomp_prefix_body_steps = l) -> exists fs_a_kmcsace_left_decomp_prefix_body_steps fs_r_kmcsace_left_decomp_prefix_body_steps fs_s_kmcsace_left_decomp_prefix_body_steps. ((((exists fs_h_kmcsace_left_decomp_prefix_body_steps_summand. fs_h_kmcsace_left_decomp_prefix_body_steps_summand + S (fs_a_kmcsace_left_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_left_decomp_prefix_body_steps)) * lc)) /\ exists fs_q_kmcsace_left_decomp_prefix_body_steps_summand. lb = fs_q_kmcsace_left_decomp_prefix_body_steps_summand * S ((S (fs_i_kmcsace_left_decomp_prefix_body_steps)) * lc) + (fs_a_kmcsace_left_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_left_decomp_prefix_body_steps_partial. fs_h_kmcsace_left_decomp_prefix_body_steps_partial + S (fs_r_kmcsace_left_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_left_decomp_prefix_body_steps)) * fs_v_kmcsace_left_decomp_prefix)) /\ exists fs_q_kmcsace_left_decomp_prefix_body_steps_partial. fs_u_kmcsace_left_decomp_prefix = fs_q_kmcsace_left_decomp_prefix_body_steps_partial * S ((S (fs_i_kmcsace_left_decomp_prefix_body_steps)) * fs_v_kmcsace_left_decomp_prefix) + (fs_r_kmcsace_left_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_left_decomp_prefix_body_steps_successor. fs_h_kmcsace_left_decomp_prefix_body_steps_successor + S (fs_s_kmcsace_left_decomp_prefix_body_steps) = S ((S (S fs_i_kmcsace_left_decomp_prefix_body_steps)) * fs_v_kmcsace_left_decomp_prefix)) /\ exists fs_q_kmcsace_left_decomp_prefix_body_steps_successor. fs_u_kmcsace_left_decomp_prefix = fs_q_kmcsace_left_decomp_prefix_body_steps_successor * S ((S (S fs_i_kmcsace_left_decomp_prefix_body_steps)) * fs_v_kmcsace_left_decomp_prefix) + (fs_s_kmcsace_left_decomp_prefix_body_steps))) /\ fs_s_kmcsace_left_decomp_prefix_body_steps = fs_r_kmcsace_left_decomp_prefix_body_steps + fs_a_kmcsace_left_decomp_prefix_body_steps)))))) /\ L = u + z)
  60. 0060specialize beta_sum_succ_decompose lb
  61. 0061specialize beta_sum_succ_decompose lc
  62. 0062specialize beta_sum_succ_decompose l
  63. 0063specialize beta_sum_succ_decompose L
  64. 0064apply beta_sum_succ_decompose
  65. 0065exact hleft
  66. 0066cases hleft_decomp
  67. 0067cases hleft_decomp_witness
  68. 0068cases hleft_decomp_witness_witness
  69. 0069cases hleft_decomp_witness_witness_right
  70. 0070have hright_decomp : ∃ z. ∃ u. BetaAt(rb,rc,l,z) ∧ (Sum(rb,rc,l,u) ∧ M = u + z)
    Exact native replay linehave hright_decomp : exists z u. (((exists fs_h_kmcsace_right_decomp_entry. fs_h_kmcsace_right_decomp_entry + S (z) = S ((S (l)) * rc)) /\ exists fs_q_kmcsace_right_decomp_entry. rb = fs_q_kmcsace_right_decomp_entry * S ((S (l)) * rc) + (z))) /\ ((exists fs_u_kmcsace_right_decomp_prefix fs_v_kmcsace_right_decomp_prefix. ((((exists fs_h_kmcsace_right_decomp_prefix_body_start. fs_h_kmcsace_right_decomp_prefix_body_start + S (0) = S ((S (0)) * fs_v_kmcsace_right_decomp_prefix)) /\ exists fs_q_kmcsace_right_decomp_prefix_body_start. fs_u_kmcsace_right_decomp_prefix = fs_q_kmcsace_right_decomp_prefix_body_start * S ((S (0)) * fs_v_kmcsace_right_decomp_prefix) + (0))) /\ ((((exists fs_h_kmcsace_right_decomp_prefix_body_terminal. fs_h_kmcsace_right_decomp_prefix_body_terminal + S (u) = S ((S (l)) * fs_v_kmcsace_right_decomp_prefix)) /\ exists fs_q_kmcsace_right_decomp_prefix_body_terminal. fs_u_kmcsace_right_decomp_prefix = fs_q_kmcsace_right_decomp_prefix_body_terminal * S ((S (l)) * fs_v_kmcsace_right_decomp_prefix) + (u))) /\ forall fs_i_kmcsace_right_decomp_prefix_body_steps. (exists fs_lt_kmcsace_right_decomp_prefix_body_steps_bound. fs_lt_kmcsace_right_decomp_prefix_body_steps_bound + S fs_i_kmcsace_right_decomp_prefix_body_steps = l) -> exists fs_a_kmcsace_right_decomp_prefix_body_steps fs_r_kmcsace_right_decomp_prefix_body_steps fs_s_kmcsace_right_decomp_prefix_body_steps. ((((exists fs_h_kmcsace_right_decomp_prefix_body_steps_summand. fs_h_kmcsace_right_decomp_prefix_body_steps_summand + S (fs_a_kmcsace_right_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_right_decomp_prefix_body_steps)) * rc)) /\ exists fs_q_kmcsace_right_decomp_prefix_body_steps_summand. rb = fs_q_kmcsace_right_decomp_prefix_body_steps_summand * S ((S (fs_i_kmcsace_right_decomp_prefix_body_steps)) * rc) + (fs_a_kmcsace_right_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_right_decomp_prefix_body_steps_partial. fs_h_kmcsace_right_decomp_prefix_body_steps_partial + S (fs_r_kmcsace_right_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_right_decomp_prefix_body_steps)) * fs_v_kmcsace_right_decomp_prefix)) /\ exists fs_q_kmcsace_right_decomp_prefix_body_steps_partial. fs_u_kmcsace_right_decomp_prefix = fs_q_kmcsace_right_decomp_prefix_body_steps_partial * S ((S (fs_i_kmcsace_right_decomp_prefix_body_steps)) * fs_v_kmcsace_right_decomp_prefix) + (fs_r_kmcsace_right_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_right_decomp_prefix_body_steps_successor. fs_h_kmcsace_right_decomp_prefix_body_steps_successor + S (fs_s_kmcsace_right_decomp_prefix_body_steps) = S ((S (S fs_i_kmcsace_right_decomp_prefix_body_steps)) * fs_v_kmcsace_right_decomp_prefix)) /\ exists fs_q_kmcsace_right_decomp_prefix_body_steps_successor. fs_u_kmcsace_right_decomp_prefix = fs_q_kmcsace_right_decomp_prefix_body_steps_successor * S ((S (S fs_i_kmcsace_right_decomp_prefix_body_steps)) * fs_v_kmcsace_right_decomp_prefix) + (fs_s_kmcsace_right_decomp_prefix_body_steps))) /\ fs_s_kmcsace_right_decomp_prefix_body_steps = fs_r_kmcsace_right_decomp_prefix_body_steps + fs_a_kmcsace_right_decomp_prefix_body_steps)))))) /\ M = u + z)
  71. 0071specialize beta_sum_succ_decompose rb
  72. 0072specialize beta_sum_succ_decompose rc
  73. 0073specialize beta_sum_succ_decompose l
  74. 0074specialize beta_sum_succ_decompose M
  75. 0075apply beta_sum_succ_decompose
  76. 0076exact hright
  77. 0077cases hright_decomp
  78. 0078cases hright_decomp_witness
  79. 0079cases hright_decomp_witness_witness
  80. 0080cases hright_decomp_witness_witness_right
  81. 0081have htotal_decomp : ∃ z. ∃ u. BetaAt(tb,tc,l,z) ∧ (Sum(tb,tc,l,u) ∧ T = u + z)
    Exact native replay linehave htotal_decomp : exists z u. (((exists fs_h_kmcsace_total_decomp_entry. fs_h_kmcsace_total_decomp_entry + S (z) = S ((S (l)) * tc)) /\ exists fs_q_kmcsace_total_decomp_entry. tb = fs_q_kmcsace_total_decomp_entry * S ((S (l)) * tc) + (z))) /\ ((exists fs_u_kmcsace_total_decomp_prefix fs_v_kmcsace_total_decomp_prefix. ((((exists fs_h_kmcsace_total_decomp_prefix_body_start. fs_h_kmcsace_total_decomp_prefix_body_start + S (0) = S ((S (0)) * fs_v_kmcsace_total_decomp_prefix)) /\ exists fs_q_kmcsace_total_decomp_prefix_body_start. fs_u_kmcsace_total_decomp_prefix = fs_q_kmcsace_total_decomp_prefix_body_start * S ((S (0)) * fs_v_kmcsace_total_decomp_prefix) + (0))) /\ ((((exists fs_h_kmcsace_total_decomp_prefix_body_terminal. fs_h_kmcsace_total_decomp_prefix_body_terminal + S (u) = S ((S (l)) * fs_v_kmcsace_total_decomp_prefix)) /\ exists fs_q_kmcsace_total_decomp_prefix_body_terminal. fs_u_kmcsace_total_decomp_prefix = fs_q_kmcsace_total_decomp_prefix_body_terminal * S ((S (l)) * fs_v_kmcsace_total_decomp_prefix) + (u))) /\ forall fs_i_kmcsace_total_decomp_prefix_body_steps. (exists fs_lt_kmcsace_total_decomp_prefix_body_steps_bound. fs_lt_kmcsace_total_decomp_prefix_body_steps_bound + S fs_i_kmcsace_total_decomp_prefix_body_steps = l) -> exists fs_a_kmcsace_total_decomp_prefix_body_steps fs_r_kmcsace_total_decomp_prefix_body_steps fs_s_kmcsace_total_decomp_prefix_body_steps. ((((exists fs_h_kmcsace_total_decomp_prefix_body_steps_summand. fs_h_kmcsace_total_decomp_prefix_body_steps_summand + S (fs_a_kmcsace_total_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_total_decomp_prefix_body_steps)) * tc)) /\ exists fs_q_kmcsace_total_decomp_prefix_body_steps_summand. tb = fs_q_kmcsace_total_decomp_prefix_body_steps_summand * S ((S (fs_i_kmcsace_total_decomp_prefix_body_steps)) * tc) + (fs_a_kmcsace_total_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_total_decomp_prefix_body_steps_partial. fs_h_kmcsace_total_decomp_prefix_body_steps_partial + S (fs_r_kmcsace_total_decomp_prefix_body_steps) = S ((S (fs_i_kmcsace_total_decomp_prefix_body_steps)) * fs_v_kmcsace_total_decomp_prefix)) /\ exists fs_q_kmcsace_total_decomp_prefix_body_steps_partial. fs_u_kmcsace_total_decomp_prefix = fs_q_kmcsace_total_decomp_prefix_body_steps_partial * S ((S (fs_i_kmcsace_total_decomp_prefix_body_steps)) * fs_v_kmcsace_total_decomp_prefix) + (fs_r_kmcsace_total_decomp_prefix_body_steps))) /\ ((((exists fs_h_kmcsace_total_decomp_prefix_body_steps_successor. fs_h_kmcsace_total_decomp_prefix_body_steps_successor + S (fs_s_kmcsace_total_decomp_prefix_body_steps) = S ((S (S fs_i_kmcsace_total_decomp_prefix_body_steps)) * fs_v_kmcsace_total_decomp_prefix)) /\ exists fs_q_kmcsace_total_decomp_prefix_body_steps_successor. fs_u_kmcsace_total_decomp_prefix = fs_q_kmcsace_total_decomp_prefix_body_steps_successor * S ((S (S fs_i_kmcsace_total_decomp_prefix_body_steps)) * fs_v_kmcsace_total_decomp_prefix) + (fs_s_kmcsace_total_decomp_prefix_body_steps))) /\ fs_s_kmcsace_total_decomp_prefix_body_steps = fs_r_kmcsace_total_decomp_prefix_body_steps + fs_a_kmcsace_total_decomp_prefix_body_steps)))))) /\ T = u + z)
  82. 0082specialize beta_sum_succ_decompose tb
  83. 0083specialize beta_sum_succ_decompose tc
  84. 0084specialize beta_sum_succ_decompose l
  85. 0085specialize beta_sum_succ_decompose T
  86. 0086apply beta_sum_succ_decompose
  87. 0087exact htotal
  88. 0088cases htotal_decomp
  89. 0089cases htotal_decomp_witness
  90. 0090cases htotal_decomp_witness_witness
  91. 0091cases htotal_decomp_witness_witness_right
  92. 0092have hcount_decomp : ∃ bit. ∃ z. BetaAt(cb,cc,l,bit) ∧ (BitCount(cb,cc,l,z) ∧ ((bit = 0 ∨ bit = 1) ∧ E = z + bit))
    Exact native replay linehave hcount_decomp : exists bit z. (((exists fs_h_kmcsace_count_last. fs_h_kmcsace_count_last + S (bit) = S ((S (l)) * cc)) /\ exists fs_q_kmcsace_count_last. cb = fs_q_kmcsace_count_last * S ((S (l)) * cc) + (bit))) /\ ((((exists ff_u_kmcsace_count_previous_sum ff_v_kmcsace_count_previous_sum. ((((exists ff_h_kmcsace_count_previous_sum_start. ff_h_kmcsace_count_previous_sum_start + S (0) = S ((S (0)) * ff_v_kmcsace_count_previous_sum)) /\ exists ff_q_kmcsace_count_previous_sum_start. ff_u_kmcsace_count_previous_sum = ff_q_kmcsace_count_previous_sum_start * S ((S (0)) * ff_v_kmcsace_count_previous_sum) + (0))) /\ ((((exists ff_h_kmcsace_count_previous_sum_terminal. ff_h_kmcsace_count_previous_sum_terminal + S (z) = S ((S (l)) * ff_v_kmcsace_count_previous_sum)) /\ exists ff_q_kmcsace_count_previous_sum_terminal. ff_u_kmcsace_count_previous_sum = ff_q_kmcsace_count_previous_sum_terminal * S ((S (l)) * ff_v_kmcsace_count_previous_sum) + (z))) /\ forall ff_i_kmcsace_count_previous_sum. (exists ff_lt_kmcsace_count_previous_sum_bound. ff_lt_kmcsace_count_previous_sum_bound + S ff_i_kmcsace_count_previous_sum = l) -> exists ff_a_kmcsace_count_previous_sum ff_r_kmcsace_count_previous_sum ff_s_kmcsace_count_previous_sum. ((((exists ff_h_kmcsace_count_previous_sum_summand. ff_h_kmcsace_count_previous_sum_summand + S (ff_a_kmcsace_count_previous_sum) = S ((S (ff_i_kmcsace_count_previous_sum)) * cc)) /\ exists ff_q_kmcsace_count_previous_sum_summand. cb = ff_q_kmcsace_count_previous_sum_summand * S ((S (ff_i_kmcsace_count_previous_sum)) * cc) + (ff_a_kmcsace_count_previous_sum))) /\ ((((exists ff_h_kmcsace_count_previous_sum_partial. ff_h_kmcsace_count_previous_sum_partial + S (ff_r_kmcsace_count_previous_sum) = S ((S (ff_i_kmcsace_count_previous_sum)) * ff_v_kmcsace_count_previous_sum)) /\ exists ff_q_kmcsace_count_previous_sum_partial. ff_u_kmcsace_count_previous_sum = ff_q_kmcsace_count_previous_sum_partial * S ((S (ff_i_kmcsace_count_previous_sum)) * ff_v_kmcsace_count_previous_sum) + (ff_r_kmcsace_count_previous_sum))) /\ ((((exists ff_h_kmcsace_count_previous_sum_successor. ff_h_kmcsace_count_previous_sum_successor + S (ff_s_kmcsace_count_previous_sum) = S ((S (S ff_i_kmcsace_count_previous_sum)) * ff_v_kmcsace_count_previous_sum)) /\ exists ff_q_kmcsace_count_previous_sum_successor. ff_u_kmcsace_count_previous_sum = ff_q_kmcsace_count_previous_sum_successor * S ((S (S ff_i_kmcsace_count_previous_sum)) * ff_v_kmcsace_count_previous_sum) + (ff_s_kmcsace_count_previous_sum))) /\ ff_s_kmcsace_count_previous_sum = ff_r_kmcsace_count_previous_sum + ff_a_kmcsace_count_previous_sum)))))) /\ (forall ff_i_kmcsace_count_previous_bits. (exists ff_lt_kmcsace_count_previous_bits_bound. ff_lt_kmcsace_count_previous_bits_bound + S ff_i_kmcsace_count_previous_bits = l) -> exists ff_bit_kmcsace_count_previous_bits. ((((exists ff_h_kmcsace_count_previous_bits_decoded. ff_h_kmcsace_count_previous_bits_decoded + S (ff_bit_kmcsace_count_previous_bits) = S ((S (ff_i_kmcsace_count_previous_bits)) * cc)) /\ exists ff_q_kmcsace_count_previous_bits_decoded. cb = ff_q_kmcsace_count_previous_bits_decoded * S ((S (ff_i_kmcsace_count_previous_bits)) * cc) + (ff_bit_kmcsace_count_previous_bits))) /\ (ff_bit_kmcsace_count_previous_bits = 0 \/ ff_bit_kmcsace_count_previous_bits = 1))))) /\ ((bit = 0 \/ bit = 1) /\ E = z + bit))
  93. 0093specialize bit_count_succ_decompose cb
  94. 0094specialize bit_count_succ_decompose cc
  95. 0095specialize bit_count_succ_decompose l
  96. 0096specialize bit_count_succ_decompose (S l)
  97. 0097specialize bit_count_succ_decompose E
  98. 0098apply bit_count_succ_decompose
  99. 0099refl
  100. 0100exact hcount
  101. 0101cases hcount_decomp
  102. 0102cases hcount_decomp_witness
  103. 0103cases hcount_decomp_witness_witness
  104. 0104cases hcount_decomp_witness_witness_right
  105. 0105cases hcount_decomp_witness_witness_right_right
  106. 0106have hterminal : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,l,q) ∧ (BetaAt(rb,rc,l,s) ∧ (BetaAt(tb,tc,l,Q) ∧ (BetaAt(cb,cc,l,bit) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s)))))
    Exact native replay linehave hterminal : exists q s Q bit. (((exists fs_h_kmcsace_terminal_left. fs_h_kmcsace_terminal_left + S (q) = S ((S (l)) * lc)) /\ exists fs_q_kmcsace_terminal_left. lb = fs_q_kmcsace_terminal_left * S ((S (l)) * lc) + (q))) /\ ((((exists fs_h_kmcsace_terminal_right. fs_h_kmcsace_terminal_right + S (s) = S ((S (l)) * rc)) /\ exists fs_q_kmcsace_terminal_right. rb = fs_q_kmcsace_terminal_right * S ((S (l)) * rc) + (s))) /\ ((((exists fs_h_kmcsace_terminal_total. fs_h_kmcsace_terminal_total + S (Q) = S ((S (l)) * tc)) /\ exists fs_q_kmcsace_terminal_total. tb = fs_q_kmcsace_terminal_total * S ((S (l)) * tc) + (Q))) /\ ((((exists fs_h_kmcsace_terminal_bit. fs_h_kmcsace_terminal_bit + S (bit) = S ((S (l)) * cc)) /\ exists fs_q_kmcsace_terminal_bit. cb = fs_q_kmcsace_terminal_bit * S ((S (l)) * cc) + (bit))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s)))))))
  107. 0107specialize hcarry l
  108. 0108apply hcarry
  109. 0109specialize le_refl (S l)
  110. 0110exact le_refl
  111. 0111cases hterminal
  112. 0112cases hterminal_witness
  113. 0113cases hterminal_witness_witness
  114. 0114cases hterminal_witness_witness_witness
  115. 0115cases hterminal_witness_witness_witness_witness
  116. 0116cases hterminal_witness_witness_witness_witness_right
  117. 0117cases hterminal_witness_witness_witness_witness_right_right
  118. 0118cases hterminal_witness_witness_witness_witness_right_right_right
  119. 0119have hq : x = x8
  120. 0120specialize beta_at_unique lb
  121. 0121specialize beta_at_unique lc
  122. 0122specialize beta_at_unique l
  123. 0123specialize beta_at_unique x
  124. 0124specialize beta_at_unique x8
  125. 0125apply beta_at_unique
  126. 0126exact hleft_decomp_witness_witness_left
  127. 0127exact hterminal_witness_witness_witness_witness_left
  128. 0128have hs : x2 = x9
  129. 0129specialize beta_at_unique rb
  130. 0130specialize beta_at_unique rc
  131. 0131specialize beta_at_unique l
  132. 0132specialize beta_at_unique x2
  133. 0133specialize beta_at_unique x9
  134. 0134apply beta_at_unique
  135. 0135exact hright_decomp_witness_witness_left
  136. 0136exact hterminal_witness_witness_witness_witness_right_left
  137. 0137have hQ : x4 = x10
  138. 0138specialize beta_at_unique tb
  139. 0139specialize beta_at_unique tc
  140. 0140specialize beta_at_unique l
  141. 0141specialize beta_at_unique x4
  142. 0142specialize beta_at_unique x10
  143. 0143apply beta_at_unique
  144. 0144exact htotal_decomp_witness_witness_left
  145. 0145exact hterminal_witness_witness_witness_witness_right_right_left
  146. 0146have hbit : x6 = x11
  147. 0147specialize beta_at_unique cb
  148. 0148specialize beta_at_unique cc
  149. 0149specialize beta_at_unique l
  150. 0150specialize beta_at_unique x6
  151. 0151specialize beta_at_unique x11
  152. 0152apply beta_at_unique
  153. 0153exact hcount_decomp_witness_witness_left
  154. 0154exact hterminal_witness_witness_witness_witness_right_right_right_left
  155. 0155rewrite hq at hleft_decomp_witness_witness_right_right
  156. 0156rewrite hs at hright_decomp_witness_witness_right_right
  157. 0157rewrite hQ at htotal_decomp_witness_witness_right_right
  158. 0158rewrite hbit at hcount_decomp_witness_witness_right_right_right
  159. 0159have hprefix : ∀ kmc_index_kmcsace_restricted. Lt(kmc_index_kmcsace_restricted,l) → ∃ x. ∃ y. ∃ z. ∃ n. BetaAt(lb,lc,kmc_index_kmcsace_restricted,x) ∧ (BetaAt(rb,rc,kmc_index_kmcsace_restricted,y) ∧ (BetaAt(tb,tc,kmc_index_kmcsace_restricted,z) ∧ (BetaAt(cb,cc,kmc_index_kmcsace_restricted,n) ∧ (n = 0 ∧ z = x + y ∨ n = 1 ∧ z = S (x + y)))))
    Exact native replay linehave hprefix : forall kmc_index_kmcsace_restricted. (exists bcf_lt_gap_kmcsace_restricted_bound. bcf_lt_gap_kmcsace_restricted_bound + S (kmc_index_kmcsace_restricted) = l) -> exists kmc_left_kmcsace_restricted kmc_right_kmcsace_restricted kmc_total_kmcsace_restricted kmc_bit_kmcsace_restricted. (((exists fs_h_kmcsace_restricted_left. fs_h_kmcsace_restricted_left + S (kmc_left_kmcsace_restricted) = S ((S (kmc_index_kmcsace_restricted)) * lc)) /\ exists fs_q_kmcsace_restricted_left. lb = fs_q_kmcsace_restricted_left * S ((S (kmc_index_kmcsace_restricted)) * lc) + (kmc_left_kmcsace_restricted))) /\ ((((exists fs_h_kmcsace_restricted_right. fs_h_kmcsace_restricted_right + S (kmc_right_kmcsace_restricted) = S ((S (kmc_index_kmcsace_restricted)) * rc)) /\ exists fs_q_kmcsace_restricted_right. rb = fs_q_kmcsace_restricted_right * S ((S (kmc_index_kmcsace_restricted)) * rc) + (kmc_right_kmcsace_restricted))) /\ ((((exists fs_h_kmcsace_restricted_total. fs_h_kmcsace_restricted_total + S (kmc_total_kmcsace_restricted) = S ((S (kmc_index_kmcsace_restricted)) * tc)) /\ exists fs_q_kmcsace_restricted_total. tb = fs_q_kmcsace_restricted_total * S ((S (kmc_index_kmcsace_restricted)) * tc) + (kmc_total_kmcsace_restricted))) /\ ((((exists fs_h_kmcsace_restricted_bit. fs_h_kmcsace_restricted_bit + S (kmc_bit_kmcsace_restricted) = S ((S (kmc_index_kmcsace_restricted)) * cc)) /\ exists fs_q_kmcsace_restricted_bit. cb = fs_q_kmcsace_restricted_bit * S ((S (kmc_index_kmcsace_restricted)) * cc) + (kmc_bit_kmcsace_restricted))) /\ (((kmc_bit_kmcsace_restricted = 0 /\ kmc_total_kmcsace_restricted = kmc_left_kmcsace_restricted + kmc_right_kmcsace_restricted) \/ (kmc_bit_kmcsace_restricted = 1 /\ kmc_total_kmcsace_restricted = S (kmc_left_kmcsace_restricted + kmc_right_kmcsace_restricted)))))))
  160. 0160specialize add_quotient_carry_prefix_restrict lb
  161. 0161specialize add_quotient_carry_prefix_restrict lc
  162. 0162specialize add_quotient_carry_prefix_restrict rb
  163. 0163specialize add_quotient_carry_prefix_restrict rc
  164. 0164specialize add_quotient_carry_prefix_restrict tb
  165. 0165specialize add_quotient_carry_prefix_restrict tc
  166. 0166specialize add_quotient_carry_prefix_restrict cb
  167. 0167specialize add_quotient_carry_prefix_restrict cc
  168. 0168specialize add_quotient_carry_prefix_restrict l
  169. 0169apply add_quotient_carry_prefix_restrict
  170. 0170exact hcarry
  171. 0171have hbalance : x5 = (x1 + x3) + x7
  172. 0172specialize IH x1
  173. 0173specialize IH x3
  174. 0174specialize IH x5
  175. 0175specialize IH x7
  176. 0176apply IH
  177. 0177exact hleft_decomp_witness_witness_right_left
  178. 0178exact hright_decomp_witness_witness_right_left
  179. 0179exact htotal_decomp_witness_witness_right_left
  180. 0180exact hprefix
  181. 0181exact hcount_decomp_witness_witness_right_left
  182. 0182have hinner : x3 + (x7 + (x8 + (x9 + x1))) = x8 + (x3 + (x9 + (x7 + x1)))
  183. 0183have hleft_assoc : x3 + (x7 + (x8 + (x9 + x1))) = (x3 + x7) + (x8 + (x9 + x1))
  184. 0184symm
  185. 0185apply add_assoc
  186. 0186have hshuffle : (x3 + x7) + (x8 + (x9 + x1)) = (x3 + x8) + (x7 + (x9 + x1))
  187. 0187apply add_shuffle_middle
  188. 0188have hswap : x7 + (x9 + x1) = x9 + (x7 + x1)
  189. 0189trans (x7 + x9) + x1
  190. 0190symm
  191. 0191apply add_assoc
  192. 0192trans (x9 + x7) + x1
  193. 0193congr
  194. 0194apply add_comm
  195. 0195refl
  196. 0196apply add_assoc
  197. 0197have hpermute : (x3 + x8) + (x7 + (x9 + x1)) = (x8 + x3) + (x9 + (x7 + x1))
  198. 0198congr
  199. 0199apply add_comm
  200. 0200exact hswap
  201. 0201have hright_assoc : (x8 + x3) + (x9 + (x7 + x1)) = x8 + (x3 + (x9 + (x7 + x1)))
  202. 0202apply add_assoc
  203. 0203trans (x3 + x7) + (x8 + (x9 + x1))
  204. 0204exact hleft_assoc
  205. 0205trans (x3 + x8) + (x7 + (x9 + x1))
  206. 0206exact hshuffle
  207. 0207trans (x8 + x3) + (x9 + (x7 + x1))
  208. 0208exact hpermute
  209. 0209exact hright_assoc
  210. 0210cases hterminal_witness_witness_witness_witness_right_right_right_right
  211. 0211cases hterminal_witness_witness_witness_witness_right_right_right_right_left
  212. 0212rewrite htotal_decomp_witness_witness_right_right
  213. 0213rewrite hleft_decomp_witness_witness_right_right
  214. 0214rewrite hright_decomp_witness_witness_right_right
  215. 0215rewrite hcount_decomp_witness_witness_right_right_right
  216. 0216rewrite hbalance
  217. 0217rewrite hterminal_witness_witness_witness_witness_right_right_right_right_left_left
  218. 0218rewrite hterminal_witness_witness_witness_witness_right_right_right_right_left_right
  219. 0219simp [add_assoc, add_comm]
  220. 0220cases hterminal_witness_witness_witness_witness_right_right_right_right_right
  221. 0221rewrite htotal_decomp_witness_witness_right_right
  222. 0222rewrite hleft_decomp_witness_witness_right_right
  223. 0223rewrite hright_decomp_witness_witness_right_right
  224. 0224rewrite hcount_decomp_witness_witness_right_right_right
  225. 0225rewrite hbalance
  226. 0226rewrite hterminal_witness_witness_witness_witness_right_right_right_right_right_left
  227. 0227rewrite hterminal_witness_witness_witness_witness_right_right_right_right_right_right
  228. 0228simp [add_assoc, add_comm]