CRTPrefixLCM(b,c,l,M)

Hygienic expanded first-order definition

((forall gcrt_common_index_research_own gcrt_common_modulus_research_own. (exists ff_lt_gcrt_research_own_bound. ff_lt_gcrt_research_own_bound + S gcrt_common_index_research_own = l) -> (((exists ff_h_gcrt_research_own_entry. ff_h_gcrt_research_own_entry + S (gcrt_common_modulus_research_own) = S ((S (gcrt_common_index_research_own)) * c)) /\ exists ff_q_gcrt_research_own_entry. b = ff_q_gcrt_research_own_entry * S ((S (gcrt_common_index_research_own)) * c) + (gcrt_common_modulus_research_own))) -> exists gcrt_common_quotient_research_own. M = gcrt_common_modulus_research_own * gcrt_common_quotient_research_own) /\ forall gcrt_lcm_common_research. (forall gcrt_common_index_research_other gcrt_common_modulus_research_other. (exists ff_lt_gcrt_research_other_bound. ff_lt_gcrt_research_other_bound + S gcrt_common_index_research_other = l) -> (((exists ff_h_gcrt_research_other_entry. ff_h_gcrt_research_other_entry + S (gcrt_common_modulus_research_other) = S ((S (gcrt_common_index_research_other)) * c)) /\ exists ff_q_gcrt_research_other_entry. b = ff_q_gcrt_research_other_entry * S ((S (gcrt_common_index_research_other)) * c) + (gcrt_common_modulus_research_other))) -> exists gcrt_common_quotient_research_other. gcrt_lcm_common_research = gcrt_common_modulus_research_other * gcrt_common_quotient_research_other) -> exists gcrt_lcm_quotient_research. gcrt_lcm_common_research = M * gcrt_lcm_quotient_research)

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