beta_product_prefix_suffix_split

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 z
4. 0004intro d
5. 0005intro l
6. 0006induction m
7. 0007intro n
8. 0008intro hshift
9. 0009intro htotal
10. 0010specialize beta_product_exists z
11. 0011specialize beta_product_exists d
12. 0012specialize beta_product_exists 0
13. 0013cases beta_product_exists
14. 0014cases beta_product_exists_witness
15. 0015cases beta_product_exists_witness_witness
16. 0016have hqone : x = 1
17. 0017specialize beta_product_zero z
18. 0018specialize beta_product_zero d
19. 0019specialize beta_product_zero x
20. 0020apply beta_product_zero
21. 0021exists x1
22. 0022exists x2
23. 0023exact beta_product_exists_witness_witness_witness
24. 0024exists n
25. 0025exists x
26. 0026split
27. 0027have hbase : l + 0 = l
28. 0028apply PA3
29. 0029rewrite hbase at htotal
30. 0030rewrite hbase at htotal
31. 0031rewrite hbase at htotal
32. 0032exact htotal
33. 0033split
34. 0034exists x1
35. 0035exists x2
36. 0036exact beta_product_exists_witness_witness_witness
37. 0037rewrite hqone
38. 0038specialize mul_one n
39. 0039symm
40. 0040exact mul_one
41. 0041intro n
42. 0042intro hshift
43. 0043intro htotal
44. 0044have hlength : l + S m = S (l + m)
45. 0045apply PA4
46. 0046rewrite hlength at htotal
47. 0047rewrite hlength at htotal
48. 0048rewrite hlength at htotal
49. 0049have hdecomposition : exists a r. (((exists fps_height_bps_split_last. fps_height_bps_split_last + S (a) = S ((S (l + m)) * c)) /\ exists fps_quotient_bps_split_last. b = fps_quotient_bps_split_last * S ((S (l + m)) * c) + (a))) /\ ((exists fps_accumulator_bps_split_previous_total fps_scale_bps_split_previous_total. ((((exists fps_height_bps_split_previous_total_start. fps_height_bps_split_previous_total_start + S (1) = S ((S (0)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_start. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_start * S ((S (0)) * fps_scale_bps_split_previous_total) + (1))) /\ ((((exists fps_height_bps_split_previous_total_terminal. fps_height_bps_split_previous_total_terminal + S (r) = S ((S (l + m)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_terminal. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_terminal * S ((S (l + m)) * fps_scale_bps_split_previous_total) + (r))) /\ forall fps_index_bps_split_previous_total. (exists fps_gap_bps_split_previous_total_bound. fps_gap_bps_split_previous_total_bound + S fps_index_bps_split_previous_total = l + m) -> exists fps_factor_bps_split_previous_total fps_partial_bps_split_previous_total fps_successor_bps_split_previous_total. ((((exists fps_height_bps_split_previous_total_factor. fps_height_bps_split_previous_total_factor + S (fps_factor_bps_split_previous_total) = S ((S (fps_index_bps_split_previous_total)) * c)) /\ exists fps_quotient_bps_split_previous_total_factor. b = fps_quotient_bps_split_previous_total_factor * S ((S (fps_index_bps_split_previous_total)) * c) + (fps_factor_bps_split_previous_total))) /\ ((((exists fps_height_bps_split_previous_total_partial. fps_height_bps_split_previous_total_partial + S (fps_partial_bps_split_previous_total) = S ((S (fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_partial. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_partial * S ((S (fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total) + (fps_partial_bps_split_previous_total))) /\ ((((exists fps_height_bps_split_previous_total_successor. fps_height_bps_split_previous_total_successor + S (fps_successor_bps_split_previous_total) = S ((S (S fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_successor. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_successor * S ((S (S fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total) + (fps_successor_bps_split_previous_total))) /\ fps_successor_bps_split_previous_total = fps_partial_bps_split_previous_total * fps_factor_bps_split_previous_total)))))) /\ n = r * a)
50. 0050specialize beta_product_succ_decompose b
51. 0051specialize beta_product_succ_decompose c
52. 0052specialize beta_product_succ_decompose (l + m)
53. 0053specialize beta_product_succ_decompose n
54. 0054apply beta_product_succ_decompose
55. 0055exact htotal
56. 0056cases hdecomposition
57. 0057cases hdecomposition_witness
58. 0058cases hdecomposition_witness_witness
59. 0059cases hdecomposition_witness_witness_right
60. 0060have hprefix_shift : forall i a. (exists fps_bound_bps_split_previous_shift. fps_bound_bps_split_previous_shift + S i = m) -> (((exists fps_height_bps_split_previous_shift_source. fps_height_bps_split_previous_shift_source + S (a) = S ((S (l + i)) * c)) /\ exists fps_quotient_bps_split_previous_shift_source. b = fps_quotient_bps_split_previous_shift_source * S ((S (l + i)) * c) + (a))) -> (((exists fps_height_bps_split_previous_shift_suffix. fps_height_bps_split_previous_shift_suffix + S (a) = S ((S (i)) * d)) /\ exists fps_quotient_bps_split_previous_shift_suffix. z = fps_quotient_bps_split_previous_shift_suffix * S ((S (i)) * d) + (a)))
61. 0061intro i
62. 0062intro a
63. 0063intro hi
64. 0064intro ha
65. 0065specialize hshift i
66. 0066specialize hshift a
67. 0067apply hshift
68. 0068specialize le_succ (S i)
69. 0069specialize le_succ m
70. 0070apply le_succ
71. 0071exact hi
72. 0072exact ha
73. 0073have hrecursive : exists p q. (exists ff_u_bps_split_recursive_prefix ff_v_bps_split_recursive_prefix. ((((exists ff_h_bps_split_recursive_prefix_start. ff_h_bps_split_recursive_prefix_start + S (1) = S ((S (0)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_start. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_start * S ((S (0)) * ff_v_bps_split_recursive_prefix) + (1))) /\ ((((exists ff_h_bps_split_recursive_prefix_terminal. ff_h_bps_split_recursive_prefix_terminal + S (p) = S ((S (l)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_terminal. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_terminal * S ((S (l)) * ff_v_bps_split_recursive_prefix) + (p))) /\ forall ff_i_bps_split_recursive_prefix. (exists ff_lt_bps_split_recursive_prefix_bound. ff_lt_bps_split_recursive_prefix_bound + S ff_i_bps_split_recursive_prefix = l) -> exists ff_p_bps_split_recursive_prefix ff_r_bps_split_recursive_prefix ff_s_bps_split_recursive_prefix. ((((exists ff_h_bps_split_recursive_prefix_factor. ff_h_bps_split_recursive_prefix_factor + S (ff_p_bps_split_recursive_prefix) = S ((S (ff_i_bps_split_recursive_prefix)) * c)) /\ exists ff_q_bps_split_recursive_prefix_factor. b = ff_q_bps_split_recursive_prefix_factor * S ((S (ff_i_bps_split_recursive_prefix)) * c) + (ff_p_bps_split_recursive_prefix))) /\ ((((exists ff_h_bps_split_recursive_prefix_partial. ff_h_bps_split_recursive_prefix_partial + S (ff_r_bps_split_recursive_prefix) = S ((S (ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_partial. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_partial * S ((S (ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix) + (ff_r_bps_split_recursive_prefix))) /\ ((((exists ff_h_bps_split_recursive_prefix_successor. ff_h_bps_split_recursive_prefix_successor + S (ff_s_bps_split_recursive_prefix) = S ((S (S ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_successor. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_successor * S ((S (S ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix) + (ff_s_bps_split_recursive_prefix))) /\ ff_s_bps_split_recursive_prefix = ff_r_bps_split_recursive_prefix * ff_p_bps_split_recursive_prefix)))))) /\ ((exists ff_u_bps_split_recursive_suffix ff_v_bps_split_recursive_suffix. ((((exists ff_h_bps_split_recursive_suffix_start. ff_h_bps_split_recursive_suffix_start + S (1) = S ((S (0)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_start. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_start * S ((S (0)) * ff_v_bps_split_recursive_suffix) + (1))) /\ ((((exists ff_h_bps_split_recursive_suffix_terminal. ff_h_bps_split_recursive_suffix_terminal + S (q) = S ((S (m)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_terminal. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_terminal * S ((S (m)) * ff_v_bps_split_recursive_suffix) + (q))) /\ forall ff_i_bps_split_recursive_suffix. (exists ff_lt_bps_split_recursive_suffix_bound. ff_lt_bps_split_recursive_suffix_bound + S ff_i_bps_split_recursive_suffix = m) -> exists ff_p_bps_split_recursive_suffix ff_r_bps_split_recursive_suffix ff_s_bps_split_recursive_suffix. ((((exists ff_h_bps_split_recursive_suffix_factor. ff_h_bps_split_recursive_suffix_factor + S (ff_p_bps_split_recursive_suffix) = S ((S (ff_i_bps_split_recursive_suffix)) * d)) /\ exists ff_q_bps_split_recursive_suffix_factor. z = ff_q_bps_split_recursive_suffix_factor * S ((S (ff_i_bps_split_recursive_suffix)) * d) + (ff_p_bps_split_recursive_suffix))) /\ ((((exists ff_h_bps_split_recursive_suffix_partial. ff_h_bps_split_recursive_suffix_partial + S (ff_r_bps_split_recursive_suffix) = S ((S (ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_partial. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_partial * S ((S (ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix) + (ff_r_bps_split_recursive_suffix))) /\ ((((exists ff_h_bps_split_recursive_suffix_successor. ff_h_bps_split_recursive_suffix_successor + S (ff_s_bps_split_recursive_suffix) = S ((S (S ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_successor. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_successor * S ((S (S ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix) + (ff_s_bps_split_recursive_suffix))) /\ ff_s_bps_split_recursive_suffix = ff_r_bps_split_recursive_suffix * ff_p_bps_split_recursive_suffix)))))) /\ x1 = p * q)
74. 0074specialize IH x1
75. 0075apply IH
76. 0076exact hprefix_shift
77. 0077exact hdecomposition_witness_witness_right_left
78. 0078cases hrecursive
79. 0079cases hrecursive_witness
80. 0080cases hrecursive_witness_witness
81. 0081cases hrecursive_witness_witness_right
82. 0082have hsuffix_last : ((exists ff_h_bps_split_suffix_last. ff_h_bps_split_suffix_last + S (x) = S ((S (m)) * d)) /\ exists ff_q_bps_split_suffix_last. z = ff_q_bps_split_suffix_last * S ((S (m)) * d) + (x))
83. 0083specialize hshift m
84. 0084specialize hshift x
85. 0085apply hshift
86. 0086specialize le_refl (S m)
87. 0087exact le_refl
88. 0088exact hdecomposition_witness_witness_left
89. 0089exists x2
90. 0090exists x3 * x
91. 0091split
92. 0092exact hrecursive_witness_witness_left
93. 0093split
94. 0094specialize beta_product_succ_append z
95. 0095specialize beta_product_succ_append d
96. 0096specialize beta_product_succ_append m
97. 0097specialize beta_product_succ_append x3
98. 0098specialize beta_product_succ_append x
99. 0099apply beta_product_succ_append
100. 0100exact hrecursive_witness_witness_right_left
101. 0101exact hsuffix_last
102. 0102rewrite hdecomposition_witness_witness_right_right
103. 0103rewrite hrecursive_witness_witness_right_right
104. 0104specialize mul_assoc x2
105. 0105specialize mul_assoc x3
106. 0106specialize mul_assoc x
107. 0107exact mul_assoc