konig = dtext + bddefs + consts subseq_rel :: "'a relation => (nat => 'a) => (nat => 'a)" fiseq :: "'f psc set => (nat => 'f dertree) => nat => (nat * (nat => 'f dertree))" lfiseq :: "'f psc set => (nat => 'f dertree) => nat => ('f list * (nat * (nat => 'f dertree)))" next_fiseq :: "'f psc set => (nat => 'f dertree) => (nat * (nat => 'f dertree))" primrec Z "subseq_rel r f 0 = f 0" S "subseq_rel r f (Suc m) = f (LEAST n. (subseq_rel r f m, f n) : r)" defs nf_def "next_fiseq rls f == (SOME (i, g). i < length ((nextUp o f o Suc) 0) & (ALL k. (g k, g (Suc k)) : ext_ppt rls & (EX j. g k = (nextUp o f o Suc) j ! i)))" primrec Z "fiseq rls f 0 = (0, f)" (* first component meaningless *) S "fiseq rls f (Suc n) = next_fiseq rls (snd (fiseq rls f n))" (* records items taken off *) primrec Z "lfiseq rls f 0 = ([], (0, f))" (* zero meaningless *) S "lfiseq rls f (Suc n) = (conclDT (snd (snd (lfiseq rls f n)) 0) # fst (lfiseq rls f n), next_fiseq rls (snd (snd (lfiseq rls f n))))" consts lctr_concl_unique :: "('f multiset, 'f) sequent dertree => bool" lctr_irred :: "('f multiset, 'f) sequent dertree => bool" primrec lctr_cu_Der "lctr_concl_unique (Der GC dts) = (case GC of G |- C => (~ (EX F. set_of F <= set_of G & G <= F & (F |- C) :# dt_contentss dts)))" lctr_cu_Unf "lctr_concl_unique (Unf f) = True" defs lctr_irred_def "lctr_irred == allDT lctr_concl_unique" end