PA009J

scaled_orbit_closed_unused_mate

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

Shifted orbit closure transfers omission across a decoded back edge.

Exact expanded PA statement

forall u v b c l i j. (forall espo_position_unused_closed espo_source_unused_closed espo_mate_unused_closed. (exists wpo_gap_unused_closed_position_bound. wpo_gap_unused_closed_position_bound + S (espo_position_unused_closed) = l) -> (((exists wpo_beta_height_unused_closed_source_entry. wpo_beta_height_unused_closed_source_entry + S (espo_source_unused_closed) = S ((S (espo_position_unused_closed)) * c)) /\ exists wpo_beta_quotient_unused_closed_source_entry. b = wpo_beta_quotient_unused_closed_source_entry * S ((S (espo_position_unused_closed)) * c) + (espo_source_unused_closed))) -> (((exists wpo_beta_height_unused_closed_scaled_entry. wpo_beta_height_unused_closed_scaled_entry + S (S espo_mate_unused_closed) = S ((S (espo_source_unused_closed)) * v)) /\ exists wpo_beta_quotient_unused_closed_scaled_entry. u = wpo_beta_quotient_unused_closed_scaled_entry * S ((S (espo_source_unused_closed)) * v) + (S espo_mate_unused_closed))) -> exists espo_mate_position_unused_closed. ((exists wpo_gap_unused_closed_mate_bound. wpo_gap_unused_closed_mate_bound + S (espo_mate_position_unused_closed) = l) /\ (((exists wpo_beta_height_unused_closed_mate_entry. wpo_beta_height_unused_closed_mate_entry + S (espo_mate_unused_closed) = S ((S (espo_mate_position_unused_closed)) * c)) /\ exists wpo_beta_quotient_unused_closed_mate_entry. b = wpo_beta_quotient_unused_closed_mate_entry * S ((S (espo_mate_position_unused_closed)) * c) + (espo_mate_unused_closed))))) -> (~(exists wpo_index_unused_source_omit_contains. ((exists wpo_gap_unused_source_omit_contains_bound. wpo_gap_unused_source_omit_contains_bound + S (wpo_index_unused_source_omit_contains) = l) /\ (((exists wpo_beta_height_unused_source_omit_contains_entry. wpo_beta_height_unused_source_omit_contains_entry + S (i) = S ((S (wpo_index_unused_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_unused_source_omit_contains_entry. b = wpo_beta_quotient_unused_source_omit_contains_entry * S ((S (wpo_index_unused_source_omit_contains)) * c) + (i)))))) -> (((exists wpo_beta_height_unused_back. wpo_beta_height_unused_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_unused_back. u = wpo_beta_quotient_unused_back * S ((S (j)) * v) + (S i))) -> (~(exists wpo_index_unused_mate_omit_contains. ((exists wpo_gap_unused_mate_omit_contains_bound. wpo_gap_unused_mate_omit_contains_bound + S (wpo_index_unused_mate_omit_contains) = l) /\ (((exists wpo_beta_height_unused_mate_omit_contains_entry. wpo_beta_height_unused_mate_omit_contains_entry + S (j) = S ((S (wpo_index_unused_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_unused_mate_omit_contains_entry. b = wpo_beta_quotient_unused_mate_omit_contains_entry * S ((S (wpo_index_unused_mate_omit_contains)) * c) + (j))))))

Structural proof guide

Generated structural guide

Shifted orbit closure transfers omission across a decoded back edge.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

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

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA009O scaled_inverse_pair_order_choose_append

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 u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro i
  7. 0007intro j
  8. 0008intro hclosed
  9. 0009intro hiomit
  10. 0010intro hback
  11. 0011intro hjcontains
  12. 0012cases hjcontains
  13. 0013cases hjcontains_witness
  14. 0014have hioccurs : exists wpo_index_unused_source_occurs. ((exists wpo_gap_unused_source_occurs_bound. wpo_gap_unused_source_occurs_bound + S (wpo_index_unused_source_occurs) = l) /\ (((exists wpo_beta_height_unused_source_occurs_entry. wpo_beta_height_unused_source_occurs_entry + S (i) = S ((S (wpo_index_unused_source_occurs)) * c)) /\ exists wpo_beta_quotient_unused_source_occurs_entry. b = wpo_beta_quotient_unused_source_occurs_entry * S ((S (wpo_index_unused_source_occurs)) * c) + (i))))
  15. 0015specialize hclosed x
  16. 0016specialize hclosed j
  17. 0017specialize hclosed i
  18. 0018apply hclosed
  19. 0019exact hjcontains_witness_left
  20. 0020exact hjcontains_witness_right
  21. 0021exact hback
  22. 0022cases hioccurs
  23. 0023cases hioccurs_witness
  24. 0024apply hiomit
  25. 0025exists x1
  26. 0026split
  27. 0027exact hioccurs_witness_left
  28. 0028exact hioccurs_witness_right