theory AC_Gen_DC imports AC_DI_DC AC_Subst_defs Int_AC (* AC_Theory *) begin consts (* satisfiability of list-type deducibility constraint system *) satldc :: "('n => 'n msg) => 'n ldc => bool" satldcs :: "('n => 'n msg) => 'n ldc list => bool" primrec "satldc f (R, con) = (if R then (subst_con f con : acder_rt) else subst_con f con : acder)" defs satldcs_def : "satldcs f Cs == Ball (set Cs) (satldc f)" consts xdcs_red :: "'n mlsred => ('n => 'n msg) => 'n ldc list => bool" defs xdcs_red_def : "xdcs_red red theta Cs == (EX Cs' sig gamma. (sig, Cs', Cs) : red & satldcs gamma Cs' & theta = comp_subst gamma sig)" end