BT00US

primorial_interval_factor_prefix_exists

Alpha body-checked · checked-use disabled

Every offset and length has a beta-coded selector interval.

Exact expanded PA statement

forall a l. exists b c. (forall bpr_index_bpifpx_result. (exists bpr_gap_bpifpx_result_bound. bpr_gap_bpifpx_result_bound + S (bpr_index_bpifpx_result) = l) -> exists bpr_value_bpifpx_result. ((((exists bpr_height_bpifpx_result_decoded. bpr_height_bpifpx_result_decoded + S (bpr_value_bpifpx_result) = S ((S (bpr_index_bpifpx_result)) * c)) /\ exists bpr_quotient_bpifpx_result_decoded. b = bpr_quotient_bpifpx_result_decoded * S ((S (bpr_index_bpifpx_result)) * c) + (bpr_value_bpifpx_result))) /\ (((((~(S (a + bpr_index_bpifpx_result) = 1) /\ forall bpr_left_bpifpx_result_choice_prime bpr_right_bpifpx_result_choice_prime. S (a + bpr_index_bpifpx_result) = bpr_left_bpifpx_result_choice_prime * bpr_right_bpifpx_result_choice_prime -> bpr_left_bpifpx_result_choice_prime = 1 \/ bpr_right_bpifpx_result_choice_prime = 1)) /\ bpr_value_bpifpx_result = S (a + bpr_index_bpifpx_result)) \/ (~((~(S (a + bpr_index_bpifpx_result) = 1) /\ forall bpr_left_bpifpx_result_choice_prime bpr_right_bpifpx_result_choice_prime. S (a + bpr_index_bpifpx_result) = bpr_left_bpifpx_result_choice_prime * bpr_right_bpifpx_result_choice_prime -> bpr_left_bpifpx_result_choice_prime = 1 \/ bpr_right_bpifpx_result_choice_prime = 1)) /\ bpr_value_bpifpx_result = 1)))))

Structural proof guide

Every offset and length has a beta-coded selector interval.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, primorial_interval_factor_prefix_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00UR primorial_interval_factor_prefix_extend

Direct dependents

BT00UY primorial_prefix_interval_split

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. 0002induction l
  3. 0003exists 0
  4. 0004exists 0
  5. 0005intro i
  6. 0006intro hi
  7. 0007exfalso
  8. 0008cases hi
  9. 0009have hsi : S i = 0
  10. 0010apply add_eq_zero_right
  11. 0011exact hi_witness
  12. 0012apply succ_ne_zero
  13. 0013exact hsi
  14. 0014have hprevious : exists b c. (forall bpr_index_bpifpx_previous. (exists bpr_gap_bpifpx_previous_bound. bpr_gap_bpifpx_previous_bound + S (bpr_index_bpifpx_previous) = l) -> exists bpr_value_bpifpx_previous. ((((exists bpr_height_bpifpx_previous_decoded. bpr_height_bpifpx_previous_decoded + S (bpr_value_bpifpx_previous) = S ((S (bpr_index_bpifpx_previous)) * c)) /\ exists bpr_quotient_bpifpx_previous_decoded. b = bpr_quotient_bpifpx_previous_decoded * S ((S (bpr_index_bpifpx_previous)) * c) + (bpr_value_bpifpx_previous))) /\ (((((~(S (a + bpr_index_bpifpx_previous) = 1) /\ forall bpr_left_bpifpx_previous_choice_prime bpr_right_bpifpx_previous_choice_prime. S (a + bpr_index_bpifpx_previous) = bpr_left_bpifpx_previous_choice_prime * bpr_right_bpifpx_previous_choice_prime -> bpr_left_bpifpx_previous_choice_prime = 1 \/ bpr_right_bpifpx_previous_choice_prime = 1)) /\ bpr_value_bpifpx_previous = S (a + bpr_index_bpifpx_previous)) \/ (~((~(S (a + bpr_index_bpifpx_previous) = 1) /\ forall bpr_left_bpifpx_previous_choice_prime bpr_right_bpifpx_previous_choice_prime. S (a + bpr_index_bpifpx_previous) = bpr_left_bpifpx_previous_choice_prime * bpr_right_bpifpx_previous_choice_prime -> bpr_left_bpifpx_previous_choice_prime = 1 \/ bpr_right_bpifpx_previous_choice_prime = 1)) /\ bpr_value_bpifpx_previous = 1)))))
  15. 0015exact IH
  16. 0016cases hprevious
  17. 0017cases hprevious_witness
  18. 0018have hnext : exists b c. (forall bpr_index_bpifpx_successor. (exists bpr_gap_bpifpx_successor_bound. bpr_gap_bpifpx_successor_bound + S (bpr_index_bpifpx_successor) = S l) -> exists bpr_value_bpifpx_successor. ((((exists bpr_height_bpifpx_successor_decoded. bpr_height_bpifpx_successor_decoded + S (bpr_value_bpifpx_successor) = S ((S (bpr_index_bpifpx_successor)) * c)) /\ exists bpr_quotient_bpifpx_successor_decoded. b = bpr_quotient_bpifpx_successor_decoded * S ((S (bpr_index_bpifpx_successor)) * c) + (bpr_value_bpifpx_successor))) /\ (((((~(S (a + bpr_index_bpifpx_successor) = 1) /\ forall bpr_left_bpifpx_successor_choice_prime bpr_right_bpifpx_successor_choice_prime. S (a + bpr_index_bpifpx_successor) = bpr_left_bpifpx_successor_choice_prime * bpr_right_bpifpx_successor_choice_prime -> bpr_left_bpifpx_successor_choice_prime = 1 \/ bpr_right_bpifpx_successor_choice_prime = 1)) /\ bpr_value_bpifpx_successor = S (a + bpr_index_bpifpx_successor)) \/ (~((~(S (a + bpr_index_bpifpx_successor) = 1) /\ forall bpr_left_bpifpx_successor_choice_prime bpr_right_bpifpx_successor_choice_prime. S (a + bpr_index_bpifpx_successor) = bpr_left_bpifpx_successor_choice_prime * bpr_right_bpifpx_successor_choice_prime -> bpr_left_bpifpx_successor_choice_prime = 1 \/ bpr_right_bpifpx_successor_choice_prime = 1)) /\ bpr_value_bpifpx_successor = 1)))))
  19. 0019apply primorial_interval_factor_prefix_extend
  20. 0020exact hprevious_witness_witness
  21. 0021exact hnext