PA009O

scaled_inverse_pair_order_choose_append

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

Choose one omitted fixed-point-free scaled orbit and append its two sources adjacently.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall p a n u v b c l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_espo_choose_prime esi_prime_right_espo_choose_prime. p = esi_prime_left_espo_choose_prime * esi_prime_right_espo_choose_prime -> esi_prime_left_espo_choose_prime = 1 \/ esi_prime_right_espo_choose_prime = 1)) -> ~(exists qr_x_espo_choose_nonresidue. exists qr_u_espo_choose_nonresidue qr_v_espo_choose_nonresidue. qr_x_espo_choose_nonresidue * qr_x_espo_choose_nonresidue + p * qr_u_espo_choose_nonresidue = a + p * qr_v_espo_choose_nonresidue) -> (forall esip_index_espo_choose_prefix. (exists esip_gap_espo_choose_prefix_prefix_bound. esip_gap_espo_choose_prefix_prefix_bound + S (esip_index_espo_choose_prefix) = n) -> exists esip_mate_espo_choose_prefix. ((((exists ff_h_esip_espo_choose_prefix_entry. ff_h_esip_espo_choose_prefix_entry + S (esip_mate_espo_choose_prefix) = S ((S (esip_index_espo_choose_prefix)) * v)) /\ exists ff_q_esip_espo_choose_prefix_entry. u = ff_q_esip_espo_choose_prefix_entry * S ((S (esip_index_espo_choose_prefix)) * v) + (esip_mate_espo_choose_prefix))) /\ ((exists esip_gap_espo_choose_prefix_relation_index_bound. esip_gap_espo_choose_prefix_relation_index_bound + S (esip_index_espo_choose_prefix) = n) /\ ((((~((S esip_index_espo_choose_prefix) = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_left_bound. esip_gap_espo_choose_prefix_relation_scaled_left_bound + S (S esip_index_espo_choose_prefix) = p))) /\ (((~(esip_mate_espo_choose_prefix = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_right_bound. esip_gap_espo_choose_prefix_relation_scaled_right_bound + S (esip_mate_espo_choose_prefix) = p))) /\ (exists esi_mod_left_espo_choose_prefix_relation_scaled_mod esi_mod_right_espo_choose_prefix_relation_scaled_mod. ((S esip_index_espo_choose_prefix) * esip_mate_espo_choose_prefix) + p * esi_mod_left_espo_choose_prefix_relation_scaled_mod = (a) + p * esi_mod_right_espo_choose_prefix_relation_scaled_mod))))))) -> (exists wpo_gap_choose_short. wpo_gap_choose_short + S (l) = n) -> (forall espo_position_step_closed_before espo_source_step_closed_before espo_mate_step_closed_before. (exists wpo_gap_step_closed_before_position_bound. wpo_gap_step_closed_before_position_bound + S (espo_position_step_closed_before) = l) -> (((exists wpo_beta_height_step_closed_before_source_entry. wpo_beta_height_step_closed_before_source_entry + S (espo_source_step_closed_before) = S ((S (espo_position_step_closed_before)) * c)) /\ exists wpo_beta_quotient_step_closed_before_source_entry. b = wpo_beta_quotient_step_closed_before_source_entry * S ((S (espo_position_step_closed_before)) * c) + (espo_source_step_closed_before))) -> (((exists wpo_beta_height_step_closed_before_scaled_entry. wpo_beta_height_step_closed_before_scaled_entry + S (S espo_mate_step_closed_before) = S ((S (espo_source_step_closed_before)) * v)) /\ exists wpo_beta_quotient_step_closed_before_scaled_entry. u = wpo_beta_quotient_step_closed_before_scaled_entry * S ((S (espo_source_step_closed_before)) * v) + (S espo_mate_step_closed_before))) -> exists espo_mate_position_step_closed_before. ((exists wpo_gap_step_closed_before_mate_bound. wpo_gap_step_closed_before_mate_bound + S (espo_mate_position_step_closed_before) = l) /\ (((exists wpo_beta_height_step_closed_before_mate_entry. wpo_beta_height_step_closed_before_mate_entry + S (espo_mate_step_closed_before) = S ((S (espo_mate_position_step_closed_before)) * c)) /\ exists wpo_beta_quotient_step_closed_before_mate_entry. b = wpo_beta_quotient_step_closed_before_mate_entry * S ((S (espo_mate_position_step_closed_before)) * c) + (espo_mate_step_closed_before))))) -> (forall wpo_injective_left_step_injective_before wpo_injective_right_step_injective_before wpo_injective_value_step_injective_before. (exists wpo_gap_step_injective_before_left_bound. wpo_gap_step_injective_before_left_bound + S (wpo_injective_left_step_injective_before) = l) -> (exists wpo_gap_step_injective_before_right_bound. wpo_gap_step_injective_before_right_bound + S (wpo_injective_right_step_injective_before) = l) -> (((exists wpo_beta_height_step_injective_before_left_entry. wpo_beta_height_step_injective_before_left_entry + S (wpo_injective_value_step_injective_before) = S ((S (wpo_injective_left_step_injective_before)) * c)) /\ exists wpo_beta_quotient_step_injective_before_left_entry. b = wpo_beta_quotient_step_injective_before_left_entry * S ((S (wpo_injective_left_step_injective_before)) * c) + (wpo_injective_value_step_injective_before))) -> (((exists wpo_beta_height_step_injective_before_right_entry. wpo_beta_height_step_injective_before_right_entry + S (wpo_injective_value_step_injective_before) = S ((S (wpo_injective_right_step_injective_before)) * c)) /\ exists wpo_beta_quotient_step_injective_before_right_entry. b = wpo_beta_quotient_step_injective_before_right_entry * S ((S (wpo_injective_right_step_injective_before)) * c) + (wpo_injective_value_step_injective_before))) -> wpo_injective_left_step_injective_before = wpo_injective_right_step_injective_before) -> (exists z d i j. ((((((exists wpo_beta_height_step_trace_first. wpo_beta_height_step_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_step_trace_first. z = wpo_beta_quotient_step_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_step_trace_second. wpo_beta_height_step_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_step_trace_second. z = wpo_beta_quotient_step_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_step_trace wpo_old_value_step_trace. (exists wpo_gap_step_trace_old_bound. wpo_gap_step_trace_old_bound + S (wpo_old_index_step_trace) = l) -> (((exists wpo_beta_height_step_trace_old_entry. wpo_beta_height_step_trace_old_entry + S (wpo_old_value_step_trace) = S ((S (wpo_old_index_step_trace)) * c)) /\ exists wpo_beta_quotient_step_trace_old_entry. b = wpo_beta_quotient_step_trace_old_entry * S ((S (wpo_old_index_step_trace)) * c) + (wpo_old_value_step_trace))) -> (((exists wpo_beta_height_step_trace_new_entry. wpo_beta_height_step_trace_new_entry + S (wpo_old_value_step_trace) = S ((S (wpo_old_index_step_trace)) * d)) /\ exists wpo_beta_quotient_step_trace_new_entry. z = wpo_beta_quotient_step_trace_new_entry * S ((S (wpo_old_index_step_trace)) * d) + (wpo_old_value_step_trace))))))) /\ (((exists wpo_gap_chosen_i_bound. wpo_gap_chosen_i_bound + S (i) = n) /\ (((exists wpo_gap_chosen_j_bound. wpo_gap_chosen_j_bound + S (j) = n) /\ (((~(exists wpo_index_chosen_i_omit_contains. ((exists wpo_gap_chosen_i_omit_contains_bound. wpo_gap_chosen_i_omit_contains_bound + S (wpo_index_chosen_i_omit_contains) = l) /\ (((exists wpo_beta_height_chosen_i_omit_contains_entry. wpo_beta_height_chosen_i_omit_contains_entry + S (i) = S ((S (wpo_index_chosen_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_chosen_i_omit_contains_entry. b = wpo_beta_quotient_chosen_i_omit_contains_entry * S ((S (wpo_index_chosen_i_omit_contains)) * c) + (i)))))) /\ (((~(exists wpo_index_step_j_omit_contains. ((exists wpo_gap_step_j_omit_contains_bound. wpo_gap_step_j_omit_contains_bound + S (wpo_index_step_j_omit_contains) = l) /\ (((exists wpo_beta_height_step_j_omit_contains_entry. wpo_beta_height_step_j_omit_contains_entry + S (j) = S ((S (wpo_index_step_j_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_j_omit_contains_entry. b = wpo_beta_quotient_step_j_omit_contains_entry * S ((S (wpo_index_step_j_omit_contains)) * c) + (j)))))) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_chosen_forward. wpo_beta_height_chosen_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_chosen_forward. u = wpo_beta_quotient_chosen_forward * S ((S (i)) * v) + (S j))) /\ (((((exists wpo_beta_height_chosen_back. wpo_beta_height_chosen_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_back. u = wpo_beta_quotient_chosen_back * S ((S (j)) * v) + (S i))) /\ (((forall espo_position_step_closed_after espo_source_step_closed_after espo_mate_step_closed_after. (exists wpo_gap_step_closed_after_position_bound. wpo_gap_step_closed_after_position_bound + S (espo_position_step_closed_after) = S (S l)) -> (((exists wpo_beta_height_step_closed_after_source_entry. wpo_beta_height_step_closed_after_source_entry + S (espo_source_step_closed_after) = S ((S (espo_position_step_closed_after)) * d)) /\ exists wpo_beta_quotient_step_closed_after_source_entry. z = wpo_beta_quotient_step_closed_after_source_entry * S ((S (espo_position_step_closed_after)) * d) + (espo_source_step_closed_after))) -> (((exists wpo_beta_height_step_closed_after_scaled_entry. wpo_beta_height_step_closed_after_scaled_entry + S (S espo_mate_step_closed_after) = S ((S (espo_source_step_closed_after)) * v)) /\ exists wpo_beta_quotient_step_closed_after_scaled_entry. u = wpo_beta_quotient_step_closed_after_scaled_entry * S ((S (espo_source_step_closed_after)) * v) + (S espo_mate_step_closed_after))) -> exists espo_mate_position_step_closed_after. ((exists wpo_gap_step_closed_after_mate_bound. wpo_gap_step_closed_after_mate_bound + S (espo_mate_position_step_closed_after) = S (S l)) /\ (((exists wpo_beta_height_step_closed_after_mate_entry. wpo_beta_height_step_closed_after_mate_entry + S (espo_mate_step_closed_after) = S ((S (espo_mate_position_step_closed_after)) * d)) /\ exists wpo_beta_quotient_step_closed_after_mate_entry. z = wpo_beta_quotient_step_closed_after_mate_entry * S ((S (espo_mate_position_step_closed_after)) * d) + (espo_mate_step_closed_after))))) /\ (forall wpo_injective_left_step_injective_after wpo_injective_right_step_injective_after wpo_injective_value_step_injective_after. (exists wpo_gap_step_injective_after_left_bound. wpo_gap_step_injective_after_left_bound + S (wpo_injective_left_step_injective_after) = S (S l)) -> (exists wpo_gap_step_injective_after_right_bound. wpo_gap_step_injective_after_right_bound + S (wpo_injective_right_step_injective_after) = S (S l)) -> (((exists wpo_beta_height_step_injective_after_left_entry. wpo_beta_height_step_injective_after_left_entry + S (wpo_injective_value_step_injective_after) = S ((S (wpo_injective_left_step_injective_after)) * d)) /\ exists wpo_beta_quotient_step_injective_after_left_entry. z = wpo_beta_quotient_step_injective_after_left_entry * S ((S (wpo_injective_left_step_injective_after)) * d) + (wpo_injective_value_step_injective_after))) -> (((exists wpo_beta_height_step_injective_after_right_entry. wpo_beta_height_step_injective_after_right_entry + S (wpo_injective_value_step_injective_after) = S ((S (wpo_injective_right_step_injective_after)) * d)) /\ exists wpo_beta_quotient_step_injective_after_right_entry. z = wpo_beta_quotient_step_injective_after_right_entry * S ((S (wpo_injective_right_step_injective_after)) * d) + (wpo_injective_value_step_injective_after))) -> wpo_injective_left_step_injective_after = wpo_injective_right_step_injective_after)))))))))))))))))))

Structural proof guide

Generated structural guide

Choose one omitted fixed-point-free scaled orbit and append its two sources adjacently.

Use the direct prerequisites scaled_inverse_prefix_choose_omitted_orbit, scaled_orbit_closed_unused_mate, beta_prefix_append_two_exists, beta_prefix_append_two_scaled_orbit_closed, beta_prefix_append_two_injective as previously established PA formulas.

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

Referenced ingredients

PA009I scaled_inverse_prefix_choose_omitted_orbit PA009J scaled_orbit_closed_unused_mate PA009K beta_prefix_append_two_exists PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective

Proof neighborhood

Direct dependencies

PA009I scaled_inverse_prefix_choose_omitted_orbit PA009J scaled_orbit_closed_unused_mate PA009K beta_prefix_append_two_exists PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective

Direct dependents

PA009T scaled_inverse_pair_order_paired_state_step

Formal native tactic body

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

Read the argument

Proof checkpoints

114 script commands · 34 reading checkpoints · 6 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (5)
scaled inverse prefix choose omitted orbitscaled orbit closed unused matebeta prefix append two existsbeta prefix append two scaled orbit closedbeta prefix append two injective

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro l
  9. L9
    intro hpn
  10. L10
    intro hp
02Fix variables and assumptionsL11–15

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hnotqres
  2. L12
    intro hprefix
  3. L13
    intro hshort
  4. L14
    intro hclosed
  5. L15
    intro hinjective
03Establish hchosenL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse prefix choose omitted orbit.

  1. L16
    have hchosen : ∃ i. ∃ j. Lt(i,n) ∧ (¬ContainsPrefix(b,c,l,i) ∧ (Lt(j,n) ∧ (¬i = j ∧ (BetaAt(u,v,i,S j) ∧ BetaAt(u,v,j,S i)))))Definitions: LtBetaAtContainsPrefix
  2. L17
    specialize scaled_inverse_prefix_choose_omitted_orbit p
  3. L18
    specialize scaled_inverse_prefix_choose_omitted_orbit a
  4. L19
    specialize scaled_inverse_prefix_choose_omitted_orbit n
  5. L20
    specialize scaled_inverse_prefix_choose_omitted_orbit u
  6. L21
    specialize scaled_inverse_prefix_choose_omitted_orbit v
  7. L22
    specialize scaled_inverse_prefix_choose_omitted_orbit b
  8. L23
    specialize scaled_inverse_prefix_choose_omitted_orbit c
  9. L24
    specialize scaled_inverse_prefix_choose_omitted_orbit l
  10. L25
    apply scaled_inverse_prefix_choose_omitted_orbit
04Use earlier factsL26–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    exact hpn
  2. L27
    exact hp
  3. L28
    exact hnotqres
  4. L29
    exact hprefix
  5. L30
    exact hshort
05Separate the logical casesL31–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hchosen
  2. L32
    cases hchosen_witness
06Establish hpartsL33–34

Establish this local claim before using it. It is not an additional assumption.

  1. L33
    have hparts : Lt(x,n) ∧ (¬ContainsPrefix(b,c,l,x) ∧ (Lt(x1,n) ∧ (¬x = x1 ∧ (BetaAt(u,v,x,S x1) ∧ BetaAt(u,v,x1,S x)))))Definitions: LtBetaAtContainsPrefix
  2. L34
    exact hchosen_witness_witness
07Separate the logical casesL35–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    cases hparts
  2. L36
    cases hparts_right
  3. L37
    cases hparts_right_right
  4. L38
    cases hparts_right_right_right
  5. L39
    cases hparts_right_right_right_right
08Establish hjomitL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled orbit closed unused mate.

  1. L40
    have hjomit : ~(exists wpo_index_witness_j_omit_contains. ((exists wpo_gap_witness_j_omit_contains_bound. wpo_gap_witness_j_omit_contains_bound + S (wpo_index_witness_j_omit_contains) = l) /\ (((exists wpo_beta_height_witness_j_omit_contains_entry. wpo_beta_height_witness_j_omit_contains_entry + S (x1) = S ((S (wpo_index_witness_j_omit_contains)) * c)) /\ exists wpo_beta_quotient_witness_j_omit_contains_entry. b = wpo_beta_quotient_witness_j_omit_contains_entry * S ((S (wpo_index_witness_j_omit_contains)) * c) + (x1)))))
  2. L41
    intro hjcontains
  3. L42
    specialize scaled_orbit_closed_unused_mate u
  4. L43
    specialize scaled_orbit_closed_unused_mate v
  5. L44
    specialize scaled_orbit_closed_unused_mate b
  6. L45
    specialize scaled_orbit_closed_unused_mate c
  7. L46
    specialize scaled_orbit_closed_unused_mate l
  8. L47
    specialize scaled_orbit_closed_unused_mate x
  9. L48
    specialize scaled_orbit_closed_unused_mate x1
  10. L49
    apply scaled_orbit_closed_unused_mate
09Use earlier factsL50–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    exact hclosed
  2. L51
    exact hparts_right_left
  3. L52
    exact hparts_right_right_right_right_right
  4. L53
    exact hjcontains
10Establish happendL54–60

Establish this local claim before using it. It is not an additional assumption.

  1. L54
    have happend : ∃ z. ∃ d. BetaAt(z,d,l,x) ∧ (BetaAt(z,d,S l,x1) ∧ (∀ y. ∀ n. Lt(y,l) → BetaAt(b,c,y,n) → BetaAt(z,d,y,n)))Definitions: LtBetaAt
  2. L55
    specialize beta_prefix_append_two_exists b
  3. L56
    specialize beta_prefix_append_two_exists c
  4. L57
    specialize beta_prefix_append_two_exists l
  5. L58
    specialize beta_prefix_append_two_exists x
  6. L59
    specialize beta_prefix_append_two_exists x1
  7. L60
    exact beta_prefix_append_two_exists
11Separate the logical casesL61–62

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L61
    cases happend
  2. L62
    cases happend_witness
12Establish hclosed_afterL63–72

Establish this local claim before using it. It is not an additional assumption.

  1. L63
    have hclosed_after : ∀ espo_position_witness_closed_after. ∀ espo_source_witness_closed_after. ∀ espo_mate_witness_closed_after. Lt(espo_position_witness_closed_after,S S l) → BetaAt(x2,x3,espo_position_witness_closed_after,espo_source_witness_closed_after) → BetaAt(u,v,espo_source_witness_closed_after,S espo_mate_witness_closed_after) → ContainsPrefix(x2,x3,S S l,espo_mate_witness_closed_after)Definitions: LtBetaAtContainsPrefix
  2. L64
    specialize beta_prefix_append_two_scaled_orbit_closed u
  3. L65
    specialize beta_prefix_append_two_scaled_orbit_closed v
  4. L66
    specialize beta_prefix_append_two_scaled_orbit_closed b
  5. L67
    specialize beta_prefix_append_two_scaled_orbit_closed c
  6. L68
    specialize beta_prefix_append_two_scaled_orbit_closed x2
  7. L69
    specialize beta_prefix_append_two_scaled_orbit_closed x3
  8. L70
    specialize beta_prefix_append_two_scaled_orbit_closed l
  9. L71
    specialize beta_prefix_append_two_scaled_orbit_closed x
  10. L72
    specialize beta_prefix_append_two_scaled_orbit_closed x1
13Use earlier factsL73–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L73
    apply beta_prefix_append_two_scaled_orbit_closed
  2. L74
    exact happend_witness_witness
  3. L75
    exact hclosed
  4. L76
    exact hparts_right_right_right_right_left
  5. L77
    exact hparts_right_right_right_right_right
14Establish hinjective_afterL78–87

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix append two injective.

  1. L78
    have hinjective_after : InjectivePrefix(x2,x3,S S l)Definitions: InjectivePrefix
  2. L79
    specialize beta_prefix_append_two_injective b
  3. L80
    specialize beta_prefix_append_two_injective c
  4. L81
    specialize beta_prefix_append_two_injective x2
  5. L82
    specialize beta_prefix_append_two_injective x3
  6. L83
    specialize beta_prefix_append_two_injective l
  7. L84
    specialize beta_prefix_append_two_injective x
  8. L85
    specialize beta_prefix_append_two_injective x1
  9. L86
    apply beta_prefix_append_two_injective
  10. L87
    exact happend_witness_witness
15Use earlier factsL88–91

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L88
    exact hinjective
  2. L89
    exact hparts_right_left
  3. L90
    exact hjomit
  4. L91
    exact hparts_right_right_right_left
16Construct an explicit witnessL92–95

Supply the displayed value, then prove that it has the required property.

  1. L92
    exists x2
  2. L93
    exists x3
  3. L94
    exists x
  4. L95
    exists x1
17Separate the logical casesL96–96

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L96
    split
18Use earlier factsL97–97

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L97
    exact happend_witness_witness
19Separate the logical casesL98–98

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L98
    split
20Use earlier factsL99–99

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L99
    exact hparts_left
21Separate the logical casesL100–100

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L100
    split
22Use earlier factsL101–101

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L101
    exact hparts_right_right_left
23Separate the logical casesL102–102

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L102
    split
24Use earlier factsL103–103

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L103
    exact hparts_right_left
25Separate the logical casesL104–104

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L104
    split
26Use earlier factsL105–105

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L105
    exact hjomit
27Separate the logical casesL106–106

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L106
    split
28Use earlier factsL107–107

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L107
    exact hparts_right_right_right_left
29Separate the logical casesL108–108

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L108
    split
30Use earlier factsL109–109

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L109
    exact hparts_right_right_right_right_left
31Separate the logical casesL110–110

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L110
    split
32Use earlier factsL111–111

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L111
    exact hparts_right_right_right_right_right
33Separate the logical casesL112–112

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L112
    split
34Use earlier factsL113–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L113
    exact hclosed_after
  2. L114
    exact hinjective_after

Library-wide reading audit

Original exact command ledger · 114 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro l
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hnotqres
  12. 0012intro hprefix
  13. 0013intro hshort
  14. 0014intro hclosed
  15. 0015intro hinjective
  16. 0016have hchosen : exists i j. ((exists wpo_gap_chosen_i_bound. wpo_gap_chosen_i_bound + S (i) = n) /\ (((~(exists wpo_index_chosen_i_omit_contains. ((exists wpo_gap_chosen_i_omit_contains_bound. wpo_gap_chosen_i_omit_contains_bound + S (wpo_index_chosen_i_omit_contains) = l) /\ (((exists wpo_beta_height_chosen_i_omit_contains_entry. wpo_beta_height_chosen_i_omit_contains_entry + S (i) = S ((S (wpo_index_chosen_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_chosen_i_omit_contains_entry. b = wpo_beta_quotient_chosen_i_omit_contains_entry * S ((S (wpo_index_chosen_i_omit_contains)) * c) + (i)))))) /\ (((exists wpo_gap_chosen_j_bound. wpo_gap_chosen_j_bound + S (j) = n) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_chosen_forward. wpo_beta_height_chosen_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_chosen_forward. u = wpo_beta_quotient_chosen_forward * S ((S (i)) * v) + (S j))) /\ (((exists wpo_beta_height_chosen_back. wpo_beta_height_chosen_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_back. u = wpo_beta_quotient_chosen_back * S ((S (j)) * v) + (S i))))))))))))
  17. 0017specialize scaled_inverse_prefix_choose_omitted_orbit p
  18. 0018specialize scaled_inverse_prefix_choose_omitted_orbit a
  19. 0019specialize scaled_inverse_prefix_choose_omitted_orbit n
  20. 0020specialize scaled_inverse_prefix_choose_omitted_orbit u
  21. 0021specialize scaled_inverse_prefix_choose_omitted_orbit v
  22. 0022specialize scaled_inverse_prefix_choose_omitted_orbit b
  23. 0023specialize scaled_inverse_prefix_choose_omitted_orbit c
  24. 0024specialize scaled_inverse_prefix_choose_omitted_orbit l
  25. 0025apply scaled_inverse_prefix_choose_omitted_orbit
  26. 0026exact hpn
  27. 0027exact hp
  28. 0028exact hnotqres
  29. 0029exact hprefix
  30. 0030exact hshort
  31. 0031cases hchosen
  32. 0032cases hchosen_witness
  33. 0033have hparts : ((exists wpo_gap_witness_i_bound. wpo_gap_witness_i_bound + S (x) = n) /\ (((~(exists wpo_index_witness_i_omit_contains. ((exists wpo_gap_witness_i_omit_contains_bound. wpo_gap_witness_i_omit_contains_bound + S (wpo_index_witness_i_omit_contains) = l) /\ (((exists wpo_beta_height_witness_i_omit_contains_entry. wpo_beta_height_witness_i_omit_contains_entry + S (x) = S ((S (wpo_index_witness_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_witness_i_omit_contains_entry. b = wpo_beta_quotient_witness_i_omit_contains_entry * S ((S (wpo_index_witness_i_omit_contains)) * c) + (x)))))) /\ (((exists wpo_gap_witness_j_bound. wpo_gap_witness_j_bound + S (x1) = n) /\ (((~(x = x1)) /\ (((((exists wpo_beta_height_witness_forward. wpo_beta_height_witness_forward + S (S x1) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_witness_forward. u = wpo_beta_quotient_witness_forward * S ((S (x)) * v) + (S x1))) /\ (((exists wpo_beta_height_witness_back. wpo_beta_height_witness_back + S (S x) = S ((S (x1)) * v)) /\ exists wpo_beta_quotient_witness_back. u = wpo_beta_quotient_witness_back * S ((S (x1)) * v) + (S x))))))))))))
  34. 0034exact hchosen_witness_witness
  35. 0035cases hparts
  36. 0036cases hparts_right
  37. 0037cases hparts_right_right
  38. 0038cases hparts_right_right_right
  39. 0039cases hparts_right_right_right_right
  40. 0040have hjomit : ~(exists wpo_index_witness_j_omit_contains. ((exists wpo_gap_witness_j_omit_contains_bound. wpo_gap_witness_j_omit_contains_bound + S (wpo_index_witness_j_omit_contains) = l) /\ (((exists wpo_beta_height_witness_j_omit_contains_entry. wpo_beta_height_witness_j_omit_contains_entry + S (x1) = S ((S (wpo_index_witness_j_omit_contains)) * c)) /\ exists wpo_beta_quotient_witness_j_omit_contains_entry. b = wpo_beta_quotient_witness_j_omit_contains_entry * S ((S (wpo_index_witness_j_omit_contains)) * c) + (x1)))))
  41. 0041intro hjcontains
  42. 0042specialize scaled_orbit_closed_unused_mate u
  43. 0043specialize scaled_orbit_closed_unused_mate v
  44. 0044specialize scaled_orbit_closed_unused_mate b
  45. 0045specialize scaled_orbit_closed_unused_mate c
  46. 0046specialize scaled_orbit_closed_unused_mate l
  47. 0047specialize scaled_orbit_closed_unused_mate x
  48. 0048specialize scaled_orbit_closed_unused_mate x1
  49. 0049apply scaled_orbit_closed_unused_mate
  50. 0050exact hclosed
  51. 0051exact hparts_right_left
  52. 0052exact hparts_right_right_right_right_right
  53. 0053exact hjcontains
  54. 0054have happend : exists z d. (((((exists wpo_beta_height_witness_exists_trace_first. wpo_beta_height_witness_exists_trace_first + S (x) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_witness_exists_trace_first. z = wpo_beta_quotient_witness_exists_trace_first * S ((S (l)) * d) + (x))) /\ ((((exists wpo_beta_height_witness_exists_trace_second. wpo_beta_height_witness_exists_trace_second + S (x1) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_witness_exists_trace_second. z = wpo_beta_quotient_witness_exists_trace_second * S ((S (S (l))) * d) + (x1))) /\ (forall wpo_old_index_witness_exists_trace wpo_old_value_witness_exists_trace. (exists wpo_gap_witness_exists_trace_old_bound. wpo_gap_witness_exists_trace_old_bound + S (wpo_old_index_witness_exists_trace) = l) -> (((exists wpo_beta_height_witness_exists_trace_old_entry. wpo_beta_height_witness_exists_trace_old_entry + S (wpo_old_value_witness_exists_trace) = S ((S (wpo_old_index_witness_exists_trace)) * c)) /\ exists wpo_beta_quotient_witness_exists_trace_old_entry. b = wpo_beta_quotient_witness_exists_trace_old_entry * S ((S (wpo_old_index_witness_exists_trace)) * c) + (wpo_old_value_witness_exists_trace))) -> (((exists wpo_beta_height_witness_exists_trace_new_entry. wpo_beta_height_witness_exists_trace_new_entry + S (wpo_old_value_witness_exists_trace) = S ((S (wpo_old_index_witness_exists_trace)) * d)) /\ exists wpo_beta_quotient_witness_exists_trace_new_entry. z = wpo_beta_quotient_witness_exists_trace_new_entry * S ((S (wpo_old_index_witness_exists_trace)) * d) + (wpo_old_value_witness_exists_trace)))))))
  55. 0055specialize beta_prefix_append_two_exists b
  56. 0056specialize beta_prefix_append_two_exists c
  57. 0057specialize beta_prefix_append_two_exists l
  58. 0058specialize beta_prefix_append_two_exists x
  59. 0059specialize beta_prefix_append_two_exists x1
  60. 0060exact beta_prefix_append_two_exists
  61. 0061cases happend
  62. 0062cases happend_witness
  63. 0063have hclosed_after : forall espo_position_witness_closed_after espo_source_witness_closed_after espo_mate_witness_closed_after. (exists wpo_gap_witness_closed_after_position_bound. wpo_gap_witness_closed_after_position_bound + S (espo_position_witness_closed_after) = S (S l)) -> (((exists wpo_beta_height_witness_closed_after_source_entry. wpo_beta_height_witness_closed_after_source_entry + S (espo_source_witness_closed_after) = S ((S (espo_position_witness_closed_after)) * x3)) /\ exists wpo_beta_quotient_witness_closed_after_source_entry. x2 = wpo_beta_quotient_witness_closed_after_source_entry * S ((S (espo_position_witness_closed_after)) * x3) + (espo_source_witness_closed_after))) -> (((exists wpo_beta_height_witness_closed_after_scaled_entry. wpo_beta_height_witness_closed_after_scaled_entry + S (S espo_mate_witness_closed_after) = S ((S (espo_source_witness_closed_after)) * v)) /\ exists wpo_beta_quotient_witness_closed_after_scaled_entry. u = wpo_beta_quotient_witness_closed_after_scaled_entry * S ((S (espo_source_witness_closed_after)) * v) + (S espo_mate_witness_closed_after))) -> exists espo_mate_position_witness_closed_after. ((exists wpo_gap_witness_closed_after_mate_bound. wpo_gap_witness_closed_after_mate_bound + S (espo_mate_position_witness_closed_after) = S (S l)) /\ (((exists wpo_beta_height_witness_closed_after_mate_entry. wpo_beta_height_witness_closed_after_mate_entry + S (espo_mate_witness_closed_after) = S ((S (espo_mate_position_witness_closed_after)) * x3)) /\ exists wpo_beta_quotient_witness_closed_after_mate_entry. x2 = wpo_beta_quotient_witness_closed_after_mate_entry * S ((S (espo_mate_position_witness_closed_after)) * x3) + (espo_mate_witness_closed_after))))
  64. 0064specialize beta_prefix_append_two_scaled_orbit_closed u
  65. 0065specialize beta_prefix_append_two_scaled_orbit_closed v
  66. 0066specialize beta_prefix_append_two_scaled_orbit_closed b
  67. 0067specialize beta_prefix_append_two_scaled_orbit_closed c
  68. 0068specialize beta_prefix_append_two_scaled_orbit_closed x2
  69. 0069specialize beta_prefix_append_two_scaled_orbit_closed x3
  70. 0070specialize beta_prefix_append_two_scaled_orbit_closed l
  71. 0071specialize beta_prefix_append_two_scaled_orbit_closed x
  72. 0072specialize beta_prefix_append_two_scaled_orbit_closed x1
  73. 0073apply beta_prefix_append_two_scaled_orbit_closed
  74. 0074exact happend_witness_witness
  75. 0075exact hclosed
  76. 0076exact hparts_right_right_right_right_left
  77. 0077exact hparts_right_right_right_right_right
  78. 0078have hinjective_after : forall wpo_injective_left_witness_injective_after wpo_injective_right_witness_injective_after wpo_injective_value_witness_injective_after. (exists wpo_gap_witness_injective_after_left_bound. wpo_gap_witness_injective_after_left_bound + S (wpo_injective_left_witness_injective_after) = S (S l)) -> (exists wpo_gap_witness_injective_after_right_bound. wpo_gap_witness_injective_after_right_bound + S (wpo_injective_right_witness_injective_after) = S (S l)) -> (((exists wpo_beta_height_witness_injective_after_left_entry. wpo_beta_height_witness_injective_after_left_entry + S (wpo_injective_value_witness_injective_after) = S ((S (wpo_injective_left_witness_injective_after)) * x3)) /\ exists wpo_beta_quotient_witness_injective_after_left_entry. x2 = wpo_beta_quotient_witness_injective_after_left_entry * S ((S (wpo_injective_left_witness_injective_after)) * x3) + (wpo_injective_value_witness_injective_after))) -> (((exists wpo_beta_height_witness_injective_after_right_entry. wpo_beta_height_witness_injective_after_right_entry + S (wpo_injective_value_witness_injective_after) = S ((S (wpo_injective_right_witness_injective_after)) * x3)) /\ exists wpo_beta_quotient_witness_injective_after_right_entry. x2 = wpo_beta_quotient_witness_injective_after_right_entry * S ((S (wpo_injective_right_witness_injective_after)) * x3) + (wpo_injective_value_witness_injective_after))) -> wpo_injective_left_witness_injective_after = wpo_injective_right_witness_injective_after
  79. 0079specialize beta_prefix_append_two_injective b
  80. 0080specialize beta_prefix_append_two_injective c
  81. 0081specialize beta_prefix_append_two_injective x2
  82. 0082specialize beta_prefix_append_two_injective x3
  83. 0083specialize beta_prefix_append_two_injective l
  84. 0084specialize beta_prefix_append_two_injective x
  85. 0085specialize beta_prefix_append_two_injective x1
  86. 0086apply beta_prefix_append_two_injective
  87. 0087exact happend_witness_witness
  88. 0088exact hinjective
  89. 0089exact hparts_right_left
  90. 0090exact hjomit
  91. 0091exact hparts_right_right_right_left
  92. 0092exists x2
  93. 0093exists x3
  94. 0094exists x
  95. 0095exists x1
  96. 0096split
  97. 0097exact happend_witness_witness
  98. 0098split
  99. 0099exact hparts_left
  100. 0100split
  101. 0101exact hparts_right_right_left
  102. 0102split
  103. 0103exact hparts_right_left
  104. 0104split
  105. 0105exact hjomit
  106. 0106split
  107. 0107exact hparts_right_right_right_left
  108. 0108split
  109. 0109exact hparts_right_right_right_right_left
  110. 0110split
  111. 0111exact hparts_right_right_right_right_right
  112. 0112split
  113. 0113exact hclosed_after
  114. 0114exact hinjective_after