BT00Q0

one_le_pow

Alpha body-checked · checked-use disabled

Every relational power of a base at least one is at least one.

Exact expanded PA statement

forall a e x. (exists bpg_gap_base. bpg_gap_base + (1) = (a)) -> (exists ff_b_bpg_value ff_c_bpg_value. ((forall ff_i_bpg_value_repeat. (exists ff_lt_bpg_value_repeat_bound. ff_lt_bpg_value_repeat_bound + S ff_i_bpg_value_repeat = e) -> (((exists ff_h_bpg_value_repeat_decoded. ff_h_bpg_value_repeat_decoded + S (a) = S ((S (ff_i_bpg_value_repeat)) * ff_c_bpg_value)) /\ exists ff_q_bpg_value_repeat_decoded. ff_b_bpg_value = ff_q_bpg_value_repeat_decoded * S ((S (ff_i_bpg_value_repeat)) * ff_c_bpg_value) + (a)))) /\ (exists ff_u_bpg_value_product ff_v_bpg_value_product. ((((exists ff_h_bpg_value_product_start. ff_h_bpg_value_product_start + S (1) = S ((S (0)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_start. ff_u_bpg_value_product = ff_q_bpg_value_product_start * S ((S (0)) * ff_v_bpg_value_product) + (1))) /\ ((((exists ff_h_bpg_value_product_terminal. ff_h_bpg_value_product_terminal + S (x) = S ((S (e)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_terminal. ff_u_bpg_value_product = ff_q_bpg_value_product_terminal * S ((S (e)) * ff_v_bpg_value_product) + (x))) /\ forall ff_i_bpg_value_product. (exists ff_lt_bpg_value_product_bound. ff_lt_bpg_value_product_bound + S ff_i_bpg_value_product = e) -> exists ff_p_bpg_value_product ff_r_bpg_value_product ff_s_bpg_value_product. ((((exists ff_h_bpg_value_product_factor. ff_h_bpg_value_product_factor + S (ff_p_bpg_value_product) = S ((S (ff_i_bpg_value_product)) * ff_c_bpg_value)) /\ exists ff_q_bpg_value_product_factor. ff_b_bpg_value = ff_q_bpg_value_product_factor * S ((S (ff_i_bpg_value_product)) * ff_c_bpg_value) + (ff_p_bpg_value_product))) /\ ((((exists ff_h_bpg_value_product_partial. ff_h_bpg_value_product_partial + S (ff_r_bpg_value_product) = S ((S (ff_i_bpg_value_product)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_partial. ff_u_bpg_value_product = ff_q_bpg_value_product_partial * S ((S (ff_i_bpg_value_product)) * ff_v_bpg_value_product) + (ff_r_bpg_value_product))) /\ ((((exists ff_h_bpg_value_product_successor. ff_h_bpg_value_product_successor + S (ff_s_bpg_value_product) = S ((S (S ff_i_bpg_value_product)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_successor. ff_u_bpg_value_product = ff_q_bpg_value_product_successor * S ((S (S ff_i_bpg_value_product)) * ff_v_bpg_value_product) + (ff_s_bpg_value_product))) /\ ff_s_bpg_value_product = ff_r_bpg_value_product * ff_p_bpg_value_product)))))))) -> (exists bpg_gap_value. bpg_gap_value + (1) = (x))

Structural proof guide

Every relational power of a base at least one is at least one.

Direct prerequisites: pow_zero, pow_successor_decompose, le_refl, le_mul_of_one_le_right, le_trans. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT000E le_refl BT00PW le_mul_of_one_le_right BT000F le_trans

Direct dependents

BT00Q1 pow_nonzero_of_one_le BT00SN pow_exponent_monotone_from_total BT00XJ pow_le_pow_of_exponent_le

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro e
  3. 0003induction e
  4. 0004intro x
  5. 0005intro ha
  6. 0006intro hx
  7. 0007have hx1 : x = 1
  8. 0008specialize pow_zero a
  9. 0009specialize pow_zero 0
  10. 0010specialize pow_zero x
  11. 0011apply pow_zero
  12. 0012refl
  13. 0013exact hx
  14. 0014rewrite hx1
  15. 0015specialize le_refl 1
  16. 0016exact le_refl
  17. 0017intro x
  18. 0018intro ha
  19. 0019intro hx
  20. 0020have hstep : exists r. (exists ff_b_bpg_prefix ff_c_bpg_prefix. ((forall ff_i_bpg_prefix_repeat. (exists ff_lt_bpg_prefix_repeat_bound. ff_lt_bpg_prefix_repeat_bound + S ff_i_bpg_prefix_repeat = e) -> (((exists ff_h_bpg_prefix_repeat_decoded. ff_h_bpg_prefix_repeat_decoded + S (a) = S ((S (ff_i_bpg_prefix_repeat)) * ff_c_bpg_prefix)) /\ exists ff_q_bpg_prefix_repeat_decoded. ff_b_bpg_prefix = ff_q_bpg_prefix_repeat_decoded * S ((S (ff_i_bpg_prefix_repeat)) * ff_c_bpg_prefix) + (a)))) /\ (exists ff_u_bpg_prefix_product ff_v_bpg_prefix_product. ((((exists ff_h_bpg_prefix_product_start. ff_h_bpg_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_start. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_start * S ((S (0)) * ff_v_bpg_prefix_product) + (1))) /\ ((((exists ff_h_bpg_prefix_product_terminal. ff_h_bpg_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_terminal. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_terminal * S ((S (e)) * ff_v_bpg_prefix_product) + (r))) /\ forall ff_i_bpg_prefix_product. (exists ff_lt_bpg_prefix_product_bound. ff_lt_bpg_prefix_product_bound + S ff_i_bpg_prefix_product = e) -> exists ff_p_bpg_prefix_product ff_r_bpg_prefix_product ff_s_bpg_prefix_product. ((((exists ff_h_bpg_prefix_product_factor. ff_h_bpg_prefix_product_factor + S (ff_p_bpg_prefix_product) = S ((S (ff_i_bpg_prefix_product)) * ff_c_bpg_prefix)) /\ exists ff_q_bpg_prefix_product_factor. ff_b_bpg_prefix = ff_q_bpg_prefix_product_factor * S ((S (ff_i_bpg_prefix_product)) * ff_c_bpg_prefix) + (ff_p_bpg_prefix_product))) /\ ((((exists ff_h_bpg_prefix_product_partial. ff_h_bpg_prefix_product_partial + S (ff_r_bpg_prefix_product) = S ((S (ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_partial. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_partial * S ((S (ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product) + (ff_r_bpg_prefix_product))) /\ ((((exists ff_h_bpg_prefix_product_successor. ff_h_bpg_prefix_product_successor + S (ff_s_bpg_prefix_product) = S ((S (S ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_successor. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_successor * S ((S (S ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product) + (ff_s_bpg_prefix_product))) /\ ff_s_bpg_prefix_product = ff_r_bpg_prefix_product * ff_p_bpg_prefix_product)))))))) /\ x = r * a
  21. 0021specialize pow_successor_decompose a
  22. 0022specialize pow_successor_decompose e
  23. 0023specialize pow_successor_decompose (S e)
  24. 0024specialize pow_successor_decompose x
  25. 0025apply pow_successor_decompose
  26. 0026refl
  27. 0027exact hx
  28. 0028cases hstep
  29. 0029cases hstep_witness
  30. 0030have hr : exists k. k + 1 = x1
  31. 0031specialize IH x1
  32. 0032apply IH
  33. 0033exact ha
  34. 0034exact hstep_witness_left
  35. 0035have hrproduct : exists k. k + x1 = x1 * a
  36. 0036specialize le_mul_of_one_le_right x1
  37. 0037specialize le_mul_of_one_le_right a
  38. 0038apply le_mul_of_one_le_right
  39. 0039exact ha
  40. 0040rewrite hstep_witness_right
  41. 0041specialize le_trans 1
  42. 0042specialize le_trans x1
  43. 0043specialize le_trans (x1 * a)
  44. 0044apply le_trans
  45. 0045exact hr
  46. 0046exact hrproduct