BT00W5

pow_eleven_two_le_pow_two_seven_from_total

Alpha body-checked · checked-use disabled

The concrete seed inequality 11^2 <= 2^7 in the relational graph.

Exact expanded PA statement

forall x y. (forall bpt_a_hj32_eleven_two bpt_e_hj32_eleven_two. exists bpt_x_hj32_eleven_two. (exists ff_b_bpt_value_hj32_eleven_two ff_c_bpt_value_hj32_eleven_two. ((forall ff_i_bpt_value_hj32_eleven_two_repeat. (exists ff_lt_bpt_value_hj32_eleven_two_repeat_bound. ff_lt_bpt_value_hj32_eleven_two_repeat_bound + S ff_i_bpt_value_hj32_eleven_two_repeat = bpt_e_hj32_eleven_two) -> (((exists ff_h_bpt_value_hj32_eleven_two_repeat_decoded. ff_h_bpt_value_hj32_eleven_two_repeat_decoded + S (bpt_a_hj32_eleven_two) = S ((S (ff_i_bpt_value_hj32_eleven_two_repeat)) * ff_c_bpt_value_hj32_eleven_two)) /\ exists ff_q_bpt_value_hj32_eleven_two_repeat_decoded. ff_b_bpt_value_hj32_eleven_two = ff_q_bpt_value_hj32_eleven_two_repeat_decoded * S ((S (ff_i_bpt_value_hj32_eleven_two_repeat)) * ff_c_bpt_value_hj32_eleven_two) + (bpt_a_hj32_eleven_two)))) /\ (exists ff_u_bpt_value_hj32_eleven_two_product ff_v_bpt_value_hj32_eleven_two_product. ((((exists ff_h_bpt_value_hj32_eleven_two_product_start. ff_h_bpt_value_hj32_eleven_two_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_eleven_two_product)) /\ exists ff_q_bpt_value_hj32_eleven_two_product_start. ff_u_bpt_value_hj32_eleven_two_product = ff_q_bpt_value_hj32_eleven_two_product_start * S ((S (0)) * ff_v_bpt_value_hj32_eleven_two_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_eleven_two_product_terminal. ff_h_bpt_value_hj32_eleven_two_product_terminal + S (bpt_x_hj32_eleven_two) = S ((S (bpt_e_hj32_eleven_two)) * ff_v_bpt_value_hj32_eleven_two_product)) /\ exists ff_q_bpt_value_hj32_eleven_two_product_terminal. ff_u_bpt_value_hj32_eleven_two_product = ff_q_bpt_value_hj32_eleven_two_product_terminal * S ((S (bpt_e_hj32_eleven_two)) * ff_v_bpt_value_hj32_eleven_two_product) + (bpt_x_hj32_eleven_two))) /\ forall ff_i_bpt_value_hj32_eleven_two_product. (exists ff_lt_bpt_value_hj32_eleven_two_product_bound. ff_lt_bpt_value_hj32_eleven_two_product_bound + S ff_i_bpt_value_hj32_eleven_two_product = bpt_e_hj32_eleven_two) -> exists ff_p_bpt_value_hj32_eleven_two_product ff_r_bpt_value_hj32_eleven_two_product ff_s_bpt_value_hj32_eleven_two_product. ((((exists ff_h_bpt_value_hj32_eleven_two_product_factor. ff_h_bpt_value_hj32_eleven_two_product_factor + S (ff_p_bpt_value_hj32_eleven_two_product) = S ((S (ff_i_bpt_value_hj32_eleven_two_product)) * ff_c_bpt_value_hj32_eleven_two)) /\ exists ff_q_bpt_value_hj32_eleven_two_product_factor. ff_b_bpt_value_hj32_eleven_two = ff_q_bpt_value_hj32_eleven_two_product_factor * S ((S (ff_i_bpt_value_hj32_eleven_two_product)) * ff_c_bpt_value_hj32_eleven_two) + (ff_p_bpt_value_hj32_eleven_two_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_two_product_partial. ff_h_bpt_value_hj32_eleven_two_product_partial + S (ff_r_bpt_value_hj32_eleven_two_product) = S ((S (ff_i_bpt_value_hj32_eleven_two_product)) * ff_v_bpt_value_hj32_eleven_two_product)) /\ exists ff_q_bpt_value_hj32_eleven_two_product_partial. ff_u_bpt_value_hj32_eleven_two_product = ff_q_bpt_value_hj32_eleven_two_product_partial * S ((S (ff_i_bpt_value_hj32_eleven_two_product)) * ff_v_bpt_value_hj32_eleven_two_product) + (ff_r_bpt_value_hj32_eleven_two_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_two_product_successor. ff_h_bpt_value_hj32_eleven_two_product_successor + S (ff_s_bpt_value_hj32_eleven_two_product) = S ((S (S ff_i_bpt_value_hj32_eleven_two_product)) * ff_v_bpt_value_hj32_eleven_two_product)) /\ exists ff_q_bpt_value_hj32_eleven_two_product_successor. ff_u_bpt_value_hj32_eleven_two_product = ff_q_bpt_value_hj32_eleven_two_product_successor * S ((S (S ff_i_bpt_value_hj32_eleven_two_product)) * ff_v_bpt_value_hj32_eleven_two_product) + (ff_s_bpt_value_hj32_eleven_two_product))) /\ ff_s_bpt_value_hj32_eleven_two_product = ff_r_bpt_value_hj32_eleven_two_product * ff_p_bpt_value_hj32_eleven_two_product))))))))) -> (exists pa_b_hj32_eleven_two_left pa_c_hj32_eleven_two_left. ((forall pa_i_hj32_eleven_two_left_repeat. (exists pa_lt_hj32_eleven_two_left_repeat_bound. pa_lt_hj32_eleven_two_left_repeat_bound + S pa_i_hj32_eleven_two_left_repeat = 2) -> (((exists pa_h_hj32_eleven_two_left_repeat_decoded. pa_h_hj32_eleven_two_left_repeat_decoded + S (11) = S ((S (pa_i_hj32_eleven_two_left_repeat)) * pa_c_hj32_eleven_two_left)) /\ exists pa_q_hj32_eleven_two_left_repeat_decoded. pa_b_hj32_eleven_two_left = pa_q_hj32_eleven_two_left_repeat_decoded * S ((S (pa_i_hj32_eleven_two_left_repeat)) * pa_c_hj32_eleven_two_left) + (11)))) /\ (exists pa_u_hj32_eleven_two_left_product pa_v_hj32_eleven_two_left_product. ((((exists pa_h_hj32_eleven_two_left_product_start. pa_h_hj32_eleven_two_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_two_left_product)) /\ exists pa_q_hj32_eleven_two_left_product_start. pa_u_hj32_eleven_two_left_product = pa_q_hj32_eleven_two_left_product_start * S ((S (0)) * pa_v_hj32_eleven_two_left_product) + (1))) /\ ((((exists pa_h_hj32_eleven_two_left_product_terminal. pa_h_hj32_eleven_two_left_product_terminal + S (x) = S ((S (2)) * pa_v_hj32_eleven_two_left_product)) /\ exists pa_q_hj32_eleven_two_left_product_terminal. pa_u_hj32_eleven_two_left_product = pa_q_hj32_eleven_two_left_product_terminal * S ((S (2)) * pa_v_hj32_eleven_two_left_product) + (x))) /\ forall pa_i_hj32_eleven_two_left_product. (exists pa_lt_hj32_eleven_two_left_product_bound. pa_lt_hj32_eleven_two_left_product_bound + S pa_i_hj32_eleven_two_left_product = 2) -> exists pa_p_hj32_eleven_two_left_product pa_r_hj32_eleven_two_left_product pa_s_hj32_eleven_two_left_product. ((((exists pa_h_hj32_eleven_two_left_product_factor. pa_h_hj32_eleven_two_left_product_factor + S (pa_p_hj32_eleven_two_left_product) = S ((S (pa_i_hj32_eleven_two_left_product)) * pa_c_hj32_eleven_two_left)) /\ exists pa_q_hj32_eleven_two_left_product_factor. pa_b_hj32_eleven_two_left = pa_q_hj32_eleven_two_left_product_factor * S ((S (pa_i_hj32_eleven_two_left_product)) * pa_c_hj32_eleven_two_left) + (pa_p_hj32_eleven_two_left_product))) /\ ((((exists pa_h_hj32_eleven_two_left_product_partial. pa_h_hj32_eleven_two_left_product_partial + S (pa_r_hj32_eleven_two_left_product) = S ((S (pa_i_hj32_eleven_two_left_product)) * pa_v_hj32_eleven_two_left_product)) /\ exists pa_q_hj32_eleven_two_left_product_partial. pa_u_hj32_eleven_two_left_product = pa_q_hj32_eleven_two_left_product_partial * S ((S (pa_i_hj32_eleven_two_left_product)) * pa_v_hj32_eleven_two_left_product) + (pa_r_hj32_eleven_two_left_product))) /\ ((((exists pa_h_hj32_eleven_two_left_product_successor. pa_h_hj32_eleven_two_left_product_successor + S (pa_s_hj32_eleven_two_left_product) = S ((S (S pa_i_hj32_eleven_two_left_product)) * pa_v_hj32_eleven_two_left_product)) /\ exists pa_q_hj32_eleven_two_left_product_successor. pa_u_hj32_eleven_two_left_product = pa_q_hj32_eleven_two_left_product_successor * S ((S (S pa_i_hj32_eleven_two_left_product)) * pa_v_hj32_eleven_two_left_product) + (pa_s_hj32_eleven_two_left_product))) /\ pa_s_hj32_eleven_two_left_product = pa_r_hj32_eleven_two_left_product * pa_p_hj32_eleven_two_left_product)))))))) -> (exists pa_b_hj32_eleven_two_right pa_c_hj32_eleven_two_right. ((forall pa_i_hj32_eleven_two_right_repeat. (exists pa_lt_hj32_eleven_two_right_repeat_bound. pa_lt_hj32_eleven_two_right_repeat_bound + S pa_i_hj32_eleven_two_right_repeat = 7) -> (((exists pa_h_hj32_eleven_two_right_repeat_decoded. pa_h_hj32_eleven_two_right_repeat_decoded + S (2) = S ((S (pa_i_hj32_eleven_two_right_repeat)) * pa_c_hj32_eleven_two_right)) /\ exists pa_q_hj32_eleven_two_right_repeat_decoded. pa_b_hj32_eleven_two_right = pa_q_hj32_eleven_two_right_repeat_decoded * S ((S (pa_i_hj32_eleven_two_right_repeat)) * pa_c_hj32_eleven_two_right) + (2)))) /\ (exists pa_u_hj32_eleven_two_right_product pa_v_hj32_eleven_two_right_product. ((((exists pa_h_hj32_eleven_two_right_product_start. pa_h_hj32_eleven_two_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_two_right_product)) /\ exists pa_q_hj32_eleven_two_right_product_start. pa_u_hj32_eleven_two_right_product = pa_q_hj32_eleven_two_right_product_start * S ((S (0)) * pa_v_hj32_eleven_two_right_product) + (1))) /\ ((((exists pa_h_hj32_eleven_two_right_product_terminal. pa_h_hj32_eleven_two_right_product_terminal + S (y) = S ((S (7)) * pa_v_hj32_eleven_two_right_product)) /\ exists pa_q_hj32_eleven_two_right_product_terminal. pa_u_hj32_eleven_two_right_product = pa_q_hj32_eleven_two_right_product_terminal * S ((S (7)) * pa_v_hj32_eleven_two_right_product) + (y))) /\ forall pa_i_hj32_eleven_two_right_product. (exists pa_lt_hj32_eleven_two_right_product_bound. pa_lt_hj32_eleven_two_right_product_bound + S pa_i_hj32_eleven_two_right_product = 7) -> exists pa_p_hj32_eleven_two_right_product pa_r_hj32_eleven_two_right_product pa_s_hj32_eleven_two_right_product. ((((exists pa_h_hj32_eleven_two_right_product_factor. pa_h_hj32_eleven_two_right_product_factor + S (pa_p_hj32_eleven_two_right_product) = S ((S (pa_i_hj32_eleven_two_right_product)) * pa_c_hj32_eleven_two_right)) /\ exists pa_q_hj32_eleven_two_right_product_factor. pa_b_hj32_eleven_two_right = pa_q_hj32_eleven_two_right_product_factor * S ((S (pa_i_hj32_eleven_two_right_product)) * pa_c_hj32_eleven_two_right) + (pa_p_hj32_eleven_two_right_product))) /\ ((((exists pa_h_hj32_eleven_two_right_product_partial. pa_h_hj32_eleven_two_right_product_partial + S (pa_r_hj32_eleven_two_right_product) = S ((S (pa_i_hj32_eleven_two_right_product)) * pa_v_hj32_eleven_two_right_product)) /\ exists pa_q_hj32_eleven_two_right_product_partial. pa_u_hj32_eleven_two_right_product = pa_q_hj32_eleven_two_right_product_partial * S ((S (pa_i_hj32_eleven_two_right_product)) * pa_v_hj32_eleven_two_right_product) + (pa_r_hj32_eleven_two_right_product))) /\ ((((exists pa_h_hj32_eleven_two_right_product_successor. pa_h_hj32_eleven_two_right_product_successor + S (pa_s_hj32_eleven_two_right_product) = S ((S (S pa_i_hj32_eleven_two_right_product)) * pa_v_hj32_eleven_two_right_product)) /\ exists pa_q_hj32_eleven_two_right_product_successor. pa_u_hj32_eleven_two_right_product = pa_q_hj32_eleven_two_right_product_successor * S ((S (S pa_i_hj32_eleven_two_right_product)) * pa_v_hj32_eleven_two_right_product) + (pa_s_hj32_eleven_two_right_product))) /\ pa_s_hj32_eleven_two_right_product = pa_r_hj32_eleven_two_right_product * pa_p_hj32_eleven_two_right_product)))))))) -> (exists bqb_le_gap_hj32_eleven_two_result. bqb_le_gap_hj32_eleven_two_result + (x) = (y))

Structural proof guide

The concrete seed inequality 11^2 <= 2^7 in the relational graph.

Direct prerequisites: pow_two, pow_two_seed_bundle_from_total, pow_successor_compose_from_total, pow_functional, pow_add, add_mul, mul_add, add_assoc, add_comm. The authored body proceeds by case analysis (1), intermediate claims (12), equality transport (8), closed numeral normalization (4).

Proof neighborhood

Direct dependencies

BT009W pow_two BT00SO pow_two_seed_bundle_from_total BT00SL pow_successor_compose_from_total BT0082 pow_functional BT009X pow_add BT000B add_mul BT0007 mul_add BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total

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 hx_square : x = 11 * 11
  7. 0007specialize pow_two 11
  8. 0008specialize pow_two 2
  9. 0009specialize pow_two x
  10. 0010apply pow_two
  11. 0011refl
  12. 0012exact hx
  13. 0013have hseeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product))))))))
  14. 0014apply pow_two_seed_bundle_from_total
  15. 0015exact htotal
  16. 0016cases hseeds
  17. 0017have htwo_three : exists pa_b_hj32_two_three_exact pa_c_hj32_two_three_exact. ((forall pa_i_hj32_two_three_exact_repeat. (exists pa_lt_hj32_two_three_exact_repeat_bound. pa_lt_hj32_two_three_exact_repeat_bound + S pa_i_hj32_two_three_exact_repeat = 3) -> (((exists pa_h_hj32_two_three_exact_repeat_decoded. pa_h_hj32_two_three_exact_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_three_exact_repeat)) * pa_c_hj32_two_three_exact)) /\ exists pa_q_hj32_two_three_exact_repeat_decoded. pa_b_hj32_two_three_exact = pa_q_hj32_two_three_exact_repeat_decoded * S ((S (pa_i_hj32_two_three_exact_repeat)) * pa_c_hj32_two_three_exact) + (2)))) /\ (exists pa_u_hj32_two_three_exact_product pa_v_hj32_two_three_exact_product. ((((exists pa_h_hj32_two_three_exact_product_start. pa_h_hj32_two_three_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_three_exact_product)) /\ exists pa_q_hj32_two_three_exact_product_start. pa_u_hj32_two_three_exact_product = pa_q_hj32_two_three_exact_product_start * S ((S (0)) * pa_v_hj32_two_three_exact_product) + (1))) /\ ((((exists pa_h_hj32_two_three_exact_product_terminal. pa_h_hj32_two_three_exact_product_terminal + S (4 * 2) = S ((S (3)) * pa_v_hj32_two_three_exact_product)) /\ exists pa_q_hj32_two_three_exact_product_terminal. pa_u_hj32_two_three_exact_product = pa_q_hj32_two_three_exact_product_terminal * S ((S (3)) * pa_v_hj32_two_three_exact_product) + (4 * 2))) /\ forall pa_i_hj32_two_three_exact_product. (exists pa_lt_hj32_two_three_exact_product_bound. pa_lt_hj32_two_three_exact_product_bound + S pa_i_hj32_two_three_exact_product = 3) -> exists pa_p_hj32_two_three_exact_product pa_r_hj32_two_three_exact_product pa_s_hj32_two_three_exact_product. ((((exists pa_h_hj32_two_three_exact_product_factor. pa_h_hj32_two_three_exact_product_factor + S (pa_p_hj32_two_three_exact_product) = S ((S (pa_i_hj32_two_three_exact_product)) * pa_c_hj32_two_three_exact)) /\ exists pa_q_hj32_two_three_exact_product_factor. pa_b_hj32_two_three_exact = pa_q_hj32_two_three_exact_product_factor * S ((S (pa_i_hj32_two_three_exact_product)) * pa_c_hj32_two_three_exact) + (pa_p_hj32_two_three_exact_product))) /\ ((((exists pa_h_hj32_two_three_exact_product_partial. pa_h_hj32_two_three_exact_product_partial + S (pa_r_hj32_two_three_exact_product) = S ((S (pa_i_hj32_two_three_exact_product)) * pa_v_hj32_two_three_exact_product)) /\ exists pa_q_hj32_two_three_exact_product_partial. pa_u_hj32_two_three_exact_product = pa_q_hj32_two_three_exact_product_partial * S ((S (pa_i_hj32_two_three_exact_product)) * pa_v_hj32_two_three_exact_product) + (pa_r_hj32_two_three_exact_product))) /\ ((((exists pa_h_hj32_two_three_exact_product_successor. pa_h_hj32_two_three_exact_product_successor + S (pa_s_hj32_two_three_exact_product) = S ((S (S pa_i_hj32_two_three_exact_product)) * pa_v_hj32_two_three_exact_product)) /\ exists pa_q_hj32_two_three_exact_product_successor. pa_u_hj32_two_three_exact_product = pa_q_hj32_two_three_exact_product_successor * S ((S (S pa_i_hj32_two_three_exact_product)) * pa_v_hj32_two_three_exact_product) + (pa_s_hj32_two_three_exact_product))) /\ pa_s_hj32_two_three_exact_product = pa_r_hj32_two_three_exact_product * pa_p_hj32_two_three_exact_product)))))))
  18. 0018specialize pow_successor_compose_from_total 2
  19. 0019specialize pow_successor_compose_from_total 2
  20. 0020specialize pow_successor_compose_from_total 4
  21. 0021specialize pow_successor_compose_from_total (4 * 2)
  22. 0022apply pow_successor_compose_from_total
  23. 0023exact htotal
  24. 0024exact hseeds_left
  25. 0025refl
  26. 0026have htwo_four : exists pa_b_hj32_two_four_exact pa_c_hj32_two_four_exact. ((forall pa_i_hj32_two_four_exact_repeat. (exists pa_lt_hj32_two_four_exact_repeat_bound. pa_lt_hj32_two_four_exact_repeat_bound + S pa_i_hj32_two_four_exact_repeat = 4) -> (((exists pa_h_hj32_two_four_exact_repeat_decoded. pa_h_hj32_two_four_exact_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_four_exact_repeat)) * pa_c_hj32_two_four_exact)) /\ exists pa_q_hj32_two_four_exact_repeat_decoded. pa_b_hj32_two_four_exact = pa_q_hj32_two_four_exact_repeat_decoded * S ((S (pa_i_hj32_two_four_exact_repeat)) * pa_c_hj32_two_four_exact) + (2)))) /\ (exists pa_u_hj32_two_four_exact_product pa_v_hj32_two_four_exact_product. ((((exists pa_h_hj32_two_four_exact_product_start. pa_h_hj32_two_four_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_four_exact_product)) /\ exists pa_q_hj32_two_four_exact_product_start. pa_u_hj32_two_four_exact_product = pa_q_hj32_two_four_exact_product_start * S ((S (0)) * pa_v_hj32_two_four_exact_product) + (1))) /\ ((((exists pa_h_hj32_two_four_exact_product_terminal. pa_h_hj32_two_four_exact_product_terminal + S ((4 * 2) * 2) = S ((S (4)) * pa_v_hj32_two_four_exact_product)) /\ exists pa_q_hj32_two_four_exact_product_terminal. pa_u_hj32_two_four_exact_product = pa_q_hj32_two_four_exact_product_terminal * S ((S (4)) * pa_v_hj32_two_four_exact_product) + ((4 * 2) * 2))) /\ forall pa_i_hj32_two_four_exact_product. (exists pa_lt_hj32_two_four_exact_product_bound. pa_lt_hj32_two_four_exact_product_bound + S pa_i_hj32_two_four_exact_product = 4) -> exists pa_p_hj32_two_four_exact_product pa_r_hj32_two_four_exact_product pa_s_hj32_two_four_exact_product. ((((exists pa_h_hj32_two_four_exact_product_factor. pa_h_hj32_two_four_exact_product_factor + S (pa_p_hj32_two_four_exact_product) = S ((S (pa_i_hj32_two_four_exact_product)) * pa_c_hj32_two_four_exact)) /\ exists pa_q_hj32_two_four_exact_product_factor. pa_b_hj32_two_four_exact = pa_q_hj32_two_four_exact_product_factor * S ((S (pa_i_hj32_two_four_exact_product)) * pa_c_hj32_two_four_exact) + (pa_p_hj32_two_four_exact_product))) /\ ((((exists pa_h_hj32_two_four_exact_product_partial. pa_h_hj32_two_four_exact_product_partial + S (pa_r_hj32_two_four_exact_product) = S ((S (pa_i_hj32_two_four_exact_product)) * pa_v_hj32_two_four_exact_product)) /\ exists pa_q_hj32_two_four_exact_product_partial. pa_u_hj32_two_four_exact_product = pa_q_hj32_two_four_exact_product_partial * S ((S (pa_i_hj32_two_four_exact_product)) * pa_v_hj32_two_four_exact_product) + (pa_r_hj32_two_four_exact_product))) /\ ((((exists pa_h_hj32_two_four_exact_product_successor. pa_h_hj32_two_four_exact_product_successor + S (pa_s_hj32_two_four_exact_product) = S ((S (S pa_i_hj32_two_four_exact_product)) * pa_v_hj32_two_four_exact_product)) /\ exists pa_q_hj32_two_four_exact_product_successor. pa_u_hj32_two_four_exact_product = pa_q_hj32_two_four_exact_product_successor * S ((S (S pa_i_hj32_two_four_exact_product)) * pa_v_hj32_two_four_exact_product) + (pa_s_hj32_two_four_exact_product))) /\ pa_s_hj32_two_four_exact_product = pa_r_hj32_two_four_exact_product * pa_p_hj32_two_four_exact_product)))))))
  27. 0027specialize pow_successor_compose_from_total 2
  28. 0028specialize pow_successor_compose_from_total 3
  29. 0029specialize pow_successor_compose_from_total (4 * 2)
  30. 0030specialize pow_successor_compose_from_total ((4 * 2) * 2)
  31. 0031apply pow_successor_compose_from_total
  32. 0032exact htotal
  33. 0033exact htwo_three
  34. 0034refl
  35. 0035have htwo_five : exists pa_b_hj32_two_five_exact pa_c_hj32_two_five_exact. ((forall pa_i_hj32_two_five_exact_repeat. (exists pa_lt_hj32_two_five_exact_repeat_bound. pa_lt_hj32_two_five_exact_repeat_bound + S pa_i_hj32_two_five_exact_repeat = 5) -> (((exists pa_h_hj32_two_five_exact_repeat_decoded. pa_h_hj32_two_five_exact_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_five_exact_repeat)) * pa_c_hj32_two_five_exact)) /\ exists pa_q_hj32_two_five_exact_repeat_decoded. pa_b_hj32_two_five_exact = pa_q_hj32_two_five_exact_repeat_decoded * S ((S (pa_i_hj32_two_five_exact_repeat)) * pa_c_hj32_two_five_exact) + (2)))) /\ (exists pa_u_hj32_two_five_exact_product pa_v_hj32_two_five_exact_product. ((((exists pa_h_hj32_two_five_exact_product_start. pa_h_hj32_two_five_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_five_exact_product)) /\ exists pa_q_hj32_two_five_exact_product_start. pa_u_hj32_two_five_exact_product = pa_q_hj32_two_five_exact_product_start * S ((S (0)) * pa_v_hj32_two_five_exact_product) + (1))) /\ ((((exists pa_h_hj32_two_five_exact_product_terminal. pa_h_hj32_two_five_exact_product_terminal + S (((4 * 2) * 2) * 2) = S ((S (5)) * pa_v_hj32_two_five_exact_product)) /\ exists pa_q_hj32_two_five_exact_product_terminal. pa_u_hj32_two_five_exact_product = pa_q_hj32_two_five_exact_product_terminal * S ((S (5)) * pa_v_hj32_two_five_exact_product) + (((4 * 2) * 2) * 2))) /\ forall pa_i_hj32_two_five_exact_product. (exists pa_lt_hj32_two_five_exact_product_bound. pa_lt_hj32_two_five_exact_product_bound + S pa_i_hj32_two_five_exact_product = 5) -> exists pa_p_hj32_two_five_exact_product pa_r_hj32_two_five_exact_product pa_s_hj32_two_five_exact_product. ((((exists pa_h_hj32_two_five_exact_product_factor. pa_h_hj32_two_five_exact_product_factor + S (pa_p_hj32_two_five_exact_product) = S ((S (pa_i_hj32_two_five_exact_product)) * pa_c_hj32_two_five_exact)) /\ exists pa_q_hj32_two_five_exact_product_factor. pa_b_hj32_two_five_exact = pa_q_hj32_two_five_exact_product_factor * S ((S (pa_i_hj32_two_five_exact_product)) * pa_c_hj32_two_five_exact) + (pa_p_hj32_two_five_exact_product))) /\ ((((exists pa_h_hj32_two_five_exact_product_partial. pa_h_hj32_two_five_exact_product_partial + S (pa_r_hj32_two_five_exact_product) = S ((S (pa_i_hj32_two_five_exact_product)) * pa_v_hj32_two_five_exact_product)) /\ exists pa_q_hj32_two_five_exact_product_partial. pa_u_hj32_two_five_exact_product = pa_q_hj32_two_five_exact_product_partial * S ((S (pa_i_hj32_two_five_exact_product)) * pa_v_hj32_two_five_exact_product) + (pa_r_hj32_two_five_exact_product))) /\ ((((exists pa_h_hj32_two_five_exact_product_successor. pa_h_hj32_two_five_exact_product_successor + S (pa_s_hj32_two_five_exact_product) = S ((S (S pa_i_hj32_two_five_exact_product)) * pa_v_hj32_two_five_exact_product)) /\ exists pa_q_hj32_two_five_exact_product_successor. pa_u_hj32_two_five_exact_product = pa_q_hj32_two_five_exact_product_successor * S ((S (S pa_i_hj32_two_five_exact_product)) * pa_v_hj32_two_five_exact_product) + (pa_s_hj32_two_five_exact_product))) /\ pa_s_hj32_two_five_exact_product = pa_r_hj32_two_five_exact_product * pa_p_hj32_two_five_exact_product)))))))
  36. 0036specialize pow_successor_compose_from_total 2
  37. 0037specialize pow_successor_compose_from_total 4
  38. 0038specialize pow_successor_compose_from_total ((4 * 2) * 2)
  39. 0039specialize pow_successor_compose_from_total (((4 * 2) * 2) * 2)
  40. 0040apply pow_successor_compose_from_total
  41. 0041exact htotal
  42. 0042exact htwo_four
  43. 0043refl
  44. 0044have htwo_six : exists pa_b_hj32_two_six_exact pa_c_hj32_two_six_exact. ((forall pa_i_hj32_two_six_exact_repeat. (exists pa_lt_hj32_two_six_exact_repeat_bound. pa_lt_hj32_two_six_exact_repeat_bound + S pa_i_hj32_two_six_exact_repeat = 6) -> (((exists pa_h_hj32_two_six_exact_repeat_decoded. pa_h_hj32_two_six_exact_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_six_exact_repeat)) * pa_c_hj32_two_six_exact)) /\ exists pa_q_hj32_two_six_exact_repeat_decoded. pa_b_hj32_two_six_exact = pa_q_hj32_two_six_exact_repeat_decoded * S ((S (pa_i_hj32_two_six_exact_repeat)) * pa_c_hj32_two_six_exact) + (2)))) /\ (exists pa_u_hj32_two_six_exact_product pa_v_hj32_two_six_exact_product. ((((exists pa_h_hj32_two_six_exact_product_start. pa_h_hj32_two_six_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_six_exact_product)) /\ exists pa_q_hj32_two_six_exact_product_start. pa_u_hj32_two_six_exact_product = pa_q_hj32_two_six_exact_product_start * S ((S (0)) * pa_v_hj32_two_six_exact_product) + (1))) /\ ((((exists pa_h_hj32_two_six_exact_product_terminal. pa_h_hj32_two_six_exact_product_terminal + S ((((4 * 2) * 2) * 2) * 2) = S ((S (6)) * pa_v_hj32_two_six_exact_product)) /\ exists pa_q_hj32_two_six_exact_product_terminal. pa_u_hj32_two_six_exact_product = pa_q_hj32_two_six_exact_product_terminal * S ((S (6)) * pa_v_hj32_two_six_exact_product) + ((((4 * 2) * 2) * 2) * 2))) /\ forall pa_i_hj32_two_six_exact_product. (exists pa_lt_hj32_two_six_exact_product_bound. pa_lt_hj32_two_six_exact_product_bound + S pa_i_hj32_two_six_exact_product = 6) -> exists pa_p_hj32_two_six_exact_product pa_r_hj32_two_six_exact_product pa_s_hj32_two_six_exact_product. ((((exists pa_h_hj32_two_six_exact_product_factor. pa_h_hj32_two_six_exact_product_factor + S (pa_p_hj32_two_six_exact_product) = S ((S (pa_i_hj32_two_six_exact_product)) * pa_c_hj32_two_six_exact)) /\ exists pa_q_hj32_two_six_exact_product_factor. pa_b_hj32_two_six_exact = pa_q_hj32_two_six_exact_product_factor * S ((S (pa_i_hj32_two_six_exact_product)) * pa_c_hj32_two_six_exact) + (pa_p_hj32_two_six_exact_product))) /\ ((((exists pa_h_hj32_two_six_exact_product_partial. pa_h_hj32_two_six_exact_product_partial + S (pa_r_hj32_two_six_exact_product) = S ((S (pa_i_hj32_two_six_exact_product)) * pa_v_hj32_two_six_exact_product)) /\ exists pa_q_hj32_two_six_exact_product_partial. pa_u_hj32_two_six_exact_product = pa_q_hj32_two_six_exact_product_partial * S ((S (pa_i_hj32_two_six_exact_product)) * pa_v_hj32_two_six_exact_product) + (pa_r_hj32_two_six_exact_product))) /\ ((((exists pa_h_hj32_two_six_exact_product_successor. pa_h_hj32_two_six_exact_product_successor + S (pa_s_hj32_two_six_exact_product) = S ((S (S pa_i_hj32_two_six_exact_product)) * pa_v_hj32_two_six_exact_product)) /\ exists pa_q_hj32_two_six_exact_product_successor. pa_u_hj32_two_six_exact_product = pa_q_hj32_two_six_exact_product_successor * S ((S (S pa_i_hj32_two_six_exact_product)) * pa_v_hj32_two_six_exact_product) + (pa_s_hj32_two_six_exact_product))) /\ pa_s_hj32_two_six_exact_product = pa_r_hj32_two_six_exact_product * pa_p_hj32_two_six_exact_product)))))))
  45. 0045specialize pow_successor_compose_from_total 2
  46. 0046specialize pow_successor_compose_from_total 5
  47. 0047specialize pow_successor_compose_from_total (((4 * 2) * 2) * 2)
  48. 0048specialize pow_successor_compose_from_total ((((4 * 2) * 2) * 2) * 2)
  49. 0049apply pow_successor_compose_from_total
  50. 0050exact htotal
  51. 0051exact htwo_five
  52. 0052refl
  53. 0053have htwo_seven : exists pa_b_hj32_two_seven_exact pa_c_hj32_two_seven_exact. ((forall pa_i_hj32_two_seven_exact_repeat. (exists pa_lt_hj32_two_seven_exact_repeat_bound. pa_lt_hj32_two_seven_exact_repeat_bound + S pa_i_hj32_two_seven_exact_repeat = 7) -> (((exists pa_h_hj32_two_seven_exact_repeat_decoded. pa_h_hj32_two_seven_exact_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_seven_exact_repeat)) * pa_c_hj32_two_seven_exact)) /\ exists pa_q_hj32_two_seven_exact_repeat_decoded. pa_b_hj32_two_seven_exact = pa_q_hj32_two_seven_exact_repeat_decoded * S ((S (pa_i_hj32_two_seven_exact_repeat)) * pa_c_hj32_two_seven_exact) + (2)))) /\ (exists pa_u_hj32_two_seven_exact_product pa_v_hj32_two_seven_exact_product. ((((exists pa_h_hj32_two_seven_exact_product_start. pa_h_hj32_two_seven_exact_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_seven_exact_product)) /\ exists pa_q_hj32_two_seven_exact_product_start. pa_u_hj32_two_seven_exact_product = pa_q_hj32_two_seven_exact_product_start * S ((S (0)) * pa_v_hj32_two_seven_exact_product) + (1))) /\ ((((exists pa_h_hj32_two_seven_exact_product_terminal. pa_h_hj32_two_seven_exact_product_terminal + S (((((4 * 2) * 2) * 2) * 2) * 2) = S ((S (7)) * pa_v_hj32_two_seven_exact_product)) /\ exists pa_q_hj32_two_seven_exact_product_terminal. pa_u_hj32_two_seven_exact_product = pa_q_hj32_two_seven_exact_product_terminal * S ((S (7)) * pa_v_hj32_two_seven_exact_product) + (((((4 * 2) * 2) * 2) * 2) * 2))) /\ forall pa_i_hj32_two_seven_exact_product. (exists pa_lt_hj32_two_seven_exact_product_bound. pa_lt_hj32_two_seven_exact_product_bound + S pa_i_hj32_two_seven_exact_product = 7) -> exists pa_p_hj32_two_seven_exact_product pa_r_hj32_two_seven_exact_product pa_s_hj32_two_seven_exact_product. ((((exists pa_h_hj32_two_seven_exact_product_factor. pa_h_hj32_two_seven_exact_product_factor + S (pa_p_hj32_two_seven_exact_product) = S ((S (pa_i_hj32_two_seven_exact_product)) * pa_c_hj32_two_seven_exact)) /\ exists pa_q_hj32_two_seven_exact_product_factor. pa_b_hj32_two_seven_exact = pa_q_hj32_two_seven_exact_product_factor * S ((S (pa_i_hj32_two_seven_exact_product)) * pa_c_hj32_two_seven_exact) + (pa_p_hj32_two_seven_exact_product))) /\ ((((exists pa_h_hj32_two_seven_exact_product_partial. pa_h_hj32_two_seven_exact_product_partial + S (pa_r_hj32_two_seven_exact_product) = S ((S (pa_i_hj32_two_seven_exact_product)) * pa_v_hj32_two_seven_exact_product)) /\ exists pa_q_hj32_two_seven_exact_product_partial. pa_u_hj32_two_seven_exact_product = pa_q_hj32_two_seven_exact_product_partial * S ((S (pa_i_hj32_two_seven_exact_product)) * pa_v_hj32_two_seven_exact_product) + (pa_r_hj32_two_seven_exact_product))) /\ ((((exists pa_h_hj32_two_seven_exact_product_successor. pa_h_hj32_two_seven_exact_product_successor + S (pa_s_hj32_two_seven_exact_product) = S ((S (S pa_i_hj32_two_seven_exact_product)) * pa_v_hj32_two_seven_exact_product)) /\ exists pa_q_hj32_two_seven_exact_product_successor. pa_u_hj32_two_seven_exact_product = pa_q_hj32_two_seven_exact_product_successor * S ((S (S pa_i_hj32_two_seven_exact_product)) * pa_v_hj32_two_seven_exact_product) + (pa_s_hj32_two_seven_exact_product))) /\ pa_s_hj32_two_seven_exact_product = pa_r_hj32_two_seven_exact_product * pa_p_hj32_two_seven_exact_product)))))))
  54. 0054specialize pow_successor_compose_from_total 2
  55. 0055specialize pow_successor_compose_from_total 6
  56. 0056specialize pow_successor_compose_from_total ((((4 * 2) * 2) * 2) * 2)
  57. 0057specialize pow_successor_compose_from_total (((((4 * 2) * 2) * 2) * 2) * 2)
  58. 0058apply pow_successor_compose_from_total
  59. 0059exact htotal
  60. 0060exact htwo_six
  61. 0061refl
  62. 0062have htwo_seven_product : ((((4 * 2) * 2) * 2) * 2) * 2 = (4 * 2) * ((4 * 2) * 2)
  63. 0063specialize pow_add 2
  64. 0064specialize pow_add 3
  65. 0065specialize pow_add 4
  66. 0066specialize pow_add 7
  67. 0067specialize pow_add (4 * 2)
  68. 0068specialize pow_add ((4 * 2) * 2)
  69. 0069specialize pow_add (((((4 * 2) * 2) * 2) * 2) * 2)
  70. 0070apply pow_add
  71. 0071norm_num
  72. 0072exact htwo_three
  73. 0073exact htwo_four
  74. 0074exact htwo_seven
  75. 0075have hy_value : y = ((((4 * 2) * 2) * 2) * 2) * 2
  76. 0076specialize pow_functional 2
  77. 0077specialize pow_functional 7
  78. 0078specialize pow_functional y
  79. 0079specialize pow_functional (((((4 * 2) * 2) * 2) * 2) * 2)
  80. 0080apply pow_functional
  81. 0081exact hy
  82. 0082exact htwo_seven
  83. 0083rewrite hx_square
  84. 0084rewrite hy_value
  85. 0085exists 7
  86. 0086rewrite htwo_seven_product
  87. 0087have heleven_split : 11 = (4 * 2) + 3
  88. 0088norm_num
  89. 0089rewrite heleven_split
  90. 0090specialize add_mul (4 * 2)
  91. 0091specialize add_mul 3
  92. 0092specialize add_mul 11
  93. 0093rewrite add_mul
  94. 0094have htwo_four_split : (4 * 2) * 2 = 11 + 5
  95. 0095norm_num
  96. 0096rewrite htwo_four_split
  97. 0097specialize mul_add (4 * 2)
  98. 0098specialize mul_add 11
  99. 0099specialize mul_add 5
  100. 0100rewrite mul_add
  101. 0101have hsmall_gap : 7 + 3 * 11 = (4 * 2) * 5
  102. 0102norm_num
  103. 0103trans (7 + (4 * 2) * 11) + 3 * 11
  104. 0104symm
  105. 0105specialize add_assoc 7
  106. 0106specialize add_assoc ((4 * 2) * 11)
  107. 0107specialize add_assoc (3 * 11)
  108. 0108apply add_assoc
  109. 0109trans ((4 * 2) * 11 + 7) + 3 * 11
  110. 0110congr
  111. 0111specialize add_comm 7
  112. 0112specialize add_comm ((4 * 2) * 11)
  113. 0113apply add_comm
  114. 0114refl
  115. 0115trans (4 * 2) * 11 + (7 + 3 * 11)
  116. 0116specialize add_assoc ((4 * 2) * 11)
  117. 0117specialize add_assoc 7
  118. 0118specialize add_assoc (3 * 11)
  119. 0119apply add_assoc
  120. 0120rewrite hsmall_gap
  121. 0121refl