Started by an SCM change Running as SYSTEM [EnvInject] - Loading node environment variables. Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all [isabelle-all] $ hg showconfig paths.default [isabelle-all] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ real URL is https://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-all] $ hg update --clean --rev default 1 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-all] $ hg log --rev . --template {node} [isabelle-all] $ hg log --rev . --template {rev} [isabelle-all] $ hg log --rev 83d465d71fc6287d9736b47d94828044720e1fa8 --template exists\n exists [isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(83d465d71fc6287d9736b47d94828044720e1fa8)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://foss.heptapod.net/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 1424 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev 75a5ba7c00bcb5f44d7f40dd0d400c2b6056b140 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(75a5ba7c00bcb5f44d7f40dd0d400c2b6056b140)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-all] $ /bin/sh -xe /tmp/jenkins6957395974096204597.sh + Admin/jenkins/run_build all + set -e + PROFILE=all + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ... ### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ... Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ... ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ... ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ... + bin/isabelle ocaml_setup # Run eval $(opam env) to update the current shell environment [NOTE] It seems you have not updated your repositories for a while. Consider updating them with: opam update [NOTE] Package zarith is already installed (current version is 1.12). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.10.7 + bin/isabelle ci_build_all === CONFIGURATION === ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g" ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64_32-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-15c840d48c9a/x86_64_32-linux" ML_SYSTEM="polyml-5.9" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 8, threads = 8, numa = true === BUILD === Build started at Wed, 21 Sep 2022 07:42:28 +0200 Isabelle id d435f7b57212 AFP id bccf6f281b7b === LOG === Session Pure/Pure Session Misc/CTT Session Misc/Cube Session FOL/FOL Session FOL/CCL Session FOL/FOL-ex Session FOL/FOLP Session FOL/FOLP-ex Session Doc/Intro (doc) Session FOL/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Pure/Pure-Examples Session Pure/Pure-ex Session Misc/SML Session Misc/Sequents Session Doc/Sledgehammer (doc) Session AFP/SpecCheck (AFP) Session Misc/Tools Session HOL/HOL (main) Session AFP/AVL-Trees (AFP) Session AFP/AWN (AFP) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/Ackermanns_not_PR (AFP) Session AFP/AnselmGod (AFP) Session AFP/Aristotles_Assertoric_Syllogistic (AFP) Session AFP/Attack_Trees (AFP) Session AFP/AxiomaticCategoryTheory (AFP) Session AFP/Belief_Revision (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Boolos_Curious_Inference (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/C2KA_DistributedSystems (AFP) Session AFP/CISC-Kernel (AFP) Session AFP/CYK (AFP) Session AFP/Cauchy (AFP) Session AFP/Sqrt_Babylonian (AFP) Session Doc/Classes (doc) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/Complete_Non_Orders (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Dedekind_Real (AFP) Session AFP/Depth-First-Search (AFP) Session AFP/Digit_Expansions (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/DiskPaxos (AFP) Session AFP/Example-Submission (AFP) Session AFP/FFT (AFP) Session AFP/FLP (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Foundation_of_geometry (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/Fresh_Identifiers (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session Doc/Functions (doc) Session AFP/GPU_Kernel_PL (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (AFP) Session AFP/GoedelGod (AFP) Session AFP/Goodstein_Lambda (AFP) Session HOL/HOL-Cardinals (timing) Session AFP/Binding_Syntax_Theory (AFP) Session AFP/Ordinals_and_Cardinals (AFP) Session HOL/HOL-Hoare Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-IMPP Session HOL/HOL-IOA Session HOL/HOL-Import Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session AFP/ADS_Functor (AFP) Session AFP/Approximation_Algorithms (AFP) Session AFP/ArrowImpossibilityGS (AFP) Session AFP/Auto2_HOL (AFP) Session AFP/BNF_CC (AFP) Session AFP/BNF_Operations (AFP) Session AFP/Binomial-Heaps (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BD_Security_Compositional (AFP) Session AFP/CoSMeDis (AFP) Session AFP/CoCon (AFP) Session AFP/CoSMed (AFP) Session AFP/Buildings (AFP) Session AFP/CRDT (AFP) Session AFP/IMAP-CRDT (AFP) Session AFP/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Category (AFP) Session Doc/Codegen (doc) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/Conditional_Simplification (AFP) Session AFP/Conditional_Transfer_Rule (AFP) Session AFP/CoreC++ (AFP) Session AFP/Core_DOM (AFP) Session AFP/Shadow_DOM (AFP) Session AFP/DOM_Components (AFP) Session AFP/Core_SC_DOM (AFP) Session AFP/Shadow_SC_DOM (AFP) Session AFP/SC_DOM_Components (AFP) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Epistemic_Logic (AFP) Session AFP/Public_Announcement_Logic (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Seq_Calc1 (AFP) Session AFP/FOL_Axiomatic (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (AFP) Session AFP/FinFun (AFP) Session AFP/Extended_Finite_State_Machines (AFP) Session AFP/Extended_Finite_State_Machine_Inference (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Finite-Map-Extras (AFP) Session AFP/Generalized_Counting_Sort (AFP) Session AFP/Graph_Saturation (AFP) Session AFP/Group-Ring-Module (AFP) Session AFP/Valuation (AFP) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Combinatorics (main timing) Session AFP/Blue_Eyes (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session AFP/Finitely_Generated_Abelian_Groups (AFP) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP) Session AFP/Localization_Ring (AFP) Session AFP/Orbit_Stabiliser (AFP) Session AFP/Perfect-Number-Thm (AFP) Session AFP/Secondary_Sylow (AFP) Session AFP/Jordan_Hoelder (AFP) Session AFP/VectorSpace (AFP) Session HOL/HOL-Analysis (main timing) Session AFP/Actuarial_Mathematics (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/Coinductive (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Architectural_Design_Patterns (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Topology (AFP) Session AFP/Complex_Geometry (AFP) Session AFP/Poincare_Disc (AFP) Session AFP/Differential_Game_Logic (AFP) Session AFP/First_Welfare_Theorem (AFP) Session AFP/Green (AFP) Session HOL/HOL-Analysis-ex Session HOL/HOL-Complex_Analysis (main timing) Session AFP/Cartan_FP (AFP) Session HOL/HOL-Eisbach Session AFP/Allen_Calculus (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Equivalence_Relation_Enumeration (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/Case_Labeling (AFP) Session AFP/Clean (AFP) Session AFP/Combinatorics_Words (AFP) Session AFP/Combinatorics_Words_Graph_Lemma (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session Doc/Eisbach (doc) Session HOL/HOL-Hahn_Banach Session HOL/HOL-Homology (timing) Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/DiscretePricing (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Gromov_Hyperbolicity (AFP) Session AFP/Laws_of_Large_Numbers (AFP) Session AFP/Fisher_Yates (AFP) Session AFP/Girth_Chromatic (AFP) Session AFP/Random_Graph_Subgraph_Threshold (AFP) Session HOL/HOL-Probability-ex (timing) Session AFP/Hahn_Jordan_Decomposition (AFP) Session AFP/Lp (AFP) Session AFP/MDP-Rewards (AFP) Session AFP/Markov_Models (AFP) Session AFP/Monad_Normalisation (AFP) Session AFP/Monomorphic_Monad (AFP) Session AFP/Neumann_Morgenstern_Utility (AFP) Session AFP/Probabilistic_Noninterference (AFP) Session AFP/Probabilistic_System_Zoo (AFP) Session AFP/Quasi_Borel_Spaces (AFP) Session AFP/Skip_Lists (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Hyperdual (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Laplace_Transform (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Octonions (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Quaternions (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Hermite (AFP) Session AFP/MDP-Algorithms (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/Youngs_Inequality (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Examples Session HOL/HOL-Isar_Examples Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session AFP/Arith_Prog_Rel_Primes (AFP) Session AFP/Bernoulli (AFP) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session AFP/Efficient-Mergesort (AFP) Session HOL/HOL-Codegenerator_Test Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Lehmer (AFP) Session AFP/Lifting_the_Exponent (AFP) Session AFP/Padic_Ints (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (AFP) Session AFP/RSAPSS (AFP) Session AFP/SumSquares (AFP) Session AFP/Liouville_Numbers (AFP) Session AFP/Lucas_Theorem (AFP) Session AFP/DPRM_Theorem (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Formal_Puiseux_Series (AFP) Session AFP/Probabilistic_Prime_Tests (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Safe_Distance (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Budan_Fourier (AFP) Session AFP/Three_Circles (AFP) Session AFP/Winding_Number_Eval (AFP) Session AFP/Count_Complex_Roots (AFP) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session AFP/Relational-Incorrectness-Logic (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Auto2_Imperative_HOL (AFP) Session AFP/Imperative_Insertion_Sort (AFP) Session HOL/HOL-Induct Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-ex Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/Free-Groups (AFP) Session AFP/Stern_Brocot (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/HyperCTL (AFP) Session AFP/Integration (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/LTL (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Landau_Symbols (AFP) Session AFP/Akra_Bazzi (AFP) Session AFP/Catalan_Numbers (AFP) Session AFP/Error_Function (AFP) Session AFP/Euler_MacLaurin (AFP) Session AFP/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/Median_Method (AFP) Session AFP/MuchAdoAboutTwo (AFP) Session AFP/Optics (AFP) Session AFP/UTP-Toolkit (AFP) Session AFP/UTP (AFP) Session AFP/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (AFP) Session AFP/Pell (AFP) Session AFP/Prefix_Free_Code_Combinators (AFP) Session AFP/Presburger-Automata (AFP) Session AFP/Priority_Queue_Braun (AFP) Session AFP/Program-Conflict-Analysis (AFP) Session AFP/Regular-Sets (AFP) Session AFP/Abstract-Rewriting (AFP) Session AFP/Decreasing-Diagrams (AFP) Session AFP/First_Order_Terms (AFP) Session AFP/Stateful_Protocol_Composition_and_Typing (AFP) Session AFP/Automated_Stateful_Protocol_Verification (AFP) Session AFP/Matrix (AFP) Session AFP/Matrix_Tensor (AFP) Session AFP/Knot_Theory (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/ResiduatedTransitionSystem (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Safe_OCL (AFP) Session AFP/Schutz_Spacetime (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Simplex (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Solidity (AFP) Session AFP/Sort_Encodings (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Closest_Pair_Points (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session Doc/System (doc) Session AFP/Szemeredi_Regularity (AFP) Session AFP/Roth_Arithmetic_Progressions (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-Matrix_LP Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mirabelle-ex Session HOL/HOL-Mutabelle Session HOL/HOL-NanoJava Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal Session AFP/CCS (AFP) Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/Pi_Calculus (AFP) Session AFP/Psi_Calculi (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Prolog Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-Real_Asymp Session AFP/Cotangent_PFD_Formula (AFP) Session AFP/Fourier (AFP) Session AFP/Furstenberg_Topology (AFP) Session HOL/HOL-Real_Asymp-Manual Session AFP/Sophomores_Dream (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/Irrationals_From_THEBOOK (AFP) Session AFP/Lambert_W (AFP) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-SMT_Examples (timing) Session HOL/HOL-SPARK Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session HOL/HOL-SPARK-Manual Session HOL/HOL-Statespace Session HOL/HOL-TLA Session HOL/HOL-TLA-Buffer Session HOL/HOL-TLA-Inc Session HOL/HOL-TLA-Memory Session HOL/HOL-TPTP Session HOL/HOL-Types_To_Sets Session AFP/Banach_Steinhaus (AFP) Session AFP/Smooth_Manifolds (AFP) Session AFP/Types_To_Sets_Extension (AFP) Session HOL/HOL-Unix Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session AFP/HOL-CSP (AFP) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session AFP/CSP_RefTK (AFP) Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session AFP/BirdKMP (AFP) Session HOL/HOLCF-Tutorial Session HOL/IOA (timing) Session HOL/IOA-ABP Session HOL/IOA-NTP Session HOL/IOA-Storage Session HOL/IOA-ex Session AFP/Shivers-CFA (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/Tycon (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Hales_Jewett (AFP) Session Misc/Haskell Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hello_World (AFP) Session AFP/Hood_Melville_Queue (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Huffman (AFP) Session AFP/Hybrid_Logic (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IFC_Tracking (AFP) Session AFP/IMP2 (AFP) Session AFP/IMP2_Binary_Heap (AFP) Session AFP/IMP_Compiler (AFP) Session AFP/IMP_Compiler_Reuse (AFP) Session Doc/Implementation (doc) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/Inductive_Inference (AFP) Session AFP/InfPathElimination (AFP) Session AFP/Intro_Dest_Elim (AFP) Session AFP/Involutions2Squares (AFP) Session AFP/IsaGeoCoq (AFP) Session AFP/IsaNet (AFP) Session Doc/Isar_Ref (doc) Session AFP/Isabelle_C (AFP) Session Doc/JEdit (doc) Session AFP/Jacobson_Basic_Algebra (AFP) Session AFP/Grothendieck_Schemes (AFP) Session AFP/Pluennecke_Ruzsa_Inequality (AFP) Session AFP/Khovanskii_Theorem (AFP) Session AFP/JiveDataStoreModel (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/Kleene_Algebra (AFP) Session AFP/KAD (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Algebraic_VCs (AFP) Session AFP/Multirelations (AFP) Session AFP/Quantales (AFP) Session AFP/Transformer_Semantics (AFP) Session AFP/Regular_Algebras (AFP) Session AFP/Relation_Algebra (AFP) Session AFP/Relational_Paths (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/Knights_Tour (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Jinja (AFP) Session AFP/Dominance_CHK (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/JinjaDCI (AFP) Session AFP/Regression_Test_Selection (AFP) Session AFP/List_Update (AFP) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Random_BSTs (AFP) Session AFP/Randomised_BSTs (AFP) Session AFP/Treaps (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/Fishburn_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/LocalLexing (AFP) Session Doc/Locales (doc) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Logging_Independent_Anonymity (AFP) Session AFP/Lowe_Ontological_Argument (AFP) Session Doc/Main (doc) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Matroids (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/KD_Tree (AFP) Session AFP/Menger (AFP) Session AFP/Mereology (AFP) Session AFP/Metalogic_ProofChecker (AFP) Session AFP/MiniML (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Nano_JSON (AFP) Session AFP/Nash_Williams (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/LambdaAuth (AFP) Session AFP/Launchbury (AFP) Session AFP/Call_Arity (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Rewriting_Z (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/NormByEval (AFP) Session AFP/OpSets (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/Design_Theory (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Lambda_Free_EPO (AFP) Session AFP/Ordered_Resolution_Prover (AFP) Session AFP/Chandy_Lamport (AFP) Session AFP/Saturation_Framework (AFP) Session AFP/Saturation_Framework_Extensions (AFP) Session AFP/Progress_Tracking (AFP) Session AFP/PAL (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Package_logic (AFP) Session AFP/Combinable_Wands (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/GaleStewart_Games (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Physical_Quantities (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session AFP/Priority_Search_Trees (AFP) Session AFP/Prim_Dijkstra_Simple (AFP) Session Doc/Prog_Prove (doc) Session AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Real_Power (AFP) Session AFP/Real_Time_Deque (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/Minsky_Machines (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Regex_Equivalence (AFP) Session AFP/Relational_Method (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Hoare_Time (AFP) Session AFP/Separata (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/SimplifiedOntologicalArgument (AFP) Session AFP/Sliding_Window_Algorithm (AFP) Session AFP/Statecharts (AFP) Session AFP/Stellar_Quorums (AFP) Session AFP/Stone_Algebras (AFP) Session AFP/Stone_Relation_Algebras (AFP) Session AFP/Stone_Kleene_Relation_Algebras (AFP) Session AFP/Aggregation_Algebras (AFP) Session AFP/Relational_Disjoint_Set_Forests (AFP) Session AFP/Relational_Minimum_Spanning_Trees (AFP) Session AFP/Relational_Forests (AFP) Session AFP/Subset_Boolean_Algebras (AFP) Session AFP/Correctness_Algebras (AFP) Session AFP/Store_Buffer_Reduction (AFP) Session AFP/Strong_Security (AFP) Session Doc/Sugar (doc) Session AFP/Sunflowers (AFP) Session AFP/Clique_and_Monotone_Circuits (AFP) Session AFP/Syntax_Independent_Logic (AFP) Session AFP/Goedel_Incompleteness (AFP) Session AFP/Goedel_HFSet_Semantic (AFP) Session AFP/Goedel_HFSet_Semanticless (AFP) Session AFP/Robinson_Arithmetic (AFP) Session AFP/Szpilrajn (AFP) Session AFP/Combinatorics_Words_Lyndon (AFP) Session AFP/TESL_Language (AFP) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Probabilistic_Timed_Automata (AFP) Session AFP/Topological_Semantics (AFP) Session AFP/Transitive-Closure-II (AFP) Session AFP/Tree_Decomposition (AFP) Session Doc/Tutorial (doc) Session Doc/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Van_der_Waerden (AFP) Session AFP/VeriComp (AFP) Session AFP/Interpreter_Optimizations (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session AFP/Weight_Balanced_Trees (AFP) Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Interval_Arithmetic_Word32 (AFP) Session AFP/LEM (AFP) Session AFP/Native_Word (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/FOL_Seq_Calc3 (AFP) Session AFP/Incredible_Proof_Machine (AFP) Session AFP/Deriving (AFP) Session AFP/CAVA_Base (AFP) Session AFP/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Gabow_SCC (AFP) Session AFP/LTL_to_GBA (AFP) Session AFP/Promela (AFP) Session AFP/Containers (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/Eval_FO (AFP) Session AFP/MFOTL_Monitor (AFP) Session AFP/Generic_Join (AFP) Session AFP/MFODL_Monitor_Optimized (AFP) Session AFP/VYDRA_MDL (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session AFP/Show (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/Hybrid_Systems_VCs (AFP) Session AFP/Matrices_for_ODEs (AFP) Session AFP/Taylor_Models (AFP) Session AFP/CakeML (AFP) Session AFP/Certification_Monads (AFP) Session AFP/AI_Planning_Languages_Semantics (AFP) Session AFP/Verified_SAT_Based_AI_Planning (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Monad_Memo_DP (AFP) Session AFP/Hidden_Markov_Models (AFP) Session AFP/Optimal_BST (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Amicable_Numbers (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Finite_Fields (AFP) Session AFP/Universal_Hash_Families (AFP) Session AFP/Frequency_Moments (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Gauss_Sums (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (AFP) Session AFP/IMO2019 (AFP) Session AFP/Irrational_Series_Erdos_Straus (AFP) Session AFP/Transcendence_Series_Hancl_Rucki (AFP) Session AFP/Zeta_3_Irrational (AFP) Session AFP/Gaussian_Integers (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Farkas (AFP) Session AFP/Isabelle_Marries_Dirac (AFP) Session AFP/Knuth_Bendix_Order (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Regular_Tree_Relations (AFP) Session AFP/FO_Theory_Rewriting (AFP) Session AFP/Rewrite_Properties_Reduction (AFP) Session AFP/Weighted_Path_Order (AFP) Session AFP/Multiset_Ordering_NPC (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Subresultants (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/BenOr_Kozen_Reif (AFP) Session AFP/LLL_Basis_Reduction (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Inequalities (AFP) Session AFP/LP_Duality (AFP) Session AFP/Linear_Programming (AFP) Session AFP/Number_Theoretic_Transform (AFP) Session AFP/CRYSTALS-Kyber (AFP) Session AFP/Smith_Normal_Form (AFP) Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP) Session AFP/Polynomials (AFP) Session AFP/Deep_Learning (AFP) Session AFP/QHLProver (AFP) Session AFP/Projective_Measurements (AFP) Session AFP/Commuting_Hermitian (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Fishers_Inequality (AFP) Session AFP/Groebner_Macaulay (AFP) Session AFP/Nullstellensatz (AFP) Session AFP/Signature_Groebner (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Symmetric_Polynomials (AFP) Session AFP/Pi_Transcendental (AFP) Session AFP/Power_Sum_Polynomials (AFP) Session AFP/Hermite_Lindemann (AFP) Session AFP/Factor_Algebraic_Polynomial (AFP) Session AFP/Cubic_Quartic_Equations (AFP) Session AFP/Linear_Recurrences_Solver (AFP) Session AFP/Virtual_Substitution (AFP) Session AFP/Real_Impl (AFP) Session AFP/Complex_Bounded_Operators (AFP) Session AFP/Registers (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/XML (AFP) Session AFP/Van_Emde_Boas_Trees (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/FOL_Seq_Calc2 (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/Gale_Shapley (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-ARCH-COMP (AFP) Session AFP/HOL-ODE-Examples (AFP large) Session AFP/Lorenz_Approximation (AFP) Session AFP/Lorenz_C0 (AFP large) Session AFP/Lorenz_C1 (AFP large) Session AFP/Poincare_Bendixson (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Adaptive_State_Counting (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/LTL_Master_Theorem (AFP) Session AFP/LTL_Normal_Form (AFP) Session AFP/Partial_Order_Reduction (AFP) Session AFP/SM_Base (AFP) Session AFP/SM (AFP) Session AFP/CAVA_Setup (AFP) Session AFP/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (AFP) Session AFP/KBPs (AFP) Session AFP/LTL_to_DRA (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Tree-Automata (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Higher_Order_Terms (AFP) Session AFP/CakeML_Codegen (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/WOOT_Strong_Eventual_Consistency (AFP) Session AFP/FSM_Tests (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session AFP/Mersenne_Primes (AFP) Session AFP/MiniSail (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/BTree (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Sepref_IICF (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/CryptHOL (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Multi_Party_Computation (AFP) Session AFP/Sigma_Commit_Crypto (AFP) Session AFP/Constructive_Cryptography_CM (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/Kruskal (AFP) Session AFP/PAC_Checker (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/VerifyThis2019 (AFP) Session AFP/Simplicial_complexes_and_boolean_functions (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/WebAssembly (AFP) Session AFP/SPARCv8 (AFP) Session AFP/X86_Semantics (AFP) Session AFP/ZFC_in_HOL (AFP) Session AFP/CZH_Foundations (AFP) Session AFP/CZH_Elementary_Categories (AFP) Session AFP/CZH_Universal_Constructions (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/Ordinal_Partitions (AFP) Session AFP/Wetzels_Problem (AFP) Session FOL/ZF (main timing) Session Doc/Logics_ZF (doc) Session AFP/Recursion-Addition (AFP) Session FOL/ZF-AC Session FOL/ZF-Coind Session FOL/ZF-Constructible Session AFP/Delta_System_Lemma (AFP) Session AFP/Transitive_Models (AFP) Session AFP/Independence_CH (AFP) Session AFP/Forcing (AFP) Session FOL/ZF-IMP Session FOL/ZF-Induct Session FOL/ZF-UNITY (timing) Session FOL/ZF-Resid Session FOL/ZF-ex Building Echelon_Form ... Building HOL-Computational_Algebra ... Running HOL-Codegenerator_Test ... Building Complex_Bounded_Operators ... Running Virtual_Substitution ... Building Projective_Measurements ... Building Dirichlet_Series ... Running Stochastic_Matrices ... Echelon_Form: theory HOL-Library.Code_Target_Int Echelon_Form: theory HOL-Library.More_List Echelon_Form: theory HOL-Library.Code_Abstract_Nat Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field Echelon_Form: theory HOL-Library.Function_Algebras Echelon_Form: theory HOL-Library.IArray HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring Echelon_Form: theory HOL-Library.Code_Cardinality Echelon_Form: theory HOL-Library.Z2 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fraction_Field HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Group_Closure HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Factorial_Ring HOL-Codegenerator_Test: theory HOL-Examples.Records HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Lazy_Test HOL-Codegenerator_Test: theory HOL-Examples.Gauss_Numbers HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field Dirichlet_Series: theory HOL-Combinatorics.Stirling Dirichlet_Series: theory HOL-Library.Adhoc_Overloading Dirichlet_Series: theory HOL-Library.BNF_Corec Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure Dirichlet_Series: theory HOL-Number_Theory.Cong Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree Complex_Bounded_Operators: theory Containers.List_Fusion Complex_Bounded_Operators: theory Containers.Extend_Partial_Order Complex_Bounded_Operators: theory Deriving.Comparator Complex_Bounded_Operators: theory Deriving.Derive_Manager Complex_Bounded_Operators: theory Deriving.Generator_Aux Complex_Bounded_Operators: theory Containers.Equal Complex_Bounded_Operators: theory HOL-Cardinals.Fun_More Complex_Bounded_Operators: theory HOL-Cardinals.Order_Relation_More Stochastic_Matrices: theory HOL-Eisbach.Eisbach Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field Stochastic_Matrices: theory HOL-Algebra.Congruence Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc Stochastic_Matrices: theory HOL-Library.Function_Algebras Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets Complex_Bounded_Operators: theory Containers.Closure_Set Stochastic_Matrices: theory HOL-Library.More_List HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del Echelon_Form: theory HOL-Library.Code_Target_Nat Complex_Bounded_Operators: theory HOL-Cardinals.Order_Union Virtual_Substitution: theory Deriving.Generator_Aux Projective_Measurements: theory HOL-Computational_Algebra.Fraction_Field Virtual_Substitution: theory Deriving.Derive_Manager Projective_Measurements: theory HOL-Algebra.Congruence Virtual_Substitution: theory HOL-Library.AList Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc Projective_Measurements: theory Abstract-Rewriting.Seq Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat Virtual_Substitution: theory HOL-Library.Conditional_Parametricity Projective_Measurements: theory HOL-Library.More_List Projective_Measurements: theory HOL-Library.While_Combinator Virtual_Substitution: theory HOL-Library.Fun_Lexorder Virtual_Substitution: theory HOL-Library.Code_Target_Int Virtual_Substitution: theory HOL-Library.Function_Algebras Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring Complex_Bounded_Operators: theory HOL-Computational_Algebra.Fraction_Field Complex_Bounded_Operators: theory HOL-Library.Adhoc_Overloading Virtual_Substitution: theory HOL-Library.Groups_Big_Fun Dirichlet_Series: theory HOL-Library.Monad_Syntax Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_Specs Virtual_Substitution: theory Abstract-Rewriting.Seq Echelon_Form: theory HOL-Computational_Algebra.Polynomial Echelon_Form: theory Cayley_Hamilton.Square_Matrix Echelon_Form: theory HOL-Library.Code_Target_Numeral Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat Echelon_Form: theory Gauss_Jordan.Code_Set Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_Specs Echelon_Form: theory Gauss_Jordan.Code_Z2 Dirichlet_Series: theory HOL-Library.Code_Target_Int Dirichlet_Series: theory HOL-Algebra.Congruence Complex_Bounded_Operators: theory HOL-Library.Char_ord Virtual_Substitution: theory HOL-Library.Code_Target_Nat HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted Projective_Measurements: theory Jordan_Normal_Form.Conjugate Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Extension Dirichlet_Series: theory HOL-Library.Code_Target_Nat Echelon_Form: theory Gauss_Jordan.IArray_Addenda Virtual_Substitution: theory HOL-Library.Ramsey Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom Dirichlet_Series: theory HOL-Library.Function_Algebras Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial Virtual_Substitution: theory HOL-Library.More_List Projective_Measurements: theory HOL-Computational_Algebra.Polynomial Dirichlet_Series: theory HOL-Library.More_List Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With Complex_Bounded_Operators: theory HOL-Library.Monad_Syntax Dirichlet_Series: theory HOL-Library.Code_Target_Numeral HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map Complex_Bounded_Operators: theory Deriving.Equality_Generator Dirichlet_Series: theory HOL-Library.Power_By_Squaring Complex_Bounded_Operators: theory HOL-Library.Code_Abstract_Nat Projective_Measurements: theory Matrix.Utility Complex_Bounded_Operators: theory HOL-Cardinals.Wellfounded_More Complex_Bounded_Operators: theory Containers.Containers_Auxiliary Complex_Bounded_Operators: theory HOL-Library.Code_Target_Int Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Relation Virtual_Substitution: theory HOL-Library.Sublist Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes Complex_Bounded_Operators: theory HOL-Library.Code_Target_Nat Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom Virtual_Substitution: theory HOL-Library.While_Combinator Dirichlet_Series: theory HOL-Real_Asymp.Inst_Existentials Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order Dirichlet_Series: theory Bernoulli.Bernoulli Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial Virtual_Substitution: theory HOL-Library.FSet Dirichlet_Series: theory HOL-Library.Going_To_Filter Projective_Measurements: theory Regular-Sets.Regular_Set Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Embedding Complex_Bounded_Operators: theory HOL-Library.Complemented_Lattices Projective_Measurements: theory HOL-Algebra.Order Complex_Bounded_Operators: theory HOL-Algebra.Congruence Complex_Bounded_Operators: theory HOL-Library.Code_Target_Numeral HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial Projective_Measurements: theory HOL-Computational_Algebra.Normalized_Fraction Dirichlet_Series: theory HOL-Number_Theory.Fib Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers Virtual_Substitution: theory HOL-Library.Poly_Mapping Virtual_Substitution: theory Polynomials.More_Modules Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial Projective_Measurements: theory VectorSpace.FunctionLemmas Complex_Bounded_Operators: theory Deriving.Equality_Instances Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_Misc Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction Dirichlet_Series: theory HOL-Algebra.Order Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant Complex_Bounded_Operators: theory HOL-Library.Function_Algebras Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Constructions Stochastic_Matrices: theory VectorSpace.FunctionLemmas Dirichlet_Series: theory HOL-Real_Asymp.Eventuallize Complex_Bounded_Operators: theory HOL-Library.IArray Dirichlet_Series: theory HOL-Real_Asymp.Lazy_Eval Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala Dirichlet_Series: theory HOL-Number_Theory.Totient Stochastic_Matrices: theory HOL-Algebra.Order Complex_Bounded_Operators: theory HOL-Library.More_List HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial Complex_Bounded_Operators: theory Deriving.Compare Virtual_Substitution: theory Matrix.Utility Virtual_Substitution: theory Open_Induction.Restricted_Predicates Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction Virtual_Substitution: theory Regular-Sets.Regular_Set Projective_Measurements: theory HOL-Algebra.Lattice Dirichlet_Series: theory Landau_Symbols.Group_Sort Dirichlet_Series: theory Matrix.Utility Complex_Bounded_Operators: theory Deriving.Comparator_Generator Complex_Bounded_Operators: theory Containers.Lexicographic_Order Virtual_Substitution: theory Show.Show Complex_Bounded_Operators: theory HOL-Computational_Algebra.Normalized_Fraction Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences Complex_Bounded_Operators: theory HOL-Algebra.Order Complex_Bounded_Operators: theory Containers.Containers_Generator Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements Dirichlet_Series: theory Polynomial_Factorization.Missing_List Stochastic_Matrices: theory HOL-Algebra.Lattice Complex_Bounded_Operators: theory Containers.Set_Linorder Complex_Bounded_Operators: theory HOL-Cardinals.Cardinal_Order_Relation Dirichlet_Series: theory HOL-Algebra.Lattice Projective_Measurements: theory HOL-Algebra.Complete_Lattice Complex_Bounded_Operators: theory HOL-Cardinals.Ordinal_Arithmetic Complex_Bounded_Operators: theory HOL-Library.RBT_Impl Echelon_Form: theory Gauss_Jordan.Code_Matrix Echelon_Form: theory Gauss_Jordan.Rref Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Normalized_Fraction Complex_Bounded_Operators: theory Containers.Collection_Enum Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products Echelon_Form: theory Gauss_Jordan.Elementary_Operations Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice Echelon_Form: theory Gauss_Jordan.Rank HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Primes Projective_Measurements: theory HOL-Algebra.Group HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Nth_Powers HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Squarefree Complex_Bounded_Operators: theory Deriving.Compare_Generator HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Dirichlet_Series: theory HOL-Algebra.Complete_Lattice HOL-Codegenerator_Test: theory HOL-Number_Theory.Eratosthenes Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Power_Series Virtual_Substitution: theory Show.Show_Instances Virtual_Substitution: theory Show.Show_Real Virtual_Substitution: theory Polynomials.MPoly_Type Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray Echelon_Form: theory Gauss_Jordan.Gauss_Jordan Stochastic_Matrices: theory HOL-Algebra.Group Complex_Bounded_Operators: theory HOL-Cardinals.Cardinal_Arithmetic HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring Complex_Bounded_Operators: theory Deriving.Compare_Instances Virtual_Substitution: theory Polynomials.More_MPoly_Type HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree Complex_Bounded_Operators: theory HOL-Algebra.Lattice Dirichlet_Series: theory HOL-Algebra.Group Projective_Measurements: theory HOL-Algebra.Coset Projective_Measurements: theory HOL-Algebra.FiniteProduct Complex_Bounded_Operators: theory Containers.Collection_Eq HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial Complex_Bounded_Operators: theory HOL-Library.Rewrite Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset Complex_Bounded_Operators: theory HOL-Cardinals.Cardinals Stochastic_Matrices: theory HOL-Algebra.Coset Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization Stochastic_Matrices: theory HOL-Algebra.FiniteProduct Complex_Bounded_Operators: theory HOL-Types_To_Sets.Types_To_Sets Projective_Measurements: theory HOL-Algebra.Ring HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_FPS Complex_Bounded_Operators: theory Polynomial_Interpolation.Missing_Unsorted HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Laurent_Series Virtual_Substitution: theory HOL-Library.Finite_Map Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays Echelon_Form: theory Gauss_Jordan.Linear_Maps Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial Complex_Bounded_Operators: theory Cauchy.CauchysMeanTheorem Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton Stochastic_Matrices: theory HOL-Algebra.Ring Complex_Bounded_Operators: theory Containers.DList_Set Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial Complex_Bounded_Operators: theory HOL-Computational_Algebra.Polynomial Complex_Bounded_Operators: theory HOL-Examples.Sqrt Complex_Bounded_Operators: theory HOL-Algebra.Complete_Lattice HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Computational_Algebra Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series Complex_Bounded_Operators: theory HOL-Algebra.Group Complex_Bounded_Operators: theory Jordan_Normal_Form.Conjugate HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces Echelon_Form: theory Gauss_Jordan.Determinants2 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays Echelon_Form: theory Gauss_Jordan.Inverse Projective_Measurements: theory HOL-Algebra.Module Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Abstract_Char HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat Echelon_Form: theory Gauss_Jordan.System_Of_Equations Projective_Measurements: theory VectorSpace.RingModuleFacts Projective_Measurements: theory VectorSpace.MonoidSums Projective_Measurements: theory VectorSpace.LinearCombinations Stochastic_Matrices: theory HOL-Algebra.Module Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring Complex_Bounded_Operators: theory HOL-Algebra.Coset Echelon_Form: theory Gauss_Jordan.Inverse_IArrays Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Projective_Measurements: theory Jordan_Normal_Form.Matrix Stochastic_Matrices: theory VectorSpace.RingModuleFacts Stochastic_Matrices: theory VectorSpace.MonoidSums Stochastic_Matrices: theory VectorSpace.LinearCombinations Stochastic_Matrices: theory Jordan_Normal_Form.Matrix Complex_Bounded_Operators: theory HOL-Algebra.FiniteProduct Dirichlet_Series: theory HOL-Algebra.Coset Dirichlet_Series: theory HOL-Algebra.FiniteProduct HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra Projective_Measurements: theory VectorSpace.SumSpaces Virtual_Substitution: theory Regular-Sets.Regular_Exp Complex_Bounded_Operators: theory HOL-Algebra.Ring Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm Virtual_Substitution: theory Regular-Sets.NDerivative Virtual_Substitution: theory Regular-Sets.Relation_Interpretation Complex_Bounded_Operators: theory Banach_Steinhaus.Banach_Steinhaus_Missing Projective_Measurements: theory VectorSpace.VectorSpace Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs Dirichlet_Series: theory HOL-Algebra.Ring Virtual_Substitution: theory Regular-Sets.Equivalence_Checking Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Virtual_Substitution: theory Regular-Sets.Regexp_Method Complex_Bounded_Operators: theory Banach_Steinhaus.Banach_Steinhaus Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full Complex_Bounded_Operators: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Dirichlet_Series: theory Landau_Symbols.Landau_More Complex_Bounded_Operators: theory Sqrt_Babylonian.Log_Impl Stochastic_Matrices: theory VectorSpace.SumSpaces Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Complex_Bounded_Operators: theory Sqrt_Babylonian.NthRoot_Impl Stochastic_Matrices: theory VectorSpace.VectorSpace Complex_Bounded_Operators: theory Polynomial_Interpolation.Ring_Hom Projective_Measurements: theory Jordan_Normal_Form.Column_Operations Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial Echelon_Form: theory Echelon_Form.Rings2 Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Projective_Measurements: theory Jordan_Normal_Form.Determinant Virtual_Substitution: theory Abstract-Rewriting.SN_Orders Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations Complex_Bounded_Operators: theory Sqrt_Babylonian.Sqrt_Babylonian Complex_Bounded_Operators: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Virtual_Substitution: theory Polynomials.Utils Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders Complex_Bounded_Operators: theory HOL-Computational_Algebra.Polynomial_Factorial Complex_Bounded_Operators: theory Real_Impl.Real_Impl Complex_Bounded_Operators: theory HOL-Algebra.Module Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_Ring Virtual_Substitution: theory Polynomials.Power_Products Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion Complex_Bounded_Operators: theory Containers.Collection_Order Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible Dirichlet_Series: theory HOL-Algebra.Generated_Groups Echelon_Form: theory Echelon_Form.Echelon_Form Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton Projective_Measurements: theory Jordan_Normal_Form.Char_Poly Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Complex_Bounded_Operators: theory Show.Show Timing HOL-Computational_Algebra (8 threads, 40.553s elapsed time, 199.601s cpu time, 6.310s GC time, factor 4.92) Finished HOL-Computational_Algebra (0:02:53 elapsed time, 0:04:11 cpu time, factor 1.45) Building HOL-Algebra ... Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial Complex_Bounded_Operators: theory VectorSpace.FunctionLemmas Complex_Bounded_Operators: theory VectorSpace.RingModuleFacts Virtual_Substitution: theory Polynomials.Polynomials Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace Dirichlet_Series: theory HOL-Algebra.Elementary_Groups HOL-Algebra: theory HOL-Algebra.README HOL-Algebra: theory HOL-Cardinals.Fun_More HOL-Algebra: theory HOL-Combinatorics.Transposition HOL-Algebra: theory HOL-Algebra.Congruence HOL-Algebra: theory HOL-Cardinals.Order_Union HOL-Algebra: theory HOL-Cardinals.Order_Relation_More HOL-Algebra: theory HOL-Algebra.Exponent Complex_Bounded_Operators: theory Show.Show_Instances Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form Complex_Bounded_Operators: theory VectorSpace.MonoidSums Stochastic_Matrices: theory Jordan_Normal_Form.Determinant Complex_Bounded_Operators: theory VectorSpace.LinearCombinations Dirichlet_Series: theory HOL-Computational_Algebra.Formal_Laurent_Series HOL-Algebra: theory HOL-Combinatorics.Permutations Echelon_Form: theory Echelon_Form.Echelon_Form_Det Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays HOL-Algebra: theory HOL-Cardinals.Wellfounded_More HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation Projective_Measurements: theory Isabelle_Marries_Dirac.Basics Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions Virtual_Substitution: theory Polynomials.Show_Polynomials Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly HOL-Algebra: theory HOL-Algebra.Order Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays Projective_Measurements: theory Jordan_Normal_Form.VS_Connect Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace Virtual_Substitution: theory Polynomials.MPoly_Type_Class Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays Dirichlet_Series: theory HOL-Algebra.AbelCoset Dirichlet_Series: theory HOL-Algebra.Module Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form HOL-Algebra: theory HOL-Combinatorics.Cycles Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces HOL-Algebra: theory HOL-Combinatorics.List_Permutation Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect HOL-Algebra: theory HOL-Algebra.Lattice Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic Complex_Bounded_Operators: theory VectorSpace.SumSpaces Virtual_Substitution: theory Virtual_Substitution.MPolyExtension Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition Dirichlet_Series: theory HOL-Algebra.Ideal Virtual_Substitution: theory Virtual_Substitution.PolyAtoms Complex_Bounded_Operators: theory VectorSpace.VectorSpace Complex_Bounded_Operators: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Complex_Bounded_Operators: theory Jordan_Normal_Form.Show_Matrix HOL-Algebra: theory HOL-Algebra.Complete_Lattice Virtual_Substitution: theory Virtual_Substitution.QE Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Dirichlet_Series: theory HOL-Algebra.RingHom Virtual_Substitution: theory Virtual_Substitution.Debruijn Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting HOL-Algebra: theory HOL-Algebra.Group HOL-Algebra: theory HOL-Algebra.Galois_Connection Complex_Bounded_Operators: theory Jordan_Normal_Form.Column_Operations Dirichlet_Series: theory HOL-Algebra.UnivPoly Complex_Bounded_Operators: theory Polynomial_Interpolation.Missing_Polynomial Complex_Bounded_Operators: theory Jordan_Normal_Form.Determinant Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition Projective_Measurements: theory QHLProver.Complex_Matrix Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0 Complex_Bounded_Operators: theory Polynomial_Factorization.Order_Polynomial Complex_Bounded_Operators: theory Polynomial_Interpolation.Ring_Hom_Poly HOL-Algebra: theory HOL-Algebra.Bij HOL-Algebra: theory HOL-Algebra.Coset HOL-Algebra: theory HOL-Algebra.FiniteProduct Complex_Bounded_Operators: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Preparing Echelon_Form/document ... Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence HOL-Algebra: theory HOL-Algebra.Ring Virtual_Substitution: theory Virtual_Substitution.Optimizations Virtual_Substitution: theory Virtual_Substitution.Reindex Complex_Bounded_Operators: theory Jordan_Normal_Form.Determinant_Impl Virtual_Substitution: theory Virtual_Substitution.UniAtoms Finished Echelon_Form/document (0:00:06 elapsed time) Preparing Echelon_Form/outline ... Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product Projective_Measurements: theory QHLProver.Gates HOL-Algebra: theory HOL-Algebra.Group_Action HOL-Algebra: theory HOL-Algebra.Sylow HOL-Algebra: theory HOL-Algebra.Generated_Groups HOL-Algebra: theory HOL-Algebra.Divisibility Finished Echelon_Form/outline (0:00:03 elapsed time) Timing Echelon_Form (8 threads, 142.433s elapsed time, 857.651s cpu time, 54.947s GC time, factor 6.02) Finished Echelon_Form (0:03:55 elapsed time, 0:15:28 cpu time, factor 3.94) Building Hermite ... Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_VectorSpace Hermite: theory Hermite.Hermite HOL-Algebra: theory HOL-Algebra.Zassenhaus Complex_Bounded_Operators: theory Jordan_Normal_Form.Char_Poly HOL-Algebra: theory HOL-Algebra.Solvable_Groups HOL-Algebra: theory HOL-Algebra.Elementary_Groups Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect HOL-Algebra: theory HOL-Algebra.Sym_Groups Hermite: theory Hermite.Hermite_IArrays HOL-Algebra: theory HOL-Algebra.Exact_Sequence Complex_Bounded_Operators: theory Jordan_Normal_Form.Jordan_Normal_Form Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group HOL-Algebra: theory HOL-Algebra.Product_Groups Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0 HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups Virtual_Substitution: theory Virtual_Substitution.VSAlgos Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux Complex_Bounded_Operators: theory Jordan_Normal_Form.VS_Connect HOL-Algebra: theory HOL-Algebra.AbelCoset HOL-Algebra: theory HOL-Algebra.Module Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible HOL-Algebra: theory HOL-Algebra.Ideal Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Dirichlet_Series: theory HOL-Number_Theory.Residues Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function Projective_Measurements: theory Regular-Sets.Regular_Exp Projective_Measurements: theory Regular-Sets.NDerivative Projective_Measurements: theory Regular-Sets.Equivalence_Checking Projective_Measurements: theory Regular-Sets.Relation_Interpretation Projective_Measurements: theory Regular-Sets.Regexp_Method Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting Virtual_Substitution: theory Virtual_Substitution.DNF Virtual_Substitution: theory Virtual_Substitution.Heuristic Virtual_Substitution: theory Virtual_Substitution.LinearCase Virtual_Substitution: theory Virtual_Substitution.NegInfinity Virtual_Substitution: theory Virtual_Substitution.QuadraticCase Dirichlet_Series: theory HOL-Real_Asymp.Real_Asymp Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion Dirichlet_Series: theory HOL-Number_Theory.Pocklington HOL-Algebra: theory HOL-Algebra.Ideal_Product HOL-Algebra: theory HOL-Algebra.RingHom Virtual_Substitution: theory Virtual_Substitution.EliminateVariable Virtual_Substitution: theory Virtual_Substitution.Infinitesimals Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni Dirichlet_Series: theory HOL-Number_Theory.Gauss Virtual_Substitution: theory Virtual_Substitution.LuckyFind Projective_Measurements: theory Abstract-Rewriting.SN_Orders Virtual_Substitution: theory Virtual_Substitution.EqualityVS Preparing Hermite/document ... Projective_Measurements: theory Matrix.Ordered_Semiring HOL-Algebra: theory HOL-Algebra.QuotRing HOL-Algebra: theory HOL-Algebra.UnivPoly Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots Projective_Measurements: theory Matrix.Matrix_Legacy Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni Finished Hermite/document (0:00:03 elapsed time) Preparing Hermite/outline ... Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor Dirichlet_Series: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory Bernoulli.Bernoulli_FPS Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function Finished Hermite/outline (0:00:02 elapsed time) Timing Hermite (8 threads, 27.602s elapsed time, 109.626s cpu time, 2.053s GC time, factor 3.97) Finished Hermite (0:00:49 elapsed time, 0:02:31 cpu time, factor 3.03) Building Smith_Normal_Form ... Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product Virtual_Substitution: theory Virtual_Substitution.DNFUni Dirichlet_Series: theory Dirichlet_Series.Euler_Products Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF HOL-Algebra: theory HOL-Algebra.IntRing HOL-Algebra: theory HOL-Algebra.Weak_Morphisms Smith_Normal_Form: theory HOL-Eisbach.Eisbach Smith_Normal_Form: theory Deriving.Generator_Aux Smith_Normal_Form: theory Deriving.Derive_Manager Smith_Normal_Form: theory HOL-Number_Theory.Cong Smith_Normal_Form: theory HOL-Algebra.Congruence Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra HOL-Algebra: theory HOL-Algebra.Chinese_Remainder Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2 Virtual_Substitution: theory Virtual_Substitution.VSQuad Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements Virtual_Substitution: theory Virtual_Substitution.Exports Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List Preparing Stochastic_Matrices/document ... Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist Smith_Normal_Form: theory List-Index.List_Index Finished Stochastic_Matrices/document (0:00:03 elapsed time) Preparing Stochastic_Matrices/outline ... Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau Projective_Measurements: theory Projective_Measurements.Projective_Measurements Finished Stochastic_Matrices/outline (0:00:02 elapsed time) Complex_Bounded_Operators: theory Jordan_Normal_Form.Gram_Schmidt Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_Kernel Timing Stochastic_Matrices (8 threads, 209.372s elapsed time, 1140.413s cpu time, 87.853s GC time, factor 5.45) Finished Stochastic_Matrices (0:05:12 elapsed time, 0:19:07 cpu time, factor 3.67) Building HOL-Number_Theory ... Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom Dirichlet_Series: theory Dirichlet_Series.More_Totient Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form Smith_Normal_Form: theory HOL-Algebra.Order Dirichlet_Series: theory Dirichlet_Series.Divisor_Count Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith Smith_Normal_Form: theory Show.Show Smith_Normal_Form: theory HOL-Number_Theory.Totient HOL-Number_Theory: theory HOL-Algebra.Congruence HOL-Number_Theory: theory HOL-Number_Theory.Cong HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers HOL-Number_Theory: theory HOL-Number_Theory.Fib Projective_Measurements: theory Projective_Measurements.CHSH_Inequality Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory Virtual_Substitution: theory Virtual_Substitution.ExportProofs Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code Complex_Bounded_Operators: theory Jordan_Normal_Form.Schur_Decomposition Dirichlet_Series: theory Dirichlet_Series.Partial_Summation Smith_Normal_Form: theory Subresultants.Binary_Exponentiation Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial Smith_Normal_Form: theory VectorSpace.FunctionLemmas Smith_Normal_Form: theory HOL-Algebra.Lattice HOL-Number_Theory: theory HOL-Algebra.Order HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp HOL-Number_Theory: theory HOL-Number_Theory.Totient Smith_Normal_Form: theory Show.Show_Instances Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis HOL-Number_Theory: theory HOL-Algebra.Lattice Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form Complex_Bounded_Operators: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence HOL-Algebra: theory HOL-Algebra.Multiplicative_Group Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized HOL-Number_Theory: theory HOL-Algebra.Group Smith_Normal_Form: theory Show.Show_Poly Smith_Normal_Form: theory HOL-Algebra.Group Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly HOL-Algebra: theory HOL-Algebra.Ring_Divisibility HOL-Algebra: theory HOL-Algebra.Subrings HOL-Number_Theory: theory HOL-Algebra.Coset HOL-Number_Theory: theory HOL-Algebra.FiniteProduct HOL-Number_Theory: theory HOL-Algebra.Ring Smith_Normal_Form: theory HOL-Algebra.Coset Smith_Normal_Form: theory HOL-Algebra.FiniteProduct HOL-Algebra: theory HOL-Algebra.Embedded_Algebras HOL-Algebra: theory HOL-Algebra.Generated_Rings HOL-Number_Theory: theory HOL-Algebra.Generated_Groups HOL-Algebra: theory HOL-Algebra.Generated_Fields Smith_Normal_Form: theory HOL-Algebra.Ring HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups Smith_Normal_Form: theory HOL-Algebra.Generated_Groups Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups HOL-Number_Theory: theory HOL-Algebra.AbelCoset HOL-Number_Theory: theory HOL-Algebra.Module Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics Smith_Normal_Form: theory HOL-Algebra.AbelCoset Smith_Normal_Form: theory HOL-Algebra.Module Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring HOL-Algebra: theory HOL-Algebra.Polynomials HOL-Number_Theory: theory HOL-Algebra.Ideal Smith_Normal_Form: theory VectorSpace.RingModuleFacts Smith_Normal_Form: theory VectorSpace.MonoidSums HOL-Number_Theory: theory HOL-Algebra.RingHom Smith_Normal_Form: theory VectorSpace.LinearCombinations HOL-Number_Theory: theory HOL-Algebra.UnivPoly Smith_Normal_Form: theory HOL-Algebra.Ideal Complex_Bounded_Operators: theory Containers.RBT_ext Complex_Bounded_Operators: theory Deriving.RBT_Comparator_Impl Smith_Normal_Form: theory Jordan_Normal_Form.Matrix Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix Smith_Normal_Form: theory HOL-Algebra.RingHom HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility HOL-Number_Theory: theory HOL-Number_Theory.Residues Smith_Normal_Form: theory HOL-Algebra.UnivPoly HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion HOL-Number_Theory: theory HOL-Number_Theory.Pocklington Smith_Normal_Form: theory VectorSpace.SumSpaces HOL-Number_Theory: theory HOL-Number_Theory.Gauss HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity Smith_Normal_Form: theory VectorSpace.VectorSpace Complex_Bounded_Operators: theory Containers.RBT_Mapping2 Complex_Bounded_Operators: theory Containers.RBT_Set2 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory HOL-Algebra: theory HOL-Algebra.Finite_Extensions HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix Complex_Bounded_Operators: theory Containers.Set_Impl Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations HOL-Algebra: theory HOL-Algebra.Algebraic_Closure Smith_Normal_Form: theory Jordan_Normal_Form.Determinant HOL-Algebra: theory HOL-Algebra.Algebra Preparing Virtual_Substitution/document ... Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group Smith_Normal_Form: theory HOL-Number_Theory.Residues Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_IArray_Impl Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition Complex_Bounded_Operators: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_Impl Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps Preparing HOL-Number_Theory/document ... Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified Finished HOL-Number_Theory/document (0:00:06 elapsed time) Preparing HOL-Number_Theory/outline ... Finished HOL-Number_Theory/outline (0:00:04 elapsed time) Timing HOL-Number_Theory (8 threads, 56.429s elapsed time, 309.004s cpu time, 22.390s GC time, factor 5.48) Finished HOL-Number_Theory (0:02:05 elapsed time, 0:06:25 cpu time, factor 3.06) Running HOL-ex ... HOL-ex: theory HOL-ex.Quicksort HOL-ex: theory HOL-ex.Bubblesort HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples HOL-ex: theory HOL-Combinatorics.Transposition HOL-ex: theory HOL-ex.MergeSort HOL-ex: theory HOL-ex.IArray_Examples HOL-ex: theory HOL-ex.Datatype_Record_Examples HOL-ex: theory HOL-Combinatorics.Perm HOL-ex: theory HOL-ex.Code_Lazy_Demo HOL-ex: theory HOL-ex.Refute_Examples HOL-ex: theory HOL-ex.Radix_Sort HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex HOL-ex: theory HOL-ex.While_Combinator_Example HOL-ex: theory HOL-ex.Code_Timing HOL-ex: theory HOL-ex.Antiquote HOL-ex: theory HOL-ex.Arith_Examples HOL-ex: theory HOL-ex.Specifications_with_bundle_mixins HOL-ex: theory HOL-ex.Perm_Fragments HOL-ex: theory HOL-ex.Birthday_Paradox HOL-ex: theory HOL-ex.CTL HOL-ex: theory HOL-ex.Cartouche_Examples HOL-ex: theory HOL-ex.Case_Product HOL-ex: theory HOL-ex.Chinese HOL-ex: theory HOL-ex.Classical HOL-ex: theory HOL-ex.Coercion_Examples HOL-ex: theory HOL-ex.Computations HOL-ex: theory HOL-ex.Erdoes_Szekeres HOL-ex: theory HOL-ex.Executable_Relation HOL-ex: theory HOL-ex.Execute_Choice HOL-ex: theory HOL-ex.Hebrew HOL-ex: theory HOL-ex.Hex_Bin_Examples HOL-ex: theory HOL-ex.Intuitionistic HOL-ex: theory HOL-ex.Join_Theory HOL-ex: theory HOL-ex.Lagrange HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples HOL-ex: theory HOL-ex.LocaleTest2 HOL-ex: theory HOL-ex.MonoidGroup HOL-ex: theory HOL-ex.Multiquote HOL-ex: theory HOL-ex.NatSum HOL-ex: theory HOL-ex.PER HOL-ex: theory HOL-ex.Peano_Axioms HOL-ex: theory HOL-ex.PresburgerEx HOL-ex: theory HOL-ex.Residue_Ring HOL-ex: theory HOL-ex.Serbian HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples HOL-ex: theory HOL-ex.Set_Theory HOL-ex: theory HOL-ex.Simproc_Tests HOL-ex: theory HOL-ex.Sketch_and_Explore HOL-ex: theory HOL-ex.Sorting_Algorithms_Examples HOL-ex: theory HOL-ex.Sudoku HOL-ex: theory HOL-ex.Tarski HOL-ex: theory HOL-ex.Termination HOL-ex: theory HOL-ex.ThreeDivides HOL-ex: theory HOL-ex.Transfer_Int_Nat HOL-ex: theory HOL-ex.Tree23 HOL-ex: theory HOL-ex.Unification HOL-ex: theory HOL-ex.veriT_Preprocessing HOL-ex: theory HOL-ex.Transfer_Debug HOL-ex: theory HOL-ex.Function_Growth HOL-ex: theory HOL-ex.SOS HOL-ex: theory HOL-ex.SOS_Cert HOL-ex: theory HOL-ex.Argo_Examples HOL-ex: theory HOL-ex.Ballot HOL-ex: theory HOL-ex.BinEx HOL-ex: theory HOL-ex.Code_Binary_Nat_examples HOL-ex: theory HOL-ex.Cubic_Quartic Preparing HOL-Algebra/document ... HOL-ex: theory HOL-ex.Eval_Examples HOL-ex: theory HOL-ex.Gauge_Integration Finished Virtual_Substitution/document (0:00:54 elapsed time) Preparing Virtual_Substitution/outline ... HOL-ex: theory HOL-ex.HarmonicSeries HOL-ex: theory HOL-ex.Normalization_by_Evaluation HOL-ex: theory HOL-ex.Parallel_Example HOL-ex: theory HOL-ex.Pythagoras HOL-ex: theory HOL-ex.Reflection_Examples HOL-ex: theory HOL-ex.Sqrt_Script HOL-ex: theory HOL-ex.Triangular_Numbers Preparing Projective_Measurements/document ... Preparing Dirichlet_Series/document ... Finished Virtual_Substitution/outline (0:00:16 elapsed time) Timing Virtual_Substitution (8 threads, 415.655s elapsed time, 1192.381s cpu time, 109.512s GC time, factor 2.87) Finished Virtual_Substitution (0:06:59 elapsed time, 0:19:55 cpu time, factor 2.85) Running Irrational_Series_Erdos_Straus ... Finished Projective_Measurements/document (0:00:06 elapsed time) Preparing Projective_Measurements/outline ... Finished Projective_Measurements/outline (0:00:02 elapsed time) Irrational_Series_Erdos_Straus: theory HOL-Eisbach.Eisbach Irrational_Series_Erdos_Straus: theory Pure-ex.Guess Irrational_Series_Erdos_Straus: theory HOL-Combinatorics.Stirling Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Fraction_Field Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Group_Closure Irrational_Series_Erdos_Straus: theory HOL-Library.BNF_Corec Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Nth_Powers Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Squarefree Timing Projective_Measurements (8 threads, 248.054s elapsed time, 1386.228s cpu time, 98.979s GC time, factor 5.59) Finished Projective_Measurements (0:08:04 elapsed time, 0:26:04 cpu time, factor 3.23) Running PAC_Checker ... Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Cong Irrational_Series_Erdos_Straus: theory HOL-Algebra.Congruence Irrational_Series_Erdos_Straus: theory HOL-Library.Function_Algebras Irrational_Series_Erdos_Straus: theory HOL-Library.More_List Irrational_Series_Erdos_Straus: theory HOL-Library.Power_By_Squaring Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Eratosthenes Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Inst_Existentials Irrational_Series_Erdos_Straus: theory Bernoulli.Bernoulli Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Field_as_Ring Irrational_Series_Erdos_Straus: theory HOL-Eisbach.Eisbach_Tools Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Polynomial Irrational_Series_Erdos_Straus: theory HOL-Library.Going_To_Filter Irrational_Series_Erdos_Straus: theory HOL-Library.Landau_Symbols Irrational_Series_Erdos_Straus: theory Bernoulli.Periodic_Bernpoly Irrational_Series_Erdos_Straus: theory HOL-Algebra.Order Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Normalized_Fraction Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Missing_Topology Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Mod_Exp Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Contour_Integration Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Fib PAC_Checker: theory Deriving.Derive_Manager PAC_Checker: theory Deriving.Generator_Aux PAC_Checker: theory HOL-Library.Multiset_Order PAC_Checker: theory HOL-Library.Conditional_Parametricity PAC_Checker: theory HOL-Combinatorics.Transposition PAC_Checker: theory HOL-Library.FuncSet PAC_Checker: theory HOL-Library.Fun_Lexorder PAC_Checker: theory HOL-Library.Function_Algebras Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Prime_Powers PAC_Checker: theory HOL-Library.Groups_Big_Fun PAC_Checker: theory Abstract-Rewriting.Seq Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Totient PAC_Checker: theory HOL-Library.More_List Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Eventuallize PAC_Checker: theory HOL-Library.Sublist Irrational_Series_Erdos_Straus: theory HOL-Algebra.Lattice Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Lazy_Eval PAC_Checker: theory HOL-Library.Countable_Set PAC_Checker: theory HOL-Library.FSet Finished Dirichlet_Series/document (0:00:12 elapsed time) Preparing Dirichlet_Series/outline ... PAC_Checker: theory Polynomials.More_Modules PAC_Checker: theory Open_Induction.Restricted_Predicates PAC_Checker: theory HOL-Library.Poly_Mapping Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem PAC_Checker: theory PAC_Checker.PAC_Misc Irrational_Series_Erdos_Straus: theory Landau_Symbols.Group_Sort PAC_Checker: theory PAC_Checker.PAC_Version PAC_Checker: theory HOL-Algebra.Congruence PAC_Checker: theory HOL-Library.Disjoint_Sets PAC_Checker: theory HOL-Library.Ramsey PAC_Checker: theory PAC_Checker.More_Loops PAC_Checker: theory HOL-Combinatorics.Permutations PAC_Checker: theory Regular-Sets.Regular_Set Irrational_Series_Erdos_Straus: theory HOL-Algebra.Complete_Lattice PAC_Checker: theory Show.Show Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Winding_Numbers PAC_Checker: theory Well_Quasi_Orders.Infinite_Sequences PAC_Checker: theory Well_Quasi_Orders.Minimal_Elements Finished HOL-Algebra/document (0:00:32 elapsed time) Preparing HOL-Algebra/outline ... PAC_Checker: theory HOL-Algebra.Order PAC_Checker: theory Well_Quasi_Orders.Least_Enum PAC_Checker: theory Native_Word.Uint64 Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Cauchy_Integral_Formula Irrational_Series_Erdos_Straus: theory HOL-Algebra.Group Irrational_Series_Erdos_Straus: theory Landau_Symbols.Landau_Real_Products Finished Dirichlet_Series/outline (0:00:07 elapsed time) PAC_Checker: theory HOL-Combinatorics.List_Permutation PAC_Checker: theory Show.Show_Instances Timing Dirichlet_Series (8 threads, 108.077s elapsed time, 733.272s cpu time, 67.410s GC time, factor 6.78) Finished Dirichlet_Series (0:08:07 elapsed time, 0:14:29 cpu time, factor 1.78) Building E_Transcendental ... PAC_Checker: theory Polynomials.MPoly_Type PAC_Checker: theory Nested_Multisets_Ordinals.Multiset_More PAC_Checker: theory HOL-Algebra.Lattice PAC_Checker: theory Polynomials.More_MPoly_Type PAC_Checker: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset PAC_Checker: theory PAC_Checker.WB_Sort PAC_Checker: theory HOL-Algebra.Complete_Lattice E_Transcendental: theory HOL-Number_Theory.Cong E_Transcendental: theory HOL-Algebra.Congruence E_Transcendental: theory HOL-Library.More_List E_Transcendental: theory HOL-Library.Power_By_Squaring E_Transcendental: theory HOL-Number_Theory.Eratosthenes E_Transcendental: theory HOL-Number_Theory.Fib E_Transcendental: theory HOL-Number_Theory.Prime_Powers E_Transcendental: theory HOL-Computational_Algebra.Polynomial PAC_Checker: theory HOL-Library.Finite_Map E_Transcendental: theory HOL-Algebra.Order PAC_Checker: theory HOL-Algebra.Group E_Transcendental: theory HOL-Number_Theory.Mod_Exp E_Transcendental: theory HOL-Number_Theory.Totient Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Conformal_Mappings E_Transcendental: theory HOL-Algebra.Lattice Finished HOL-Algebra/outline (0:00:16 elapsed time) PAC_Checker: theory HOL-Algebra.Coset PAC_Checker: theory HOL-Algebra.FiniteProduct E_Transcendental: theory HOL-Algebra.Complete_Lattice Timing HOL-Algebra (8 threads, 126.985s elapsed time, 652.016s cpu time, 91.181s GC time, factor 5.13) Finished HOL-Algebra (0:04:58 elapsed time, 0:12:57 cpu time, factor 2.61) Building Jordan_Normal_Form ... Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Complex_Singularities Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Great_Picard Irrational_Series_Erdos_Straus: theory HOL-Algebra.Coset PAC_Checker: theory HOL-Algebra.Ring E_Transcendental: theory HOL-Algebra.Group PAC_Checker: theory HOL-Algebra.Generated_Groups PAC_Checker: theory HOL-Algebra.Divisibility Irrational_Series_Erdos_Straus: theory HOL-Algebra.FiniteProduct Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Complex_Residues Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Residue_Theorem Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Riemann_Mapping PAC_Checker: theory HOL-Algebra.Elementary_Groups Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc E_Transcendental: theory HOL-Algebra.Coset E_Transcendental: theory HOL-Algebra.FiniteProduct Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring Irrational_Series_Erdos_Straus: theory HOL-Algebra.Ring E_Transcendental: theory HOL-Algebra.Ring Irrational_Series_Erdos_Straus: theory HOL-Algebra.Generated_Groups PAC_Checker: theory HOL-Algebra.AbelCoset PAC_Checker: theory HOL-Algebra.Module E_Transcendental: theory HOL-Algebra.Generated_Groups PAC_Checker: theory HOL-Algebra.Ideal Irrational_Series_Erdos_Straus: theory HOL-Complex_Analysis.Complex_Analysis Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Multiseries_Expansion Jordan_Normal_Form: theory Containers.Equal Jordan_Normal_Form: theory Containers.Extend_Partial_Order Jordan_Normal_Form: theory Containers.List_Fusion Jordan_Normal_Form: theory Deriving.Comparator Jordan_Normal_Form: theory Deriving.Derive_Manager Jordan_Normal_Form: theory Deriving.Generator_Aux Jordan_Normal_Form: theory Containers.Containers_Auxiliary Jordan_Normal_Form: theory Abstract-Rewriting.Seq Jordan_Normal_Form: theory Containers.Closure_Set E_Transcendental: theory HOL-Algebra.Elementary_Groups PAC_Checker: theory HOL-Algebra.RingHom Irrational_Series_Erdos_Straus: theory Landau_Symbols.Landau_Simprocs Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Missing_Analysis Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom PAC_Checker: theory HOL-Algebra.QuotRing PAC_Checker: theory HOL-Algebra.UnivPoly Jordan_Normal_Form: theory Deriving.Equality_Generator Jordan_Normal_Form: theory Containers.Containers_Generator E_Transcendental: theory HOL-Algebra.AbelCoset E_Transcendental: theory HOL-Algebra.Module Jordan_Normal_Form: theory Regular-Sets.Regular_Set Irrational_Series_Erdos_Straus: theory HOL-Algebra.Elementary_Groups Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Polynomial_FPS Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Polynomial_Factorial Irrational_Series_Erdos_Straus: theory Landau_Symbols.Landau_More Jordan_Normal_Form: theory Containers.Collection_Enum PAC_Checker: theory Regular-Sets.Regular_Exp Irrational_Series_Erdos_Straus: theory Stirling_Formula.Stirling_Formula Jordan_Normal_Form: theory Deriving.Equality_Instances Jordan_Normal_Form: theory Deriving.Compare Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Formal_Laurent_Series Jordan_Normal_Form: theory Deriving.Comparator_Generator E_Transcendental: theory HOL-Algebra.Ideal Jordan_Normal_Form: theory Containers.Lexicographic_Order Jordan_Normal_Form: theory Containers.Collection_Eq Jordan_Normal_Form: theory Containers.Set_Linorder PAC_Checker: theory Regular-Sets.NDerivative PAC_Checker: theory Regular-Sets.Relation_Interpretation Jordan_Normal_Form: theory Containers.RBT_ext PAC_Checker: theory Regular-Sets.Equivalence_Checking PAC_Checker: theory Regular-Sets.Regexp_Method Jordan_Normal_Form: theory Deriving.Compare_Generator Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl Jordan_Normal_Form: theory Containers.DList_Set E_Transcendental: theory HOL-Algebra.RingHom PAC_Checker: theory Well_Quasi_Orders.Almost_Full Jordan_Normal_Form: theory Deriving.Compare_Instances E_Transcendental: theory HOL-Algebra.UnivPoly PAC_Checker: theory Well_Quasi_Orders.Minimal_Bad_Sequences PAC_Checker: theory Well_Quasi_Orders.Almost_Full_Relations Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial PAC_Checker: theory Polynomials.Utils Jordan_Normal_Form: theory Show.Show PAC_Checker: theory Well_Quasi_Orders.Well_Quasi_Orders Irrational_Series_Erdos_Straus: theory HOL-Algebra.AbelCoset Irrational_Series_Erdos_Straus: theory HOL-Algebra.Module PAC_Checker: theory Polynomials.Power_Products PAC_Checker: theory HOL-Algebra.Multiplicative_Group Jordan_Normal_Form: theory VectorSpace.FunctionLemmas Jordan_Normal_Form: theory VectorSpace.RingModuleFacts PAC_Checker: theory HOL-Algebra.Ring_Divisibility PAC_Checker: theory HOL-Algebra.Subrings Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial Jordan_Normal_Form: theory Show.Show_Instances Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly Jordan_Normal_Form: theory VectorSpace.MonoidSums Jordan_Normal_Form: theory VectorSpace.LinearCombinations E_Transcendental: theory HOL-Algebra.Multiplicative_Group HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton Irrational_Series_Erdos_Straus: theory HOL-Algebra.Ideal PAC_Checker: theory HOL-Algebra.Polynomials E_Transcendental: theory HOL-Number_Theory.Residues E_Transcendental: theory HOL-Number_Theory.Euler_Criterion PAC_Checker: theory Polynomials.MPoly_Type_Class E_Transcendental: theory HOL-Number_Theory.Gauss E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity E_Transcendental: theory HOL-Number_Theory.Pocklington HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml Irrational_Series_Erdos_Straus: theory HOL-Algebra.RingHom HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots Irrational_Series_Erdos_Straus: theory HOL-Algebra.UnivPoly E_Transcendental: theory HOL-Number_Theory.Number_Theory Timing HOL-Codegenerator_Test (8 threads, 569.622s elapsed time, 1080.206s cpu time, 63.152s GC time, factor 1.90) Finished HOL-Codegenerator_Test (0:09:33 elapsed time, 0:18:03 cpu time, factor 1.89) Building Groebner_Bases ... Irrational_Series_Erdos_Straus: theory HOL-Computational_Algebra.Computational_Algebra Irrational_Series_Erdos_Straus: theory Sturm_Tarski.PolyMisc E_Transcendental: theory E_Transcendental.E_Transcendental Irrational_Series_Erdos_Straus: theory Sturm_Tarski.Sturm_Tarski Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Preparing Complex_Bounded_Operators/document ... Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix Jordan_Normal_Form: theory VectorSpace.SumSpaces Irrational_Series_Erdos_Straus: theory Budan_Fourier.BF_Misc Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations Jordan_Normal_Form: theory VectorSpace.VectorSpace Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant PAC_Checker: theory PAC_Checker.PAC_More_Poly Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code Groebner_Bases: theory Containers.Equal Groebner_Bases: theory Containers.List_Fusion Groebner_Bases: theory Containers.Extend_Partial_Order Groebner_Bases: theory Deriving.Comparator Groebner_Bases: theory Deriving.Derive_Manager Groebner_Bases: theory Deriving.Generator_Aux Groebner_Bases: theory Containers.Containers_Auxiliary Groebner_Bases: theory Jordan_Normal_Form.Missing_Misc Groebner_Bases: theory Containers.Closure_Set Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Missing_Algebraic Groebner_Bases: theory Abstract-Rewriting.Seq Jordan_Normal_Form: theory Containers.Collection_Order Groebner_Bases: theory Polynomials.MPoly_Type PAC_Checker: theory PAC_Checker.PAC_Specification Groebner_Bases: theory Jordan_Normal_Form.Missing_Ring Groebner_Bases: theory Polynomials.More_Modules Groebner_Bases: theory Deriving.Equality_Generator Groebner_Bases: theory Containers.Containers_Generator Groebner_Bases: theory Polynomial_Interpolation.Missing_Unsorted Groebner_Bases: theory Groebner_Bases.Code_Target_Rat Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly Groebner_Bases: theory Polynomials.More_MPoly_Type Groebner_Bases: theory Deriving.Equality_Instances Groebner_Bases: theory Jordan_Normal_Form.Conjugate Groebner_Bases: theory Containers.Collection_Enum Groebner_Bases: theory Containers.Collection_Eq Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Missing_Transcendental Groebner_Bases: theory Deriving.Compare Groebner_Bases: theory Polynomials.OAlist Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Cauchy_Index_Theorem Groebner_Bases: theory Deriving.Comparator_Generator Jordan_Normal_Form: theory Containers.RBT_Mapping2 Groebner_Bases: theory Containers.Lexicographic_Order Groebner_Bases: theory Containers.DList_Set Groebner_Bases: theory Containers.RBT_ext Groebner_Bases: theory Containers.Set_Linorder Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace Jordan_Normal_Form: theory Containers.RBT_Set2 Groebner_Bases: theory Deriving.Compare_Generator Groebner_Bases: theory Deriving.RBT_Comparator_Impl Groebner_Bases: theory Deriving.Compare_Instances Groebner_Bases: theory Open_Induction.Restricted_Predicates Irrational_Series_Erdos_Straus: theory Winding_Number_Eval.Winding_Number_Eval Groebner_Bases: theory Polynomial_Interpolation.Ring_Hom Groebner_Bases: theory Regular-Sets.Regular_Set Jordan_Normal_Form: theory Containers.Set_Impl Jordan_Normal_Form: theory Regular-Sets.Regular_Exp Groebner_Bases: theory Well_Quasi_Orders.Infinite_Sequences Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect Groebner_Bases: theory Well_Quasi_Orders.Minimal_Elements Groebner_Bases: theory Well_Quasi_Orders.Least_Enum Jordan_Normal_Form: theory Regular-Sets.NDerivative Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking Jordan_Normal_Form: theory Regular-Sets.Regexp_Method Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting Groebner_Bases: theory Jordan_Normal_Form.Matrix Irrational_Series_Erdos_Straus: theory HOL-Algebra.Multiplicative_Group Preparing E_Transcendental/document ... Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound Finished Complex_Bounded_Operators/document (0:00:38 elapsed time) Preparing Complex_Bounded_Operators/outline ... Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Residues Finished E_Transcendental/document (0:00:03 elapsed time) Preparing E_Transcendental/outline ... Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier Jordan_Normal_Form: theory Matrix.Ordered_Semiring Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition PAC_Checker: theory PAC_Checker.Finite_Map_Multiset Finished E_Transcendental/outline (0:00:02 elapsed time) Timing E_Transcendental (8 threads, 60.384s elapsed time, 371.949s cpu time, 27.494s GC time, factor 6.16) Finished E_Transcendental (0:01:38 elapsed time, 0:07:20 cpu time, factor 4.48) Running HOL-Decision_Procs ... PAC_Checker: theory PAC_Checker.PAC_Polynomials PAC_Checker: theory PAC_Checker.PAC_Checker_Specification PAC_Checker: theory PAC_Checker.PAC_Map_Rel Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Groebner_Bases: theory Containers.Collection_Order Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds PAC_Checker: theory PAC_Checker.PAC_Polynomials_Term PAC_Checker: theory PAC_Checker.PAC_Assoc_Map_Rel Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Euler_Criterion Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Pocklington Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Gauss Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Quadratic_Reciprocity Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Residue_Primitive_Roots Groebner_Bases: theory Containers.RBT_Mapping2 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair Groebner_Bases: theory Containers.RBT_Set2 PAC_Checker: theory PAC_Checker.PAC_Polynomials_Operations Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius Finished Complex_Bounded_Operators/outline (0:00:15 elapsed time) Irrational_Series_Erdos_Straus: theory HOL-Real_Asymp.Real_Asymp Timing Complex_Bounded_Operators (8 threads, 378.747s elapsed time, 2538.275s cpu time, 243.488s GC time, factor 6.70) Finished Complex_Bounded_Operators (0:09:30 elapsed time, 0:47:10 cpu time, factor 4.96) Building Count_Complex_Roots ... Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl Irrational_Series_Erdos_Straus: theory HOL-Number_Theory.Number_Theory Groebner_Bases: theory Containers.Set_Impl HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring Count_Complex_Roots: theory HOL-Eisbach.Eisbach Count_Complex_Roots: theory HOL-Library.More_List Count_Complex_Roots: theory Polynomial_Interpolation.Missing_Unsorted Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom PAC_Checker: theory PAC_Checker.PAC_Checker Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial Irrational_Series_Erdos_Straus: theory Bernoulli.Bernoulli_FPS Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Dirichlet_Misc HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Multiplicative_Function HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack HOL-Decision_Procs: theory HOL-Decision_Procs.MIR HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Dirichlet_Product Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Euler_Products Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Dirichlet_Series Irrational_Series_Erdos_Straus: theory Bernoulli.Bernoulli_Zeta Irrational_Series_Erdos_Straus: theory Euler_MacLaurin.Euler_MacLaurin HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Moebius_Mu HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete PAC_Checker: theory PAC_Checker.PAC_Checker_Relation Irrational_Series_Erdos_Straus: theory Dirichlet_Series.More_Totient Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Liouville_Lambda Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Divisor_Count PAC_Checker: theory PAC_Checker.PAC_Checker_Init HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Primes_Omega Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Arithmetic_Summatory HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex Irrational_Series_Erdos_Straus: theory Euler_MacLaurin.Euler_MacLaurin_Landau Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Partial_Summation Groebner_Bases: theory Jordan_Normal_Form.Matrix_IArray_Impl Groebner_Bases: theory Regular-Sets.Regular_Exp HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Dirichlet_Series_Analysis Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Groebner_Bases: theory Regular-Sets.NDerivative Groebner_Bases: theory Regular-Sets.Relation_Interpretation Groebner_Bases: theory Regular-Sets.Equivalence_Checking Groebner_Bases: theory Regular-Sets.Regexp_Method Groebner_Bases: theory Abstract-Rewriting.Abstract_Rewriting Groebner_Bases: theory Well_Quasi_Orders.Almost_Full PAC_Checker: theory PAC_Checker.PAC_Checker_Synthesis Groebner_Bases: theory Well_Quasi_Orders.Minimal_Bad_Sequences Groebner_Bases: theory Groebner_Bases.Confluence Groebner_Bases: theory Well_Quasi_Orders.Almost_Full_Relations Groebner_Bases: theory Polynomials.Utils Groebner_Bases: theory Well_Quasi_Orders.Well_Quasi_Orders Groebner_Bases: theory Groebner_Bases.General Groebner_Bases: theory Polynomials.Power_Products Irrational_Series_Erdos_Straus: theory Zeta_Function.Zeta_Library Irrational_Series_Erdos_Straus: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics Irrational_Series_Erdos_Straus: theory Zeta_Function.Zeta_Function Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial Count_Complex_Roots: theory Polynomial_Interpolation.Missing_Polynomial Count_Complex_Roots: theory Sturm_Tarski.PolyMisc Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Groebner_Bases: theory Polynomials.MPoly_Type_Class Groebner_Bases: theory Polynomials.PP_Type Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom_Poly PAC_Checker: theory PAC_Checker.PAC_Checker_MLton HOL-ex: theory HOL-ex.Meson_Test HOL-ex: theory HOL-ex.SAT_Examples Count_Complex_Roots: theory Budan_Fourier.BF_Misc HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex Preparing Smith_Normal_Form/document ... Count_Complex_Roots: theory Budan_Fourier.Sturm_Multiple_Roots Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Counting_Functions Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental Groebner_Bases: theory Polynomials.MPoly_Type_Class_Ordered Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem Count_Complex_Roots: theory Count_Complex_Roots.CC_Polynomials_Extra Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Lcm_Nat_Upto Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Mertens_Theorems Finished Smith_Normal_Form/document (0:00:14 elapsed time) Preparing Smith_Normal_Form/outline ... Preparing PAC_Checker/document ... Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.More_Dirichlet_Misc Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Primorial Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Shapiro_Tauberian Finished Smith_Normal_Form/outline (0:00:05 elapsed time) Groebner_Bases: theory Groebner_Bases.More_MPoly_Type_Class Groebner_Bases: theory Polynomials.OAlist_Poly_Mapping Groebner_Bases: theory Polynomials.Quasi_PM_Power_Products Groebner_Bases: theory Groebner_Bases.Reduction Timing Smith_Normal_Form (8 threads, 319.283s elapsed time, 1876.374s cpu time, 135.997s GC time, factor 5.88) Finished Smith_Normal_Form (0:06:41 elapsed time, 0:34:37 cpu time, factor 5.18) Running Modular_arithmetic_LLL_and_HNF_algorithms ... Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.Moebius_Mu_Sum Latex error (line 24 of "PAC_Checker_MLton.tex"): Undefined control sequence. ...\isacharparenleft}{\kern0pt}\isactrlverbatim Failed to build document "document" PAC_Checker FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/PAC_Checker) ./PAC_Checker_MLton.tex:45: Undefined control sequence. l.45 ...\isacharparenleft}{\kern0pt}\isactrlverbatim {\isasymopen}{\isachardou... )) No file root.bbl. [191] (./root.aux) Package rerunfilecheck Warning: File `root.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Warning: There were undefined references. ) (see the transcript file for additional information) 720 words of node memory still in use: 6 hlist, 2 vlist, 2 rule, 2 glue, 4 kern, 1 glyph, 13 attribute, 95 glue_spe c, 8 attribute_list, 2 write nodes avail lists: 1:5,2:4565,3:81,4:26,5:973,6:57,7:4113,8:35,9:648,10:9,11:212 {/usr/share/texmf/fonts/enc/dvips/lm/lm-ec.enc}{/usr/share/texmf/fonts/enc/dvip s/lm/lm-ts1.enc} Output written on root.pdf (191 pages, 1032624 bytes). Transcript written on root.log. *** Latex error (line 24 of "PAC_Checker_MLton.tex"): *** Undefined control sequence. *** ...\isacharparenleft}{\kern0pt}\isactrlverbatim *** Failed to build document "document" Building Bernoulli ... Count_Complex_Roots: theory Count_Complex_Roots.Count_Line Irrational_Series_Erdos_Straus: theory Prime_Distribution_Elementary.PNT_Consequences Bernoulli: theory HOL-Combinatorics.Stirling Bernoulli: theory HOL-Computational_Algebra.Fraction_Field Bernoulli: theory HOL-Computational_Algebra.Group_Closure Bernoulli: theory HOL-Computational_Algebra.Nth_Powers Bernoulli: theory HOL-Algebra.Congruence Bernoulli: theory HOL-Computational_Algebra.Squarefree Bernoulli: theory HOL-Number_Theory.Cong Bernoulli: theory HOL-Library.More_List Groebner_Bases: theory Groebner_Bases.Macaulay_Matrix Count_Complex_Roots: theory Count_Complex_Roots.Count_Half_Plane Count_Complex_Roots: theory Count_Complex_Roots.Count_Circle Count_Complex_Roots: theory Count_Complex_Roots.Count_Rectangle Bernoulli: theory HOL-Library.Power_By_Squaring Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples Bernoulli: theory HOL-Number_Theory.Eratosthenes Bernoulli: theory Bernoulli.Bernoulli Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set Bernoulli: theory HOL-Computational_Algebra.Polynomial Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray Bernoulli: theory HOL-Number_Theory.Fib Bernoulli: theory HOL-Number_Theory.Prime_Powers Bernoulli: theory Bernoulli.Periodic_Bernpoly Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based Bernoulli: theory HOL-Algebra.Order Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus Groebner_Bases: theory Polynomials.MPoly_PM Bernoulli: theory HOL-Computational_Algebra.Normalized_Fraction Bernoulli: theory HOL-Number_Theory.Mod_Exp Bernoulli: theory HOL-Number_Theory.Totient Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping Bernoulli: theory HOL-Algebra.Lattice Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder Bernoulli: theory HOL-Algebra.Complete_Lattice Timing HOL-ex (8 threads, 295.563s elapsed time, 1340.707s cpu time, 107.456s GC time, factor 4.54) Finished HOL-ex (0:05:00 elapsed time, 0:22:25 cpu time, factor 4.48) Running Transcendence_Series_Hancl_Rucki ... Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fraction_Field Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach Transcendence_Series_Hancl_Rucki: theory Pure-ex.Guess Transcendence_Series_Hancl_Rucki: theory HOL-Combinatorics.Stirling Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Group_Closure Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Nth_Powers Transcendence_Series_Hancl_Rucki: theory HOL-Library.BNF_Corec Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Squarefree Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set Bernoulli: theory HOL-Algebra.Group Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Cong Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator Groebner_Bases: theory Groebner_Bases.Auto_Reduction Groebner_Bases: theory Groebner_Bases.Groebner_Bases Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Divisibility Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Congruence Bernoulli: theory HOL-Algebra.Coset Bernoulli: theory HOL-Algebra.FiniteProduct Transcendence_Series_Hancl_Rucki: theory HOL-Library.More_List Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility Bernoulli: theory HOL-Algebra.Ring Groebner_Bases: theory Polynomials.Term_Order Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma Transcendence_Series_Hancl_Rucki: theory HOL-Library.Power_By_Squaring Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian Bernoulli: theory HOL-Algebra.Generated_Groups Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Eratosthenes Bernoulli: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Bernoulli: theory HOL-Computational_Algebra.Polynomial_FPS Bernoulli: theory HOL-Computational_Algebra.Polynomial_Factorial Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Inst_Existentials Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix Bernoulli: theory HOL-Algebra.Elementary_Groups Bernoulli: theory HOL-Computational_Algebra.Formal_Laurent_Series Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Field_as_Ring Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach_Tools Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset Transcendence_Series_Hancl_Rucki: theory HOL-Library.Going_To_Filter Transcendence_Series_Hancl_Rucki: theory Bernoulli.Periodic_Bernpoly Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Topology Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Order Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Normalized_Fraction Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Analysis Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Fib Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Mod_Exp Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Prime_Powers Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Totient Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Eventuallize Bernoulli: theory HOL-Algebra.AbelCoset Bernoulli: theory HOL-Algebra.Module Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Lazy_Eval Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization Groebner_Bases: theory Polynomials.MPoly_Type_Class_OAlist Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Lattice Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension Bernoulli: theory HOL-Algebra.Ideal Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF Groebner_Bases: theory Groebner_Bases.Algorithm_Schema Groebner_Bases: theory Groebner_Bases.Reduced_GB Groebner_Bases: theory Groebner_Bases.Syzygy Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Complete_Lattice Bernoulli: theory HOL-Algebra.RingHom Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel Bernoulli: theory HOL-Algebra.UnivPoly Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Group Bernoulli: theory HOL-Computational_Algebra.Computational_Algebra Preparing Count_Complex_Roots/document ... Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly Finished Count_Complex_Roots/document (0:00:11 elapsed time) Preparing Count_Complex_Roots/outline ... Groebner_Bases: theory Groebner_Bases.Groebner_PM Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod Finished Count_Complex_Roots/outline (0:00:04 elapsed time) Bernoulli: theory HOL-Algebra.Multiplicative_Group Timing Count_Complex_Roots (8 threads, 70.133s elapsed time, 417.583s cpu time, 12.231s GC time, factor 5.95) Finished Count_Complex_Roots (0:03:25 elapsed time, 0:08:06 cpu time, factor 2.37) Building Zeta_Function ... Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Coset Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.FiniteProduct Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field Bernoulli: theory HOL-Number_Theory.Residues Zeta_Function: theory Bernoulli.Bernoulli_Zeta Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ring Bernoulli: theory HOL-Number_Theory.Euler_Criterion Bernoulli: theory HOL-Number_Theory.Gauss Bernoulli: theory HOL-Number_Theory.Quadratic_Reciprocity Bernoulli: theory HOL-Number_Theory.Pocklington Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based Bernoulli: theory HOL-Number_Theory.Residue_Primitive_Roots Zeta_Function: theory HOL-Eisbach.Eisbach Zeta_Function: theory Pure-ex.Guess Zeta_Function: theory Sturm_Tarski.PolyMisc Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring Zeta_Function: theory Winding_Number_Eval.Missing_Topology Zeta_Function: theory Winding_Number_Eval.Missing_Analysis Zeta_Function: theory Zeta_Function.Zeta_Library Bernoulli: theory HOL-Number_Theory.Number_Theory Bernoulli: theory Bernoulli.Bernoulli_FPS Groebner_Bases: theory Groebner_Bases.Benchmarks Bernoulli: theory Bernoulli.Bernoulli_Zeta Preparing Jordan_Normal_Form/document ... Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization Zeta_Function: theory HOL-Eisbach.Eisbach_Tools Timing HOL-Decision_Procs (8 threads, 261.714s elapsed time, 1401.107s cpu time, 145.315s GC time, factor 5.35) Finished HOL-Decision_Procs (0:04:28 elapsed time, 0:23:27 cpu time, factor 5.25) Building Pi_Transcendental ... Zeta_Function: theory Sturm_Tarski.Sturm_Tarski Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Multiseries_Expansion Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field Pi_Transcendental: theory HOL-Library.BNF_Corec Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree Pi_Transcendental: theory HOL-Library.Fun_Lexorder Pi_Transcendental: theory HOL-Library.Groups_Big_Fun Pi_Transcendental: theory HOL-Real_Asymp.Inst_Existentials Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Zeta_Function: theory Budan_Fourier.BF_Misc Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_FPS Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Generated_Groups Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_FPS Pi_Transcendental: theory HOL-Real_Asymp.Eventuallize Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic Pi_Transcendental: theory HOL-Real_Asymp.Lazy_Eval Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_Factorial Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem Pi_Transcendental: theory HOL-Library.Poly_Mapping Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Elementary_Groups Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT Finished Jordan_Normal_Form/document (0:00:29 elapsed time) Preparing Jordan_Normal_Form/outline ... Pi_Transcendental: theory HOL-Computational_Algebra.Formal_Laurent_Series Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Formal_Laurent_Series Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction Zeta_Function: theory Zeta_Function.Zeta_Function Finished Jordan_Normal_Form/outline (0:00:11 elapsed time) Timing Jordan_Normal_Form (8 threads, 268.548s elapsed time, 1590.152s cpu time, 143.683s GC time, factor 5.92) Finished Jordan_Normal_Form (0:05:47 elapsed time, 0:29:30 cpu time, factor 5.10) Building Subresultants ... Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.AbelCoset Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Module Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl Preparing Bernoulli/document ... Pi_Transcendental: theory Polynomials.MPoly_Type Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial Subresultants: theory Subresultants.Coeff_Int Subresultants: theory Subresultants.Dichotomous_Lazard Subresultants: theory Subresultants.More_Homomorphisms Subresultants: theory Subresultants.Resultant_Prelim Subresultants: theory Subresultants.Binary_Exponentiation Finished Bernoulli/document (0:00:05 elapsed time) Preparing Bernoulli/outline ... Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization Pi_Transcendental: theory Polynomials.More_MPoly_Type Finished Bernoulli/outline (0:00:03 elapsed time) Timing Bernoulli (8 threads, 62.611s elapsed time, 435.090s cpu time, 25.937s GC time, factor 6.95) Finished Bernoulli (0:03:07 elapsed time, 0:08:35 cpu time, factor 2.74) Running Perron_Frobenius ... Subresultants: theory Subresultants.Subresultant Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ideal Groebner_Bases: theory Groebner_Bases.Buchberger Groebner_Bases: theory Groebner_Bases.F4 Groebner_Bases: theory Groebner_Bases.Algorithm_Schema_Impl Perron_Frobenius: theory HOL-Eisbach.Eisbach Perron_Frobenius: theory Pure-ex.Guess Perron_Frobenius: theory HOL-Analysis.Metric_Arith Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets Perron_Frobenius: theory HOL-Analysis.Abstract_Topology Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable Perron_Frobenius: theory HOL-Analysis.Inner_Product Perron_Frobenius: theory HOL-Analysis.L2_Norm Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row Perron_Frobenius: theory HOL-Analysis.Operator_Norm Perron_Frobenius: theory HOL-Analysis.Product_Vector Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Divisibility Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.RingHom Subresultants: theory Subresultants.Subresultant_Gcd Preparing Irrational_Series_Erdos_Straus/document ... Perron_Frobenius: theory HOL-Analysis.Norm_Arith Perron_Frobenius: theory Matrix.Utility Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.UnivPoly Finished Irrational_Series_Erdos_Straus/document (0:00:04 elapsed time) Preparing Irrational_Series_Erdos_Straus/outline ... Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Computational_Algebra Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.PolyMisc Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.Sturm_Tarski Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order Finished Irrational_Series_Erdos_Straus/outline (0:00:02 elapsed time) Timing Irrational_Series_Erdos_Straus (8 threads, 214.168s elapsed time, 1464.325s cpu time, 145.329s GC time, factor 6.84) Finished Irrational_Series_Erdos_Straus (0:07:22 elapsed time, 0:24:34 cpu time, factor 3.34) Running Linear_Programming ... Groebner_Bases: theory Groebner_Bases.Buchberger_Examples Groebner_Bases: theory Groebner_Bases.Syzygy_Examples Groebner_Bases: theory Groebner_Bases.Reduced_GB_Examples Transcendence_Series_Hancl_Rucki: theory Budan_Fourier.BF_Misc Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Algebraic Linear_Programming: theory Simplex.Simplex_Auxiliary Linear_Programming: theory Simplex.Simplex_Algebra Linear_Programming: theory Linear_Programming.More_Jordan_Normal_Forms Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Transcendental Perron_Frobenius: theory Sturm_Sequences.Sturm_Library Linear_Programming: theory Simplex.Rel_Chain Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Cauchy_Index_Theorem Groebner_Bases: theory Groebner_Bases.F4_Examples Linear_Programming: theory Simplex.Abstract_Linear_Poly Perron_Frobenius: theory HOL-Analysis.Elementary_Topology Perron_Frobenius: theory HOL-Analysis.Euclidean_Space Linear_Programming: theory Simplex.Linear_Poly_Maps Linear_Programming: theory Simplex.QDelta Linear_Programming: theory Simplex.Simplex Perron_Frobenius: theory Sturm_Sequences.Sturm_Method Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Winding_Number_Eval Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion Perron_Frobenius: theory HOL-Analysis.Abstract_Limits Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method Perron_Frobenius: theory HOL-Analysis.Linear_Algebra Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library Pi_Transcendental: theory Symmetric_Polynomials.Vieta Linear_Programming: theory Farkas.Farkas Linear_Programming: theory Simplex.Simplex_Incremental Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Multiplicative_Group Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier Perron_Frobenius: theory HOL-Analysis.Affine Perron_Frobenius: theory HOL-Analysis.Connected Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces Perron_Frobenius: theory HOL-Analysis.Convex Preparing Subresultants/document ... Perron_Frobenius: theory HOL-Analysis.Cartesian_Space Perron_Frobenius: theory HOL-Analysis.Function_Topology Preparing Zeta_Function/document ... Linear_Programming: theory Farkas.Matrix_Farkas Perron_Frobenius: theory HOL-Analysis.Product_Topology Finished Subresultants/document (0:00:07 elapsed time) Preparing Subresultants/outline ... Perron_Frobenius: theory HOL-Analysis.T1_Spaces Finished Zeta_Function/document (0:00:10 elapsed time) Preparing Zeta_Function/outline ... Finished Subresultants/outline (0:00:04 elapsed time) Timing Subresultants (8 threads, 49.414s elapsed time, 254.375s cpu time, 4.577s GC time, factor 5.15) Finished Subresultants (0:01:29 elapsed time, 0:05:32 cpu time, factor 3.72) Building Berlekamp_Zassenhaus ... Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residues Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Linear_Programming: theory Farkas.Simplex_for_Reals Perron_Frobenius: theory HOL-Analysis.Determinants Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces Linear_Programming: theory Linear_Programming.Matrix_LinPoly Finished Zeta_Function/outline (0:00:04 elapsed time) Timing Zeta_Function (8 threads, 42.379s elapsed time, 247.111s cpu time, 6.465s GC time, factor 5.83) Finished Zeta_Function (0:02:30 elapsed time, 0:05:09 cpu time, factor 2.06) Running Padic_Ints ... Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Euler_Criterion Linear_Programming: theory Linear_Programming.LP_Preliminaries Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension Berlekamp_Zassenhaus: theory Word_Lib.More_Divides Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets Padic_Ints: theory Padic_Ints.Function_Ring Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts Padic_Ints: theory HOL-Number_Theory.Cong Padic_Ints: theory Padic_Ints.Extended_Int Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Pocklington Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Real_Asymp Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Gauss Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem Linear_Programming: theory Linear_Programming.Linear_Programming Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residue_Primitive_Roots Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits Perron_Frobenius: theory HOL-Analysis.Line_Segment Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Quadratic_Reciprocity Padic_Ints: theory HOL-Number_Theory.Totient Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Divisibility Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Berlekamp_Zassenhaus: theory Matrix.Utility Padic_Ints: theory HOL-Number_Theory.Residues Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Number_Theory Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_FPS Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Misc Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Multiplicative_Function Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Product Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Euler_Products Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series Padic_Ints: theory Padic_Ints.Padic_Construction Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues Perron_Frobenius: theory HOL-Analysis.Starlike Perron_Frobenius: theory HOL-Analysis.Summation_Tests Padic_Ints: theory Padic_Ints.Padic_Integers Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_Zeta Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots Preparing Linear_Programming/document ... Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly Padic_Ints: theory Padic_Ints.Cring_Poly Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Berlekamp_Zassenhaus: theory Show.Show_Poly Perron_Frobenius: theory HOL-Analysis.Uniform_Limit Finished Linear_Programming/document (0:00:05 elapsed time) Preparing Linear_Programming/outline ... Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic Berlekamp_Zassenhaus: theory Word_Lib.More_Word Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization Finished Linear_Programming/outline (0:00:03 elapsed time) Timing Linear_Programming (8 threads, 96.522s elapsed time, 432.738s cpu time, 21.021s GC time, factor 4.48) Finished Linear_Programming (0:01:44 elapsed time, 0:07:20 cpu time, factor 4.22) Running Safe_Distance ... Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Moebius_Mu Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.More_Totient Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Liouville_Lambda Safe_Distance: theory Pure-ex.Guess Safe_Distance: theory HOL-Decision_Procs.Dense_Linear_Order Safe_Distance: theory HOL-Computational_Algebra.Fraction_Field Safe_Distance: theory HOL-Library.Code_Abstract_Nat Safe_Distance: theory HOL-Library.Code_Target_Int Safe_Distance: theory HOL-Library.More_List Safe_Distance: theory HOL-Computational_Algebra.Field_as_Ring Safe_Distance: theory HOL-Library.Lattice_Algebras Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count Perron_Frobenius: theory HOL-Analysis.Path_Connected Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory Safe_Distance: theory HOL-Library.Code_Target_Nat Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms Safe_Distance: theory HOL-Library.Log_Nat Pi_Transcendental: theory HOL-Real_Asymp.Real_Asymp Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field Safe_Distance: theory HOL-Computational_Algebra.Polynomial Safe_Distance: theory HOL-Library.Code_Target_Numeral Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit Safe_Distance: theory HOL-Computational_Algebra.Normalized_Fraction Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation Perron_Frobenius: theory HOL-Analysis.Derivative Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit Perron_Frobenius: theory HOL-Analysis.Homotopy Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly Padic_Ints: theory Padic_Ints.Padic_Int_Topology Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Library Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space Safe_Distance: theory HOL-Library.Interval Safe_Distance: theory HOL-Library.Float Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod Padic_Ints: theory Padic_Ints.Zp_Compact Perron_Frobenius: theory HOL-Analysis.Homeomorphism Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field Preparing Pi_Transcendental/document ... Preparing Groebner_Bases/document ... Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint Finished Pi_Transcendental/document (0:00:03 elapsed time) Preparing Pi_Transcendental/outline ... Safe_Distance: theory HOL-Library.Code_Target_Numeral_Float Finished Pi_Transcendental/outline (0:00:02 elapsed time) Safe_Distance: theory HOL-Library.Interval_Float Safe_Distance: theory HOL-Computational_Algebra.Polynomial_Factorial Timing Pi_Transcendental (8 threads, 42.758s elapsed time, 197.080s cpu time, 9.009s GC time, factor 4.61) Finished Pi_Transcendental (0:03:46 elapsed time, 0:04:27 cpu time, factor 1.18) Running Polynomials ... Safe_Distance: theory HOL-Decision_Procs.Approximation_Bounds Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials Padic_Ints: theory Padic_Ints.Hensels_Lemma Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous Polynomials: theory Deriving.Comparator Polynomials: theory Deriving.Generator_Aux Polynomials: theory Polynomials.More_Modules Polynomials: theory Polynomials.MPoly_Type Polynomials: theory Deriving.Derive_Manager Polynomials: theory HOL-Computational_Algebra.Factorial_Ring Polynomials: theory Matrix.Utility Polynomials: theory Open_Induction.Restricted_Predicates Polynomials: theory Well_Quasi_Orders.Infinite_Sequences Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Safe_Distance: theory HOL-Decision_Procs.Approximation Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization Polynomials: theory Show.Show Polynomials: theory Well_Quasi_Orders.Least_Enum Preparing Padic_Ints/document ... Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series Polynomials: theory Polynomials.Polynomials Polynomials: theory Well_Quasi_Orders.Minimal_Elements Polynomials: theory Well_Quasi_Orders.Almost_Full Polynomials: theory Polynomials.More_MPoly_Type Safe_Distance: theory Sturm_Sequences.Misc_Polynomial Finished Groebner_Bases/document (0:00:25 elapsed time) Preparing Groebner_Bases/outline ... Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL Polynomials: theory Polynomials.Poly_Mapping_Finite_Map Polynomials: theory Polynomials.OAlist Safe_Distance: theory Sturm_Sequences.Sturm_Library Safe_Distance: theory Sturm_Sequences.Sturm_Theorem Polynomials: theory Show.Show_Instances Safe_Distance: theory Sturm_Sequences.Sturm_Method Finished Groebner_Bases/outline (0:00:10 elapsed time) Timing Groebner_Bases (8 threads, 273.608s elapsed time, 1354.799s cpu time, 185.086s GC time, factor 4.95) Finished Groebner_Bases (0:09:00 elapsed time, 0:28:42 cpu time, factor 3.19) Running Groebner_Macaulay ... Safe_Distance: theory Sturm_Sequences.Sturm Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations Polynomials: theory Polynomials.Utils Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders Groebner_Macaulay: theory Groebner_Macaulay.Binomial_Int Groebner_Macaulay: theory Groebner_Macaulay.Dube_Prelims Groebner_Macaulay: theory Groebner_Macaulay.Monomial_Module Groebner_Macaulay: theory Groebner_Macaulay.Degree_Bound_Utils Groebner_Macaulay: theory Groebner_Macaulay.Degree_Section Polynomials: theory Polynomials.Power_Products Finished Padic_Ints/document (0:00:31 elapsed time) Preparing Padic_Ints/outline ... Groebner_Macaulay: theory Groebner_Macaulay.Hilbert_Function Safe_Distance: theory Safe_Distance.Safe_Distance Groebner_Macaulay: theory Groebner_Macaulay.Poly_Fun Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds Safe_Distance: theory Safe_Distance.Evaluation Safe_Distance: theory Safe_Distance.Safe_Distance_Reaction Finished Padic_Ints/outline (0:00:11 elapsed time) Timing Padic_Ints (8 threads, 102.108s elapsed time, 473.908s cpu time, 69.659s GC time, factor 4.64) Finished Padic_Ints (0:01:55 elapsed time, 0:08:00 cpu time, factor 4.18) Building Coinductive ... Polynomials: theory Polynomials.NZM Polynomials: theory Polynomials.Show_Polynomials Coinductive: theory Coinductive.Resumption Coinductive: theory HOL-Combinatorics.Transposition Coinductive: theory HOL-Analysis.Metric_Arith Coinductive: theory HOL-Analysis.Abstract_Topology Coinductive: theory HOL-Analysis.Inner_Product Coinductive: theory HOL-Analysis.L2_Norm Coinductive: theory HOL-Analysis.Product_Vector Coinductive: theory Coinductive.Coinductive_Nat Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit Berlekamp_Zassenhaus: theory Native_Word.Uint32 Berlekamp_Zassenhaus: theory Native_Word.Uint64 Coinductive: theory HOL-Analysis.Norm_Arith Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based Polynomials: theory HOL-Computational_Algebra.Polynomial Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification Coinductive: theory Coinductive.Coinductive_List Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay Groebner_Macaulay: theory Groebner_Macaulay.Cone_Decomposition Coinductive: theory HOL-Analysis.Elementary_Topology Coinductive: theory HOL-Analysis.Euclidean_Space Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl Preparing Transcendence_Series_Hancl_Rucki/document ... Preparing Safe_Distance/document ... Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int Polynomials: theory Polynomials.MPoly_Type_Class Polynomials: theory Polynomials.MPoly_Type_Univariate Finished Transcendence_Series_Hancl_Rucki/document (0:00:03 elapsed time) Preparing Transcendence_Series_Hancl_Rucki/outline ... Polynomials: theory Polynomials.PP_Type Finished Transcendence_Series_Hancl_Rucki/outline (0:00:02 elapsed time) Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound Timing Transcendence_Series_Hancl_Rucki (8 threads, 128.456s elapsed time, 868.980s cpu time, 77.572s GC time, factor 6.76) Finished Transcendence_Series_Hancl_Rucki (0:07:43 elapsed time, 0:14:38 cpu time, factor 1.90) Running DPRM_Theorem ... Finished Safe_Distance/document (0:00:06 elapsed time) Preparing Safe_Distance/outline ... DPRM_Theorem: theory DPRM_Theorem.RegisterMachineSpecification DPRM_Theorem: theory DPRM_Theorem.Parametric_Polynomials DPRM_Theorem: theory Digit_Expansions.Bits_Digits DPRM_Theorem: theory HOL-Computational_Algebra.Fraction_Field DPRM_Theorem: theory HOL-Library.Cancellation DPRM_Theorem: theory HOL-Computational_Algebra.Group_Closure DPRM_Theorem: theory HOL-Library.Infinite_Set DPRM_Theorem: theory HOL-Library.More_List Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl Finished Safe_Distance/outline (0:00:03 elapsed time) Timing Safe_Distance (8 threads, 160.026s elapsed time, 408.604s cpu time, 31.692s GC time, factor 2.55) Finished Safe_Distance (0:02:43 elapsed time, 0:06:51 cpu time, factor 2.51) Building Symmetric_Polynomials ... Polynomials: theory Polynomials.MPoly_Type_Class_Ordered Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based DPRM_Theorem: theory Digit_Expansions.Carries DPRM_Theorem: theory HOL-Library.Rewrite Symmetric_Polynomials: theory Polynomials.MPoly_Type Symmetric_Polynomials: theory Abstract-Rewriting.Seq Symmetric_Polynomials: theory Polynomials.More_Modules Symmetric_Polynomials: theory HOL-Combinatorics.Transposition Symmetric_Polynomials: theory Symmetric_Polynomials.Vieta Symmetric_Polynomials: theory Regular-Sets.Regular_Set Symmetric_Polynomials: theory Open_Induction.Restricted_Predicates Symmetric_Polynomials: theory Well_Quasi_Orders.Infinite_Sequences Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction DPRM_Theorem: theory Digit_Expansions.Binary_Operations DPRM_Theorem: theory HOL-Library.Discrete Symmetric_Polynomials: theory Well_Quasi_Orders.Least_Enum DPRM_Theorem: theory HOL-Library.Multiset Symmetric_Polynomials: theory HOL-Combinatorics.Permutations Coinductive: theory HOL-Analysis.Finite_Cartesian_Product Coinductive: theory HOL-Analysis.Linear_Algebra Coinductive: theory HOL-Analysis.Abstract_Topology_2 DPRM_Theorem: theory DPRM_Theorem.Exponentiation Polynomials: theory Polynomials.MPoly_Type_Class_FMap Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Elements Symmetric_Polynomials: theory Polynomials.More_MPoly_Type Polynomials: theory Polynomials.Quasi_PM_Power_Products Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus Polynomials: theory Polynomials.MPoly_PM DPRM_Theorem: theory DPRM_Theorem.RegisterMachineProperties Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly DPRM_Theorem: theory DPRM_Theorem.RegisterMachineSimulation Symmetric_Polynomials: theory Polynomials.Poly_Mapping_Finite_Map Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials Polynomials: theory Polynomials.OAlist_Poly_Mapping Polynomials: theory Polynomials.Term_Order DPRM_Theorem: theory DPRM_Theorem.SingleStepRegister DPRM_Theorem: theory DPRM_Theorem.SingleStepState DPRM_Theorem: theory DPRM_Theorem.Assignments Polynomials: theory Polynomials.MPoly_Type_Class_OAlist DPRM_Theorem: theory DPRM_Theorem.MultipleStepState DPRM_Theorem: theory DPRM_Theorem.MultipleStepRegister Coinductive: theory HOL-Analysis.Connected Coinductive: theory HOL-Analysis.Elementary_Metric_Spaces Coinductive: theory HOL-Analysis.Cartesian_Space DPRM_Theorem: theory DPRM_Theorem.Diophantine_Relations Groebner_Macaulay: theory Groebner_Macaulay.Dube_Bound Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF DPRM_Theorem: theory HOL-Computational_Algebra.Factorial_Ring DPRM_Theorem: theory DPRM_Theorem.Existential_Quantifier DPRM_Theorem: theory DPRM_Theorem.Equation_Setup DPRM_Theorem: theory DPRM_Theorem.Register_Machine_Sums DPRM_Theorem: theory DPRM_Theorem.Modulo_Divisibility DPRM_Theorem: theory DPRM_Theorem.Alpha_Sequence DPRM_Theorem: theory DPRM_Theorem.Exponential_Relation DPRM_Theorem: theory DPRM_Theorem.Digit_Function DPRM_Theorem: theory DPRM_Theorem.Binomial_Coefficient Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay_Examples Perron_Frobenius: theory Perron_Frobenius.Bij_Nat Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize Perron_Frobenius: theory Perron_Frobenius.Roots_Unity Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan Perron_Frobenius: theory Perron_Frobenius.HMA_Connect Coinductive: theory HOL-Analysis.Elementary_Normed_Spaces Coinductive: theory Coinductive.Coinductive_List_Prefix Coinductive: theory Coinductive.Hamming_Stream Coinductive: theory Coinductive.Koenigslemma Coinductive: theory Coinductive.LMirror Coinductive: theory Coinductive.Lazy_LList Coinductive: theory Coinductive.Quotient_Coinductive_List Coinductive: theory Coinductive.TLList Symmetric_Polynomials: theory Regular-Sets.Regular_Exp Coinductive: theory Coinductive.Coinductive_Stream Symmetric_Polynomials: theory Regular-Sets.Relation_Interpretation Symmetric_Polynomials: theory Regular-Sets.NDerivative Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion DPRM_Theorem: theory HOL-Computational_Algebra.Euclidean_Algorithm DPRM_Theorem: theory HOL-Computational_Algebra.Polynomial Symmetric_Polynomials: theory Regular-Sets.Equivalence_Checking Symmetric_Polynomials: theory Regular-Sets.Regexp_Method Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full Coinductive: theory HOL-Analysis.Topology_Euclidean_Space Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux Symmetric_Polynomials: theory Polynomials.Utils Symmetric_Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders Coinductive: theory Coinductive.Lazy_TLList Coinductive: theory Coinductive.Quotient_TLList Coinductive: theory Coinductive.TLList_CCPO Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius Symmetric_Polynomials: theory Polynomials.Power_Products Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory Coinductive: theory Coinductive.TLList_CCPO_Examples Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General Coinductive: theory Coinductive.Coinductive Coinductive: theory HOL-Analysis.Extended_Real_Limits DPRM_Theorem: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra DPRM_Theorem: theory HOL-Computational_Algebra.Normalized_Fraction DPRM_Theorem: theory HOL-Computational_Algebra.Primes Coinductive: theory Coinductive.CCPO_Topology DPRM_Theorem: theory HOL-Computational_Algebra.Formal_Power_Series DPRM_Theorem: theory HOL-Computational_Algebra.Nth_Powers DPRM_Theorem: theory HOL-Computational_Algebra.Squarefree Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class DPRM_Theorem: theory HOL-Computational_Algebra.Polynomial_Factorial Coinductive: theory Coinductive.LList_CCPO_Topology Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_Ordered Coinductive: theory Coinductive.Coinductive_Examples Preparing Polynomials/document ... Preparing Berlekamp_Zassenhaus/document ... DPRM_Theorem: theory HOL-Computational_Algebra.Polynomial_FPS DPRM_Theorem: theory HOL-Computational_Algebra.Formal_Laurent_Series Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_FMap Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials_Code Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds DPRM_Theorem: theory HOL-Computational_Algebra.Computational_Algebra DPRM_Theorem: theory Lucas_Theorem.Lucas_Theorem Preparing Groebner_Macaulay/document ... DPRM_Theorem: theory DPRM_Theorem.Binary_Orthogonal DPRM_Theorem: theory DPRM_Theorem.Binary_Masking DPRM_Theorem: theory DPRM_Theorem.Binary_And DPRM_Theorem: theory DPRM_Theorem.MachineMasking DPRM_Theorem: theory DPRM_Theorem.RM_Sums_Diophantine DPRM_Theorem: theory DPRM_Theorem.Register_Equations DPRM_Theorem: theory DPRM_Theorem.State_Unique_Equations DPRM_Theorem: theory DPRM_Theorem.Constants_Equations DPRM_Theorem: theory DPRM_Theorem.MachineEquations DPRM_Theorem: theory DPRM_Theorem.Mask_Equations DPRM_Theorem: theory DPRM_Theorem.State_0_Equation Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp DPRM_Theorem: theory DPRM_Theorem.CommutationRelations DPRM_Theorem: theory DPRM_Theorem.MultipleToSingleSteps Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block DPRM_Theorem: theory DPRM_Theorem.State_d_Equation DPRM_Theorem: theory DPRM_Theorem.All_State_Equations Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth DPRM_Theorem: theory DPRM_Theorem.All_Equations_Invariance DPRM_Theorem: theory DPRM_Theorem.All_Equations DPRM_Theorem: theory DPRM_Theorem.Machine_Equation_Equivalence DPRM_Theorem: theory DPRM_Theorem.DPRM Finished Berlekamp_Zassenhaus/document (0:00:26 elapsed time) Preparing Berlekamp_Zassenhaus/outline ... Preparing Perron_Frobenius/document ... Finished Groebner_Macaulay/document (0:00:17 elapsed time) Preparing Groebner_Macaulay/outline ... Finished Polynomials/document (0:00:31 elapsed time) Preparing Polynomials/outline ... Preparing DPRM_Theorem/document ... Finished Groebner_Macaulay/outline (0:00:06 elapsed time) Preparing Symmetric_Polynomials/document ... Finished Perron_Frobenius/document (0:00:09 elapsed time) Preparing Perron_Frobenius/outline ... Timing Groebner_Macaulay (8 threads, 190.965s elapsed time, 314.859s cpu time, 64.654s GC time, factor 1.65) Finished Groebner_Macaulay (0:03:21 elapsed time, 0:05:25 cpu time, factor 1.61) Running Signature_Groebner ... Finished Berlekamp_Zassenhaus/outline (0:00:11 elapsed time) Timing Berlekamp_Zassenhaus (8 threads, 199.128s elapsed time, 661.348s cpu time, 40.313s GC time, factor 3.32) Finished Berlekamp_Zassenhaus (0:05:22 elapsed time, 0:13:17 cpu time, factor 2.47) Building LLL_Basis_Reduction ... Finished Perron_Frobenius/outline (0:00:04 elapsed time) Finished Symmetric_Polynomials/document (0:00:05 elapsed time) Preparing Symmetric_Polynomials/outline ... Timing Perron_Frobenius (8 threads, 161.373s elapsed time, 991.423s cpu time, 88.479s GC time, factor 6.14) Finished Perron_Frobenius (0:07:15 elapsed time, 0:16:43 cpu time, factor 2.30) Building Algebraic_Numbers ... Finished Polynomials/outline (0:00:14 elapsed time) Timing Polynomials (8 threads, 93.840s elapsed time, 452.767s cpu time, 30.194s GC time, factor 4.82) Finished Polynomials (0:03:35 elapsed time, 0:07:48 cpu time, factor 2.17) Running Linear_Recurrences_Solver ... Finished Symmetric_Polynomials/outline (0:00:03 elapsed time) Timing Symmetric_Polynomials (8 threads, 105.782s elapsed time, 198.300s cpu time, 14.542s GC time, factor 1.87) Finished Symmetric_Polynomials (0:02:15 elapsed time, 0:04:19 cpu time, factor 1.91) Running Gauss_Sums ... Signature_Groebner: theory Signature_Groebner.Prelims Signature_Groebner: theory Signature_Groebner.More_MPoly LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials Signature_Groebner: theory Signature_Groebner.Signature_Groebner LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication Gauss_Sums: theory HOL-Algebra.QuotRing Algebraic_Numbers: theory Pure-ex.Guess Algebraic_Numbers: theory Deriving.Compare_Rat Algebraic_Numbers: theory Deriving.Compare_Real Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials Algebraic_Numbers: theory Show.Show_Real Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial Algebraic_Numbers: theory Show.Show_Complex Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend Finished DPRM_Theorem/document (0:00:20 elapsed time) Preparing DPRM_Theorem/outline ... LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem Linear_Recurrences_Solver: theory Pure-ex.Guess Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling Linear_Recurrences_Solver: theory Polynomials.MPoly_Type Linear_Recurrences_Solver: theory Deriving.Compare_Rat Linear_Recurrences_Solver: theory Deriving.Compare_Real Linear_Recurrences_Solver: theory Polynomials.More_Modules Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial Preparing Coinductive/document ... Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex Finished DPRM_Theorem/outline (0:00:08 elapsed time) Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates Gauss_Sums: theory HOL-Algebra.IntRing Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials Timing DPRM_Theorem (8 threads, 83.302s elapsed time, 573.344s cpu time, 39.505s GC time, factor 6.88) Finished DPRM_Theorem (0:02:15 elapsed time, 0:09:37 cpu time, factor 4.27) Running Mersenne_Primes ... Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary Algebraic_Numbers: theory Algebraic_Numbers.Resultant Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend Mersenne_Primes: theory HOL-Number_Theory.Cong Mersenne_Primes: theory Word_Lib.Bit_Comprehension Mersenne_Primes: theory Word_Lib.More_Divides Mersenne_Primes: theory HOL-Number_Theory.Fib Mersenne_Primes: theory HOL-Number_Theory.Prime_Powers Mersenne_Primes: theory HOL-Number_Theory.Eratosthenes Mersenne_Primes: theory Pell.Pell Mersenne_Primes: theory Native_Word.Code_Int_Integer_Conversion Mersenne_Primes: theory Word_Lib.More_Arithmetic Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library Finished Coinductive/document (0:00:10 elapsed time) Preparing Coinductive/outline ... Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials Mersenne_Primes: theory Word_Lib.More_Word Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim Finished Coinductive/outline (0:00:05 elapsed time) Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials Timing Coinductive (8 threads, 71.659s elapsed time, 353.637s cpu time, 21.259s GC time, factor 4.93) Finished Coinductive (0:03:36 elapsed time, 0:07:05 cpu time, factor 1.97) Running Deep_Learning ... Linear_Recurrences_Solver: theory Show.Show_Real Deep_Learning: theory Deep_Learning.Tensor Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set Deep_Learning: theory HOL-Computational_Algebra.Fraction_Field Deep_Learning: theory HOL-Library.Fun_Lexorder Deep_Learning: theory HOL-Algebra.Congruence Deep_Learning: theory Jordan_Normal_Form.Missing_Misc Deep_Learning: theory HOL-Library.More_List Deep_Learning: theory HOL-Library.Groups_Big_Fun Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted Deep_Learning: theory Jordan_Normal_Form.Conjugate Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum Deep_Learning: theory Deep_Learning.Lebesgue_Functional Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements Linear_Recurrences_Solver: theory Show.Show_Complex Mersenne_Primes: theory HOL-Number_Theory.Mod_Exp Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full Mersenne_Primes: theory HOL-Number_Theory.Totient Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List Deep_Learning: theory HOL-Computational_Algebra.Polynomial Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist Deep_Learning: theory HOL-Library.Poly_Mapping Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver Deep_Learning: theory Deep_Learning.Tensor_Subtensor Deep_Learning: theory Deep_Learning.Tensor_Plus Mersenne_Primes: theory Word_Lib.Bit_Shifts_Infix_Syntax Mersenne_Primes: theory Word_Lib.Least_significant_bit Deep_Learning: theory Polynomial_Interpolation.Ring_Hom Mersenne_Primes: theory HOL-Number_Theory.Residues Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult Deep_Learning: theory Deep_Learning.Tensor_Product Deep_Learning: theory HOL-Algebra.Order Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers Deep_Learning: theory Deep_Learning.Tensor_Rank Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters Deep_Learning: theory VectorSpace.FunctionLemmas Mersenne_Primes: theory Word_Lib.Most_significant_bit LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2 Mersenne_Primes: theory Word_Lib.Generic_set_bit Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences Mersenne_Primes: theory HOL-Number_Theory.Euler_Criterion Mersenne_Primes: theory HOL-Number_Theory.Pocklington Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic Mersenne_Primes: theory Native_Word.Code_Target_Integer_Bit Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary Mersenne_Primes: theory HOL-Number_Theory.Gauss Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library Linear_Recurrences_Solver: theory Polynomials.Utils Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums Mersenne_Primes: theory HOL-Number_Theory.Residue_Primitive_Roots Mersenne_Primes: theory HOL-Number_Theory.Quadratic_Reciprocity Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW Deep_Learning: theory HOL-Algebra.Lattice Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders Deep_Learning: theory Polynomials.MPoly_Type Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly Mersenne_Primes: theory HOL-Number_Theory.Number_Theory Gauss_Sums: theory Gauss_Sums.Gauss_Sums Linear_Recurrences_Solver: theory Polynomials.Power_Products Mersenne_Primes: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries Mersenne_Primes: theory Probabilistic_Prime_Tests.Legendre_Symbol Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers Deep_Learning: theory Polynomials.More_MPoly_Type Mersenne_Primes: theory Probabilistic_Prime_Tests.Jacobi_Symbol Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Auxiliary Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer Deep_Learning: theory HOL-Algebra.Complete_Lattice Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests Deep_Learning: theory HOL-Algebra.Group Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers Deep_Learning: theory HOL-Algebra.Coset Deep_Learning: theory HOL-Algebra.FiniteProduct Signature_Groebner: theory Signature_Groebner.Signature_Examples Deep_Learning: theory HOL-Algebra.Ring Deep_Learning: theory Polynomials.MPoly_Type_Univariate Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set Deep_Learning: theory HOL-Algebra.Module Deep_Learning: theory Jordan_Normal_Form.Missing_Ring Deep_Learning: theory VectorSpace.RingModuleFacts Deep_Learning: theory VectorSpace.MonoidSums Deep_Learning: theory VectorSpace.LinearCombinations LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class Deep_Learning: theory Jordan_Normal_Form.Matrix Preparing Gauss_Sums/document ... Mersenne_Primes: theory Native_Word.Code_Target_Int_Bit Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Code Deep_Learning: theory VectorSpace.SumSpaces Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered Deep_Learning: theory VectorSpace.VectorSpace Preparing Signature_Groebner/document ... Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix Deep_Learning: theory Deep_Learning.Tensor_Matricization Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Deep_Learning: theory Deep_Learning.DL_Network Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise Deep_Learning: theory Jordan_Normal_Form.Column_Operations Deep_Learning: theory Jordan_Normal_Form.Determinant Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers Finished Gauss_Sums/document (0:00:08 elapsed time) Preparing Gauss_Sums/outline ... Deep_Learning: theory Deep_Learning.DL_Shallow_Model Deep_Learning: theory Deep_Learning.DL_Deep_Model Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace Finished Gauss_Sums/outline (0:00:03 elapsed time) Timing Gauss_Sums (8 threads, 84.466s elapsed time, 233.130s cpu time, 10.097s GC time, factor 2.76) Finished Gauss_Sums (0:01:29 elapsed time, 0:03:57 cpu time, factor 2.66) Running Isabelle_Marries_Dirac ... Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly Deep_Learning: theory Jordan_Normal_Form.VS_Connect Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly Deep_Learning: theory Jordan_Normal_Form.DL_Rank Isabelle_Marries_Dirac: theory Matrix.Utility Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Basics Preparing Mersenne_Primes/document ... Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Binary_Nat Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum Isabelle_Marries_Dirac: theory Matrix.Matrix_Legacy Finished Signature_Groebner/document (0:00:17 elapsed time) Preparing Signature_Groebner/outline ... Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity Isabelle_Marries_Dirac: theory Matrix_Tensor.Matrix_Tensor Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Complex_Vectors Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Measurement Finished Mersenne_Primes/document (0:00:04 elapsed time) Preparing Mersenne_Primes/outline ... LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver Finished Mersenne_Primes/outline (0:00:03 elapsed time) Timing Mersenne_Primes (8 threads, 89.840s elapsed time, 287.853s cpu time, 7.571s GC time, factor 3.20) Finished Mersenne_Primes (0:01:36 elapsed time, 0:04:53 cpu time, factor 3.06) Running Rep_Fin_Groups ... Finished Signature_Groebner/outline (0:00:06 elapsed time) Timing Signature_Groebner (8 threads, 92.547s elapsed time, 192.269s cpu time, 26.471s GC time, factor 2.08) Finished Signature_Groebner (0:01:42 elapsed time, 0:03:21 cpu time, factor 1.97) Running Linear_Recurrences ... Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Tensor Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.More_Tensor Rep_Fin_Groups: theory Rep_Fin_Groups.Rep_Fin_Groups Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.No_Cloning Linear_Recurrences: theory HOL-Combinatorics.Stirling Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree Linear_Recurrences: theory HOL-Library.Code_Target_Int Linear_Recurrences: theory HOL-Library.BNF_Corec Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat Linear_Recurrences: theory HOL-Library.Sublist Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Entanglement Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Teleportation Linear_Recurrences: theory HOL-Library.Code_Target_Nat Linear_Recurrences: theory HOL-Real_Asymp.Inst_Existentials Linear_Recurrences: theory HOL-Computational_Algebra.Polynomial_FPS Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch_Jozsa Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Divisibility Linear_Recurrences: theory HOL-Library.Code_Target_Numeral Linear_Recurrences: theory HOL-Real_Asymp.Eventuallize Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Linear_Recurrences: theory HOL-Real_Asymp.Lazy_Eval Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials Linear_Recurrences: theory Matrix.Utility Preparing Deep_Learning/document ... Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization Linear_Recurrences: theory HOL-Computational_Algebra.Formal_Laurent_Series Finished Deep_Learning/document (0:00:08 elapsed time) Preparing Deep_Learning/outline ... LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity Finished Deep_Learning/outline (0:00:04 elapsed time) Timing Deep_Learning (8 threads, 88.398s elapsed time, 635.140s cpu time, 39.374s GC time, factor 7.19) Finished Deep_Learning (0:01:40 elapsed time, 0:10:39 cpu time, factor 6.34) Building Stirling_Formula ... Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials Stirling_Formula: theory HOL-Library.BNF_Corec Stirling_Formula: theory Landau_Symbols.Group_Sort Stirling_Formula: theory HOL-Library.Function_Algebras Stirling_Formula: theory HOL-Real_Asymp.Lazy_Eval Stirling_Formula: theory HOL-Real_Asymp.Eventuallize Stirling_Formula: theory HOL-Real_Asymp.Inst_Existentials Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc Linear_Recurrences: theory Linear_Recurrences.RatFPS Linear_Recurrences: theory Linear_Recurrences.Factorizations Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition Stirling_Formula: theory Landau_Symbols.Landau_Real_Products Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion Stirling_Formula: theory Landau_Symbols.Landau_Simprocs Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences Stirling_Formula: theory Landau_Symbols.Landau_More Stirling_Formula: theory Stirling_Formula.Stirling_Formula Stirling_Formula: theory HOL-Real_Asymp.Multiseries_Expansion Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Linear_Recurrences: theory HOL-Real_Asymp.Real_Asymp Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics Preparing Algebraic_Numbers/document ... Stirling_Formula: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Preparing Isabelle_Marries_Dirac/document ... Finished Algebraic_Numbers/document (0:00:14 elapsed time) Preparing Algebraic_Numbers/outline ... Stirling_Formula: theory HOL-Real_Asymp.Real_Asymp Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics Finished Algebraic_Numbers/outline (0:00:07 elapsed time) Timing Algebraic_Numbers (8 threads, 127.684s elapsed time, 684.412s cpu time, 32.267s GC time, factor 5.36) Finished Algebraic_Numbers (0:02:55 elapsed time, 0:13:00 cpu time, factor 4.43) Running Dirichlet_L ... Finished Isabelle_Marries_Dirac/document (0:00:09 elapsed time) Preparing Isabelle_Marries_Dirac/outline ... Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order Dirichlet_L: theory HOL-Library.Lattice_Algebras Dirichlet_L: theory HOL-Library.Log_Nat Dirichlet_L: theory Lehmer.Lehmer Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate Preparing Rep_Fin_Groups/document ... Finished Isabelle_Marries_Dirac/outline (0:00:04 elapsed time) Timing Isabelle_Marries_Dirac (8 threads, 75.300s elapsed time, 521.593s cpu time, 21.182s GC time, factor 6.93) Finished Isabelle_Marries_Dirac (0:01:23 elapsed time, 0:08:49 cpu time, factor 6.36) Running Fishers_Inequality ... Timing Linear_Recurrences_Solver (8 threads, 193.619s elapsed time, 966.113s cpu time, 95.717s GC time, factor 4.99) Finished Linear_Recurrences_Solver (0:03:22 elapsed time, 0:16:14 cpu time, factor 4.82) Running BenOr_Kozen_Reif ... Preparing Linear_Recurrences/document ... Dirichlet_L: theory HOL-Library.Interval Dirichlet_L: theory HOL-Library.Float Dirichlet_L: theory HOL-Library.Interval_Float Finished Linear_Recurrences/document (0:00:03 elapsed time) Preparing Linear_Recurrences/outline ... Fishers_Inequality: theory Polynomials.MPoly_Type Fishers_Inequality: theory Card_Partitions.Set_Partition Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More Fishers_Inequality: theory Polynomials.More_Modules Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations Fishers_Inequality: theory List-Index.List_Index Fishers_Inequality: theory Open_Induction.Restricted_Predicates Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum Finished Linear_Recurrences/outline (0:00:02 elapsed time) Timing Linear_Recurrences (8 threads, 77.840s elapsed time, 292.062s cpu time, 20.541s GC time, factor 3.75) Finished Linear_Recurrences (0:01:22 elapsed time, 0:04:55 cpu time, factor 3.60) Running Registers ... Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full Finished Rep_Fin_Groups/document (0:00:12 elapsed time) Preparing Rep_Fin_Groups/outline ... Preparing LLL_Basis_Reduction/document ... BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix Fishers_Inequality: theory Polynomials.More_MPoly_Type BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset Dirichlet_L: theory Bertrands_Postulate.Bertrand Fishers_Inequality: theory Design_Theory.Multisets_Extras Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences Registers: theory HOL-Eisbach.Eisbach Registers: theory HOL-Library.Type_Length Registers: theory HOL-Library.Z2 Registers: theory Registers.Axioms Registers: theory Registers.Axioms_Classical Fishers_Inequality: theory Design_Theory.Design_Basics Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations Registers: theory Registers.Laws Finished Rep_Fin_Groups/outline (0:00:06 elapsed time) Timing Rep_Fin_Groups (8 threads, 75.872s elapsed time, 211.532s cpu time, 4.442s GC time, factor 2.79) Finished Rep_Fin_Groups (0:01:19 elapsed time, 0:03:35 cpu time, factor 2.70) Running Hermite_Lindemann ... Registers: theory Registers.Laws_Classical BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm Fishers_Inequality: theory Polynomials.Utils Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders Fishers_Inequality: theory Design_Theory.Design_Operations Registers: theory Registers.Misc BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction Fishers_Inequality: theory Groebner_Bases.General BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm Fishers_Inequality: theory Polynomials.Power_Products BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW Hermite_Lindemann: theory HOL-Algebra.Divisibility Fishers_Inequality: theory Design_Theory.Block_Designs Fishers_Inequality: theory Design_Theory.Sub_Designs Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring Hermite_Lindemann: theory HOL-Library.Monad_Syntax Hermite_Lindemann: theory Containers.Containers_Auxiliary Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision Registers: theory HOL-Library.Word Fishers_Inequality: theory Design_Theory.Design_Isomorphisms Hermite_Lindemann: theory Matrix.Utility Preparing Stirling_Formula/document ... Registers: theory Registers.Axioms_Complement Registers: theory Registers.Laws_Complement Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat Finished LLL_Basis_Reduction/document (0:00:16 elapsed time) Preparing LLL_Basis_Reduction/outline ... Fishers_Inequality: theory Design_Theory.BIBD Hermite_Lindemann: theory Polynomial_Factorization.Missing_List Registers: theory Registers.Classical_Extra Registers: theory Registers.Finite_Tensor_Product Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom Registers: theory Registers.Axioms_Quantum Fishers_Inequality: theory Fishers_Inequality.Design_Extras Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial Registers: theory Registers.Finite_Tensor_Product_Matrices Registers: theory Registers.Quantum Finished Stirling_Formula/document (0:00:06 elapsed time) Preparing Stirling_Formula/outline ... Registers: theory Registers.Laws_Quantum Finished LLL_Basis_Reduction/outline (0:00:06 elapsed time) Timing LLL_Basis_Reduction (8 threads, 162.376s elapsed time, 494.651s cpu time, 35.890s GC time, factor 3.05) Finished LLL_Basis_Reduction (0:03:39 elapsed time, 0:10:14 cpu time, factor 2.80) Running Polynomial_Factorization ... BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision Finished Stirling_Formula/outline (0:00:03 elapsed time) Timing Stirling_Formula (8 threads, 46.670s elapsed time, 153.857s cpu time, 11.891s GC time, factor 3.30) Finished Stirling_Formula (0:01:20 elapsed time, 0:03:41 cpu time, factor 2.76) Running Factor_Algebraic_Polynomial ... Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication Dirichlet_L: theory HOL-Algebra.QuotRing Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend Polynomial_Factorization: theory Containers.Containers_Auxiliary Polynomial_Factorization: theory Deriving.Derive_Manager Polynomial_Factorization: theory Deriving.Generator_Aux Polynomial_Factorization: theory Containers.List_Fusion Polynomial_Factorization: theory Deriving.Comparator Polynomial_Factorization: theory Containers.Extend_Partial_Order Polynomial_Factorization: theory Polynomial_Interpolation.Missing_Unsorted Polynomial_Factorization: theory Cauchy.CauchysMeanTheorem Polynomial_Factorization: theory Polynomial_Interpolation.Improved_Code_Equations Polynomial_Factorization: theory Polynomial_Interpolation.Neville_Aitken_Interpolation Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type Factor_Algebraic_Polynomial: theory Polynomials.More_Modules Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Divisibility Preparing Modular_arithmetic_LLL_and_HNF_algorithms/document ... Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Dirichlet_L: theory HOL-Algebra.IntRing Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Polynomial_Factorization: theory Containers.Containers_Generator Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library Polynomial_Factorization: theory Matrix.Utility Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary Registers: theory Registers.Quantum_Extra Polynomial_Factorization: theory Polynomial_Interpolation.Divmod_Int Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds Polynomial_Factorization: theory Polynomial_Interpolation.Ring_Hom Fishers_Inequality: theory Polynomials.MPoly_Type_Class Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset Polynomial_Factorization: theory Polynomial_Factorization.Missing_List Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW Polynomial_Factorization: theory Show.Show Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full Polynomial_Factorization: theory Polynomial_Interpolation.Is_Rat_To_Rat Polynomial_Factorization: theory Sqrt_Babylonian.Log_Impl Polynomial_Factorization: theory Deriving.Compare Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend Polynomial_Factorization: theory Deriving.Comparator_Generator Polynomial_Factorization: theory Containers.Lexicographic_Order Registers: theory Registers.Axioms_Complement_Quantum Registers: theory Registers.QHoare Hermite_Lindemann: theory Jordan_Normal_Form.Matrix Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials Registers: theory Registers.Teleport Polynomial_Factorization: theory Containers.Set_Linorder Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered Registers: theory Registers.Laws_Complement_Quantum Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences Registers: theory Registers.Check_Autogenerated_Files Registers: theory Registers.Quantum_Extra2 Polynomial_Factorization: theory Containers.RBT_ext Polynomial_Factorization: theory Deriving.RBT_Comparator_Impl Registers: theory Registers.Pure_States Polynomial_Factorization: theory Polynomial_Interpolation.Missing_Polynomial Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma Finished Modular_arithmetic_LLL_and_HNF_algorithms/document (0:00:21 elapsed time) Preparing Modular_arithmetic_LLL_and_HNF_algorithms/outline ... Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups Polynomial_Factorization: theory Deriving.Compare_Generator Factor_Algebraic_Polynomial: theory Polynomials.Utils Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders Polynomial_Factorization: theory Sqrt_Babylonian.NthRoot_Impl Finished Modular_arithmetic_LLL_and_HNF_algorithms/outline (0:00:05 elapsed time) Timing Modular_arithmetic_LLL_and_HNF_algorithms (8 threads, 894.801s elapsed time, 4275.700s cpu time, 822.765s GC time, factor 4.78) Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:15:01 elapsed time, 1:11:21 cpu time, factor 4.75) Running Winding_Number_Eval ... Polynomial_Factorization: theory Deriving.Compare_Instances Factor_Algebraic_Polynomial: theory Polynomials.Power_Products Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters Winding_Number_Eval: theory HOL-Eisbach.Eisbach Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field Winding_Number_Eval: theory HOL-Library.More_List Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis Preparing BenOr_Kozen_Reif/document ... Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility Polynomial_Factorization: theory Polynomial_Interpolation.Lagrange_Interpolation Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Polynomial_Factorization: theory Show.Show_Instances Preparing Registers/document ... Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix Hermite_Lindemann: theory Jordan_Normal_Form.Determinant Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod Hermite_Lindemann: theory Subresultants.More_Homomorphisms Hermite_Lindemann: theory Subresultants.Resultant_Prelim Finished BenOr_Kozen_Reif/document (0:00:24 elapsed time) Preparing BenOr_Kozen_Reif/outline ... Finished Registers/document (0:00:16 elapsed time) Preparing Registers/outline ... Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly Polynomial_Factorization: theory Polynomial_Interpolation.Ring_Hom_Poly Polynomial_Factorization: theory Show.Show_Poly Fishers_Inequality: theory Fishers_Inequality.Dual_Systems Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations Hermite_Lindemann: theory Algebraic_Numbers.Resultant Finished BenOr_Kozen_Reif/outline (0:00:08 elapsed time) Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly Finished Registers/outline (0:00:08 elapsed time) Timing BenOr_Kozen_Reif (8 threads, 55.286s elapsed time, 340.301s cpu time, 8.138s GC time, factor 6.16) Finished BenOr_Kozen_Reif (0:01:16 elapsed time, 0:05:49 cpu time, factor 4.56) Timing Registers (8 threads, 72.968s elapsed time, 438.553s cpu time, 13.512s GC time, factor 6.01) Finished Registers (0:01:19 elapsed time, 0:07:24 cpu time, factor 5.62) Running CRYSTALS-Kyber ... Running LLL_Factorization ... Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers Preparing Fishers_Inequality/document ... Preparing Dirichlet_L/document ... Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization Polynomial_Factorization: theory Polynomial_Interpolation.Newton_Interpolation Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers CRYSTALS-Kyber: theory HOL-Number_Theory.Fib CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint LLL_Factorization: theory LLL_Factorization.Sub_Sums LLL_Factorization: theory LLL_Factorization.Factor_Bound_2 CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss Finished Dirichlet_L/document (0:00:06 elapsed time) Preparing Dirichlet_L/outline ... LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl Finished Dirichlet_L/outline (0:00:03 elapsed time) Timing Dirichlet_L (8 threads, 69.240s elapsed time, 385.571s cpu time, 26.963s GC time, factor 5.57) Finished Dirichlet_L (0:02:04 elapsed time, 0:06:30 cpu time, factor 3.15) Building UTP-Toolkit ... LLL_Factorization: theory LLL_Factorization.LLL_Factorization Finished Fishers_Inequality/document (0:00:13 elapsed time) Preparing Fishers_Inequality/outline ... CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide Polynomial_Factorization: theory Polynomial_Interpolation.Polynomial_Interpolation Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial UTP-Toolkit: theory HOL-Eisbach.Eisbach UTP-Toolkit: theory UTP-Toolkit.Map_Extra UTP-Toolkit: theory UTP-Toolkit.FSet_Extra UTP-Toolkit: theory Optics.Two UTP-Toolkit: theory Optics.Interp UTP-Toolkit: theory UTP-Toolkit.List_Lexord_Alt UTP-Toolkit: theory UTP-Toolkit.Total_Recall UTP-Toolkit: theory UTP-Toolkit.Infinity UTP-Toolkit: theory Optics.Lens_Laws Finished Fishers_Inequality/outline (0:00:07 elapsed time) Timing Fishers_Inequality (8 threads, 62.058s elapsed time, 389.542s cpu time, 30.585s GC time, factor 6.28) Finished Fishers_Inequality (0:01:56 elapsed time, 0:06:39 cpu time, factor 3.42) Running Finite_Fields ... LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22 Winding_Number_Eval: theory Sturm_Tarski.PolyMisc Polynomial_Factorization: theory Containers.Collection_Order Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski UTP-Toolkit: theory UTP-Toolkit.Positive CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory Finite_Fields: theory HOL-Number_Theory.Cong Finite_Fields: theory HOL-Number_Theory.Eratosthenes Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results Finite_Fields: theory HOL-Number_Theory.Fib Finite_Fields: theory HOL-Number_Theory.Prime_Powers CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space Winding_Number_Eval: theory Budan_Fourier.BF_Misc Polynomial_Factorization: theory Containers.RBT_Mapping2 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic Polynomial_Factorization: theory Containers.RBT_Set2 UTP-Toolkit: theory Optics.Lens_Algebra Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental UTP-Toolkit: theory Optics.Lens_Order Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product UTP-Toolkit: theory Optics.Lens_Symmetric Polynomial_Factorization: theory Polynomial_Factorization.Precomputation UTP-Toolkit: theory Optics.Lens_Instances Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization Finite_Fields: theory HOL-Number_Theory.Mod_Exp Finite_Fields: theory HOL-Number_Theory.Totient Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress UTP-Toolkit: theory UTP-Toolkit.List_Extra UTP-Toolkit: theory Optics.Lenses UTP-Toolkit: theory UTP-Toolkit.Partial_Fun Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly Finite_Fields: theory HOL-Number_Theory.Residues Preparing Hermite_Lindemann/document ... UTP-Toolkit: theory UTP-Toolkit.Finite_Fun UTP-Toolkit: theory UTP-Toolkit.Sequence Preparing LLL_Factorization/document ... CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme UTP-Toolkit: theory UTP-Toolkit.Countable_Set_Extra Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly UTP-Toolkit: theory UTP-Toolkit.utp_toolkit Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly Finished Hermite_Lindemann/document (0:00:06 elapsed time) Preparing Hermite_Lindemann/outline ... Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples Finished LLL_Factorization/document (0:00:06 elapsed time) Preparing LLL_Factorization/outline ... CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values Preparing Factor_Algebraic_Polynomial/document ... Finite_Fields: theory HOL-Number_Theory.Euler_Criterion Finite_Fields: theory HOL-Number_Theory.Pocklington Finished Hermite_Lindemann/outline (0:00:03 elapsed time) Timing Hermite_Lindemann (8 threads, 57.204s elapsed time, 380.763s cpu time, 13.825s GC time, factor 6.66) Finished Hermite_Lindemann (0:02:27 elapsed time, 0:06:27 cpu time, factor 2.62) Building Linear_Inequalities ... Finite_Fields: theory HOL-Number_Theory.Gauss Finished LLL_Factorization/outline (0:00:03 elapsed time) Timing LLL_Factorization (8 threads, 44.033s elapsed time, 138.855s cpu time, 3.433s GC time, factor 3.15) Finished LLL_Factorization (0:00:54 elapsed time, 0:02:28 cpu time, factor 2.75) Running Amicable_Numbers ... Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext Amicable_Numbers: theory Lehmer.Lehmer Amicable_Numbers: theory Matrix.Utility Amicable_Numbers: theory Pratt_Certificate.Pratt_Certificate Finished Factor_Algebraic_Polynomial/document (0:00:08 elapsed time) Preparing Factor_Algebraic_Polynomial/outline ... Amicable_Numbers: theory Polynomial_Factorization.Missing_List Preparing Polynomial_Factorization/document ... Finite_Fields: theory Finite_Fields.Ring_Characteristic Finite_Fields: theory HOL-Number_Theory.Number_Theory Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc Finite_Fields: theory Dirichlet_Series.Multiplicative_Function Preparing CRYSTALS-Kyber/document ... Finite_Fields: theory Dirichlet_Series.Dirichlet_Product Finished Factor_Algebraic_Polynomial/outline (0:00:04 elapsed time) Timing Factor_Algebraic_Polynomial (8 threads, 53.565s elapsed time, 220.732s cpu time, 17.181s GC time, factor 4.12) Finished Factor_Algebraic_Polynomial (0:02:18 elapsed time, 0:03:51 cpu time, factor 1.67) Running Buchi_Complementation ... Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect Finite_Fields: theory Dirichlet_Series.Dirichlet_Series Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set Linear_Inequalities: theory Linear_Inequalities.Basis_Extension Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors Finite_Fields: theory Dirichlet_Series.Moebius_Mu Finished CRYSTALS-Kyber/document (0:00:04 elapsed time) Preparing CRYSTALS-Kyber/outline ... Amicable_Numbers: theory Polynomial_Factorization.Missing_Multiset Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization Buchi_Complementation: theory Buchi_Complementation.Alternate Buchi_Complementation: theory Buchi_Complementation.Formula Buchi_Complementation: theory Buchi_Complementation.Graph Finished Polynomial_Factorization/document (0:00:09 elapsed time) Preparing Polynomial_Factorization/outline ... Amicable_Numbers: theory Pratt_Certificate.Pratt_Certificate_Code Amicable_Numbers: theory Polynomial_Factorization.Prime_Factorization Buchi_Complementation: theory Buchi_Complementation.Ranking Finished CRYSTALS-Kyber/outline (0:00:03 elapsed time) Buchi_Complementation: theory Buchi_Complementation.Complementation Timing CRYSTALS-Kyber (8 threads, 47.080s elapsed time, 260.820s cpu time, 7.071s GC time, factor 5.54) Finished CRYSTALS-Kyber (0:01:14 elapsed time, 0:04:30 cpu time, factor 3.64) Running Lambert_W ... Amicable_Numbers: theory Amicable_Numbers.Amicable_Numbers Linear_Inequalities: theory Linear_Inequalities.Cone Preparing UTP-Toolkit/document ... Buchi_Complementation: theory Buchi_Complementation.Complementation_Implement Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux Finished Polynomial_Factorization/outline (0:00:04 elapsed time) Timing Polynomial_Factorization (8 threads, 56.025s elapsed time, 330.483s cpu time, 20.753s GC time, factor 5.90) Finished Polynomial_Factorization (0:02:29 elapsed time, 0:05:38 cpu time, factor 2.27) Running Elliptic_Curves_Group_Law ... Preparing Winding_Number_Eval/document ... Linear_Inequalities: theory Linear_Inequalities.Convex_Hull Lambert_W: theory HOL-Library.BNF_Corec Lambert_W: theory HOL-Library.Function_Algebras Lambert_W: theory HOL-Real_Asymp.Inst_Existentials Lambert_W: theory HOL-Real_Asymp.Eventuallize Lambert_W: theory HOL-Real_Asymp.Lazy_Eval Lambert_W: theory Landau_Symbols.Group_Sort Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Algebra_Aux Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Conversions Linear_Inequalities: theory Linear_Inequalities.Dim_Span Linear_Inequalities: theory Linear_Inequalities.Normal_Vector Finished UTP-Toolkit/document (0:00:06 elapsed time) Preparing UTP-Toolkit/outline ... Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic Buchi_Complementation: theory Buchi_Complementation.Complementation_Final Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities Lambert_W: theory Landau_Symbols.Landau_Real_Products Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Commutative_Ring Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem Finished UTP-Toolkit/outline (0:00:05 elapsed time) Preparing Finite_Fields/document ... Timing UTP-Toolkit (8 threads, 12.228s elapsed time, 85.775s cpu time, 2.609s GC time, factor 7.01) Finished UTP-Toolkit (0:01:08 elapsed time, 0:02:19 cpu time, factor 2.03) Building Sturm_Sequences ... Lambert_W: theory Landau_Symbols.Landau_Simprocs Finished Winding_Number_Eval/document (0:00:13 elapsed time) Preparing Winding_Number_Eval/outline ... Sturm_Sequences: theory Sturm_Sequences.Sturm_Library_Document Sturm_Sequences: theory Pure-ex.Guess Sturm_Sequences: theory Sturm_Sequences.Misc_Polynomial Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Reflective_Field Lambert_W: theory Landau_Symbols.Landau_More Lambert_W: theory Stirling_Formula.Stirling_Formula Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions Sturm_Sequences: theory Sturm_Sequences.Sturm_Library Sturm_Sequences: theory Sturm_Sequences.Sturm_Theorem Finished Winding_Number_Eval/outline (0:00:04 elapsed time) Timing Winding_Number_Eval (8 threads, 43.607s elapsed time, 228.706s cpu time, 6.484s GC time, factor 5.24) Finished Winding_Number_Eval (0:02:04 elapsed time, 0:03:53 cpu time, factor 1.87) Running RSAPSS ... Finished Finite_Fields/document (0:00:07 elapsed time) Preparing Finite_Fields/outline ... Linear_Inequalities: theory Linear_Inequalities.Integer_Hull Sturm_Sequences: theory Sturm_Sequences.Sturm_Method Lambert_W: theory HOL-Real_Asymp.Multiseries_Expansion Sturm_Sequences: theory Sturm_Sequences.Sturm Sturm_Sequences: theory Sturm_Sequences.Sturm_Ex RSAPSS: theory RSAPSS.Word Finished Finite_Fields/outline (0:00:03 elapsed time) Timing Finite_Fields (8 threads, 42.421s elapsed time, 272.584s cpu time, 18.949s GC time, factor 6.43) Finished Finite_Fields (0:01:11 elapsed time, 0:04:39 cpu time, factor 3.91) Running HOL-Quotient_Examples ... Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Axclass Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Locale Buchi_Complementation: theory Buchi_Complementation.Complementation_Build RSAPSS: theory RSAPSS.Mod RSAPSS: theory RSAPSS.WordOperations RSAPSS: theory RSAPSS.Crypt RSAPSS: theory RSAPSS.Pdifference RSAPSS: theory RSAPSS.Productdivides RSAPSS: theory RSAPSS.Cryptinverts RSAPSS: theory RSAPSS.SHA1Padding RSAPSS: theory RSAPSS.Wordarith RSAPSS: theory RSAPSS.SHA1 Preparing Amicable_Numbers/document ... RSAPSS: theory RSAPSS.EMSAPSS HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Test HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message RSAPSS: theory RSAPSS.RSAPSS HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat Finished Amicable_Numbers/document (0:00:03 elapsed time) Preparing Amicable_Numbers/outline ... Finished Amicable_Numbers/outline (0:00:02 elapsed time) Timing Amicable_Numbers (8 threads, 41.752s elapsed time, 240.377s cpu time, 3.688s GC time, factor 5.76) Finished Amicable_Numbers (0:00:46 elapsed time, 0:04:04 cpu time, factor 5.29) Building Prime_Number_Theorem ... Preparing Buchi_Complementation/document ... Lambert_W: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula Latex error (line 18 of "Complementation_Build.tex"): Undefined control sequence. ...\isacharparenleft}{\kern0pt}\isactrlverbatim Failed to build document "document" Buchi_Complementation FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Buchi_Complementation) [57]) (./Complementation_Build.tex ./Complementation_Build.tex:58: Undefined control sequence. l.58 ...\isacharparenleft}{\kern0pt}\isactrlverbatim {\isasymopen}{\isachardou... Overfull \hbox (22.56604pt too wide) in paragraph at lines 57--58 [][] \T1/lmr/m/it/10 val [] $\OT1/cmr/m/n/10 =$ \T1/lmr/m/it/10 exec \T1/l mr/m/n/10 ^^N\T1/lmr/m/it/10 Com-pi-la-tion\T1/lmr/m/n/10 ^^O $\OT1/cmr/m/n/10 ($\T1/lmr/m/n/10 ^^N$\OT1/cmr/m/n/10 $$\T1/lmr/m/it/10 ISABELLE[]MLTON $\OT1/cm r/m/n/10 $$\T1/lmr/m/it/10 ISABELLE[]MLTON[]OPTIONS )) No file root.bbl. [58] (./root.aux) Package rerunfilecheck Warning: File `root.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Warning: There were undefined references. ) (see the transcript file for additional information) 421 words of node memory still in use: 3 hlist, 1 vlist, 1 rule, 2 glue, 3 kern, 1 glyph, 4 attribute, 51 glue_spec , 4 attribute_list, 1 write nodes avail lists: 2:2805,3:66,4:16,5:831,6:50,7:3716,8:10,9:362,10:7,11:101 {/usr/share/texmf/fonts/enc/dvips/lm/lm-ec.enc} Output written on root.pdf (58 pages, 447355 bytes). Transcript written on root.log. *** Latex error (line 18 of "Complementation_Build.tex"): *** Undefined control sequence. *** ...\isacharparenleft}{\kern0pt}\isactrlverbatim *** Failed to build document "document" Running Knot_Theory ... Lambert_W: theory HOL-Real_Asymp.Real_Asymp Lambert_W: theory Lambert_W.Lambert_W Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series Knot_Theory: theory HOL-Computational_Algebra.Factorial_Ring Knot_Theory: theory HOL-Computational_Algebra.Fraction_Field Knot_Theory: theory Knot_Theory.Preliminaries Knot_Theory: theory Knot_Theory.Tangle_Relation Preparing Elliptic_Curves_Group_Law/document ... Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems Knot_Theory: theory Knot_Theory.Tangles Knot_Theory: theory Knot_Theory.Tangle_Algebra Knot_Theory: theory Knot_Theory.Tangle_Moves Knot_Theory: theory Knot_Theory.Link_Algebra Preparing Lambert_W/document ... Knot_Theory: theory Knot_Theory.Example Finished Elliptic_Curves_Group_Law/document (0:00:06 elapsed time) Preparing Elliptic_Curves_Group_Law/outline ... Preparing Sturm_Sequences/document ... Finished Elliptic_Curves_Group_Law/outline (0:00:03 elapsed time) Timing Elliptic_Curves_Group_Law (8 threads, 39.284s elapsed time, 166.075s cpu time, 5.495s GC time, factor 4.23) Finished Elliptic_Curves_Group_Law (0:00:43 elapsed time, 0:02:50 cpu time, factor 3.89) Running Power_Sum_Polynomials ... Knot_Theory: theory HOL-Computational_Algebra.Polynomial Finished Lambert_W/document (0:00:06 elapsed time) Preparing Lambert_W/outline ... Finished Sturm_Sequences/document (0:00:04 elapsed time) Preparing Sturm_Sequences/outline ... Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Unsorted Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom Power_Sum_Polynomials: theory Matrix.Utility Preparing RSAPSS/document ... Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_List Finished Sturm_Sequences/outline (0:00:02 elapsed time) Preparing Sturm_Sequences/userguide ... Preparing Linear_Inequalities/document ... Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Polynomial Finished Sturm_Sequences/userguide (0:00:01 elapsed time) Timing HOL-Quotient_Examples (8 threads, 32.083s elapsed time, 46.650s cpu time, 2.085s GC time, factor 1.45) Finished HOL-Quotient_Examples (0:00:38 elapsed time, 0:00:52 cpu time, factor 1.37) Timing Sturm_Sequences (8 threads, 22.454s elapsed time, 93.318s cpu time, 1.883s GC time, factor 4.16) Finished Sturm_Sequences (0:00:41 elapsed time, 0:02:07 cpu time, factor 3.09) Running Bertrands_Postulate ... Running Koenigsberg_Friendship ... Finished Lambert_W/outline (0:00:06 elapsed time) Timing Lambert_W (8 threads, 44.777s elapsed time, 149.911s cpu time, 14.670s GC time, factor 3.35) Finished Lambert_W (0:00:50 elapsed time, 0:02:34 cpu time, factor 3.07) Running UTP ... Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Multiset Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Polynomial_Factorial Power_Sum_Polynomials: theory Polynomial_Factorization.Order_Polynomial Power_Sum_Polynomials: theory Polynomial_Factorization.Prime_Factorization Power_Sum_Polynomials: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library Finished RSAPSS/document (0:00:04 elapsed time) Preparing RSAPSS/outline ... Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom_Poly Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials Knot_Theory: theory Knot_Theory.Kauffman_Matrix Bertrands_Postulate: theory Lehmer.Lehmer Bertrands_Postulate: theory HOL-Decision_Procs.Dense_Linear_Order Koenigsberg_Friendship: theory Dijkstra_Shortest_Path.Graph Bertrands_Postulate: theory Pratt_Certificate.Pratt_Certificate Finished RSAPSS/outline (0:00:03 elapsed time) Timing RSAPSS (8 threads, 36.338s elapsed time, 75.100s cpu time, 1.607s GC time, factor 2.07) Finished RSAPSS (0:00:40 elapsed time, 0:01:19 cpu time, factor 1.95) Running QHLProver ... Power_Sum_Polynomials: theory Polynomial_Factorization.Gauss_Lemma Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph UTP: theory UTP.utp_parser_utils UTP: theory UTP.utp_var Knot_Theory: theory Knot_Theory.Computations Power_Sum_Polynomials: theory Polynomial_Factorization.Rational_Root_Test UTP: theory UTP.utp_expr Knot_Theory: theory Knot_Theory.Linkrel_Kauffman Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Puzzle Finished Linear_Inequalities/document (0:00:10 elapsed time) Preparing Linear_Inequalities/outline ... UTP: theory UTP.utp_expr_insts UTP: theory UTP.utp_expr_funcs UTP: theory UTP.utp_unrest Knot_Theory: theory Knot_Theory.Kauffman_Invariance UTP: theory UTP.utp_usedby UTP: theory UTP.utp_subst Knot_Theory: theory Knot_Theory.Knot_Theory UTP: theory UTP.utp_tactics Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge UTP: theory UTP.utp_meta_subst QHLProver: theory Deep_Learning.Tensor QHLProver: theory QHLProver.Complex_Matrix Bertrands_Postulate: theory HOL-Decision_Procs.Approximation_Bounds Finished Linear_Inequalities/outline (0:00:04 elapsed time) UTP: theory UTP.utp_pred Timing Linear_Inequalities (8 threads, 36.821s elapsed time, 146.795s cpu time, 4.532s GC time, factor 3.99) Finished Linear_Inequalities (0:01:21 elapsed time, 0:03:50 cpu time, factor 2.82) Building Prime_Distribution_Elementary ... QHLProver: theory Deep_Learning.Tensor_Subtensor QHLProver: theory Deep_Learning.Tensor_Plus QHLProver: theory Deep_Learning.Tensor_Matricization UTP: theory UTP.utp_pred_laws UTP: theory UTP.utp_alphabet Preparing Prime_Number_Theorem/document ... Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega Preparing Knot_Theory/document ... UTP: theory UTP.utp_lift Bertrands_Postulate: theory Bertrands_Postulate.Bertrand UTP: theory UTP.utp_healthy UTP: theory UTP.utp_sequent UTP: theory UTP.utp_rel QHLProver: theory QHLProver.Gates QHLProver: theory QHLProver.Matrix_Limit Finished Knot_Theory/document (0:00:05 elapsed time) Preparing Knot_Theory/outline ... Finished Prime_Number_Theorem/document (0:00:09 elapsed time) Preparing Prime_Number_Theorem/outline ... Finished Knot_Theory/outline (0:00:02 elapsed time) UTP: theory UTP.utp_recursion UTP: theory UTP.utp_state_parser Timing Knot_Theory (8 threads, 35.012s elapsed time, 193.326s cpu time, 11.022s GC time, factor 5.52) Finished Knot_Theory (0:00:38 elapsed time, 0:03:16 cpu time, factor 5.09) Running Clique_and_Monotone_Circuits ... UTP: theory UTP.utp_rel_laws QHLProver: theory QHLProver.Quantum_Program Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions Finished Prime_Number_Theorem/outline (0:00:04 elapsed time) Preparing Power_Sum_Polynomials/document ... Timing Prime_Number_Theorem (8 threads, 16.489s elapsed time, 102.928s cpu time, 2.508s GC time, factor 6.24) Finished Prime_Number_Theorem (0:00:43 elapsed time, 0:02:33 cpu time, factor 3.52) Running Gaussian_Integers ... Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries UTP: theory UTP.utp_theory UTP: theory UTP.utp_hoare UTP: theory UTP.utp_concurrency UTP: theory UTP.utp_rel_opsem UTP: theory UTP.utp_wp UTP: theory UTP.utp_sym_eval UTP: theory UTP.utp_dynlog UTP: theory UTP.utp_sp QHLProver: theory QHLProver.Partial_State QHLProver: theory QHLProver.Quantum_Hoare Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower Preparing Koenigsberg_Friendship/document ... Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower UTP: theory UTP.utp UTP: theory UTP.utp_expr_ovld UTP: theory UTP.utp_simple_time UTP: theory UTP.utp_full UTP: theory UTP.utp_easy_parser UTP: theory UTP.sum_list Finished Power_Sum_Polynomials/document (0:00:03 elapsed time) Preparing Power_Sum_Polynomials/outline ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library Gaussian_Integers: theory Matrix.Utility Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems Preparing Bertrands_Postulate/document ... Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits Gaussian_Integers: theory Polynomial_Factorization.Missing_List Finished Power_Sum_Polynomials/outline (0:00:03 elapsed time) Timing Power_Sum_Polynomials (8 threads, 33.626s elapsed time, 134.194s cpu time, 3.656s GC time, factor 3.99) Finished Power_Sum_Polynomials (0:00:37 elapsed time, 0:02:18 cpu time, factor 3.65) Running Number_Theoretic_Transform ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds Preparing UTP/document ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian QHLProver: theory QHLProver.Grover Finished Bertrands_Postulate/document (0:00:04 elapsed time) Preparing Bertrands_Postulate/outline ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds Number_Theoretic_Transform: theory Polynomial_Interpolation.Missing_Unsorted Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum Number_Theoretic_Transform: theory Polynomial_Interpolation.Ring_Hom Number_Theoretic_Transform: theory Subresultants.Binary_Exponentiation Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula Finished Koenigsberg_Friendship/document (0:00:08 elapsed time) Preparing Koenigsberg_Friendship/outline ... Finished Bertrands_Postulate/outline (0:00:03 elapsed time) Timing Bertrands_Postulate (8 threads, 31.863s elapsed time, 164.986s cpu time, 2.692s GC time, factor 5.18) Finished Bertrands_Postulate (0:00:36 elapsed time, 0:02:49 cpu time, factor 4.66) Running Three_Circles ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares Number_Theoretic_Transform: theory Polynomial_Interpolation.Missing_Polynomial Gaussian_Integers: theory Polynomial_Factorization.Missing_Multiset Gaussian_Integers: theory Polynomial_Factorization.Prime_Factorization Finished Koenigsberg_Friendship/outline (0:00:03 elapsed time) Timing Koenigsberg_Friendship (8 threads, 29.961s elapsed time, 148.570s cpu time, 5.315s GC time, factor 4.96) Finished Koenigsberg_Friendship (0:00:34 elapsed time, 0:02:32 cpu time, factor 4.43) Running Show ... Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Test Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Everything Three_Circles: theory Sturm_Tarski.PolyMisc Three_Circles: theory Polynomial_Interpolation.Missing_Unsorted Three_Circles: theory Polynomial_Interpolation.Ring_Hom Three_Circles: theory Sturm_Tarski.Sturm_Tarski Number_Theoretic_Transform: theory Polynomial_Interpolation.Ring_Hom_Poly Show: theory Show.Show Show: theory HOL-Computational_Algebra.Factorial_Ring Finished UTP/document (0:00:11 elapsed time) Preparing UTP/outline ... Number_Theoretic_Transform: theory Berlekamp_Zassenhaus.Finite_Field Number_Theoretic_Transform: theory Number_Theoretic_Transform.Preliminary_Lemmas Show: theory Show.Show_Instances Show: theory Show.Show_Real Number_Theoretic_Transform: theory Number_Theoretic_Transform.NTT Number_Theoretic_Transform: theory Number_Theoretic_Transform.Butterfly Show: theory Show.Show_Complex Show: theory Show.Show_Real_Impl Show: theory HOL-Computational_Algebra.Polynomial Three_Circles: theory Budan_Fourier.BF_Misc Finished UTP/outline (0:00:09 elapsed time) Timing UTP (8 threads, 32.227s elapsed time, 132.598s cpu time, 5.315s GC time, factor 4.11) Finished UTP (0:00:38 elapsed time, 0:02:18 cpu time, factor 3.60) Building DynamicArchitectures ... Three_Circles: theory Polynomial_Interpolation.Missing_Polynomial Preparing Clique_and_Monotone_Circuits/document ... Preparing Gaussian_Integers/document ... Three_Circles: theory Budan_Fourier.Budan_Fourier Preparing QHLProver/document ... DynamicArchitectures: theory DynamicArchitectures.Configuration_Traces Three_Circles: theory Polynomial_Interpolation.Ring_Hom_Poly Three_Circles: theory Three_Circles.RRI_Misc DynamicArchitectures: theory DynamicArchitectures.Dynamic_Architecture_Calculus Finished Gaussian_Integers/document (0:00:05 elapsed time) Preparing Gaussian_Integers/outline ... Preparing Number_Theoretic_Transform/document ... Three_Circles: theory Three_Circles.Bernstein_01 Three_Circles: theory Three_Circles.Normal_Poly Finished Clique_and_Monotone_Circuits/document (0:00:07 elapsed time) Preparing Clique_and_Monotone_Circuits/outline ... Three_Circles: theory Three_Circles.Bernstein Show: theory Show.Show_Poly Three_Circles: theory Three_Circles.Three_Circles Preparing Show/document ... Finished Gaussian_Integers/outline (0:00:03 elapsed time) Timing Gaussian_Integers (8 threads, 26.655s elapsed time, 122.143s cpu time, 2.520s GC time, factor 4.58) Finished Gaussian_Integers (0:00:31 elapsed time, 0:02:06 cpu time, factor 4.05) Running VectorSpace ... Finished Show/document (0:00:02 elapsed time) Finished Clique_and_Monotone_Circuits/outline (0:00:04 elapsed time) Preparing Show/outline ... Timing Clique_and_Monotone_Circuits (8 threads, 30.160s elapsed time, 93.174s cpu time, 2.341s GC time, factor 3.09) Finished Clique_and_Monotone_Circuits (0:00:35 elapsed time, 0:01:37 cpu time, factor 2.77) Running Zeta_3_Irrational ... Finished Number_Theoretic_Transform/document (0:00:07 elapsed time) Preparing Number_Theoretic_Transform/outline ... VectorSpace: theory VectorSpace.FunctionLemmas VectorSpace: theory VectorSpace.RingModuleFacts Finished Show/outline (0:00:02 elapsed time) Preparing Three_Circles/document ... Timing Show (8 threads, 20.433s elapsed time, 69.484s cpu time, 6.560s GC time, factor 3.40) Finished Show (0:00:24 elapsed time, 0:01:12 cpu time, factor 2.98) Running Special_Function_Bounds ... VectorSpace: theory VectorSpace.MonoidSums VectorSpace: theory VectorSpace.LinearCombinations Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega Zeta_3_Irrational: theory E_Transcendental.E_Transcendental Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds Finished QHLProver/document (0:00:17 elapsed time) Preparing QHLProver/outline ... Finished Number_Theoretic_Transform/outline (0:00:06 elapsed time) Timing Number_Theoretic_Transform (8 threads, 25.042s elapsed time, 113.938s cpu time, 3.042s GC time, factor 4.55) Finished Number_Theoretic_Transform (0:00:29 elapsed time, 0:01:58 cpu time, factor 3.99) Running Localization_Ring ... Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum Preparing Prime_Distribution_Elementary/document ... VectorSpace: theory VectorSpace.SumSpaces VectorSpace: theory VectorSpace.VectorSpace Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences Finished Three_Circles/document (0:00:10 elapsed time) Preparing Three_Circles/outline ... Localization_Ring: theory Localization_Ring.Localization Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational Finished QHLProver/outline (0:00:06 elapsed time) Timing QHLProver (8 threads, 30.358s elapsed time, 206.209s cpu time, 5.581s GC time, factor 6.79) Finished QHLProver (0:00:58 elapsed time, 0:03:34 cpu time, factor 3.67) Running Cubic_Quartic_Equations ... Finished Three_Circles/outline (0:00:04 elapsed time) Timing Three_Circles (8 threads, 20.999s elapsed time, 150.197s cpu time, 3.757s GC time, factor 7.15) Finished Three_Circles (0:00:32 elapsed time, 0:02:34 cpu time, factor 4.74) Running Interpolation_Polynomials_HOL_Algebra ... Preparing DynamicArchitectures/document ... Finished Prime_Distribution_Elementary/document (0:00:10 elapsed time) Preparing Prime_Distribution_Elementary/outline ... Preparing VectorSpace/document ... Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle Preparing Zeta_3_Irrational/document ... Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots Finished Prime_Distribution_Elementary/outline (0:00:04 elapsed time) Preparing Special_Function_Bounds/document ... Timing Prime_Distribution_Elementary (8 threads, 20.095s elapsed time, 145.777s cpu time, 3.686s GC time, factor 7.25) Finished Prime_Distribution_Elementary (0:01:09 elapsed time, 0:03:20 cpu time, factor 2.87) Running Formal_Puiseux_Series ... Finished VectorSpace/document (0:00:03 elapsed time) Preparing VectorSpace/outline ... Finished VectorSpace/outline (0:00:02 elapsed time) Timing VectorSpace (8 threads, 17.265s elapsed time, 75.956s cpu time, 3.085s GC time, factor 4.40) Finished VectorSpace (0:00:23 elapsed time, 0:01:21 cpu time, factor 3.50) Running Commuting_Hermitian ... Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Unsorted Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Laurent_Library Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom Finished DynamicArchitectures/document (0:00:08 elapsed time) Preparing DynamicArchitectures/outline ... Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities Finished Zeta_3_Irrational/document (0:00:05 elapsed time) Preparing Zeta_3_Irrational/outline ... Finished Special_Function_Bounds/document (0:00:04 elapsed time) Preparing Special_Function_Bounds/outline ... Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Polynomial Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials Preparing Localization_Ring/document ... Finished Zeta_3_Irrational/outline (0:00:03 elapsed time) Finished DynamicArchitectures/outline (0:00:04 elapsed time) Timing Zeta_3_Irrational (8 threads, 16.928s elapsed time, 116.164s cpu time, 2.324s GC time, factor 6.86) Finished Zeta_3_Irrational (0:00:21 elapsed time, 0:02:01 cpu time, factor 5.50) Timing DynamicArchitectures (8 threads, 6.012s elapsed time, 38.860s cpu time, 0.823s GC time, factor 6.46) Finished DynamicArchitectures (0:00:31 elapsed time, 0:01:21 cpu time, factor 2.59) Running Architectural_Design_Patterns ... Running Polynomial_Interpolation ... Finished Special_Function_Bounds/outline (0:00:03 elapsed time) Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom_Poly Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc Timing Special_Function_Bounds (8 threads, 16.789s elapsed time, 68.992s cpu time, 1.254s GC time, factor 4.11) Finished Special_Function_Bounds (0:00:20 elapsed time, 0:01:12 cpu time, factor 3.53) Running Budan_Fourier ... Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Polynomial_Library Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Unsorted Polynomial_Interpolation: theory Polynomial_Interpolation.Improved_Code_Equations Polynomial_Interpolation: theory Polynomial_Interpolation.Neville_Aitken_Interpolation Polynomial_Interpolation: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Polynomial_Interpolation: theory Polynomial_Interpolation.Divmod_Int Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom Finished Localization_Ring/document (0:00:04 elapsed time) Preparing Localization_Ring/outline ... Architectural_Design_Patterns: theory Architectural_Design_Patterns.Auxiliary Architectural_Design_Patterns: theory Architectural_Design_Patterns.Singleton Architectural_Design_Patterns: theory Architectural_Design_Patterns.RF_LTL Budan_Fourier: theory Sturm_Tarski.PolyMisc Architectural_Design_Patterns: theory Architectural_Design_Patterns.Publisher_Subscriber Polynomial_Interpolation: theory Polynomial_Interpolation.Is_Rat_To_Rat Budan_Fourier: theory Sturm_Tarski.Sturm_Tarski Formal_Puiseux_Series: theory Formal_Puiseux_Series.FPS_Hensel Finished Localization_Ring/outline (0:00:03 elapsed time) Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blockchain Timing Localization_Ring (8 threads, 15.680s elapsed time, 72.386s cpu time, 1.536s GC time, factor 4.62) Finished Localization_Ring (0:00:21 elapsed time, 0:01:18 cpu time, factor 3.59) Running Cayley_Hamilton ... Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Polynomial Preparing Cubic_Quartic_Equations/document ... Formal_Puiseux_Series: theory Formal_Puiseux_Series.Formal_Puiseux_Series Preparing Interpolation_Polynomials_HOL_Algebra/document ... Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix Cayley_Hamilton: theory HOL-Library.More_List Polynomial_Interpolation: theory Polynomial_Interpolation.Lagrange_Interpolation Budan_Fourier: theory Budan_Fourier.BF_Misc Finished Interpolation_Polynomials_HOL_Algebra/document (0:00:03 elapsed time) Preparing Interpolation_Polynomials_HOL_Algebra/outline ... Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom_Poly Finished Cubic_Quartic_Equations/document (0:00:05 elapsed time) Preparing Cubic_Quartic_Equations/outline ... Finished Interpolation_Polynomials_HOL_Algebra/outline (0:00:02 elapsed time) Timing Interpolation_Polynomials_HOL_Algebra (8 threads, 15.618s elapsed time, 41.461s cpu time, 2.401s GC time, factor 2.65) Finished Interpolation_Polynomials_HOL_Algebra (0:00:21 elapsed time, 0:00:47 cpu time, factor 2.18) Running Stream_Fusion_Code ... Budan_Fourier: theory Budan_Fourier.Budan_Fourier Budan_Fourier: theory Budan_Fourier.Sturm_Multiple_Roots Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blackboard Polynomial_Interpolation: theory Polynomial_Interpolation.Newton_Interpolation Finished Cubic_Quartic_Equations/outline (0:00:03 elapsed time) Timing Cubic_Quartic_Equations (8 threads, 15.645s elapsed time, 48.543s cpu time, 1.948s GC time, factor 3.10) Finished Cubic_Quartic_Equations (0:00:24 elapsed time, 0:00:57 cpu time, factor 2.34) Building HOL-Nonstandard_Analysis ... Budan_Fourier: theory Budan_Fourier.Descartes_Roots_Test Preparing Formal_Puiseux_Series/document ... Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion Polynomial_Interpolation: theory Polynomial_Interpolation.Polynomial_Interpolation Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef Preparing Polynomial_Interpolation/document ... Finished Formal_Puiseux_Series/document (0:00:06 elapsed time) Preparing Formal_Puiseux_Series/outline ... Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA Preparing Commuting_Hermitian/document ... Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples Finished Formal_Puiseux_Series/outline (0:00:04 elapsed time) Timing Formal_Puiseux_Series (8 threads, 14.564s elapsed time, 57.305s cpu time, 1.612s GC time, factor 3.93) Finished Formal_Puiseux_Series (0:00:25 elapsed time, 0:01:01 cpu time, factor 2.40) Running Sturm_Tarski ... Finished Polynomial_Interpolation/document (0:00:07 elapsed time) Preparing Polynomial_Interpolation/outline ... Preparing Budan_Fourier/document ... Preparing Stream_Fusion_Code/document ... HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv Preparing Architectural_Design_Patterns/document ... Sturm_Tarski: theory Sturm_Tarski.PolyMisc HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries Sturm_Tarski: theory Sturm_Tarski.Sturm_Tarski HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental Finished Polynomial_Interpolation/outline (0:00:04 elapsed time) Timing Polynomial_Interpolation (8 threads, 13.433s elapsed time, 66.938s cpu time, 2.031s GC time, factor 4.98) Finished Polynomial_Interpolation (0:00:21 elapsed time, 0:01:10 cpu time, factor 3.26) Running Pell ... HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton Finished Commuting_Hermitian/document (0:00:05 elapsed time) Preparing Commuting_Hermitian/outline ... HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis Finished Budan_Fourier/document (0:00:05 elapsed time) Preparing Budan_Fourier/outline ... Preparing Cayley_Hamilton/document ... Pell: theory Pell.Efficient_Discrete_Sqrt Pell: theory Pell.Pell Finished Stream_Fusion_Code/document (0:00:06 elapsed time) Preparing Stream_Fusion_Code/outline ... Finished Commuting_Hermitian/outline (0:00:02 elapsed time) Timing Commuting_Hermitian (8 threads, 13.435s elapsed time, 89.769s cpu time, 2.299s GC time, factor 6.68) Finished Commuting_Hermitian (0:00:32 elapsed time, 0:01:35 cpu time, factor 2.89) Running IMO2019 ... Pell: theory Pell.Pell_Algorithm Finished Budan_Fourier/outline (0:00:03 elapsed time) Timing Budan_Fourier (8 threads, 11.942s elapsed time, 74.625s cpu time, 1.306s GC time, factor 6.25) Finished Budan_Fourier (0:00:28 elapsed time, 0:01:18 cpu time, factor 2.74) Running Euler_MacLaurin ... Finished Cayley_Hamilton/document (0:00:03 elapsed time) Preparing Cayley_Hamilton/outline ... Pell: theory Pell.Pell_Algorithm_Test Finished Cayley_Hamilton/outline (0:00:02 elapsed time) Finished Architectural_Design_Patterns/document (0:00:09 elapsed time) Preparing Architectural_Design_Patterns/outline ... IMO2019: theory IMO2019.IMO2019_Q5 IMO2019: theory IMO2019.IMO2019_Q1 Timing Cayley_Hamilton (8 threads, 10.676s elapsed time, 49.314s cpu time, 1.533s GC time, factor 4.62) Finished Cayley_Hamilton (0:00:29 elapsed time, 0:00:52 cpu time, factor 1.82) Running Finitely_Generated_Abelian_Groups ... IMO2019: theory IMO2019.IMO2019_Q4 Preparing Sturm_Tarski/document ... Finished Stream_Fusion_Code/outline (0:00:05 elapsed time) Euler_MacLaurin: theory HOL-Library.Function_Algebras Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin Euler_MacLaurin: theory Landau_Symbols.Group_Sort Timing Stream_Fusion_Code (8 threads, 9.830s elapsed time, 46.500s cpu time, 1.264s GC time, factor 4.73) Finished Stream_Fusion_Code (0:00:15 elapsed time, 0:00:50 cpu time, factor 3.17) Running Jordan_Hoelder ... Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products Finished Architectural_Design_Patterns/outline (0:00:04 elapsed time) Preparing Pell/document ... Finished Sturm_Tarski/document (0:00:04 elapsed time) Preparing Sturm_Tarski/outline ... Timing Architectural_Design_Patterns (8 threads, 13.835s elapsed time, 70.531s cpu time, 2.761s GC time, factor 5.10) Finished Architectural_Design_Patterns (0:00:31 elapsed time, 0:01:14 cpu time, factor 2.34) Running Pratt_Certificate ... Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend Jordan_Hoelder: theory Secondary_Sylow.GroupAction Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds Finished Sturm_Tarski/outline (0:00:02 elapsed time) Euler_MacLaurin: theory Landau_Symbols.Landau_More Timing Sturm_Tarski (8 threads, 8.990s elapsed time, 46.494s cpu time, 0.721s GC time, factor 5.17) Finished Sturm_Tarski (0:00:12 elapsed time, 0:00:49 cpu time, factor 3.87) Running Orbit_Stabiliser ... Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau Finished Pell/document (0:00:04 elapsed time) Preparing Pell/outline ... Pratt_Certificate: theory Lehmer.Lehmer Preparing IMO2019/document ... Jordan_Hoelder: theory Secondary_Sylow.SndSylow Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate Preparing HOL-Nonstandard_Analysis/document ... Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups Preparing Euler_MacLaurin/document ... Finished Pell/outline (0:00:03 elapsed time) Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups Timing Pell (8 threads, 9.147s elapsed time, 46.793s cpu time, 0.808s GC time, factor 5.12) Finished Pell (0:00:12 elapsed time, 0:00:50 cpu time, factor 3.93) Running Nullstellensatz ... Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations Finished IMO2019/document (0:00:03 elapsed time) Preparing IMO2019/outline ... Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups Finished IMO2019/outline (0:00:02 elapsed time) Finished Euler_MacLaurin/document (0:00:05 elapsed time) Preparing Euler_MacLaurin/outline ... Timing IMO2019 (8 threads, 8.805s elapsed time, 15.813s cpu time, 0.209s GC time, factor 1.80) Finished IMO2019 (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.48) Running Fermat3_4 ... Preparing Jordan_Hoelder/document ... Finished HOL-Nonstandard_Analysis/document (0:00:07 elapsed time) Preparing HOL-Nonstandard_Analysis/outline ... Preparing Pratt_Certificate/document ... Preparing Finitely_Generated_Abelian_Groups/document ... Finished Euler_MacLaurin/outline (0:00:03 elapsed time) Timing Euler_MacLaurin (8 threads, 7.936s elapsed time, 46.977s cpu time, 1.454s GC time, factor 5.92) Finished Euler_MacLaurin (0:00:13 elapsed time, 0:00:51 cpu time, factor 3.87) Running Comparison_Sort_Lower_Bound ... Fermat3_4: theory Fermat3_4.Fermat4 Fermat3_4: theory Fermat3_4.Quad_Form Preparing Orbit_Stabiliser/document ... Fermat3_4: theory Fermat3_4.Fermat3 Finished Pratt_Certificate/document (0:00:03 elapsed time) Preparing Pratt_Certificate/outline ... Nullstellensatz: theory Nullstellensatz.Lex_Order_PP Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields Nullstellensatz: theory Nullstellensatz.Univariate_PM Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets Finished HOL-Nonstandard_Analysis/outline (0:00:05 elapsed time) Timing HOL-Nonstandard_Analysis (8 threads, 7.651s elapsed time, 36.928s cpu time, 1.307s GC time, factor 4.83) Finished HOL-Nonstandard_Analysis (0:00:34 elapsed time, 0:01:14 cpu time, factor 2.16) Running HOL-Isar_Examples ... Finished Jordan_Hoelder/document (0:00:05 elapsed time) Preparing Jordan_Hoelder/outline ... Nullstellensatz: theory Nullstellensatz.Nullstellensatz Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations Comparison_Sort_Lower_Bound: theory List-Index.List_Index Finished Orbit_Stabiliser/document (0:00:03 elapsed time) Preparing Orbit_Stabiliser/outline ... Finished Pratt_Certificate/outline (0:00:03 elapsed time) Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations Timing Pratt_Certificate (8 threads, 8.106s elapsed time, 38.219s cpu time, 0.581s GC time, factor 4.71) Finished Pratt_Certificate (0:00:13 elapsed time, 0:00:42 cpu time, factor 3.19) Running LP_Duality ... Finished Jordan_Hoelder/outline (0:00:02 elapsed time) HOL-Isar_Examples: theory HOL-Isar_Examples.Expr_Compiler HOL-Isar_Examples: theory HOL-Isar_Examples.Group HOL-Isar_Examples: theory HOL-Isar_Examples.Basic_Logic HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Context HOL-Isar_Examples: theory HOL-Hoare.Hoare_Tac HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Notepad HOL-Isar_Examples: theory HOL-Isar_Examples.Puzzle HOL-Isar_Examples: theory HOL-Isar_Examples.Mutilated_Checkerboard Timing Jordan_Hoelder (8 threads, 7.678s elapsed time, 46.111s cpu time, 1.724s GC time, factor 6.01) Finished Jordan_Hoelder (0:00:15 elapsed time, 0:00:52 cpu time, factor 3.33) HOL-Isar_Examples: theory HOL-Isar_Examples.Structured_Statements HOL-Isar_Examples: theory HOL-Isar_Examples.Summation Running SumSquares ... Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound HOL-Isar_Examples: theory HOL-Isar_Examples.Fibonacci Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field Finished Orbit_Stabiliser/outline (0:00:02 elapsed time) Preparing Fermat3_4/document ... Timing Orbit_Stabiliser (8 threads, 6.710s elapsed time, 23.350s cpu time, 0.562s GC time, factor 3.48) Finished Orbit_Stabiliser (0:00:12 elapsed time, 0:00:29 cpu time, factor 2.28) Running Topology ... Finished Finitely_Generated_Abelian_Groups/document (0:00:09 elapsed time) Preparing Finitely_Generated_Abelian_Groups/outline ... HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare_Ex Preparing Comparison_Sort_Lower_Bound/document ... SumSquares: theory SumSquares.FourSquares SumSquares: theory SumSquares.TwoSquares Preparing Nullstellensatz/document ... Topology: theory Topology.Topology Topology: theory Lazy-Lists-II.LList2 Preparing HOL-Isar_Examples/document ... Finished Finitely_Generated_Abelian_Groups/outline (0:00:04 elapsed time) Timing Finitely_Generated_Abelian_Groups (8 threads, 7.903s elapsed time, 51.859s cpu time, 2.709s GC time, factor 6.56) Finished Finitely_Generated_Abelian_Groups (0:00:18 elapsed time, 0:00:57 cpu time, factor 3.22) Running Arith_Prog_Rel_Primes ... Finished Comparison_Sort_Lower_Bound/document (0:00:03 elapsed time) Preparing Comparison_Sort_Lower_Bound/outline ... Finished Fermat3_4/document (0:00:05 elapsed time) Preparing Fermat3_4/outline ... Topology: theory Topology.LList_Topology LP_Duality: theory LP_Duality.Minimum_Maximum LP_Duality: theory LP_Duality.LP_Duality Preparing SumSquares/document ... Finished Comparison_Sort_Lower_Bound/outline (0:00:02 elapsed time) Timing Comparison_Sort_Lower_Bound (8 threads, 5.317s elapsed time, 19.295s cpu time, 0.605s GC time, factor 3.63) Finished Comparison_Sort_Lower_Bound (0:00:10 elapsed time, 0:00:23 cpu time, factor 2.37) Running Secondary_Sylow ... Finished HOL-Isar_Examples/document (0:00:04 elapsed time) Preparing HOL-Isar_Examples/outline ... Finished Nullstellensatz/document (0:00:05 elapsed time) Preparing Nullstellensatz/outline ... Preparing Topology/document ... Finished Fermat3_4/outline (0:00:03 elapsed time) Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes Timing Fermat3_4 (8 threads, 6.163s elapsed time, 42.273s cpu time, 0.988s GC time, factor 6.86) Finished Fermat3_4 (0:00:10 elapsed time, 0:00:46 cpu time, factor 4.39) Running Mason_Stothers ... Finished SumSquares/document (0:00:03 elapsed time) Preparing SumSquares/outline ... Finished HOL-Isar_Examples/outline (0:00:03 elapsed time) Finished Nullstellensatz/outline (0:00:03 elapsed time) Timing HOL-Isar_Examples (8 threads, 4.943s elapsed time, 12.806s cpu time, 0.284s GC time, factor 2.59) Finished HOL-Isar_Examples (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.87) Timing Nullstellensatz (8 threads, 6.483s elapsed time, 22.508s cpu time, 0.915s GC time, factor 3.47) Finished Nullstellensatz (0:00:17 elapsed time, 0:00:32 cpu time, factor 1.84) Running Lazy-Lists-II ... Running Irrationals_From_THEBOOK ... Mason_Stothers: theory Mason_Stothers.Mason_Stothers Preparing LP_Duality/document ... Finished Topology/document (0:00:04 elapsed time) Preparing Topology/outline ... Preparing Arith_Prog_Rel_Primes/document ... Secondary_Sylow: theory Secondary_Sylow.GroupAction Finished SumSquares/outline (0:00:02 elapsed time) Timing SumSquares (8 threads, 4.220s elapsed time, 25.471s cpu time, 0.356s GC time, factor 6.04) Finished SumSquares (0:00:08 elapsed time, 0:00:29 cpu time, factor 3.38) Running HOL-Nonstandard_Analysis-Examples ... Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation Secondary_Sylow: theory Secondary_Sylow.SndSylow Preparing Mason_Stothers/document ... Lazy-Lists-II: theory Lazy-Lists-II.LList2 Finished LP_Duality/document (0:00:03 elapsed time) Preparing LP_Duality/outline ... Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK Finished Topology/outline (0:00:03 elapsed time) Finished Arith_Prog_Rel_Primes/document (0:00:03 elapsed time) Preparing Arith_Prog_Rel_Primes/outline ... Timing Topology (8 threads, 4.083s elapsed time, 18.107s cpu time, 0.933s GC time, factor 4.43) Finished Topology (0:00:08 elapsed time, 0:00:22 cpu time, factor 2.70) Running Descartes_Sign_Rule ... HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes Preparing Secondary_Sylow/document ... Finished Mason_Stothers/document (0:00:02 elapsed time) Preparing Mason_Stothers/outline ... Preparing Lazy-Lists-II/document ... Preparing Irrationals_From_THEBOOK/document ... Finished LP_Duality/outline (0:00:02 elapsed time) Timing LP_Duality (8 threads, 4.582s elapsed time, 15.328s cpu time, 0.172s GC time, factor 3.35) Finished LP_Duality (0:00:14 elapsed time, 0:00:25 cpu time, factor 1.71) Running Perfect-Number-Thm ... Finished Arith_Prog_Rel_Primes/outline (0:00:02 elapsed time) Timing Arith_Prog_Rel_Primes (8 threads, 3.155s elapsed time, 17.857s cpu time, 0.290s GC time, factor 5.66) Finished Arith_Prog_Rel_Primes (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.81) Running Liouville_Numbers ... Timing HOL-Nonstandard_Analysis-Examples (8 threads, 1.613s elapsed time, 4.096s cpu time, 0.000s GC time, factor 2.54) Finished HOL-Nonstandard_Analysis-Examples (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.40) Running Lucas_Theorem ... Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule Finished Secondary_Sylow/document (0:00:02 elapsed time) Preparing Secondary_Sylow/outline ... Finished Mason_Stothers/outline (0:00:02 elapsed time) Timing Mason_Stothers (8 threads, 1.847s elapsed time, 7.618s cpu time, 0.146s GC time, factor 4.12) Finished Mason_Stothers (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.04) Running Lifting_the_Exponent ... Finished Irrationals_From_THEBOOK/document (0:00:02 elapsed time) Preparing Irrationals_From_THEBOOK/outline ... Finished Lazy-Lists-II/document (0:00:03 elapsed time) Preparing Lazy-Lists-II/outline ... Preparing Descartes_Sign_Rule/document ... Finished Secondary_Sylow/outline (0:00:01 elapsed time) Timing Secondary_Sylow (8 threads, 2.866s elapsed time, 17.923s cpu time, 0.562s GC time, factor 6.25) Finished Secondary_Sylow (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.65) Running Lehmer ... Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem Finished Irrationals_From_THEBOOK/outline (0:00:02 elapsed time) Timing Irrationals_From_THEBOOK (8 threads, 1.604s elapsed time, 9.058s cpu time, 0.089s GC time, factor 5.65) Finished Irrationals_From_THEBOOK (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.16) Preparing Liouville_Numbers/document ... Finished Lazy-Lists-II/outline (0:00:02 elapsed time) Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics Timing Lazy-Lists-II (8 threads, 1.702s elapsed time, 5.483s cpu time, 0.000s GC time, factor 3.22) Finished Lazy-Lists-II (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.64) Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma Preparing Lucas_Theorem/document ... Lifting_the_Exponent: theory Lifting_the_Exponent.LTE Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect Finished Descartes_Sign_Rule/document (0:00:03 elapsed time) Preparing Descartes_Sign_Rule/outline ... Lehmer: theory Lehmer.Lehmer Preparing Perfect-Number-Thm/document ... Preparing Lifting_the_Exponent/document ... Finished Liouville_Numbers/document (0:00:02 elapsed time) Preparing Liouville_Numbers/outline ... Finished Lucas_Theorem/document (0:00:02 elapsed time) Preparing Lucas_Theorem/outline ... Finished Descartes_Sign_Rule/outline (0:00:02 elapsed time) Timing Descartes_Sign_Rule (8 threads, 1.427s elapsed time, 8.689s cpu time, 0.113s GC time, factor 6.09) Finished Descartes_Sign_Rule (0:00:05 elapsed time, 0:00:12 cpu time, factor 2.38) Preparing Lehmer/document ... Finished Perfect-Number-Thm/document (0:00:02 elapsed time) Preparing Perfect-Number-Thm/outline ... Finished Liouville_Numbers/outline (0:00:02 elapsed time) Timing Liouville_Numbers (8 threads, 1.220s elapsed time, 4.850s cpu time, 0.000s GC time, factor 3.98) Finished Liouville_Numbers (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.71) Finished Lucas_Theorem/outline (0:00:02 elapsed time) Timing Lucas_Theorem (8 threads, 1.262s elapsed time, 6.591s cpu time, 0.115s GC time, factor 5.22) Finished Lucas_Theorem (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.08) Finished Lifting_the_Exponent/document (0:00:03 elapsed time) Preparing Lifting_the_Exponent/outline ... Finished Lehmer/document (0:00:02 elapsed time) Preparing Lehmer/outline ... Finished Perfect-Number-Thm/outline (0:00:02 elapsed time) Timing Perfect-Number-Thm (8 threads, 1.477s elapsed time, 5.687s cpu time, 0.000s GC time, factor 3.85) Finished Perfect-Number-Thm (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.54) Finished Lehmer/outline (0:00:02 elapsed time) Finished Lifting_the_Exponent/outline (0:00:02 elapsed time) Timing Lehmer (8 threads, 1.136s elapsed time, 3.373s cpu time, 0.000s GC time, factor 2.97) Finished Lehmer (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.37) Timing Lifting_the_Exponent (8 threads, 1.189s elapsed time, 6.415s cpu time, 0.100s GC time, factor 5.40) Finished Lifting_the_Exponent (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.89) Unfinished session(s): Buchi_Complementation, PAC_Checker === TIMING === Group AFP: 3:34:46 elapsed time, 11:55:34 cpu time, factor 3.33 Group main: 0:09:57 elapsed time, 0:23:34 cpu time, factor 2.37 Group large: 0:00:00 elapsed time Group no_doc: 0:00:00 elapsed time Group doc: 0:00:00 elapsed time Group timing: 0:20:43 elapsed time, 1:11:41 cpu time, factor 3.46 Overall: 0:35:40 elapsed time, 13:25:36 cpu time, factor 22.59 === FAILED SESSIONS === Session Buchi_Complementation: FAILED 1 Session PAC_Checker: FAILED 1 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === REPORT === Writing report file ... === SITEGEN === Writing status file ... Running sitegen ... === NOTIFICATIONS === === COMPLETED === Build step 'Execute shell' marked build as failure Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 1 second No emails were triggered. Finished: FAILURE