(* tables of connectives appearing in rules *) RA_FL = RA_Rls + GCut + consts sucFLs, antFLs :: "structr rule set => (string * nat * structr rule) set" sucFLs_1, antFLs_1 :: "structr rule => (string * nat * structr rule) set" inductive "sucFLs rules" intrs sflI "[| inst : rules ; ($X |- FC conn fl) = conclRule inst |] ==> (conn, length fl, inst) : sucFLs rules" inductive "antFLs rules" intrs aflI "[| inst : rules ; (FC conn fl |- $X) = conclRule inst |] ==> (conn, length fl, inst) : antFLs rules" defs antFLs_1_def "antFLs_1 r == antFLs {r}" sucFLs_1_def "sucFLs_1 r == sucFLs {r}" end