BT00UX

primorial_factor_prefix_restrict_add

Alpha body-checked · checked-use disabled

Restrict a selector prefix of length a+l to its first a entries.

Exact expanded PA statement

forall a b c l. (forall bpr_index_bpfpra_source. (exists bpr_gap_bpfpra_source_bound. bpr_gap_bpfpra_source_bound + S (bpr_index_bpfpra_source) = a + l) -> exists bpr_value_bpfpra_source. ((((exists bpr_height_bpfpra_source_decoded. bpr_height_bpfpra_source_decoded + S (bpr_value_bpfpra_source) = S ((S (bpr_index_bpfpra_source)) * c)) /\ exists bpr_quotient_bpfpra_source_decoded. b = bpr_quotient_bpfpra_source_decoded * S ((S (bpr_index_bpfpra_source)) * c) + (bpr_value_bpfpra_source))) /\ (((((~(S (bpr_index_bpfpra_source) = 1) /\ forall bpr_left_bpfpra_source_choice_prime bpr_right_bpfpra_source_choice_prime. S (bpr_index_bpfpra_source) = bpr_left_bpfpra_source_choice_prime * bpr_right_bpfpra_source_choice_prime -> bpr_left_bpfpra_source_choice_prime = 1 \/ bpr_right_bpfpra_source_choice_prime = 1)) /\ bpr_value_bpfpra_source = S (bpr_index_bpfpra_source)) \/ (~((~(S (bpr_index_bpfpra_source) = 1) /\ forall bpr_left_bpfpra_source_choice_prime bpr_right_bpfpra_source_choice_prime. S (bpr_index_bpfpra_source) = bpr_left_bpfpra_source_choice_prime * bpr_right_bpfpra_source_choice_prime -> bpr_left_bpfpra_source_choice_prime = 1 \/ bpr_right_bpfpra_source_choice_prime = 1)) /\ bpr_value_bpfpra_source = 1))))) -> (forall bpr_index_bpfpra_target. (exists bpr_gap_bpfpra_target_bound. bpr_gap_bpfpra_target_bound + S (bpr_index_bpfpra_target) = a) -> exists bpr_value_bpfpra_target. ((((exists bpr_height_bpfpra_target_decoded. bpr_height_bpfpra_target_decoded + S (bpr_value_bpfpra_target) = S ((S (bpr_index_bpfpra_target)) * c)) /\ exists bpr_quotient_bpfpra_target_decoded. b = bpr_quotient_bpfpra_target_decoded * S ((S (bpr_index_bpfpra_target)) * c) + (bpr_value_bpfpra_target))) /\ (((((~(S (bpr_index_bpfpra_target) = 1) /\ forall bpr_left_bpfpra_target_choice_prime bpr_right_bpfpra_target_choice_prime. S (bpr_index_bpfpra_target) = bpr_left_bpfpra_target_choice_prime * bpr_right_bpfpra_target_choice_prime -> bpr_left_bpfpra_target_choice_prime = 1 \/ bpr_right_bpfpra_target_choice_prime = 1)) /\ bpr_value_bpfpra_target = S (bpr_index_bpfpra_target)) \/ (~((~(S (bpr_index_bpfpra_target) = 1) /\ forall bpr_left_bpfpra_target_choice_prime bpr_right_bpfpra_target_choice_prime. S (bpr_index_bpfpra_target) = bpr_left_bpfpra_target_choice_prime * bpr_right_bpfpra_target_choice_prime -> bpr_left_bpfpra_target_choice_prime = 1 \/ bpr_right_bpfpra_target_choice_prime = 1)) /\ bpr_value_bpfpra_target = 1)))))

Structural proof guide

Restrict a selector prefix of length a+l to its first a entries.

Direct prerequisites: le_add_right, lt_of_lt_of_le. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0013 le_add_right BT001D lt_of_lt_of_le

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. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro hsource
  6. 0006intro i
  7. 0007intro hi
  8. 0008apply hsource
  9. 0009specialize lt_of_lt_of_le i
  10. 0010specialize lt_of_lt_of_le a
  11. 0011specialize lt_of_lt_of_le (a + l)
  12. 0012apply lt_of_lt_of_le
  13. 0013exact hi
  14. 0014specialize le_add_right a
  15. 0015specialize le_add_right l
  16. 0016exact le_add_right