BA002D

cf_convergent_old_history_nonempty_head

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A genuine nonempty quotient list in G071 exposes an actual Euclidean first step and an actual shorter history length.

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 first-order arithmetic statement

forall a b s h e L. (exists cf_gcd_head_source. ((((exists ff_h_cf_head_source_initial_state. ff_h_cf_head_source_initial_state + S (((cf_gcd_head_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_source) + (((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_head_source_initial_state. h = ff_q_cf_head_source_initial_state * S ((S (0)) * e) + (((cf_gcd_head_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_source) + (((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_head_source_terminal_state. ff_h_cf_head_source_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 (L)) * e)) /\ exists ff_q_cf_head_source_terminal_state. h = ff_q_cf_head_source_terminal_state * S ((S (L)) * e) + (((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_head_source. (exists ff_lt_cf_head_source_index. ff_lt_cf_head_source_index + S cf_index_head_source = L) -> exists cf_old_a_head_source cf_old_b_head_source cf_tail_head_source cf_new_a_head_source cf_new_b_head_source cf_head_head_source cf_quotient_head_source. ((((exists ff_h_cf_head_source_previous_state. ff_h_cf_head_source_previous_state + S (((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) * S ((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) + ((((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))))) = S ((S (cf_index_head_source)) * e)) /\ exists ff_q_cf_head_source_previous_state. h = ff_q_cf_head_source_previous_state * S ((S (cf_index_head_source)) * e) + (((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) * S ((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) + ((((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))))))) /\ ((((exists ff_h_cf_head_source_following_state. ff_h_cf_head_source_following_state + S (((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) * S ((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) + ((((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))))) = S ((S (S cf_index_head_source)) * e)) /\ exists ff_q_cf_head_source_following_state. h = ff_q_cf_head_source_following_state * S ((S (S cf_index_head_source)) * e) + (((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) * S ((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) + ((((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))))))) /\ (cf_new_b_head_source = cf_old_a_head_source /\ (cf_new_a_head_source = cf_new_b_head_source * cf_quotient_head_source + cf_old_b_head_source /\ ((exists ff_lt_cf_head_source_remainder. ff_lt_cf_head_source_remainder + S cf_old_b_head_source = cf_new_b_head_source) /\ (cf_head_head_source = S ((cf_quotient_head_source + cf_tail_head_source) * S (cf_quotient_head_source + cf_tail_head_source) + (cf_tail_head_source + cf_tail_head_source))))))))))) -> ~(s = 0) -> (exists cfc_q_head_result cfc_r_head_result cfc_tail_head_result cfc_length_head_result. (((L) = S cfc_length_head_result) /\ (((a) = (b) * cfc_q_head_result + cfc_r_head_result) /\ ((exists cfba_gap_head_resultbound. cfba_gap_head_resultbound + S (cfc_r_head_result) = (b)) /\ ((s = S ((cfc_q_head_result + cfc_tail_head_result) * S (cfc_q_head_result + cfc_tail_head_result) + (cfc_tail_head_result + cfc_tail_head_result))) /\ (exists cf_gcd_head_resulthistory. ((((exists ff_h_cf_head_resulthistory_initial_state. ff_h_cf_head_resulthistory_initial_state + S (((cf_gcd_head_resulthistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_resulthistory) + (((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_head_resulthistory_initial_state. h = ff_q_cf_head_resulthistory_initial_state * S ((S (0)) * e) + (((cf_gcd_head_resulthistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_resulthistory) + (((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_head_resulthistory_terminal_state. ff_h_cf_head_resulthistory_terminal_state + S (((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) * S ((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) + ((((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))))) = S ((S (cfc_length_head_result)) * e)) /\ exists ff_q_cf_head_resulthistory_terminal_state. h = ff_q_cf_head_resulthistory_terminal_state * S ((S (cfc_length_head_result)) * e) + (((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) * S ((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) + ((((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))))))) /\ forall cf_index_head_resulthistory. (exists ff_lt_cf_head_resulthistory_index. ff_lt_cf_head_resulthistory_index + S cf_index_head_resulthistory = cfc_length_head_result) -> exists cf_old_a_head_resulthistory cf_old_b_head_resulthistory cf_tail_head_resulthistory cf_new_a_head_resulthistory cf_new_b_head_resulthistory cf_head_head_resulthistory cf_quotient_head_resulthistory. ((((exists ff_h_cf_head_resulthistory_previous_state. ff_h_cf_head_resulthistory_previous_state + S (((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) * S ((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) + ((((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))))) = S ((S (cf_index_head_resulthistory)) * e)) /\ exists ff_q_cf_head_resulthistory_previous_state. h = ff_q_cf_head_resulthistory_previous_state * S ((S (cf_index_head_resulthistory)) * e) + (((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) * S ((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) + ((((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))))))) /\ ((((exists ff_h_cf_head_resulthistory_following_state. ff_h_cf_head_resulthistory_following_state + S (((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) * S ((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) + ((((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))))) = S ((S (S cf_index_head_resulthistory)) * e)) /\ exists ff_q_cf_head_resulthistory_following_state. h = ff_q_cf_head_resulthistory_following_state * S ((S (S cf_index_head_resulthistory)) * e) + (((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) * S ((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) + ((((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))))))) /\ (cf_new_b_head_resulthistory = cf_old_a_head_resulthistory /\ (cf_new_a_head_resulthistory = cf_new_b_head_resulthistory * cf_quotient_head_resulthistory + cf_old_b_head_resulthistory /\ ((exists ff_lt_cf_head_resulthistory_remainder. ff_lt_cf_head_resulthistory_remainder + S cf_old_b_head_resulthistory = cf_new_b_head_resulthistory) /\ (cf_head_head_resulthistory = S ((cf_quotient_head_resulthistory + cf_tail_head_resulthistory) * S (cf_quotient_head_resulthistory + cf_tail_head_resulthistory) + (cf_tail_head_resulthistory + cf_tail_head_resulthistory))))))))))))))))

Constructive proof overview

Generated structural guide

A genuine nonempty quotient list in G071 exposes an actual Euclidean first step and an actual shorter history length.

The unchanged tactic script uses 4 declared prerequisites and contains 75 exact native proof lines.

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

Proof neighborhood

Direct dependencies

zero_or_succ Stable theorem; checked-use authorized BA002C cf_convergent_old_history_length_transport BA0029 cf_convergent_old_history_zero_elimination BA002A cf_convergent_old_history_successor_elimination

Direct dependents

BA003D cf_convergent_euclidean_matrix_step_alignment

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

75 script commands · 22 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 (3)
cf convergent old history length transportcf convergent old history zero eliminationcf convergent old history successor elimination

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–8

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro h
  5. L5
    intro e
  6. L6
    intro L
  7. L7
    intro ht
  8. L8
    intro hn
02Establish hlL9–11

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

  1. L9
    have hl : L = 0 \/ exists k. L = S k
  2. L10
    specialize zero_or_succ (L)
  3. L11
    apply zero_or_succ
03Separate the logical casesL12–12

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

  1. L12
    cases hl
04Establish hzL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history length transport.

  1. L13
    have hz : ContinuedFractionTrace(a,b,s,h,e,0)Definitions: ContinuedFractionTrace
  2. L14
    specialize cf_convergent_old_history_length_transport (a)
  3. L15
    specialize cf_convergent_old_history_length_transport (b)
  4. L16
    specialize cf_convergent_old_history_length_transport (s)
  5. L17
    specialize cf_convergent_old_history_length_transport (h)
  6. L18
    specialize cf_convergent_old_history_length_transport (e)
  7. L19
    specialize cf_convergent_old_history_length_transport (L)
  8. L20
    specialize cf_convergent_old_history_length_transport (0)
  9. L21
    apply cf_convergent_old_history_length_transport
  10. L22
    exact hl_left
05Use earlier factsL23–23

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

  1. L23
    exact ht
06Establish heL24–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history zero elimination.

  1. L24
    have he : b = 0 /\ s = 0
  2. L25
    specialize cf_convergent_old_history_zero_elimination (a)
  3. L26
    specialize cf_convergent_old_history_zero_elimination (b)
  4. L27
    specialize cf_convergent_old_history_zero_elimination (s)
  5. L28
    specialize cf_convergent_old_history_zero_elimination (h)
  6. L29
    specialize cf_convergent_old_history_zero_elimination (e)
  7. L30
    apply cf_convergent_old_history_zero_elimination
  8. L31
    exact hz
07Separate the logical casesL32–33

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

  1. L32
    cases he
  2. L33
    exfalso
08Use earlier factsL34–35

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

  1. L34
    apply hn
  2. L35
    exact he_right
09Separate the logical casesL36–36

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

  1. L36
    cases hl_right
10Establish hhL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history length transport.

  1. L37
    have hh : ContinuedFractionTrace(a,b,s,h,e,S x)Definitions: ContinuedFractionTrace
  2. L38
    specialize cf_convergent_old_history_length_transport (a)
  3. L39
    specialize cf_convergent_old_history_length_transport (b)
  4. L40
    specialize cf_convergent_old_history_length_transport (s)
  5. L41
    specialize cf_convergent_old_history_length_transport (h)
  6. L42
    specialize cf_convergent_old_history_length_transport (e)
  7. L43
    specialize cf_convergent_old_history_length_transport (L)
  8. L44
    specialize cf_convergent_old_history_length_transport (S x)
  9. L45
    apply cf_convergent_old_history_length_transport
  10. L46
    exact hl_right_witness
11Use earlier factsL47–47

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

  1. L47
    exact ht
12Establish hpL48–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history successor elimination.

  1. L48
    have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,h,e,x)))Definitions: ListCellContinuedFractionTraceLt
  2. L49
    specialize cf_convergent_old_history_successor_elimination (a)
  3. L50
    specialize cf_convergent_old_history_successor_elimination (b)
  4. L51
    specialize cf_convergent_old_history_successor_elimination (s)
  5. L52
    specialize cf_convergent_old_history_successor_elimination (h)
  6. L53
    specialize cf_convergent_old_history_successor_elimination (e)
  7. L54
    specialize cf_convergent_old_history_successor_elimination (x)
  8. L55
    apply cf_convergent_old_history_successor_elimination
  9. L56
    exact hh
13Separate the logical casesL57–62

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

  1. L57
    cases hp
  2. L58
    cases hp_witness
  3. L59
    cases hp_witness_witness
  4. L60
    cases hp_witness_witness_witness
  5. L61
    cases hp_witness_witness_witness_right
  6. L62
    cases hp_witness_witness_witness_right_right
14Construct an explicit witnessL63–66

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

  1. L63
    exists x1
  2. L64
    exists x2
  3. L65
    exists x3
  4. L66
    exists x
15Separate the logical casesL67–67

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

  1. L67
    split
16Use earlier factsL68–68

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

  1. L68
    exact hl_right_witness
17Separate the logical casesL69–69

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

  1. L69
    split
18Use earlier factsL70–70

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

  1. L70
    exact hp_witness_witness_witness_left
19Separate the logical casesL71–71

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

  1. L71
    split
20Use earlier factsL72–72

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

  1. L72
    exact hp_witness_witness_witness_right_left
21Separate the logical casesL73–73

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

  1. L73
    split
22Use earlier factsL74–75

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

  1. L74
    exact hp_witness_witness_witness_right_right_left
  2. L75
    exact hp_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro L
  7. 0007intro ht
  8. 0008intro hn
  9. 0009have hl : L = 0 \/ exists k. L = S k
  10. 0010specialize zero_or_succ (L)
  11. 0011apply zero_or_succ
  12. 0012cases hl
  13. 0013have hz : exists cf_gcd_head_empty. ((((exists ff_h_cf_head_empty_initial_state. ff_h_cf_head_empty_initial_state + S (((cf_gcd_head_empty) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_empty) + (((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_head_empty_initial_state. h = ff_q_cf_head_empty_initial_state * S ((S (0)) * e) + (((cf_gcd_head_empty) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_empty) + (((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_head_empty_terminal_state. ff_h_cf_head_empty_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 (0)) * e)) /\ exists ff_q_cf_head_empty_terminal_state. h = ff_q_cf_head_empty_terminal_state * S ((S (0)) * e) + (((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_head_empty. (exists ff_lt_cf_head_empty_index. ff_lt_cf_head_empty_index + S cf_index_head_empty = 0) -> exists cf_old_a_head_empty cf_old_b_head_empty cf_tail_head_empty cf_new_a_head_empty cf_new_b_head_empty cf_head_head_empty cf_quotient_head_empty. ((((exists ff_h_cf_head_empty_previous_state. ff_h_cf_head_empty_previous_state + S (((cf_old_a_head_empty) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty)))) * S ((cf_old_a_head_empty) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty)))) + ((((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty))) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty))))) = S ((S (cf_index_head_empty)) * e)) /\ exists ff_q_cf_head_empty_previous_state. h = ff_q_cf_head_empty_previous_state * S ((S (cf_index_head_empty)) * e) + (((cf_old_a_head_empty) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty)))) * S ((cf_old_a_head_empty) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty)))) + ((((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty))) + (((cf_old_b_head_empty) + (cf_tail_head_empty)) * S ((cf_old_b_head_empty) + (cf_tail_head_empty)) + ((cf_tail_head_empty) + (cf_tail_head_empty))))))) /\ ((((exists ff_h_cf_head_empty_following_state. ff_h_cf_head_empty_following_state + S (((cf_new_a_head_empty) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty)))) * S ((cf_new_a_head_empty) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty)))) + ((((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty))) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty))))) = S ((S (S cf_index_head_empty)) * e)) /\ exists ff_q_cf_head_empty_following_state. h = ff_q_cf_head_empty_following_state * S ((S (S cf_index_head_empty)) * e) + (((cf_new_a_head_empty) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty)))) * S ((cf_new_a_head_empty) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty)))) + ((((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty))) + (((cf_new_b_head_empty) + (cf_head_head_empty)) * S ((cf_new_b_head_empty) + (cf_head_head_empty)) + ((cf_head_head_empty) + (cf_head_head_empty))))))) /\ (cf_new_b_head_empty = cf_old_a_head_empty /\ (cf_new_a_head_empty = cf_new_b_head_empty * cf_quotient_head_empty + cf_old_b_head_empty /\ ((exists ff_lt_cf_head_empty_remainder. ff_lt_cf_head_empty_remainder + S cf_old_b_head_empty = cf_new_b_head_empty) /\ (cf_head_head_empty = S ((cf_quotient_head_empty + cf_tail_head_empty) * S (cf_quotient_head_empty + cf_tail_head_empty) + (cf_tail_head_empty + cf_tail_head_empty))))))))))
  14. 0014specialize cf_convergent_old_history_length_transport (a)
  15. 0015specialize cf_convergent_old_history_length_transport (b)
  16. 0016specialize cf_convergent_old_history_length_transport (s)
  17. 0017specialize cf_convergent_old_history_length_transport (h)
  18. 0018specialize cf_convergent_old_history_length_transport (e)
  19. 0019specialize cf_convergent_old_history_length_transport (L)
  20. 0020specialize cf_convergent_old_history_length_transport (0)
  21. 0021apply cf_convergent_old_history_length_transport
  22. 0022exact hl_left
  23. 0023exact ht
  24. 0024have he : b = 0 /\ s = 0
  25. 0025specialize cf_convergent_old_history_zero_elimination (a)
  26. 0026specialize cf_convergent_old_history_zero_elimination (b)
  27. 0027specialize cf_convergent_old_history_zero_elimination (s)
  28. 0028specialize cf_convergent_old_history_zero_elimination (h)
  29. 0029specialize cf_convergent_old_history_zero_elimination (e)
  30. 0030apply cf_convergent_old_history_zero_elimination
  31. 0031exact hz
  32. 0032cases he
  33. 0033exfalso
  34. 0034apply hn
  35. 0035exact he_right
  36. 0036cases hl_right
  37. 0037have hh : exists cf_gcd_head_nonempty. ((((exists ff_h_cf_head_nonempty_initial_state. ff_h_cf_head_nonempty_initial_state + S (((cf_gcd_head_nonempty) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_nonempty) + (((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_head_nonempty_initial_state. h = ff_q_cf_head_nonempty_initial_state * S ((S (0)) * e) + (((cf_gcd_head_nonempty) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_nonempty) + (((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_head_nonempty_terminal_state. ff_h_cf_head_nonempty_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 x)) * e)) /\ exists ff_q_cf_head_nonempty_terminal_state. h = ff_q_cf_head_nonempty_terminal_state * S ((S (S x)) * e) + (((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_head_nonempty. (exists ff_lt_cf_head_nonempty_index. ff_lt_cf_head_nonempty_index + S cf_index_head_nonempty = S x) -> exists cf_old_a_head_nonempty cf_old_b_head_nonempty cf_tail_head_nonempty cf_new_a_head_nonempty cf_new_b_head_nonempty cf_head_head_nonempty cf_quotient_head_nonempty. ((((exists ff_h_cf_head_nonempty_previous_state. ff_h_cf_head_nonempty_previous_state + S (((cf_old_a_head_nonempty) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty)))) * S ((cf_old_a_head_nonempty) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty)))) + ((((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty))) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty))))) = S ((S (cf_index_head_nonempty)) * e)) /\ exists ff_q_cf_head_nonempty_previous_state. h = ff_q_cf_head_nonempty_previous_state * S ((S (cf_index_head_nonempty)) * e) + (((cf_old_a_head_nonempty) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty)))) * S ((cf_old_a_head_nonempty) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty)))) + ((((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty))) + (((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) * S ((cf_old_b_head_nonempty) + (cf_tail_head_nonempty)) + ((cf_tail_head_nonempty) + (cf_tail_head_nonempty))))))) /\ ((((exists ff_h_cf_head_nonempty_following_state. ff_h_cf_head_nonempty_following_state + S (((cf_new_a_head_nonempty) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty)))) * S ((cf_new_a_head_nonempty) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty)))) + ((((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty))) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty))))) = S ((S (S cf_index_head_nonempty)) * e)) /\ exists ff_q_cf_head_nonempty_following_state. h = ff_q_cf_head_nonempty_following_state * S ((S (S cf_index_head_nonempty)) * e) + (((cf_new_a_head_nonempty) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty)))) * S ((cf_new_a_head_nonempty) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty)))) + ((((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty))) + (((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) * S ((cf_new_b_head_nonempty) + (cf_head_head_nonempty)) + ((cf_head_head_nonempty) + (cf_head_head_nonempty))))))) /\ (cf_new_b_head_nonempty = cf_old_a_head_nonempty /\ (cf_new_a_head_nonempty = cf_new_b_head_nonempty * cf_quotient_head_nonempty + cf_old_b_head_nonempty /\ ((exists ff_lt_cf_head_nonempty_remainder. ff_lt_cf_head_nonempty_remainder + S cf_old_b_head_nonempty = cf_new_b_head_nonempty) /\ (cf_head_head_nonempty = S ((cf_quotient_head_nonempty + cf_tail_head_nonempty) * S (cf_quotient_head_nonempty + cf_tail_head_nonempty) + (cf_tail_head_nonempty + cf_tail_head_nonempty))))))))))
  38. 0038specialize cf_convergent_old_history_length_transport (a)
  39. 0039specialize cf_convergent_old_history_length_transport (b)
  40. 0040specialize cf_convergent_old_history_length_transport (s)
  41. 0041specialize cf_convergent_old_history_length_transport (h)
  42. 0042specialize cf_convergent_old_history_length_transport (e)
  43. 0043specialize cf_convergent_old_history_length_transport (L)
  44. 0044specialize cf_convergent_old_history_length_transport (S x)
  45. 0045apply cf_convergent_old_history_length_transport
  46. 0046exact hl_right_witness
  47. 0047exact ht
  48. 0048have hp : exists q r t. ((a = b * q + r) /\ ((exists cfba_gap_head_remainder. cfba_gap_head_remainder + S (r) = (b)) /\ ((s = S ((q + t) * S (q + t) + (t + t))) /\ (exists cf_gcd_head_predecessor. ((((exists ff_h_cf_head_predecessor_initial_state. ff_h_cf_head_predecessor_initial_state + S (((cf_gcd_head_predecessor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_predecessor) + (((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_head_predecessor_initial_state. h = ff_q_cf_head_predecessor_initial_state * S ((S (0)) * e) + (((cf_gcd_head_predecessor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_predecessor) + (((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_head_predecessor_terminal_state. ff_h_cf_head_predecessor_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 (x)) * e)) /\ exists ff_q_cf_head_predecessor_terminal_state. h = ff_q_cf_head_predecessor_terminal_state * S ((S (x)) * 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_head_predecessor. (exists ff_lt_cf_head_predecessor_index. ff_lt_cf_head_predecessor_index + S cf_index_head_predecessor = x) -> exists cf_old_a_head_predecessor cf_old_b_head_predecessor cf_tail_head_predecessor cf_new_a_head_predecessor cf_new_b_head_predecessor cf_head_head_predecessor cf_quotient_head_predecessor. ((((exists ff_h_cf_head_predecessor_previous_state. ff_h_cf_head_predecessor_previous_state + S (((cf_old_a_head_predecessor) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor)))) * S ((cf_old_a_head_predecessor) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor)))) + ((((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor))) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor))))) = S ((S (cf_index_head_predecessor)) * e)) /\ exists ff_q_cf_head_predecessor_previous_state. h = ff_q_cf_head_predecessor_previous_state * S ((S (cf_index_head_predecessor)) * e) + (((cf_old_a_head_predecessor) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor)))) * S ((cf_old_a_head_predecessor) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor)))) + ((((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor))) + (((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) * S ((cf_old_b_head_predecessor) + (cf_tail_head_predecessor)) + ((cf_tail_head_predecessor) + (cf_tail_head_predecessor))))))) /\ ((((exists ff_h_cf_head_predecessor_following_state. ff_h_cf_head_predecessor_following_state + S (((cf_new_a_head_predecessor) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor)))) * S ((cf_new_a_head_predecessor) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor)))) + ((((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor))) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor))))) = S ((S (S cf_index_head_predecessor)) * e)) /\ exists ff_q_cf_head_predecessor_following_state. h = ff_q_cf_head_predecessor_following_state * S ((S (S cf_index_head_predecessor)) * e) + (((cf_new_a_head_predecessor) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor)))) * S ((cf_new_a_head_predecessor) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor)))) + ((((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor))) + (((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) * S ((cf_new_b_head_predecessor) + (cf_head_head_predecessor)) + ((cf_head_head_predecessor) + (cf_head_head_predecessor))))))) /\ (cf_new_b_head_predecessor = cf_old_a_head_predecessor /\ (cf_new_a_head_predecessor = cf_new_b_head_predecessor * cf_quotient_head_predecessor + cf_old_b_head_predecessor /\ ((exists ff_lt_cf_head_predecessor_remainder. ff_lt_cf_head_predecessor_remainder + S cf_old_b_head_predecessor = cf_new_b_head_predecessor) /\ (cf_head_head_predecessor = S ((cf_quotient_head_predecessor + cf_tail_head_predecessor) * S (cf_quotient_head_predecessor + cf_tail_head_predecessor) + (cf_tail_head_predecessor + cf_tail_head_predecessor))))))))))))))
  49. 0049specialize cf_convergent_old_history_successor_elimination (a)
  50. 0050specialize cf_convergent_old_history_successor_elimination (b)
  51. 0051specialize cf_convergent_old_history_successor_elimination (s)
  52. 0052specialize cf_convergent_old_history_successor_elimination (h)
  53. 0053specialize cf_convergent_old_history_successor_elimination (e)
  54. 0054specialize cf_convergent_old_history_successor_elimination (x)
  55. 0055apply cf_convergent_old_history_successor_elimination
  56. 0056exact hh
  57. 0057cases hp
  58. 0058cases hp_witness
  59. 0059cases hp_witness_witness
  60. 0060cases hp_witness_witness_witness
  61. 0061cases hp_witness_witness_witness_right
  62. 0062cases hp_witness_witness_witness_right_right
  63. 0063exists x1
  64. 0064exists x2
  65. 0065exists x3
  66. 0066exists x
  67. 0067split
  68. 0068exact hl_right_witness
  69. 0069split
  70. 0070exact hp_witness_witness_witness_left
  71. 0071split
  72. 0072exact hp_witness_witness_witness_right_left
  73. 0073split
  74. 0074exact hp_witness_witness_witness_right_right_left
  75. 0075exact hp_witness_witness_witness_right_right_right