BT00U7

primorial_factor_prefix_extend

Alpha body-checked · checked-use disabled

Append one selector factor while preserving the previous prefix.

Exact expanded PA statement

forall b c m. (forall bpr_index_bpfpe_before. (exists bpr_gap_bpfpe_before_bound. bpr_gap_bpfpe_before_bound + S (bpr_index_bpfpe_before) = m) -> exists bpr_value_bpfpe_before. ((((exists bpr_height_bpfpe_before_decoded. bpr_height_bpfpe_before_decoded + S (bpr_value_bpfpe_before) = S ((S (bpr_index_bpfpe_before)) * c)) /\ exists bpr_quotient_bpfpe_before_decoded. b = bpr_quotient_bpfpe_before_decoded * S ((S (bpr_index_bpfpe_before)) * c) + (bpr_value_bpfpe_before))) /\ (((((~(S (bpr_index_bpfpe_before) = 1) /\ forall bpr_left_bpfpe_before_choice_prime bpr_right_bpfpe_before_choice_prime. S (bpr_index_bpfpe_before) = bpr_left_bpfpe_before_choice_prime * bpr_right_bpfpe_before_choice_prime -> bpr_left_bpfpe_before_choice_prime = 1 \/ bpr_right_bpfpe_before_choice_prime = 1)) /\ bpr_value_bpfpe_before = S (bpr_index_bpfpe_before)) \/ (~((~(S (bpr_index_bpfpe_before) = 1) /\ forall bpr_left_bpfpe_before_choice_prime bpr_right_bpfpe_before_choice_prime. S (bpr_index_bpfpe_before) = bpr_left_bpfpe_before_choice_prime * bpr_right_bpfpe_before_choice_prime -> bpr_left_bpfpe_before_choice_prime = 1 \/ bpr_right_bpfpe_before_choice_prime = 1)) /\ bpr_value_bpfpe_before = 1))))) -> exists d e. (forall bpr_index_bpfpe_after. (exists bpr_gap_bpfpe_after_bound. bpr_gap_bpfpe_after_bound + S (bpr_index_bpfpe_after) = S m) -> exists bpr_value_bpfpe_after. ((((exists bpr_height_bpfpe_after_decoded. bpr_height_bpfpe_after_decoded + S (bpr_value_bpfpe_after) = S ((S (bpr_index_bpfpe_after)) * e)) /\ exists bpr_quotient_bpfpe_after_decoded. d = bpr_quotient_bpfpe_after_decoded * S ((S (bpr_index_bpfpe_after)) * e) + (bpr_value_bpfpe_after))) /\ (((((~(S (bpr_index_bpfpe_after) = 1) /\ forall bpr_left_bpfpe_after_choice_prime bpr_right_bpfpe_after_choice_prime. S (bpr_index_bpfpe_after) = bpr_left_bpfpe_after_choice_prime * bpr_right_bpfpe_after_choice_prime -> bpr_left_bpfpe_after_choice_prime = 1 \/ bpr_right_bpfpe_after_choice_prime = 1)) /\ bpr_value_bpfpe_after = S (bpr_index_bpfpe_after)) \/ (~((~(S (bpr_index_bpfpe_after) = 1) /\ forall bpr_left_bpfpe_after_choice_prime bpr_right_bpfpe_after_choice_prime. S (bpr_index_bpfpe_after) = bpr_left_bpfpe_after_choice_prime * bpr_right_bpfpe_after_choice_prime -> bpr_left_bpfpe_after_choice_prime = 1 \/ bpr_right_bpfpe_after_choice_prime = 1)) /\ bpr_value_bpfpe_after = 1)))))

Structural proof guide

Append one selector factor while preserving the previous prefix.

Direct prerequisites: primorial_factor_choice_exists, beta_prefix_extend, finite_lt_succ_eq_or_lt. The authored body proceeds by case analysis (7), intermediate claims (4), equality transport (7).

Proof neighborhood

Direct dependencies

BT00U5 primorial_factor_choice_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00U8 primorial_factor_prefix_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 m
  4. 0004intro hprefix
  5. 0005have hchoice : exists x. (((((~(S (m) = 1) /\ forall bpr_left_bpfpe_last_choice_prime bpr_right_bpfpe_last_choice_prime. S (m) = bpr_left_bpfpe_last_choice_prime * bpr_right_bpfpe_last_choice_prime -> bpr_left_bpfpe_last_choice_prime = 1 \/ bpr_right_bpfpe_last_choice_prime = 1)) /\ x = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bpfpe_last_choice_prime bpr_right_bpfpe_last_choice_prime. S (m) = bpr_left_bpfpe_last_choice_prime * bpr_right_bpfpe_last_choice_prime -> bpr_left_bpfpe_last_choice_prime = 1 \/ bpr_right_bpfpe_last_choice_prime = 1)) /\ x = 1)))
  6. 0006apply primorial_factor_choice_exists
  7. 0007cases hchoice
  8. 0008have hext : exists d e. ((((exists bpr_height_bpfpe_append. bpr_height_bpfpe_append + S (x) = S ((S (m)) * e)) /\ exists bpr_quotient_bpfpe_append. d = bpr_quotient_bpfpe_append * S ((S (m)) * e) + (x))) /\ forall i a. (exists bpr_gap_bpfpe_old_bound. bpr_gap_bpfpe_old_bound + S (i) = m) -> (((exists bpr_height_bpfpe_old. bpr_height_bpfpe_old + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_bpfpe_old. b = bpr_quotient_bpfpe_old * S ((S (i)) * c) + (a))) -> (((exists bpr_height_bpfpe_new. bpr_height_bpfpe_new + S (a) = S ((S (i)) * e)) /\ exists bpr_quotient_bpfpe_new. d = bpr_quotient_bpfpe_new * S ((S (i)) * e) + (a))))
  9. 0009apply beta_prefix_extend
  10. 0010cases hext
  11. 0011cases hext_witness
  12. 0012cases hext_witness_witness
  13. 0013exists x1
  14. 0014exists x2
  15. 0015intro i
  16. 0016intro hi
  17. 0017have hsplit : i = m \/ exists gap. gap + S i = m
  18. 0018apply finite_lt_succ_eq_or_lt
  19. 0019exact hi
  20. 0020cases hsplit
  21. 0021rewrite hsplit_left
  22. 0022rewrite hsplit_left
  23. 0023rewrite hsplit_left
  24. 0024rewrite hsplit_left
  25. 0025rewrite hsplit_left
  26. 0026rewrite hsplit_left
  27. 0027rewrite hsplit_left
  28. 0028exists x
  29. 0029split
  30. 0030exact hext_witness_witness_left
  31. 0031exact hchoice_witness
  32. 0032have hold : exists a. ((((exists bpr_height_bpfpe_hold_decoded. bpr_height_bpfpe_hold_decoded + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_bpfpe_hold_decoded. b = bpr_quotient_bpfpe_hold_decoded * S ((S (i)) * c) + (a))) /\ (((((~(S (i) = 1) /\ forall bpr_left_bpfpe_hold_choice_prime bpr_right_bpfpe_hold_choice_prime. S (i) = bpr_left_bpfpe_hold_choice_prime * bpr_right_bpfpe_hold_choice_prime -> bpr_left_bpfpe_hold_choice_prime = 1 \/ bpr_right_bpfpe_hold_choice_prime = 1)) /\ a = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfpe_hold_choice_prime bpr_right_bpfpe_hold_choice_prime. S (i) = bpr_left_bpfpe_hold_choice_prime * bpr_right_bpfpe_hold_choice_prime -> bpr_left_bpfpe_hold_choice_prime = 1 \/ bpr_right_bpfpe_hold_choice_prime = 1)) /\ a = 1))))
  33. 0033apply hprefix
  34. 0034exact hsplit_right
  35. 0035cases hold
  36. 0036cases hold_witness
  37. 0037exists x3
  38. 0038split
  39. 0039apply hext_witness_witness_right
  40. 0040exact hsplit_right
  41. 0041exact hold_witness_left
  42. 0042exact hold_witness_right