diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy @@ -1,61 +1,45 @@ section \Algorithms on Nondeterministic Generalized Büchi Automata\ theory NGBA_Algorithms imports - NBA_Algorithms NGBA_Implement NBA_Combine + NBA_Algorithms + Degeneralization_Refine begin subsection \Implementations\ context begin interpretation autoref_syn by this - (* TODO: move *) - lemma degen_param[param, autoref_rules]: "(degen, degen) \ \S \ bool_rel\ list_rel \ S \\<^sub>r nat_rel \ bool_rel" - proof (intro fun_relI) - fix cs ds ak bl - assume "(cs, ds) \ \S \ bool_rel\ list_rel" "(ak, bl) \ S \\<^sub>r nat_rel" - then show "(degen cs ak, degen ds bl) \ bool_rel" - unfolding degen_def list_rel_def fun_rel_def list_all2_conv_all_nth - by (cases "snd ak < length cs") (auto 0 3) - qed - - (* TODO: move *) - lemmas [param] = null_transfer[unfolded pred_bool_Id, to_set] - - (* TODO: move *) - lemma count_param[param, autoref_rules]: "(Degeneralization.count, Degeneralization.count) \ - \A \ bool_rel\ list_rel \ A \ nat_rel \ nat_rel" - unfolding count_def null_def[symmetric] by parametricity - - (* TODO: why do we need this? *) lemma degeneralize_alt_def: "degeneralize A = nba (ngba.alphabet A) ((\ p. (p, 0)) ` ngba.initial A) (\ a (p, k). (\ q. (q, Degeneralization.count (ngba.accepting A) p k)) ` ngba.transition A a p) (degen (ngba.accepting A))" unfolding degeneralization.degeneralize_def by auto schematic_goal ngba_degeneralize: "(?f :: ?'a, degeneralize) \ ?R" - unfolding degeneralize_alt_def by autoref + unfolding degeneralize_alt_def + using degen_param[autoref_rules] count_param[autoref_rules] + by autoref concrete_definition ngba_degeneralize uses ngba_degeneralize lemmas ngba_degeneralize_refine[autoref_rules] = ngba_degeneralize.refine schematic_goal nba_intersect': assumes [autoref_rules]: "(seq, HOL.eq) \ L \ L \ bool_rel" shows "(?f, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" unfolding intersection.product_def by autoref concrete_definition nba_intersect' uses nba_intersect' lemma nba_intersect'_refine[autoref_rules]: assumes "GEN_OP seq HOL.eq (L \ L \ bool_rel)" shows "(nba_intersect' seq, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" using nba_intersect'.refine assms unfolding autoref_tag_defs by this end end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Basic/Degeneralization_Refine.thy b/thys/Transition_Systems_and_Automata/Basic/Degeneralization_Refine.thy new file mode 100644 --- /dev/null +++ b/thys/Transition_Systems_and_Automata/Basic/Degeneralization_Refine.thy @@ -0,0 +1,18 @@ +theory Degeneralization_Refine +imports Degeneralization Refine +begin + + lemma degen_param[param]: "(degen, degen) \ \S \ bool_rel\ list_rel \ S \\<^sub>r nat_rel \ bool_rel" + proof (intro fun_relI) + fix cs ds ak bl + assume "(cs, ds) \ \S \ bool_rel\ list_rel" "(ak, bl) \ S \\<^sub>r nat_rel" + then show "(degen cs ak, degen ds bl) \ bool_rel" + unfolding degen_def list_rel_def fun_rel_def list_all2_conv_all_nth + by (cases "snd ak < length cs") (auto 0 3) + qed + + lemma count_param[param]: "(Degeneralization.count, Degeneralization.count) \ + \A \ bool_rel\ list_rel \ A \ nat_rel \ nat_rel" + unfolding count_def null_def[symmetric] by parametricity + +end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Basic/Refine.thy b/thys/Transition_Systems_and_Automata/Basic/Refine.thy --- a/thys/Transition_Systems_and_Automata/Basic/Refine.thy +++ b/thys/Transition_Systems_and_Automata/Basic/Refine.thy @@ -1,368 +1,370 @@ section \Relations and Refinement\ theory Refine imports "Automatic_Refinement.Automatic_Refinement" (* TODO Peter: list_set_rel is defined in Refine_Monadic.Refine_Foreach, but it should probably be somewhere in Automatic_Refinement as it has nothing to do with the nondeterminism monad *) "Refine_Monadic.Refine_Foreach" "Sequence_LTL" "Maps" begin (* TODO Peter: - there is some infrastructure for converting between predicates and sets using the constants rel2p and p2rel - however, HOL already has the pred_set_conv attributes - with some additional setup connecting the refinement framework relators to their lifting/transfer counterparts, the attribute to_set can be used to instantly convert lifting/transfer rules to set-based relation format - examples can be found throughout this theory (look for the to_set attribute) *) subsection \Predicate to Set Conversion Setup\ (* TODO Peter: it would be nice if there were corresponding constants for all the relation predicates in Transfer.thy (left_total, left_unique, right_total, right_unique, bi_total, bi_unique *) lemma right_unique_pred_set_conv[pred_set_conv]: "right_unique = single_valuedp" unfolding right_unique_def single_valuedp_def by auto lemma bi_unique_pred_set_conv[pred_set_conv]: "bi_unique (\ x y. (x, y) \ R) \ bijective R" unfolding bi_unique_def bijective_def by blast text \useful for unfolding equality constants in theorems about predicates\ lemma pred_Id: "HOL.eq = (\ x y. (x, y) \ Id)" by simp lemma pred_bool_Id: "HOL.eq = (\ x y. (x, y) \ (Id :: bool rel))" by simp lemma pred_nat_Id: "HOL.eq = (\ x y. (x, y) \ (Id :: nat rel))" by simp lemma pred_set_Id: "HOL.eq = (\ x y. (x, y) \ (Id :: 'a set rel))" by simp lemma pred_list_Id: "HOL.eq = (\ x y. (x, y) \ (Id :: 'a list rel))" by simp lemma pred_stream_Id: "HOL.eq = (\ x y. (x, y) \ (Id :: 'a stream rel))" by simp lemma eq_onp_Id_on_eq[pred_set_conv]: "eq_onp (\ a. a \ A) = (\ x y. (x, y) \ Id_on A)" unfolding eq_onp_def by auto lemma rel_fun_fun_rel_eq[pred_set_conv]: "rel_fun (\ x y. (x, y) \ A) (\ x y. (x, y) \ B) = (\ f g. (f, g) \ A \ B)" by (force simp: rel_fun_def fun_rel_def) lemma rel_prod_prod_rel_eq[pred_set_conv]: "rel_prod (\ x y. (x, y) \ A) (\ x y. (x, y) \ B) = (\ f g. (f, g) \ A \\<^sub>r B)" by (force simp: prod_rel_def elim: rel_prod.cases) lemma rel_sum_sum_rel_eq[pred_set_conv]: "rel_sum (\ x y. (x, y) \ A) (\ x y. (x, y) \ B) = (\ f g. (f, g) \ \A, B\ sum_rel)" by (force simp: sum_rel_def elim: rel_sum.cases) lemma rel_set_set_rel_eq[pred_set_conv]: "rel_set (\ x y. (x, y) \ A) = (\ f g. (f, g) \ \A\ set_rel)" unfolding rel_set_def set_rel_def by simp lemma rel_option_option_rel_eq[pred_set_conv]: "rel_option (\ x y. (x, y) \ A) = (\ f g. (f, g) \ \A\ option_rel)" by (force simp: option_rel_def elim: option.rel_cases) (* TODO Peter: pred_set_conv examples *) thm image_transfer image_transfer[to_set] thm fun_upd_transfer fun_upd_transfer[to_set] subsection \Relation Composition\ lemma relcomp_trans_1[trans]: assumes "(f, g) \ A\<^sub>1" assumes "(g, h) \ A\<^sub>2" shows "(f, h) \ A\<^sub>1 O A\<^sub>2" using relcompI assms by this lemma relcomp_trans_2[trans]: assumes "(f, g) \ A\<^sub>1 \ B\<^sub>1" assumes "(g, h) \ A\<^sub>2 \ B\<^sub>2" shows "(f, h) \ A\<^sub>1 O A\<^sub>2 \ B\<^sub>1 O B\<^sub>2" proof - note assms(1) also note assms(2) also note fun_rel_comp_dist finally show ?thesis by this qed lemma relcomp_trans_3[trans]: assumes "(f, g) \ A\<^sub>1 \ B\<^sub>1 \ C\<^sub>1" assumes "(g, h) \ A\<^sub>2 \ B\<^sub>2 \ C\<^sub>2" shows "(f, h) \ A\<^sub>1 O A\<^sub>2 \ B\<^sub>1 O B\<^sub>2 \ C\<^sub>1 O C\<^sub>2" proof - note assms(1) also note assms(2) also note fun_rel_mono[OF order_refl fun_rel_comp_dist] finally show ?thesis by this qed lemma relcomp_trans_4[trans]: assumes "(f, g) \ A\<^sub>1 \ B\<^sub>1 \ C\<^sub>1 \ D\<^sub>1" assumes "(g, h) \ A\<^sub>2 \ B\<^sub>2 \ C\<^sub>2 \ D\<^sub>2" shows "(f, h) \ A\<^sub>1 O A\<^sub>2 \ B\<^sub>1 O B\<^sub>2 \ C\<^sub>1 O C\<^sub>2 \ D\<^sub>1 O D\<^sub>2" proof - note assms(1) also note assms(2) also note fun_rel_mono[OF order_refl fun_rel_mono[OF order_refl fun_rel_comp_dist]] finally show ?thesis by this qed lemma relcomp_trans_5[trans]: assumes "(f, g) \ A\<^sub>1 \ B\<^sub>1 \ C\<^sub>1 \ D\<^sub>1 \ E\<^sub>1" assumes "(g, h) \ A\<^sub>2 \ B\<^sub>2 \ C\<^sub>2 \ D\<^sub>2 \ E\<^sub>2" shows "(f, h) \ A\<^sub>1 O A\<^sub>2 \ B\<^sub>1 O B\<^sub>2 \ C\<^sub>1 O C\<^sub>2 \ D\<^sub>1 O D\<^sub>2 \ E\<^sub>1 O E\<^sub>2" proof - note assms(1) also note assms(2) also note fun_rel_mono[OF order_refl fun_rel_mono[OF order_refl fun_rel_mono[OF order_refl fun_rel_comp_dist]]] finally show ?thesis by this qed subsection \Relation Basics\ (* TODO Peter: these were copied from Sepref_HOL_Bindings, they should probably be part of $AFP/Automatic_Refinement *) lemma inv_fun_rel_eq[simp]: "(A\B)\ = A\\B\" by (auto dest: fun_relD) lemma inv_option_rel_eq[simp]: "(\K\option_rel)\ = \K\\option_rel" by (auto simp: option_rel_def) lemma inv_prod_rel_eq[simp]: "(P \\<^sub>r Q)\ = P\ \\<^sub>r Q\" by (auto) lemma inv_sum_rel_eq[simp]: "(\P,Q\sum_rel)\ = \P\,Q\\sum_rel" by (auto simp: sum_rel_def) lemma set_rel_converse[simp]: "(\A\ set_rel)\ = \A\\ set_rel" unfolding set_rel_def by auto lemma build_rel_domain[simp]: "Domain (br \ I) = Collect I" unfolding build_rel_def by auto lemma build_rel_range[simp]: "Range (br \ I) = \ ` Collect I" unfolding build_rel_def by auto lemma build_rel_image[simp]: "br \ I `` A = \ ` (A \ Collect I)" unfolding build_rel_def by auto lemma prod_rel_domain[simp]: "Domain (A \\<^sub>r B) = Domain A \ Domain B" unfolding prod_rel_def by auto lemma prod_rel_range[simp]: "Range (A \\<^sub>r B) = Range A \ Range B" unfolding prod_rel_def by auto lemma member_Id_on[iff]: "(x, y) \ Id_on A \ x = y \ y \ A" unfolding Id_on_def by auto lemma bijective_Id_on[intro!, simp]: "bijective (Id_on A)" unfolding bijective_def by auto lemma relcomp_Id_on[simp]: "Id_on A O Id_on B = Id_on (A \ B)" by auto lemma prod_rel_Id_on[simp]: "Id_on A \\<^sub>r Id_on B = Id_on (A \ B)" by auto lemma set_rel_Id_on[simp]: "\Id_on S\ set_rel = Id_on (Pow S)" unfolding set_rel_def by auto subsection \Parametricity\ lemmas basic_param[param] = option.rel_transfer[unfolded pred_bool_Id, to_set] All_transfer[unfolded pred_bool_Id, to_set] Ex_transfer[unfolded pred_bool_Id, to_set] Union_transfer[to_set] image_transfer[to_set] Image_parametric[to_set] lemma Sigma_param[param]: "(Sigma, Sigma) \ \A\ set_rel \ (A \ \B\ set_rel) \ \A \\<^sub>r B\ set_rel" unfolding Sigma_def by parametricity (* TODO: Lifting_Set.filter_transfer is too weak *) lemma set_filter_param[param]: "(Set.filter, Set.filter) \ (A \ bool_rel) \ \A\ set_rel \ \A\ set_rel" unfolding Set.filter_def fun_rel_def set_rel_def by blast lemma is_singleton_param[param]: assumes "bijective A" shows "(is_singleton, is_singleton) \ \A\ set_rel \ bool_rel" using assms unfolding is_singleton_def set_rel_def bijective_def by auto blast+ lemma the_elem_param[param]: assumes "is_singleton S" "is_singleton T" assumes "(S, T) \ \A\ set_rel" shows "(the_elem S, the_elem T) \ A" using assms unfolding set_rel_def is_singleton_def by auto subsection \Lists\ lemma list_all2_list_rel_conv[pred_set_conv]: "list_all2 (\ x y. (x, y) \ R) = (\ x y. (x, y) \ \R\ list_rel)" unfolding list_rel_def by simp lemmas list_rel_single_valued[iff] = list_rel_sv_iff lemmas list_rel_simps[simp] = list.rel_eq_onp[to_set] list.rel_conversep[to_set, symmetric] list.rel_compp[to_set] lemmas list_rel_param[param] = list.set_transfer[to_set] list.pred_transfer[unfolded pred_bool_Id, to_set, folded pred_list_listsp] list.rel_transfer[unfolded pred_bool_Id, to_set] + lemmas null_param[param] = null_transfer[unfolded pred_bool_Id, to_set] + (* TODO Peter: param_set is too restrictive *) thm param_set list.set_transfer[to_set] lemmas scan_param[param] = scan.transfer[to_set] lemma bind_param[param]: "(List.bind, List.bind) \ \A\ list_rel \ (A \ \B\ list_rel) \ \B\ list_rel" unfolding List.bind_def by parametricity lemma set_id_param[param]: "(set, id) \ \A\ list_set_rel \ \A\ set_rel" unfolding list_set_rel_def relcomp_unfold in_br_conv by auto parametricity subsection \Streams\ definition stream_rel :: "('a \ 'b) set \ ('a stream \ 'b stream) set" where [to_relAPP]: "stream_rel R \ {(x, y). stream_all2 (\ x y. (x, y) \ R) x y}" lemma stream_all2_stream_rel_conv[pred_set_conv]: "stream_all2 (\ x y. (x, y) \ R) = (\ x y. (x, y) \ \R\ stream_rel)" unfolding stream_rel_def by simp lemmas stream_rel_coinduct'[case_names stream_rel, coinduct set: stream_rel] = stream_rel_coinduct[to_set] lemmas stream_rel_intros = stream.rel_intros[to_set] lemmas stream_rel_cases = stream.rel_cases[to_set] lemmas stream_rel_inject[iff] = stream.rel_inject[to_set] (* TODO: why is stream.right_unique_rel not generated as an iff rule? *) lemma stream_rel_single_valued[iff]: "single_valued (\A\ stream_rel) \ single_valued A" proof show "single_valued A" if "single_valued (\A\ stream_rel)" proof (intro single_valuedI) fix x y z assume "(x, y) \ A" "(x, z) \ A" then have "(sconst x, sconst y) \ \A\ stream_rel" "(sconst x, sconst z) \ \A\ stream_rel" unfolding stream_rel_sconst[to_set] by this then have "sconst y = sconst z" using single_valuedD that by metis then show "y = z" by simp qed show "single_valued A \ single_valued (\A\ stream_rel)" using stream.right_unique_rel[to_set, to_set] by this qed lemmas stream_rel_simps[simp] = stream.rel_eq[unfolded pred_Id, THEN IdD, to_set] stream.rel_eq_onp[to_set] stream.rel_conversep[to_set] stream.rel_compp[to_set] lemmas stream_rel_param[param] = stream.ctr_transfer[to_set] stream.sel_transfer[to_set] stream.pred_transfer[unfolded pred_bool_Id, to_set, folded pred_stream_streamsp] stream.rel_transfer[unfolded pred_bool_Id, to_set] stream.map_transfer[to_set] stream.set_transfer[to_set] stream.case_transfer[to_set] stream.corec_transfer[unfolded pred_bool_Id, to_set] (* TODO: why is this not generated by the datatype package when stream.Domainp_rel is? *) lemma stream_Rangep_rel: "Rangep (stream_all2 R) = pred_stream (Rangep R)" proof - have 1: "pred_stream (Rangep R) v" if "stream_all2 R u v" for u v using that by (coinduction arbitrary: u v) (auto elim: stream.rel_cases) have 2: "stream_all2 R (smap (\ y. SOME x. R x y) v) v" if "pred_stream (Rangep R) v" for v using that by (coinduction arbitrary: v) (auto intro: someI) show ?thesis using 1 2 by blast qed lemmas stream_rel_domain[simp] = stream.Domainp_rel[to_set] lemmas stream_rel_range[simp] = stream_Rangep_rel[to_set] lemma stream_param[param]: assumes"(HOL.eq, HOL.eq) \ R \ R \ bool_rel" shows "(HOL.eq, HOL.eq) \ \R\ stream_rel \ \R\ stream_rel \ bool_rel" proof - have "(stream_all2 HOL.eq, stream_all2 HOL.eq) \ \R\ stream_rel \ \R\ stream_rel \ bool_rel" using assms by parametricity then show ?thesis unfolding stream.rel_eq by this qed lemmas szip_param[param] = szip_transfer[to_set] lemmas siterate_param[param] = siterate_transfer[to_set] lemmas sscan_param[param] = sscan.transfer[to_set] lemma streams_param[param]: "(streams, streams) \ \A\ set_rel \ \\A\ stream_rel\ set_rel" proof (intro fun_relI set_relI) fix S T assume 1: "(S, T) \ \A\ set_rel" obtain f where 2: "\ x. x \ S \ f x \ T \ (x, f x) \ A" using 1 unfolding set_rel_def by auto metis have 3: "f ` S \ T" "(id, f) \ Id_on S \ A" using 2 by auto obtain g where 4: "\ y. y \ T \ g y \ S \ (g y, y) \ A" using 1 unfolding set_rel_def by auto metis have 5: "g ` T \ S" "(g, id) \ Id_on T \ A" using 4 by auto show "\ v \ streams T. (u, v) \ \A\ stream_rel" if "u \ streams S" for u proof show "smap f u \ streams T" using smap_streams 3 that by blast have "(smap id u, smap f u) \ \A\ stream_rel" using 3 that by parametricity auto then show "(u, smap f u) \ \A\ stream_rel" by simp qed show "\ u \ streams S. (u, v) \ \A\ stream_rel" if "v \ streams T" for v proof show "smap g v \ streams S" using smap_streams 5 that by blast have "(smap g v, smap id v) \ \A\ stream_rel" using 5 that by parametricity auto then show "(smap g v, v) \ \A\ stream_rel" by simp qed qed lemma holds_param[param]: "(holds, holds) \ (A \ bool_rel) \ (\A\ stream_rel \ bool_rel)" unfolding holds.simps by parametricity lemma HLD_param[param]: assumes "single_valued A" "single_valued (A\)" shows "(HLD, HLD) \ \A\ set_rel \ \A\ stream_rel \ bool_rel" using assms unfolding HLD_def by parametricity lemma ev_param[param]: "(ev, ev) \ (\A\ stream_rel \ bool_rel) \ (\A\ stream_rel \ bool_rel)" proof safe fix P Q u v assume 1: "(P, Q) \ \A\ stream_rel \ bool_rel" "(u, v) \ \A\ stream_rel" note 2 = 1[param_fo] stream_rel_param(3)[param_fo] show "ev Q v" if "ev P u" using that 2 by (induct arbitrary: v) (blast+) show "ev P u" if "ev Q v" using that 2 by (induct arbitrary: u) (blast+) qed lemma alw_param[param]: "(alw, alw) \ (\A\ stream_rel \ bool_rel) \ (\A\ stream_rel \ bool_rel)" proof safe fix P Q u v assume 1: "(P, Q) \ \A\ stream_rel \ bool_rel" "(u, v) \ \A\ stream_rel" note 2 = 1[param_fo] stream_rel_param(3)[param_fo] show "alw Q v" if "alw P u" using that 2 by (coinduction arbitrary: u v) (auto, blast) show "alw P u" if "alw Q v" using that 2 by (coinduction arbitrary: u v) (auto, blast) qed subsection \Functional Relations\ lemma br_set_rel: "\br f P\ set_rel = br (image f) (\ A. Ball A P)" using br_set_rel_alt by (auto simp: build_rel_def) lemma br_list_rel: "\br f P\ list_rel = br (map f) (list_all P)" proof safe fix u v show "(u, v) \ br (map f) (list_all P)" if "(u, v) \ \br f P\ list_rel" using that unfolding build_rel_def by induct auto show "(u, v) \ \br f P\ list_rel" if "(u, v) \ br (map f) (list_all P)" using that unfolding build_rel_def by (induct u arbitrary: v) (auto) qed lemma br_list_set_rel: "\br f P\ list_set_rel = br (set \ map f) (\ s. list_all P s \ distinct (map f s))" unfolding list_set_rel_def br_list_rel unfolding br_chain by rule lemma br_fun_rel1: "Id \ br f P = br (comp f) (All \ comp P)" unfolding fun_rel_def Ball_def by (auto simp: build_rel_def) (* notes *) (* TODO Peter: the way \\ and \\\ are declared, a lot of unexpected abbreviation folding takes place *) term "set \ map f \ map g \ map h" (* in large expressions, this can introduce unneccessary paretheses and in general, makes things very hard to read *) (* it is even possible for other abbreviations to be torn apart by this *) term "set \ sort" (* I think that there were even cases where eta-expanded terms were torn apart, but I do not have an example at the moment *) (* the following abbreviations work better, a term can only be abbreviated by comp_n if it contains the constant comp at least n times, thus they should only be folded back if the original term really had the right degree of "point-free-ness" *) (* abbreviation comp_2 (infixl "\\" 55) where "f \\ g \ comp (comp f) g" abbreviation comp_3 (infixl "\\\" 55) where "f \\\ g \ comp (comp (comp f)) g" abbreviation comp_4 (infixl "\\\\" 55) where "f \\\\ g \ comp (comp (comp (comp f))) g" abbreviation comp_5 (infixl "\\\\\" 55) where "f \\\\\ g \ comp (comp (comp (comp (comp f)))) g" *) (* since the root of the right hand side term is not a lambda abstraction, this abbreviation should also not be able to introduce any parentheses *) end diff --git a/thys/Transition_Systems_and_Automata/ROOT b/thys/Transition_Systems_and_Automata/ROOT --- a/thys/Transition_Systems_and_Automata/ROOT +++ b/thys/Transition_Systems_and_Automata/ROOT @@ -1,42 +1,43 @@ chapter AFP session Transition_Systems_and_Automata (AFP) = "Collections" + options [timeout = 2400] sessions "DFS_Framework" "Gabow_SCC" directories "Basic" "Transition_Systems" "Automata" "Automata/DFA" "Automata/NFA" "Automata/DBA" "Automata/DBTA" "Automata/DCA" "Automata/DRA" "Automata/NBA" "Automata/NBTA" theories "Basic/Basic" "Basic/Sequence" "Basic/Sequence_Zip" "Basic/Sequence_LTL" "Basic/Maps" "Basic/Acceptance" + "Basic/Degeneralization" "Transition_Systems/Transition_System" "Transition_Systems/Transition_System_Extra" "Transition_Systems/Transition_System_Construction" "Automata/DFA/DFA" "Automata/NFA/NFA" "Automata/DBA/DBA_Combine" "Automata/DBTA/DBTA_Combine" "Automata/DCA/DCA_Combine" "Automata/DRA/DRA_Combine" "Automata/DRA/DRA_Translate" "Automata/NBA/NBA_Combine" "Automata/NBA/NBA_Translate" "Automata/NBA/NGBA_Algorithms" "Automata/NBTA/NBTA_Combine" document_files "root.tex"