beta_sum_double_carry_exact

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

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 : 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 : 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 : 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 : 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 : 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]