BT005L

beta_product_transport_prefix

Stable · empty-context checked

One-way extensional factor-prefix preservation transports Product without changing its trace.

Exact expanded PA statement

forall b c z e l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> (forall i a. (exists h. h + S i = l) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + a)) -> (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))

Structural proof guide

One-way extensional factor-prefix preservation transports Product without changing its trace.

Direct prerequisites: none. The authored body proceeds by case analysis (10), intermediate claims (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT0082 pow_functional BT0090 factorial_functional

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro hproduct
  8. 0008intro hpres
  9. 0009cases hproduct
  10. 0010cases hproduct_witness
  11. 0011cases hproduct_witness_witness
  12. 0012cases hproduct_witness_witness_right
  13. 0013exists x
  14. 0014exists x1
  15. 0015split
  16. 0016exact hproduct_witness_witness_left
  17. 0017split
  18. 0018exact hproduct_witness_witness_right_left
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hstep : exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r) /\ (((exists h. h + S s = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s) /\ s = r * p)))
  22. 0022specialize hproduct_witness_witness_right_right i
  23. 0023apply hproduct_witness_witness_right_right
  24. 0024exact hi
  25. 0025cases hstep
  26. 0026cases hstep_witness
  27. 0027cases hstep_witness_witness
  28. 0028cases hstep_witness_witness_witness
  29. 0029cases hstep_witness_witness_witness_right
  30. 0030cases hstep_witness_witness_witness_right_right
  31. 0031exists x2
  32. 0032exists x3
  33. 0033exists x4
  34. 0034split
  35. 0035specialize hpres i
  36. 0036specialize hpres x2
  37. 0037apply hpres
  38. 0038exact hi
  39. 0039exact hstep_witness_witness_witness_left
  40. 0040split
  41. 0041exact hstep_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hstep_witness_witness_witness_right_right_left
  44. 0044exact hstep_witness_witness_witness_right_right_right