diff --git a/thys/EFSM_Inference/Code_Generation.thy b/thys/Extended_Finite_State_Machine_Inference/Code_Generation.thy rename from thys/EFSM_Inference/Code_Generation.thy rename to thys/Extended_Finite_State_Machine_Inference/Code_Generation.thy diff --git a/thys/EFSM_Inference/EFSM_Dot.thy b/thys/Extended_Finite_State_Machine_Inference/EFSM_Dot.thy rename from thys/EFSM_Inference/EFSM_Dot.thy rename to thys/Extended_Finite_State_Machine_Inference/EFSM_Dot.thy diff --git a/thys/EFSM_Inference/Inference.thy b/thys/Extended_Finite_State_Machine_Inference/Inference.thy rename from thys/EFSM_Inference/Inference.thy rename to thys/Extended_Finite_State_Machine_Inference/Inference.thy diff --git a/thys/EFSM_Inference/ROOT b/thys/Extended_Finite_State_Machine_Inference/ROOT rename from thys/EFSM_Inference/ROOT rename to thys/Extended_Finite_State_Machine_Inference/ROOT --- a/thys/EFSM_Inference/ROOT +++ b/thys/Extended_Finite_State_Machine_Inference/ROOT @@ -1,36 +1,36 @@ chapter AFP -session EFSM_Inference (AFP) = Extended_Finite_State_Machines + +session Extended_Finite_State_Machine_Inference (AFP) = Extended_Finite_State_Machines + options [timeout = 600] directories "heuristics" "code-targets" "examples" theories "Subsumption" "examples/Drinks_Subsumption" "Inference" "SelectionStrategies" "heuristics/Store_Reuse" "heuristics/Store_Reuse_Subsumption" "heuristics/Increment_Reset" "heuristics/Same_Register" "heuristics/Least_Upper_Bound" "heuristics/Distinguishing_Guards" "heuristics/Weak_Subsumption" "heuristics/PTA_Generalisation" "EFSM_Dot" "efsm2sal" "code-targets/Code_Target_List" "code-targets/Code_Target_Set" "code-targets/Code_Target_FSet" "Code_Generation" document_files "root.tex" "root.bib" diff --git a/thys/EFSM_Inference/SelectionStrategies.thy b/thys/Extended_Finite_State_Machine_Inference/SelectionStrategies.thy rename from thys/EFSM_Inference/SelectionStrategies.thy rename to thys/Extended_Finite_State_Machine_Inference/SelectionStrategies.thy diff --git a/thys/EFSM_Inference/Subsumption.thy b/thys/Extended_Finite_State_Machine_Inference/Subsumption.thy rename from thys/EFSM_Inference/Subsumption.thy rename to thys/Extended_Finite_State_Machine_Inference/Subsumption.thy diff --git a/thys/EFSM_Inference/code-targets/Code_Target_FSet.thy b/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_FSet.thy rename from thys/EFSM_Inference/code-targets/Code_Target_FSet.thy rename to thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_FSet.thy diff --git a/thys/EFSM_Inference/code-targets/Code_Target_List.thy b/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_List.thy rename from thys/EFSM_Inference/code-targets/Code_Target_List.thy rename to thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_List.thy diff --git a/thys/EFSM_Inference/code-targets/Code_Target_Set.thy b/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy rename from thys/EFSM_Inference/code-targets/Code_Target_Set.thy rename to thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy diff --git a/thys/EFSM_Inference/document/root.bib b/thys/Extended_Finite_State_Machine_Inference/document/root.bib rename from thys/EFSM_Inference/document/root.bib rename to thys/Extended_Finite_State_Machine_Inference/document/root.bib diff --git a/thys/EFSM_Inference/document/root.tex b/thys/Extended_Finite_State_Machine_Inference/document/root.tex rename from thys/EFSM_Inference/document/root.tex rename to thys/Extended_Finite_State_Machine_Inference/document/root.tex diff --git a/thys/EFSM_Inference/efsm2sal.thy b/thys/Extended_Finite_State_Machine_Inference/efsm2sal.thy rename from thys/EFSM_Inference/efsm2sal.thy rename to thys/Extended_Finite_State_Machine_Inference/efsm2sal.thy diff --git a/thys/EFSM_Inference/examples/Drinks_Subsumption.thy b/thys/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy rename from thys/EFSM_Inference/examples/Drinks_Subsumption.thy rename to thys/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy --- a/thys/EFSM_Inference/examples/Drinks_Subsumption.thy +++ b/thys/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy @@ -1,154 +1,154 @@ subsection{*Example*} text{*This theory shows how contexts can be used to prove transition subsumption.*} theory Drinks_Subsumption -imports "EFSM_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2" +imports "Extended_Finite_State_Machine_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2" begin lemma stop_at_3: "\obtains 1 c drinks2 3 r t" proof(induct t arbitrary: r) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) by (simp add: drinks2_def) qed lemma no_1_2: "\obtains 1 c drinks2 2 r t" proof(induct t arbitrary: r) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) apply (simp add: drinks2_def) apply clarsimp apply (simp add: drinks2_def[symmetric]) apply (erule disjE) apply simp apply (erule disjE) apply simp by (simp add: stop_at_3) qed lemma no_change_1_1: "obtains 1 c drinks2 1 r t \ c = r" proof(induct t) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) apply (simp add: drinks2_def) apply clarsimp apply (simp add: drinks2_def[symmetric]) apply (erule disjE) apply (simp add: vend_nothing_def apply_updates_def) by (simp add: no_1_2) qed lemma obtains_1: "obtains 1 c drinks2 0 <> t \ c $ 2 = Some (Num 0)" proof(induct t) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) apply (simp add: drinks2_def) apply clarsimp apply (simp add: drinks2_def[symmetric]) apply (simp add: select_def can_take apply_updates_def) using no_change_1_1 by fastforce qed lemma obtains_1_1_2: "obtains 1 c1 drinks2 1 r t \ obtains 1 c2 drinks 1 r t \ c1 = r \ c2 = r" proof(induct t arbitrary: r) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) apply (simp add: drinks2_def drinks_def) apply clarsimp apply (simp add: drinks2_def[symmetric] drinks_def[symmetric]) apply safe using Cons.prems(1) no_change_1_1 apply blast apply (simp add: coin_def vend_nothing_def) using Cons.prems(1) no_change_1_1 apply blast apply (simp add: vend_fail_def vend_nothing_def apply_updates_def) using Cons.prems(1) no_change_1_1 apply blast apply (metis drinks_rejects_future numeral_eq_one_iff obtains.cases obtains_recognises semiring_norm(85)) using no_1_2 apply blast using no_1_2 apply blast using Cons.prems(1) no_change_1_1 apply blast using no_1_2 apply blast using no_1_2 apply blast using no_1_2 by blast qed lemma obtains_1_c2: "obtains 1 c1 drinks2 0 <> t \ obtains 1 c2 drinks 0 <> t \ c2 $ 2 = Some (Num 0)" proof(induct t) case Nil then show ?case by (simp add: obtains_base) next case (Cons a t) then show ?case apply (case_tac a) apply (simp add: obtains_step) apply clarify apply (simp add: in_possible_steps[symmetric]) apply (simp add: drinks2_def drinks_def) apply clarsimp apply (simp add: drinks2_def[symmetric] drinks_def[symmetric]) apply (simp add: select_def can_take apply_updates_def) using obtains_1_1_2 by fastforce qed lemma directly_subsumes: "directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing" apply (rule direct_subsumption[of _ _ _ _ "\c2. c2 $ 2 = Some (Num 0)"]) apply (simp add: obtains_1_c2) apply (rule subsumption) apply (simp add: vend_fail_def vend_nothing_def) apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true) apply (simp add: vend_fail_def vend_nothing_def) by (simp add: posterior_separate_def vend_fail_def vend_nothing_def) lemma directly_subsumes_flip: "directly_subsumes drinks2 drinks 1 1 vend_nothing vend_fail" apply (rule direct_subsumption[of _ _ _ _ "\c2. c2 $ 2 = Some (Num 0)"]) apply (simp add: obtains_1_c2) apply (rule subsumption) apply (simp add: vend_fail_def vend_nothing_def) apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true) apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true) by (simp add: posterior_separate_def vend_fail_def vend_nothing_def) end diff --git a/thys/EFSM_Inference/heuristics/Distinguishing_Guards.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Distinguishing_Guards.thy rename from thys/EFSM_Inference/heuristics/Distinguishing_Guards.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Distinguishing_Guards.thy diff --git a/thys/EFSM_Inference/heuristics/Group_By.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Group_By.thy rename from thys/EFSM_Inference/heuristics/Group_By.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Group_By.thy diff --git a/thys/EFSM_Inference/heuristics/Increment_Reset.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Increment_Reset.thy rename from thys/EFSM_Inference/heuristics/Increment_Reset.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Increment_Reset.thy diff --git a/thys/EFSM_Inference/heuristics/Least_Upper_Bound.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy rename from thys/EFSM_Inference/heuristics/Least_Upper_Bound.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy diff --git a/thys/EFSM_Inference/heuristics/PTA_Generalisation.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/PTA_Generalisation.thy rename from thys/EFSM_Inference/heuristics/PTA_Generalisation.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/PTA_Generalisation.thy diff --git a/thys/EFSM_Inference/heuristics/Same_Register.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Same_Register.thy rename from thys/EFSM_Inference/heuristics/Same_Register.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Same_Register.thy diff --git a/thys/EFSM_Inference/heuristics/Store_Reuse.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse.thy rename from thys/EFSM_Inference/heuristics/Store_Reuse.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse.thy diff --git a/thys/EFSM_Inference/heuristics/Store_Reuse_Subsumption.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse_Subsumption.thy rename from thys/EFSM_Inference/heuristics/Store_Reuse_Subsumption.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse_Subsumption.thy diff --git a/thys/EFSM_Inference/heuristics/Weak_Subsumption.thy b/thys/Extended_Finite_State_Machine_Inference/heuristics/Weak_Subsumption.thy rename from thys/EFSM_Inference/heuristics/Weak_Subsumption.thy rename to thys/Extended_Finite_State_Machine_Inference/heuristics/Weak_Subsumption.thy diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,561 +1,561 @@ ADS_Functor AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations Banach_Steinhaus Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DynamicArchitectures Dynamic_Tables -EFSM_Inference E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machines +Extended_Finite_State_Machine_Inference FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Projective_Geometry Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD Robinson_Arithmetic RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL