choose_symmetry

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. 0001induction n
2. 0002induction k
3. 0003induction j
4. 0004intro x
5. 0005intro y
6. 0006intro hsum
7. 0007intro hleft
8. 0008intro hright
9. 0009have hx : x = 1
10. 0010specialize choose_zero 0
11. 0011specialize choose_zero x
12. 0012apply choose_zero
13. 0013exact hleft
14. 0014have hy : y = 1
15. 0015specialize choose_zero 0
16. 0016specialize choose_zero y
17. 0017apply choose_zero
18. 0018exact hright
19. 0019trans 1
20. 0020exact hx
21. 0021symm
22. 0022exact hy
23. 0023intro x
24. 0024intro y
25. 0025intro hsum
26. 0026intro hleft
27. 0027intro hright
28. 0028specialize zero_add (S j)
29. 0029rewrite zero_add at hsum
30. 0030exfalso
31. 0031apply PA1
32. 0032exact hsum
33. 0033intro j
34. 0034intro x
35. 0035intro y
36. 0036intro hsum
37. 0037intro hleft
38. 0038intro hright
39. 0039specialize add_succ_left k
40. 0040specialize add_succ_left j
41. 0041rewrite add_succ_left at hsum
42. 0042exfalso
43. 0043apply PA1
44. 0044exact hsum
45. 0045induction k
46. 0046intro j
47. 0047intro x
48. 0048intro y
49. 0049intro hsum
50. 0050intro hleft
51. 0051intro hright
52. 0052have hx : x = 1
53. 0053specialize choose_zero (S n)
54. 0054specialize choose_zero x
55. 0055apply choose_zero
56. 0056exact hleft
57. 0057have hj : j = S n
58. 0058trans 0 + j
59. 0059symm
60. 0060apply zero_add
61. 0061exact hsum
62. 0062have hy : y = 1
63. 0063specialize choose_self_of_eq (S n)
64. 0064specialize choose_self_of_eq j
65. 0065specialize choose_self_of_eq y
66. 0066apply choose_self_of_eq
67. 0067exact hj
68. 0068exact hright
69. 0069trans 1
70. 0070exact hx
71. 0071symm
72. 0072exact hy
73. 0073induction j
74. 0074intro x
75. 0075intro y
76. 0076intro hsum
77. 0077intro hleft
78. 0078intro hright
79. 0079have hk : S k = S n
80. 0080rewrite PA3 at hsum
81. 0081exact hsum
82. 0082have hx : x = 1
83. 0083specialize choose_self_of_eq (S n)
84. 0084specialize choose_self_of_eq (S k)
85. 0085specialize choose_self_of_eq x
86. 0086apply choose_self_of_eq
87. 0087exact hk
88. 0088exact hleft
89. 0089have hy : y = 1
90. 0090specialize choose_zero (S n)
91. 0091specialize choose_zero y
92. 0092apply choose_zero
93. 0093exact hright
94. 0094trans 1
95. 0095exact hx
96. 0096symm
97. 0097exact hy
98. 0098intro x
99. 0099intro y
100. 0100intro hsum
101. 0101intro hleft
102. 0102intro hright
103. 0103have ha_exists : exists a. (((exists bcf_lt_gap_bcs_previous_left_out_of_range. bcf_lt_gap_bcs_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcs_previous_left_in_range. bcf_le_gap_bcs_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcs_previous_left bcf_row_code_scale_bcs_previous_left bcf_row_scale_code_bcs_previous_left bcf_row_scale_scale_bcs_previous_left bcf_row_code_bcs_previous_left bcf_row_scale_bcs_previous_left. ((forall bcf_row_index_bcs_previous_left_table. (exists bcf_lt_gap_bcs_previous_left_table_row_bound. bcf_lt_gap_bcs_previous_left_table_row_bound + S (bcf_row_index_bcs_previous_left_table) = S (n)) -> exists bcf_row_code_bcs_previous_left_table bcf_row_scale_bcs_previous_left_table. ((((exists bcf_height_bcs_previous_left_table_decoded_row_code. bcf_height_bcs_previous_left_table_decoded_row_code + S (bcf_row_code_bcs_previous_left_table) = S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_row_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left) + (bcf_row_code_bcs_previous_left_table))) /\ ((((exists bcf_height_bcs_previous_left_table_decoded_row_scale. bcf_height_bcs_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcs_previous_left_table) = S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_row_scale_bcs_previous_left_table))) /\ ((bcf_row_index_bcs_previous_left_table = 0 /\ (forall bcf_index_bcs_previous_left_table_zero_row. (exists bcf_lt_gap_bcs_previous_left_table_zero_row_bound. bcf_lt_gap_bcs_previous_left_table_zero_row_bound + S (bcf_index_bcs_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcs_previous_left_table_zero_row. ((((exists bcf_height_bcs_previous_left_table_zero_row_entry. bcf_height_bcs_previous_left_table_zero_row_entry + S (bcf_value_bcs_previous_left_table_zero_row) = S ((S (bcf_index_bcs_previous_left_table_zero_row)) * bcf_row_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_zero_row_entry. bcf_row_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_zero_row_entry * S ((S (bcf_index_bcs_previous_left_table_zero_row)) * bcf_row_scale_bcs_previous_left_table) + (bcf_value_bcs_previous_left_table_zero_row))) /\ ((bcf_index_bcs_previous_left_table_zero_row = 0 /\ bcf_value_bcs_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcs_previous_left_table_zero_row. bcf_index_bcs_previous_left_table_zero_row = S bcf_predecessor_bcs_previous_left_table_zero_row /\ bcf_value_bcs_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_previous_left_table bcf_previous_code_bcs_previous_left_table bcf_previous_scale_bcs_previous_left_table. bcf_row_index_bcs_previous_left_table = S bcf_predecessor_bcs_previous_left_table /\ ((((exists bcf_height_bcs_previous_left_table_decoded_previous_code. bcf_height_bcs_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcs_previous_left_table) = S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_previous_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left) + (bcf_previous_code_bcs_previous_left_table))) /\ ((((exists bcf_height_bcs_previous_left_table_decoded_previous_scale. bcf_height_bcs_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcs_previous_left_table) = S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_previous_scale_bcs_previous_left_table))) /\ (forall bcf_index_bcs_previous_left_table_row_step. (exists bcf_lt_gap_bcs_previous_left_table_row_step_bound. bcf_lt_gap_bcs_previous_left_table_row_step_bound + S (bcf_index_bcs_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcs_previous_left_table_row_step. ((((exists bcf_height_bcs_previous_left_table_row_step_entry. bcf_height_bcs_previous_left_table_row_step_entry + S (bcf_value_bcs_previous_left_table_row_step) = S ((S (bcf_index_bcs_previous_left_table_row_step)) * bcf_row_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_entry. bcf_row_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_entry * S ((S (bcf_index_bcs_previous_left_table_row_step)) * bcf_row_scale_bcs_previous_left_table) + (bcf_value_bcs_previous_left_table_row_step))) /\ ((bcf_index_bcs_previous_left_table_row_step = 0 /\ bcf_value_bcs_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcs_previous_left_table_row_step bcf_left_bcs_previous_left_table_row_step bcf_right_bcs_previous_left_table_row_step. bcf_index_bcs_previous_left_table_row_step = S bcf_predecessor_bcs_previous_left_table_row_step /\ ((((exists bcf_height_bcs_previous_left_table_row_step_previous_left. bcf_height_bcs_previous_left_table_row_step_previous_left + S (bcf_left_bcs_previous_left_table_row_step) = S ((S (bcf_predecessor_bcs_previous_left_table_row_step)) * bcf_previous_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_previous_left. bcf_previous_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_previous_left_table_row_step)) * bcf_previous_scale_bcs_previous_left_table) + (bcf_left_bcs_previous_left_table_row_step))) /\ ((((exists bcf_height_bcs_previous_left_table_row_step_previous_right. bcf_height_bcs_previous_left_table_row_step_previous_right + S (bcf_right_bcs_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcs_previous_left_table_row_step))) * bcf_previous_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_previous_right. bcf_previous_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_previous_left_table_row_step))) * bcf_previous_scale_bcs_previous_left_table) + (bcf_right_bcs_previous_left_table_row_step))) /\ bcf_value_bcs_previous_left_table_row_step = bcf_left_bcs_previous_left_table_row_step + bcf_right_bcs_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_previous_left_decoded_row_code. bcf_height_bcs_previous_left_decoded_row_code + S (bcf_row_code_bcs_previous_left) = S ((S (n)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_row_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_previous_left) + (bcf_row_code_bcs_previous_left))) /\ ((((exists bcf_height_bcs_previous_left_decoded_row_scale. bcf_height_bcs_previous_left_decoded_row_scale + S (bcf_row_scale_bcs_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_row_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_row_scale_bcs_previous_left))) /\ (((exists bcf_height_bcs_previous_left_decoded_value. bcf_height_bcs_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_value. bcf_row_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcs_previous_left) + (a)))))))))
104. 0104specialize choose_exists n
105. 0105specialize choose_exists k
106. 0106exact choose_exists
107. 0107cases ha_exists
108. 0108have hb_exists : exists b. (((exists bcf_lt_gap_bcs_current_left_out_of_range. bcf_lt_gap_bcs_current_left_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcs_current_left_in_range. bcf_le_gap_bcs_current_left_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcs_current_left bcf_row_code_scale_bcs_current_left bcf_row_scale_code_bcs_current_left bcf_row_scale_scale_bcs_current_left bcf_row_code_bcs_current_left bcf_row_scale_bcs_current_left. ((forall bcf_row_index_bcs_current_left_table. (exists bcf_lt_gap_bcs_current_left_table_row_bound. bcf_lt_gap_bcs_current_left_table_row_bound + S (bcf_row_index_bcs_current_left_table) = S (n)) -> exists bcf_row_code_bcs_current_left_table bcf_row_scale_bcs_current_left_table. ((((exists bcf_height_bcs_current_left_table_decoded_row_code. bcf_height_bcs_current_left_table_decoded_row_code + S (bcf_row_code_bcs_current_left_table) = S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_row_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_row_code * S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left) + (bcf_row_code_bcs_current_left_table))) /\ ((((exists bcf_height_bcs_current_left_table_decoded_row_scale. bcf_height_bcs_current_left_table_decoded_row_scale + S (bcf_row_scale_bcs_current_left_table) = S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_row_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_row_scale * S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left) + (bcf_row_scale_bcs_current_left_table))) /\ ((bcf_row_index_bcs_current_left_table = 0 /\ (forall bcf_index_bcs_current_left_table_zero_row. (exists bcf_lt_gap_bcs_current_left_table_zero_row_bound. bcf_lt_gap_bcs_current_left_table_zero_row_bound + S (bcf_index_bcs_current_left_table_zero_row) = S (n)) -> exists bcf_value_bcs_current_left_table_zero_row. ((((exists bcf_height_bcs_current_left_table_zero_row_entry. bcf_height_bcs_current_left_table_zero_row_entry + S (bcf_value_bcs_current_left_table_zero_row) = S ((S (bcf_index_bcs_current_left_table_zero_row)) * bcf_row_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_zero_row_entry. bcf_row_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_zero_row_entry * S ((S (bcf_index_bcs_current_left_table_zero_row)) * bcf_row_scale_bcs_current_left_table) + (bcf_value_bcs_current_left_table_zero_row))) /\ ((bcf_index_bcs_current_left_table_zero_row = 0 /\ bcf_value_bcs_current_left_table_zero_row = 1) \/ exists bcf_predecessor_bcs_current_left_table_zero_row. bcf_index_bcs_current_left_table_zero_row = S bcf_predecessor_bcs_current_left_table_zero_row /\ bcf_value_bcs_current_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_current_left_table bcf_previous_code_bcs_current_left_table bcf_previous_scale_bcs_current_left_table. bcf_row_index_bcs_current_left_table = S bcf_predecessor_bcs_current_left_table /\ ((((exists bcf_height_bcs_current_left_table_decoded_previous_code. bcf_height_bcs_current_left_table_decoded_previous_code + S (bcf_previous_code_bcs_current_left_table) = S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_previous_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left) + (bcf_previous_code_bcs_current_left_table))) /\ ((((exists bcf_height_bcs_current_left_table_decoded_previous_scale. bcf_height_bcs_current_left_table_decoded_previous_scale + S (bcf_previous_scale_bcs_current_left_table) = S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_previous_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left) + (bcf_previous_scale_bcs_current_left_table))) /\ (forall bcf_index_bcs_current_left_table_row_step. (exists bcf_lt_gap_bcs_current_left_table_row_step_bound. bcf_lt_gap_bcs_current_left_table_row_step_bound + S (bcf_index_bcs_current_left_table_row_step) = S (n)) -> exists bcf_value_bcs_current_left_table_row_step. ((((exists bcf_height_bcs_current_left_table_row_step_entry. bcf_height_bcs_current_left_table_row_step_entry + S (bcf_value_bcs_current_left_table_row_step) = S ((S (bcf_index_bcs_current_left_table_row_step)) * bcf_row_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_entry. bcf_row_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_entry * S ((S (bcf_index_bcs_current_left_table_row_step)) * bcf_row_scale_bcs_current_left_table) + (bcf_value_bcs_current_left_table_row_step))) /\ ((bcf_index_bcs_current_left_table_row_step = 0 /\ bcf_value_bcs_current_left_table_row_step = 1) \/ exists bcf_predecessor_bcs_current_left_table_row_step bcf_left_bcs_current_left_table_row_step bcf_right_bcs_current_left_table_row_step. bcf_index_bcs_current_left_table_row_step = S bcf_predecessor_bcs_current_left_table_row_step /\ ((((exists bcf_height_bcs_current_left_table_row_step_previous_left. bcf_height_bcs_current_left_table_row_step_previous_left + S (bcf_left_bcs_current_left_table_row_step) = S ((S (bcf_predecessor_bcs_current_left_table_row_step)) * bcf_previous_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_previous_left. bcf_previous_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_current_left_table_row_step)) * bcf_previous_scale_bcs_current_left_table) + (bcf_left_bcs_current_left_table_row_step))) /\ ((((exists bcf_height_bcs_current_left_table_row_step_previous_right. bcf_height_bcs_current_left_table_row_step_previous_right + S (bcf_right_bcs_current_left_table_row_step) = S ((S (S (bcf_predecessor_bcs_current_left_table_row_step))) * bcf_previous_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_previous_right. bcf_previous_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_current_left_table_row_step))) * bcf_previous_scale_bcs_current_left_table) + (bcf_right_bcs_current_left_table_row_step))) /\ bcf_value_bcs_current_left_table_row_step = bcf_left_bcs_current_left_table_row_step + bcf_right_bcs_current_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_current_left_decoded_row_code. bcf_height_bcs_current_left_decoded_row_code + S (bcf_row_code_bcs_current_left) = S ((S (n)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_row_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_current_left) + (bcf_row_code_bcs_current_left))) /\ ((((exists bcf_height_bcs_current_left_decoded_row_scale. bcf_height_bcs_current_left_decoded_row_scale + S (bcf_row_scale_bcs_current_left) = S ((S (n)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_row_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_current_left) + (bcf_row_scale_bcs_current_left))) /\ (((exists bcf_height_bcs_current_left_decoded_value. bcf_height_bcs_current_left_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_value. bcf_row_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_value * S ((S (S k)) * bcf_row_scale_bcs_current_left) + (b)))))))))
109. 0109specialize choose_exists n
110. 0110specialize choose_exists (S k)
111. 0111exact choose_exists
112. 0112cases hb_exists
113. 0113have hc_exists : exists c. (((exists bcf_lt_gap_bcs_previous_right_out_of_range. bcf_lt_gap_bcs_previous_right_out_of_range + S (n) = j) /\ c = 0) \/ ((exists bcf_le_gap_bcs_previous_right_in_range. bcf_le_gap_bcs_previous_right_in_range + (j) = n) /\ (exists bcf_row_code_code_bcs_previous_right bcf_row_code_scale_bcs_previous_right bcf_row_scale_code_bcs_previous_right bcf_row_scale_scale_bcs_previous_right bcf_row_code_bcs_previous_right bcf_row_scale_bcs_previous_right. ((forall bcf_row_index_bcs_previous_right_table. (exists bcf_lt_gap_bcs_previous_right_table_row_bound. bcf_lt_gap_bcs_previous_right_table_row_bound + S (bcf_row_index_bcs_previous_right_table) = S (n)) -> exists bcf_row_code_bcs_previous_right_table bcf_row_scale_bcs_previous_right_table. ((((exists bcf_height_bcs_previous_right_table_decoded_row_code. bcf_height_bcs_previous_right_table_decoded_row_code + S (bcf_row_code_bcs_previous_right_table) = S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_row_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right) + (bcf_row_code_bcs_previous_right_table))) /\ ((((exists bcf_height_bcs_previous_right_table_decoded_row_scale. bcf_height_bcs_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcs_previous_right_table) = S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_row_scale_bcs_previous_right_table))) /\ ((bcf_row_index_bcs_previous_right_table = 0 /\ (forall bcf_index_bcs_previous_right_table_zero_row. (exists bcf_lt_gap_bcs_previous_right_table_zero_row_bound. bcf_lt_gap_bcs_previous_right_table_zero_row_bound + S (bcf_index_bcs_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcs_previous_right_table_zero_row. ((((exists bcf_height_bcs_previous_right_table_zero_row_entry. bcf_height_bcs_previous_right_table_zero_row_entry + S (bcf_value_bcs_previous_right_table_zero_row) = S ((S (bcf_index_bcs_previous_right_table_zero_row)) * bcf_row_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_zero_row_entry. bcf_row_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_zero_row_entry * S ((S (bcf_index_bcs_previous_right_table_zero_row)) * bcf_row_scale_bcs_previous_right_table) + (bcf_value_bcs_previous_right_table_zero_row))) /\ ((bcf_index_bcs_previous_right_table_zero_row = 0 /\ bcf_value_bcs_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcs_previous_right_table_zero_row. bcf_index_bcs_previous_right_table_zero_row = S bcf_predecessor_bcs_previous_right_table_zero_row /\ bcf_value_bcs_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_previous_right_table bcf_previous_code_bcs_previous_right_table bcf_previous_scale_bcs_previous_right_table. bcf_row_index_bcs_previous_right_table = S bcf_predecessor_bcs_previous_right_table /\ ((((exists bcf_height_bcs_previous_right_table_decoded_previous_code. bcf_height_bcs_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcs_previous_right_table) = S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_previous_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right) + (bcf_previous_code_bcs_previous_right_table))) /\ ((((exists bcf_height_bcs_previous_right_table_decoded_previous_scale. bcf_height_bcs_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcs_previous_right_table) = S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_previous_scale_bcs_previous_right_table))) /\ (forall bcf_index_bcs_previous_right_table_row_step. (exists bcf_lt_gap_bcs_previous_right_table_row_step_bound. bcf_lt_gap_bcs_previous_right_table_row_step_bound + S (bcf_index_bcs_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcs_previous_right_table_row_step. ((((exists bcf_height_bcs_previous_right_table_row_step_entry. bcf_height_bcs_previous_right_table_row_step_entry + S (bcf_value_bcs_previous_right_table_row_step) = S ((S (bcf_index_bcs_previous_right_table_row_step)) * bcf_row_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_entry. bcf_row_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_entry * S ((S (bcf_index_bcs_previous_right_table_row_step)) * bcf_row_scale_bcs_previous_right_table) + (bcf_value_bcs_previous_right_table_row_step))) /\ ((bcf_index_bcs_previous_right_table_row_step = 0 /\ bcf_value_bcs_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcs_previous_right_table_row_step bcf_left_bcs_previous_right_table_row_step bcf_right_bcs_previous_right_table_row_step. bcf_index_bcs_previous_right_table_row_step = S bcf_predecessor_bcs_previous_right_table_row_step /\ ((((exists bcf_height_bcs_previous_right_table_row_step_previous_left. bcf_height_bcs_previous_right_table_row_step_previous_left + S (bcf_left_bcs_previous_right_table_row_step) = S ((S (bcf_predecessor_bcs_previous_right_table_row_step)) * bcf_previous_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_previous_left. bcf_previous_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_previous_right_table_row_step)) * bcf_previous_scale_bcs_previous_right_table) + (bcf_left_bcs_previous_right_table_row_step))) /\ ((((exists bcf_height_bcs_previous_right_table_row_step_previous_right. bcf_height_bcs_previous_right_table_row_step_previous_right + S (bcf_right_bcs_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcs_previous_right_table_row_step))) * bcf_previous_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_previous_right. bcf_previous_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_previous_right_table_row_step))) * bcf_previous_scale_bcs_previous_right_table) + (bcf_right_bcs_previous_right_table_row_step))) /\ bcf_value_bcs_previous_right_table_row_step = bcf_left_bcs_previous_right_table_row_step + bcf_right_bcs_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_previous_right_decoded_row_code. bcf_height_bcs_previous_right_decoded_row_code + S (bcf_row_code_bcs_previous_right) = S ((S (n)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_row_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_previous_right) + (bcf_row_code_bcs_previous_right))) /\ ((((exists bcf_height_bcs_previous_right_decoded_row_scale. bcf_height_bcs_previous_right_decoded_row_scale + S (bcf_row_scale_bcs_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_row_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_row_scale_bcs_previous_right))) /\ (((exists bcf_height_bcs_previous_right_decoded_value. bcf_height_bcs_previous_right_decoded_value + S (c) = S ((S (j)) * bcf_row_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_value. bcf_row_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_value * S ((S (j)) * bcf_row_scale_bcs_previous_right) + (c)))))))))
114. 0114specialize choose_exists n
115. 0115specialize choose_exists j
116. 0116exact choose_exists
117. 0117cases hc_exists
118. 0118have hd_exists : exists d. (((exists bcf_lt_gap_bcs_current_right_out_of_range. bcf_lt_gap_bcs_current_right_out_of_range + S (n) = S j) /\ d = 0) \/ ((exists bcf_le_gap_bcs_current_right_in_range. bcf_le_gap_bcs_current_right_in_range + (S j) = n) /\ (exists bcf_row_code_code_bcs_current_right bcf_row_code_scale_bcs_current_right bcf_row_scale_code_bcs_current_right bcf_row_scale_scale_bcs_current_right bcf_row_code_bcs_current_right bcf_row_scale_bcs_current_right. ((forall bcf_row_index_bcs_current_right_table. (exists bcf_lt_gap_bcs_current_right_table_row_bound. bcf_lt_gap_bcs_current_right_table_row_bound + S (bcf_row_index_bcs_current_right_table) = S (n)) -> exists bcf_row_code_bcs_current_right_table bcf_row_scale_bcs_current_right_table. ((((exists bcf_height_bcs_current_right_table_decoded_row_code. bcf_height_bcs_current_right_table_decoded_row_code + S (bcf_row_code_bcs_current_right_table) = S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_row_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_row_code * S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right) + (bcf_row_code_bcs_current_right_table))) /\ ((((exists bcf_height_bcs_current_right_table_decoded_row_scale. bcf_height_bcs_current_right_table_decoded_row_scale + S (bcf_row_scale_bcs_current_right_table) = S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_row_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_row_scale * S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right) + (bcf_row_scale_bcs_current_right_table))) /\ ((bcf_row_index_bcs_current_right_table = 0 /\ (forall bcf_index_bcs_current_right_table_zero_row. (exists bcf_lt_gap_bcs_current_right_table_zero_row_bound. bcf_lt_gap_bcs_current_right_table_zero_row_bound + S (bcf_index_bcs_current_right_table_zero_row) = S (n)) -> exists bcf_value_bcs_current_right_table_zero_row. ((((exists bcf_height_bcs_current_right_table_zero_row_entry. bcf_height_bcs_current_right_table_zero_row_entry + S (bcf_value_bcs_current_right_table_zero_row) = S ((S (bcf_index_bcs_current_right_table_zero_row)) * bcf_row_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_zero_row_entry. bcf_row_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_zero_row_entry * S ((S (bcf_index_bcs_current_right_table_zero_row)) * bcf_row_scale_bcs_current_right_table) + (bcf_value_bcs_current_right_table_zero_row))) /\ ((bcf_index_bcs_current_right_table_zero_row = 0 /\ bcf_value_bcs_current_right_table_zero_row = 1) \/ exists bcf_predecessor_bcs_current_right_table_zero_row. bcf_index_bcs_current_right_table_zero_row = S bcf_predecessor_bcs_current_right_table_zero_row /\ bcf_value_bcs_current_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_current_right_table bcf_previous_code_bcs_current_right_table bcf_previous_scale_bcs_current_right_table. bcf_row_index_bcs_current_right_table = S bcf_predecessor_bcs_current_right_table /\ ((((exists bcf_height_bcs_current_right_table_decoded_previous_code. bcf_height_bcs_current_right_table_decoded_previous_code + S (bcf_previous_code_bcs_current_right_table) = S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_previous_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right) + (bcf_previous_code_bcs_current_right_table))) /\ ((((exists bcf_height_bcs_current_right_table_decoded_previous_scale. bcf_height_bcs_current_right_table_decoded_previous_scale + S (bcf_previous_scale_bcs_current_right_table) = S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_previous_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right) + (bcf_previous_scale_bcs_current_right_table))) /\ (forall bcf_index_bcs_current_right_table_row_step. (exists bcf_lt_gap_bcs_current_right_table_row_step_bound. bcf_lt_gap_bcs_current_right_table_row_step_bound + S (bcf_index_bcs_current_right_table_row_step) = S (n)) -> exists bcf_value_bcs_current_right_table_row_step. ((((exists bcf_height_bcs_current_right_table_row_step_entry. bcf_height_bcs_current_right_table_row_step_entry + S (bcf_value_bcs_current_right_table_row_step) = S ((S (bcf_index_bcs_current_right_table_row_step)) * bcf_row_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_entry. bcf_row_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_entry * S ((S (bcf_index_bcs_current_right_table_row_step)) * bcf_row_scale_bcs_current_right_table) + (bcf_value_bcs_current_right_table_row_step))) /\ ((bcf_index_bcs_current_right_table_row_step = 0 /\ bcf_value_bcs_current_right_table_row_step = 1) \/ exists bcf_predecessor_bcs_current_right_table_row_step bcf_left_bcs_current_right_table_row_step bcf_right_bcs_current_right_table_row_step. bcf_index_bcs_current_right_table_row_step = S bcf_predecessor_bcs_current_right_table_row_step /\ ((((exists bcf_height_bcs_current_right_table_row_step_previous_left. bcf_height_bcs_current_right_table_row_step_previous_left + S (bcf_left_bcs_current_right_table_row_step) = S ((S (bcf_predecessor_bcs_current_right_table_row_step)) * bcf_previous_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_previous_left. bcf_previous_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_current_right_table_row_step)) * bcf_previous_scale_bcs_current_right_table) + (bcf_left_bcs_current_right_table_row_step))) /\ ((((exists bcf_height_bcs_current_right_table_row_step_previous_right. bcf_height_bcs_current_right_table_row_step_previous_right + S (bcf_right_bcs_current_right_table_row_step) = S ((S (S (bcf_predecessor_bcs_current_right_table_row_step))) * bcf_previous_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_previous_right. bcf_previous_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_current_right_table_row_step))) * bcf_previous_scale_bcs_current_right_table) + (bcf_right_bcs_current_right_table_row_step))) /\ bcf_value_bcs_current_right_table_row_step = bcf_left_bcs_current_right_table_row_step + bcf_right_bcs_current_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_current_right_decoded_row_code. bcf_height_bcs_current_right_decoded_row_code + S (bcf_row_code_bcs_current_right) = S ((S (n)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_row_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_current_right) + (bcf_row_code_bcs_current_right))) /\ ((((exists bcf_height_bcs_current_right_decoded_row_scale. bcf_height_bcs_current_right_decoded_row_scale + S (bcf_row_scale_bcs_current_right) = S ((S (n)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_row_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_current_right) + (bcf_row_scale_bcs_current_right))) /\ (((exists bcf_height_bcs_current_right_decoded_value. bcf_height_bcs_current_right_decoded_value + S (d) = S ((S (S j)) * bcf_row_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_value. bcf_row_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_value * S ((S (S j)) * bcf_row_scale_bcs_current_right) + (d)))))))))
119. 0119specialize choose_exists n
120. 0120specialize choose_exists (S j)
121. 0121exact choose_exists
122. 0122cases hd_exists
123. 0123have hleft_complement : S k + j = n
124. 0124apply PA2
125. 0125trans S k + S j
126. 0126symm
127. 0127apply PA4
128. 0128exact hsum
129. 0129have hright_complement : k + S j = n
130. 0130trans S (k + j)
131. 0131apply PA4
132. 0132trans S k + j
133. 0133symm
134. 0134apply add_succ_left
135. 0135exact hleft_complement
136. 0136have hx_sum : x = x1 + x2
137. 0137specialize choose_succ_succ n
138. 0138specialize choose_succ_succ k
139. 0139specialize choose_succ_succ x1
140. 0140specialize choose_succ_succ x2
141. 0141specialize choose_succ_succ x
142. 0142apply choose_succ_succ
143. 0143exact ha_exists_witness
144. 0144exact hb_exists_witness
145. 0145exact hleft
146. 0146have hy_sum : y = x3 + x4
147. 0147specialize choose_succ_succ n
148. 0148specialize choose_succ_succ j
149. 0149specialize choose_succ_succ x3
150. 0150specialize choose_succ_succ x4
151. 0151specialize choose_succ_succ y
152. 0152apply choose_succ_succ
153. 0153exact hc_exists_witness
154. 0154exact hd_exists_witness
155. 0155exact hright
156. 0156have hfirst : x1 = x4
157. 0157specialize IH k
158. 0158specialize IH (S j)
159. 0159specialize IH x1
160. 0160specialize IH x4
161. 0161apply IH
162. 0162exact hright_complement
163. 0163exact ha_exists_witness
164. 0164exact hd_exists_witness
165. 0165have hsecond : x2 = x3
166. 0166specialize IH (S k)
167. 0167specialize IH j
168. 0168specialize IH x2
169. 0169specialize IH x3
170. 0170apply IH
171. 0171exact hleft_complement
172. 0172exact hb_exists_witness
173. 0173exact hc_exists_witness
174. 0174rewrite hx_sum
175. 0175rewrite hy_sum
176. 0176rewrite hfirst
177. 0177rewrite hsecond
178. 0178apply add_comm