pow_three_five_le_pow_four_four_from_total

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 x
2. 0002intro y
3. 0003intro htotal
4. 0004intro hx
5. 0005intro hy
6. 0006have hthree_zero_any : exists q. (exists pa_b_hj32_three_zero_any pa_c_hj32_three_zero_any. ((forall pa_i_hj32_three_zero_any_repeat. (exists pa_lt_hj32_three_zero_any_repeat_bound. pa_lt_hj32_three_zero_any_repeat_bound + S pa_i_hj32_three_zero_any_repeat = 0) -> (((exists pa_h_hj32_three_zero_any_repeat_decoded. pa_h_hj32_three_zero_any_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_zero_any_repeat)) * pa_c_hj32_three_zero_any)) /\ exists pa_q_hj32_three_zero_any_repeat_decoded. pa_b_hj32_three_zero_any = pa_q_hj32_three_zero_any_repeat_decoded * S ((S (pa_i_hj32_three_zero_any_repeat)) * pa_c_hj32_three_zero_any) + (3)))) /\ (exists pa_u_hj32_three_zero_any_product pa_v_hj32_three_zero_any_product. ((((exists pa_h_hj32_three_zero_any_product_start. pa_h_hj32_three_zero_any_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_start. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_start * S ((S (0)) * pa_v_hj32_three_zero_any_product) + (1))) /\ ((((exists pa_h_hj32_three_zero_any_product_terminal. pa_h_hj32_three_zero_any_product_terminal + S (q) = S ((S (0)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_terminal. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_terminal * S ((S (0)) * pa_v_hj32_three_zero_any_product) + (q))) /\ forall pa_i_hj32_three_zero_any_product. (exists pa_lt_hj32_three_zero_any_product_bound. pa_lt_hj32_three_zero_any_product_bound + S pa_i_hj32_three_zero_any_product = 0) -> exists pa_p_hj32_three_zero_any_product pa_r_hj32_three_zero_any_product pa_s_hj32_three_zero_any_product. ((((exists pa_h_hj32_three_zero_any_product_factor. pa_h_hj32_three_zero_any_product_factor + S (pa_p_hj32_three_zero_any_product) = S ((S (pa_i_hj32_three_zero_any_product)) * pa_c_hj32_three_zero_any)) /\ exists pa_q_hj32_three_zero_any_product_factor. pa_b_hj32_three_zero_any = pa_q_hj32_three_zero_any_product_factor * S ((S (pa_i_hj32_three_zero_any_product)) * pa_c_hj32_three_zero_any) + (pa_p_hj32_three_zero_any_product))) /\ ((((exists pa_h_hj32_three_zero_any_product_partial. pa_h_hj32_three_zero_any_product_partial + S (pa_r_hj32_three_zero_any_product) = S ((S (pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_partial. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_partial * S ((S (pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product) + (pa_r_hj32_three_zero_any_product))) /\ ((((exists pa_h_hj32_three_zero_any_product_successor. pa_h_hj32_three_zero_any_product_successor + S (pa_s_hj32_three_zero_any_product) = S ((S (S pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product)) /\ exists pa_q_hj32_three_zero_any_product_successor. pa_u_hj32_three_zero_any_product = pa_q_hj32_three_zero_any_product_successor * S ((S (S pa_i_hj32_three_zero_any_product)) * pa_v_hj32_three_zero_any_product) + (pa_s_hj32_three_zero_any_product))) /\ pa_s_hj32_three_zero_any_product = pa_r_hj32_three_zero_any_product * pa_p_hj32_three_zero_any_product))))))))
7. 0007specialize htotal 3
8. 0008specialize htotal 0
9. 0009exact htotal
10. 0010cases hthree_zero_any
11. 0011have hthree_zero_value : x1 = 1
12. 0012specialize pow_zero 3
13. 0013specialize pow_zero 0
14. 0014specialize pow_zero x1
15. 0015apply pow_zero
16. 0016refl
17. 0017exact hthree_zero_any_witness
18. 0018have hthree_zero : exists pa_b_hj32_three_zero pa_c_hj32_three_zero. ((forall pa_i_hj32_three_zero_repeat. (exists pa_lt_hj32_three_zero_repeat_bound. pa_lt_hj32_three_zero_repeat_bound + S pa_i_hj32_three_zero_repeat = 0) -> (((exists pa_h_hj32_three_zero_repeat_decoded. pa_h_hj32_three_zero_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_zero_repeat)) * pa_c_hj32_three_zero)) /\ exists pa_q_hj32_three_zero_repeat_decoded. pa_b_hj32_three_zero = pa_q_hj32_three_zero_repeat_decoded * S ((S (pa_i_hj32_three_zero_repeat)) * pa_c_hj32_three_zero) + (3)))) /\ (exists pa_u_hj32_three_zero_product pa_v_hj32_three_zero_product. ((((exists pa_h_hj32_three_zero_product_start. pa_h_hj32_three_zero_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_start. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_start * S ((S (0)) * pa_v_hj32_three_zero_product) + (1))) /\ ((((exists pa_h_hj32_three_zero_product_terminal. pa_h_hj32_three_zero_product_terminal + S (1) = S ((S (0)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_terminal. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_terminal * S ((S (0)) * pa_v_hj32_three_zero_product) + (1))) /\ forall pa_i_hj32_three_zero_product. (exists pa_lt_hj32_three_zero_product_bound. pa_lt_hj32_three_zero_product_bound + S pa_i_hj32_three_zero_product = 0) -> exists pa_p_hj32_three_zero_product pa_r_hj32_three_zero_product pa_s_hj32_three_zero_product. ((((exists pa_h_hj32_three_zero_product_factor. pa_h_hj32_three_zero_product_factor + S (pa_p_hj32_three_zero_product) = S ((S (pa_i_hj32_three_zero_product)) * pa_c_hj32_three_zero)) /\ exists pa_q_hj32_three_zero_product_factor. pa_b_hj32_three_zero = pa_q_hj32_three_zero_product_factor * S ((S (pa_i_hj32_three_zero_product)) * pa_c_hj32_three_zero) + (pa_p_hj32_three_zero_product))) /\ ((((exists pa_h_hj32_three_zero_product_partial. pa_h_hj32_three_zero_product_partial + S (pa_r_hj32_three_zero_product) = S ((S (pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_partial. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_partial * S ((S (pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product) + (pa_r_hj32_three_zero_product))) /\ ((((exists pa_h_hj32_three_zero_product_successor. pa_h_hj32_three_zero_product_successor + S (pa_s_hj32_three_zero_product) = S ((S (S pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product)) /\ exists pa_q_hj32_three_zero_product_successor. pa_u_hj32_three_zero_product = pa_q_hj32_three_zero_product_successor * S ((S (S pa_i_hj32_three_zero_product)) * pa_v_hj32_three_zero_product) + (pa_s_hj32_three_zero_product))) /\ pa_s_hj32_three_zero_product = pa_r_hj32_three_zero_product * pa_p_hj32_three_zero_product)))))))
19. 0019rewrite hthree_zero_value at hthree_zero_any_witness
20. 0020rewrite hthree_zero_value at hthree_zero_any_witness
21. 0021exact hthree_zero_any_witness
22. 0022have hthree_one : exists pa_b_hj32_three_one pa_c_hj32_three_one. ((forall pa_i_hj32_three_one_repeat. (exists pa_lt_hj32_three_one_repeat_bound. pa_lt_hj32_three_one_repeat_bound + S pa_i_hj32_three_one_repeat = 1) -> (((exists pa_h_hj32_three_one_repeat_decoded. pa_h_hj32_three_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_one_repeat)) * pa_c_hj32_three_one)) /\ exists pa_q_hj32_three_one_repeat_decoded. pa_b_hj32_three_one = pa_q_hj32_three_one_repeat_decoded * S ((S (pa_i_hj32_three_one_repeat)) * pa_c_hj32_three_one) + (3)))) /\ (exists pa_u_hj32_three_one_product pa_v_hj32_three_one_product. ((((exists pa_h_hj32_three_one_product_start. pa_h_hj32_three_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_start. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_start * S ((S (0)) * pa_v_hj32_three_one_product) + (1))) /\ ((((exists pa_h_hj32_three_one_product_terminal. pa_h_hj32_three_one_product_terminal + S (1 * 3) = S ((S (1)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_terminal. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_terminal * S ((S (1)) * pa_v_hj32_three_one_product) + (1 * 3))) /\ forall pa_i_hj32_three_one_product. (exists pa_lt_hj32_three_one_product_bound. pa_lt_hj32_three_one_product_bound + S pa_i_hj32_three_one_product = 1) -> exists pa_p_hj32_three_one_product pa_r_hj32_three_one_product pa_s_hj32_three_one_product. ((((exists pa_h_hj32_three_one_product_factor. pa_h_hj32_three_one_product_factor + S (pa_p_hj32_three_one_product) = S ((S (pa_i_hj32_three_one_product)) * pa_c_hj32_three_one)) /\ exists pa_q_hj32_three_one_product_factor. pa_b_hj32_three_one = pa_q_hj32_three_one_product_factor * S ((S (pa_i_hj32_three_one_product)) * pa_c_hj32_three_one) + (pa_p_hj32_three_one_product))) /\ ((((exists pa_h_hj32_three_one_product_partial. pa_h_hj32_three_one_product_partial + S (pa_r_hj32_three_one_product) = S ((S (pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_partial. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_partial * S ((S (pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product) + (pa_r_hj32_three_one_product))) /\ ((((exists pa_h_hj32_three_one_product_successor. pa_h_hj32_three_one_product_successor + S (pa_s_hj32_three_one_product) = S ((S (S pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product)) /\ exists pa_q_hj32_three_one_product_successor. pa_u_hj32_three_one_product = pa_q_hj32_three_one_product_successor * S ((S (S pa_i_hj32_three_one_product)) * pa_v_hj32_three_one_product) + (pa_s_hj32_three_one_product))) /\ pa_s_hj32_three_one_product = pa_r_hj32_three_one_product * pa_p_hj32_three_one_product)))))))
23. 0023specialize pow_successor_compose_from_total 3
24. 0024specialize pow_successor_compose_from_total 0
25. 0025specialize pow_successor_compose_from_total 1
26. 0026specialize pow_successor_compose_from_total (1 * 3)
27. 0027apply pow_successor_compose_from_total
28. 0028exact htotal
29. 0029exact hthree_zero
30. 0030refl
31. 0031have hthree_two : exists pa_b_hj32_three_two pa_c_hj32_three_two. ((forall pa_i_hj32_three_two_repeat. (exists pa_lt_hj32_three_two_repeat_bound. pa_lt_hj32_three_two_repeat_bound + S pa_i_hj32_three_two_repeat = 2) -> (((exists pa_h_hj32_three_two_repeat_decoded. pa_h_hj32_three_two_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_two_repeat)) * pa_c_hj32_three_two)) /\ exists pa_q_hj32_three_two_repeat_decoded. pa_b_hj32_three_two = pa_q_hj32_three_two_repeat_decoded * S ((S (pa_i_hj32_three_two_repeat)) * pa_c_hj32_three_two) + (3)))) /\ (exists pa_u_hj32_three_two_product pa_v_hj32_three_two_product. ((((exists pa_h_hj32_three_two_product_start. pa_h_hj32_three_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_start. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_start * S ((S (0)) * pa_v_hj32_three_two_product) + (1))) /\ ((((exists pa_h_hj32_three_two_product_terminal. pa_h_hj32_three_two_product_terminal + S ((1 * 3) * 3) = S ((S (2)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_terminal. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_terminal * S ((S (2)) * pa_v_hj32_three_two_product) + ((1 * 3) * 3))) /\ forall pa_i_hj32_three_two_product. (exists pa_lt_hj32_three_two_product_bound. pa_lt_hj32_three_two_product_bound + S pa_i_hj32_three_two_product = 2) -> exists pa_p_hj32_three_two_product pa_r_hj32_three_two_product pa_s_hj32_three_two_product. ((((exists pa_h_hj32_three_two_product_factor. pa_h_hj32_three_two_product_factor + S (pa_p_hj32_three_two_product) = S ((S (pa_i_hj32_three_two_product)) * pa_c_hj32_three_two)) /\ exists pa_q_hj32_three_two_product_factor. pa_b_hj32_three_two = pa_q_hj32_three_two_product_factor * S ((S (pa_i_hj32_three_two_product)) * pa_c_hj32_three_two) + (pa_p_hj32_three_two_product))) /\ ((((exists pa_h_hj32_three_two_product_partial. pa_h_hj32_three_two_product_partial + S (pa_r_hj32_three_two_product) = S ((S (pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_partial. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_partial * S ((S (pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product) + (pa_r_hj32_three_two_product))) /\ ((((exists pa_h_hj32_three_two_product_successor. pa_h_hj32_three_two_product_successor + S (pa_s_hj32_three_two_product) = S ((S (S pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product)) /\ exists pa_q_hj32_three_two_product_successor. pa_u_hj32_three_two_product = pa_q_hj32_three_two_product_successor * S ((S (S pa_i_hj32_three_two_product)) * pa_v_hj32_three_two_product) + (pa_s_hj32_three_two_product))) /\ pa_s_hj32_three_two_product = pa_r_hj32_three_two_product * pa_p_hj32_three_two_product)))))))
32. 0032specialize pow_successor_compose_from_total 3
33. 0033specialize pow_successor_compose_from_total 1
34. 0034specialize pow_successor_compose_from_total (1 * 3)
35. 0035specialize pow_successor_compose_from_total ((1 * 3) * 3)
36. 0036apply pow_successor_compose_from_total
37. 0037exact htotal
38. 0038exact hthree_one
39. 0039refl
40. 0040have hthree_three : exists pa_b_hj32_three_three pa_c_hj32_three_three. ((forall pa_i_hj32_three_three_repeat. (exists pa_lt_hj32_three_three_repeat_bound. pa_lt_hj32_three_three_repeat_bound + S pa_i_hj32_three_three_repeat = 3) -> (((exists pa_h_hj32_three_three_repeat_decoded. pa_h_hj32_three_three_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_three_repeat)) * pa_c_hj32_three_three)) /\ exists pa_q_hj32_three_three_repeat_decoded. pa_b_hj32_three_three = pa_q_hj32_three_three_repeat_decoded * S ((S (pa_i_hj32_three_three_repeat)) * pa_c_hj32_three_three) + (3)))) /\ (exists pa_u_hj32_three_three_product pa_v_hj32_three_three_product. ((((exists pa_h_hj32_three_three_product_start. pa_h_hj32_three_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_start. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_start * S ((S (0)) * pa_v_hj32_three_three_product) + (1))) /\ ((((exists pa_h_hj32_three_three_product_terminal. pa_h_hj32_three_three_product_terminal + S (((1 * 3) * 3) * 3) = S ((S (3)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_terminal. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_terminal * S ((S (3)) * pa_v_hj32_three_three_product) + (((1 * 3) * 3) * 3))) /\ forall pa_i_hj32_three_three_product. (exists pa_lt_hj32_three_three_product_bound. pa_lt_hj32_three_three_product_bound + S pa_i_hj32_three_three_product = 3) -> exists pa_p_hj32_three_three_product pa_r_hj32_three_three_product pa_s_hj32_three_three_product. ((((exists pa_h_hj32_three_three_product_factor. pa_h_hj32_three_three_product_factor + S (pa_p_hj32_three_three_product) = S ((S (pa_i_hj32_three_three_product)) * pa_c_hj32_three_three)) /\ exists pa_q_hj32_three_three_product_factor. pa_b_hj32_three_three = pa_q_hj32_three_three_product_factor * S ((S (pa_i_hj32_three_three_product)) * pa_c_hj32_three_three) + (pa_p_hj32_three_three_product))) /\ ((((exists pa_h_hj32_three_three_product_partial. pa_h_hj32_three_three_product_partial + S (pa_r_hj32_three_three_product) = S ((S (pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_partial. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_partial * S ((S (pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product) + (pa_r_hj32_three_three_product))) /\ ((((exists pa_h_hj32_three_three_product_successor. pa_h_hj32_three_three_product_successor + S (pa_s_hj32_three_three_product) = S ((S (S pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product)) /\ exists pa_q_hj32_three_three_product_successor. pa_u_hj32_three_three_product = pa_q_hj32_three_three_product_successor * S ((S (S pa_i_hj32_three_three_product)) * pa_v_hj32_three_three_product) + (pa_s_hj32_three_three_product))) /\ pa_s_hj32_three_three_product = pa_r_hj32_three_three_product * pa_p_hj32_three_three_product)))))))
41. 0041specialize pow_successor_compose_from_total 3
42. 0042specialize pow_successor_compose_from_total 2
43. 0043specialize pow_successor_compose_from_total ((1 * 3) * 3)
44. 0044specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3)
45. 0045apply pow_successor_compose_from_total
46. 0046exact htotal
47. 0047exact hthree_two
48. 0048refl
49. 0049have hthree_four : exists pa_b_hj32_three_four pa_c_hj32_three_four. ((forall pa_i_hj32_three_four_repeat. (exists pa_lt_hj32_three_four_repeat_bound. pa_lt_hj32_three_four_repeat_bound + S pa_i_hj32_three_four_repeat = 4) -> (((exists pa_h_hj32_three_four_repeat_decoded. pa_h_hj32_three_four_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_four_repeat)) * pa_c_hj32_three_four)) /\ exists pa_q_hj32_three_four_repeat_decoded. pa_b_hj32_three_four = pa_q_hj32_three_four_repeat_decoded * S ((S (pa_i_hj32_three_four_repeat)) * pa_c_hj32_three_four) + (3)))) /\ (exists pa_u_hj32_three_four_product pa_v_hj32_three_four_product. ((((exists pa_h_hj32_three_four_product_start. pa_h_hj32_three_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_start. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_start * S ((S (0)) * pa_v_hj32_three_four_product) + (1))) /\ ((((exists pa_h_hj32_three_four_product_terminal. pa_h_hj32_three_four_product_terminal + S ((((1 * 3) * 3) * 3) * 3) = S ((S (4)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_terminal. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_terminal * S ((S (4)) * pa_v_hj32_three_four_product) + ((((1 * 3) * 3) * 3) * 3))) /\ forall pa_i_hj32_three_four_product. (exists pa_lt_hj32_three_four_product_bound. pa_lt_hj32_three_four_product_bound + S pa_i_hj32_three_four_product = 4) -> exists pa_p_hj32_three_four_product pa_r_hj32_three_four_product pa_s_hj32_three_four_product. ((((exists pa_h_hj32_three_four_product_factor. pa_h_hj32_three_four_product_factor + S (pa_p_hj32_three_four_product) = S ((S (pa_i_hj32_three_four_product)) * pa_c_hj32_three_four)) /\ exists pa_q_hj32_three_four_product_factor. pa_b_hj32_three_four = pa_q_hj32_three_four_product_factor * S ((S (pa_i_hj32_three_four_product)) * pa_c_hj32_three_four) + (pa_p_hj32_three_four_product))) /\ ((((exists pa_h_hj32_three_four_product_partial. pa_h_hj32_three_four_product_partial + S (pa_r_hj32_three_four_product) = S ((S (pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_partial. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_partial * S ((S (pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product) + (pa_r_hj32_three_four_product))) /\ ((((exists pa_h_hj32_three_four_product_successor. pa_h_hj32_three_four_product_successor + S (pa_s_hj32_three_four_product) = S ((S (S pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product)) /\ exists pa_q_hj32_three_four_product_successor. pa_u_hj32_three_four_product = pa_q_hj32_three_four_product_successor * S ((S (S pa_i_hj32_three_four_product)) * pa_v_hj32_three_four_product) + (pa_s_hj32_three_four_product))) /\ pa_s_hj32_three_four_product = pa_r_hj32_three_four_product * pa_p_hj32_three_four_product)))))))
50. 0050specialize pow_successor_compose_from_total 3
51. 0051specialize pow_successor_compose_from_total 3
52. 0052specialize pow_successor_compose_from_total (((1 * 3) * 3) * 3)
53. 0053specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3)
54. 0054apply pow_successor_compose_from_total
55. 0055exact htotal
56. 0056exact hthree_three
57. 0057refl
58. 0058have hthree_five : exists pa_b_hj32_three_five_exact pa_c_hj32_three_five_exact. ((forall pa_i_hj32_three_five_exact_repeat. (exists pa_lt_hj32_three_five_exact_repeat_bound. pa_lt_hj32_three_five_exact_repeat_bound + S pa_i_hj32_three_five_exact_repeat = 5) -> (((exists pa_h_hj32_three_five_exact_repeat_decoded. pa_h_hj32_three_five_exact_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_five_exact_repeat)) * pa_c_hj32_three_five_exact)) /\ exists pa_q_hj32_three_five_exact_repeat_decoded. pa_b_hj32_three_five_exact = pa_q_hj32_three_five_exact_repeat_decoded * S ((S (pa_i_hj32_three_five_exact_repeat)) * pa_c_hj32_three_five_exact) + (3)))) /\ (exists pa_u_hj32_three_five_exact_product pa_v_hj32_three_five_exact_product. ((((exists pa_h_hj32_three_five_exact_product_start. pa_h_hj32_three_five_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_start. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_start * S ((S (0)) * pa_v_hj32_three_five_exact_product) + (1))) /\ ((((exists pa_h_hj32_three_five_exact_product_terminal. pa_h_hj32_three_five_exact_product_terminal + S (((((1 * 3) * 3) * 3) * 3) * 3) = S ((S (5)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_terminal. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_terminal * S ((S (5)) * pa_v_hj32_three_five_exact_product) + (((((1 * 3) * 3) * 3) * 3) * 3))) /\ forall pa_i_hj32_three_five_exact_product. (exists pa_lt_hj32_three_five_exact_product_bound. pa_lt_hj32_three_five_exact_product_bound + S pa_i_hj32_three_five_exact_product = 5) -> exists pa_p_hj32_three_five_exact_product pa_r_hj32_three_five_exact_product pa_s_hj32_three_five_exact_product. ((((exists pa_h_hj32_three_five_exact_product_factor. pa_h_hj32_three_five_exact_product_factor + S (pa_p_hj32_three_five_exact_product) = S ((S (pa_i_hj32_three_five_exact_product)) * pa_c_hj32_three_five_exact)) /\ exists pa_q_hj32_three_five_exact_product_factor. pa_b_hj32_three_five_exact = pa_q_hj32_three_five_exact_product_factor * S ((S (pa_i_hj32_three_five_exact_product)) * pa_c_hj32_three_five_exact) + (pa_p_hj32_three_five_exact_product))) /\ ((((exists pa_h_hj32_three_five_exact_product_partial. pa_h_hj32_three_five_exact_product_partial + S (pa_r_hj32_three_five_exact_product) = S ((S (pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_partial. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_partial * S ((S (pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product) + (pa_r_hj32_three_five_exact_product))) /\ ((((exists pa_h_hj32_three_five_exact_product_successor. pa_h_hj32_three_five_exact_product_successor + S (pa_s_hj32_three_five_exact_product) = S ((S (S pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product)) /\ exists pa_q_hj32_three_five_exact_product_successor. pa_u_hj32_three_five_exact_product = pa_q_hj32_three_five_exact_product_successor * S ((S (S pa_i_hj32_three_five_exact_product)) * pa_v_hj32_three_five_exact_product) + (pa_s_hj32_three_five_exact_product))) /\ pa_s_hj32_three_five_exact_product = pa_r_hj32_three_five_exact_product * pa_p_hj32_three_five_exact_product)))))))
59. 0059specialize pow_successor_compose_from_total 3
60. 0060specialize pow_successor_compose_from_total 4
61. 0061specialize pow_successor_compose_from_total ((((1 * 3) * 3) * 3) * 3)
62. 0062specialize pow_successor_compose_from_total (((((1 * 3) * 3) * 3) * 3) * 3)
63. 0063apply pow_successor_compose_from_total
64. 0064exact htotal
65. 0065exact hthree_four
66. 0066refl
67. 0067have hfour_zero_any : exists q. (exists pa_b_hj32_four_zero_any pa_c_hj32_four_zero_any. ((forall pa_i_hj32_four_zero_any_repeat. (exists pa_lt_hj32_four_zero_any_repeat_bound. pa_lt_hj32_four_zero_any_repeat_bound + S pa_i_hj32_four_zero_any_repeat = 0) -> (((exists pa_h_hj32_four_zero_any_repeat_decoded. pa_h_hj32_four_zero_any_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_zero_any_repeat)) * pa_c_hj32_four_zero_any)) /\ exists pa_q_hj32_four_zero_any_repeat_decoded. pa_b_hj32_four_zero_any = pa_q_hj32_four_zero_any_repeat_decoded * S ((S (pa_i_hj32_four_zero_any_repeat)) * pa_c_hj32_four_zero_any) + (4)))) /\ (exists pa_u_hj32_four_zero_any_product pa_v_hj32_four_zero_any_product. ((((exists pa_h_hj32_four_zero_any_product_start. pa_h_hj32_four_zero_any_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_start. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_start * S ((S (0)) * pa_v_hj32_four_zero_any_product) + (1))) /\ ((((exists pa_h_hj32_four_zero_any_product_terminal. pa_h_hj32_four_zero_any_product_terminal + S (q) = S ((S (0)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_terminal. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_terminal * S ((S (0)) * pa_v_hj32_four_zero_any_product) + (q))) /\ forall pa_i_hj32_four_zero_any_product. (exists pa_lt_hj32_four_zero_any_product_bound. pa_lt_hj32_four_zero_any_product_bound + S pa_i_hj32_four_zero_any_product = 0) -> exists pa_p_hj32_four_zero_any_product pa_r_hj32_four_zero_any_product pa_s_hj32_four_zero_any_product. ((((exists pa_h_hj32_four_zero_any_product_factor. pa_h_hj32_four_zero_any_product_factor + S (pa_p_hj32_four_zero_any_product) = S ((S (pa_i_hj32_four_zero_any_product)) * pa_c_hj32_four_zero_any)) /\ exists pa_q_hj32_four_zero_any_product_factor. pa_b_hj32_four_zero_any = pa_q_hj32_four_zero_any_product_factor * S ((S (pa_i_hj32_four_zero_any_product)) * pa_c_hj32_four_zero_any) + (pa_p_hj32_four_zero_any_product))) /\ ((((exists pa_h_hj32_four_zero_any_product_partial. pa_h_hj32_four_zero_any_product_partial + S (pa_r_hj32_four_zero_any_product) = S ((S (pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_partial. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_partial * S ((S (pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product) + (pa_r_hj32_four_zero_any_product))) /\ ((((exists pa_h_hj32_four_zero_any_product_successor. pa_h_hj32_four_zero_any_product_successor + S (pa_s_hj32_four_zero_any_product) = S ((S (S pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product)) /\ exists pa_q_hj32_four_zero_any_product_successor. pa_u_hj32_four_zero_any_product = pa_q_hj32_four_zero_any_product_successor * S ((S (S pa_i_hj32_four_zero_any_product)) * pa_v_hj32_four_zero_any_product) + (pa_s_hj32_four_zero_any_product))) /\ pa_s_hj32_four_zero_any_product = pa_r_hj32_four_zero_any_product * pa_p_hj32_four_zero_any_product))))))))
68. 0068specialize htotal 4
69. 0069specialize htotal 0
70. 0070exact htotal
71. 0071cases hfour_zero_any
72. 0072have hfour_zero_value : x2 = 1
73. 0073specialize pow_zero 4
74. 0074specialize pow_zero 0
75. 0075specialize pow_zero x2
76. 0076apply pow_zero
77. 0077refl
78. 0078exact hfour_zero_any_witness
79. 0079have hfour_zero : exists pa_b_hj32_four_zero pa_c_hj32_four_zero. ((forall pa_i_hj32_four_zero_repeat. (exists pa_lt_hj32_four_zero_repeat_bound. pa_lt_hj32_four_zero_repeat_bound + S pa_i_hj32_four_zero_repeat = 0) -> (((exists pa_h_hj32_four_zero_repeat_decoded. pa_h_hj32_four_zero_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_zero_repeat)) * pa_c_hj32_four_zero)) /\ exists pa_q_hj32_four_zero_repeat_decoded. pa_b_hj32_four_zero = pa_q_hj32_four_zero_repeat_decoded * S ((S (pa_i_hj32_four_zero_repeat)) * pa_c_hj32_four_zero) + (4)))) /\ (exists pa_u_hj32_four_zero_product pa_v_hj32_four_zero_product. ((((exists pa_h_hj32_four_zero_product_start. pa_h_hj32_four_zero_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_start. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_start * S ((S (0)) * pa_v_hj32_four_zero_product) + (1))) /\ ((((exists pa_h_hj32_four_zero_product_terminal. pa_h_hj32_four_zero_product_terminal + S (1) = S ((S (0)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_terminal. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_terminal * S ((S (0)) * pa_v_hj32_four_zero_product) + (1))) /\ forall pa_i_hj32_four_zero_product. (exists pa_lt_hj32_four_zero_product_bound. pa_lt_hj32_four_zero_product_bound + S pa_i_hj32_four_zero_product = 0) -> exists pa_p_hj32_four_zero_product pa_r_hj32_four_zero_product pa_s_hj32_four_zero_product. ((((exists pa_h_hj32_four_zero_product_factor. pa_h_hj32_four_zero_product_factor + S (pa_p_hj32_four_zero_product) = S ((S (pa_i_hj32_four_zero_product)) * pa_c_hj32_four_zero)) /\ exists pa_q_hj32_four_zero_product_factor. pa_b_hj32_four_zero = pa_q_hj32_four_zero_product_factor * S ((S (pa_i_hj32_four_zero_product)) * pa_c_hj32_four_zero) + (pa_p_hj32_four_zero_product))) /\ ((((exists pa_h_hj32_four_zero_product_partial. pa_h_hj32_four_zero_product_partial + S (pa_r_hj32_four_zero_product) = S ((S (pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_partial. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_partial * S ((S (pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product) + (pa_r_hj32_four_zero_product))) /\ ((((exists pa_h_hj32_four_zero_product_successor. pa_h_hj32_four_zero_product_successor + S (pa_s_hj32_four_zero_product) = S ((S (S pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product)) /\ exists pa_q_hj32_four_zero_product_successor. pa_u_hj32_four_zero_product = pa_q_hj32_four_zero_product_successor * S ((S (S pa_i_hj32_four_zero_product)) * pa_v_hj32_four_zero_product) + (pa_s_hj32_four_zero_product))) /\ pa_s_hj32_four_zero_product = pa_r_hj32_four_zero_product * pa_p_hj32_four_zero_product)))))))
80. 0080rewrite hfour_zero_value at hfour_zero_any_witness
81. 0081rewrite hfour_zero_value at hfour_zero_any_witness
82. 0082exact hfour_zero_any_witness
83. 0083have hfour_one : exists pa_b_hj32_four_one pa_c_hj32_four_one. ((forall pa_i_hj32_four_one_repeat. (exists pa_lt_hj32_four_one_repeat_bound. pa_lt_hj32_four_one_repeat_bound + S pa_i_hj32_four_one_repeat = 1) -> (((exists pa_h_hj32_four_one_repeat_decoded. pa_h_hj32_four_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_one_repeat)) * pa_c_hj32_four_one)) /\ exists pa_q_hj32_four_one_repeat_decoded. pa_b_hj32_four_one = pa_q_hj32_four_one_repeat_decoded * S ((S (pa_i_hj32_four_one_repeat)) * pa_c_hj32_four_one) + (4)))) /\ (exists pa_u_hj32_four_one_product pa_v_hj32_four_one_product. ((((exists pa_h_hj32_four_one_product_start. pa_h_hj32_four_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_start. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_start * S ((S (0)) * pa_v_hj32_four_one_product) + (1))) /\ ((((exists pa_h_hj32_four_one_product_terminal. pa_h_hj32_four_one_product_terminal + S (1 * 4) = S ((S (1)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_terminal. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_terminal * S ((S (1)) * pa_v_hj32_four_one_product) + (1 * 4))) /\ forall pa_i_hj32_four_one_product. (exists pa_lt_hj32_four_one_product_bound. pa_lt_hj32_four_one_product_bound + S pa_i_hj32_four_one_product = 1) -> exists pa_p_hj32_four_one_product pa_r_hj32_four_one_product pa_s_hj32_four_one_product. ((((exists pa_h_hj32_four_one_product_factor. pa_h_hj32_four_one_product_factor + S (pa_p_hj32_four_one_product) = S ((S (pa_i_hj32_four_one_product)) * pa_c_hj32_four_one)) /\ exists pa_q_hj32_four_one_product_factor. pa_b_hj32_four_one = pa_q_hj32_four_one_product_factor * S ((S (pa_i_hj32_four_one_product)) * pa_c_hj32_four_one) + (pa_p_hj32_four_one_product))) /\ ((((exists pa_h_hj32_four_one_product_partial. pa_h_hj32_four_one_product_partial + S (pa_r_hj32_four_one_product) = S ((S (pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_partial. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_partial * S ((S (pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product) + (pa_r_hj32_four_one_product))) /\ ((((exists pa_h_hj32_four_one_product_successor. pa_h_hj32_four_one_product_successor + S (pa_s_hj32_four_one_product) = S ((S (S pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product)) /\ exists pa_q_hj32_four_one_product_successor. pa_u_hj32_four_one_product = pa_q_hj32_four_one_product_successor * S ((S (S pa_i_hj32_four_one_product)) * pa_v_hj32_four_one_product) + (pa_s_hj32_four_one_product))) /\ pa_s_hj32_four_one_product = pa_r_hj32_four_one_product * pa_p_hj32_four_one_product)))))))
84. 0084specialize pow_successor_compose_from_total 4
85. 0085specialize pow_successor_compose_from_total 0
86. 0086specialize pow_successor_compose_from_total 1
87. 0087specialize pow_successor_compose_from_total (1 * 4)
88. 0088apply pow_successor_compose_from_total
89. 0089exact htotal
90. 0090exact hfour_zero
91. 0091refl
92. 0092have hfour_two : exists pa_b_hj32_four_two pa_c_hj32_four_two. ((forall pa_i_hj32_four_two_repeat. (exists pa_lt_hj32_four_two_repeat_bound. pa_lt_hj32_four_two_repeat_bound + S pa_i_hj32_four_two_repeat = 2) -> (((exists pa_h_hj32_four_two_repeat_decoded. pa_h_hj32_four_two_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_two_repeat)) * pa_c_hj32_four_two)) /\ exists pa_q_hj32_four_two_repeat_decoded. pa_b_hj32_four_two = pa_q_hj32_four_two_repeat_decoded * S ((S (pa_i_hj32_four_two_repeat)) * pa_c_hj32_four_two) + (4)))) /\ (exists pa_u_hj32_four_two_product pa_v_hj32_four_two_product. ((((exists pa_h_hj32_four_two_product_start. pa_h_hj32_four_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_start. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_start * S ((S (0)) * pa_v_hj32_four_two_product) + (1))) /\ ((((exists pa_h_hj32_four_two_product_terminal. pa_h_hj32_four_two_product_terminal + S ((1 * 4) * 4) = S ((S (2)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_terminal. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_terminal * S ((S (2)) * pa_v_hj32_four_two_product) + ((1 * 4) * 4))) /\ forall pa_i_hj32_four_two_product. (exists pa_lt_hj32_four_two_product_bound. pa_lt_hj32_four_two_product_bound + S pa_i_hj32_four_two_product = 2) -> exists pa_p_hj32_four_two_product pa_r_hj32_four_two_product pa_s_hj32_four_two_product. ((((exists pa_h_hj32_four_two_product_factor. pa_h_hj32_four_two_product_factor + S (pa_p_hj32_four_two_product) = S ((S (pa_i_hj32_four_two_product)) * pa_c_hj32_four_two)) /\ exists pa_q_hj32_four_two_product_factor. pa_b_hj32_four_two = pa_q_hj32_four_two_product_factor * S ((S (pa_i_hj32_four_two_product)) * pa_c_hj32_four_two) + (pa_p_hj32_four_two_product))) /\ ((((exists pa_h_hj32_four_two_product_partial. pa_h_hj32_four_two_product_partial + S (pa_r_hj32_four_two_product) = S ((S (pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_partial. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_partial * S ((S (pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product) + (pa_r_hj32_four_two_product))) /\ ((((exists pa_h_hj32_four_two_product_successor. pa_h_hj32_four_two_product_successor + S (pa_s_hj32_four_two_product) = S ((S (S pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product)) /\ exists pa_q_hj32_four_two_product_successor. pa_u_hj32_four_two_product = pa_q_hj32_four_two_product_successor * S ((S (S pa_i_hj32_four_two_product)) * pa_v_hj32_four_two_product) + (pa_s_hj32_four_two_product))) /\ pa_s_hj32_four_two_product = pa_r_hj32_four_two_product * pa_p_hj32_four_two_product)))))))
93. 0093specialize pow_successor_compose_from_total 4
94. 0094specialize pow_successor_compose_from_total 1
95. 0095specialize pow_successor_compose_from_total (1 * 4)
96. 0096specialize pow_successor_compose_from_total ((1 * 4) * 4)
97. 0097apply pow_successor_compose_from_total
98. 0098exact htotal
99. 0099exact hfour_one
100. 0100refl
101. 0101have hfour_three : exists pa_b_hj32_four_three pa_c_hj32_four_three. ((forall pa_i_hj32_four_three_repeat. (exists pa_lt_hj32_four_three_repeat_bound. pa_lt_hj32_four_three_repeat_bound + S pa_i_hj32_four_three_repeat = 3) -> (((exists pa_h_hj32_four_three_repeat_decoded. pa_h_hj32_four_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_three_repeat)) * pa_c_hj32_four_three)) /\ exists pa_q_hj32_four_three_repeat_decoded. pa_b_hj32_four_three = pa_q_hj32_four_three_repeat_decoded * S ((S (pa_i_hj32_four_three_repeat)) * pa_c_hj32_four_three) + (4)))) /\ (exists pa_u_hj32_four_three_product pa_v_hj32_four_three_product. ((((exists pa_h_hj32_four_three_product_start. pa_h_hj32_four_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_start. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_start * S ((S (0)) * pa_v_hj32_four_three_product) + (1))) /\ ((((exists pa_h_hj32_four_three_product_terminal. pa_h_hj32_four_three_product_terminal + S (((1 * 4) * 4) * 4) = S ((S (3)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_terminal. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_terminal * S ((S (3)) * pa_v_hj32_four_three_product) + (((1 * 4) * 4) * 4))) /\ forall pa_i_hj32_four_three_product. (exists pa_lt_hj32_four_three_product_bound. pa_lt_hj32_four_three_product_bound + S pa_i_hj32_four_three_product = 3) -> exists pa_p_hj32_four_three_product pa_r_hj32_four_three_product pa_s_hj32_four_three_product. ((((exists pa_h_hj32_four_three_product_factor. pa_h_hj32_four_three_product_factor + S (pa_p_hj32_four_three_product) = S ((S (pa_i_hj32_four_three_product)) * pa_c_hj32_four_three)) /\ exists pa_q_hj32_four_three_product_factor. pa_b_hj32_four_three = pa_q_hj32_four_three_product_factor * S ((S (pa_i_hj32_four_three_product)) * pa_c_hj32_four_three) + (pa_p_hj32_four_three_product))) /\ ((((exists pa_h_hj32_four_three_product_partial. pa_h_hj32_four_three_product_partial + S (pa_r_hj32_four_three_product) = S ((S (pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_partial. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_partial * S ((S (pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product) + (pa_r_hj32_four_three_product))) /\ ((((exists pa_h_hj32_four_three_product_successor. pa_h_hj32_four_three_product_successor + S (pa_s_hj32_four_three_product) = S ((S (S pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product)) /\ exists pa_q_hj32_four_three_product_successor. pa_u_hj32_four_three_product = pa_q_hj32_four_three_product_successor * S ((S (S pa_i_hj32_four_three_product)) * pa_v_hj32_four_three_product) + (pa_s_hj32_four_three_product))) /\ pa_s_hj32_four_three_product = pa_r_hj32_four_three_product * pa_p_hj32_four_three_product)))))))
102. 0102specialize pow_successor_compose_from_total 4
103. 0103specialize pow_successor_compose_from_total 2
104. 0104specialize pow_successor_compose_from_total ((1 * 4) * 4)
105. 0105specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4)
106. 0106apply pow_successor_compose_from_total
107. 0107exact htotal
108. 0108exact hfour_two
109. 0109refl
110. 0110have hfour_four : exists pa_b_hj32_four_four_exact pa_c_hj32_four_four_exact. ((forall pa_i_hj32_four_four_exact_repeat. (exists pa_lt_hj32_four_four_exact_repeat_bound. pa_lt_hj32_four_four_exact_repeat_bound + S pa_i_hj32_four_four_exact_repeat = 4) -> (((exists pa_h_hj32_four_four_exact_repeat_decoded. pa_h_hj32_four_four_exact_repeat_decoded + S (4) = S ((S (pa_i_hj32_four_four_exact_repeat)) * pa_c_hj32_four_four_exact)) /\ exists pa_q_hj32_four_four_exact_repeat_decoded. pa_b_hj32_four_four_exact = pa_q_hj32_four_four_exact_repeat_decoded * S ((S (pa_i_hj32_four_four_exact_repeat)) * pa_c_hj32_four_four_exact) + (4)))) /\ (exists pa_u_hj32_four_four_exact_product pa_v_hj32_four_four_exact_product. ((((exists pa_h_hj32_four_four_exact_product_start. pa_h_hj32_four_four_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_start. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_start * S ((S (0)) * pa_v_hj32_four_four_exact_product) + (1))) /\ ((((exists pa_h_hj32_four_four_exact_product_terminal. pa_h_hj32_four_four_exact_product_terminal + S ((((1 * 4) * 4) * 4) * 4) = S ((S (4)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_terminal. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_terminal * S ((S (4)) * pa_v_hj32_four_four_exact_product) + ((((1 * 4) * 4) * 4) * 4))) /\ forall pa_i_hj32_four_four_exact_product. (exists pa_lt_hj32_four_four_exact_product_bound. pa_lt_hj32_four_four_exact_product_bound + S pa_i_hj32_four_four_exact_product = 4) -> exists pa_p_hj32_four_four_exact_product pa_r_hj32_four_four_exact_product pa_s_hj32_four_four_exact_product. ((((exists pa_h_hj32_four_four_exact_product_factor. pa_h_hj32_four_four_exact_product_factor + S (pa_p_hj32_four_four_exact_product) = S ((S (pa_i_hj32_four_four_exact_product)) * pa_c_hj32_four_four_exact)) /\ exists pa_q_hj32_four_four_exact_product_factor. pa_b_hj32_four_four_exact = pa_q_hj32_four_four_exact_product_factor * S ((S (pa_i_hj32_four_four_exact_product)) * pa_c_hj32_four_four_exact) + (pa_p_hj32_four_four_exact_product))) /\ ((((exists pa_h_hj32_four_four_exact_product_partial. pa_h_hj32_four_four_exact_product_partial + S (pa_r_hj32_four_four_exact_product) = S ((S (pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_partial. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_partial * S ((S (pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product) + (pa_r_hj32_four_four_exact_product))) /\ ((((exists pa_h_hj32_four_four_exact_product_successor. pa_h_hj32_four_four_exact_product_successor + S (pa_s_hj32_four_four_exact_product) = S ((S (S pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product)) /\ exists pa_q_hj32_four_four_exact_product_successor. pa_u_hj32_four_four_exact_product = pa_q_hj32_four_four_exact_product_successor * S ((S (S pa_i_hj32_four_four_exact_product)) * pa_v_hj32_four_four_exact_product) + (pa_s_hj32_four_four_exact_product))) /\ pa_s_hj32_four_four_exact_product = pa_r_hj32_four_four_exact_product * pa_p_hj32_four_four_exact_product)))))))
111. 0111specialize pow_successor_compose_from_total 4
112. 0112specialize pow_successor_compose_from_total 3
113. 0113specialize pow_successor_compose_from_total (((1 * 4) * 4) * 4)
114. 0114specialize pow_successor_compose_from_total ((((1 * 4) * 4) * 4) * 4)
115. 0115apply pow_successor_compose_from_total
116. 0116exact htotal
117. 0117exact hfour_three
118. 0118refl
119. 0119have hx_value : x = ((((1 * 3) * 3) * 3) * 3) * 3
120. 0120specialize pow_functional 3
121. 0121specialize pow_functional 5
122. 0122specialize pow_functional x
123. 0123specialize pow_functional (((((1 * 3) * 3) * 3) * 3) * 3)
124. 0124apply pow_functional
125. 0125exact hx
126. 0126exact hthree_five
127. 0127have hy_value : y = (((1 * 4) * 4) * 4) * 4
128. 0128specialize pow_functional 4
129. 0129specialize pow_functional 4
130. 0130specialize pow_functional y
131. 0131specialize pow_functional ((((1 * 4) * 4) * 4) * 4)
132. 0132apply pow_functional
133. 0133exact hy
134. 0134exact hfour_four
135. 0135rewrite hx_value
136. 0136rewrite hy_value
137. 0137exists 13
138. 0138have hthree_four_split : (((1 * 3) * 3) * 3) * 3 = (((1 * 4) * 4) * 4) + 17
139. 0139norm_num
140. 0140rewrite hthree_four_split
141. 0141specialize add_mul (((1 * 4) * 4) * 4)
142. 0142specialize add_mul 17
143. 0143specialize add_mul 3
144. 0144rewrite add_mul
145. 0145have hfour_step : (((1 * 4) * 4) * 4) * 4 = (((1 * 4) * 4) * 4) * 3 + (((1 * 4) * 4) * 4)
146. 0146apply PA6
147. 0147rewrite hfour_step
148. 0148have hseventeen_three : 17 * 3 = 51
149. 0149norm_num
150. 0150rewrite hseventeen_three
151. 0151have hthirteen_fifty_one : 13 + 51 = ((1 * 4) * 4) * 4
152. 0152norm_num
153. 0153trans (13 + (((1 * 4) * 4) * 4) * 3) + 51
154. 0154symm
155. 0155specialize add_assoc 13
156. 0156specialize add_assoc ((((1 * 4) * 4) * 4) * 3)
157. 0157specialize add_assoc 51
158. 0158apply add_assoc
159. 0159trans ((((1 * 4) * 4) * 4) * 3 + 13) + 51
160. 0160congr
161. 0161specialize add_comm 13
162. 0162specialize add_comm ((((1 * 4) * 4) * 4) * 3)
163. 0163apply add_comm
164. 0164refl
165. 0165trans (((1 * 4) * 4) * 4) * 3 + (13 + 51)
166. 0166specialize add_assoc ((((1 * 4) * 4) * 4) * 3)
167. 0167specialize add_assoc 13
168. 0168specialize add_assoc 51
169. 0169apply add_assoc
170. 0170rewrite hthirteen_fifty_one
171. 0171refl