begin
:: deftheorem Def1 defines with_common_domain MARGREL1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem defines = MARGREL1:def 2 :
theorem Th9:
:: deftheorem MARGREL1:def 3 :
canceled;
:: deftheorem defines the_arity_of MARGREL1:def 4 :
:: deftheorem defines relation_length MARGREL1:def 5 :
:: deftheorem defines relation MARGREL1:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem Th21:
:: deftheorem defines relation MARGREL1:def 7 :
:: deftheorem Def8 defines relations_on MARGREL1:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
:: deftheorem Def9 defines = MARGREL1:def 9 :
:: deftheorem Def10 defines empty_rel MARGREL1:def 10 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines the_arity_of MARGREL1:def 11 :
:: deftheorem defines BOOLEAN MARGREL1:def 12 :
:: deftheorem Def13 defines boolean MARGREL1:def 13 :
:: deftheorem defines 'not' MARGREL1:def 14 :
:: deftheorem defines '&' MARGREL1:def 15 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
:: deftheorem Def16 defines ALL MARGREL1:def 16 :
theorem
begin
:: deftheorem Def17 defines boolean-valued MARGREL1:def 17 :
:: deftheorem Def18 defines 'not' MARGREL1:def 18 :
:: deftheorem Def19 defines '&' MARGREL1:def 19 :
:: deftheorem defines 'not' MARGREL1:def 20 :
:: deftheorem defines '&' MARGREL1:def 21 :