PA009N

beta_prefix_append_two_injective

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

Appending two distinct values omitted by an injective old prefix preserves decoded-prefix injectivity.

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 b c z d l a e. (((((exists wpo_beta_height_injective_trace_first. wpo_beta_height_injective_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_injective_trace_first. z = wpo_beta_quotient_injective_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_injective_trace_second. wpo_beta_height_injective_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_injective_trace_second. z = wpo_beta_quotient_injective_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_injective_trace wpo_old_value_injective_trace. (exists wpo_gap_injective_trace_old_bound. wpo_gap_injective_trace_old_bound + S (wpo_old_index_injective_trace) = l) -> (((exists wpo_beta_height_injective_trace_old_entry. wpo_beta_height_injective_trace_old_entry + S (wpo_old_value_injective_trace) = S ((S (wpo_old_index_injective_trace)) * c)) /\ exists wpo_beta_quotient_injective_trace_old_entry. b = wpo_beta_quotient_injective_trace_old_entry * S ((S (wpo_old_index_injective_trace)) * c) + (wpo_old_value_injective_trace))) -> (((exists wpo_beta_height_injective_trace_new_entry. wpo_beta_height_injective_trace_new_entry + S (wpo_old_value_injective_trace) = S ((S (wpo_old_index_injective_trace)) * d)) /\ exists wpo_beta_quotient_injective_trace_new_entry. z = wpo_beta_quotient_injective_trace_new_entry * S ((S (wpo_old_index_injective_trace)) * d) + (wpo_old_value_injective_trace))))))) -> (forall wpo_injective_left_injective_before wpo_injective_right_injective_before wpo_injective_value_injective_before. (exists wpo_gap_injective_before_left_bound. wpo_gap_injective_before_left_bound + S (wpo_injective_left_injective_before) = l) -> (exists wpo_gap_injective_before_right_bound. wpo_gap_injective_before_right_bound + S (wpo_injective_right_injective_before) = l) -> (((exists wpo_beta_height_injective_before_left_entry. wpo_beta_height_injective_before_left_entry + S (wpo_injective_value_injective_before) = S ((S (wpo_injective_left_injective_before)) * c)) /\ exists wpo_beta_quotient_injective_before_left_entry. b = wpo_beta_quotient_injective_before_left_entry * S ((S (wpo_injective_left_injective_before)) * c) + (wpo_injective_value_injective_before))) -> (((exists wpo_beta_height_injective_before_right_entry. wpo_beta_height_injective_before_right_entry + S (wpo_injective_value_injective_before) = S ((S (wpo_injective_right_injective_before)) * c)) /\ exists wpo_beta_quotient_injective_before_right_entry. b = wpo_beta_quotient_injective_before_right_entry * S ((S (wpo_injective_right_injective_before)) * c) + (wpo_injective_value_injective_before))) -> wpo_injective_left_injective_before = wpo_injective_right_injective_before) -> (~(exists wpo_index_injective_first_omit_contains. ((exists wpo_gap_injective_first_omit_contains_bound. wpo_gap_injective_first_omit_contains_bound + S (wpo_index_injective_first_omit_contains) = l) /\ (((exists wpo_beta_height_injective_first_omit_contains_entry. wpo_beta_height_injective_first_omit_contains_entry + S (a) = S ((S (wpo_index_injective_first_omit_contains)) * c)) /\ exists wpo_beta_quotient_injective_first_omit_contains_entry. b = wpo_beta_quotient_injective_first_omit_contains_entry * S ((S (wpo_index_injective_first_omit_contains)) * c) + (a)))))) -> (~(exists wpo_index_injective_second_omit_contains. ((exists wpo_gap_injective_second_omit_contains_bound. wpo_gap_injective_second_omit_contains_bound + S (wpo_index_injective_second_omit_contains) = l) /\ (((exists wpo_beta_height_injective_second_omit_contains_entry. wpo_beta_height_injective_second_omit_contains_entry + S (e) = S ((S (wpo_index_injective_second_omit_contains)) * c)) /\ exists wpo_beta_quotient_injective_second_omit_contains_entry. b = wpo_beta_quotient_injective_second_omit_contains_entry * S ((S (wpo_index_injective_second_omit_contains)) * c) + (e)))))) -> ~(a = e) -> (forall wpo_injective_left_injective_after wpo_injective_right_injective_after wpo_injective_value_injective_after. (exists wpo_gap_injective_after_left_bound. wpo_gap_injective_after_left_bound + S (wpo_injective_left_injective_after) = S (S l)) -> (exists wpo_gap_injective_after_right_bound. wpo_gap_injective_after_right_bound + S (wpo_injective_right_injective_after) = S (S l)) -> (((exists wpo_beta_height_injective_after_left_entry. wpo_beta_height_injective_after_left_entry + S (wpo_injective_value_injective_after) = S ((S (wpo_injective_left_injective_after)) * d)) /\ exists wpo_beta_quotient_injective_after_left_entry. z = wpo_beta_quotient_injective_after_left_entry * S ((S (wpo_injective_left_injective_after)) * d) + (wpo_injective_value_injective_after))) -> (((exists wpo_beta_height_injective_after_right_entry. wpo_beta_height_injective_after_right_entry + S (wpo_injective_value_injective_after) = S ((S (wpo_injective_right_injective_after)) * d)) /\ exists wpo_beta_quotient_injective_after_right_entry. z = wpo_beta_quotient_injective_after_right_entry * S ((S (wpo_injective_right_injective_after)) * d) + (wpo_injective_value_injective_after))) -> wpo_injective_left_injective_after = wpo_injective_right_injective_after)

Structural proof guide

Generated structural guide

Appending two distinct values omitted by an injective old prefix preserves decoded-prefix injectivity.

Use the direct prerequisites beta_prefix_append_two_reflect as previously established PA formulas.

The proof proceeds by case analysis (20), intermediate claims (5), equality transport (8).

Referenced ingredients

PA009L beta_prefix_append_two_reflect

Proof neighborhood

Direct dependencies

PA009L beta_prefix_append_two_reflect

Direct dependents

PA009O scaled_inverse_pair_order_choose_append PA00AW prime_pair_order_choose_append_injective

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

133 script commands · 55 reading checkpoints · 5 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 (1)
beta prefix append two reflect

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 b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro d
  5. L5
    intro l
  6. L6
    intro a
  7. L7
    intro e
  8. L8
    intro htrace
  9. L9
    intro hold_injective
  10. L10
    intro hfirst_omit
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hsecond_omit
  2. L12
    intro hdistinct
03Establish hright_reflect_theoremL13–21

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

  1. L13
    have hright_reflect_theorem : ∀ b. ∀ c. ∀ z. ∀ d. ∀ l. ∀ a. ∀ e. BetaAt(z,d,l,a) ∧ (BetaAt(z,d,S l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) → ∀ x. ∀ y. Lt(x,S S l) → BetaAt(z,d,x,y) → x = S l ∧ y = e ∨ (x = l ∧ y = a ∨ Lt(x,l) ∧ BetaAt(b,c,x,y))Definitions: LtBetaAt
  2. L14
    exact beta_prefix_append_two_reflect
  3. L15
    intro q
  4. L16
    intro r
  5. L17
    intro w
  6. L18
    intro hq
  7. L19
    intro hr
  8. L20
    intro hleft_entry
  9. L21
    intro hright_entry
04Establish hleft_allL22–31

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

  1. L22
    have hleft_all : ∀ q. ∀ w. Lt(q,S S l) → BetaAt(z,d,q,w) → q = S l ∧ w = e ∨ (q = l ∧ w = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,w))Definitions: LtBetaAt
  2. L23
    specialize beta_prefix_append_two_reflect b
  3. L24
    specialize beta_prefix_append_two_reflect c
  4. L25
    specialize beta_prefix_append_two_reflect z
  5. L26
    specialize beta_prefix_append_two_reflect d
  6. L27
    specialize beta_prefix_append_two_reflect l
  7. L28
    specialize beta_prefix_append_two_reflect a
  8. L29
    specialize beta_prefix_append_two_reflect e
  9. L30
    apply beta_prefix_append_two_reflect
  10. L31
    exact htrace
05Establish hright_allL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright reflect theorem.

  1. L32
    have hright_all : ∀ r. ∀ w. Lt(r,S S l) → BetaAt(z,d,r,w) → r = S l ∧ w = e ∨ (r = l ∧ w = a ∨ Lt(r,l) ∧ BetaAt(b,c,r,w))Definitions: LtBetaAt
  2. L33
    specialize hright_reflect_theorem b
  3. L34
    specialize hright_reflect_theorem c
  4. L35
    specialize hright_reflect_theorem z
  5. L36
    specialize hright_reflect_theorem d
  6. L37
    specialize hright_reflect_theorem l
  7. L38
    specialize hright_reflect_theorem a
  8. L39
    specialize hright_reflect_theorem e
  9. L40
    apply hright_reflect_theorem
  10. L41
    exact htrace
06Establish hleft_classL42–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft all.

  1. L42
    have hleft_class : ((q = S (l) /\ w = e) \/ ((q = l /\ w = a) \/ ((exists wpo_gap_injective_left_reflection_old_bound. wpo_gap_injective_left_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_injective_left_reflection_old_entry. wpo_beta_height_injective_left_reflection_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_injective_left_reflection_old_entry. b = wpo_beta_quotient_injective_left_reflection_old_entry * S ((S (q)) * c) + (w))))))
  2. L43
    specialize hleft_all q
  3. L44
    specialize hleft_all w
  4. L45
    apply hleft_all
  5. L46
    exact hq
  6. L47
    exact hleft_entry
07Establish hright_classL48–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright all.

  1. L48
    have hright_class : ((r = S (l) /\ w = e) \/ ((r = l /\ w = a) \/ ((exists wpo_gap_injective_right_reflection_old_bound. wpo_gap_injective_right_reflection_old_bound + S (r) = l) /\ (((exists wpo_beta_height_injective_right_reflection_old_entry. wpo_beta_height_injective_right_reflection_old_entry + S (w) = S ((S (r)) * c)) /\ exists wpo_beta_quotient_injective_right_reflection_old_entry. b = wpo_beta_quotient_injective_right_reflection_old_entry * S ((S (r)) * c) + (w))))))
  2. L49
    specialize hright_all r
  3. L50
    specialize hright_all w
  4. L51
    apply hright_all
  5. L52
    exact hr
  6. L53
    exact hright_entry
08Separate the logical casesL54–57

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

  1. L54
    cases hleft_class
  2. L55
    cases hleft_class_left
  3. L56
    cases hright_class
  4. L57
    cases hright_class_left
09Calculate and transport equalitiesL58–58

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L58
    trans (S l)
10Use earlier factsL59–59

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

  1. L59
    exact hleft_class_left_left
11Calculate and transport equalitiesL60–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    symm
12Use earlier factsL61–61

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

  1. L61
    exact hright_class_left_left
13Separate the logical casesL62–64

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

  1. L62
    cases hright_class_right
  2. L63
    cases hright_class_right_left
  3. L64
    exfalso
14Use earlier factsL65–65

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

  1. L65
    apply hdistinct
15Calculate and transport equalitiesL66–67

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L66
    trans w
  2. L67
    symm
16Use earlier factsL68–69

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

  1. L68
    exact hright_class_right_left_right
  2. L69
    exact hleft_class_left_right
17Separate the logical casesL70–71

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

  1. L70
    cases hright_class_right_right
  2. L71
    exfalso
18Use earlier factsL72–72

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

  1. L72
    apply hsecond_omit
19Construct an explicit witnessL73–73

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

  1. L73
    exists r
20Separate the logical casesL74–74

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

  1. L74
    split
21Use earlier factsL75–75

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

  1. L75
    exact hright_class_right_right_left
22Calculate and transport equalitiesL76–77

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L76
    rewrite hleft_class_left_right at hright_class_right_right_right
  2. L77
    rewrite hleft_class_left_right at hright_class_right_right_right
23Use earlier factsL78–78

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

  1. L78
    exact hright_class_right_right_right
24Separate the logical casesL79–83

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

  1. L79
    cases hleft_class_right
  2. L80
    cases hleft_class_right_left
  3. L81
    cases hright_class
  4. L82
    cases hright_class_left
  5. L83
    exfalso
25Use earlier factsL84–84

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

  1. L84
    apply hdistinct
26Calculate and transport equalitiesL85–86

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L85
    trans w
  2. L86
    symm
27Use earlier factsL87–88

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

  1. L87
    exact hleft_class_right_left_right
  2. L88
    exact hright_class_left_right
28Separate the logical casesL89–90

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

  1. L89
    cases hright_class_right
  2. L90
    cases hright_class_right_left
29Calculate and transport equalitiesL91–91

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L91
    trans l
30Use earlier factsL92–92

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

  1. L92
    exact hleft_class_right_left_left
31Calculate and transport equalitiesL93–93

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L93
    symm
32Use earlier factsL94–94

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

  1. L94
    exact hright_class_right_left_left
33Separate the logical casesL95–96

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

  1. L95
    cases hright_class_right_right
  2. L96
    exfalso
34Use earlier factsL97–97

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

  1. L97
    apply hfirst_omit
35Construct an explicit witnessL98–98

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

  1. L98
    exists r
36Separate the logical casesL99–99

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

  1. L99
    split
37Use earlier factsL100–100

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

  1. L100
    exact hright_class_right_right_left
38Calculate and transport equalitiesL101–102

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L101
    rewrite hleft_class_right_left_right at hright_class_right_right_right
  2. L102
    rewrite hleft_class_right_left_right at hright_class_right_right_right
39Use earlier factsL103–103

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

  1. L103
    exact hright_class_right_right_right
40Separate the logical casesL104–107

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

  1. L104
    cases hleft_class_right_right
  2. L105
    cases hright_class
  3. L106
    cases hright_class_left
  4. L107
    exfalso
41Use earlier factsL108–108

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

  1. L108
    apply hsecond_omit
42Construct an explicit witnessL109–109

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

  1. L109
    exists q
43Separate the logical casesL110–110

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

  1. L110
    split
44Use earlier factsL111–111

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

  1. L111
    exact hleft_class_right_right_left
45Calculate and transport equalitiesL112–113

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L112
    rewrite hright_class_left_right at hleft_class_right_right_right
  2. L113
    rewrite hright_class_left_right at hleft_class_right_right_right
46Use earlier factsL114–114

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

  1. L114
    exact hleft_class_right_right_right
47Separate the logical casesL115–117

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

  1. L115
    cases hright_class_right
  2. L116
    cases hright_class_right_left
  3. L117
    exfalso
48Use earlier factsL118–118

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

  1. L118
    apply hfirst_omit
49Construct an explicit witnessL119–119

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

  1. L119
    exists q
50Separate the logical casesL120–120

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

  1. L120
    split
51Use earlier factsL121–121

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

  1. L121
    exact hleft_class_right_right_left
52Calculate and transport equalitiesL122–123

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L122
    rewrite hright_class_right_left_right at hleft_class_right_right_right
  2. L123
    rewrite hright_class_right_left_right at hleft_class_right_right_right
53Use earlier factsL124–124

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

  1. L124
    exact hleft_class_right_right_right
54Separate the logical casesL125–125

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

  1. L125
    cases hright_class_right_right
55Use earlier factsL126–133

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

  1. L126
    specialize hold_injective q
  2. L127
    specialize hold_injective r
  3. L128
    specialize hold_injective w
  4. L129
    apply hold_injective
  5. L130
    exact hleft_class_right_right_left
  6. L131
    exact hright_class_right_right_left
  7. L132
    exact hleft_class_right_right_right
  8. L133
    exact hright_class_right_right_right

Library-wide reading audit

Original exact command ledger · 133 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro l
  6. 0006intro a
  7. 0007intro e
  8. 0008intro htrace
  9. 0009intro hold_injective
  10. 0010intro hfirst_omit
  11. 0011intro hsecond_omit
  12. 0012intro hdistinct
  13. 0013have hright_reflect_theorem : forall b c z d l a e. (((((exists wpo_beta_height_reflect_trace_first. wpo_beta_height_reflect_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_reflect_trace_first. z = wpo_beta_quotient_reflect_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_reflect_trace_second. wpo_beta_height_reflect_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_reflect_trace_second. z = wpo_beta_quotient_reflect_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_reflect_trace wpo_old_value_reflect_trace. (exists wpo_gap_reflect_trace_old_bound. wpo_gap_reflect_trace_old_bound + S (wpo_old_index_reflect_trace) = l) -> (((exists wpo_beta_height_reflect_trace_old_entry. wpo_beta_height_reflect_trace_old_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * c)) /\ exists wpo_beta_quotient_reflect_trace_old_entry. b = wpo_beta_quotient_reflect_trace_old_entry * S ((S (wpo_old_index_reflect_trace)) * c) + (wpo_old_value_reflect_trace))) -> (((exists wpo_beta_height_reflect_trace_new_entry. wpo_beta_height_reflect_trace_new_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * d)) /\ exists wpo_beta_quotient_reflect_trace_new_entry. z = wpo_beta_quotient_reflect_trace_new_entry * S ((S (wpo_old_index_reflect_trace)) * d) + (wpo_old_value_reflect_trace))))))) -> forall i v. (exists wpo_gap_reflect_new_bound. wpo_gap_reflect_new_bound + S (i) = S (S l)) -> (((exists wpo_beta_height_reflect_new_entry. wpo_beta_height_reflect_new_entry + S (v) = S ((S (i)) * d)) /\ exists wpo_beta_quotient_reflect_new_entry. z = wpo_beta_quotient_reflect_new_entry * S ((S (i)) * d) + (v))) -> (((i = S (l) /\ v = e) \/ ((i = l /\ v = a) \/ ((exists wpo_gap_reflect_result_old_bound. wpo_gap_reflect_result_old_bound + S (i) = l) /\ (((exists wpo_beta_height_reflect_result_old_entry. wpo_beta_height_reflect_result_old_entry + S (v) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_result_old_entry. b = wpo_beta_quotient_reflect_result_old_entry * S ((S (i)) * c) + (v)))))))
  14. 0014exact beta_prefix_append_two_reflect
  15. 0015intro q
  16. 0016intro r
  17. 0017intro w
  18. 0018intro hq
  19. 0019intro hr
  20. 0020intro hleft_entry
  21. 0021intro hright_entry
  22. 0022have hleft_all : forall q w. (exists wpo_gap_injective_left_bound. wpo_gap_injective_left_bound + S (q) = S (S l)) -> (((exists wpo_beta_height_injective_left_entry. wpo_beta_height_injective_left_entry + S (w) = S ((S (q)) * d)) /\ exists wpo_beta_quotient_injective_left_entry. z = wpo_beta_quotient_injective_left_entry * S ((S (q)) * d) + (w))) -> (((q = S (l) /\ w = e) \/ ((q = l /\ w = a) \/ ((exists wpo_gap_injective_left_reflection_old_bound. wpo_gap_injective_left_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_injective_left_reflection_old_entry. wpo_beta_height_injective_left_reflection_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_injective_left_reflection_old_entry. b = wpo_beta_quotient_injective_left_reflection_old_entry * S ((S (q)) * c) + (w)))))))
  23. 0023specialize beta_prefix_append_two_reflect b
  24. 0024specialize beta_prefix_append_two_reflect c
  25. 0025specialize beta_prefix_append_two_reflect z
  26. 0026specialize beta_prefix_append_two_reflect d
  27. 0027specialize beta_prefix_append_two_reflect l
  28. 0028specialize beta_prefix_append_two_reflect a
  29. 0029specialize beta_prefix_append_two_reflect e
  30. 0030apply beta_prefix_append_two_reflect
  31. 0031exact htrace
  32. 0032have hright_all : forall r w. (exists wpo_gap_injective_right_bound. wpo_gap_injective_right_bound + S (r) = S (S l)) -> (((exists wpo_beta_height_injective_right_entry. wpo_beta_height_injective_right_entry + S (w) = S ((S (r)) * d)) /\ exists wpo_beta_quotient_injective_right_entry. z = wpo_beta_quotient_injective_right_entry * S ((S (r)) * d) + (w))) -> (((r = S (l) /\ w = e) \/ ((r = l /\ w = a) \/ ((exists wpo_gap_injective_right_reflection_old_bound. wpo_gap_injective_right_reflection_old_bound + S (r) = l) /\ (((exists wpo_beta_height_injective_right_reflection_old_entry. wpo_beta_height_injective_right_reflection_old_entry + S (w) = S ((S (r)) * c)) /\ exists wpo_beta_quotient_injective_right_reflection_old_entry. b = wpo_beta_quotient_injective_right_reflection_old_entry * S ((S (r)) * c) + (w)))))))
  33. 0033specialize hright_reflect_theorem b
  34. 0034specialize hright_reflect_theorem c
  35. 0035specialize hright_reflect_theorem z
  36. 0036specialize hright_reflect_theorem d
  37. 0037specialize hright_reflect_theorem l
  38. 0038specialize hright_reflect_theorem a
  39. 0039specialize hright_reflect_theorem e
  40. 0040apply hright_reflect_theorem
  41. 0041exact htrace
  42. 0042have hleft_class : ((q = S (l) /\ w = e) \/ ((q = l /\ w = a) \/ ((exists wpo_gap_injective_left_reflection_old_bound. wpo_gap_injective_left_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_injective_left_reflection_old_entry. wpo_beta_height_injective_left_reflection_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_injective_left_reflection_old_entry. b = wpo_beta_quotient_injective_left_reflection_old_entry * S ((S (q)) * c) + (w))))))
  43. 0043specialize hleft_all q
  44. 0044specialize hleft_all w
  45. 0045apply hleft_all
  46. 0046exact hq
  47. 0047exact hleft_entry
  48. 0048have hright_class : ((r = S (l) /\ w = e) \/ ((r = l /\ w = a) \/ ((exists wpo_gap_injective_right_reflection_old_bound. wpo_gap_injective_right_reflection_old_bound + S (r) = l) /\ (((exists wpo_beta_height_injective_right_reflection_old_entry. wpo_beta_height_injective_right_reflection_old_entry + S (w) = S ((S (r)) * c)) /\ exists wpo_beta_quotient_injective_right_reflection_old_entry. b = wpo_beta_quotient_injective_right_reflection_old_entry * S ((S (r)) * c) + (w))))))
  49. 0049specialize hright_all r
  50. 0050specialize hright_all w
  51. 0051apply hright_all
  52. 0052exact hr
  53. 0053exact hright_entry
  54. 0054cases hleft_class
  55. 0055cases hleft_class_left
  56. 0056cases hright_class
  57. 0057cases hright_class_left
  58. 0058trans (S l)
  59. 0059exact hleft_class_left_left
  60. 0060symm
  61. 0061exact hright_class_left_left
  62. 0062cases hright_class_right
  63. 0063cases hright_class_right_left
  64. 0064exfalso
  65. 0065apply hdistinct
  66. 0066trans w
  67. 0067symm
  68. 0068exact hright_class_right_left_right
  69. 0069exact hleft_class_left_right
  70. 0070cases hright_class_right_right
  71. 0071exfalso
  72. 0072apply hsecond_omit
  73. 0073exists r
  74. 0074split
  75. 0075exact hright_class_right_right_left
  76. 0076rewrite hleft_class_left_right at hright_class_right_right_right
  77. 0077rewrite hleft_class_left_right at hright_class_right_right_right
  78. 0078exact hright_class_right_right_right
  79. 0079cases hleft_class_right
  80. 0080cases hleft_class_right_left
  81. 0081cases hright_class
  82. 0082cases hright_class_left
  83. 0083exfalso
  84. 0084apply hdistinct
  85. 0085trans w
  86. 0086symm
  87. 0087exact hleft_class_right_left_right
  88. 0088exact hright_class_left_right
  89. 0089cases hright_class_right
  90. 0090cases hright_class_right_left
  91. 0091trans l
  92. 0092exact hleft_class_right_left_left
  93. 0093symm
  94. 0094exact hright_class_right_left_left
  95. 0095cases hright_class_right_right
  96. 0096exfalso
  97. 0097apply hfirst_omit
  98. 0098exists r
  99. 0099split
  100. 0100exact hright_class_right_right_left
  101. 0101rewrite hleft_class_right_left_right at hright_class_right_right_right
  102. 0102rewrite hleft_class_right_left_right at hright_class_right_right_right
  103. 0103exact hright_class_right_right_right
  104. 0104cases hleft_class_right_right
  105. 0105cases hright_class
  106. 0106cases hright_class_left
  107. 0107exfalso
  108. 0108apply hsecond_omit
  109. 0109exists q
  110. 0110split
  111. 0111exact hleft_class_right_right_left
  112. 0112rewrite hright_class_left_right at hleft_class_right_right_right
  113. 0113rewrite hright_class_left_right at hleft_class_right_right_right
  114. 0114exact hleft_class_right_right_right
  115. 0115cases hright_class_right
  116. 0116cases hright_class_right_left
  117. 0117exfalso
  118. 0118apply hfirst_omit
  119. 0119exists q
  120. 0120split
  121. 0121exact hleft_class_right_right_left
  122. 0122rewrite hright_class_right_left_right at hleft_class_right_right_right
  123. 0123rewrite hright_class_right_left_right at hleft_class_right_right_right
  124. 0124exact hleft_class_right_right_right
  125. 0125cases hright_class_right_right
  126. 0126specialize hold_injective q
  127. 0127specialize hold_injective r
  128. 0128specialize hold_injective w
  129. 0129apply hold_injective
  130. 0130exact hleft_class_right_right_left
  131. 0131exact hright_class_right_right_left
  132. 0132exact hleft_class_right_right_right
  133. 0133exact hright_class_right_right_right