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.
Definition in prerequisite notation
∃ cf_gcd_explorer. Beta(u,v,0,(cf_gcd_explorer + ((0 + 0) · S (0 + 0) + (0 + 0))) · S (cf_gcd_explorer + ((0 + 0) · S (0 + 0) + (0 + 0))) + ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0)))) ∧ (Beta(u,v,ell,(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)))) ∧ (∀ x. Lt(x,ell) → ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. Beta(u,v,x,(y + ((z + n) · S (z + n) + (n + n))) · S (y + ((z + n) · S (z + n) + (n + n))) + ((z + n) · S (z + n) + (n + n) + ((z + n) · S (z + n) + (n + n)))) ∧ (Beta(u,v,S x,(m + ((k + i) · S (k + i) + (i + i))) · S (m + ((k + i) · S (k + i) + (i + i))) + ((k + i) · S (k + i) + (i + i) + ((k + i) · S (k + i) + (i + i)))) ∧ (k = y ∧ (m = k · j + z ∧ (Lt(z,k) ∧ ListCell(i,j,n)))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cf_gcd_explorer. ((((exists ff_h_cf_explorer_initial_state. ff_h_cf_explorer_initial_state + S (((cf_gcd_explorer) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_explorer) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * v)) /\ exists ff_q_cf_explorer_initial_state. u = ff_q_cf_explorer_initial_state * S ((S (0)) * v) + (((cf_gcd_explorer) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_explorer) + (((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_explorer_terminal_state. ff_h_cf_explorer_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 (ell)) * v)) /\ exists ff_q_cf_explorer_terminal_state. u = ff_q_cf_explorer_terminal_state * S ((S (ell)) * v) + (((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_explorer. (exists ff_lt_cf_explorer_index. ff_lt_cf_explorer_index + S cf_index_explorer = ell) -> exists cf_old_a_explorer cf_old_b_explorer cf_tail_explorer cf_new_a_explorer cf_new_b_explorer cf_head_explorer cf_quotient_explorer. ((((exists ff_h_cf_explorer_previous_state. ff_h_cf_explorer_previous_state + S (((cf_old_a_explorer) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer)))) * S ((cf_old_a_explorer) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer)))) + ((((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer))) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer))))) = S ((S (cf_index_explorer)) * v)) /\ exists ff_q_cf_explorer_previous_state. u = ff_q_cf_explorer_previous_state * S ((S (cf_index_explorer)) * v) + (((cf_old_a_explorer) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer)))) * S ((cf_old_a_explorer) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer)))) + ((((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer))) + (((cf_old_b_explorer) + (cf_tail_explorer)) * S ((cf_old_b_explorer) + (cf_tail_explorer)) + ((cf_tail_explorer) + (cf_tail_explorer))))))) /\ ((((exists ff_h_cf_explorer_following_state. ff_h_cf_explorer_following_state + S (((cf_new_a_explorer) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer)))) * S ((cf_new_a_explorer) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer)))) + ((((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer))) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer))))) = S ((S (S cf_index_explorer)) * v)) /\ exists ff_q_cf_explorer_following_state. u = ff_q_cf_explorer_following_state * S ((S (S cf_index_explorer)) * v) + (((cf_new_a_explorer) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer)))) * S ((cf_new_a_explorer) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer)))) + ((((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer))) + (((cf_new_b_explorer) + (cf_head_explorer)) * S ((cf_new_b_explorer) + (cf_head_explorer)) + ((cf_head_explorer) + (cf_head_explorer))))))) /\ (cf_new_b_explorer = cf_old_a_explorer /\ (cf_new_a_explorer = cf_new_b_explorer * cf_quotient_explorer + cf_old_b_explorer /\ ((exists ff_lt_cf_explorer_remainder. ff_lt_cf_explorer_remainder + S cf_old_b_explorer = cf_new_b_explorer) /\ (cf_head_explorer = S ((cf_quotient_explorer + cf_tail_explorer) * S (cf_quotient_explorer + cf_tail_explorer) + (cf_tail_explorer + cf_tail_explorer))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
BA0029 · cf_convergent_old_history_zero_eliminationBA002A · cf_convergent_old_history_successor_eliminationBA002C · cf_convergent_old_history_length_transportBA002D · cf_convergent_old_history_nonempty_headBA003D · cf_convergent_euclidean_matrix_step_alignmentBA003E · cf_convergent_actual_prefix_error_invariantBA003F · cf_convergent_every_valid_matrix_prefix_existsBA0040 · cf_convergent_actual_prefix_index_boundBA0041 · continued_fraction_convergent_exists_at_history_indexBA0042 · continued_fraction_convergent_index_is_validBA0046 · continued_fraction_initial_zero_over_oneBA0047 · cf_convergent_full_matrix_is_exactBA0048 · continued_fraction_terminal_convergent_is_exactBA0049 · continued_fraction_exact_terminal_convergent_existsBA004D · continued_fraction_convergent_exists_unique_at_history_index