PA00BG · theorem

beta_range_two_product_is_factorial_succ

Alpha v34 checked-use theorem · independently closed; not Stable

A product of 2,...,l+1 is the factorial of l+1; the missing leading factor is one.

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

∀ l. ∀ b. ∀ c. ∀ P. Range(b,c,2,l) → Product(b,c,l,P) → Factorial(S l,P)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0014 Product PD0018 Range PD0023 Factorial

3 occurrences

In local proof propositions

PD0013 BetaAt PD0014 Product PD0018 Range PD0023 Factorial

7 occurrences

Exact expanded native-PA statement
forall l b c P. (forall wtp_range_index_wer_range_two. (exists wtp_range_gap_wer_range_two. wtp_range_gap_wer_range_two + S wtp_range_index_wer_range_two = l) -> (((exists ff_h_wer_range_two_decoded. ff_h_wer_range_two_decoded + S (2 + wtp_range_index_wer_range_two) = S ((S (wtp_range_index_wer_range_two)) * c)) /\ exists ff_q_wer_range_two_decoded. b = ff_q_wer_range_two_decoded * S ((S (wtp_range_index_wer_range_two)) * c) + (2 + wtp_range_index_wer_range_two)))) -> (exists ff_u_wer_range_two_product ff_v_wer_range_two_product. ((((exists ff_h_wer_range_two_product_start. ff_h_wer_range_two_product_start + S (1) = S ((S (0)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_start. ff_u_wer_range_two_product = ff_q_wer_range_two_product_start * S ((S (0)) * ff_v_wer_range_two_product) + (1))) /\ ((((exists ff_h_wer_range_two_product_terminal. ff_h_wer_range_two_product_terminal + S (P) = S ((S (l)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_terminal. ff_u_wer_range_two_product = ff_q_wer_range_two_product_terminal * S ((S (l)) * ff_v_wer_range_two_product) + (P))) /\ forall ff_i_wer_range_two_product. (exists ff_lt_wer_range_two_product_bound. ff_lt_wer_range_two_product_bound + S ff_i_wer_range_two_product = l) -> exists ff_p_wer_range_two_product ff_r_wer_range_two_product ff_s_wer_range_two_product. ((((exists ff_h_wer_range_two_product_factor. ff_h_wer_range_two_product_factor + S (ff_p_wer_range_two_product) = S ((S (ff_i_wer_range_two_product)) * c)) /\ exists ff_q_wer_range_two_product_factor. b = ff_q_wer_range_two_product_factor * S ((S (ff_i_wer_range_two_product)) * c) + (ff_p_wer_range_two_product))) /\ ((((exists ff_h_wer_range_two_product_partial. ff_h_wer_range_two_product_partial + S (ff_r_wer_range_two_product) = S ((S (ff_i_wer_range_two_product)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_partial. ff_u_wer_range_two_product = ff_q_wer_range_two_product_partial * S ((S (ff_i_wer_range_two_product)) * ff_v_wer_range_two_product) + (ff_r_wer_range_two_product))) /\ ((((exists ff_h_wer_range_two_product_successor. ff_h_wer_range_two_product_successor + S (ff_s_wer_range_two_product) = S ((S (S ff_i_wer_range_two_product)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_successor. ff_u_wer_range_two_product = ff_q_wer_range_two_product_successor * S ((S (S ff_i_wer_range_two_product)) * ff_v_wer_range_two_product) + (ff_s_wer_range_two_product))) /\ ff_s_wer_range_two_product = ff_r_wer_range_two_product * ff_p_wer_range_two_product)))))) -> (exists wer_factor_code_wer_factorial_successor wer_factor_scale_wer_factorial_successor. ((forall wer_range_index_wer_factorial_successor_range. (exists wer_range_gap_wer_factorial_successor_range. wer_range_gap_wer_factorial_successor_range + S wer_range_index_wer_factorial_successor_range = S l) -> (((exists ff_h_wer_factorial_successor_range_decoded. ff_h_wer_factorial_successor_range_decoded + S (1 + wer_range_index_wer_factorial_successor_range) = S ((S (wer_range_index_wer_factorial_successor_range)) * wer_factor_scale_wer_factorial_successor)) /\ exists ff_q_wer_factorial_successor_range_decoded. wer_factor_code_wer_factorial_successor = ff_q_wer_factorial_successor_range_decoded * S ((S (wer_range_index_wer_factorial_successor_range)) * wer_factor_scale_wer_factorial_successor) + (1 + wer_range_index_wer_factorial_successor_range)))) /\ (exists ff_u_wer_factorial_successor_product ff_v_wer_factorial_successor_product. ((((exists ff_h_wer_factorial_successor_product_start. ff_h_wer_factorial_successor_product_start + S (1) = S ((S (0)) * ff_v_wer_factorial_successor_product)) /\ exists ff_q_wer_factorial_successor_product_start. ff_u_wer_factorial_successor_product = ff_q_wer_factorial_successor_product_start * S ((S (0)) * ff_v_wer_factorial_successor_product) + (1))) /\ ((((exists ff_h_wer_factorial_successor_product_terminal. ff_h_wer_factorial_successor_product_terminal + S (P) = S ((S (S l)) * ff_v_wer_factorial_successor_product)) /\ exists ff_q_wer_factorial_successor_product_terminal. ff_u_wer_factorial_successor_product = ff_q_wer_factorial_successor_product_terminal * S ((S (S l)) * ff_v_wer_factorial_successor_product) + (P))) /\ forall ff_i_wer_factorial_successor_product. (exists ff_lt_wer_factorial_successor_product_bound. ff_lt_wer_factorial_successor_product_bound + S ff_i_wer_factorial_successor_product = S l) -> exists ff_p_wer_factorial_successor_product ff_r_wer_factorial_successor_product ff_s_wer_factorial_successor_product. ((((exists ff_h_wer_factorial_successor_product_factor. ff_h_wer_factorial_successor_product_factor + S (ff_p_wer_factorial_successor_product) = S ((S (ff_i_wer_factorial_successor_product)) * wer_factor_scale_wer_factorial_successor)) /\ exists ff_q_wer_factorial_successor_product_factor. wer_factor_code_wer_factorial_successor = ff_q_wer_factorial_successor_product_factor * S ((S (ff_i_wer_factorial_successor_product)) * wer_factor_scale_wer_factorial_successor) + (ff_p_wer_factorial_successor_product))) /\ ((((exists ff_h_wer_factorial_successor_product_partial. ff_h_wer_factorial_successor_product_partial + S (ff_r_wer_factorial_successor_product) = S ((S (ff_i_wer_factorial_successor_product)) * ff_v_wer_factorial_successor_product)) /\ exists ff_q_wer_factorial_successor_product_partial. ff_u_wer_factorial_successor_product = ff_q_wer_factorial_successor_product_partial * S ((S (ff_i_wer_factorial_successor_product)) * ff_v_wer_factorial_successor_product) + (ff_r_wer_factorial_successor_product))) /\ ((((exists ff_h_wer_factorial_successor_product_successor. ff_h_wer_factorial_successor_product_successor + S (ff_s_wer_factorial_successor_product) = S ((S (S ff_i_wer_factorial_successor_product)) * ff_v_wer_factorial_successor_product)) /\ exists ff_q_wer_factorial_successor_product_successor. ff_u_wer_factorial_successor_product = ff_q_wer_factorial_successor_product_successor * S ((S (S ff_i_wer_factorial_successor_product)) * ff_v_wer_factorial_successor_product) + (ff_s_wer_factorial_successor_product))) /\ ff_s_wer_factorial_successor_product = ff_r_wer_factorial_successor_product * ff_p_wer_factorial_successor_product))))))))

Proof neighborhood

Direct theorem prerequisites

PA00A3 factorial_one_value PA0049 beta_product_zero PA004A beta_product_succ_decompose PA0032 beta_range_entry_eq PA0060 factorial_exists PA0065 factorial_succ_decompose PA006B factorial_functional PA002O le_succ PA001A le_refl PA000E add_succ_left PA0001 zero_add PA0050 mul_congr

Direct theorem dependents

PA00BH beta_range_two_product_restore_last

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

115 script commands · 28 reading checkpoints · 13 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 (10)
factorial one valuebeta product zerobeta product succ decomposebeta range entry eqfactorial existsfactorial succ decomposefactorial functionalle succle reflmul congr
01Fix variables and assumptionsL1–1

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

  1. L1
    intro l
02Induction on lL2–7

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

  1. L2
    induction l
  2. L3
    intro b
  3. L4
    intro c
  4. L5
    intro P
  5. L6
    intro hrange
  6. L7
    intro hproduct
03Establish hponeL8–13

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

  1. L8
    have hpone : P = 1
  2. L9
    specialize beta_product_zero b
  3. L10
    specialize beta_product_zero c
  4. L11
    specialize beta_product_zero P
  5. L12
    apply beta_product_zero
  6. L13
    exact hproduct
04Establish hfactorialL14–16

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

  1. L14
    have hfactorial : ∃ F. Factorial(1,F)Definitions: Factorial(1,F)Original native command in the exact edition
  2. L15
    specialize factorial_exists 1
  3. L16
    exact factorial_exists
05Separate the logical casesL17–17

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

  1. L17
    cases hfactorial
06Establish hfoneL18–23

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

  1. L18
    have hfone : x = 1
  2. L19
    specialize factorial_one_value 1
  3. L20
    specialize factorial_one_value x
  4. L21
    apply factorial_one_value
  5. L22
    refl
  6. L23
    exact hfactorial_witness
07Establish hpxL24–33

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

  1. L24
    have hpx : P = x
  2. L25
    trans 1
  3. L26
    exact hpone
  4. L27
    symm
  5. L28
    exact hfone
  6. L29
    rewrite hpx
  7. L30
    rewrite hpx
  8. L31
    exact hfactorial_witness
  9. L32
    intro b
  10. L33
    intro c
08Fix variables and assumptionsL34–36

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

  1. L34
    intro P
  2. L35
    intro hrange
  3. L36
    intro hproduct
09Establish hrange_prefixL37–45

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

  1. L37
    have hrange_prefix : Range(b,c,2,l)Definitions: Range(b,c,2,l)Original native command in the exact edition
  2. L38
    intro i
  3. L39
    intro hi
  4. L40
    specialize hrange i
  5. L41
    apply hrange
  6. L42
    specialize le_succ (S i)
  7. L43
    specialize le_succ l
  8. L44
    apply le_succ
  9. L45
    exact hi
10Establish hdecompL46–52

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

  1. L46
    have hdecomp : ∃ x. ∃ x1. BetaAt(b,c,l,x) ∧ (Product(b,c,l,x1) ∧ P = x1 · x)Definitions: BetaAt(b,c,l,x)Product(b,c,l,x1)Original native command in the exact edition
  2. L47
    specialize beta_product_succ_decompose b
  3. L48
    specialize beta_product_succ_decompose c
  4. L49
    specialize beta_product_succ_decompose l
  5. L50
    specialize beta_product_succ_decompose P
  6. L51
    apply beta_product_succ_decompose
  7. L52
    exact hproduct
11Separate the logical casesL53–56

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

  1. L53
    cases hdecomp
  2. L54
    cases hdecomp_witness
  3. L55
    cases hdecomp_witness_witness
  4. L56
    cases hdecomp_witness_witness_right
12Establish hprefix_factorialL57–63

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

  1. L57
    have hprefix_factorial : Factorial(S l,x1)Definitions: Factorial(S l,x1)Original native command in the exact edition
  2. L58
    specialize IH b
  3. L59
    specialize IH c
  4. L60
    specialize IH x1
  5. L61
    apply IH
  6. L62
    exact hrange_prefix
  7. L63
    exact hdecomp_witness_witness_right_left
13Establish hfactor_valueL64–64

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

  1. L64
    have hfactor_value : x = S (S l)
14Establish hfactor_rawL65–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.

  1. L65
    have hfactor_raw : x = 2 + l
  2. L66
    specialize beta_range_entry_eq b
  3. L67
    specialize beta_range_entry_eq c
  4. L68
    specialize beta_range_entry_eq 2
  5. L69
    specialize beta_range_entry_eq (S l)
  6. L70
    specialize beta_range_entry_eq l
  7. L71
    specialize beta_range_entry_eq x
  8. L72
    apply beta_range_entry_eq
  9. L73
    exact hrange
  10. L74
    specialize le_refl (S l)
15Use earlier factsL75–76

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

  1. L75
    exact le_refl
  2. L76
    exact hdecomp_witness_witness_left
16Calculate and transport equalitiesL77–77

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

  1. L77
    trans 2 + l
17Use earlier factsL78–78

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

  1. L78
    exact hfactor_raw
18Calculate and transport equalitiesL79–79

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

  1. L79
    simp [add_succ_left, zero_add]
19Establish hfull_factorialL80–82

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

  1. L80
    have hfull_factorial : ∃ F. Factorial(S S l,F)Definitions: Factorial(S S l,F)Original native command in the exact edition
  2. L81
    specialize factorial_exists (S (S l))
  3. L82
    exact factorial_exists
20Separate the logical casesL83–83

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

  1. L83
    cases hfull_factorial
21Establish hfactorial_decompL84–90

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

  1. L84
    have hfactorial_decomp : ∃ x3. Factorial(S l,x3) ∧ x2 = x3 · S S lDefinitions: Factorial(S l,x3)Original native command in the exact edition
  2. L85
    specialize factorial_succ_decompose (S l)
  3. L86
    specialize factorial_succ_decompose (S (S l))
  4. L87
    specialize factorial_succ_decompose x2
  5. L88
    apply factorial_succ_decompose
  6. L89
    refl
  7. L90
    exact hfull_factorial_witness
22Separate the logical casesL91–92

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

  1. L91
    cases hfactorial_decomp
  2. L92
    cases hfactorial_decomp_witness
23Establish hprefix_eqL93–99

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

  1. L93
    have hprefix_eq : x1 = x3
  2. L94
    specialize factorial_functional (S l)
  3. L95
    specialize factorial_functional x1
  4. L96
    specialize factorial_functional x3
  5. L97
    apply factorial_functional
  6. L98
    exact hprefix_factorial
  7. L99
    exact hfactorial_decomp_witness_left
24Establish hproduct_eqL100–109

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

  1. L100
    have hproduct_eq : P = x2
  2. L101
    trans x1 * x
  3. L102
    exact hdecomp_witness_witness_right_right
  4. L103
    trans x1 * S (S l)
  5. L104
    apply mul_congr
  6. L105
    refl
  7. L106
    exact hfactor_value
  8. L107
    trans x3 * S (S l)
  9. L108
    apply mul_congr
  10. L109
    exact hprefix_eq
25Calculate and transport equalitiesL110–111

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

  1. L110
    refl
  2. L111
    symm
26Use earlier factsL112–112

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

  1. L112
    exact hfactorial_decomp_witness_right
27Calculate and transport equalitiesL113–114

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

  1. L113
    rewrite hproduct_eq
  2. L114
    rewrite hproduct_eq
28Use earlier factsL115–115

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

  1. L115
    exact hfull_factorial_witness

Library-wide reading audit

Original defined command ledger · 115 lines
  1. 0001intro l
  2. 0002induction l
  3. 0003intro b
  4. 0004intro c
  5. 0005intro P
  6. 0006intro hrange
  7. 0007intro hproduct
  8. 0008have hpone : P = 1
  9. 0009specialize beta_product_zero b
  10. 0010specialize beta_product_zero c
  11. 0011specialize beta_product_zero P
  12. 0012apply beta_product_zero
  13. 0013exact hproduct
  14. 0014have hfactorial : ∃ F. Factorial(1,F)
    Exact native replay linehave hfactorial : exists F. (exists wer_factor_code_wer_factorial_one_F wer_factor_scale_wer_factorial_one_F. ((forall wer_range_index_wer_factorial_one_F_range. (exists wer_range_gap_wer_factorial_one_F_range. wer_range_gap_wer_factorial_one_F_range + S wer_range_index_wer_factorial_one_F_range = 1) -> (((exists ff_h_wer_factorial_one_F_range_decoded. ff_h_wer_factorial_one_F_range_decoded + S (1 + wer_range_index_wer_factorial_one_F_range) = S ((S (wer_range_index_wer_factorial_one_F_range)) * wer_factor_scale_wer_factorial_one_F)) /\ exists ff_q_wer_factorial_one_F_range_decoded. wer_factor_code_wer_factorial_one_F = ff_q_wer_factorial_one_F_range_decoded * S ((S (wer_range_index_wer_factorial_one_F_range)) * wer_factor_scale_wer_factorial_one_F) + (1 + wer_range_index_wer_factorial_one_F_range)))) /\ (exists ff_u_wer_factorial_one_F_product ff_v_wer_factorial_one_F_product. ((((exists ff_h_wer_factorial_one_F_product_start. ff_h_wer_factorial_one_F_product_start + S (1) = S ((S (0)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_start. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_start * S ((S (0)) * ff_v_wer_factorial_one_F_product) + (1))) /\ ((((exists ff_h_wer_factorial_one_F_product_terminal. ff_h_wer_factorial_one_F_product_terminal + S (F) = S ((S (1)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_terminal. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_terminal * S ((S (1)) * ff_v_wer_factorial_one_F_product) + (F))) /\ forall ff_i_wer_factorial_one_F_product. (exists ff_lt_wer_factorial_one_F_product_bound. ff_lt_wer_factorial_one_F_product_bound + S ff_i_wer_factorial_one_F_product = 1) -> exists ff_p_wer_factorial_one_F_product ff_r_wer_factorial_one_F_product ff_s_wer_factorial_one_F_product. ((((exists ff_h_wer_factorial_one_F_product_factor. ff_h_wer_factorial_one_F_product_factor + S (ff_p_wer_factorial_one_F_product) = S ((S (ff_i_wer_factorial_one_F_product)) * wer_factor_scale_wer_factorial_one_F)) /\ exists ff_q_wer_factorial_one_F_product_factor. wer_factor_code_wer_factorial_one_F = ff_q_wer_factorial_one_F_product_factor * S ((S (ff_i_wer_factorial_one_F_product)) * wer_factor_scale_wer_factorial_one_F) + (ff_p_wer_factorial_one_F_product))) /\ ((((exists ff_h_wer_factorial_one_F_product_partial. ff_h_wer_factorial_one_F_product_partial + S (ff_r_wer_factorial_one_F_product) = S ((S (ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_partial. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_partial * S ((S (ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product) + (ff_r_wer_factorial_one_F_product))) /\ ((((exists ff_h_wer_factorial_one_F_product_successor. ff_h_wer_factorial_one_F_product_successor + S (ff_s_wer_factorial_one_F_product) = S ((S (S ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_successor. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_successor * S ((S (S ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product) + (ff_s_wer_factorial_one_F_product))) /\ ff_s_wer_factorial_one_F_product = ff_r_wer_factorial_one_F_product * ff_p_wer_factorial_one_F_product))))))))
  15. 0015specialize factorial_exists 1
  16. 0016exact factorial_exists
  17. 0017cases hfactorial
  18. 0018have hfone : x = 1
  19. 0019specialize factorial_one_value 1
  20. 0020specialize factorial_one_value x
  21. 0021apply factorial_one_value
  22. 0022refl
  23. 0023exact hfactorial_witness
  24. 0024have hpx : P = x
  25. 0025trans 1
  26. 0026exact hpone
  27. 0027symm
  28. 0028exact hfone
  29. 0029rewrite hpx
  30. 0030rewrite hpx
  31. 0031exact hfactorial_witness
  32. 0032intro b
  33. 0033intro c
  34. 0034intro P
  35. 0035intro hrange
  36. 0036intro hproduct
  37. 0037have hrange_prefix : Range(b,c,2,l)
    Exact native replay linehave hrange_prefix : forall wtp_range_index_wer_step_prefix_range. (exists wtp_range_gap_wer_step_prefix_range. wtp_range_gap_wer_step_prefix_range + S wtp_range_index_wer_step_prefix_range = l) -> (((exists ff_h_wer_step_prefix_range_decoded. ff_h_wer_step_prefix_range_decoded + S (2 + wtp_range_index_wer_step_prefix_range) = S ((S (wtp_range_index_wer_step_prefix_range)) * c)) /\ exists ff_q_wer_step_prefix_range_decoded. b = ff_q_wer_step_prefix_range_decoded * S ((S (wtp_range_index_wer_step_prefix_range)) * c) + (2 + wtp_range_index_wer_step_prefix_range)))
  38. 0038intro i
  39. 0039intro hi
  40. 0040specialize hrange i
  41. 0041apply hrange
  42. 0042specialize le_succ (S i)
  43. 0043specialize le_succ l
  44. 0044apply le_succ
  45. 0045exact hi
  46. 0046have hdecomp : ∃ x. ∃ x1. BetaAt(b,c,l,x) ∧ (Product(b,c,l,x1) ∧ P = x1 · x)
    Exact native replay linehave hdecomp : exists x x1. ((((exists ff_h_wer_step_factor. ff_h_wer_step_factor + S (x) = S ((S (l)) * c)) /\ exists ff_q_wer_step_factor. b = ff_q_wer_step_factor * S ((S (l)) * c) + (x))) /\ ((exists ff_u_wer_step_prefix_product ff_v_wer_step_prefix_product. ((((exists ff_h_wer_step_prefix_product_start. ff_h_wer_step_prefix_product_start + S (1) = S ((S (0)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_start. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_start * S ((S (0)) * ff_v_wer_step_prefix_product) + (1))) /\ ((((exists ff_h_wer_step_prefix_product_terminal. ff_h_wer_step_prefix_product_terminal + S (x1) = S ((S (l)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_terminal. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_terminal * S ((S (l)) * ff_v_wer_step_prefix_product) + (x1))) /\ forall ff_i_wer_step_prefix_product. (exists ff_lt_wer_step_prefix_product_bound. ff_lt_wer_step_prefix_product_bound + S ff_i_wer_step_prefix_product = l) -> exists ff_p_wer_step_prefix_product ff_r_wer_step_prefix_product ff_s_wer_step_prefix_product. ((((exists ff_h_wer_step_prefix_product_factor. ff_h_wer_step_prefix_product_factor + S (ff_p_wer_step_prefix_product) = S ((S (ff_i_wer_step_prefix_product)) * c)) /\ exists ff_q_wer_step_prefix_product_factor. b = ff_q_wer_step_prefix_product_factor * S ((S (ff_i_wer_step_prefix_product)) * c) + (ff_p_wer_step_prefix_product))) /\ ((((exists ff_h_wer_step_prefix_product_partial. ff_h_wer_step_prefix_product_partial + S (ff_r_wer_step_prefix_product) = S ((S (ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_partial. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_partial * S ((S (ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product) + (ff_r_wer_step_prefix_product))) /\ ((((exists ff_h_wer_step_prefix_product_successor. ff_h_wer_step_prefix_product_successor + S (ff_s_wer_step_prefix_product) = S ((S (S ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_successor. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_successor * S ((S (S ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product) + (ff_s_wer_step_prefix_product))) /\ ff_s_wer_step_prefix_product = ff_r_wer_step_prefix_product * ff_p_wer_step_prefix_product)))))) /\ P = x1 * x))
  47. 0047specialize beta_product_succ_decompose b
  48. 0048specialize beta_product_succ_decompose c
  49. 0049specialize beta_product_succ_decompose l
  50. 0050specialize beta_product_succ_decompose P
  51. 0051apply beta_product_succ_decompose
  52. 0052exact hproduct
  53. 0053cases hdecomp
  54. 0054cases hdecomp_witness
  55. 0055cases hdecomp_witness_witness
  56. 0056cases hdecomp_witness_witness_right
  57. 0057have hprefix_factorial : Factorial(S l,x1)
    Exact native replay linehave hprefix_factorial : exists wer_factor_code_wer_step_prefix_factorial wer_factor_scale_wer_step_prefix_factorial. ((forall wer_range_index_wer_step_prefix_factorial_range. (exists wer_range_gap_wer_step_prefix_factorial_range. wer_range_gap_wer_step_prefix_factorial_range + S wer_range_index_wer_step_prefix_factorial_range = S l) -> (((exists ff_h_wer_step_prefix_factorial_range_decoded. ff_h_wer_step_prefix_factorial_range_decoded + S (1 + wer_range_index_wer_step_prefix_factorial_range) = S ((S (wer_range_index_wer_step_prefix_factorial_range)) * wer_factor_scale_wer_step_prefix_factorial)) /\ exists ff_q_wer_step_prefix_factorial_range_decoded. wer_factor_code_wer_step_prefix_factorial = ff_q_wer_step_prefix_factorial_range_decoded * S ((S (wer_range_index_wer_step_prefix_factorial_range)) * wer_factor_scale_wer_step_prefix_factorial) + (1 + wer_range_index_wer_step_prefix_factorial_range)))) /\ (exists ff_u_wer_step_prefix_factorial_product ff_v_wer_step_prefix_factorial_product. ((((exists ff_h_wer_step_prefix_factorial_product_start. ff_h_wer_step_prefix_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_start. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_start * S ((S (0)) * ff_v_wer_step_prefix_factorial_product) + (1))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_terminal. ff_h_wer_step_prefix_factorial_product_terminal + S (x1) = S ((S (S l)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_terminal. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_terminal * S ((S (S l)) * ff_v_wer_step_prefix_factorial_product) + (x1))) /\ forall ff_i_wer_step_prefix_factorial_product. (exists ff_lt_wer_step_prefix_factorial_product_bound. ff_lt_wer_step_prefix_factorial_product_bound + S ff_i_wer_step_prefix_factorial_product = S l) -> exists ff_p_wer_step_prefix_factorial_product ff_r_wer_step_prefix_factorial_product ff_s_wer_step_prefix_factorial_product. ((((exists ff_h_wer_step_prefix_factorial_product_factor. ff_h_wer_step_prefix_factorial_product_factor + S (ff_p_wer_step_prefix_factorial_product) = S ((S (ff_i_wer_step_prefix_factorial_product)) * wer_factor_scale_wer_step_prefix_factorial)) /\ exists ff_q_wer_step_prefix_factorial_product_factor. wer_factor_code_wer_step_prefix_factorial = ff_q_wer_step_prefix_factorial_product_factor * S ((S (ff_i_wer_step_prefix_factorial_product)) * wer_factor_scale_wer_step_prefix_factorial) + (ff_p_wer_step_prefix_factorial_product))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_partial. ff_h_wer_step_prefix_factorial_product_partial + S (ff_r_wer_step_prefix_factorial_product) = S ((S (ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_partial. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_partial * S ((S (ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product) + (ff_r_wer_step_prefix_factorial_product))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_successor. ff_h_wer_step_prefix_factorial_product_successor + S (ff_s_wer_step_prefix_factorial_product) = S ((S (S ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_successor. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_successor * S ((S (S ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product) + (ff_s_wer_step_prefix_factorial_product))) /\ ff_s_wer_step_prefix_factorial_product = ff_r_wer_step_prefix_factorial_product * ff_p_wer_step_prefix_factorial_product)))))))
  58. 0058specialize IH b
  59. 0059specialize IH c
  60. 0060specialize IH x1
  61. 0061apply IH
  62. 0062exact hrange_prefix
  63. 0063exact hdecomp_witness_witness_right_left
  64. 0064have hfactor_value : x = S (S l)
  65. 0065have hfactor_raw : x = 2 + l
  66. 0066specialize beta_range_entry_eq b
  67. 0067specialize beta_range_entry_eq c
  68. 0068specialize beta_range_entry_eq 2
  69. 0069specialize beta_range_entry_eq (S l)
  70. 0070specialize beta_range_entry_eq l
  71. 0071specialize beta_range_entry_eq x
  72. 0072apply beta_range_entry_eq
  73. 0073exact hrange
  74. 0074specialize le_refl (S l)
  75. 0075exact le_refl
  76. 0076exact hdecomp_witness_witness_left
  77. 0077trans 2 + l
  78. 0078exact hfactor_raw
  79. 0079simp [add_succ_left, zero_add]
  80. 0080have hfull_factorial : ∃ F. Factorial(S S l,F)
    Exact native replay linehave hfull_factorial : exists F. (exists wer_factor_code_wer_step_full_factorial_F wer_factor_scale_wer_step_full_factorial_F. ((forall wer_range_index_wer_step_full_factorial_F_range. (exists wer_range_gap_wer_step_full_factorial_F_range. wer_range_gap_wer_step_full_factorial_F_range + S wer_range_index_wer_step_full_factorial_F_range = S (S l)) -> (((exists ff_h_wer_step_full_factorial_F_range_decoded. ff_h_wer_step_full_factorial_F_range_decoded + S (1 + wer_range_index_wer_step_full_factorial_F_range) = S ((S (wer_range_index_wer_step_full_factorial_F_range)) * wer_factor_scale_wer_step_full_factorial_F)) /\ exists ff_q_wer_step_full_factorial_F_range_decoded. wer_factor_code_wer_step_full_factorial_F = ff_q_wer_step_full_factorial_F_range_decoded * S ((S (wer_range_index_wer_step_full_factorial_F_range)) * wer_factor_scale_wer_step_full_factorial_F) + (1 + wer_range_index_wer_step_full_factorial_F_range)))) /\ (exists ff_u_wer_step_full_factorial_F_product ff_v_wer_step_full_factorial_F_product. ((((exists ff_h_wer_step_full_factorial_F_product_start. ff_h_wer_step_full_factorial_F_product_start + S (1) = S ((S (0)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_start. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_start * S ((S (0)) * ff_v_wer_step_full_factorial_F_product) + (1))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_terminal. ff_h_wer_step_full_factorial_F_product_terminal + S (F) = S ((S (S (S l))) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_terminal. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_terminal * S ((S (S (S l))) * ff_v_wer_step_full_factorial_F_product) + (F))) /\ forall ff_i_wer_step_full_factorial_F_product. (exists ff_lt_wer_step_full_factorial_F_product_bound. ff_lt_wer_step_full_factorial_F_product_bound + S ff_i_wer_step_full_factorial_F_product = S (S l)) -> exists ff_p_wer_step_full_factorial_F_product ff_r_wer_step_full_factorial_F_product ff_s_wer_step_full_factorial_F_product. ((((exists ff_h_wer_step_full_factorial_F_product_factor. ff_h_wer_step_full_factorial_F_product_factor + S (ff_p_wer_step_full_factorial_F_product) = S ((S (ff_i_wer_step_full_factorial_F_product)) * wer_factor_scale_wer_step_full_factorial_F)) /\ exists ff_q_wer_step_full_factorial_F_product_factor. wer_factor_code_wer_step_full_factorial_F = ff_q_wer_step_full_factorial_F_product_factor * S ((S (ff_i_wer_step_full_factorial_F_product)) * wer_factor_scale_wer_step_full_factorial_F) + (ff_p_wer_step_full_factorial_F_product))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_partial. ff_h_wer_step_full_factorial_F_product_partial + S (ff_r_wer_step_full_factorial_F_product) = S ((S (ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_partial. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_partial * S ((S (ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product) + (ff_r_wer_step_full_factorial_F_product))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_successor. ff_h_wer_step_full_factorial_F_product_successor + S (ff_s_wer_step_full_factorial_F_product) = S ((S (S ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_successor. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_successor * S ((S (S ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product) + (ff_s_wer_step_full_factorial_F_product))) /\ ff_s_wer_step_full_factorial_F_product = ff_r_wer_step_full_factorial_F_product * ff_p_wer_step_full_factorial_F_product))))))))
  81. 0081specialize factorial_exists (S (S l))
  82. 0082exact factorial_exists
  83. 0083cases hfull_factorial
  84. 0084have hfactorial_decomp : ∃ x3. Factorial(S l,x3) ∧ x2 = x3 · S S l
    Exact native replay linehave hfactorial_decomp : exists x3. ((exists wer_factor_code_wer_step_previous_factorial wer_factor_scale_wer_step_previous_factorial. ((forall wer_range_index_wer_step_previous_factorial_range. (exists wer_range_gap_wer_step_previous_factorial_range. wer_range_gap_wer_step_previous_factorial_range + S wer_range_index_wer_step_previous_factorial_range = S l) -> (((exists ff_h_wer_step_previous_factorial_range_decoded. ff_h_wer_step_previous_factorial_range_decoded + S (1 + wer_range_index_wer_step_previous_factorial_range) = S ((S (wer_range_index_wer_step_previous_factorial_range)) * wer_factor_scale_wer_step_previous_factorial)) /\ exists ff_q_wer_step_previous_factorial_range_decoded. wer_factor_code_wer_step_previous_factorial = ff_q_wer_step_previous_factorial_range_decoded * S ((S (wer_range_index_wer_step_previous_factorial_range)) * wer_factor_scale_wer_step_previous_factorial) + (1 + wer_range_index_wer_step_previous_factorial_range)))) /\ (exists ff_u_wer_step_previous_factorial_product ff_v_wer_step_previous_factorial_product. ((((exists ff_h_wer_step_previous_factorial_product_start. ff_h_wer_step_previous_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_start. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_start * S ((S (0)) * ff_v_wer_step_previous_factorial_product) + (1))) /\ ((((exists ff_h_wer_step_previous_factorial_product_terminal. ff_h_wer_step_previous_factorial_product_terminal + S (x3) = S ((S (S l)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_terminal. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_terminal * S ((S (S l)) * ff_v_wer_step_previous_factorial_product) + (x3))) /\ forall ff_i_wer_step_previous_factorial_product. (exists ff_lt_wer_step_previous_factorial_product_bound. ff_lt_wer_step_previous_factorial_product_bound + S ff_i_wer_step_previous_factorial_product = S l) -> exists ff_p_wer_step_previous_factorial_product ff_r_wer_step_previous_factorial_product ff_s_wer_step_previous_factorial_product. ((((exists ff_h_wer_step_previous_factorial_product_factor. ff_h_wer_step_previous_factorial_product_factor + S (ff_p_wer_step_previous_factorial_product) = S ((S (ff_i_wer_step_previous_factorial_product)) * wer_factor_scale_wer_step_previous_factorial)) /\ exists ff_q_wer_step_previous_factorial_product_factor. wer_factor_code_wer_step_previous_factorial = ff_q_wer_step_previous_factorial_product_factor * S ((S (ff_i_wer_step_previous_factorial_product)) * wer_factor_scale_wer_step_previous_factorial) + (ff_p_wer_step_previous_factorial_product))) /\ ((((exists ff_h_wer_step_previous_factorial_product_partial. ff_h_wer_step_previous_factorial_product_partial + S (ff_r_wer_step_previous_factorial_product) = S ((S (ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_partial. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_partial * S ((S (ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product) + (ff_r_wer_step_previous_factorial_product))) /\ ((((exists ff_h_wer_step_previous_factorial_product_successor. ff_h_wer_step_previous_factorial_product_successor + S (ff_s_wer_step_previous_factorial_product) = S ((S (S ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_successor. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_successor * S ((S (S ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product) + (ff_s_wer_step_previous_factorial_product))) /\ ff_s_wer_step_previous_factorial_product = ff_r_wer_step_previous_factorial_product * ff_p_wer_step_previous_factorial_product)))))))) /\ x2 = x3 * S (S l))
  85. 0085specialize factorial_succ_decompose (S l)
  86. 0086specialize factorial_succ_decompose (S (S l))
  87. 0087specialize factorial_succ_decompose x2
  88. 0088apply factorial_succ_decompose
  89. 0089refl
  90. 0090exact hfull_factorial_witness
  91. 0091cases hfactorial_decomp
  92. 0092cases hfactorial_decomp_witness
  93. 0093have hprefix_eq : x1 = x3
  94. 0094specialize factorial_functional (S l)
  95. 0095specialize factorial_functional x1
  96. 0096specialize factorial_functional x3
  97. 0097apply factorial_functional
  98. 0098exact hprefix_factorial
  99. 0099exact hfactorial_decomp_witness_left
  100. 0100have hproduct_eq : P = x2
  101. 0101trans x1 * x
  102. 0102exact hdecomp_witness_witness_right_right
  103. 0103trans x1 * S (S l)
  104. 0104apply mul_congr
  105. 0105refl
  106. 0106exact hfactor_value
  107. 0107trans x3 * S (S l)
  108. 0108apply mul_congr
  109. 0109exact hprefix_eq
  110. 0110refl
  111. 0111symm
  112. 0112exact hfactorial_decomp_witness_right
  113. 0113rewrite hproduct_eq
  114. 0114rewrite hproduct_eq
  115. 0115exact hfull_factorial_witness