BT00U8

primorial_factor_prefix_exists

Alpha body-checked · checked-use disabled

Every finite length has a beta-coded selector prefix.

Exact expanded PA statement

forall m. exists b c. (forall bpr_index_bpfpx_result. (exists bpr_gap_bpfpx_result_bound. bpr_gap_bpfpx_result_bound + S (bpr_index_bpfpx_result) = m) -> exists bpr_value_bpfpx_result. ((((exists bpr_height_bpfpx_result_decoded. bpr_height_bpfpx_result_decoded + S (bpr_value_bpfpx_result) = S ((S (bpr_index_bpfpx_result)) * c)) /\ exists bpr_quotient_bpfpx_result_decoded. b = bpr_quotient_bpfpx_result_decoded * S ((S (bpr_index_bpfpx_result)) * c) + (bpr_value_bpfpx_result))) /\ (((((~(S (bpr_index_bpfpx_result) = 1) /\ forall bpr_left_bpfpx_result_choice_prime bpr_right_bpfpx_result_choice_prime. S (bpr_index_bpfpx_result) = bpr_left_bpfpx_result_choice_prime * bpr_right_bpfpx_result_choice_prime -> bpr_left_bpfpx_result_choice_prime = 1 \/ bpr_right_bpfpx_result_choice_prime = 1)) /\ bpr_value_bpfpx_result = S (bpr_index_bpfpx_result)) \/ (~((~(S (bpr_index_bpfpx_result) = 1) /\ forall bpr_left_bpfpx_result_choice_prime bpr_right_bpfpx_result_choice_prime. S (bpr_index_bpfpx_result) = bpr_left_bpfpx_result_choice_prime * bpr_right_bpfpx_result_choice_prime -> bpr_left_bpfpx_result_choice_prime = 1 \/ bpr_right_bpfpx_result_choice_prime = 1)) /\ bpr_value_bpfpx_result = 1)))))

Structural proof guide

Every finite length has a beta-coded selector prefix.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, primorial_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 BT00U7 primorial_factor_prefix_extend

Direct dependents

BT00UA primorial_exists

Formal native tactic body

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

  1. 0001induction m
  2. 0002exists 0
  3. 0003exists 0
  4. 0004intro i
  5. 0005intro hi
  6. 0006exfalso
  7. 0007cases hi
  8. 0008have hsi : S i = 0
  9. 0009apply add_eq_zero_right
  10. 0010exact hi_witness
  11. 0011apply succ_ne_zero
  12. 0012exact hsi
  13. 0013have hprevious : exists b c. (forall bpr_index_bpfpx_previous. (exists bpr_gap_bpfpx_previous_bound. bpr_gap_bpfpx_previous_bound + S (bpr_index_bpfpx_previous) = m) -> exists bpr_value_bpfpx_previous. ((((exists bpr_height_bpfpx_previous_decoded. bpr_height_bpfpx_previous_decoded + S (bpr_value_bpfpx_previous) = S ((S (bpr_index_bpfpx_previous)) * c)) /\ exists bpr_quotient_bpfpx_previous_decoded. b = bpr_quotient_bpfpx_previous_decoded * S ((S (bpr_index_bpfpx_previous)) * c) + (bpr_value_bpfpx_previous))) /\ (((((~(S (bpr_index_bpfpx_previous) = 1) /\ forall bpr_left_bpfpx_previous_choice_prime bpr_right_bpfpx_previous_choice_prime. S (bpr_index_bpfpx_previous) = bpr_left_bpfpx_previous_choice_prime * bpr_right_bpfpx_previous_choice_prime -> bpr_left_bpfpx_previous_choice_prime = 1 \/ bpr_right_bpfpx_previous_choice_prime = 1)) /\ bpr_value_bpfpx_previous = S (bpr_index_bpfpx_previous)) \/ (~((~(S (bpr_index_bpfpx_previous) = 1) /\ forall bpr_left_bpfpx_previous_choice_prime bpr_right_bpfpx_previous_choice_prime. S (bpr_index_bpfpx_previous) = bpr_left_bpfpx_previous_choice_prime * bpr_right_bpfpx_previous_choice_prime -> bpr_left_bpfpx_previous_choice_prime = 1 \/ bpr_right_bpfpx_previous_choice_prime = 1)) /\ bpr_value_bpfpx_previous = 1)))))
  14. 0014exact IH
  15. 0015cases hprevious
  16. 0016cases hprevious_witness
  17. 0017have hnext : exists b c. (forall bpr_index_bpfpx_successor. (exists bpr_gap_bpfpx_successor_bound. bpr_gap_bpfpx_successor_bound + S (bpr_index_bpfpx_successor) = S m) -> exists bpr_value_bpfpx_successor. ((((exists bpr_height_bpfpx_successor_decoded. bpr_height_bpfpx_successor_decoded + S (bpr_value_bpfpx_successor) = S ((S (bpr_index_bpfpx_successor)) * c)) /\ exists bpr_quotient_bpfpx_successor_decoded. b = bpr_quotient_bpfpx_successor_decoded * S ((S (bpr_index_bpfpx_successor)) * c) + (bpr_value_bpfpx_successor))) /\ (((((~(S (bpr_index_bpfpx_successor) = 1) /\ forall bpr_left_bpfpx_successor_choice_prime bpr_right_bpfpx_successor_choice_prime. S (bpr_index_bpfpx_successor) = bpr_left_bpfpx_successor_choice_prime * bpr_right_bpfpx_successor_choice_prime -> bpr_left_bpfpx_successor_choice_prime = 1 \/ bpr_right_bpfpx_successor_choice_prime = 1)) /\ bpr_value_bpfpx_successor = S (bpr_index_bpfpx_successor)) \/ (~((~(S (bpr_index_bpfpx_successor) = 1) /\ forall bpr_left_bpfpx_successor_choice_prime bpr_right_bpfpx_successor_choice_prime. S (bpr_index_bpfpx_successor) = bpr_left_bpfpx_successor_choice_prime * bpr_right_bpfpx_successor_choice_prime -> bpr_left_bpfpx_successor_choice_prime = 1 \/ bpr_right_bpfpx_successor_choice_prime = 1)) /\ bpr_value_bpfpx_successor = 1)))))
  18. 0018apply primorial_factor_prefix_extend
  19. 0019exact hprevious_witness_witness
  20. 0020exact hnext