BT00TX · Bertrand theorem

choose_factorial_bridge

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

Complementary factorials represent each constructive Choose value.

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

∀ n. ∀ k. ∀ j. ∀ c. ∀ F. ∀ K. ∀ J. k + j = n → Choose(n,k,c) → Factorial(n,F) → Factorial(k,K) → Factorial(j,J) → F = K · J · c

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

PD0023 Factorial PD0041 Choose

4 occurrences

In local proof propositions

PD0023 Factorial PD0041 Choose

3 occurrences

Exact expanded native-PA statement
forall n k j c F K J. k + j = n -> (((exists bcf_lt_gap_bcfb_choose_out_of_range. bcf_lt_gap_bcfb_choose_out_of_range + S (n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bcfb_choose_in_range. bcf_le_gap_bcfb_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bcfb_choose bcf_row_code_scale_bcfb_choose bcf_row_scale_code_bcfb_choose bcf_row_scale_scale_bcfb_choose bcf_row_code_bcfb_choose bcf_row_scale_bcfb_choose. ((forall bcf_row_index_bcfb_choose_table. (exists bcf_lt_gap_bcfb_choose_table_row_bound. bcf_lt_gap_bcfb_choose_table_row_bound + S (bcf_row_index_bcfb_choose_table) = S (n)) -> exists bcf_row_code_bcfb_choose_table bcf_row_scale_bcfb_choose_table. ((((exists bcf_height_bcfb_choose_table_decoded_row_code. bcf_height_bcfb_choose_table_decoded_row_code + S (bcf_row_code_bcfb_choose_table) = S ((S (bcf_row_index_bcfb_choose_table)) * bcf_row_code_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_table_decoded_row_code. bcf_row_code_code_bcfb_choose = bcf_quotient_bcfb_choose_table_decoded_row_code * S ((S (bcf_row_index_bcfb_choose_table)) * bcf_row_code_scale_bcfb_choose) + (bcf_row_code_bcfb_choose_table))) /\ ((((exists bcf_height_bcfb_choose_table_decoded_row_scale. bcf_height_bcfb_choose_table_decoded_row_scale + S (bcf_row_scale_bcfb_choose_table) = S ((S (bcf_row_index_bcfb_choose_table)) * bcf_row_scale_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_table_decoded_row_scale. bcf_row_scale_code_bcfb_choose = bcf_quotient_bcfb_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcfb_choose_table)) * bcf_row_scale_scale_bcfb_choose) + (bcf_row_scale_bcfb_choose_table))) /\ ((bcf_row_index_bcfb_choose_table = 0 /\ (forall bcf_index_bcfb_choose_table_zero_row. (exists bcf_lt_gap_bcfb_choose_table_zero_row_bound. bcf_lt_gap_bcfb_choose_table_zero_row_bound + S (bcf_index_bcfb_choose_table_zero_row) = S (n)) -> exists bcf_value_bcfb_choose_table_zero_row. ((((exists bcf_height_bcfb_choose_table_zero_row_entry. bcf_height_bcfb_choose_table_zero_row_entry + S (bcf_value_bcfb_choose_table_zero_row) = S ((S (bcf_index_bcfb_choose_table_zero_row)) * bcf_row_scale_bcfb_choose_table)) /\ exists bcf_quotient_bcfb_choose_table_zero_row_entry. bcf_row_code_bcfb_choose_table = bcf_quotient_bcfb_choose_table_zero_row_entry * S ((S (bcf_index_bcfb_choose_table_zero_row)) * bcf_row_scale_bcfb_choose_table) + (bcf_value_bcfb_choose_table_zero_row))) /\ ((bcf_index_bcfb_choose_table_zero_row = 0 /\ bcf_value_bcfb_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcfb_choose_table_zero_row. bcf_index_bcfb_choose_table_zero_row = S bcf_predecessor_bcfb_choose_table_zero_row /\ bcf_value_bcfb_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcfb_choose_table bcf_previous_code_bcfb_choose_table bcf_previous_scale_bcfb_choose_table. bcf_row_index_bcfb_choose_table = S bcf_predecessor_bcfb_choose_table /\ ((((exists bcf_height_bcfb_choose_table_decoded_previous_code. bcf_height_bcfb_choose_table_decoded_previous_code + S (bcf_previous_code_bcfb_choose_table) = S ((S (bcf_predecessor_bcfb_choose_table)) * bcf_row_code_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_table_decoded_previous_code. bcf_row_code_code_bcfb_choose = bcf_quotient_bcfb_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcfb_choose_table)) * bcf_row_code_scale_bcfb_choose) + (bcf_previous_code_bcfb_choose_table))) /\ ((((exists bcf_height_bcfb_choose_table_decoded_previous_scale. bcf_height_bcfb_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcfb_choose_table) = S ((S (bcf_predecessor_bcfb_choose_table)) * bcf_row_scale_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_table_decoded_previous_scale. bcf_row_scale_code_bcfb_choose = bcf_quotient_bcfb_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcfb_choose_table)) * bcf_row_scale_scale_bcfb_choose) + (bcf_previous_scale_bcfb_choose_table))) /\ (forall bcf_index_bcfb_choose_table_row_step. (exists bcf_lt_gap_bcfb_choose_table_row_step_bound. bcf_lt_gap_bcfb_choose_table_row_step_bound + S (bcf_index_bcfb_choose_table_row_step) = S (n)) -> exists bcf_value_bcfb_choose_table_row_step. ((((exists bcf_height_bcfb_choose_table_row_step_entry. bcf_height_bcfb_choose_table_row_step_entry + S (bcf_value_bcfb_choose_table_row_step) = S ((S (bcf_index_bcfb_choose_table_row_step)) * bcf_row_scale_bcfb_choose_table)) /\ exists bcf_quotient_bcfb_choose_table_row_step_entry. bcf_row_code_bcfb_choose_table = bcf_quotient_bcfb_choose_table_row_step_entry * S ((S (bcf_index_bcfb_choose_table_row_step)) * bcf_row_scale_bcfb_choose_table) + (bcf_value_bcfb_choose_table_row_step))) /\ ((bcf_index_bcfb_choose_table_row_step = 0 /\ bcf_value_bcfb_choose_table_row_step = 1) \/ exists bcf_predecessor_bcfb_choose_table_row_step bcf_left_bcfb_choose_table_row_step bcf_right_bcfb_choose_table_row_step. bcf_index_bcfb_choose_table_row_step = S bcf_predecessor_bcfb_choose_table_row_step /\ ((((exists bcf_height_bcfb_choose_table_row_step_previous_left. bcf_height_bcfb_choose_table_row_step_previous_left + S (bcf_left_bcfb_choose_table_row_step) = S ((S (bcf_predecessor_bcfb_choose_table_row_step)) * bcf_previous_scale_bcfb_choose_table)) /\ exists bcf_quotient_bcfb_choose_table_row_step_previous_left. bcf_previous_code_bcfb_choose_table = bcf_quotient_bcfb_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcfb_choose_table_row_step)) * bcf_previous_scale_bcfb_choose_table) + (bcf_left_bcfb_choose_table_row_step))) /\ ((((exists bcf_height_bcfb_choose_table_row_step_previous_right. bcf_height_bcfb_choose_table_row_step_previous_right + S (bcf_right_bcfb_choose_table_row_step) = S ((S (S (bcf_predecessor_bcfb_choose_table_row_step))) * bcf_previous_scale_bcfb_choose_table)) /\ exists bcf_quotient_bcfb_choose_table_row_step_previous_right. bcf_previous_code_bcfb_choose_table = bcf_quotient_bcfb_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcfb_choose_table_row_step))) * bcf_previous_scale_bcfb_choose_table) + (bcf_right_bcfb_choose_table_row_step))) /\ bcf_value_bcfb_choose_table_row_step = bcf_left_bcfb_choose_table_row_step + bcf_right_bcfb_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcfb_choose_decoded_row_code. bcf_height_bcfb_choose_decoded_row_code + S (bcf_row_code_bcfb_choose) = S ((S (n)) * bcf_row_code_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_decoded_row_code. bcf_row_code_code_bcfb_choose = bcf_quotient_bcfb_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcfb_choose) + (bcf_row_code_bcfb_choose))) /\ ((((exists bcf_height_bcfb_choose_decoded_row_scale. bcf_height_bcfb_choose_decoded_row_scale + S (bcf_row_scale_bcfb_choose) = S ((S (n)) * bcf_row_scale_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_decoded_row_scale. bcf_row_scale_code_bcfb_choose = bcf_quotient_bcfb_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcfb_choose) + (bcf_row_scale_bcfb_choose))) /\ (((exists bcf_height_bcfb_choose_decoded_value. bcf_height_bcfb_choose_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bcfb_choose)) /\ exists bcf_quotient_bcfb_choose_decoded_value. bcf_row_code_bcfb_choose = bcf_quotient_bcfb_choose_decoded_value * S ((S (k)) * bcf_row_scale_bcfb_choose) + (c))))))))) -> (exists ff_b_bcfb_total ff_c_bcfb_total. ((forall ff_i_bcfb_total_range. (exists ff_lt_bcfb_total_range_bound. ff_lt_bcfb_total_range_bound + S ff_i_bcfb_total_range = n) -> (((exists ff_h_bcfb_total_range_decoded. ff_h_bcfb_total_range_decoded + S (1 + ff_i_bcfb_total_range) = S ((S (ff_i_bcfb_total_range)) * ff_c_bcfb_total)) /\ exists ff_q_bcfb_total_range_decoded. ff_b_bcfb_total = ff_q_bcfb_total_range_decoded * S ((S (ff_i_bcfb_total_range)) * ff_c_bcfb_total) + (1 + ff_i_bcfb_total_range)))) /\ (exists ff_u_bcfb_total_product ff_v_bcfb_total_product. ((((exists ff_h_bcfb_total_product_start. ff_h_bcfb_total_product_start + S (1) = S ((S (0)) * ff_v_bcfb_total_product)) /\ exists ff_q_bcfb_total_product_start. ff_u_bcfb_total_product = ff_q_bcfb_total_product_start * S ((S (0)) * ff_v_bcfb_total_product) + (1))) /\ ((((exists ff_h_bcfb_total_product_terminal. ff_h_bcfb_total_product_terminal + S (F) = S ((S (n)) * ff_v_bcfb_total_product)) /\ exists ff_q_bcfb_total_product_terminal. ff_u_bcfb_total_product = ff_q_bcfb_total_product_terminal * S ((S (n)) * ff_v_bcfb_total_product) + (F))) /\ forall ff_i_bcfb_total_product. (exists ff_lt_bcfb_total_product_bound. ff_lt_bcfb_total_product_bound + S ff_i_bcfb_total_product = n) -> exists ff_p_bcfb_total_product ff_r_bcfb_total_product ff_s_bcfb_total_product. ((((exists ff_h_bcfb_total_product_factor. ff_h_bcfb_total_product_factor + S (ff_p_bcfb_total_product) = S ((S (ff_i_bcfb_total_product)) * ff_c_bcfb_total)) /\ exists ff_q_bcfb_total_product_factor. ff_b_bcfb_total = ff_q_bcfb_total_product_factor * S ((S (ff_i_bcfb_total_product)) * ff_c_bcfb_total) + (ff_p_bcfb_total_product))) /\ ((((exists ff_h_bcfb_total_product_partial. ff_h_bcfb_total_product_partial + S (ff_r_bcfb_total_product) = S ((S (ff_i_bcfb_total_product)) * ff_v_bcfb_total_product)) /\ exists ff_q_bcfb_total_product_partial. ff_u_bcfb_total_product = ff_q_bcfb_total_product_partial * S ((S (ff_i_bcfb_total_product)) * ff_v_bcfb_total_product) + (ff_r_bcfb_total_product))) /\ ((((exists ff_h_bcfb_total_product_successor. ff_h_bcfb_total_product_successor + S (ff_s_bcfb_total_product) = S ((S (S ff_i_bcfb_total_product)) * ff_v_bcfb_total_product)) /\ exists ff_q_bcfb_total_product_successor. ff_u_bcfb_total_product = ff_q_bcfb_total_product_successor * S ((S (S ff_i_bcfb_total_product)) * ff_v_bcfb_total_product) + (ff_s_bcfb_total_product))) /\ ff_s_bcfb_total_product = ff_r_bcfb_total_product * ff_p_bcfb_total_product)))))))) -> (exists ff_b_bcfb_left ff_c_bcfb_left. ((forall ff_i_bcfb_left_range. (exists ff_lt_bcfb_left_range_bound. ff_lt_bcfb_left_range_bound + S ff_i_bcfb_left_range = k) -> (((exists ff_h_bcfb_left_range_decoded. ff_h_bcfb_left_range_decoded + S (1 + ff_i_bcfb_left_range) = S ((S (ff_i_bcfb_left_range)) * ff_c_bcfb_left)) /\ exists ff_q_bcfb_left_range_decoded. ff_b_bcfb_left = ff_q_bcfb_left_range_decoded * S ((S (ff_i_bcfb_left_range)) * ff_c_bcfb_left) + (1 + ff_i_bcfb_left_range)))) /\ (exists ff_u_bcfb_left_product ff_v_bcfb_left_product. ((((exists ff_h_bcfb_left_product_start. ff_h_bcfb_left_product_start + S (1) = S ((S (0)) * ff_v_bcfb_left_product)) /\ exists ff_q_bcfb_left_product_start. ff_u_bcfb_left_product = ff_q_bcfb_left_product_start * S ((S (0)) * ff_v_bcfb_left_product) + (1))) /\ ((((exists ff_h_bcfb_left_product_terminal. ff_h_bcfb_left_product_terminal + S (K) = S ((S (k)) * ff_v_bcfb_left_product)) /\ exists ff_q_bcfb_left_product_terminal. ff_u_bcfb_left_product = ff_q_bcfb_left_product_terminal * S ((S (k)) * ff_v_bcfb_left_product) + (K))) /\ forall ff_i_bcfb_left_product. (exists ff_lt_bcfb_left_product_bound. ff_lt_bcfb_left_product_bound + S ff_i_bcfb_left_product = k) -> exists ff_p_bcfb_left_product ff_r_bcfb_left_product ff_s_bcfb_left_product. ((((exists ff_h_bcfb_left_product_factor. ff_h_bcfb_left_product_factor + S (ff_p_bcfb_left_product) = S ((S (ff_i_bcfb_left_product)) * ff_c_bcfb_left)) /\ exists ff_q_bcfb_left_product_factor. ff_b_bcfb_left = ff_q_bcfb_left_product_factor * S ((S (ff_i_bcfb_left_product)) * ff_c_bcfb_left) + (ff_p_bcfb_left_product))) /\ ((((exists ff_h_bcfb_left_product_partial. ff_h_bcfb_left_product_partial + S (ff_r_bcfb_left_product) = S ((S (ff_i_bcfb_left_product)) * ff_v_bcfb_left_product)) /\ exists ff_q_bcfb_left_product_partial. ff_u_bcfb_left_product = ff_q_bcfb_left_product_partial * S ((S (ff_i_bcfb_left_product)) * ff_v_bcfb_left_product) + (ff_r_bcfb_left_product))) /\ ((((exists ff_h_bcfb_left_product_successor. ff_h_bcfb_left_product_successor + S (ff_s_bcfb_left_product) = S ((S (S ff_i_bcfb_left_product)) * ff_v_bcfb_left_product)) /\ exists ff_q_bcfb_left_product_successor. ff_u_bcfb_left_product = ff_q_bcfb_left_product_successor * S ((S (S ff_i_bcfb_left_product)) * ff_v_bcfb_left_product) + (ff_s_bcfb_left_product))) /\ ff_s_bcfb_left_product = ff_r_bcfb_left_product * ff_p_bcfb_left_product)))))))) -> (exists ff_b_bcfb_right ff_c_bcfb_right. ((forall ff_i_bcfb_right_range. (exists ff_lt_bcfb_right_range_bound. ff_lt_bcfb_right_range_bound + S ff_i_bcfb_right_range = j) -> (((exists ff_h_bcfb_right_range_decoded. ff_h_bcfb_right_range_decoded + S (1 + ff_i_bcfb_right_range) = S ((S (ff_i_bcfb_right_range)) * ff_c_bcfb_right)) /\ exists ff_q_bcfb_right_range_decoded. ff_b_bcfb_right = ff_q_bcfb_right_range_decoded * S ((S (ff_i_bcfb_right_range)) * ff_c_bcfb_right) + (1 + ff_i_bcfb_right_range)))) /\ (exists ff_u_bcfb_right_product ff_v_bcfb_right_product. ((((exists ff_h_bcfb_right_product_start. ff_h_bcfb_right_product_start + S (1) = S ((S (0)) * ff_v_bcfb_right_product)) /\ exists ff_q_bcfb_right_product_start. ff_u_bcfb_right_product = ff_q_bcfb_right_product_start * S ((S (0)) * ff_v_bcfb_right_product) + (1))) /\ ((((exists ff_h_bcfb_right_product_terminal. ff_h_bcfb_right_product_terminal + S (J) = S ((S (j)) * ff_v_bcfb_right_product)) /\ exists ff_q_bcfb_right_product_terminal. ff_u_bcfb_right_product = ff_q_bcfb_right_product_terminal * S ((S (j)) * ff_v_bcfb_right_product) + (J))) /\ forall ff_i_bcfb_right_product. (exists ff_lt_bcfb_right_product_bound. ff_lt_bcfb_right_product_bound + S ff_i_bcfb_right_product = j) -> exists ff_p_bcfb_right_product ff_r_bcfb_right_product ff_s_bcfb_right_product. ((((exists ff_h_bcfb_right_product_factor. ff_h_bcfb_right_product_factor + S (ff_p_bcfb_right_product) = S ((S (ff_i_bcfb_right_product)) * ff_c_bcfb_right)) /\ exists ff_q_bcfb_right_product_factor. ff_b_bcfb_right = ff_q_bcfb_right_product_factor * S ((S (ff_i_bcfb_right_product)) * ff_c_bcfb_right) + (ff_p_bcfb_right_product))) /\ ((((exists ff_h_bcfb_right_product_partial. ff_h_bcfb_right_product_partial + S (ff_r_bcfb_right_product) = S ((S (ff_i_bcfb_right_product)) * ff_v_bcfb_right_product)) /\ exists ff_q_bcfb_right_product_partial. ff_u_bcfb_right_product = ff_q_bcfb_right_product_partial * S ((S (ff_i_bcfb_right_product)) * ff_v_bcfb_right_product) + (ff_r_bcfb_right_product))) /\ ((((exists ff_h_bcfb_right_product_successor. ff_h_bcfb_right_product_successor + S (ff_s_bcfb_right_product) = S ((S (S ff_i_bcfb_right_product)) * ff_v_bcfb_right_product)) /\ exists ff_q_bcfb_right_product_successor. ff_u_bcfb_right_product = ff_q_bcfb_right_product_successor * S ((S (S ff_i_bcfb_right_product)) * ff_v_bcfb_right_product) + (ff_s_bcfb_right_product))) /\ ff_s_bcfb_right_product = ff_r_bcfb_right_product * ff_p_bcfb_right_product)))))))) -> F = (K * J) * c

Proof neighborhood

Direct theorem prerequisites

BT000A mul_one BT00T8 choose_exists BT00TK choose_self_of_eq BT00TT choose_weighted_vertical BT0090 factorial_functional BT0091 factorial_zero BT0092 factorial_succ_decompose BT00TV factorial_length_eq_transport BT00TW factorial_weighted_product_combine

Direct theorem dependents

BT00VC choose_prime_divides_between BT00VX central_binom_prime_divisor_le_double BT00XM central_binom_factorial_valuation_balance

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

182 script commands · 35 reading checkpoints · 15 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)
mul onechoose existschoose self of eqchoose weighted verticalfactorial functionalfactorial zerofactorial succ decomposefactorial length eq transportfactorial weighted product combine
01Induction on nL1–2

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction n
  2. L2
    intro k
02Induction on jL3–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction j
  2. L4
    intro c
  3. L5
    intro F
  4. L6
    intro K
  5. L7
    intro J
  6. L8
    intro hsum
  7. L9
    intro hchoose
  8. L10
    intro hF
  9. L11
    intro hK
  10. L12
    intro hJ
03Establish hkL13–17

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

  1. L13
    have hk : k = 0
  2. L14
    trans k + 0
  3. L15
    symm
  4. L16
    apply PA3
  5. L17
    exact hsum
04Establish hc_oneL18–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose self of eq.

  1. L18
    have hc_one : c = 1
  2. L19
    specialize choose_self_of_eq 0
  3. L20
    specialize choose_self_of_eq k
  4. L21
    specialize choose_self_of_eq c
  5. L22
    apply choose_self_of_eq
  6. L23
    exact hk
  7. L24
    exact hchoose
05Establish hF_oneL25–30

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

  1. L25
    have hF_one : F = 1
  2. L26
    specialize factorial_zero 0
  3. L27
    specialize factorial_zero F
  4. L28
    apply factorial_zero
  5. L29
    refl
  6. L30
    exact hF
06Establish hK_oneL31–36

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

  1. L31
    have hK_one : K = 1
  2. L32
    specialize factorial_zero k
  3. L33
    specialize factorial_zero K
  4. L34
    apply factorial_zero
  5. L35
    exact hk
  6. L36
    exact hK
07Establish hJ_oneL37–46

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

  1. L37
    have hJ_one : J = 1
  2. L38
    specialize factorial_zero 0
  3. L39
    specialize factorial_zero J
  4. L40
    apply factorial_zero
  5. L41
    refl
  6. L42
    exact hJ
  7. L43
    rewrite hF_one
  8. L44
    rewrite hK_one
  9. L45
    rewrite hJ_one
  10. L46
    rewrite hc_one
08Use earlier factsL47–47

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

  1. L47
    specialize mul_one 1
09Calculate and transport equalitiesL48–50

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

  1. L48
    rewrite mul_one
  2. L49
    rewrite mul_one
  3. L50
    refl
10Fix variables and assumptionsL51–55

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

  1. L51
    intro c
  2. L52
    intro F
  3. L53
    intro K
  4. L54
    intro J
  5. L55
    intro hsum
11Calculate and transport equalitiesL56–56

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

  1. L56
    rewrite PA4 at hsum
12Separate the logical casesL57–57

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

  1. L57
    exfalso
13Use earlier factsL58–59

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

  1. L58
    apply PA1
  2. L59
    exact hsum
14Fix variables and assumptionsL60–60

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

  1. L60
    intro k
15Induction on jL61–70

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L61
    induction j
  2. L62
    intro c
  3. L63
    intro F
  4. L64
    intro K
  5. L65
    intro J
  6. L66
    intro hsum
  7. L67
    intro hchoose
  8. L68
    intro hF
  9. L69
    intro hK
  10. L70
    intro hJ
16Establish hkL71–75

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

  1. L71
    have hk : k = S n
  2. L72
    trans k + 0
  3. L73
    symm
  4. L74
    apply PA3
  5. L75
    exact hsum
17Establish hc_oneL76–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose self of eq.

  1. L76
    have hc_one : c = 1
  2. L77
    specialize choose_self_of_eq (S n)
  3. L78
    specialize choose_self_of_eq k
  4. L79
    specialize choose_self_of_eq c
  5. L80
    apply choose_self_of_eq
  6. L81
    exact hk
  7. L82
    exact hchoose
18Establish hJ_oneL83–88

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

  1. L83
    have hJ_one : J = 1
  2. L84
    specialize factorial_zero 0
  3. L85
    specialize factorial_zero J
  4. L86
    apply factorial_zero
  5. L87
    refl
  6. L88
    exact hJ
19Establish hFKL89–98

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

  1. L89
    have hFK : F = K
  2. L90
    specialize factorial_functional (S n)
  3. L91
    specialize factorial_functional F
  4. L92
    specialize factorial_functional K
  5. L93
    apply factorial_functional
  6. L94
    exact hF
  7. L95
    specialize factorial_length_eq_transport k
  8. L96
    specialize factorial_length_eq_transport (S n)
  9. L97
    specialize factorial_length_eq_transport K
  10. L98
    apply factorial_length_eq_transport
20Use earlier factsL99–100

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

  1. L99
    exact hk
  2. L100
    exact hK
21Calculate and transport equalitiesL101–103

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

  1. L101
    rewrite hFK
  2. L102
    rewrite hJ_one
  3. L103
    rewrite hc_one
22Use earlier factsL104–104

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

  1. L104
    specialize mul_one K
23Calculate and transport equalitiesL105–107

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

  1. L105
    rewrite mul_one
  2. L106
    rewrite mul_one
  3. L107
    refl
24Fix variables and assumptionsL108–116

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

  1. L108
    intro c
  2. L109
    intro F
  3. L110
    intro K
  4. L111
    intro J
  5. L112
    intro hsum
  6. L113
    intro hchoose
  7. L114
    intro hF
  8. L115
    intro hK
  9. L116
    intro hJ
25Establish hprevious_sumL117–122

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

  1. L117
    have hprevious_sum : k + j = n
  2. L118
    apply PA2
  3. L119
    trans k + S j
  4. L120
    symm
  5. L121
    apply PA4
  6. L122
    exact hsum
26Establish ha_existsL123–126

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

  1. L123
    have ha_exists : ∃ a. Choose(n,k,a)Definitions: Choose(n,k,a)Original native command in the exact edition
  2. L124
    specialize choose_exists n
  3. L125
    specialize choose_exists k
  4. L126
    exact choose_exists
27Separate the logical casesL127–127

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

  1. L127
    cases ha_exists
28Establish hweightedL128–137

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose weighted vertical.

  1. L128
    have hweighted : S j * c = S n * x
  2. L129
    specialize choose_weighted_vertical n
  3. L130
    specialize choose_weighted_vertical k
  4. L131
    specialize choose_weighted_vertical j
  5. L132
    specialize choose_weighted_vertical x
  6. L133
    specialize choose_weighted_vertical c
  7. L134
    apply choose_weighted_vertical
  8. L135
    exact hprevious_sum
  9. L136
    exact ha_exists_witness
  10. L137
    exact hchoose
29Establish hF_decompL138–144

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial succ decompose.

  1. L138
    have hF_decomp : ∃ f. Factorial(n,f) ∧ F = f · S nDefinitions: Factorial(n,f)Original native command in the exact edition
  2. L139
    specialize factorial_succ_decompose n
  3. L140
    specialize factorial_succ_decompose (S n)
  4. L141
    specialize factorial_succ_decompose F
  5. L142
    apply factorial_succ_decompose
  6. L143
    refl
  7. L144
    exact hF
30Separate the logical casesL145–146

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

  1. L145
    cases hF_decomp
  2. L146
    cases hF_decomp_witness
31Establish hJ_decompL147–153

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial succ decompose.

  1. L147
    have hJ_decomp : ∃ r. Factorial(j,r) ∧ J = r · S jDefinitions: Factorial(j,r)Original native command in the exact edition
  2. L148
    specialize factorial_succ_decompose j
  3. L149
    specialize factorial_succ_decompose (S j)
  4. L150
    specialize factorial_succ_decompose J
  5. L151
    apply factorial_succ_decompose
  6. L152
    refl
  7. L153
    exact hJ
32Separate the logical casesL154–155

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

  1. L154
    cases hJ_decomp
  2. L155
    cases hJ_decomp_witness
33Establish hbridgeL156–165

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

  1. L156
    have hbridge : x1 = (K * x2) * x
  2. L157
    specialize IH k
  3. L158
    specialize IH j
  4. L159
    specialize IH x
  5. L160
    specialize IH x1
  6. L161
    specialize IH K
  7. L162
    specialize IH x2
  8. L163
    apply IH
  9. L164
    exact hprevious_sum
  10. L165
    exact ha_exists_witness
34Use earlier factsL166–175

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

  1. L166
    exact hF_decomp_witness_left
  2. L167
    exact hK
  3. L168
    exact hJ_decomp_witness_left
  4. L169
    specialize factorial_weighted_product_combine (S j)
  5. L170
    specialize factorial_weighted_product_combine (S n)
  6. L171
    specialize factorial_weighted_product_combine x
  7. L172
    specialize factorial_weighted_product_combine c
  8. L173
    specialize factorial_weighted_product_combine x1
  9. L174
    specialize factorial_weighted_product_combine K
  10. L175
    specialize factorial_weighted_product_combine x2
35Use earlier factsL176–182

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

  1. L176
    specialize factorial_weighted_product_combine F
  2. L177
    specialize factorial_weighted_product_combine J
  3. L178
    apply factorial_weighted_product_combine
  4. L179
    exact hJ_decomp_witness_right
  5. L180
    exact hF_decomp_witness_right
  6. L181
    exact hweighted
  7. L182
    exact hbridge

Library-wide reading audit

Original defined command ledger · 182 lines
  1. 0001induction n
  2. 0002intro k
  3. 0003induction j
  4. 0004intro c
  5. 0005intro F
  6. 0006intro K
  7. 0007intro J
  8. 0008intro hsum
  9. 0009intro hchoose
  10. 0010intro hF
  11. 0011intro hK
  12. 0012intro hJ
  13. 0013have hk : k = 0
  14. 0014trans k + 0
  15. 0015symm
  16. 0016apply PA3
  17. 0017exact hsum
  18. 0018have hc_one : c = 1
  19. 0019specialize choose_self_of_eq 0
  20. 0020specialize choose_self_of_eq k
  21. 0021specialize choose_self_of_eq c
  22. 0022apply choose_self_of_eq
  23. 0023exact hk
  24. 0024exact hchoose
  25. 0025have hF_one : F = 1
  26. 0026specialize factorial_zero 0
  27. 0027specialize factorial_zero F
  28. 0028apply factorial_zero
  29. 0029refl
  30. 0030exact hF
  31. 0031have hK_one : K = 1
  32. 0032specialize factorial_zero k
  33. 0033specialize factorial_zero K
  34. 0034apply factorial_zero
  35. 0035exact hk
  36. 0036exact hK
  37. 0037have hJ_one : J = 1
  38. 0038specialize factorial_zero 0
  39. 0039specialize factorial_zero J
  40. 0040apply factorial_zero
  41. 0041refl
  42. 0042exact hJ
  43. 0043rewrite hF_one
  44. 0044rewrite hK_one
  45. 0045rewrite hJ_one
  46. 0046rewrite hc_one
  47. 0047specialize mul_one 1
  48. 0048rewrite mul_one
  49. 0049rewrite mul_one
  50. 0050refl
  51. 0051intro c
  52. 0052intro F
  53. 0053intro K
  54. 0054intro J
  55. 0055intro hsum
  56. 0056rewrite PA4 at hsum
  57. 0057exfalso
  58. 0058apply PA1
  59. 0059exact hsum
  60. 0060intro k
  61. 0061induction j
  62. 0062intro c
  63. 0063intro F
  64. 0064intro K
  65. 0065intro J
  66. 0066intro hsum
  67. 0067intro hchoose
  68. 0068intro hF
  69. 0069intro hK
  70. 0070intro hJ
  71. 0071have hk : k = S n
  72. 0072trans k + 0
  73. 0073symm
  74. 0074apply PA3
  75. 0075exact hsum
  76. 0076have hc_one : c = 1
  77. 0077specialize choose_self_of_eq (S n)
  78. 0078specialize choose_self_of_eq k
  79. 0079specialize choose_self_of_eq c
  80. 0080apply choose_self_of_eq
  81. 0081exact hk
  82. 0082exact hchoose
  83. 0083have hJ_one : J = 1
  84. 0084specialize factorial_zero 0
  85. 0085specialize factorial_zero J
  86. 0086apply factorial_zero
  87. 0087refl
  88. 0088exact hJ
  89. 0089have hFK : F = K
  90. 0090specialize factorial_functional (S n)
  91. 0091specialize factorial_functional F
  92. 0092specialize factorial_functional K
  93. 0093apply factorial_functional
  94. 0094exact hF
  95. 0095specialize factorial_length_eq_transport k
  96. 0096specialize factorial_length_eq_transport (S n)
  97. 0097specialize factorial_length_eq_transport K
  98. 0098apply factorial_length_eq_transport
  99. 0099exact hk
  100. 0100exact hK
  101. 0101rewrite hFK
  102. 0102rewrite hJ_one
  103. 0103rewrite hc_one
  104. 0104specialize mul_one K
  105. 0105rewrite mul_one
  106. 0106rewrite mul_one
  107. 0107refl
  108. 0108intro c
  109. 0109intro F
  110. 0110intro K
  111. 0111intro J
  112. 0112intro hsum
  113. 0113intro hchoose
  114. 0114intro hF
  115. 0115intro hK
  116. 0116intro hJ
  117. 0117have hprevious_sum : k + j = n
  118. 0118apply PA2
  119. 0119trans k + S j
  120. 0120symm
  121. 0121apply PA4
  122. 0122exact hsum
  123. 0123have ha_exists : ∃ a. Choose(n,k,a)
    Exact native replay linehave ha_exists : exists a. (((exists bcf_lt_gap_bcfb_predecessor_choose_out_of_range. bcf_lt_gap_bcfb_predecessor_choose_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcfb_predecessor_choose_in_range. bcf_le_gap_bcfb_predecessor_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bcfb_predecessor_choose bcf_row_code_scale_bcfb_predecessor_choose bcf_row_scale_code_bcfb_predecessor_choose bcf_row_scale_scale_bcfb_predecessor_choose bcf_row_code_bcfb_predecessor_choose bcf_row_scale_bcfb_predecessor_choose. ((forall bcf_row_index_bcfb_predecessor_choose_table. (exists bcf_lt_gap_bcfb_predecessor_choose_table_row_bound. bcf_lt_gap_bcfb_predecessor_choose_table_row_bound + S (bcf_row_index_bcfb_predecessor_choose_table) = S (n)) -> exists bcf_row_code_bcfb_predecessor_choose_table bcf_row_scale_bcfb_predecessor_choose_table. ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_row_code. bcf_height_bcfb_predecessor_choose_table_decoded_row_code + S (bcf_row_code_bcfb_predecessor_choose_table) = S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_row_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_row_code * S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_row_code_bcfb_predecessor_choose_table))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_row_scale. bcf_height_bcfb_predecessor_choose_table_decoded_row_scale + S (bcf_row_scale_bcfb_predecessor_choose_table) = S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_row_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_row_scale_bcfb_predecessor_choose_table))) /\ ((bcf_row_index_bcfb_predecessor_choose_table = 0 /\ (forall bcf_index_bcfb_predecessor_choose_table_zero_row. (exists bcf_lt_gap_bcfb_predecessor_choose_table_zero_row_bound. bcf_lt_gap_bcfb_predecessor_choose_table_zero_row_bound + S (bcf_index_bcfb_predecessor_choose_table_zero_row) = S (n)) -> exists bcf_value_bcfb_predecessor_choose_table_zero_row. ((((exists bcf_height_bcfb_predecessor_choose_table_zero_row_entry. bcf_height_bcfb_predecessor_choose_table_zero_row_entry + S (bcf_value_bcfb_predecessor_choose_table_zero_row) = S ((S (bcf_index_bcfb_predecessor_choose_table_zero_row)) * bcf_row_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_zero_row_entry. bcf_row_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_zero_row_entry * S ((S (bcf_index_bcfb_predecessor_choose_table_zero_row)) * bcf_row_scale_bcfb_predecessor_choose_table) + (bcf_value_bcfb_predecessor_choose_table_zero_row))) /\ ((bcf_index_bcfb_predecessor_choose_table_zero_row = 0 /\ bcf_value_bcfb_predecessor_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcfb_predecessor_choose_table_zero_row. bcf_index_bcfb_predecessor_choose_table_zero_row = S bcf_predecessor_bcfb_predecessor_choose_table_zero_row /\ bcf_value_bcfb_predecessor_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcfb_predecessor_choose_table bcf_previous_code_bcfb_predecessor_choose_table bcf_previous_scale_bcfb_predecessor_choose_table. bcf_row_index_bcfb_predecessor_choose_table = S bcf_predecessor_bcfb_predecessor_choose_table /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_previous_code. bcf_height_bcfb_predecessor_choose_table_decoded_previous_code + S (bcf_previous_code_bcfb_predecessor_choose_table) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_previous_code_bcfb_predecessor_choose_table))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_previous_scale. bcf_height_bcfb_predecessor_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcfb_predecessor_choose_table) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_previous_scale_bcfb_predecessor_choose_table))) /\ (forall bcf_index_bcfb_predecessor_choose_table_row_step. (exists bcf_lt_gap_bcfb_predecessor_choose_table_row_step_bound. bcf_lt_gap_bcfb_predecessor_choose_table_row_step_bound + S (bcf_index_bcfb_predecessor_choose_table_row_step) = S (n)) -> exists bcf_value_bcfb_predecessor_choose_table_row_step. ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_entry. bcf_height_bcfb_predecessor_choose_table_row_step_entry + S (bcf_value_bcfb_predecessor_choose_table_row_step) = S ((S (bcf_index_bcfb_predecessor_choose_table_row_step)) * bcf_row_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_entry. bcf_row_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_entry * S ((S (bcf_index_bcfb_predecessor_choose_table_row_step)) * bcf_row_scale_bcfb_predecessor_choose_table) + (bcf_value_bcfb_predecessor_choose_table_row_step))) /\ ((bcf_index_bcfb_predecessor_choose_table_row_step = 0 /\ bcf_value_bcfb_predecessor_choose_table_row_step = 1) \/ exists bcf_predecessor_bcfb_predecessor_choose_table_row_step bcf_left_bcfb_predecessor_choose_table_row_step bcf_right_bcfb_predecessor_choose_table_row_step. bcf_index_bcfb_predecessor_choose_table_row_step = S bcf_predecessor_bcfb_predecessor_choose_table_row_step /\ ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_previous_left. bcf_height_bcfb_predecessor_choose_table_row_step_previous_left + S (bcf_left_bcfb_predecessor_choose_table_row_step) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table_row_step)) * bcf_previous_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_left. bcf_previous_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcfb_predecessor_choose_table_row_step)) * bcf_previous_scale_bcfb_predecessor_choose_table) + (bcf_left_bcfb_predecessor_choose_table_row_step))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_previous_right. bcf_height_bcfb_predecessor_choose_table_row_step_previous_right + S (bcf_right_bcfb_predecessor_choose_table_row_step) = S ((S (S (bcf_predecessor_bcfb_predecessor_choose_table_row_step))) * bcf_previous_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_right. bcf_previous_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcfb_predecessor_choose_table_row_step))) * bcf_previous_scale_bcfb_predecessor_choose_table) + (bcf_right_bcfb_predecessor_choose_table_row_step))) /\ bcf_value_bcfb_predecessor_choose_table_row_step = bcf_left_bcfb_predecessor_choose_table_row_step + bcf_right_bcfb_predecessor_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcfb_predecessor_choose_decoded_row_code. bcf_height_bcfb_predecessor_choose_decoded_row_code + S (bcf_row_code_bcfb_predecessor_choose) = S ((S (n)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_row_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_row_code_bcfb_predecessor_choose))) /\ ((((exists bcf_height_bcfb_predecessor_choose_decoded_row_scale. bcf_height_bcfb_predecessor_choose_decoded_row_scale + S (bcf_row_scale_bcfb_predecessor_choose) = S ((S (n)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_row_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_row_scale_bcfb_predecessor_choose))) /\ (((exists bcf_height_bcfb_predecessor_choose_decoded_value. bcf_height_bcfb_predecessor_choose_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_value. bcf_row_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_value * S ((S (k)) * bcf_row_scale_bcfb_predecessor_choose) + (a)))))))))
  124. 0124specialize choose_exists n
  125. 0125specialize choose_exists k
  126. 0126exact choose_exists
  127. 0127cases ha_exists
  128. 0128have hweighted : S j * c = S n * x
  129. 0129specialize choose_weighted_vertical n
  130. 0130specialize choose_weighted_vertical k
  131. 0131specialize choose_weighted_vertical j
  132. 0132specialize choose_weighted_vertical x
  133. 0133specialize choose_weighted_vertical c
  134. 0134apply choose_weighted_vertical
  135. 0135exact hprevious_sum
  136. 0136exact ha_exists_witness
  137. 0137exact hchoose
  138. 0138have hF_decomp : ∃ f. Factorial(n,f) ∧ F = f · S n
    Exact native replay linehave hF_decomp : exists f. (exists ff_b_bcfb_predecessor_total ff_c_bcfb_predecessor_total. ((forall ff_i_bcfb_predecessor_total_range. (exists ff_lt_bcfb_predecessor_total_range_bound. ff_lt_bcfb_predecessor_total_range_bound + S ff_i_bcfb_predecessor_total_range = n) -> (((exists ff_h_bcfb_predecessor_total_range_decoded. ff_h_bcfb_predecessor_total_range_decoded + S (1 + ff_i_bcfb_predecessor_total_range) = S ((S (ff_i_bcfb_predecessor_total_range)) * ff_c_bcfb_predecessor_total)) /\ exists ff_q_bcfb_predecessor_total_range_decoded. ff_b_bcfb_predecessor_total = ff_q_bcfb_predecessor_total_range_decoded * S ((S (ff_i_bcfb_predecessor_total_range)) * ff_c_bcfb_predecessor_total) + (1 + ff_i_bcfb_predecessor_total_range)))) /\ (exists ff_u_bcfb_predecessor_total_product ff_v_bcfb_predecessor_total_product. ((((exists ff_h_bcfb_predecessor_total_product_start. ff_h_bcfb_predecessor_total_product_start + S (1) = S ((S (0)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_start. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_start * S ((S (0)) * ff_v_bcfb_predecessor_total_product) + (1))) /\ ((((exists ff_h_bcfb_predecessor_total_product_terminal. ff_h_bcfb_predecessor_total_product_terminal + S (f) = S ((S (n)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_terminal. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_terminal * S ((S (n)) * ff_v_bcfb_predecessor_total_product) + (f))) /\ forall ff_i_bcfb_predecessor_total_product. (exists ff_lt_bcfb_predecessor_total_product_bound. ff_lt_bcfb_predecessor_total_product_bound + S ff_i_bcfb_predecessor_total_product = n) -> exists ff_p_bcfb_predecessor_total_product ff_r_bcfb_predecessor_total_product ff_s_bcfb_predecessor_total_product. ((((exists ff_h_bcfb_predecessor_total_product_factor. ff_h_bcfb_predecessor_total_product_factor + S (ff_p_bcfb_predecessor_total_product) = S ((S (ff_i_bcfb_predecessor_total_product)) * ff_c_bcfb_predecessor_total)) /\ exists ff_q_bcfb_predecessor_total_product_factor. ff_b_bcfb_predecessor_total = ff_q_bcfb_predecessor_total_product_factor * S ((S (ff_i_bcfb_predecessor_total_product)) * ff_c_bcfb_predecessor_total) + (ff_p_bcfb_predecessor_total_product))) /\ ((((exists ff_h_bcfb_predecessor_total_product_partial. ff_h_bcfb_predecessor_total_product_partial + S (ff_r_bcfb_predecessor_total_product) = S ((S (ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_partial. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_partial * S ((S (ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product) + (ff_r_bcfb_predecessor_total_product))) /\ ((((exists ff_h_bcfb_predecessor_total_product_successor. ff_h_bcfb_predecessor_total_product_successor + S (ff_s_bcfb_predecessor_total_product) = S ((S (S ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_successor. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_successor * S ((S (S ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product) + (ff_s_bcfb_predecessor_total_product))) /\ ff_s_bcfb_predecessor_total_product = ff_r_bcfb_predecessor_total_product * ff_p_bcfb_predecessor_total_product)))))))) /\ F = f * S n
  139. 0139specialize factorial_succ_decompose n
  140. 0140specialize factorial_succ_decompose (S n)
  141. 0141specialize factorial_succ_decompose F
  142. 0142apply factorial_succ_decompose
  143. 0143refl
  144. 0144exact hF
  145. 0145cases hF_decomp
  146. 0146cases hF_decomp_witness
  147. 0147have hJ_decomp : ∃ r. Factorial(j,r) ∧ J = r · S j
    Exact native replay linehave hJ_decomp : exists r. (exists ff_b_bcfb_predecessor_right ff_c_bcfb_predecessor_right. ((forall ff_i_bcfb_predecessor_right_range. (exists ff_lt_bcfb_predecessor_right_range_bound. ff_lt_bcfb_predecessor_right_range_bound + S ff_i_bcfb_predecessor_right_range = j) -> (((exists ff_h_bcfb_predecessor_right_range_decoded. ff_h_bcfb_predecessor_right_range_decoded + S (1 + ff_i_bcfb_predecessor_right_range) = S ((S (ff_i_bcfb_predecessor_right_range)) * ff_c_bcfb_predecessor_right)) /\ exists ff_q_bcfb_predecessor_right_range_decoded. ff_b_bcfb_predecessor_right = ff_q_bcfb_predecessor_right_range_decoded * S ((S (ff_i_bcfb_predecessor_right_range)) * ff_c_bcfb_predecessor_right) + (1 + ff_i_bcfb_predecessor_right_range)))) /\ (exists ff_u_bcfb_predecessor_right_product ff_v_bcfb_predecessor_right_product. ((((exists ff_h_bcfb_predecessor_right_product_start. ff_h_bcfb_predecessor_right_product_start + S (1) = S ((S (0)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_start. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_start * S ((S (0)) * ff_v_bcfb_predecessor_right_product) + (1))) /\ ((((exists ff_h_bcfb_predecessor_right_product_terminal. ff_h_bcfb_predecessor_right_product_terminal + S (r) = S ((S (j)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_terminal. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_terminal * S ((S (j)) * ff_v_bcfb_predecessor_right_product) + (r))) /\ forall ff_i_bcfb_predecessor_right_product. (exists ff_lt_bcfb_predecessor_right_product_bound. ff_lt_bcfb_predecessor_right_product_bound + S ff_i_bcfb_predecessor_right_product = j) -> exists ff_p_bcfb_predecessor_right_product ff_r_bcfb_predecessor_right_product ff_s_bcfb_predecessor_right_product. ((((exists ff_h_bcfb_predecessor_right_product_factor. ff_h_bcfb_predecessor_right_product_factor + S (ff_p_bcfb_predecessor_right_product) = S ((S (ff_i_bcfb_predecessor_right_product)) * ff_c_bcfb_predecessor_right)) /\ exists ff_q_bcfb_predecessor_right_product_factor. ff_b_bcfb_predecessor_right = ff_q_bcfb_predecessor_right_product_factor * S ((S (ff_i_bcfb_predecessor_right_product)) * ff_c_bcfb_predecessor_right) + (ff_p_bcfb_predecessor_right_product))) /\ ((((exists ff_h_bcfb_predecessor_right_product_partial. ff_h_bcfb_predecessor_right_product_partial + S (ff_r_bcfb_predecessor_right_product) = S ((S (ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_partial. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_partial * S ((S (ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product) + (ff_r_bcfb_predecessor_right_product))) /\ ((((exists ff_h_bcfb_predecessor_right_product_successor. ff_h_bcfb_predecessor_right_product_successor + S (ff_s_bcfb_predecessor_right_product) = S ((S (S ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_successor. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_successor * S ((S (S ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product) + (ff_s_bcfb_predecessor_right_product))) /\ ff_s_bcfb_predecessor_right_product = ff_r_bcfb_predecessor_right_product * ff_p_bcfb_predecessor_right_product)))))))) /\ J = r * S j
  148. 0148specialize factorial_succ_decompose j
  149. 0149specialize factorial_succ_decompose (S j)
  150. 0150specialize factorial_succ_decompose J
  151. 0151apply factorial_succ_decompose
  152. 0152refl
  153. 0153exact hJ
  154. 0154cases hJ_decomp
  155. 0155cases hJ_decomp_witness
  156. 0156have hbridge : x1 = (K * x2) * x
  157. 0157specialize IH k
  158. 0158specialize IH j
  159. 0159specialize IH x
  160. 0160specialize IH x1
  161. 0161specialize IH K
  162. 0162specialize IH x2
  163. 0163apply IH
  164. 0164exact hprevious_sum
  165. 0165exact ha_exists_witness
  166. 0166exact hF_decomp_witness_left
  167. 0167exact hK
  168. 0168exact hJ_decomp_witness_left
  169. 0169specialize factorial_weighted_product_combine (S j)
  170. 0170specialize factorial_weighted_product_combine (S n)
  171. 0171specialize factorial_weighted_product_combine x
  172. 0172specialize factorial_weighted_product_combine c
  173. 0173specialize factorial_weighted_product_combine x1
  174. 0174specialize factorial_weighted_product_combine K
  175. 0175specialize factorial_weighted_product_combine x2
  176. 0176specialize factorial_weighted_product_combine F
  177. 0177specialize factorial_weighted_product_combine J
  178. 0178apply factorial_weighted_product_combine
  179. 0179exact hJ_decomp_witness_right
  180. 0180exact hF_decomp_witness_right
  181. 0181exact hweighted
  182. 0182exact hbridge