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.
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.