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.
Statement with defined notation
∀ pb. ∀ pc. ∀ qb. ∀ qc. ∀ b. ∀ c. ∀ d. ∀ e. ∀ w. ∀ v. (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. ∃ n. ∃ m. x = S z ∧ (BetaAt(pb,pc,z,n) ∧ (BetaAt(pb,pc,S z,m) ∧ y = n + m))))) → (∀ x. Lt(x,v) → ∃ y. BetaAt(d,e,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. ∃ n. ∃ m. x = S z ∧ (BetaAt(qb,qc,z,n) ∧ (BetaAt(qb,qc,S z,m) ∧ y = n + m))))) → (∀ x. ∀ y. ∀ z. Lt(x,w) → Lt(x,v) → BetaAt(pb,pc,x,y) → BetaAt(qb,qc,x,z) → y = z) → ∀ x. ∀ y. ∀ z. Lt(x,w) → Lt(x,v) → BetaAt(b,c,x,y) → BetaAt(d,e,x,z) → y = zEvery purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
16 occurrences
In local proof propositions
12 occurrences
Exact expanded native-PA statement
forall pb pc qb qc b c d e w v. (forall bcf_index_bpspf_left. (exists bcf_lt_gap_bpspf_left_bound. bcf_lt_gap_bpspf_left_bound + S (bcf_index_bpspf_left) = w) -> exists bcf_value_bpspf_left. ((((exists bcf_height_bpspf_left_entry. bcf_height_bpspf_left_entry + S (bcf_value_bpspf_left) = S ((S (bcf_index_bpspf_left)) * c)) /\ exists bcf_quotient_bpspf_left_entry. b = bcf_quotient_bpspf_left_entry * S ((S (bcf_index_bpspf_left)) * c) + (bcf_value_bpspf_left))) /\ ((bcf_index_bpspf_left = 0 /\ bcf_value_bpspf_left = 1) \/ exists bcf_predecessor_bpspf_left bcf_left_bpspf_left bcf_right_bpspf_left. bcf_index_bpspf_left = S bcf_predecessor_bpspf_left /\ ((((exists bcf_height_bpspf_left_previous_left. bcf_height_bpspf_left_previous_left + S (bcf_left_bpspf_left) = S ((S (bcf_predecessor_bpspf_left)) * pc)) /\ exists bcf_quotient_bpspf_left_previous_left. pb = bcf_quotient_bpspf_left_previous_left * S ((S (bcf_predecessor_bpspf_left)) * pc) + (bcf_left_bpspf_left))) /\ ((((exists bcf_height_bpspf_left_previous_right. bcf_height_bpspf_left_previous_right + S (bcf_right_bpspf_left) = S ((S (S (bcf_predecessor_bpspf_left))) * pc)) /\ exists bcf_quotient_bpspf_left_previous_right. pb = bcf_quotient_bpspf_left_previous_right * S ((S (S (bcf_predecessor_bpspf_left))) * pc) + (bcf_right_bpspf_left))) /\ bcf_value_bpspf_left = bcf_left_bpspf_left + bcf_right_bpspf_left))))) -> (forall bcf_index_bpspf_right. (exists bcf_lt_gap_bpspf_right_bound. bcf_lt_gap_bpspf_right_bound + S (bcf_index_bpspf_right) = v) -> exists bcf_value_bpspf_right. ((((exists bcf_height_bpspf_right_entry. bcf_height_bpspf_right_entry + S (bcf_value_bpspf_right) = S ((S (bcf_index_bpspf_right)) * e)) /\ exists bcf_quotient_bpspf_right_entry. d = bcf_quotient_bpspf_right_entry * S ((S (bcf_index_bpspf_right)) * e) + (bcf_value_bpspf_right))) /\ ((bcf_index_bpspf_right = 0 /\ bcf_value_bpspf_right = 1) \/ exists bcf_predecessor_bpspf_right bcf_left_bpspf_right bcf_right_bpspf_right. bcf_index_bpspf_right = S bcf_predecessor_bpspf_right /\ ((((exists bcf_height_bpspf_right_previous_left. bcf_height_bpspf_right_previous_left + S (bcf_left_bpspf_right) = S ((S (bcf_predecessor_bpspf_right)) * qc)) /\ exists bcf_quotient_bpspf_right_previous_left. qb = bcf_quotient_bpspf_right_previous_left * S ((S (bcf_predecessor_bpspf_right)) * qc) + (bcf_left_bpspf_right))) /\ ((((exists bcf_height_bpspf_right_previous_right. bcf_height_bpspf_right_previous_right + S (bcf_right_bpspf_right) = S ((S (S (bcf_predecessor_bpspf_right))) * qc)) /\ exists bcf_quotient_bpspf_right_previous_right. qb = bcf_quotient_bpspf_right_previous_right * S ((S (S (bcf_predecessor_bpspf_right))) * qc) + (bcf_right_bpspf_right))) /\ bcf_value_bpspf_right = bcf_left_bpspf_right + bcf_right_bpspf_right))))) -> (forall i x y. (exists bcf_lt_gap_bpspf_previous_left_bound. bcf_lt_gap_bpspf_previous_left_bound + S (i) = w) -> (exists bcf_lt_gap_bpspf_previous_right_bound. bcf_lt_gap_bpspf_previous_right_bound + S (i) = v) -> (((exists bcf_height_bpspf_previous_left_at. bcf_height_bpspf_previous_left_at + S (x) = S ((S (i)) * pc)) /\ exists bcf_quotient_bpspf_previous_left_at. pb = bcf_quotient_bpspf_previous_left_at * S ((S (i)) * pc) + (x))) -> (((exists bcf_height_bpspf_previous_right_at. bcf_height_bpspf_previous_right_at + S (y) = S ((S (i)) * qc)) /\ exists bcf_quotient_bpspf_previous_right_at. qb = bcf_quotient_bpspf_previous_right_at * S ((S (i)) * qc) + (y))) -> x = y) -> (forall i x y. (exists bcf_lt_gap_bpspf_current_left_bound. bcf_lt_gap_bpspf_current_left_bound + S (i) = w) -> (exists bcf_lt_gap_bpspf_current_right_bound. bcf_lt_gap_bpspf_current_right_bound + S (i) = v) -> (((exists bcf_height_bpspf_current_left_at. bcf_height_bpspf_current_left_at + S (x) = S ((S (i)) * c)) /\ exists bcf_quotient_bpspf_current_left_at. b = bcf_quotient_bpspf_current_left_at * S ((S (i)) * c) + (x))) -> (((exists bcf_height_bpspf_current_right_at. bcf_height_bpspf_current_right_at + S (y) = S ((S (i)) * e)) /\ exists bcf_quotient_bpspf_current_right_at. d = bcf_quotient_bpspf_current_right_at * S ((S (i)) * e) + (y))) -> x = y)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
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 (4)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Establish hleft_valueL21–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft.
- L21
have hleft_value : ∃ bcf_cell_value_bpspf_left_cell. BetaAt(b,c,i,bcf_cell_value_bpspf_left_cell) ∧ (i = 0 ∧ bcf_cell_value_bpspf_left_cell = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ bcf_cell_value_bpspf_left_cell = y + z))))Definitions: BetaAt(b,c,i,bcf_cell_value_bpspf_left_cell)BetaAt(pb,pc,x,y)BetaAt(pb,pc,S x,z)Original native command in the exact edition - L22
specialize hleft i - L23
apply hleft - L24
exact hiw
04Separate the logical casesL25–26
05Establish hright_valueL27–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright.
- L27
have hright_value : ∃ bcf_cell_value_bpspf_right_cell. BetaAt(d,e,i,bcf_cell_value_bpspf_right_cell) ∧ (i = 0 ∧ bcf_cell_value_bpspf_right_cell = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,z) ∧ bcf_cell_value_bpspf_right_cell = y + z))))Definitions: BetaAt(d,e,i,bcf_cell_value_bpspf_right_cell)BetaAt(qb,qc,x,y)BetaAt(qb,qc,S x,z)Original native command in the exact edition - L28
specialize hright i - L29
apply hright - L30
exact hiv
06Separate the logical casesL31–32
07Establish hx_valueL33–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
08Establish hy_valueL42–50
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
09Separate the logical casesL51–54
10Calculate and transport equalitiesL55–55
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L55
trans x1
11Use earlier factsL56–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L56
exact hx_value
12Calculate and transport equalitiesL57–57
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L57
trans 1
13Use earlier factsL58–58
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L58
exact hleft_value_witness_right_left_right
14Calculate and transport equalitiesL59–60
15Use earlier factsL61–61
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L61
exact hright_value_witness_right_left_right
16Calculate and transport equalitiesL62–62
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L62
symm
17Use earlier factsL63–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L63
exact hy_value
18Separate the logical casesL64–68
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
19Establish hbadL69–76
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.
20Separate the logical casesL77–85
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L77
cases hleft_value_witness_right_right - L78
cases hleft_value_witness_right_right_witness - L79
cases hleft_value_witness_right_right_witness_witness - L80
cases hleft_value_witness_right_right_witness_witness_witness - L81
cases hleft_value_witness_right_right_witness_witness_witness_right - L82
cases hleft_value_witness_right_right_witness_witness_witness_right_right - L83
cases hright_value_witness_right - L84
cases hright_value_witness_right_left - L85
exfalso
21Establish hbadL86–93
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.
22Separate the logical casesL94–99
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L94
cases hright_value_witness_right_right - L95
cases hright_value_witness_right_right_witness - L96
cases hright_value_witness_right_right_witness_witness - L97
cases hright_value_witness_right_right_witness_witness_witness - L98
cases hright_value_witness_right_right_witness_witness_witness_right - L99
cases hright_value_witness_right_right_witness_witness_witness_right_right
23Establish hsuccL100–104
24Establish hpredL105–109
25Establish hcurrent_wL110–112
Establish this local claim before using it. It is not an additional assumption.
26Establish hcurrent_vL113–115
Establish this local claim before using it. It is not an additional assumption.
27Establish hprevious_wL116–120
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.
28Establish hprevious_vL121–125
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.
29Establish hright_previousL126–129
Establish this local claim before using it. It is not an additional assumption.
- L126
have hright_previous : BetaAt(qb,qc,x3,x7)Definitions: BetaAt(qb,qc,x3,x7)Original native command in the exact edition - L127
rewrite hpred - L128
rewrite hpred - L129
exact hright_value_witness_right_right_witness_witness_witness_right_left
30Establish hright_currentL130–133
Establish this local claim before using it. It is not an additional assumption.
- L130
have hright_current : BetaAt(qb,qc,S x3,x8)Definitions: BetaAt(qb,qc,S x3,x8)Original native command in the exact edition - L131
rewrite hpred - L132
rewrite hpred - L133
exact hright_value_witness_right_right_witness_witness_witness_right_right_left
31Establish huL134–142
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hagree.
32Establish hvL143–152
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hagree.
33Use earlier factsL153–153
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L153
exact hx_value
34Calculate and transport equalitiesL154–154
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L154
trans x4 + x5
35Use earlier factsL155–155
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L155
exact hleft_value_witness_right_right_witness_witness_witness_right_right_right
36Calculate and transport equalitiesL156–157
37Use earlier factsL158–159
38Calculate and transport equalitiesL160–161
39Use earlier factsL162–162
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L162
exact hright_value_witness_right_right_witness_witness_witness_right_right_right
40Calculate and transport equalitiesL163–163
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L163
symm
41Use earlier factsL164–164
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L164
exact hy_value
Original defined command ledger · 164 lines
- 0001
intro pb - 0002
intro pc - 0003
intro qb - 0004
intro qc - 0005
intro b - 0006
intro c - 0007
intro d - 0008
intro e - 0009
intro w - 0010
intro v - 0011
intro hleft - 0012
intro hright - 0013
intro hagree - 0014
intro i - 0015
intro x - 0016
intro y - 0017
intro hiw - 0018
intro hiv - 0019
intro hxi - 0020
intro hyi - 0021
have hleft_value : ∃ bcf_cell_value_bpspf_left_cell. BetaAt(b,c,i,bcf_cell_value_bpspf_left_cell) ∧ (i = 0 ∧ bcf_cell_value_bpspf_left_cell = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ bcf_cell_value_bpspf_left_cell = y + z))))Exact native replay line
have hleft_value : exists bcf_cell_value_bpspf_left_cell. ((((exists bcf_height_bpspf_left_cell_entry. bcf_height_bpspf_left_cell_entry + S (bcf_cell_value_bpspf_left_cell) = S ((S (i)) * c)) /\ exists bcf_quotient_bpspf_left_cell_entry. b = bcf_quotient_bpspf_left_cell_entry * S ((S (i)) * c) + (bcf_cell_value_bpspf_left_cell))) /\ ((i = 0 /\ bcf_cell_value_bpspf_left_cell = 1) \/ exists bcf_cell_predecessor_bpspf_left_cell bcf_cell_left_bpspf_left_cell bcf_cell_right_bpspf_left_cell. i = S bcf_cell_predecessor_bpspf_left_cell /\ ((((exists bcf_height_bpspf_left_cell_previous_left. bcf_height_bpspf_left_cell_previous_left + S (bcf_cell_left_bpspf_left_cell) = S ((S (bcf_cell_predecessor_bpspf_left_cell)) * pc)) /\ exists bcf_quotient_bpspf_left_cell_previous_left. pb = bcf_quotient_bpspf_left_cell_previous_left * S ((S (bcf_cell_predecessor_bpspf_left_cell)) * pc) + (bcf_cell_left_bpspf_left_cell))) /\ ((((exists bcf_height_bpspf_left_cell_previous_right. bcf_height_bpspf_left_cell_previous_right + S (bcf_cell_right_bpspf_left_cell) = S ((S (S (bcf_cell_predecessor_bpspf_left_cell))) * pc)) /\ exists bcf_quotient_bpspf_left_cell_previous_right. pb = bcf_quotient_bpspf_left_cell_previous_right * S ((S (S (bcf_cell_predecessor_bpspf_left_cell))) * pc) + (bcf_cell_right_bpspf_left_cell))) /\ bcf_cell_value_bpspf_left_cell = bcf_cell_left_bpspf_left_cell + bcf_cell_right_bpspf_left_cell)))) - 0022
specialize hleft i - 0023
apply hleft - 0024
exact hiw - 0025
cases hleft_value - 0026
cases hleft_value_witness - 0027
have hright_value : ∃ bcf_cell_value_bpspf_right_cell. BetaAt(d,e,i,bcf_cell_value_bpspf_right_cell) ∧ (i = 0 ∧ bcf_cell_value_bpspf_right_cell = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,z) ∧ bcf_cell_value_bpspf_right_cell = y + z))))Exact native replay line
have hright_value : exists bcf_cell_value_bpspf_right_cell. ((((exists bcf_height_bpspf_right_cell_entry. bcf_height_bpspf_right_cell_entry + S (bcf_cell_value_bpspf_right_cell) = S ((S (i)) * e)) /\ exists bcf_quotient_bpspf_right_cell_entry. d = bcf_quotient_bpspf_right_cell_entry * S ((S (i)) * e) + (bcf_cell_value_bpspf_right_cell))) /\ ((i = 0 /\ bcf_cell_value_bpspf_right_cell = 1) \/ exists bcf_cell_predecessor_bpspf_right_cell bcf_cell_left_bpspf_right_cell bcf_cell_right_bpspf_right_cell. i = S bcf_cell_predecessor_bpspf_right_cell /\ ((((exists bcf_height_bpspf_right_cell_previous_left. bcf_height_bpspf_right_cell_previous_left + S (bcf_cell_left_bpspf_right_cell) = S ((S (bcf_cell_predecessor_bpspf_right_cell)) * qc)) /\ exists bcf_quotient_bpspf_right_cell_previous_left. qb = bcf_quotient_bpspf_right_cell_previous_left * S ((S (bcf_cell_predecessor_bpspf_right_cell)) * qc) + (bcf_cell_left_bpspf_right_cell))) /\ ((((exists bcf_height_bpspf_right_cell_previous_right. bcf_height_bpspf_right_cell_previous_right + S (bcf_cell_right_bpspf_right_cell) = S ((S (S (bcf_cell_predecessor_bpspf_right_cell))) * qc)) /\ exists bcf_quotient_bpspf_right_cell_previous_right. qb = bcf_quotient_bpspf_right_cell_previous_right * S ((S (S (bcf_cell_predecessor_bpspf_right_cell))) * qc) + (bcf_cell_right_bpspf_right_cell))) /\ bcf_cell_value_bpspf_right_cell = bcf_cell_left_bpspf_right_cell + bcf_cell_right_bpspf_right_cell)))) - 0028
specialize hright i - 0029
apply hright - 0030
exact hiv - 0031
cases hright_value - 0032
cases hright_value_witness - 0033
have hx_value : x = x1 - 0034
specialize beta_at_unique b - 0035
specialize beta_at_unique c - 0036
specialize beta_at_unique i - 0037
specialize beta_at_unique x - 0038
specialize beta_at_unique x1 - 0039
apply beta_at_unique - 0040
exact hxi - 0041
exact hleft_value_witness_left - 0042
have hy_value : y = x2 - 0043
specialize beta_at_unique d - 0044
specialize beta_at_unique e - 0045
specialize beta_at_unique i - 0046
specialize beta_at_unique y - 0047
specialize beta_at_unique x2 - 0048
apply beta_at_unique - 0049
exact hyi - 0050
exact hright_value_witness_left - 0051
cases hleft_value_witness_right - 0052
cases hleft_value_witness_right_left - 0053
cases hright_value_witness_right - 0054
cases hright_value_witness_right_left - 0055
trans x1 - 0056
exact hx_value - 0057
trans 1 - 0058
exact hleft_value_witness_right_left_right - 0059
trans x2 - 0060
symm - 0061
exact hright_value_witness_right_left_right - 0062
symm - 0063
exact hy_value - 0064
cases hright_value_witness_right_right - 0065
cases hright_value_witness_right_right_witness - 0066
cases hright_value_witness_right_right_witness_witness - 0067
cases hright_value_witness_right_right_witness_witness_witness - 0068
exfalso - 0069
have hbad : S x3 = 0 - 0070
trans i - 0071
symm - 0072
exact hright_value_witness_right_right_witness_witness_witness_left - 0073
exact hleft_value_witness_right_left_left - 0074
specialize succ_ne_zero x3 - 0075
apply succ_ne_zero - 0076
exact hbad - 0077
cases hleft_value_witness_right_right - 0078
cases hleft_value_witness_right_right_witness - 0079
cases hleft_value_witness_right_right_witness_witness - 0080
cases hleft_value_witness_right_right_witness_witness_witness - 0081
cases hleft_value_witness_right_right_witness_witness_witness_right - 0082
cases hleft_value_witness_right_right_witness_witness_witness_right_right - 0083
cases hright_value_witness_right - 0084
cases hright_value_witness_right_left - 0085
exfalso - 0086
have hbad : S x3 = 0 - 0087
trans i - 0088
symm - 0089
exact hleft_value_witness_right_right_witness_witness_witness_left - 0090
exact hright_value_witness_right_left_left - 0091
specialize succ_ne_zero x3 - 0092
apply succ_ne_zero - 0093
exact hbad - 0094
cases hright_value_witness_right_right - 0095
cases hright_value_witness_right_right_witness - 0096
cases hright_value_witness_right_right_witness_witness - 0097
cases hright_value_witness_right_right_witness_witness_witness - 0098
cases hright_value_witness_right_right_witness_witness_witness_right - 0099
cases hright_value_witness_right_right_witness_witness_witness_right_right - 0100
have hsucc : S x3 = S x6 - 0101
trans i - 0102
symm - 0103
exact hleft_value_witness_right_right_witness_witness_witness_left - 0104
exact hright_value_witness_right_right_witness_witness_witness_left - 0105
have hpred : x3 = x6 - 0106
specialize succ_injective x3 - 0107
specialize succ_injective x6 - 0108
apply succ_injective - 0109
exact hsucc - 0110
have hcurrent_w : Lt(S x3,w)Exact native replay line
have hcurrent_w : exists bcf_lt_gap_bpspf_current_w. bcf_lt_gap_bpspf_current_w + S (S x3) = w - 0111
rewrite <- hleft_value_witness_right_right_witness_witness_witness_left - 0112
exact hiw - 0113
have hcurrent_v : Lt(S x3,v)Exact native replay line
have hcurrent_v : exists bcf_lt_gap_bpspf_current_v. bcf_lt_gap_bpspf_current_v + S (S x3) = v - 0114
rewrite <- hleft_value_witness_right_right_witness_witness_witness_left - 0115
exact hiv - 0116
have hprevious_w : Lt(x3,w)Exact native replay line
have hprevious_w : exists bcf_lt_gap_bpspf_previous_w. bcf_lt_gap_bpspf_previous_w + S (x3) = w - 0117
specialize lt_to_le (S x3) - 0118
specialize lt_to_le w - 0119
apply lt_to_le - 0120
exact hcurrent_w - 0121
have hprevious_v : Lt(x3,v)Exact native replay line
have hprevious_v : exists bcf_lt_gap_bpspf_previous_v. bcf_lt_gap_bpspf_previous_v + S (x3) = v - 0122
specialize lt_to_le (S x3) - 0123
specialize lt_to_le v - 0124
apply lt_to_le - 0125
exact hcurrent_v - 0126
have hright_previous : BetaAt(qb,qc,x3,x7)Exact native replay line
have hright_previous : ((exists bcf_height_bpspf_aligned_previous. bcf_height_bpspf_aligned_previous + S (x7) = S ((S (x3)) * qc)) /\ exists bcf_quotient_bpspf_aligned_previous. qb = bcf_quotient_bpspf_aligned_previous * S ((S (x3)) * qc) + (x7)) - 0127
rewrite hpred - 0128
rewrite hpred - 0129
exact hright_value_witness_right_right_witness_witness_witness_right_left - 0130
have hright_current : BetaAt(qb,qc,S x3,x8)Exact native replay line
have hright_current : ((exists bcf_height_bpspf_aligned_current. bcf_height_bpspf_aligned_current + S (x8) = S ((S (S x3)) * qc)) /\ exists bcf_quotient_bpspf_aligned_current. qb = bcf_quotient_bpspf_aligned_current * S ((S (S x3)) * qc) + (x8)) - 0131
rewrite hpred - 0132
rewrite hpred - 0133
exact hright_value_witness_right_right_witness_witness_witness_right_right_left - 0134
have hu : x4 = x7 - 0135
specialize hagree x3 - 0136
specialize hagree x4 - 0137
specialize hagree x7 - 0138
apply hagree - 0139
exact hprevious_w - 0140
exact hprevious_v - 0141
exact hleft_value_witness_right_right_witness_witness_witness_right_left - 0142
exact hright_previous - 0143
have hv : x5 = x8 - 0144
specialize hagree (S x3) - 0145
specialize hagree x5 - 0146
specialize hagree x8 - 0147
apply hagree - 0148
exact hcurrent_w - 0149
exact hcurrent_v - 0150
exact hleft_value_witness_right_right_witness_witness_witness_right_right_left - 0151
exact hright_current - 0152
trans x1 - 0153
exact hx_value - 0154
trans x4 + x5 - 0155
exact hleft_value_witness_right_right_witness_witness_witness_right_right_right - 0156
trans x7 + x8 - 0157
congr - 0158
exact hu - 0159
exact hv - 0160
trans x2 - 0161
symm - 0162
exact hright_value_witness_right_right_witness_witness_witness_right_right_right - 0163
symm - 0164
exact hy_value