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
(∀ x. Lt(x,p) → (BetaAt(ub,uc,x,1) → BetaAt(b,c,x,1) ∨ (∃ y. ModularSetMember(d,e,p,y) ∧ ModEq(p,y + t,x))) ∧ (BetaAt(b,c,x,1) ∨ (∃ y. ModularSetMember(d,e,p,y) ∧ ModEq(p,y + t,x)) → BetaAt(ub,uc,x,1))) ∧ (∀ x. Lt(x,p) → (BetaAt(vb,vc,x,1) → BetaAt(d,e,x,1) ∧ (∃ y. ModularSetMember(b,c,p,y) ∧ ModEq(p,x + t,y))) ∧ (BetaAt(d,e,x,1) ∧ (∃ y. ModularSetMember(b,c,p,y) ∧ ModEq(p,x + t,y)) → BetaAt(vb,vc,x,1)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((forall cd_output_secondwave_upper. (exists fms_gap_cd_secondwave_upper_bound. fms_gap_cd_secondwave_upper_bound + S (cd_output_secondwave_upper) = (p)) -> ((((((exists fs_h_cd_secondwave_upper_result. fs_h_cd_secondwave_upper_result + S (1) = S ((S (cd_output_secondwave_upper)) * uc)) /\ exists fs_q_cd_secondwave_upper_result. ub = fs_q_cd_secondwave_upper_result * S ((S (cd_output_secondwave_upper)) * uc) + (1))) -> ((((exists fs_h_cd_secondwave_upper_old. fs_h_cd_secondwave_upper_old + S (1) = S ((S (cd_output_secondwave_upper)) * c)) /\ exists fs_q_cd_secondwave_upper_old. b = fs_q_cd_secondwave_upper_old * S ((S (cd_output_secondwave_upper)) * c) + (1))) \/ (exists cd_source_secondwave_upper. (((exists fms_gap_cd_secondwave_upper_member. fms_gap_cd_secondwave_upper_member + S (cd_source_secondwave_upper) = (p)) /\ (((exists fs_h_fms_cd_secondwave_upper_member. fs_h_fms_cd_secondwave_upper_member + S (1) = S ((S (cd_source_secondwave_upper)) * e)) /\ exists fs_q_fms_cd_secondwave_upper_member. d = fs_q_fms_cd_secondwave_upper_member * S ((S (cd_source_secondwave_upper)) * e) + (1))))) /\ (exists fms_u_cd_secondwave_upper_mod fms_v_cd_secondwave_upper_mod. (cd_source_secondwave_upper+t) + (p) * fms_u_cd_secondwave_upper_mod = (cd_output_secondwave_upper) + (p) * fms_v_cd_secondwave_upper_mod)))) /\ (((((exists fs_h_cd_secondwave_upper_old. fs_h_cd_secondwave_upper_old + S (1) = S ((S (cd_output_secondwave_upper)) * c)) /\ exists fs_q_cd_secondwave_upper_old. b = fs_q_cd_secondwave_upper_old * S ((S (cd_output_secondwave_upper)) * c) + (1))) \/ (exists cd_source_secondwave_upper. (((exists fms_gap_cd_secondwave_upper_member. fms_gap_cd_secondwave_upper_member + S (cd_source_secondwave_upper) = (p)) /\ (((exists fs_h_fms_cd_secondwave_upper_member. fs_h_fms_cd_secondwave_upper_member + S (1) = S ((S (cd_source_secondwave_upper)) * e)) /\ exists fs_q_fms_cd_secondwave_upper_member. d = fs_q_fms_cd_secondwave_upper_member * S ((S (cd_source_secondwave_upper)) * e) + (1))))) /\ (exists fms_u_cd_secondwave_upper_mod fms_v_cd_secondwave_upper_mod. (cd_source_secondwave_upper+t) + (p) * fms_u_cd_secondwave_upper_mod = (cd_output_secondwave_upper) + (p) * fms_v_cd_secondwave_upper_mod))) -> (((exists fs_h_cd_secondwave_upper_result. fs_h_cd_secondwave_upper_result + S (1) = S ((S (cd_output_secondwave_upper)) * uc)) /\ exists fs_q_cd_secondwave_upper_result. ub = fs_q_cd_secondwave_upper_result * S ((S (cd_output_secondwave_upper)) * uc) + (1))))))) /\ (forall cd_output_secondwave_lower. (exists fms_gap_cd_secondwave_lower_bound. fms_gap_cd_secondwave_lower_bound + S (cd_output_secondwave_lower) = (p)) -> ((((((exists fs_h_cd_secondwave_lower_result. fs_h_cd_secondwave_lower_result + S (1) = S ((S (cd_output_secondwave_lower)) * vc)) /\ exists fs_q_cd_secondwave_lower_result. vb = fs_q_cd_secondwave_lower_result * S ((S (cd_output_secondwave_lower)) * vc) + (1))) -> ((((exists fs_h_cd_secondwave_lower_old. fs_h_cd_secondwave_lower_old + S (1) = S ((S (cd_output_secondwave_lower)) * e)) /\ exists fs_q_cd_secondwave_lower_old. d = fs_q_cd_secondwave_lower_old * S ((S (cd_output_secondwave_lower)) * e) + (1))) /\ (exists cd_source_secondwave_lower. (((exists fms_gap_cd_secondwave_lower_member. fms_gap_cd_secondwave_lower_member + S (cd_source_secondwave_lower) = (p)) /\ (((exists fs_h_fms_cd_secondwave_lower_member. fs_h_fms_cd_secondwave_lower_member + S (1) = S ((S (cd_source_secondwave_lower)) * c)) /\ exists fs_q_fms_cd_secondwave_lower_member. b = fs_q_fms_cd_secondwave_lower_member * S ((S (cd_source_secondwave_lower)) * c) + (1))))) /\ (exists fms_u_cd_secondwave_lower_mod fms_v_cd_secondwave_lower_mod. (cd_output_secondwave_lower+t) + (p) * fms_u_cd_secondwave_lower_mod = (cd_source_secondwave_lower) + (p) * fms_v_cd_secondwave_lower_mod)))) /\ (((((exists fs_h_cd_secondwave_lower_old. fs_h_cd_secondwave_lower_old + S (1) = S ((S (cd_output_secondwave_lower)) * e)) /\ exists fs_q_cd_secondwave_lower_old. d = fs_q_cd_secondwave_lower_old * S ((S (cd_output_secondwave_lower)) * e) + (1))) /\ (exists cd_source_secondwave_lower. (((exists fms_gap_cd_secondwave_lower_member. fms_gap_cd_secondwave_lower_member + S (cd_source_secondwave_lower) = (p)) /\ (((exists fs_h_fms_cd_secondwave_lower_member. fs_h_fms_cd_secondwave_lower_member + S (1) = S ((S (cd_source_secondwave_lower)) * c)) /\ exists fs_q_fms_cd_secondwave_lower_member. b = fs_q_fms_cd_secondwave_lower_member * S ((S (cd_source_secondwave_lower)) * c) + (1))))) /\ (exists fms_u_cd_secondwave_lower_mod fms_v_cd_secondwave_lower_mod. (cd_output_secondwave_lower+t) + (p) * fms_u_cd_secondwave_lower_mod = (cd_source_secondwave_lower) + (p) * fms_v_cd_secondwave_lower_mod))) -> (((exists fs_h_cd_secondwave_lower_result. fs_h_cd_secondwave_lower_result + S (1) = S ((S (cd_output_secondwave_lower)) * vc)) /\ exists fs_q_cd_secondwave_lower_result. vb = fs_q_cd_secondwave_lower_result * S ((S (cd_output_secondwave_lower)) * vc) + (1))))))))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
none