BT005F

beta_product_exists

Stable · empty-context checked

Every finite decoded beta prefix has an exact relational product and a coded trace.

Exact expanded PA statement

forall b c l. exists n 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)))))

Structural proof guide

Every finite decoded beta prefix has an exact relational product and a coded trace.

Direct prerequisites: beta_prefix_product_trace_exists, beta_at_exists. The authored body proceeds by case analysis (4), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT005E beta_prefix_product_trace_exists BT0041 beta_at_exists

Direct dependents

BT0080 pow_exists BT008Y factorial_exists BT00UA primorial_exists BT00UQ beta_product_prefix_suffix_split BT00YS prime_contribution_product_exists

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 l
  4. 0004have htrace : exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ 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))))
  5. 0005specialize beta_prefix_product_trace_exists b
  6. 0006specialize beta_prefix_product_trace_exists c
  7. 0007specialize beta_prefix_product_trace_exists l
  8. 0008exact beta_prefix_product_trace_exists
  9. 0009cases htrace
  10. 0010cases htrace_witness
  11. 0011cases htrace_witness_witness
  12. 0012have hterminal : exists n. ((exists h. h + S n = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + n)
  13. 0013specialize beta_at_exists x
  14. 0014specialize beta_at_exists x1
  15. 0015specialize beta_at_exists l
  16. 0016exact beta_at_exists
  17. 0017cases hterminal
  18. 0018exists x2
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact htrace_witness_witness_left
  23. 0023split
  24. 0024exact hterminal_witness
  25. 0025exact htrace_witness_witness_right