BT00W5 · Bertrand theorem

pow_eleven_two_le_pow_two_seven_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ x. ∀ y. (∀ z. ∀ n. ∃ m. Pow(z,n,m)) → Pow(11,2,x) → Pow(2,7,y) → Le(x,y)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0020 Pow

4 occurrences

In local proof propositions

PD0020 Pow

7 occurrences

Exact expanded native-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))

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

121 script commands · 21 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (9)
pow twopow two seed bundle from totalpow successor compose from totalpow functionalpow addadd mulmul addadd assocadd comm
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro x
  2. L2
    intro y
  3. L3
    intro htotal
  4. L4
    intro hx
  5. L5
    intro hy
02Establish hx_squareL6–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two.

  1. L6
    have hx_square : x = 11 * 11
  2. L7
    specialize pow_two 11
  3. L8
    specialize pow_two 2
  4. L9
    specialize pow_two x
  5. L10
    apply pow_two
  6. L11
    refl
  7. L12
    exact hx
03Establish hseedsL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two seed bundle from total.

  1. L13
    have hseeds : Pow(2,2,4) ∧ Pow(2,7,128)Definitions: Pow(2,2,4)Pow(2,7,128)Original native command in the exact edition
  2. L14
    apply pow_two_seed_bundle_from_total
  3. L15
    exact htotal
04Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hseeds
05Establish htwo_threeL17–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.

  1. L17
    have htwo_three : Pow(2,3,4 · 2)Definitions: Pow(2,3,4 · 2)Original native command in the exact edition
  2. L18
    specialize pow_successor_compose_from_total 2
  3. L19
    specialize pow_successor_compose_from_total 2
  4. L20
    specialize pow_successor_compose_from_total 4
  5. L21
    specialize pow_successor_compose_from_total (4 * 2)
  6. L22
    apply pow_successor_compose_from_total
  7. L23
    exact htotal
  8. L24
    exact hseeds_left
  9. L25
    refl
06Establish htwo_fourL26–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.

  1. L26
    have htwo_four : Pow(2,4,4 · 2 · 2)Definitions: Pow(2,4,4 · 2 · 2)Original native command in the exact edition
  2. L27
    specialize pow_successor_compose_from_total 2
  3. L28
    specialize pow_successor_compose_from_total 3
  4. L29
    specialize pow_successor_compose_from_total (4 * 2)
  5. L30
    specialize pow_successor_compose_from_total ((4 * 2) * 2)
  6. L31
    apply pow_successor_compose_from_total
  7. L32
    exact htotal
  8. L33
    exact htwo_three
  9. L34
    refl
07Establish htwo_fiveL35–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.

  1. L35
    have htwo_five : Pow(2,5,4 · 2 · 2 · 2)Definitions: Pow(2,5,4 · 2 · 2 · 2)Original native command in the exact edition
  2. L36
    specialize pow_successor_compose_from_total 2
  3. L37
    specialize pow_successor_compose_from_total 4
  4. L38
    specialize pow_successor_compose_from_total ((4 * 2) * 2)
  5. L39
    specialize pow_successor_compose_from_total (((4 * 2) * 2) * 2)
  6. L40
    apply pow_successor_compose_from_total
  7. L41
    exact htotal
  8. L42
    exact htwo_four
  9. L43
    refl
08Establish htwo_sixL44–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.

  1. L44
    have htwo_six : Pow(2,6,4 · 2 · 2 · 2 · 2)Definitions: Pow(2,6,4 · 2 · 2 · 2 · 2)Original native command in the exact edition
  2. L45
    specialize pow_successor_compose_from_total 2
  3. L46
    specialize pow_successor_compose_from_total 5
  4. L47
    specialize pow_successor_compose_from_total (((4 * 2) * 2) * 2)
  5. L48
    specialize pow_successor_compose_from_total ((((4 * 2) * 2) * 2) * 2)
  6. L49
    apply pow_successor_compose_from_total
  7. L50
    exact htotal
  8. L51
    exact htwo_five
  9. L52
    refl
09Establish htwo_sevenL53–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.

  1. L53
    have htwo_seven : Pow(2,7,4 · 2 · 2 · 2 · 2 · 2)Definitions: Pow(2,7,4 · 2 · 2 · 2 · 2 · 2)Original native command in the exact edition
  2. L54
    specialize pow_successor_compose_from_total 2
  3. L55
    specialize pow_successor_compose_from_total 6
  4. L56
    specialize pow_successor_compose_from_total ((((4 * 2) * 2) * 2) * 2)
  5. L57
    specialize pow_successor_compose_from_total (((((4 * 2) * 2) * 2) * 2) * 2)
  6. L58
    apply pow_successor_compose_from_total
  7. L59
    exact htotal
  8. L60
    exact htwo_six
  9. L61
    refl
10Establish htwo_seven_productL62–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.

  1. L62
    have htwo_seven_product : ((((4 * 2) * 2) * 2) * 2) * 2 = (4 * 2) * ((4 * 2) * 2)
  2. L63
    specialize pow_add 2
  3. L64
    specialize pow_add 3
  4. L65
    specialize pow_add 4
  5. L66
    specialize pow_add 7
  6. L67
    specialize pow_add (4 * 2)
  7. L68
    specialize pow_add ((4 * 2) * 2)
  8. L69
    specialize pow_add (((((4 * 2) * 2) * 2) * 2) * 2)
  9. L70
    apply pow_add
  10. L71
    norm_num
11Use earlier factsL72–74

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L72
    exact htwo_three
  2. L73
    exact htwo_four
  3. L74
    exact htwo_seven
12Establish hy_valueL75–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow functional.

  1. L75
    have hy_value : y = ((((4 * 2) * 2) * 2) * 2) * 2
  2. L76
    specialize pow_functional 2
  3. L77
    specialize pow_functional 7
  4. L78
    specialize pow_functional y
  5. L79
    specialize pow_functional (((((4 * 2) * 2) * 2) * 2) * 2)
  6. L80
    apply pow_functional
  7. L81
    exact hy
  8. L82
    exact htwo_seven
  9. L83
    rewrite hx_square
  10. L84
    rewrite hy_value
13Construct an explicit witnessL85–85

Supply the displayed value, then prove that it has the required property.

  1. L85
    exists 7
14Calculate and transport equalitiesL86–86

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L86
    rewrite htwo_seven_product
15Establish heleven_splitL87–93

Establish this local claim before using it. It is not an additional assumption.

  1. L87
    have heleven_split : 11 = (4 * 2) + 3
  2. L88
    norm_num
  3. L89
    rewrite heleven_split
  4. L90
    specialize add_mul (4 * 2)
  5. L91
    specialize add_mul 3
  6. L92
    specialize add_mul 11
  7. L93
    rewrite add_mul
16Establish htwo_four_splitL94–100

Establish this local claim before using it. It is not an additional assumption.

  1. L94
    have htwo_four_split : (4 * 2) * 2 = 11 + 5
  2. L95
    norm_num
  3. L96
    rewrite htwo_four_split
  4. L97
    specialize mul_add (4 * 2)
  5. L98
    specialize mul_add 11
  6. L99
    specialize mul_add 5
  7. L100
    rewrite mul_add
17Establish hsmall_gapL101–110

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L101
    have hsmall_gap : 7 + 3 * 11 = (4 * 2) * 5
  2. L102
    norm_num
  3. L103
    trans (7 + (4 * 2) * 11) + 3 * 11
  4. L104
    symm
  5. L105
    specialize add_assoc 7
  6. L106
    specialize add_assoc ((4 * 2) * 11)
  7. L107
    specialize add_assoc (3 * 11)
  8. L108
    apply add_assoc
  9. L109
    trans ((4 * 2) * 11 + 7) + 3 * 11
  10. L110
    congr
18Use earlier factsL111–113

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L111
    specialize add_comm 7
  2. L112
    specialize add_comm ((4 * 2) * 11)
  3. L113
    apply add_comm
19Calculate and transport equalitiesL114–115

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L114
    refl
  2. L115
    trans (4 * 2) * 11 + (7 + 3 * 11)
20Use earlier factsL116–119

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L116
    specialize add_assoc ((4 * 2) * 11)
  2. L117
    specialize add_assoc 7
  3. L118
    specialize add_assoc (3 * 11)
  4. L119
    apply add_assoc
21Calculate and transport equalitiesL120–121

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L120
    rewrite hsmall_gap
  2. L121
    refl

Library-wide reading audit

Original defined command ledger · 121 lines
  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 : Pow(2,2,4) ∧ Pow(2,7,128)
    Exact native replay linehave 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 : Pow(2,3,4 · 2)
    Exact native replay linehave 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 : Pow(2,4,4 · 2 · 2)
    Exact native replay linehave 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 : Pow(2,5,4 · 2 · 2 · 2)
    Exact native replay linehave 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 : Pow(2,6,4 · 2 · 2 · 2 · 2)
    Exact native replay linehave 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 : Pow(2,7,4 · 2 · 2 · 2 · 2 · 2)
    Exact native replay linehave 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