CF0004

continued_fraction_trace_extend

A strict Euclidean division prepends its quotient and extends one beta-coded history without changing any earlier state.

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable

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 theorem in conservative defined notation

∀ a. ∀ b. ∀ q. ∀ r. ∀ t. ∀ h. ∀ e. ∀ l. a = b · q + r → Lt(r,b) → ContinuedFractionTrace(b,r,t,h,e,l) → ∃ x. ∃ y. ∃ z. ListCell(x,q,t) ∧ ContinuedFractionTrace(a,b,x,y,z,S l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ListCell(s,q,t) · 1ContinuedFractionTrace(a,b,s,u,v,ell) · 2Lt(a,b) · 1

Actual proof prerequisites

cell_constructor · checked external prerequisitebeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitezero_add · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisitesucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall a b q r t h e l. a = b * q + r -> (exists ff_lt_cf_extension_bound. ff_lt_cf_extension_bound + S r = b) -> (exists cf_gcd_old. ((((exists ff_h_cf_old_initial_state. ff_h_cf_old_initial_state + S (((cf_gcd_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_old_initial_state. h = ff_q_cf_old_initial_state * S ((S (0)) * e) + (((cf_gcd_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_old_terminal_state. ff_h_cf_old_terminal_state + S (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))) = S ((S (l)) * e)) /\ exists ff_q_cf_old_terminal_state. h = ff_q_cf_old_terminal_state * S ((S (l)) * e) + (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))))) /\ forall cf_index_old. (exists ff_lt_cf_old_index. ff_lt_cf_old_index + S cf_index_old = l) -> exists cf_old_a_old cf_old_b_old cf_tail_old cf_new_a_old cf_new_b_old cf_head_old cf_quotient_old. ((((exists ff_h_cf_old_previous_state. ff_h_cf_old_previous_state + S (((cf_old_a_old) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old)))) * S ((cf_old_a_old) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old)))) + ((((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old))) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old))))) = S ((S (cf_index_old)) * e)) /\ exists ff_q_cf_old_previous_state. h = ff_q_cf_old_previous_state * S ((S (cf_index_old)) * e) + (((cf_old_a_old) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old)))) * S ((cf_old_a_old) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old)))) + ((((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old))) + (((cf_old_b_old) + (cf_tail_old)) * S ((cf_old_b_old) + (cf_tail_old)) + ((cf_tail_old) + (cf_tail_old))))))) /\ ((((exists ff_h_cf_old_following_state. ff_h_cf_old_following_state + S (((cf_new_a_old) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old)))) * S ((cf_new_a_old) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old)))) + ((((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old))) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old))))) = S ((S (S cf_index_old)) * e)) /\ exists ff_q_cf_old_following_state. h = ff_q_cf_old_following_state * S ((S (S cf_index_old)) * e) + (((cf_new_a_old) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old)))) * S ((cf_new_a_old) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old)))) + ((((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old))) + (((cf_new_b_old) + (cf_head_old)) * S ((cf_new_b_old) + (cf_head_old)) + ((cf_head_old) + (cf_head_old))))))) /\ (cf_new_b_old = cf_old_a_old /\ (cf_new_a_old = cf_new_b_old * cf_quotient_old + cf_old_b_old /\ ((exists ff_lt_cf_old_remainder. ff_lt_cf_old_remainder + S cf_old_b_old = cf_new_b_old) /\ (cf_head_old = S ((cf_quotient_old + cf_tail_old) * S (cf_quotient_old + cf_tail_old) + (cf_tail_old + cf_tail_old))))))))))) -> exists s z c. ((s = S ((q + t) * S (q + t) + (t + t))) /\ (exists cf_gcd_new. ((((exists ff_h_cf_new_initial_state. ff_h_cf_new_initial_state + S (((cf_gcd_new) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_new) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * c)) /\ exists ff_q_cf_new_initial_state. z = ff_q_cf_new_initial_state * S ((S (0)) * c) + (((cf_gcd_new) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_new) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_new_terminal_state. ff_h_cf_new_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (S l)) * c)) /\ exists ff_q_cf_new_terminal_state. z = ff_q_cf_new_terminal_state * S ((S (S l)) * c) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_new. (exists ff_lt_cf_new_index. ff_lt_cf_new_index + S cf_index_new = S l) -> exists cf_old_a_new cf_old_b_new cf_tail_new cf_new_a_new cf_new_b_new cf_head_new cf_quotient_new. ((((exists ff_h_cf_new_previous_state. ff_h_cf_new_previous_state + S (((cf_old_a_new) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new)))) * S ((cf_old_a_new) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new)))) + ((((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new))) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new))))) = S ((S (cf_index_new)) * c)) /\ exists ff_q_cf_new_previous_state. z = ff_q_cf_new_previous_state * S ((S (cf_index_new)) * c) + (((cf_old_a_new) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new)))) * S ((cf_old_a_new) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new)))) + ((((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new))) + (((cf_old_b_new) + (cf_tail_new)) * S ((cf_old_b_new) + (cf_tail_new)) + ((cf_tail_new) + (cf_tail_new))))))) /\ ((((exists ff_h_cf_new_following_state. ff_h_cf_new_following_state + S (((cf_new_a_new) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new)))) * S ((cf_new_a_new) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new)))) + ((((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new))) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new))))) = S ((S (S cf_index_new)) * c)) /\ exists ff_q_cf_new_following_state. z = ff_q_cf_new_following_state * S ((S (S cf_index_new)) * c) + (((cf_new_a_new) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new)))) * S ((cf_new_a_new) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new)))) + ((((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new))) + (((cf_new_b_new) + (cf_head_new)) * S ((cf_new_b_new) + (cf_head_new)) + ((cf_head_new) + (cf_head_new))))))) /\ (cf_new_b_new = cf_old_a_new /\ (cf_new_a_new = cf_new_b_new * cf_quotient_new + cf_old_b_new /\ ((exists ff_lt_cf_new_remainder. ff_lt_cf_new_remainder + S cf_old_b_new = cf_new_b_new) /\ (cf_head_new = S ((cf_quotient_new + cf_tail_new) * S (cf_quotient_new + cf_tail_new) + (cf_tail_new + cf_tail_new))))))))))))

Complete unchanged native tactic proof

All 133 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

133 script commands · 52 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 a
  2. L2
    intro b
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro t
  6. L6
    intro h
  7. L7
    intro e
  8. L8
    intro l
  9. L9
    intro hdivision
  10. L10
    intro hbound
02Fix variables and assumptionsL11–11

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

  1. L11
    intro htrace
03Use earlier factsL12–13

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

  1. L12
    specialize cell_constructor q
  2. L13
    specialize cell_constructor t
04Separate the logical casesL14–14

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

  1. L14
    cases cell_constructor
05Establish hsL15–16

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

  1. L15
    have hs : x = S ((q + t) * S (q + t) + (t + t))
  2. L16
    exact cell_constructor_witness
06Separate the logical casesL17–19

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

  1. L17
    cases htrace
  2. L18
    cases htrace_witness
  3. L19
    cases htrace_witness_right
07Establish hextensionL20–25

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

  1. L20
    have hextension : ∃ z. ∃ c. Beta(z,c,S l,(a + ((b + x) · S (b + x) + (x + x))) · S (a + ((b + x) · S (b + x) + (x + x))) + ((b + x) · S (b + x) + (x + x) + ((b + x) · S (b + x) + (x + x)))) ∧ (∀ y. ∀ n. Lt(y,S l) → Beta(h,e,y,n) → Beta(z,c,y,n))Definitions: BetaLtOriginal native command in the exact edition
  2. L21
    specialize beta_prefix_extend (S l)
  3. L22
    specialize beta_prefix_extend h
  4. L23
    specialize beta_prefix_extend e
  5. L24
    specialize beta_prefix_extend (((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) * S ((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) + ((((b) + (x)) * S ((b) + (x)) + ((x) + (x))) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))))
  6. L25
    exact beta_prefix_extend
08Separate the logical casesL26–28

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

  1. L26
    cases hextension
  2. L27
    cases hextension_witness
  3. L28
    cases hextension_witness_witness
09Construct an explicit witnessL29–31

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

  1. L29
    exists x
  2. L30
    exists x2
  3. L31
    exists x3
10Separate the logical casesL32–32

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

  1. L32
    split
11Use earlier factsL33–33

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

  1. L33
    exact hs
12Construct an explicit witnessL34–34

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

  1. L34
    exists x1
13Separate the logical casesL35–35

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

  1. L35
    split
14Use earlier factsL36–38

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

  1. L36
    specialize hextension_witness_witness_right 0
  2. L37
    specialize hextension_witness_witness_right (((x1) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((x1) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  3. L38
    apply hextension_witness_witness_right
15Construct an explicit witnessL39–39

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

  1. L39
    exists l
16Calculate and transport equalitiesL40–40

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

  1. L40
    simp
17Use earlier factsL41–41

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

  1. L41
    exact htrace_witness_left
18Separate the logical casesL42–42

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

  1. L42
    split
19Use earlier factsL43–43

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

  1. L43
    exact hextension_witness_witness_left
20Fix variables and assumptionsL44–45

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

  1. L44
    intro i
  2. L45
    intro hi
21Establish hsplitL46–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L46
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L47
    specialize finite_lt_succ_eq_or_lt l
  3. L48
    specialize finite_lt_succ_eq_or_lt i
  4. L49
    apply finite_lt_succ_eq_or_lt
  5. L50
    exact hi
22Separate the logical casesL51–51

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

  1. L51
    cases hsplit
23Calculate and transport equalitiesL52–55

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

  1. L52
    rewrite hsplit_left
  2. L53
    rewrite hsplit_left
  3. L54
    rewrite hsplit_left
  4. L55
    rewrite hsplit_left
24Construct an explicit witnessL56–62

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

  1. L56
    exists b
  2. L57
    exists r
  3. L58
    exists t
  4. L59
    exists a
  5. L60
    exists b
  6. L61
    exists x
  7. L62
    exists q
25Separate the logical casesL63–63

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

  1. L63
    split
26Use earlier factsL64–66

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

  1. L64
    specialize hextension_witness_witness_right l
  2. L65
    specialize hextension_witness_witness_right (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))))
  3. L66
    apply hextension_witness_witness_right
27Construct an explicit witnessL67–67

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

  1. L67
    exists 0
28Use earlier factsL68–69

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

  1. L68
    apply zero_add
  2. L69
    exact htrace_witness_right_left
29Separate the logical casesL70–70

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

  1. L70
    split
30Use earlier factsL71–71

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

  1. L71
    exact hextension_witness_witness_left
31Separate the logical casesL72–72

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

  1. L72
    split
32Calculate and transport equalitiesL73–73

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

  1. L73
    refl
33Separate the logical casesL74–74

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

  1. L74
    split
34Use earlier factsL75–75

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

  1. L75
    exact hdivision
35Separate the logical casesL76–76

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

  1. L76
    split
36Use earlier factsL77–79

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

  1. L77
    exact hbound
  2. L78
    exact hs
  3. L79
    specialize htrace_witness_right_right i
37Establish hpreviousL80–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply htrace witness right right.

  1. L80
    have hprevious : ∃ A. ∃ B. ∃ T. ∃ C. ∃ D. ∃ U. ∃ Q. Beta(h,e,i,(A + ((B + T) · S (B + T) + (T + T))) · S (A + ((B + T) · S (B + T) + (T + T))) + ((B + T) · S (B + T) + (T + T) + ((B + T) · S (B + T) + (T + T)))) ∧ (Beta(h,e,S i,(C + ((D + U) · S (D + U) + (U + U))) · S (C + ((D + U) · S (D + U) + (U + U))) + ((D + U) · S (D + U) + (U + U) + ((D + U) · S (D + U) + (U + U)))) ∧ (D = A ∧ (C = D · Q + B ∧ (Lt(B,D) ∧ ListCell(U,Q,T)))))Definitions: BetaListCellLtOriginal native command in the exact edition
  2. L81
    apply htrace_witness_right_right
  3. L82
    exact hsplit_right
38Separate the logical casesL83–92

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

  1. L83
    cases hprevious
  2. L84
    cases hprevious_witness
  3. L85
    cases hprevious_witness_witness
  4. L86
    cases hprevious_witness_witness_witness
  5. L87
    cases hprevious_witness_witness_witness_witness
  6. L88
    cases hprevious_witness_witness_witness_witness_witness
  7. L89
    cases hprevious_witness_witness_witness_witness_witness_witness
  8. L90
    cases hprevious_witness_witness_witness_witness_witness_witness_witness
  9. L91
    cases hprevious_witness_witness_witness_witness_witness_witness_witness_right
  10. L92
    cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right
39Separate the logical casesL93–94

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

  1. L93
    cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right
  2. L94
    cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
40Establish hipreserveL95–102

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L95
    have hipreserve : exists gap. gap + S i = S l
  2. L96
    specialize lt_of_lt_of_le i
  3. L97
    specialize lt_of_lt_of_le l
  4. L98
    specialize lt_of_lt_of_le (S l)
  5. L99
    apply lt_of_lt_of_le
  6. L100
    exact hsplit_right
  7. L101
    specialize le_succ_self l
  8. L102
    exact le_succ_self
41Establish hnextpreserveL103–107

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

  1. L103
    have hnextpreserve : exists gap. gap + S (S i) = S l
  2. L104
    specialize succ_le_succ (S i)
  3. L105
    specialize succ_le_succ l
  4. L106
    apply succ_le_succ
  5. L107
    exact hsplit_right
42Construct an explicit witnessL108–114

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

  1. L108
    exists x4
  2. L109
    exists x5
  3. L110
    exists x6
  4. L111
    exists x7
  5. L112
    exists x8
  6. L113
    exists x9
  7. L114
    exists x10
43Separate the logical casesL115–115

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

  1. L115
    split
44Use earlier factsL116–120

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

  1. L116
    specialize hextension_witness_witness_right i
  2. L117
    specialize hextension_witness_witness_right (((x4) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))) * S ((x4) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))) + ((((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6))) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))))
  3. L118
    apply hextension_witness_witness_right
  4. L119
    exact hipreserve
  5. L120
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_left
45Separate the logical casesL121–121

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

  1. L121
    split
46Use earlier factsL122–126

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

  1. L122
    specialize hextension_witness_witness_right (S i)
  2. L123
    specialize hextension_witness_witness_right (((x7) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((x7) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  3. L124
    apply hextension_witness_witness_right
  4. L125
    exact hnextpreserve
  5. L126
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_left
47Separate the logical casesL127–127

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

  1. L127
    split
48Use earlier factsL128–128

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

  1. L128
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_left
49Separate the logical casesL129–129

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

  1. L129
    split
50Use earlier factsL130–130

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

  1. L130
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
51Separate the logical casesL131–131

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

  1. L131
    split
52Use earlier factsL132–133

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

  1. L132
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  2. L133
    exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro t
  6. 0006intro h
  7. 0007intro e
  8. 0008intro l
  9. 0009intro hdivision
  10. 0010intro hbound
  11. 0011intro htrace
  12. 0012specialize cell_constructor q
  13. 0013specialize cell_constructor t
  14. 0014cases cell_constructor
  15. 0015have hs : x = S ((q + t) * S (q + t) + (t + t))
  16. 0016exact cell_constructor_witness
  17. 0017cases htrace
  18. 0018cases htrace_witness
  19. 0019cases htrace_witness_right
  20. 0020have hextension : exists z c. ((((exists ff_h_cf_extension_new_state. ff_h_cf_extension_new_state + S (((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) * S ((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) + ((((b) + (x)) * S ((b) + (x)) + ((x) + (x))) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x))))) = S ((S (S l)) * c)) /\ exists ff_q_cf_extension_new_state. z = ff_q_cf_extension_new_state * S ((S (S l)) * c) + (((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) * S ((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) + ((((b) + (x)) * S ((b) + (x)) + ((x) + (x))) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x))))))) /\ forall j v. (exists ff_lt_cf_extension_prefix_bound. ff_lt_cf_extension_prefix_bound + S j = S l) -> (((exists ff_h_cf_extension_source. ff_h_cf_extension_source + S (v) = S ((S (j)) * e)) /\ exists ff_q_cf_extension_source. h = ff_q_cf_extension_source * S ((S (j)) * e) + (v))) -> (((exists ff_h_cf_extension_target. ff_h_cf_extension_target + S (v) = S ((S (j)) * c)) /\ exists ff_q_cf_extension_target. z = ff_q_cf_extension_target * S ((S (j)) * c) + (v))))
  21. 0021specialize beta_prefix_extend (S l)
  22. 0022specialize beta_prefix_extend h
  23. 0023specialize beta_prefix_extend e
  24. 0024specialize beta_prefix_extend (((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) * S ((a) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))) + ((((b) + (x)) * S ((b) + (x)) + ((x) + (x))) + (((b) + (x)) * S ((b) + (x)) + ((x) + (x)))))
  25. 0025exact beta_prefix_extend
  26. 0026cases hextension
  27. 0027cases hextension_witness
  28. 0028cases hextension_witness_witness
  29. 0029exists x
  30. 0030exists x2
  31. 0031exists x3
  32. 0032split
  33. 0033exact hs
  34. 0034exists x1
  35. 0035split
  36. 0036specialize hextension_witness_witness_right 0
  37. 0037specialize hextension_witness_witness_right (((x1) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((x1) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  38. 0038apply hextension_witness_witness_right
  39. 0039exists l
  40. 0040simp
  41. 0041exact htrace_witness_left
  42. 0042split
  43. 0043exact hextension_witness_witness_left
  44. 0044intro i
  45. 0045intro hi
  46. 0046have hsplit : i = l \/ exists gap. gap + S i = l
  47. 0047specialize finite_lt_succ_eq_or_lt l
  48. 0048specialize finite_lt_succ_eq_or_lt i
  49. 0049apply finite_lt_succ_eq_or_lt
  50. 0050exact hi
  51. 0051cases hsplit
  52. 0052rewrite hsplit_left
  53. 0053rewrite hsplit_left
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exists b
  57. 0057exists r
  58. 0058exists t
  59. 0059exists a
  60. 0060exists b
  61. 0061exists x
  62. 0062exists q
  63. 0063split
  64. 0064specialize hextension_witness_witness_right l
  65. 0065specialize hextension_witness_witness_right (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))))
  66. 0066apply hextension_witness_witness_right
  67. 0067exists 0
  68. 0068apply zero_add
  69. 0069exact htrace_witness_right_left
  70. 0070split
  71. 0071exact hextension_witness_witness_left
  72. 0072split
  73. 0073refl
  74. 0074split
  75. 0075exact hdivision
  76. 0076split
  77. 0077exact hbound
  78. 0078exact hs
  79. 0079specialize htrace_witness_right_right i
  80. 0080have hprevious : exists A B T C D U Q. ((((exists ff_h_cf_previous_old_state. ff_h_cf_previous_old_state + S (((A) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T)))) * S ((A) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T)))) + ((((B) + (T)) * S ((B) + (T)) + ((T) + (T))) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T))))) = S ((S (i)) * e)) /\ exists ff_q_cf_previous_old_state. h = ff_q_cf_previous_old_state * S ((S (i)) * e) + (((A) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T)))) * S ((A) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T)))) + ((((B) + (T)) * S ((B) + (T)) + ((T) + (T))) + (((B) + (T)) * S ((B) + (T)) + ((T) + (T))))))) /\ ((((exists ff_h_cf_previous_new_state. ff_h_cf_previous_new_state + S (((C) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U)))) * S ((C) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U)))) + ((((D) + (U)) * S ((D) + (U)) + ((U) + (U))) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U))))) = S ((S (S i)) * e)) /\ exists ff_q_cf_previous_new_state. h = ff_q_cf_previous_new_state * S ((S (S i)) * e) + (((C) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U)))) * S ((C) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U)))) + ((((D) + (U)) * S ((D) + (U)) + ((U) + (U))) + (((D) + (U)) * S ((D) + (U)) + ((U) + (U))))))) /\ (D = A /\ (C = D * Q + B /\ ((exists ff_lt_cf_previous_remainder. ff_lt_cf_previous_remainder + S B = D) /\ (U = S ((Q + T) * S (Q + T) + (T + T))))))))
  81. 0081apply htrace_witness_right_right
  82. 0082exact hsplit_right
  83. 0083cases hprevious
  84. 0084cases hprevious_witness
  85. 0085cases hprevious_witness_witness
  86. 0086cases hprevious_witness_witness_witness
  87. 0087cases hprevious_witness_witness_witness_witness
  88. 0088cases hprevious_witness_witness_witness_witness_witness
  89. 0089cases hprevious_witness_witness_witness_witness_witness_witness
  90. 0090cases hprevious_witness_witness_witness_witness_witness_witness_witness
  91. 0091cases hprevious_witness_witness_witness_witness_witness_witness_witness_right
  92. 0092cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right
  93. 0093cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right
  94. 0094cases hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  95. 0095have hipreserve : exists gap. gap + S i = S l
  96. 0096specialize lt_of_lt_of_le i
  97. 0097specialize lt_of_lt_of_le l
  98. 0098specialize lt_of_lt_of_le (S l)
  99. 0099apply lt_of_lt_of_le
  100. 0100exact hsplit_right
  101. 0101specialize le_succ_self l
  102. 0102exact le_succ_self
  103. 0103have hnextpreserve : exists gap. gap + S (S i) = S l
  104. 0104specialize succ_le_succ (S i)
  105. 0105specialize succ_le_succ l
  106. 0106apply succ_le_succ
  107. 0107exact hsplit_right
  108. 0108exists x4
  109. 0109exists x5
  110. 0110exists x6
  111. 0111exists x7
  112. 0112exists x8
  113. 0113exists x9
  114. 0114exists x10
  115. 0115split
  116. 0116specialize hextension_witness_witness_right i
  117. 0117specialize hextension_witness_witness_right (((x4) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))) * S ((x4) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))) + ((((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6))) + (((x5) + (x6)) * S ((x5) + (x6)) + ((x6) + (x6)))))
  118. 0118apply hextension_witness_witness_right
  119. 0119exact hipreserve
  120. 0120exact hprevious_witness_witness_witness_witness_witness_witness_witness_left
  121. 0121split
  122. 0122specialize hextension_witness_witness_right (S i)
  123. 0123specialize hextension_witness_witness_right (((x7) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) * S ((x7) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))) + ((((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9))) + (((x8) + (x9)) * S ((x8) + (x9)) + ((x9) + (x9)))))
  124. 0124apply hextension_witness_witness_right
  125. 0125exact hnextpreserve
  126. 0126exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_left
  127. 0127split
  128. 0128exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_left
  129. 0129split
  130. 0130exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  131. 0131split
  132. 0132exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  133. 0133exact hprevious_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right