PA00EE · theorem

complementary_bit_counts_add_length

Alpha v34 checked-use theorem · independently closed; not Stable

Complementary decoded bit prefixes have counts summing to their length.

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. ∀ z. ∀ e. ∀ l. ∀ n. ∀ m. BitCount(b,c,l,n) → BitCount(z,e,l,m) → (∀ x. ∀ y. ∀ k. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,e,x,k) → y = 0 ∧ k = 1 ∨ y = 1 ∧ k = 0) → n + m = l

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0017 BitCount

5 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

7 occurrences

Exact expanded native-PA statement
forall b c z e l n m. (((exists ff_u_complement_left_sum ff_v_complement_left_sum. ((((exists ff_h_complement_left_sum_start. ff_h_complement_left_sum_start + S (0) = S ((S (0)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_start. ff_u_complement_left_sum = ff_q_complement_left_sum_start * S ((S (0)) * ff_v_complement_left_sum) + (0))) /\ ((((exists ff_h_complement_left_sum_terminal. ff_h_complement_left_sum_terminal + S (n) = S ((S (l)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_terminal. ff_u_complement_left_sum = ff_q_complement_left_sum_terminal * S ((S (l)) * ff_v_complement_left_sum) + (n))) /\ forall ff_i_complement_left_sum. (exists ff_lt_complement_left_sum_bound. ff_lt_complement_left_sum_bound + S ff_i_complement_left_sum = l) -> exists ff_a_complement_left_sum ff_r_complement_left_sum ff_s_complement_left_sum. ((((exists ff_h_complement_left_sum_summand. ff_h_complement_left_sum_summand + S (ff_a_complement_left_sum) = S ((S (ff_i_complement_left_sum)) * c)) /\ exists ff_q_complement_left_sum_summand. b = ff_q_complement_left_sum_summand * S ((S (ff_i_complement_left_sum)) * c) + (ff_a_complement_left_sum))) /\ ((((exists ff_h_complement_left_sum_partial. ff_h_complement_left_sum_partial + S (ff_r_complement_left_sum) = S ((S (ff_i_complement_left_sum)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_partial. ff_u_complement_left_sum = ff_q_complement_left_sum_partial * S ((S (ff_i_complement_left_sum)) * ff_v_complement_left_sum) + (ff_r_complement_left_sum))) /\ ((((exists ff_h_complement_left_sum_successor. ff_h_complement_left_sum_successor + S (ff_s_complement_left_sum) = S ((S (S ff_i_complement_left_sum)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_successor. ff_u_complement_left_sum = ff_q_complement_left_sum_successor * S ((S (S ff_i_complement_left_sum)) * ff_v_complement_left_sum) + (ff_s_complement_left_sum))) /\ ff_s_complement_left_sum = ff_r_complement_left_sum + ff_a_complement_left_sum)))))) /\ (forall ff_i_complement_left_bits. (exists ff_lt_complement_left_bits_bound. ff_lt_complement_left_bits_bound + S ff_i_complement_left_bits = l) -> exists ff_bit_complement_left_bits. ((((exists ff_h_complement_left_bits_decoded. ff_h_complement_left_bits_decoded + S (ff_bit_complement_left_bits) = S ((S (ff_i_complement_left_bits)) * c)) /\ exists ff_q_complement_left_bits_decoded. b = ff_q_complement_left_bits_decoded * S ((S (ff_i_complement_left_bits)) * c) + (ff_bit_complement_left_bits))) /\ (ff_bit_complement_left_bits = 0 \/ ff_bit_complement_left_bits = 1))))) -> (((exists ff_u_complement_right_sum ff_v_complement_right_sum. ((((exists ff_h_complement_right_sum_start. ff_h_complement_right_sum_start + S (0) = S ((S (0)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_start. ff_u_complement_right_sum = ff_q_complement_right_sum_start * S ((S (0)) * ff_v_complement_right_sum) + (0))) /\ ((((exists ff_h_complement_right_sum_terminal. ff_h_complement_right_sum_terminal + S (m) = S ((S (l)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_terminal. ff_u_complement_right_sum = ff_q_complement_right_sum_terminal * S ((S (l)) * ff_v_complement_right_sum) + (m))) /\ forall ff_i_complement_right_sum. (exists ff_lt_complement_right_sum_bound. ff_lt_complement_right_sum_bound + S ff_i_complement_right_sum = l) -> exists ff_a_complement_right_sum ff_r_complement_right_sum ff_s_complement_right_sum. ((((exists ff_h_complement_right_sum_summand. ff_h_complement_right_sum_summand + S (ff_a_complement_right_sum) = S ((S (ff_i_complement_right_sum)) * e)) /\ exists ff_q_complement_right_sum_summand. z = ff_q_complement_right_sum_summand * S ((S (ff_i_complement_right_sum)) * e) + (ff_a_complement_right_sum))) /\ ((((exists ff_h_complement_right_sum_partial. ff_h_complement_right_sum_partial + S (ff_r_complement_right_sum) = S ((S (ff_i_complement_right_sum)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_partial. ff_u_complement_right_sum = ff_q_complement_right_sum_partial * S ((S (ff_i_complement_right_sum)) * ff_v_complement_right_sum) + (ff_r_complement_right_sum))) /\ ((((exists ff_h_complement_right_sum_successor. ff_h_complement_right_sum_successor + S (ff_s_complement_right_sum) = S ((S (S ff_i_complement_right_sum)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_successor. ff_u_complement_right_sum = ff_q_complement_right_sum_successor * S ((S (S ff_i_complement_right_sum)) * ff_v_complement_right_sum) + (ff_s_complement_right_sum))) /\ ff_s_complement_right_sum = ff_r_complement_right_sum + ff_a_complement_right_sum)))))) /\ (forall ff_i_complement_right_bits. (exists ff_lt_complement_right_bits_bound. ff_lt_complement_right_bits_bound + S ff_i_complement_right_bits = l) -> exists ff_bit_complement_right_bits. ((((exists ff_h_complement_right_bits_decoded. ff_h_complement_right_bits_decoded + S (ff_bit_complement_right_bits) = S ((S (ff_i_complement_right_bits)) * e)) /\ exists ff_q_complement_right_bits_decoded. z = ff_q_complement_right_bits_decoded * S ((S (ff_i_complement_right_bits)) * e) + (ff_bit_complement_right_bits))) /\ (ff_bit_complement_right_bits = 0 \/ ff_bit_complement_right_bits = 1))))) -> (forall i a d. (exists h. h + S i = l) -> (((exists ff_h_complement_left_entry. ff_h_complement_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_complement_left_entry. b = ff_q_complement_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_complement_right_entry. ff_h_complement_right_entry + S (d) = S ((S (i)) * e)) /\ exists ff_q_complement_right_entry. z = ff_q_complement_right_entry * S ((S (i)) * e) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))) -> n + m = l

Proof neighborhood

Direct theorem prerequisites

PA0048 bit_count_zero PA0042 bit_count_succ_decompose PA002O le_succ PA001A le_refl PA000E add_succ_left

Direct theorem dependents

PA00EF eisenstein_row_transposed_column_count_partition

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

112 script commands · 23 reading checkpoints · 7 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 (5)
bit count zerobit count succ decomposele succle refladd succ left
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro e
02Induction on lL5–10

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

  1. L5
    induction l
  2. L6
    intro n
  3. L7
    intro m
  4. L8
    intro hleft
  5. L9
    intro hright
  6. L10
    intro hcomplement
03Establish hnL11–18

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

  1. L11
    have hn : n = 0
  2. L12
    specialize bit_count_zero b
  3. L13
    specialize bit_count_zero c
  4. L14
    specialize bit_count_zero 0
  5. L15
    specialize bit_count_zero n
  6. L16
    apply bit_count_zero
  7. L17
    refl
  8. L18
    exact hleft
04Establish hmL19–28

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

  1. L19
    have hm : m = 0
  2. L20
    specialize bit_count_zero z
  3. L21
    specialize bit_count_zero e
  4. L22
    specialize bit_count_zero 0
  5. L23
    specialize bit_count_zero m
  6. L24
    apply bit_count_zero
  7. L25
    refl
  8. L26
    exact hright
  9. L27
    rewrite hn
  10. L28
    rewrite hm
05Calculate and transport equalitiesL29–29

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

  1. L29
    simp
06Fix variables and assumptionsL30–34

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

  1. L30
    intro n
  2. L31
    intro m
  3. L32
    intro hleft
  4. L33
    intro hright
  5. L34
    intro hcomplement
07Establish hleft_decompL35–43

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

  1. L35
    have hleft_decomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (BitCount(b,c,l,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))Definitions: BetaAt(b,c,l,a)BitCount(b,c,l,r)Original native command in the exact edition
  2. L36
    specialize bit_count_succ_decompose b
  3. L37
    specialize bit_count_succ_decompose c
  4. L38
    specialize bit_count_succ_decompose l
  5. L39
    specialize bit_count_succ_decompose (S l)
  6. L40
    specialize bit_count_succ_decompose n
  7. L41
    apply bit_count_succ_decompose
  8. L42
    refl
  9. L43
    exact hleft
08Separate the logical casesL44–48

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

  1. L44
    cases hleft_decomp
  2. L45
    cases hleft_decomp_witness
  3. L46
    cases hleft_decomp_witness_witness
  4. L47
    cases hleft_decomp_witness_witness_right
  5. L48
    cases hleft_decomp_witness_witness_right_right
09Establish hright_decompL49–57

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

  1. L49
    have hright_decomp : ∃ d. ∃ s. BetaAt(z,e,l,d) ∧ (BitCount(z,e,l,s) ∧ ((d = 0 ∨ d = 1) ∧ m = s + d))Definitions: BetaAt(z,e,l,d)BitCount(z,e,l,s)Original native command in the exact edition
  2. L50
    specialize bit_count_succ_decompose z
  3. L51
    specialize bit_count_succ_decompose e
  4. L52
    specialize bit_count_succ_decompose l
  5. L53
    specialize bit_count_succ_decompose (S l)
  6. L54
    specialize bit_count_succ_decompose m
  7. L55
    apply bit_count_succ_decompose
  8. L56
    refl
  9. L57
    exact hright
10Separate the logical casesL58–62

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

  1. L58
    cases hright_decomp
  2. L59
    cases hright_decomp_witness
  3. L60
    cases hright_decomp_witness_witness
  4. L61
    cases hright_decomp_witness_witness_right
  5. L62
    cases hright_decomp_witness_witness_right_right
11Establish hprefix_complementL63–72

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

  1. L63
    have hprefix_complement : ∀ i. ∀ a. ∀ d. Lt(i,l) → BetaAt(b,c,i,a) → BetaAt(z,e,i,d) → a = 0 ∧ d = 1 ∨ a = 1 ∧ d = 0Definitions: Lt(i,l)BetaAt(b,c,i,a)BetaAt(z,e,i,d)Original native command in the exact edition
  2. L64
    intro i
  3. L65
    intro a
  4. L66
    intro d
  5. L67
    intro hi
  6. L68
    intro ha
  7. L69
    intro hd
  8. L70
    specialize hcomplement i
  9. L71
    specialize hcomplement a
  10. L72
    specialize hcomplement d
12Use earlier factsL73–79

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

  1. L73
    apply hcomplement
  2. L74
    specialize le_succ (S i)
  3. L75
    specialize le_succ l
  4. L76
    apply le_succ
  5. L77
    exact hi
  6. L78
    exact ha
  7. L79
    exact hd
13Establish hprefixL80–86

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

  1. L80
    have hprefix : x1 + x3 = l
  2. L81
    specialize IH x1
  3. L82
    specialize IH x3
  4. L83
    apply IH
  5. L84
    exact hleft_decomp_witness_witness_right_left
  6. L85
    exact hright_decomp_witness_witness_right_left
  7. L86
    exact hprefix_complement
14Establish hlastL87–96

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

  1. L87
    have hlast : ((x = 0 /\ x2 = 1) \/ (x = 1 /\ x2 = 0))
  2. L88
    specialize hcomplement l
  3. L89
    specialize hcomplement x
  4. L90
    specialize hcomplement x2
  5. L91
    apply hcomplement
  6. L92
    specialize le_refl (S l)
  7. L93
    exact le_refl
  8. L94
    exact hleft_decomp_witness_witness_left
  9. L95
    exact hright_decomp_witness_witness_left
  10. L96
    rewrite hleft_decomp_witness_witness_right_right_right
15Calculate and transport equalitiesL97–97

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

  1. L97
    rewrite hright_decomp_witness_witness_right_right_right
16Separate the logical casesL98–99

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

  1. L98
    cases hlast
  2. L99
    cases hlast_left
17Calculate and transport equalitiesL100–102

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

  1. L100
    rewrite hlast_left_left
  2. L101
    rewrite hlast_left_right
  3. L102
    simp
18Separate the logical casesL103–103

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

  1. L103
    cases hlast_right
19Calculate and transport equalitiesL104–106

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

  1. L104
    rewrite hlast_right_left
  2. L105
    rewrite hlast_right_right
  3. L106
    simp
20Use earlier factsL107–108

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

  1. L107
    specialize add_succ_left x1
  2. L108
    specialize add_succ_left x3
21Calculate and transport equalitiesL109–109

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

  1. L109
    trans S (x1 + x3)
22Use earlier factsL110–110

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

  1. L110
    exact add_succ_left
23Calculate and transport equalitiesL111–112

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

  1. L111
    rewrite hprefix
  2. L112
    refl

Library-wide reading audit

Original defined command ledger · 112 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005induction l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010intro hcomplement
  11. 0011have hn : n = 0
  12. 0012specialize bit_count_zero b
  13. 0013specialize bit_count_zero c
  14. 0014specialize bit_count_zero 0
  15. 0015specialize bit_count_zero n
  16. 0016apply bit_count_zero
  17. 0017refl
  18. 0018exact hleft
  19. 0019have hm : m = 0
  20. 0020specialize bit_count_zero z
  21. 0021specialize bit_count_zero e
  22. 0022specialize bit_count_zero 0
  23. 0023specialize bit_count_zero m
  24. 0024apply bit_count_zero
  25. 0025refl
  26. 0026exact hright
  27. 0027rewrite hn
  28. 0028rewrite hm
  29. 0029simp
  30. 0030intro n
  31. 0031intro m
  32. 0032intro hleft
  33. 0033intro hright
  34. 0034intro hcomplement
  35. 0035have hleft_decomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (BitCount(b,c,l,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))
    Exact native replay linehave hleft_decomp : exists a r. (((exists ff_h_complement_left_last. ff_h_complement_left_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_complement_left_last. b = ff_q_complement_left_last * S ((S (l)) * c) + (a))) /\ ((((exists ff_u_complement_left_prefix_sum ff_v_complement_left_prefix_sum. ((((exists ff_h_complement_left_prefix_sum_start. ff_h_complement_left_prefix_sum_start + S (0) = S ((S (0)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_start. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_start * S ((S (0)) * ff_v_complement_left_prefix_sum) + (0))) /\ ((((exists ff_h_complement_left_prefix_sum_terminal. ff_h_complement_left_prefix_sum_terminal + S (r) = S ((S (l)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_terminal. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_terminal * S ((S (l)) * ff_v_complement_left_prefix_sum) + (r))) /\ forall ff_i_complement_left_prefix_sum. (exists ff_lt_complement_left_prefix_sum_bound. ff_lt_complement_left_prefix_sum_bound + S ff_i_complement_left_prefix_sum = l) -> exists ff_a_complement_left_prefix_sum ff_r_complement_left_prefix_sum ff_s_complement_left_prefix_sum. ((((exists ff_h_complement_left_prefix_sum_summand. ff_h_complement_left_prefix_sum_summand + S (ff_a_complement_left_prefix_sum) = S ((S (ff_i_complement_left_prefix_sum)) * c)) /\ exists ff_q_complement_left_prefix_sum_summand. b = ff_q_complement_left_prefix_sum_summand * S ((S (ff_i_complement_left_prefix_sum)) * c) + (ff_a_complement_left_prefix_sum))) /\ ((((exists ff_h_complement_left_prefix_sum_partial. ff_h_complement_left_prefix_sum_partial + S (ff_r_complement_left_prefix_sum) = S ((S (ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_partial. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_partial * S ((S (ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum) + (ff_r_complement_left_prefix_sum))) /\ ((((exists ff_h_complement_left_prefix_sum_successor. ff_h_complement_left_prefix_sum_successor + S (ff_s_complement_left_prefix_sum) = S ((S (S ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_successor. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_successor * S ((S (S ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum) + (ff_s_complement_left_prefix_sum))) /\ ff_s_complement_left_prefix_sum = ff_r_complement_left_prefix_sum + ff_a_complement_left_prefix_sum)))))) /\ (forall ff_i_complement_left_prefix_bits. (exists ff_lt_complement_left_prefix_bits_bound. ff_lt_complement_left_prefix_bits_bound + S ff_i_complement_left_prefix_bits = l) -> exists ff_bit_complement_left_prefix_bits. ((((exists ff_h_complement_left_prefix_bits_decoded. ff_h_complement_left_prefix_bits_decoded + S (ff_bit_complement_left_prefix_bits) = S ((S (ff_i_complement_left_prefix_bits)) * c)) /\ exists ff_q_complement_left_prefix_bits_decoded. b = ff_q_complement_left_prefix_bits_decoded * S ((S (ff_i_complement_left_prefix_bits)) * c) + (ff_bit_complement_left_prefix_bits))) /\ (ff_bit_complement_left_prefix_bits = 0 \/ ff_bit_complement_left_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  36. 0036specialize bit_count_succ_decompose b
  37. 0037specialize bit_count_succ_decompose c
  38. 0038specialize bit_count_succ_decompose l
  39. 0039specialize bit_count_succ_decompose (S l)
  40. 0040specialize bit_count_succ_decompose n
  41. 0041apply bit_count_succ_decompose
  42. 0042refl
  43. 0043exact hleft
  44. 0044cases hleft_decomp
  45. 0045cases hleft_decomp_witness
  46. 0046cases hleft_decomp_witness_witness
  47. 0047cases hleft_decomp_witness_witness_right
  48. 0048cases hleft_decomp_witness_witness_right_right
  49. 0049have hright_decomp : ∃ d. ∃ s. BetaAt(z,e,l,d) ∧ (BitCount(z,e,l,s) ∧ ((d = 0 ∨ d = 1) ∧ m = s + d))
    Exact native replay linehave hright_decomp : exists d s. (((exists ff_h_complement_right_last. ff_h_complement_right_last + S (d) = S ((S (l)) * e)) /\ exists ff_q_complement_right_last. z = ff_q_complement_right_last * S ((S (l)) * e) + (d))) /\ ((((exists ff_u_complement_right_prefix_sum ff_v_complement_right_prefix_sum. ((((exists ff_h_complement_right_prefix_sum_start. ff_h_complement_right_prefix_sum_start + S (0) = S ((S (0)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_start. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_start * S ((S (0)) * ff_v_complement_right_prefix_sum) + (0))) /\ ((((exists ff_h_complement_right_prefix_sum_terminal. ff_h_complement_right_prefix_sum_terminal + S (s) = S ((S (l)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_terminal. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_terminal * S ((S (l)) * ff_v_complement_right_prefix_sum) + (s))) /\ forall ff_i_complement_right_prefix_sum. (exists ff_lt_complement_right_prefix_sum_bound. ff_lt_complement_right_prefix_sum_bound + S ff_i_complement_right_prefix_sum = l) -> exists ff_a_complement_right_prefix_sum ff_r_complement_right_prefix_sum ff_s_complement_right_prefix_sum. ((((exists ff_h_complement_right_prefix_sum_summand. ff_h_complement_right_prefix_sum_summand + S (ff_a_complement_right_prefix_sum) = S ((S (ff_i_complement_right_prefix_sum)) * e)) /\ exists ff_q_complement_right_prefix_sum_summand. z = ff_q_complement_right_prefix_sum_summand * S ((S (ff_i_complement_right_prefix_sum)) * e) + (ff_a_complement_right_prefix_sum))) /\ ((((exists ff_h_complement_right_prefix_sum_partial. ff_h_complement_right_prefix_sum_partial + S (ff_r_complement_right_prefix_sum) = S ((S (ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_partial. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_partial * S ((S (ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum) + (ff_r_complement_right_prefix_sum))) /\ ((((exists ff_h_complement_right_prefix_sum_successor. ff_h_complement_right_prefix_sum_successor + S (ff_s_complement_right_prefix_sum) = S ((S (S ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_successor. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_successor * S ((S (S ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum) + (ff_s_complement_right_prefix_sum))) /\ ff_s_complement_right_prefix_sum = ff_r_complement_right_prefix_sum + ff_a_complement_right_prefix_sum)))))) /\ (forall ff_i_complement_right_prefix_bits. (exists ff_lt_complement_right_prefix_bits_bound. ff_lt_complement_right_prefix_bits_bound + S ff_i_complement_right_prefix_bits = l) -> exists ff_bit_complement_right_prefix_bits. ((((exists ff_h_complement_right_prefix_bits_decoded. ff_h_complement_right_prefix_bits_decoded + S (ff_bit_complement_right_prefix_bits) = S ((S (ff_i_complement_right_prefix_bits)) * e)) /\ exists ff_q_complement_right_prefix_bits_decoded. z = ff_q_complement_right_prefix_bits_decoded * S ((S (ff_i_complement_right_prefix_bits)) * e) + (ff_bit_complement_right_prefix_bits))) /\ (ff_bit_complement_right_prefix_bits = 0 \/ ff_bit_complement_right_prefix_bits = 1))))) /\ ((d = 0 \/ d = 1) /\ m = s + d))
  50. 0050specialize bit_count_succ_decompose z
  51. 0051specialize bit_count_succ_decompose e
  52. 0052specialize bit_count_succ_decompose l
  53. 0053specialize bit_count_succ_decompose (S l)
  54. 0054specialize bit_count_succ_decompose m
  55. 0055apply bit_count_succ_decompose
  56. 0056refl
  57. 0057exact hright
  58. 0058cases hright_decomp
  59. 0059cases hright_decomp_witness
  60. 0060cases hright_decomp_witness_witness
  61. 0061cases hright_decomp_witness_witness_right
  62. 0062cases hright_decomp_witness_witness_right_right
  63. 0063have hprefix_complement : ∀ i. ∀ a. ∀ d. Lt(i,l) → BetaAt(b,c,i,a) → BetaAt(z,e,i,d) → a = 0 ∧ d = 1 ∨ a = 1 ∧ d = 0
    Exact native replay linehave hprefix_complement : forall i a d. (exists h. h + S i = l) -> (((exists ff_h_complement_prefix_left. ff_h_complement_prefix_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_complement_prefix_left. b = ff_q_complement_prefix_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_complement_prefix_right. ff_h_complement_prefix_right + S (d) = S ((S (i)) * e)) /\ exists ff_q_complement_prefix_right. z = ff_q_complement_prefix_right * S ((S (i)) * e) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))
  64. 0064intro i
  65. 0065intro a
  66. 0066intro d
  67. 0067intro hi
  68. 0068intro ha
  69. 0069intro hd
  70. 0070specialize hcomplement i
  71. 0071specialize hcomplement a
  72. 0072specialize hcomplement d
  73. 0073apply hcomplement
  74. 0074specialize le_succ (S i)
  75. 0075specialize le_succ l
  76. 0076apply le_succ
  77. 0077exact hi
  78. 0078exact ha
  79. 0079exact hd
  80. 0080have hprefix : x1 + x3 = l
  81. 0081specialize IH x1
  82. 0082specialize IH x3
  83. 0083apply IH
  84. 0084exact hleft_decomp_witness_witness_right_left
  85. 0085exact hright_decomp_witness_witness_right_left
  86. 0086exact hprefix_complement
  87. 0087have hlast : ((x = 0 /\ x2 = 1) \/ (x = 1 /\ x2 = 0))
  88. 0088specialize hcomplement l
  89. 0089specialize hcomplement x
  90. 0090specialize hcomplement x2
  91. 0091apply hcomplement
  92. 0092specialize le_refl (S l)
  93. 0093exact le_refl
  94. 0094exact hleft_decomp_witness_witness_left
  95. 0095exact hright_decomp_witness_witness_left
  96. 0096rewrite hleft_decomp_witness_witness_right_right_right
  97. 0097rewrite hright_decomp_witness_witness_right_right_right
  98. 0098cases hlast
  99. 0099cases hlast_left
  100. 0100rewrite hlast_left_left
  101. 0101rewrite hlast_left_right
  102. 0102simp
  103. 0103cases hlast_right
  104. 0104rewrite hlast_right_left
  105. 0105rewrite hlast_right_right
  106. 0106simp
  107. 0107specialize add_succ_left x1
  108. 0108specialize add_succ_left x3
  109. 0109trans S (x1 + x3)
  110. 0110exact add_succ_left
  111. 0111rewrite hprefix
  112. 0112refl