PA008W

injective_prefix_zero

Alpha v16 checked-use theorem · independently closed; not Stable

Decoded-prefix injectivity is vacuous at length zero.

Exact expanded PA statement

forall b c. (forall wpo_injective_left_wpoi_zero_injective wpo_injective_right_wpoi_zero_injective wpo_injective_value_wpoi_zero_injective. (exists wpo_gap_wpoi_zero_injective_left_bound. wpo_gap_wpoi_zero_injective_left_bound + S (wpo_injective_left_wpoi_zero_injective) = 0) -> (exists wpo_gap_wpoi_zero_injective_right_bound. wpo_gap_wpoi_zero_injective_right_bound + S (wpo_injective_right_wpoi_zero_injective) = 0) -> (((exists wpo_beta_height_wpoi_zero_injective_left_entry. wpo_beta_height_wpoi_zero_injective_left_entry + S (wpo_injective_value_wpoi_zero_injective) = S ((S (wpo_injective_left_wpoi_zero_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_injective_left_entry. b = wpo_beta_quotient_wpoi_zero_injective_left_entry * S ((S (wpo_injective_left_wpoi_zero_injective)) * c) + (wpo_injective_value_wpoi_zero_injective))) -> (((exists wpo_beta_height_wpoi_zero_injective_right_entry. wpo_beta_height_wpoi_zero_injective_right_entry + S (wpo_injective_value_wpoi_zero_injective) = S ((S (wpo_injective_right_wpoi_zero_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_injective_right_entry. b = wpo_beta_quotient_wpoi_zero_injective_right_entry * S ((S (wpo_injective_right_wpoi_zero_injective)) * c) + (wpo_injective_value_wpoi_zero_injective))) -> wpo_injective_left_wpoi_zero_injective = wpo_injective_right_wpoi_zero_injective)

Structural proof guide

Generated structural guide

Decoded-prefix injectivity is vacuous at length zero.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Direct dependents

PA008X scaled_pair_order_state_zero PA00AA pair_order_state_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro q
  4. 0004intro r
  5. 0005intro w
  6. 0006intro hq
  7. 0007intro hr
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010exfalso
  11. 0011cases hq
  12. 0012have hsq : S q = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S q)
  15. 0015apply add_eq_zero_right
  16. 0016exact hq_witness
  17. 0017specialize succ_ne_zero q
  18. 0018apply succ_ne_zero
  19. 0019exact hsq