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. (exists cf_a_pred_zero_initial_fraction cf_b_pred_zero_initial_fraction cf_code_zero_initial_fraction cf_scale_zero_initial_fraction cf_length_pred_zero_initial_fraction. (a = S cf_a_pred_zero_initial_fraction /\ (b = S cf_b_pred_zero_initial_fraction /\ (exists cf_gcd_zero_initial_fraction_trace. ((((exists ff_h_cf_zero_initial_fraction_trace_initial_state. ff_h_cf_zero_initial_fraction_trace_initial_state + S (((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_initial_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_initial_state * S ((S (0)) * cf_scale_zero_initial_fraction) + (((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_fraction_trace) + (((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_zero_initial_fraction_trace_terminal_state. ff_h_cf_zero_initial_fraction_trace_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 cf_length_pred_zero_initial_fraction)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_terminal_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_terminal_state * S ((S (S cf_length_pred_zero_initial_fraction)) * cf_scale_zero_initial_fraction) + (((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_zero_initial_fraction_trace. (exists ff_lt_cf_zero_initial_fraction_trace_index. ff_lt_cf_zero_initial_fraction_trace_index + S cf_index_zero_initial_fraction_trace = S cf_length_pred_zero_initial_fraction) -> exists cf_old_a_zero_initial_fraction_trace cf_old_b_zero_initial_fraction_trace cf_tail_zero_initial_fraction_trace cf_new_a_zero_initial_fraction_trace cf_new_b_zero_initial_fraction_trace cf_head_zero_initial_fraction_trace cf_quotient_zero_initial_fraction_trace. ((((exists ff_h_cf_zero_initial_fraction_trace_previous_state. ff_h_cf_zero_initial_fraction_trace_previous_state + S (((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) * S ((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) + ((((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))))) = S ((S (cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_previous_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_previous_state * S ((S (cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction) + (((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) * S ((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) + ((((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))))))) /\ ((((exists ff_h_cf_zero_initial_fraction_trace_following_state. ff_h_cf_zero_initial_fraction_trace_following_state + S (((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) * S ((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) + ((((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))))) = S ((S (S cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_following_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_following_state * S ((S (S cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction) + (((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) * S ((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) + ((((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))))))) /\ (cf_new_b_zero_initial_fraction_trace = cf_old_a_zero_initial_fraction_trace /\ (cf_new_a_zero_initial_fraction_trace = cf_new_b_zero_initial_fraction_trace * cf_quotient_zero_initial_fraction_trace + cf_old_b_zero_initial_fraction_trace /\ ((exists ff_lt_cf_zero_initial_fraction_trace_remainder. ff_lt_cf_zero_initial_fraction_trace_remainder + S cf_old_b_zero_initial_fraction_trace = cf_new_b_zero_initial_fraction_trace) /\ (cf_head_zero_initial_fraction_trace = S ((cf_quotient_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace) * S (cf_quotient_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace)))))))))))))) -> (exists cfba_gap_zero_initial_input. cfba_gap_zero_initial_input + S (a) = (b)) -> (exists cfc_previous_numerator_zero_initial_actual cfc_previous_denominator_zero_initial_actual cfc_code_zero_initial_actual cfc_scale_zero_initial_actual. ((~(1 = 0)) /\ (exists cfc_tail_zero_initial_actualcomputation. ((exists cfc_state_zero_initial_actualcomputationinitial. ((exists cfc_left_zero_initial_actualcomputationinitialcode cfc_right_zero_initial_actualcomputationinitialcode cfc_matrix_zero_initial_actualcomputationinitialcode. ((cfc_left_zero_initial_actualcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_zero_initial_actualcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_zero_initial_actualcomputationinitialcode = ((cfc_left_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode)) * S ((cfc_left_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode)) + ((cfc_right_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode))) /\ ((cfc_state_zero_initial_actualcomputationinitial) = ((cfc_tail_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationinitialcode)) * S ((cfc_tail_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationinitialcode)) + ((cfc_matrix_zero_initial_actualcomputationinitialcode) + (cfc_matrix_zero_initial_actualcomputationinitialcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationinitialentry. ff_h_zero_initial_actualcomputationinitialentry + S (cfc_state_zero_initial_actualcomputationinitial) = S ((S (0)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationinitialentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationinitialentry * S ((S (0)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationinitial))))) /\ ((exists cfc_state_zero_initial_actualcomputationterminal. ((exists cfc_left_zero_initial_actualcomputationterminalcode cfc_right_zero_initial_actualcomputationterminalcode cfc_matrix_zero_initial_actualcomputationterminalcode. ((cfc_left_zero_initial_actualcomputationterminalcode = ((0) + (cfc_previous_numerator_zero_initial_actual)) * S ((0) + (cfc_previous_numerator_zero_initial_actual)) + ((cfc_previous_numerator_zero_initial_actual) + (cfc_previous_numerator_zero_initial_actual))) /\ ((cfc_right_zero_initial_actualcomputationterminalcode = ((1) + (cfc_previous_denominator_zero_initial_actual)) * S ((1) + (cfc_previous_denominator_zero_initial_actual)) + ((cfc_previous_denominator_zero_initial_actual) + (cfc_previous_denominator_zero_initial_actual))) /\ ((cfc_matrix_zero_initial_actualcomputationterminalcode = ((cfc_left_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode)) * S ((cfc_left_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode)) + ((cfc_right_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode))) /\ ((cfc_state_zero_initial_actualcomputationterminal) = ((s) + (cfc_matrix_zero_initial_actualcomputationterminalcode)) * S ((s) + (cfc_matrix_zero_initial_actualcomputationterminalcode)) + ((cfc_matrix_zero_initial_actualcomputationterminalcode) + (cfc_matrix_zero_initial_actualcomputationterminalcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationterminalentry. ff_h_zero_initial_actualcomputationterminalentry + S (cfc_state_zero_initial_actualcomputationterminal) = S ((S (S (0))) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationterminalentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationterminalentry * S ((S (S (0))) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationterminal))))) /\ (forall cfc_index_zero_initial_actualcomputation. (exists cfba_gap_zero_initial_actualcomputationbound. cfba_gap_zero_initial_actualcomputationbound + S (cfc_index_zero_initial_actualcomputation) = (S (0))) -> exists cfc_old_zero_initial_actualcomputation cfc_a_zero_initial_actualcomputation cfc_b_zero_initial_actualcomputation cfc_c_zero_initial_actualcomputation cfc_d_zero_initial_actualcomputation cfc_new_zero_initial_actualcomputation cfc_quotient_zero_initial_actualcomputation. ((exists cfc_state_zero_initial_actualcomputationprevious. ((exists cfc_left_zero_initial_actualcomputationpreviouscode cfc_right_zero_initial_actualcomputationpreviouscode cfc_matrix_zero_initial_actualcomputationpreviouscode. ((cfc_left_zero_initial_actualcomputationpreviouscode = ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) * S ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) + ((cfc_b_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation))) /\ ((cfc_right_zero_initial_actualcomputationpreviouscode = ((cfc_c_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation)) * S ((cfc_c_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation)) + ((cfc_d_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation))) /\ ((cfc_matrix_zero_initial_actualcomputationpreviouscode = ((cfc_left_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode)) * S ((cfc_left_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode)) + ((cfc_right_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode))) /\ ((cfc_state_zero_initial_actualcomputationprevious) = ((cfc_old_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationpreviouscode)) * S ((cfc_old_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationpreviouscode)) + ((cfc_matrix_zero_initial_actualcomputationpreviouscode) + (cfc_matrix_zero_initial_actualcomputationpreviouscode))))))) /\ (((exists ff_h_zero_initial_actualcomputationpreviousentry. ff_h_zero_initial_actualcomputationpreviousentry + S (cfc_state_zero_initial_actualcomputationprevious) = S ((S (cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationpreviousentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationpreviousentry * S ((S (cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationprevious))))) /\ ((exists cfc_state_zero_initial_actualcomputationfollowing. ((exists cfc_left_zero_initial_actualcomputationfollowingcode cfc_right_zero_initial_actualcomputationfollowingcode cfc_matrix_zero_initial_actualcomputationfollowingcode. ((cfc_left_zero_initial_actualcomputationfollowingcode = (((cfc_quotient_zero_initial_actualcomputation * cfc_a_zero_initial_actualcomputation + cfc_c_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation))) * S (((cfc_quotient_zero_initial_actualcomputation * cfc_a_zero_initial_actualcomputation + cfc_c_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation))) + (((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation)))) /\ ((cfc_right_zero_initial_actualcomputationfollowingcode = ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) * S ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) + ((cfc_b_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation))) /\ ((cfc_matrix_zero_initial_actualcomputationfollowingcode = ((cfc_left_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode)) * S ((cfc_left_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode)) + ((cfc_right_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode))) /\ ((cfc_state_zero_initial_actualcomputationfollowing) = ((cfc_new_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationfollowingcode)) * S ((cfc_new_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationfollowingcode)) + ((cfc_matrix_zero_initial_actualcomputationfollowingcode) + (cfc_matrix_zero_initial_actualcomputationfollowingcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationfollowingentry. ff_h_zero_initial_actualcomputationfollowingentry + S (cfc_state_zero_initial_actualcomputationfollowing) = S ((S (S cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationfollowingentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationfollowingentry * S ((S (S cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationfollowing))))) /\ (cfc_new_zero_initial_actualcomputation = S ((cfc_quotient_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation) * S (cfc_quotient_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation) + (cfc_old_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation)))))))))))Constructive proof overview
Generated structural guide
For every positive G071 fraction below one, the genuine initial convergent is 0/1. This checked theorem explicitly corrects the old planning-only numerator-positivity error.
The unchanged tactic script uses 5 declared prerequisites and contains 52 exact native proof lines.
Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
BA002A cf_convergent_old_history_successor_elimination division_remainder_unique Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized BA0045 cf_convergent_numerator_transport BA0044 continued_fraction_first_cell_is_initial_convergentDirect dependents
none
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
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)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
03Establish hpL13–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history successor elimination.
- L13
have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,x2,x3,x4)))Definitions: ListCellContinuedFractionTraceLt - L14
specialize cf_convergent_old_history_successor_elimination (a) - L15
specialize cf_convergent_old_history_successor_elimination (b) - L16
specialize cf_convergent_old_history_successor_elimination (s) - L17
specialize cf_convergent_old_history_successor_elimination (x2) - L18
specialize cf_convergent_old_history_successor_elimination (x3) - L19
specialize cf_convergent_old_history_successor_elimination (x4) - L20
apply cf_convergent_old_history_successor_elimination - L21
exact hcf_witness_witness_witness_witness_witness_right_right
04Separate the logical casesL22–27
05Establish hqL28–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder unique.
- L28
have hq : x5 = 0 /\ x6 = a - L29
specialize division_remainder_unique (b) - L30
specialize division_remainder_unique (a) - L31
specialize division_remainder_unique (x5) - L32
specialize division_remainder_unique (x6) - L33
specialize division_remainder_unique (0) - L34
specialize division_remainder_unique (a) - L35
apply division_remainder_unique - L36
exact hp_witness_witness_witness_left - L37
exact hp_witness_witness_witness_right_left
06Calculate and transport equalitiesL38–38
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L38
simp [zero_add]
07Use earlier factsL39–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L39
exact hlt
08Separate the logical casesL40–40
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L40
cases hq
09Use earlier factsL41–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
specialize cf_convergent_numerator_transport (s) - L42
specialize cf_convergent_numerator_transport (0) - L43
specialize cf_convergent_numerator_transport (x5) - L44
specialize cf_convergent_numerator_transport (0) - L45
specialize cf_convergent_numerator_transport (1) - L46
apply cf_convergent_numerator_transport - L47
exact hq_left - L48
specialize continued_fraction_first_cell_is_initial_convergent (s) - L49
specialize continued_fraction_first_cell_is_initial_convergent (x5) - L50
specialize continued_fraction_first_cell_is_initial_convergent (x7)
Original exact command ledger · 52 lines
- 0001
intro a - 0002
intro b - 0003
intro s - 0004
intro hcf - 0005
intro hlt - 0006
cases hcf - 0007
cases hcf_witness - 0008
cases hcf_witness_witness - 0009
cases hcf_witness_witness_witness - 0010
cases hcf_witness_witness_witness_witness - 0011
cases hcf_witness_witness_witness_witness_witness - 0012
cases hcf_witness_witness_witness_witness_witness_right - 0013
have hp : exists q r t. ((a = b * q + r) /\ ((exists cfba_gap_zero_initial_remainder. cfba_gap_zero_initial_remainder + S (r) = (b)) /\ ((s = S ((q + t) * S (q + t) + (t + t))) /\ (exists cf_gcd_zero_initial_history. ((((exists ff_h_cf_zero_initial_history_initial_state. ff_h_cf_zero_initial_history_initial_state + S (((cf_gcd_zero_initial_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * x3)) /\ exists ff_q_cf_zero_initial_history_initial_state. x2 = ff_q_cf_zero_initial_history_initial_state * S ((S (0)) * x3) + (((cf_gcd_zero_initial_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_history) + (((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_zero_initial_history_terminal_state. ff_h_cf_zero_initial_history_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 (x4)) * x3)) /\ exists ff_q_cf_zero_initial_history_terminal_state. x2 = ff_q_cf_zero_initial_history_terminal_state * S ((S (x4)) * x3) + (((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_zero_initial_history. (exists ff_lt_cf_zero_initial_history_index. ff_lt_cf_zero_initial_history_index + S cf_index_zero_initial_history = x4) -> exists cf_old_a_zero_initial_history cf_old_b_zero_initial_history cf_tail_zero_initial_history cf_new_a_zero_initial_history cf_new_b_zero_initial_history cf_head_zero_initial_history cf_quotient_zero_initial_history. ((((exists ff_h_cf_zero_initial_history_previous_state. ff_h_cf_zero_initial_history_previous_state + S (((cf_old_a_zero_initial_history) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history)))) * S ((cf_old_a_zero_initial_history) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history)))) + ((((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history))) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history))))) = S ((S (cf_index_zero_initial_history)) * x3)) /\ exists ff_q_cf_zero_initial_history_previous_state. x2 = ff_q_cf_zero_initial_history_previous_state * S ((S (cf_index_zero_initial_history)) * x3) + (((cf_old_a_zero_initial_history) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history)))) * S ((cf_old_a_zero_initial_history) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history)))) + ((((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history))) + (((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) * S ((cf_old_b_zero_initial_history) + (cf_tail_zero_initial_history)) + ((cf_tail_zero_initial_history) + (cf_tail_zero_initial_history))))))) /\ ((((exists ff_h_cf_zero_initial_history_following_state. ff_h_cf_zero_initial_history_following_state + S (((cf_new_a_zero_initial_history) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history)))) * S ((cf_new_a_zero_initial_history) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history)))) + ((((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history))) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history))))) = S ((S (S cf_index_zero_initial_history)) * x3)) /\ exists ff_q_cf_zero_initial_history_following_state. x2 = ff_q_cf_zero_initial_history_following_state * S ((S (S cf_index_zero_initial_history)) * x3) + (((cf_new_a_zero_initial_history) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history)))) * S ((cf_new_a_zero_initial_history) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history)))) + ((((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history))) + (((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) * S ((cf_new_b_zero_initial_history) + (cf_head_zero_initial_history)) + ((cf_head_zero_initial_history) + (cf_head_zero_initial_history))))))) /\ (cf_new_b_zero_initial_history = cf_old_a_zero_initial_history /\ (cf_new_a_zero_initial_history = cf_new_b_zero_initial_history * cf_quotient_zero_initial_history + cf_old_b_zero_initial_history /\ ((exists ff_lt_cf_zero_initial_history_remainder. ff_lt_cf_zero_initial_history_remainder + S cf_old_b_zero_initial_history = cf_new_b_zero_initial_history) /\ (cf_head_zero_initial_history = S ((cf_quotient_zero_initial_history + cf_tail_zero_initial_history) * S (cf_quotient_zero_initial_history + cf_tail_zero_initial_history) + (cf_tail_zero_initial_history + cf_tail_zero_initial_history)))))))))))))) - 0014
specialize cf_convergent_old_history_successor_elimination (a) - 0015
specialize cf_convergent_old_history_successor_elimination (b) - 0016
specialize cf_convergent_old_history_successor_elimination (s) - 0017
specialize cf_convergent_old_history_successor_elimination (x2) - 0018
specialize cf_convergent_old_history_successor_elimination (x3) - 0019
specialize cf_convergent_old_history_successor_elimination (x4) - 0020
apply cf_convergent_old_history_successor_elimination - 0021
exact hcf_witness_witness_witness_witness_witness_right_right - 0022
cases hp - 0023
cases hp_witness - 0024
cases hp_witness_witness - 0025
cases hp_witness_witness_witness - 0026
cases hp_witness_witness_witness_right - 0027
cases hp_witness_witness_witness_right_right - 0028
have hq : x5 = 0 /\ x6 = a - 0029
specialize division_remainder_unique (b) - 0030
specialize division_remainder_unique (a) - 0031
specialize division_remainder_unique (x5) - 0032
specialize division_remainder_unique (x6) - 0033
specialize division_remainder_unique (0) - 0034
specialize division_remainder_unique (a) - 0035
apply division_remainder_unique - 0036
exact hp_witness_witness_witness_left - 0037
exact hp_witness_witness_witness_right_left - 0038
simp [zero_add] - 0039
exact hlt - 0040
cases hq - 0041
specialize cf_convergent_numerator_transport (s) - 0042
specialize cf_convergent_numerator_transport (0) - 0043
specialize cf_convergent_numerator_transport (x5) - 0044
specialize cf_convergent_numerator_transport (0) - 0045
specialize cf_convergent_numerator_transport (1) - 0046
apply cf_convergent_numerator_transport - 0047
exact hq_left - 0048
specialize continued_fraction_first_cell_is_initial_convergent (s) - 0049
specialize continued_fraction_first_cell_is_initial_convergent (x5) - 0050
specialize continued_fraction_first_cell_is_initial_convergent (x7) - 0051
apply continued_fraction_first_cell_is_initial_convergent - 0052
exact hp_witness_witness_witness_right_right_left