beta_prefix_append_two_injective

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 z
4. 0004intro d
5. 0005intro l
6. 0006intro a
7. 0007intro e
8. 0008intro htrace
9. 0009intro hold_injective
10. 0010intro hfirst_omit
11. 0011intro hsecond_omit
12. 0012intro hdistinct
13. 0013have hright_reflect_theorem : forall b c z d l a e. (((((exists wpo_beta_height_reflect_trace_first. wpo_beta_height_reflect_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_reflect_trace_first. z = wpo_beta_quotient_reflect_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_reflect_trace_second. wpo_beta_height_reflect_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_reflect_trace_second. z = wpo_beta_quotient_reflect_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_reflect_trace wpo_old_value_reflect_trace. (exists wpo_gap_reflect_trace_old_bound. wpo_gap_reflect_trace_old_bound + S (wpo_old_index_reflect_trace) = l) -> (((exists wpo_beta_height_reflect_trace_old_entry. wpo_beta_height_reflect_trace_old_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * c)) /\ exists wpo_beta_quotient_reflect_trace_old_entry. b = wpo_beta_quotient_reflect_trace_old_entry * S ((S (wpo_old_index_reflect_trace)) * c) + (wpo_old_value_reflect_trace))) -> (((exists wpo_beta_height_reflect_trace_new_entry. wpo_beta_height_reflect_trace_new_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * d)) /\ exists wpo_beta_quotient_reflect_trace_new_entry. z = wpo_beta_quotient_reflect_trace_new_entry * S ((S (wpo_old_index_reflect_trace)) * d) + (wpo_old_value_reflect_trace))))))) -> forall i v. (exists wpo_gap_reflect_new_bound. wpo_gap_reflect_new_bound + S (i) = S (S l)) -> (((exists wpo_beta_height_reflect_new_entry. wpo_beta_height_reflect_new_entry + S (v) = S ((S (i)) * d)) /\ exists wpo_beta_quotient_reflect_new_entry. z = wpo_beta_quotient_reflect_new_entry * S ((S (i)) * d) + (v))) -> (((i = S (l) /\ v = e) \/ ((i = l /\ v = a) \/ ((exists wpo_gap_reflect_result_old_bound. wpo_gap_reflect_result_old_bound + S (i) = l) /\ (((exists wpo_beta_height_reflect_result_old_entry. wpo_beta_height_reflect_result_old_entry + S (v) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_result_old_entry. b = wpo_beta_quotient_reflect_result_old_entry * S ((S (i)) * c) + (v)))))))
14. 0014exact beta_prefix_append_two_reflect
15. 0015intro q
16. 0016intro r
17. 0017intro w
18. 0018intro hq
19. 0019intro hr
20. 0020intro hleft_entry
21. 0021intro hright_entry
22. 0022have hleft_all : forall q w. (exists wpo_gap_injective_left_bound. wpo_gap_injective_left_bound + S (q) = S (S l)) -> (((exists wpo_beta_height_injective_left_entry. wpo_beta_height_injective_left_entry + S (w) = S ((S (q)) * d)) /\ exists wpo_beta_quotient_injective_left_entry. z = wpo_beta_quotient_injective_left_entry * S ((S (q)) * d) + (w))) -> (((q = S (l) /\ w = e) \/ ((q = l /\ w = a) \/ ((exists wpo_gap_injective_left_reflection_old_bound. wpo_gap_injective_left_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_injective_left_reflection_old_entry. wpo_beta_height_injective_left_reflection_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_injective_left_reflection_old_entry. b = wpo_beta_quotient_injective_left_reflection_old_entry * S ((S (q)) * c) + (w)))))))
23. 0023specialize beta_prefix_append_two_reflect b
24. 0024specialize beta_prefix_append_two_reflect c
25. 0025specialize beta_prefix_append_two_reflect z
26. 0026specialize beta_prefix_append_two_reflect d
27. 0027specialize beta_prefix_append_two_reflect l
28. 0028specialize beta_prefix_append_two_reflect a
29. 0029specialize beta_prefix_append_two_reflect e
30. 0030apply beta_prefix_append_two_reflect
31. 0031exact htrace
32. 0032have hright_all : forall r w. (exists wpo_gap_injective_right_bound. wpo_gap_injective_right_bound + S (r) = S (S l)) -> (((exists wpo_beta_height_injective_right_entry. wpo_beta_height_injective_right_entry + S (w) = S ((S (r)) * d)) /\ exists wpo_beta_quotient_injective_right_entry. z = wpo_beta_quotient_injective_right_entry * S ((S (r)) * d) + (w))) -> (((r = S (l) /\ w = e) \/ ((r = l /\ w = a) \/ ((exists wpo_gap_injective_right_reflection_old_bound. wpo_gap_injective_right_reflection_old_bound + S (r) = l) /\ (((exists wpo_beta_height_injective_right_reflection_old_entry. wpo_beta_height_injective_right_reflection_old_entry + S (w) = S ((S (r)) * c)) /\ exists wpo_beta_quotient_injective_right_reflection_old_entry. b = wpo_beta_quotient_injective_right_reflection_old_entry * S ((S (r)) * c) + (w)))))))
33. 0033specialize hright_reflect_theorem b
34. 0034specialize hright_reflect_theorem c
35. 0035specialize hright_reflect_theorem z
36. 0036specialize hright_reflect_theorem d
37. 0037specialize hright_reflect_theorem l
38. 0038specialize hright_reflect_theorem a
39. 0039specialize hright_reflect_theorem e
40. 0040apply hright_reflect_theorem
41. 0041exact htrace
42. 0042have hleft_class : ((q = S (l) /\ w = e) \/ ((q = l /\ w = a) \/ ((exists wpo_gap_injective_left_reflection_old_bound. wpo_gap_injective_left_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_injective_left_reflection_old_entry. wpo_beta_height_injective_left_reflection_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_injective_left_reflection_old_entry. b = wpo_beta_quotient_injective_left_reflection_old_entry * S ((S (q)) * c) + (w))))))
43. 0043specialize hleft_all q
44. 0044specialize hleft_all w
45. 0045apply hleft_all
46. 0046exact hq
47. 0047exact hleft_entry
48. 0048have hright_class : ((r = S (l) /\ w = e) \/ ((r = l /\ w = a) \/ ((exists wpo_gap_injective_right_reflection_old_bound. wpo_gap_injective_right_reflection_old_bound + S (r) = l) /\ (((exists wpo_beta_height_injective_right_reflection_old_entry. wpo_beta_height_injective_right_reflection_old_entry + S (w) = S ((S (r)) * c)) /\ exists wpo_beta_quotient_injective_right_reflection_old_entry. b = wpo_beta_quotient_injective_right_reflection_old_entry * S ((S (r)) * c) + (w))))))
49. 0049specialize hright_all r
50. 0050specialize hright_all w
51. 0051apply hright_all
52. 0052exact hr
53. 0053exact hright_entry
54. 0054cases hleft_class
55. 0055cases hleft_class_left
56. 0056cases hright_class
57. 0057cases hright_class_left
58. 0058trans (S l)
59. 0059exact hleft_class_left_left
60. 0060symm
61. 0061exact hright_class_left_left
62. 0062cases hright_class_right
63. 0063cases hright_class_right_left
64. 0064exfalso
65. 0065apply hdistinct
66. 0066trans w
67. 0067symm
68. 0068exact hright_class_right_left_right
69. 0069exact hleft_class_left_right
70. 0070cases hright_class_right_right
71. 0071exfalso
72. 0072apply hsecond_omit
73. 0073exists r
74. 0074split
75. 0075exact hright_class_right_right_left
76. 0076rewrite hleft_class_left_right at hright_class_right_right_right
77. 0077rewrite hleft_class_left_right at hright_class_right_right_right
78. 0078exact hright_class_right_right_right
79. 0079cases hleft_class_right
80. 0080cases hleft_class_right_left
81. 0081cases hright_class
82. 0082cases hright_class_left
83. 0083exfalso
84. 0084apply hdistinct
85. 0085trans w
86. 0086symm
87. 0087exact hleft_class_right_left_right
88. 0088exact hright_class_left_right
89. 0089cases hright_class_right
90. 0090cases hright_class_right_left
91. 0091trans l
92. 0092exact hleft_class_right_left_left
93. 0093symm
94. 0094exact hright_class_right_left_left
95. 0095cases hright_class_right_right
96. 0096exfalso
97. 0097apply hfirst_omit
98. 0098exists r
99. 0099split
100. 0100exact hright_class_right_right_left
101. 0101rewrite hleft_class_right_left_right at hright_class_right_right_right
102. 0102rewrite hleft_class_right_left_right at hright_class_right_right_right
103. 0103exact hright_class_right_right_right
104. 0104cases hleft_class_right_right
105. 0105cases hright_class
106. 0106cases hright_class_left
107. 0107exfalso
108. 0108apply hsecond_omit
109. 0109exists q
110. 0110split
111. 0111exact hleft_class_right_right_left
112. 0112rewrite hright_class_left_right at hleft_class_right_right_right
113. 0113rewrite hright_class_left_right at hleft_class_right_right_right
114. 0114exact hleft_class_right_right_right
115. 0115cases hright_class_right
116. 0116cases hright_class_right_left
117. 0117exfalso
118. 0118apply hfirst_omit
119. 0119exists q
120. 0120split
121. 0121exact hleft_class_right_right_left
122. 0122rewrite hright_class_right_left_right at hleft_class_right_right_right
123. 0123rewrite hright_class_right_left_right at hleft_class_right_right_right
124. 0124exact hleft_class_right_right_right
125. 0125cases hright_class_right_right
126. 0126specialize hold_injective q
127. 0127specialize hold_injective r
128. 0128specialize hold_injective w
129. 0129apply hold_injective
130. 0130exact hleft_class_right_right_left
131. 0131exact hright_class_right_right_left
132. 0132exact hleft_class_right_right_right
133. 0133exact hright_class_right_right_right