BT00UR

primorial_interval_factor_prefix_extend

Alpha body-checked · checked-use disabled

Append one offset selector while preserving the prior interval.

Exact expanded PA statement

forall a b c l. (forall bpr_index_bpifpe_before. (exists bpr_gap_bpifpe_before_bound. bpr_gap_bpifpe_before_bound + S (bpr_index_bpifpe_before) = l) -> exists bpr_value_bpifpe_before. ((((exists bpr_height_bpifpe_before_decoded. bpr_height_bpifpe_before_decoded + S (bpr_value_bpifpe_before) = S ((S (bpr_index_bpifpe_before)) * c)) /\ exists bpr_quotient_bpifpe_before_decoded. b = bpr_quotient_bpifpe_before_decoded * S ((S (bpr_index_bpifpe_before)) * c) + (bpr_value_bpifpe_before))) /\ (((((~(S (a + bpr_index_bpifpe_before) = 1) /\ forall bpr_left_bpifpe_before_choice_prime bpr_right_bpifpe_before_choice_prime. S (a + bpr_index_bpifpe_before) = bpr_left_bpifpe_before_choice_prime * bpr_right_bpifpe_before_choice_prime -> bpr_left_bpifpe_before_choice_prime = 1 \/ bpr_right_bpifpe_before_choice_prime = 1)) /\ bpr_value_bpifpe_before = S (a + bpr_index_bpifpe_before)) \/ (~((~(S (a + bpr_index_bpifpe_before) = 1) /\ forall bpr_left_bpifpe_before_choice_prime bpr_right_bpifpe_before_choice_prime. S (a + bpr_index_bpifpe_before) = bpr_left_bpifpe_before_choice_prime * bpr_right_bpifpe_before_choice_prime -> bpr_left_bpifpe_before_choice_prime = 1 \/ bpr_right_bpifpe_before_choice_prime = 1)) /\ bpr_value_bpifpe_before = 1))))) -> exists d e. (forall bpr_index_bpifpe_after. (exists bpr_gap_bpifpe_after_bound. bpr_gap_bpifpe_after_bound + S (bpr_index_bpifpe_after) = S l) -> exists bpr_value_bpifpe_after. ((((exists bpr_height_bpifpe_after_decoded. bpr_height_bpifpe_after_decoded + S (bpr_value_bpifpe_after) = S ((S (bpr_index_bpifpe_after)) * e)) /\ exists bpr_quotient_bpifpe_after_decoded. d = bpr_quotient_bpifpe_after_decoded * S ((S (bpr_index_bpifpe_after)) * e) + (bpr_value_bpifpe_after))) /\ (((((~(S (a + bpr_index_bpifpe_after) = 1) /\ forall bpr_left_bpifpe_after_choice_prime bpr_right_bpifpe_after_choice_prime. S (a + bpr_index_bpifpe_after) = bpr_left_bpifpe_after_choice_prime * bpr_right_bpifpe_after_choice_prime -> bpr_left_bpifpe_after_choice_prime = 1 \/ bpr_right_bpifpe_after_choice_prime = 1)) /\ bpr_value_bpifpe_after = S (a + bpr_index_bpifpe_after)) \/ (~((~(S (a + bpr_index_bpifpe_after) = 1) /\ forall bpr_left_bpifpe_after_choice_prime bpr_right_bpifpe_after_choice_prime. S (a + bpr_index_bpifpe_after) = bpr_left_bpifpe_after_choice_prime * bpr_right_bpifpe_after_choice_prime -> bpr_left_bpifpe_after_choice_prime = 1 \/ bpr_right_bpifpe_after_choice_prime = 1)) /\ bpr_value_bpifpe_after = 1)))))

Structural proof guide

Append one offset selector while preserving the prior interval.

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

BT00US primorial_interval_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 a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro hprefix
  6. 0006have hchoice : exists x. (((((~(S (a + l) = 1) /\ forall bpr_left_bpifpe_last_choice_prime bpr_right_bpifpe_last_choice_prime. S (a + l) = bpr_left_bpifpe_last_choice_prime * bpr_right_bpifpe_last_choice_prime -> bpr_left_bpifpe_last_choice_prime = 1 \/ bpr_right_bpifpe_last_choice_prime = 1)) /\ x = S (a + l)) \/ (~((~(S (a + l) = 1) /\ forall bpr_left_bpifpe_last_choice_prime bpr_right_bpifpe_last_choice_prime. S (a + l) = bpr_left_bpifpe_last_choice_prime * bpr_right_bpifpe_last_choice_prime -> bpr_left_bpifpe_last_choice_prime = 1 \/ bpr_right_bpifpe_last_choice_prime = 1)) /\ x = 1)))
  7. 0007apply primorial_factor_choice_exists
  8. 0008cases hchoice
  9. 0009have hext : exists d e. ((((exists bpr_height_bpifpe_append. bpr_height_bpifpe_append + S (x) = S ((S (l)) * e)) /\ exists bpr_quotient_bpifpe_append. d = bpr_quotient_bpifpe_append * S ((S (l)) * e) + (x))) /\ forall i p. (exists bpr_gap_bpifpe_old_bound. bpr_gap_bpifpe_old_bound + S (i) = l) -> (((exists bpr_height_bpifpe_old. bpr_height_bpifpe_old + S (p) = S ((S (i)) * c)) /\ exists bpr_quotient_bpifpe_old. b = bpr_quotient_bpifpe_old * S ((S (i)) * c) + (p))) -> (((exists bpr_height_bpifpe_new. bpr_height_bpifpe_new + S (p) = S ((S (i)) * e)) /\ exists bpr_quotient_bpifpe_new. d = bpr_quotient_bpifpe_new * S ((S (i)) * e) + (p))))
  10. 0010apply beta_prefix_extend
  11. 0011cases hext
  12. 0012cases hext_witness
  13. 0013cases hext_witness_witness
  14. 0014exists x1
  15. 0015exists x2
  16. 0016intro i
  17. 0017intro hi
  18. 0018have hsplit : i = l \/ exists gap. gap + S i = l
  19. 0019apply finite_lt_succ_eq_or_lt
  20. 0020exact hi
  21. 0021cases hsplit
  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. 0028rewrite hsplit_left
  29. 0029exists x
  30. 0030split
  31. 0031exact hext_witness_witness_left
  32. 0032exact hchoice_witness
  33. 0033have hold : exists p. ((((exists bpr_height_bpifpe_hold_decoded. bpr_height_bpifpe_hold_decoded + S (p) = S ((S (i)) * c)) /\ exists bpr_quotient_bpifpe_hold_decoded. b = bpr_quotient_bpifpe_hold_decoded * S ((S (i)) * c) + (p))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpifpe_hold_choice_prime bpr_right_bpifpe_hold_choice_prime. S (a + i) = bpr_left_bpifpe_hold_choice_prime * bpr_right_bpifpe_hold_choice_prime -> bpr_left_bpifpe_hold_choice_prime = 1 \/ bpr_right_bpifpe_hold_choice_prime = 1)) /\ p = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpifpe_hold_choice_prime bpr_right_bpifpe_hold_choice_prime. S (a + i) = bpr_left_bpifpe_hold_choice_prime * bpr_right_bpifpe_hold_choice_prime -> bpr_left_bpifpe_hold_choice_prime = 1 \/ bpr_right_bpifpe_hold_choice_prime = 1)) /\ p = 1))))
  34. 0034apply hprefix
  35. 0035exact hsplit_right
  36. 0036cases hold
  37. 0037cases hold_witness
  38. 0038exists x3
  39. 0039split
  40. 0040apply hext_witness_witness_right
  41. 0041exact hsplit_right
  42. 0042exact hold_witness_left
  43. 0043exact hold_witness_right