beta_adjacent_target_pairs_product_power

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 p
2. 0002intro a
3. 0003intro b
4. 0004intro c
5. 0005induction m
6. 0006intro Q
7. 0007intro A
8. 0008intro hpairs
9. 0009intro hproduct
10. 0010intro hpower
11. 0011have hzero : 0 + 0 = 0
12. 0012simp
13. 0013rewrite hzero at hproduct
14. 0014rewrite hzero at hproduct
15. 0015rewrite hzero at hproduct
16. 0016have hQ : Q = 1
17. 0017specialize beta_product_zero b
18. 0018specialize beta_product_zero c
19. 0019specialize beta_product_zero Q
20. 0020apply beta_product_zero
21. 0021exact hproduct
22. 0022have hA : A = 1
23. 0023specialize pow_zero a
24. 0024specialize pow_zero 0
25. 0025specialize pow_zero A
26. 0026apply pow_zero
27. 0027refl
28. 0028exact hpower
29. 0029rewrite hQ
30. 0030rewrite hA
31. 0031specialize mod_eq_refl p
32. 0032specialize mod_eq_refl 1
33. 0033exact mod_eq_refl
34. 0034intro Q
35. 0035intro A
36. 0036intro hpairs
37. 0037intro hproduct
38. 0038intro hpower
39. 0039have hdouble : S m + S m = S (S (m + m))
40. 0040simp [add_succ_left]
41. 0041have hdecomposition : exists wpp_left_factor_target_successor_decomposition wpp_right_factor_target_successor_decomposition wpp_prefix_product_target_successor_decomposition. (((exists wpp_beta_height_target_successor_decomposition_left_entry. wpp_beta_height_target_successor_decomposition_left_entry + S (wpp_left_factor_target_successor_decomposition) = S ((S (m + m)) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_left_entry. b = wpp_beta_quotient_target_successor_decomposition_left_entry * S ((S (m + m)) * c) + (wpp_left_factor_target_successor_decomposition))) /\ ((((exists wpp_beta_height_target_successor_decomposition_right_entry. wpp_beta_height_target_successor_decomposition_right_entry + S (wpp_right_factor_target_successor_decomposition) = S ((S (S (m + m))) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_right_entry. b = wpp_beta_quotient_target_successor_decomposition_right_entry * S ((S (S (m + m))) * c) + (wpp_right_factor_target_successor_decomposition))) /\ ((exists wpp_trace_code_target_successor_decomposition_prefix wpp_trace_scale_target_successor_decomposition_prefix. ((((exists wpp_beta_height_target_successor_decomposition_prefix_start. wpp_beta_height_target_successor_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_start. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_target_successor_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_terminal. wpp_beta_height_target_successor_decomposition_prefix_terminal + S (wpp_prefix_product_target_successor_decomposition) = S ((S (m + m)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_terminal. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_terminal * S ((S (m + m)) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_prefix_product_target_successor_decomposition))) /\ forall wpp_index_target_successor_decomposition_prefix. (exists wpp_gap_target_successor_decomposition_prefix_bound. wpp_gap_target_successor_decomposition_prefix_bound + S (wpp_index_target_successor_decomposition_prefix) = m + m) -> exists wpp_factor_target_successor_decomposition_prefix wpp_prefix_target_successor_decomposition_prefix wpp_successor_target_successor_decomposition_prefix. ((((exists wpp_beta_height_target_successor_decomposition_prefix_factor. wpp_beta_height_target_successor_decomposition_prefix_factor + S (wpp_factor_target_successor_decomposition_prefix) = S ((S (wpp_index_target_successor_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_factor. b = wpp_beta_quotient_target_successor_decomposition_prefix_factor * S ((S (wpp_index_target_successor_decomposition_prefix)) * c) + (wpp_factor_target_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_prefix. wpp_beta_height_target_successor_decomposition_prefix_prefix + S (wpp_prefix_target_successor_decomposition_prefix) = S ((S (wpp_index_target_successor_decomposition_prefix)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_prefix. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_prefix * S ((S (wpp_index_target_successor_decomposition_prefix)) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_prefix_target_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_successor. wpp_beta_height_target_successor_decomposition_prefix_successor + S (wpp_successor_target_successor_decomposition_prefix) = S ((S (S (wpp_index_target_successor_decomposition_prefix))) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_successor. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_successor * S ((S (S (wpp_index_target_successor_decomposition_prefix))) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_successor_target_successor_decomposition_prefix))) /\ wpp_successor_target_successor_decomposition_prefix = wpp_prefix_target_successor_decomposition_prefix * wpp_factor_target_successor_decomposition_prefix)))))) /\ Q = (wpp_prefix_product_target_successor_decomposition * wpp_left_factor_target_successor_decomposition) * wpp_right_factor_target_successor_decomposition))
42. 0042specialize beta_product_double_succ_decompose b
43. 0043specialize beta_product_double_succ_decompose c
44. 0044specialize beta_product_double_succ_decompose (m + m)
45. 0045specialize beta_product_double_succ_decompose (S m + S m)
46. 0046specialize beta_product_double_succ_decompose Q
47. 0047apply beta_product_double_succ_decompose
48. 0048exact hdouble
49. 0049exact hproduct
50. 0050cases hdecomposition
51. 0051cases hdecomposition_witness
52. 0052cases hdecomposition_witness_witness
53. 0053cases hdecomposition_witness_witness_witness
54. 0054cases hdecomposition_witness_witness_witness_right
55. 0055cases hdecomposition_witness_witness_witness_right_right
56. 0056have hpairs_all : forall wpp_pair_target_all_successor_pairs wpp_left_target_all_successor_pairs wpp_right_target_all_successor_pairs. (exists wpp_gap_target_all_successor_pairs_pair_bound. wpp_gap_target_all_successor_pairs_pair_bound + S (wpp_pair_target_all_successor_pairs) = S m) -> (((exists wpp_beta_height_target_all_successor_pairs_left_entry. wpp_beta_height_target_all_successor_pairs_left_entry + S (wpp_left_target_all_successor_pairs) = S ((S ((wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_target_all_successor_pairs_left_entry. b = wpp_beta_quotient_target_all_successor_pairs_left_entry * S ((S ((wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c) + (wpp_left_target_all_successor_pairs))) -> (((exists wpp_beta_height_target_all_successor_pairs_right_entry. wpp_beta_height_target_all_successor_pairs_right_entry + S (wpp_right_target_all_successor_pairs) = S ((S (S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_target_all_successor_pairs_right_entry. b = wpp_beta_quotient_target_all_successor_pairs_right_entry * S ((S (S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c) + (wpp_right_target_all_successor_pairs))) -> (exists wpp_mod_left_target_all_successor_pairs_pair_mod wpp_mod_right_target_all_successor_pairs_pair_mod. (wpp_left_target_all_successor_pairs * wpp_right_target_all_successor_pairs) + p * wpp_mod_left_target_all_successor_pairs_pair_mod = (a) + p * wpp_mod_right_target_all_successor_pairs_pair_mod)
57. 0057exact hpairs
58. 0058have hpairs_prefix : forall wpp_pair_target_prefix_pairs wpp_left_target_prefix_pairs wpp_right_target_prefix_pairs. (exists wpp_gap_target_prefix_pairs_pair_bound. wpp_gap_target_prefix_pairs_pair_bound + S (wpp_pair_target_prefix_pairs) = m) -> (((exists wpp_beta_height_target_prefix_pairs_left_entry. wpp_beta_height_target_prefix_pairs_left_entry + S (wpp_left_target_prefix_pairs) = S ((S ((wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_target_prefix_pairs_left_entry. b = wpp_beta_quotient_target_prefix_pairs_left_entry * S ((S ((wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c) + (wpp_left_target_prefix_pairs))) -> (((exists wpp_beta_height_target_prefix_pairs_right_entry. wpp_beta_height_target_prefix_pairs_right_entry + S (wpp_right_target_prefix_pairs) = S ((S (S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_target_prefix_pairs_right_entry. b = wpp_beta_quotient_target_prefix_pairs_right_entry * S ((S (S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c) + (wpp_right_target_prefix_pairs))) -> (exists wpp_mod_left_target_prefix_pairs_pair_mod wpp_mod_right_target_prefix_pairs_pair_mod. (wpp_left_target_prefix_pairs * wpp_right_target_prefix_pairs) + p * wpp_mod_left_target_prefix_pairs_pair_mod = (a) + p * wpp_mod_right_target_prefix_pairs_pair_mod)
59. 0059intro t
60. 0060intro u
61. 0061intro v
62. 0062intro ht
63. 0063intro hu
64. 0064intro hv
65. 0065specialize hpairs_all t
66. 0066specialize hpairs_all u
67. 0067specialize hpairs_all v
68. 0068apply hpairs_all
69. 0069specialize le_succ (S t)
70. 0070specialize le_succ m
71. 0071apply le_succ
72. 0072exact ht
73. 0073exact hu
74. 0074exact hv
75. 0075have hpower_step : exists r. (exists ff_b_target_predecessor_power ff_c_target_predecessor_power. ((forall ff_i_target_predecessor_power_repeat. (exists ff_lt_target_predecessor_power_repeat_bound. ff_lt_target_predecessor_power_repeat_bound + S ff_i_target_predecessor_power_repeat = m) -> (((exists ff_h_target_predecessor_power_repeat_decoded. ff_h_target_predecessor_power_repeat_decoded + S (a) = S ((S (ff_i_target_predecessor_power_repeat)) * ff_c_target_predecessor_power)) /\ exists ff_q_target_predecessor_power_repeat_decoded. ff_b_target_predecessor_power = ff_q_target_predecessor_power_repeat_decoded * S ((S (ff_i_target_predecessor_power_repeat)) * ff_c_target_predecessor_power) + (a)))) /\ (exists ff_u_target_predecessor_power_product ff_v_target_predecessor_power_product. ((((exists ff_h_target_predecessor_power_product_start. ff_h_target_predecessor_power_product_start + S (1) = S ((S (0)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_start. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_start * S ((S (0)) * ff_v_target_predecessor_power_product) + (1))) /\ ((((exists ff_h_target_predecessor_power_product_terminal. ff_h_target_predecessor_power_product_terminal + S (r) = S ((S (m)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_terminal. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_terminal * S ((S (m)) * ff_v_target_predecessor_power_product) + (r))) /\ forall ff_i_target_predecessor_power_product. (exists ff_lt_target_predecessor_power_product_bound. ff_lt_target_predecessor_power_product_bound + S ff_i_target_predecessor_power_product = m) -> exists ff_p_target_predecessor_power_product ff_r_target_predecessor_power_product ff_s_target_predecessor_power_product. ((((exists ff_h_target_predecessor_power_product_factor. ff_h_target_predecessor_power_product_factor + S (ff_p_target_predecessor_power_product) = S ((S (ff_i_target_predecessor_power_product)) * ff_c_target_predecessor_power)) /\ exists ff_q_target_predecessor_power_product_factor. ff_b_target_predecessor_power = ff_q_target_predecessor_power_product_factor * S ((S (ff_i_target_predecessor_power_product)) * ff_c_target_predecessor_power) + (ff_p_target_predecessor_power_product))) /\ ((((exists ff_h_target_predecessor_power_product_partial. ff_h_target_predecessor_power_product_partial + S (ff_r_target_predecessor_power_product) = S ((S (ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_partial. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_partial * S ((S (ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product) + (ff_r_target_predecessor_power_product))) /\ ((((exists ff_h_target_predecessor_power_product_successor. ff_h_target_predecessor_power_product_successor + S (ff_s_target_predecessor_power_product) = S ((S (S ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_successor. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_successor * S ((S (S ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product) + (ff_s_target_predecessor_power_product))) /\ ff_s_target_predecessor_power_product = ff_r_target_predecessor_power_product * ff_p_target_predecessor_power_product)))))))) /\ A = r * a
76. 0076specialize pow_successor_decompose a
77. 0077specialize pow_successor_decompose m
78. 0078specialize pow_successor_decompose (S m)
79. 0079specialize pow_successor_decompose A
80. 0080apply pow_successor_decompose
81. 0081refl
82. 0082exact hpower
83. 0083cases hpower_step
84. 0084cases hpower_step_witness
85. 0085have hprefix : exists wpp_mod_left_target_prefix_congruence wpp_mod_right_target_prefix_congruence. (x2) + p * wpp_mod_left_target_prefix_congruence = (x3) + p * wpp_mod_right_target_prefix_congruence
86. 0086specialize IH x2
87. 0087specialize IH x3
88. 0088apply IH
89. 0089exact hpairs_prefix
90. 0090exact hdecomposition_witness_witness_witness_right_right_left
91. 0091exact hpower_step_witness_left
92. 0092have hlast : exists wpp_mod_left_target_last_pair_congruence wpp_mod_right_target_last_pair_congruence. (x * x1) + p * wpp_mod_left_target_last_pair_congruence = (a) + p * wpp_mod_right_target_last_pair_congruence
93. 0093specialize hpairs m
94. 0094specialize hpairs x
95. 0095specialize hpairs x1
96. 0096apply hpairs
97. 0097specialize le_refl (S m)
98. 0098exact le_refl
99. 0099exact hdecomposition_witness_witness_witness_left
100. 0100exact hdecomposition_witness_witness_witness_right_left
101. 0101have hfold : exists wpp_mod_left_target_folded_congruence wpp_mod_right_target_folded_congruence. (x2 * (x * x1)) + p * wpp_mod_left_target_folded_congruence = (x3 * a) + p * wpp_mod_right_target_folded_congruence
102. 0102specialize mod_eq_mul p
103. 0103specialize mod_eq_mul x2
104. 0104specialize mod_eq_mul x3
105. 0105specialize mod_eq_mul (x * x1)
106. 0106specialize mod_eq_mul a
107. 0107apply mod_eq_mul
108. 0108exact hprefix
109. 0109exact hlast
110. 0110have hassoc : (x2 * x) * x1 = x2 * (x * x1)
111. 0111specialize mul_assoc x2
112. 0112specialize mul_assoc x
113. 0113specialize mul_assoc x1
114. 0114exact mul_assoc
115. 0115rewrite hdecomposition_witness_witness_witness_right_right_right
116. 0116rewrite hassoc
117. 0117rewrite hpower_step_witness_right
118. 0118exact hfold