beta_sum_pointwise_add

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001intro b
2. 0002intro c
3. 0003intro d
4. 0004intro e
5. 0005intro f
6. 0006intro g
7. 0007induction l
8. 0008intro n
9. 0009intro m
10. 0010intro q
11. 0011intro hleft
12. 0012intro hright
13. 0013intro htotal
14. 0014intro hpointwise
15. 0015have hn : n = 0
16. 0016specialize beta_sum_zero b
17. 0017specialize beta_sum_zero c
18. 0018specialize beta_sum_zero n
19. 0019apply beta_sum_zero
20. 0020exact hleft
21. 0021have hm : m = 0
22. 0022specialize beta_sum_zero d
23. 0023specialize beta_sum_zero e
24. 0024specialize beta_sum_zero m
25. 0025apply beta_sum_zero
26. 0026exact hright
27. 0027have hq : q = 0
28. 0028specialize beta_sum_zero f
29. 0029specialize beta_sum_zero g
30. 0030specialize beta_sum_zero q
31. 0031apply beta_sum_zero
32. 0032exact htotal
33. 0033rewrite hn
34. 0034rewrite hm
35. 0035rewrite hq
36. 0036simp
37. 0037intro n
38. 0038intro m
39. 0039intro q
40. 0040intro hleft
41. 0041intro hright
42. 0042intro htotal
43. 0043intro hpointwise
44. 0044have hleft_decomp : exists a r. (((exists ff_h_pointadd_left_decomp_entry. ff_h_pointadd_left_decomp_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_pointadd_left_decomp_entry. b = ff_q_pointadd_left_decomp_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_pointadd_left_decomp_prefix ff_v_pointadd_left_decomp_prefix. ((((exists ff_h_pointadd_left_decomp_prefix_start. ff_h_pointadd_left_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_start. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_left_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_terminal. ff_h_pointadd_left_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_terminal. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_left_decomp_prefix) + (r))) /\ forall ff_i_pointadd_left_decomp_prefix. (exists ff_lt_pointadd_left_decomp_prefix_bound. ff_lt_pointadd_left_decomp_prefix_bound + S ff_i_pointadd_left_decomp_prefix = l) -> exists ff_a_pointadd_left_decomp_prefix ff_r_pointadd_left_decomp_prefix ff_s_pointadd_left_decomp_prefix. ((((exists ff_h_pointadd_left_decomp_prefix_summand. ff_h_pointadd_left_decomp_prefix_summand + S (ff_a_pointadd_left_decomp_prefix) = S ((S (ff_i_pointadd_left_decomp_prefix)) * c)) /\ exists ff_q_pointadd_left_decomp_prefix_summand. b = ff_q_pointadd_left_decomp_prefix_summand * S ((S (ff_i_pointadd_left_decomp_prefix)) * c) + (ff_a_pointadd_left_decomp_prefix))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_partial. ff_h_pointadd_left_decomp_prefix_partial + S (ff_r_pointadd_left_decomp_prefix) = S ((S (ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_partial. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_partial * S ((S (ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix) + (ff_r_pointadd_left_decomp_prefix))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_successor. ff_h_pointadd_left_decomp_prefix_successor + S (ff_s_pointadd_left_decomp_prefix) = S ((S (S ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_successor. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_successor * S ((S (S ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix) + (ff_s_pointadd_left_decomp_prefix))) /\ ff_s_pointadd_left_decomp_prefix = ff_r_pointadd_left_decomp_prefix + ff_a_pointadd_left_decomp_prefix)))))) /\ n = r + a)
45. 0045specialize beta_sum_succ_decompose b
46. 0046specialize beta_sum_succ_decompose c
47. 0047specialize beta_sum_succ_decompose l
48. 0048specialize beta_sum_succ_decompose n
49. 0049apply beta_sum_succ_decompose
50. 0050exact hleft
51. 0051cases hleft_decomp
52. 0052cases hleft_decomp_witness
53. 0053cases hleft_decomp_witness_witness
54. 0054cases hleft_decomp_witness_witness_right
55. 0055have hright_decomp : exists a r. (((exists ff_h_pointadd_right_decomp_entry. ff_h_pointadd_right_decomp_entry + S (a) = S ((S (l)) * e)) /\ exists ff_q_pointadd_right_decomp_entry. d = ff_q_pointadd_right_decomp_entry * S ((S (l)) * e) + (a))) /\ ((exists ff_u_pointadd_right_decomp_prefix ff_v_pointadd_right_decomp_prefix. ((((exists ff_h_pointadd_right_decomp_prefix_start. ff_h_pointadd_right_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_start. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_right_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_terminal. ff_h_pointadd_right_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_terminal. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_right_decomp_prefix) + (r))) /\ forall ff_i_pointadd_right_decomp_prefix. (exists ff_lt_pointadd_right_decomp_prefix_bound. ff_lt_pointadd_right_decomp_prefix_bound + S ff_i_pointadd_right_decomp_prefix = l) -> exists ff_a_pointadd_right_decomp_prefix ff_r_pointadd_right_decomp_prefix ff_s_pointadd_right_decomp_prefix. ((((exists ff_h_pointadd_right_decomp_prefix_summand. ff_h_pointadd_right_decomp_prefix_summand + S (ff_a_pointadd_right_decomp_prefix) = S ((S (ff_i_pointadd_right_decomp_prefix)) * e)) /\ exists ff_q_pointadd_right_decomp_prefix_summand. d = ff_q_pointadd_right_decomp_prefix_summand * S ((S (ff_i_pointadd_right_decomp_prefix)) * e) + (ff_a_pointadd_right_decomp_prefix))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_partial. ff_h_pointadd_right_decomp_prefix_partial + S (ff_r_pointadd_right_decomp_prefix) = S ((S (ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_partial. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_partial * S ((S (ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix) + (ff_r_pointadd_right_decomp_prefix))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_successor. ff_h_pointadd_right_decomp_prefix_successor + S (ff_s_pointadd_right_decomp_prefix) = S ((S (S ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_successor. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_successor * S ((S (S ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix) + (ff_s_pointadd_right_decomp_prefix))) /\ ff_s_pointadd_right_decomp_prefix = ff_r_pointadd_right_decomp_prefix + ff_a_pointadd_right_decomp_prefix)))))) /\ m = r + a)
56. 0056specialize beta_sum_succ_decompose d
57. 0057specialize beta_sum_succ_decompose e
58. 0058specialize beta_sum_succ_decompose l
59. 0059specialize beta_sum_succ_decompose m
60. 0060apply beta_sum_succ_decompose
61. 0061exact hright
62. 0062cases hright_decomp
63. 0063cases hright_decomp_witness
64. 0064cases hright_decomp_witness_witness
65. 0065cases hright_decomp_witness_witness_right
66. 0066have htotal_decomp : exists a r. (((exists ff_h_pointadd_total_decomp_entry. ff_h_pointadd_total_decomp_entry + S (a) = S ((S (l)) * g)) /\ exists ff_q_pointadd_total_decomp_entry. f = ff_q_pointadd_total_decomp_entry * S ((S (l)) * g) + (a))) /\ ((exists ff_u_pointadd_total_decomp_prefix ff_v_pointadd_total_decomp_prefix. ((((exists ff_h_pointadd_total_decomp_prefix_start. ff_h_pointadd_total_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_start. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_total_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_terminal. ff_h_pointadd_total_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_terminal. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_total_decomp_prefix) + (r))) /\ forall ff_i_pointadd_total_decomp_prefix. (exists ff_lt_pointadd_total_decomp_prefix_bound. ff_lt_pointadd_total_decomp_prefix_bound + S ff_i_pointadd_total_decomp_prefix = l) -> exists ff_a_pointadd_total_decomp_prefix ff_r_pointadd_total_decomp_prefix ff_s_pointadd_total_decomp_prefix. ((((exists ff_h_pointadd_total_decomp_prefix_summand. ff_h_pointadd_total_decomp_prefix_summand + S (ff_a_pointadd_total_decomp_prefix) = S ((S (ff_i_pointadd_total_decomp_prefix)) * g)) /\ exists ff_q_pointadd_total_decomp_prefix_summand. f = ff_q_pointadd_total_decomp_prefix_summand * S ((S (ff_i_pointadd_total_decomp_prefix)) * g) + (ff_a_pointadd_total_decomp_prefix))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_partial. ff_h_pointadd_total_decomp_prefix_partial + S (ff_r_pointadd_total_decomp_prefix) = S ((S (ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_partial. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_partial * S ((S (ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix) + (ff_r_pointadd_total_decomp_prefix))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_successor. ff_h_pointadd_total_decomp_prefix_successor + S (ff_s_pointadd_total_decomp_prefix) = S ((S (S ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_successor. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_successor * S ((S (S ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix) + (ff_s_pointadd_total_decomp_prefix))) /\ ff_s_pointadd_total_decomp_prefix = ff_r_pointadd_total_decomp_prefix + ff_a_pointadd_total_decomp_prefix)))))) /\ q = r + a)
67. 0067specialize beta_sum_succ_decompose f
68. 0068specialize beta_sum_succ_decompose g
69. 0069specialize beta_sum_succ_decompose l
70. 0070specialize beta_sum_succ_decompose q
71. 0071apply beta_sum_succ_decompose
72. 0072exact htotal
73. 0073cases htotal_decomp
74. 0074cases htotal_decomp_witness
75. 0075cases htotal_decomp_witness_witness
76. 0076cases htotal_decomp_witness_witness_right
77. 0077have hprefix_pointwise : forall i a z s. (exists h. h + S i = l) -> (((exists ff_h_pointadd_prefix_left_entry. ff_h_pointadd_prefix_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pointadd_prefix_left_entry. b = ff_q_pointadd_prefix_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_pointadd_prefix_right_entry. ff_h_pointadd_prefix_right_entry + S (z) = S ((S (i)) * e)) /\ exists ff_q_pointadd_prefix_right_entry. d = ff_q_pointadd_prefix_right_entry * S ((S (i)) * e) + (z))) -> (((exists ff_h_pointadd_prefix_total_entry. ff_h_pointadd_prefix_total_entry + S (s) = S ((S (i)) * g)) /\ exists ff_q_pointadd_prefix_total_entry. f = ff_q_pointadd_prefix_total_entry * S ((S (i)) * g) + (s))) -> s = a + z
78. 0078intro i
79. 0079intro a
80. 0080intro z
81. 0081intro s
82. 0082intro hi
83. 0083intro ha
84. 0084intro hz
85. 0085intro hs
86. 0086specialize hpointwise i
87. 0087specialize hpointwise a
88. 0088specialize hpointwise z
89. 0089specialize hpointwise s
90. 0090apply hpointwise
91. 0091specialize le_succ (S i)
92. 0092specialize le_succ l
93. 0093apply le_succ
94. 0094exact hi
95. 0095exact ha
96. 0096exact hz
97. 0097exact hs
98. 0098have hprefix : x1 + x3 = x5
99. 0099specialize IH x1
100. 0100specialize IH x3
101. 0101specialize IH x5
102. 0102apply IH
103. 0103exact hleft_decomp_witness_witness_right_left
104. 0104exact hright_decomp_witness_witness_right_left
105. 0105exact htotal_decomp_witness_witness_right_left
106. 0106exact hprefix_pointwise
107. 0107have hlast : x4 = x + x2
108. 0108specialize hpointwise l
109. 0109specialize hpointwise x
110. 0110specialize hpointwise x2
111. 0111specialize hpointwise x4
112. 0112apply hpointwise
113. 0113specialize le_refl (S l)
114. 0114exact le_refl
115. 0115exact hleft_decomp_witness_witness_left
116. 0116exact hright_decomp_witness_witness_left
117. 0117exact htotal_decomp_witness_witness_left
118. 0118rewrite hleft_decomp_witness_witness_right_right
119. 0119rewrite hright_decomp_witness_witness_right_right
120. 0120rewrite htotal_decomp_witness_witness_right_right
121. 0121rewrite hlast
122. 0122simp [add_assoc, add_comm]
123. 0123trans (x1 + x3) + (x2 + x)
124. 0124symm
125. 0125apply add_assoc
126. 0126rewrite hprefix
127. 0127refl