PA006B

factorial_functional

Stable checked-use theorem · independently closed

The beta-coded relational factorial has a unique value.

Exact expanded PA statement

forall n z w. (exists ff_b_functional_l ff_c_functional_l. ((forall ff_i_functional_l_range. (exists ff_lt_functional_l_range_bound. ff_lt_functional_l_range_bound + S ff_i_functional_l_range = n) -> (((exists ff_h_functional_l_range_decoded. ff_h_functional_l_range_decoded + S (1 + ff_i_functional_l_range) = S ((S (ff_i_functional_l_range)) * ff_c_functional_l)) /\ exists ff_q_functional_l_range_decoded. ff_b_functional_l = ff_q_functional_l_range_decoded * S ((S (ff_i_functional_l_range)) * ff_c_functional_l) + (1 + ff_i_functional_l_range)))) /\ (exists ff_u_functional_l_product ff_v_functional_l_product. ((((exists ff_h_functional_l_product_start. ff_h_functional_l_product_start + S (1) = S ((S (0)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_start. ff_u_functional_l_product = ff_q_functional_l_product_start * S ((S (0)) * ff_v_functional_l_product) + (1))) /\ ((((exists ff_h_functional_l_product_terminal. ff_h_functional_l_product_terminal + S (z) = S ((S (n)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_terminal. ff_u_functional_l_product = ff_q_functional_l_product_terminal * S ((S (n)) * ff_v_functional_l_product) + (z))) /\ forall ff_i_functional_l_product. (exists ff_lt_functional_l_product_bound. ff_lt_functional_l_product_bound + S ff_i_functional_l_product = n) -> exists ff_p_functional_l_product ff_r_functional_l_product ff_s_functional_l_product. ((((exists ff_h_functional_l_product_factor. ff_h_functional_l_product_factor + S (ff_p_functional_l_product) = S ((S (ff_i_functional_l_product)) * ff_c_functional_l)) /\ exists ff_q_functional_l_product_factor. ff_b_functional_l = ff_q_functional_l_product_factor * S ((S (ff_i_functional_l_product)) * ff_c_functional_l) + (ff_p_functional_l_product))) /\ ((((exists ff_h_functional_l_product_partial. ff_h_functional_l_product_partial + S (ff_r_functional_l_product) = S ((S (ff_i_functional_l_product)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_partial. ff_u_functional_l_product = ff_q_functional_l_product_partial * S ((S (ff_i_functional_l_product)) * ff_v_functional_l_product) + (ff_r_functional_l_product))) /\ ((((exists ff_h_functional_l_product_successor. ff_h_functional_l_product_successor + S (ff_s_functional_l_product) = S ((S (S ff_i_functional_l_product)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_successor. ff_u_functional_l_product = ff_q_functional_l_product_successor * S ((S (S ff_i_functional_l_product)) * ff_v_functional_l_product) + (ff_s_functional_l_product))) /\ ff_s_functional_l_product = ff_r_functional_l_product * ff_p_functional_l_product)))))))) -> (exists ff_b_functional_r ff_c_functional_r. ((forall ff_i_functional_r_range. (exists ff_lt_functional_r_range_bound. ff_lt_functional_r_range_bound + S ff_i_functional_r_range = n) -> (((exists ff_h_functional_r_range_decoded. ff_h_functional_r_range_decoded + S (1 + ff_i_functional_r_range) = S ((S (ff_i_functional_r_range)) * ff_c_functional_r)) /\ exists ff_q_functional_r_range_decoded. ff_b_functional_r = ff_q_functional_r_range_decoded * S ((S (ff_i_functional_r_range)) * ff_c_functional_r) + (1 + ff_i_functional_r_range)))) /\ (exists ff_u_functional_r_product ff_v_functional_r_product. ((((exists ff_h_functional_r_product_start. ff_h_functional_r_product_start + S (1) = S ((S (0)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_start. ff_u_functional_r_product = ff_q_functional_r_product_start * S ((S (0)) * ff_v_functional_r_product) + (1))) /\ ((((exists ff_h_functional_r_product_terminal. ff_h_functional_r_product_terminal + S (w) = S ((S (n)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_terminal. ff_u_functional_r_product = ff_q_functional_r_product_terminal * S ((S (n)) * ff_v_functional_r_product) + (w))) /\ forall ff_i_functional_r_product. (exists ff_lt_functional_r_product_bound. ff_lt_functional_r_product_bound + S ff_i_functional_r_product = n) -> exists ff_p_functional_r_product ff_r_functional_r_product ff_s_functional_r_product. ((((exists ff_h_functional_r_product_factor. ff_h_functional_r_product_factor + S (ff_p_functional_r_product) = S ((S (ff_i_functional_r_product)) * ff_c_functional_r)) /\ exists ff_q_functional_r_product_factor. ff_b_functional_r = ff_q_functional_r_product_factor * S ((S (ff_i_functional_r_product)) * ff_c_functional_r) + (ff_p_functional_r_product))) /\ ((((exists ff_h_functional_r_product_partial. ff_h_functional_r_product_partial + S (ff_r_functional_r_product) = S ((S (ff_i_functional_r_product)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_partial. ff_u_functional_r_product = ff_q_functional_r_product_partial * S ((S (ff_i_functional_r_product)) * ff_v_functional_r_product) + (ff_r_functional_r_product))) /\ ((((exists ff_h_functional_r_product_successor. ff_h_functional_r_product_successor + S (ff_s_functional_r_product) = S ((S (S ff_i_functional_r_product)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_successor. ff_u_functional_r_product = ff_q_functional_r_product_successor * S ((S (S ff_i_functional_r_product)) * ff_v_functional_r_product) + (ff_s_functional_r_product))) /\ ff_s_functional_r_product = ff_r_functional_r_product * ff_p_functional_r_product)))))))) -> z = w

Structural proof guide

Generated structural guide

The beta-coded relational factorial has a unique value.

Use the direct prerequisites beta_range_transport_entry, beta_product_transport_prefix, beta_product_functional as previously established PA formulas.

The proof proceeds by case analysis (10), intermediate claims (2).

Referenced ingredients

PA006A beta_range_transport_entry PA004Y beta_product_transport_prefix PA0051 beta_product_functional

Proof neighborhood

Direct dependencies

PA006A beta_range_transport_entry PA004Y beta_product_transport_prefix PA0051 beta_product_functional

Direct dependents

PA00BG beta_range_two_product_is_factorial_succ PA00BH beta_range_two_product_restore_last

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro n
  2. 0002intro z
  3. 0003intro w
  4. 0004intro hz
  5. 0005intro hw
  6. 0006cases hz
  7. 0007cases hz_witness
  8. 0008cases hz_witness_witness
  9. 0009cases hw
  10. 0010cases hw_witness
  11. 0011cases hw_witness_witness
  12. 0012have htransport : exists ff_u_factorial_transport ff_v_factorial_transport. ((((exists ff_h_factorial_transport_start. ff_h_factorial_transport_start + S (1) = S ((S (0)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_start. ff_u_factorial_transport = ff_q_factorial_transport_start * S ((S (0)) * ff_v_factorial_transport) + (1))) /\ ((((exists ff_h_factorial_transport_terminal. ff_h_factorial_transport_terminal + S (z) = S ((S (n)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_terminal. ff_u_factorial_transport = ff_q_factorial_transport_terminal * S ((S (n)) * ff_v_factorial_transport) + (z))) /\ forall ff_i_factorial_transport. (exists ff_lt_factorial_transport_bound. ff_lt_factorial_transport_bound + S ff_i_factorial_transport = n) -> exists ff_p_factorial_transport ff_r_factorial_transport ff_s_factorial_transport. ((((exists ff_h_factorial_transport_factor. ff_h_factorial_transport_factor + S (ff_p_factorial_transport) = S ((S (ff_i_factorial_transport)) * x3)) /\ exists ff_q_factorial_transport_factor. x2 = ff_q_factorial_transport_factor * S ((S (ff_i_factorial_transport)) * x3) + (ff_p_factorial_transport))) /\ ((((exists ff_h_factorial_transport_partial. ff_h_factorial_transport_partial + S (ff_r_factorial_transport) = S ((S (ff_i_factorial_transport)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_partial. ff_u_factorial_transport = ff_q_factorial_transport_partial * S ((S (ff_i_factorial_transport)) * ff_v_factorial_transport) + (ff_r_factorial_transport))) /\ ((((exists ff_h_factorial_transport_successor. ff_h_factorial_transport_successor + S (ff_s_factorial_transport) = S ((S (S ff_i_factorial_transport)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_successor. ff_u_factorial_transport = ff_q_factorial_transport_successor * S ((S (S ff_i_factorial_transport)) * ff_v_factorial_transport) + (ff_s_factorial_transport))) /\ ff_s_factorial_transport = ff_r_factorial_transport * ff_p_factorial_transport)))))
  13. 0013specialize beta_product_transport_prefix x
  14. 0014specialize beta_product_transport_prefix x1
  15. 0015specialize beta_product_transport_prefix x2
  16. 0016specialize beta_product_transport_prefix x3
  17. 0017specialize beta_product_transport_prefix n
  18. 0018specialize beta_product_transport_prefix z
  19. 0019apply beta_product_transport_prefix
  20. 0020exact hz_witness_witness_right
  21. 0021intro i
  22. 0022intro p
  23. 0023intro hi
  24. 0024intro hp
  25. 0025specialize beta_range_transport_entry x
  26. 0026specialize beta_range_transport_entry x1
  27. 0027specialize beta_range_transport_entry x2
  28. 0028specialize beta_range_transport_entry x3
  29. 0029specialize beta_range_transport_entry 1
  30. 0030specialize beta_range_transport_entry n
  31. 0031have hentries : forall i p. (exists h. h + S i = n) -> (((exists ff_h_factorial_transport_l. ff_h_factorial_transport_l + S (p) = S ((S (i)) * x1)) /\ exists ff_q_factorial_transport_l. x = ff_q_factorial_transport_l * S ((S (i)) * x1) + (p))) -> (((exists ff_h_factorial_transport_r. ff_h_factorial_transport_r + S (p) = S ((S (i)) * x3)) /\ exists ff_q_factorial_transport_r. x2 = ff_q_factorial_transport_r * S ((S (i)) * x3) + (p)))
  32. 0032apply beta_range_transport_entry
  33. 0033exact hz_witness_witness_left
  34. 0034exact hw_witness_witness_left
  35. 0035specialize hentries i
  36. 0036specialize hentries p
  37. 0037apply hentries
  38. 0038exact hi
  39. 0039exact hp
  40. 0040cases htransport
  41. 0041cases htransport_witness
  42. 0042cases hw_witness_witness_right
  43. 0043cases hw_witness_witness_right_witness
  44. 0044specialize beta_product_functional x2
  45. 0045specialize beta_product_functional x3
  46. 0046specialize beta_product_functional n
  47. 0047specialize beta_product_functional z
  48. 0048specialize beta_product_functional x4
  49. 0049specialize beta_product_functional x5
  50. 0050specialize beta_product_functional w
  51. 0051specialize beta_product_functional x6
  52. 0052specialize beta_product_functional x7
  53. 0053apply beta_product_functional
  54. 0054exact htransport_witness_witness
  55. 0055exact hw_witness_witness_right_witness_witness