diff --git a/thys/Lifting_the_Exponent/LTE.thy b/thys/Lifting_the_Exponent/LTE.thy new file mode 100644 --- /dev/null +++ b/thys/Lifting_the_Exponent/LTE.thy @@ -0,0 +1,418 @@ +theory LTE + imports + "HOL-Number_Theory.Number_Theory" +begin + +section "Library additions" + +lemma cong_sum_mono_neutral_right: + assumes "finite T" + assumes "S \ T" + assumes zeros: "\i \ T - S. [g i = 0] (mod n)" + shows "[sum g T = sum g S] (mod n)" +proof - + have "[sum g T = (\x\T. if x \ S then g x else 0)] (mod n)" + using zeros by (auto intro: cong_sum) + also have "(\x\T. if x \ S then g x else 0) = (\x\S. if x \ S then g x else 0)" + by (intro sum.mono_neutral_right; fact?; auto) + also have "... = sum g S" + by (auto intro: sum.cong) + finally show ?thesis. +qed + +lemma power_odd_inj: + fixes a b :: "'a::linordered_idom" + assumes "odd k" and "a^k = b^k" + shows "a = b" +proof (cases "a \ 0") + case True + then have "b \ 0" + using assms zero_le_odd_power by metis + moreover from `odd k` have "k > 0" by presburger + show ?thesis + by (rule power_eq_imp_eq_base; fact) +next + case False + then have "b < 0" + using assms power_less_zero_eq not_less by metis + from `a^k = b^k` have "(-a)^k = (-b)^k" + using `odd k` power_minus_odd by simp + moreover have "-a \ 0" and "-b \ 0" + using `\ a \ 0` and `b < 0` by auto + moreover from `odd k` have "k > 0" by presburger + ultimately have "-a = -b" by (rule power_eq_imp_eq_base) + then show ?thesis by simp +qed + +lemma power_eq_abs: + fixes a b :: "'a::linordered_idom" + assumes "a^k = b^k" and "k > 0" + shows "\a\ = \b\" +proof - + from `a^k = b^k` have "\a\^k = \b\^k" + using power_abs by metis + show "\a\ = \b\" + by (rule power_eq_imp_eq_base; fact?; auto) +qed + +lemma cong_scale: + "k \ 0 \ [a = b] (mod c) \ [k*a = k*b] (mod k*c)" + unfolding cong_def by auto + +lemma odd_square_mod_4: + fixes x :: int + assumes "odd x" + shows "[x^2 = 1] (mod 4)" +proof - + have "x^2 - 1 = (x - 1) * (x + 1)" + by (simp add: ring_distribs power2_eq_square) + moreover from `odd x` have "2 dvd x - 1" and "2 dvd x + 1" + by auto + ultimately have "4 dvd x^2 - 1" + by fastforce + thus ?thesis + by (simp add: cong_iff_dvd_diff) +qed + +section \The \p > 2\ case\ + +context + fixes x y :: int and p :: nat + assumes "prime p" + assumes "p dvd x - y" + assumes "\p dvd x" "\p dvd y" +begin + +lemma decompose_mod_p: + "[(\iiiiLemma 1:\ + +lemma multiplicity_diff_pow_coprime: + assumes "coprime p n" + shows "multiplicity p (x^n - y^n) = multiplicity p (x - y)" +proof - + have factor: "x^n - y^n = (\i p dvd (\ii p dvd x^(n-1)" + by (simp add: prime_dvd_mult_eq_int) + moreover from `coprime p n` and `prime p` have "\p dvd n" + using coprime_absorb_right not_prime_unit by auto + ultimately have "p dvd x^(n-1)" + by simp + hence "p dvd x" + using `prime p` prime_dvd_power_int prime_nat_int_transfer by blast + with `\p dvd x` show False by simp + qed + ultimately show "multiplicity p (x^n - y^n) = multiplicity p (x - y)" + using `prime p` + by (auto intro: multiplicity_prime_elem_times_other) +qed + +text \The inductive step:\ + +lemma multiplicity_diff_self_pow: + assumes "p > 2" and "x \ y" + shows "multiplicity p (x^p - y^p) = Suc (multiplicity p (x - y))" +proof - + have *: "multiplicity p (\itii\t. (t choose i) * (k*p)^i * y^(t-i))" + by (simp flip: binomial_ring add: add.commute) + also have "[... = y^(p - Suc t) * (\i\1. (t choose i) * (k*p)^i * y^(t-i))] (mod p^2)" + \ \discard \i > 1\\ + proof (intro cong_scalar_left cong_sum_mono_neutral_right; rule) + fix i + assume "i \ {..t} - {..1}" + then have "i \ 2" by simp + then obtain i' where "i = i' + 2" + using add.commute le_Suc_ex by blast + hence "(k*p)^i = (k*p)^i' * k^2 * p^2" + by (simp add: ac_simps power2_eq_square) + hence "[(k*p)^i = 0] (mod p^2)" + by (simp add: cong_mult_self_right) + thus "[(t choose i) * (k*p)^i * y^(t-i) = 0] (mod p^2)" + by (simp add: cong_0_iff) + qed (use `t \ 0` in auto) + also have "(\i\1. (t choose i) * (k*p)^i * y^(t-i)) = y^t + t*k*p*y^(t-1)" + by simp + also have "y^(p - Suc t) * ... = y^(p-1) + t*k*p*y^(p-2)" + using `t < p` `t \ 0` by (auto simp add: algebra_simps numeral_eq_Suc simp flip: power_add) + finally show ?thesis. + qed simp + + hence "[(\tttttt 2` and `prime p` have "odd p" + using prime_odd_nat by blast + thus ?thesis + by (metis (no_types, lifting) cong_0_iff div_mult_swap dvd_times_left_cancel_iff + dvd_triv_left le_0_eq linorder_not_less mult.commute odd_pos odd_two_times_div_two_nat + one_add_one power_add power_one_right) + qed + hence "[int ((p*(p - 1) div 2) * p)*k*y^(p-2) = 0] (mod p^2)" + unfolding cong_0_iff using int_dvd_int_iff by fastforce + thus ?thesis + by (simp add: ac_simps) + qed + ultimately have "[(\t p^2 dvd p*y^(p-1)" + using `p > 2` `prime p` `\ p dvd y` by (simp add: power2_eq_square prime_dvd_power_int_iff) + ultimately show "\ int p^(Suc 1) dvd (\ti y` multiplicity_zero * by auto + ultimately show ?thesis by simp +qed + +text \Theorem 1:\ + +theorem multiplicity_diff_pow: + assumes "p > 2" and "x \ y" and "n > 0" + shows "multiplicity p (x^n - y^n) = multiplicity p (x - y) + multiplicity p n" +proof - + obtain k where n: "n = p^multiplicity p n * k" and "\ p dvd k" + using `n > 0` `prime p` + by (metis neq0_conv not_prime_unit multiplicity_decompose') + have "multiplicity p (x^(p^a * k) - y^(p^a * k)) = multiplicity p (x - y) + a" for a + proof (induction a) + case 0 + from `\ p dvd k` have "coprime p k" + using `prime p` by (intro prime_imp_coprime) + thus ?case + by (simp add: multiplicity_diff_pow_coprime) + next + case (Suc a) + let ?x' = "x^(p^a*k)" and ?y' = "y^(p^a*k)" + have "\ p dvd ?x'" and "\ p dvd ?y'" + using `\ p dvd x` `\ p dvd y` and `prime p` + by (meson prime_dvd_power prime_nat_int_transfer)+ + moreover have "p dvd ?x' - ?y'" + using `p dvd x - y` by (simp add: power_diff_sumr2) + moreover have "?x' \ ?y'" + proof + assume "?x' = ?y'" + moreover have "0 < p^a * k" + using `prime p` `n > 0` n + by (metis gr0I mult_is_0 power_not_zero prime_gt_0_nat) + ultimately have "\x\ = \y\" + by (intro power_eq_abs) + with `x \ y` have "x = -y" + using abs_eq_iff by simp + with `p dvd x - y` have "p dvd 2*x" + by simp + with `prime p` have "p dvd 2 \ p dvd x" + by (metis int_dvd_int_iff of_nat_numeral prime_dvd_mult_iff prime_nat_int_transfer) + with `p > 2` have "p dvd x" + by auto + with `\ p dvd x` show False.. + qed + moreover have "p^Suc a * k = p^a * k * p" + by (simp add: ac_simps) + ultimately show ?case + using LTE.multiplicity_diff_self_pow[where x="?x'" and y="?y'", OF `prime p`] `p > 2` + and Suc.IH + by (metis add_Suc_right power_mult) + qed + with n show ?thesis by metis +qed + +end + +text \Theorem 2:\ + +corollary multiplicity_add_pow: + fixes x y :: int and p n :: nat + assumes "odd n" + and "prime p" and "p > 2" + and "p dvd x + y" and "\ p dvd x" "\ p dvd y" + and "x \ -y" + shows "multiplicity p (x^n + y^n) = multiplicity p (x + y) + multiplicity p n" +proof - + have [simp]: "(-y)^n = -(y^n)" + using `odd n` by (rule power_minus_odd) + moreover have "n > 0" + using `odd n` by presburger + with assms show ?thesis + using multiplicity_diff_pow[where x=x and y="-y" and n=n] + by simp +qed + +section \The \p = 2\ case\ + +text \Theorem 3:\ + +theorem multiplicity_2_diff_pow_4div: + fixes x y :: int + assumes "odd x" "odd y" and "4 dvd x - y" and "n > 0" "x \ y" + shows "multiplicity 2 (x^n - y^n) = multiplicity 2 (x - y) + multiplicity 2 n" +proof - + have "prime (2::nat)" by simp + then obtain k where n: "n = 2^multiplicity 2 n * k" and "\ 2 dvd k" + using `n > 0` + by (metis neq0_conv not_prime_unit multiplicity_decompose') + + have pow2: "multiplicity 2 (x^(2^k) - y^(2^k)) = multiplicity 2 (x - y) + k" for k + proof (induction k) + case (Suc k) + have "x^(2^Suc k) - y^(2^Suc k) = (x^2^k)^2 - (y^2^k)^2" + by (simp flip: power_mult algebra_simps) + also have "... = (x^2^k - y^2^k)*(x^2^k + y^2^k)" + by (simp add: power2_eq_square algebra_simps) + finally have factor: "x^(2^Suc k) - y^(2^Suc k) = (x^2^k - y^2^k)*(x^2^k + y^2^k)". + moreover have m_plus: "multiplicity 2 (x^2^k + y^2^k) = 1" + proof (rule multiplicity_eqI) + show "2^1 dvd x^2^k + y^2^k" + using `odd x` and `odd y` by simp + + have "[x^2^k + y^2^k = 2] (mod 4)" + proof (cases k) + case 0 + from `odd y` have "[y = 1] (mod 2)" + using cong_def by fastforce + hence "[2*y = 2] (mod 4)" + using cong_scale[where k=2 and b=1 and c=2, simplified] by force + moreover from `4 dvd x - y` have "[x - y = 0] (mod 4)" + by (simp add: cong_0_iff) + ultimately have "[x + y = 2] (mod 4)" + by (smt cong_add) + with `k = 0` show ?thesis by simp + next + case (Suc k') + then have "[x^2^k = 1] (mod 4)" and "[y^2^k = 1] (mod 4)" + using `odd x` `odd y` + by (auto simp add: power_mult power_Suc2 simp del: power_Suc intro: odd_square_mod_4) + thus "[x^2^k + y^2^k = 2] (mod 4)" + by (smt cong_add) + qed + thus "\ 2^Suc 1 dvd x^2^k + y^2^k" + by (simp add: cong_dvd_iff) + qed + moreover have "x^2^k + y^2^k \ 0" + using m_plus multiplicity_zero by auto + moreover have "x^2^k - y^2^k \ 0" + proof + assume "x^2^k - y^2^k = 0" + then have "\x\ = \y\" + by (intro power_eq_abs, simp, simp) + hence "x = y \ x = -y" + using abs_eq_iff by auto + with `x \ y` have "x = -y" + by simp + with `4 dvd x - y` have "4 dvd 2*x" + by simp + hence "2 dvd x" + by auto + with `odd x` show False.. + qed + ultimately have "multiplicity 2 (x^2^Suc k - y^2^Suc k) = + multiplicity 2 (x^2^k - y^2^k) + multiplicity 2 (x^2^k + y^2^k)" + by (unfold factor; intro prime_elem_multiplicity_mult_distrib; auto) + then show ?case + using m_plus Suc.IH by simp + qed simp + + moreover have even_diff: "int 2 dvd x^2^multiplicity 2 n - y^2^multiplicity 2 n" + using `odd x` and `odd y` by simp + moreover have odd_parts: "\ int 2 dvd x^2^multiplicity 2 n" "\ int 2 dvd y^2^multiplicity 2 n" + using `odd x` and `odd y` by simp+ + moreover have coprime: "coprime 2 k" + using `\ 2 dvd k` by simp + + show ?thesis + apply (subst (1) n) + apply (subst (2) n) + apply (simp only: power_mult) + apply (simp only: multiplicity_diff_pow_coprime[OF `prime 2` even_diff odd_parts coprime, simplified]) + by (rule pow2) +qed + +text \Theorem 4:\ + +theorem multiplicity_2_diff_even_pow: + fixes x y :: int + assumes "odd x" "odd y" and "even n" and "n > 0" and "\x\ \ \y\" + shows "multiplicity 2 (x^n - y^n) = multiplicity 2 (x - y) + multiplicity 2 (x + y) + multiplicity 2 n - 1" +proof - + obtain n' where "n = 2*n'" + using `even n` by auto + with `n > 0` have "n' > 0" by simp + + moreover have "4 dvd x^2 - y^2" + proof - + have "x^2 - y^2 = (x + y) * (x - y)" + by (simp add: algebra_simps power2_eq_square) + moreover have "2 dvd x + y" and "2 dvd x - y" + using `odd x` and `odd y` by auto + ultimately show "4 dvd x^2 - y^2" by fastforce + qed + + moreover have "odd (x^2)" and "odd (y^2)" + using `odd x` `odd y` by auto + moreover from `\x\ \ \y\` have "x^2 \ y^2" + using diff_0 diff_0_right power2_eq_iff by fastforce + + ultimately have "multiplicity 2 ((x^2)^n' - (y^2)^n') = multiplicity 2 (x^2 - y^2) + multiplicity 2 n'" + by (intro multiplicity_2_diff_pow_4div) + also have "multiplicity 2 ((x^2)^n' - (y^2)^n') = multiplicity 2 (x^n - y^n)" + unfolding `n = 2*n'` by (simp add: power_mult) + also have "multiplicity 2 (x^2 - y^2) = multiplicity 2 ((x - y) * (x + y))" + by (simp add: algebra_simps power2_eq_square) + also have "... = multiplicity 2 (x - y) + multiplicity 2 (x + y)" + using `\x\ \ \y\` by (auto intro: prime_elem_multiplicity_mult_distrib) + also have "multiplicity 2 n = Suc (multiplicity 2 n')" + unfolding `n = 2*n'` using `n' > 0` by (simp add: multiplicity_times_same) + ultimately show ?thesis by simp +qed + +end \ No newline at end of file diff --git a/thys/Lifting_the_Exponent/ROOT b/thys/Lifting_the_Exponent/ROOT new file mode 100644 --- /dev/null +++ b/thys/Lifting_the_Exponent/ROOT @@ -0,0 +1,9 @@ +chapter AFP + +session Lifting_the_Exponent (AFP) = "HOL-Number_Theory" + + options [timeout=300] + theories + LTE + document_files + "root.tex" + "root.bib" diff --git a/thys/Lifting_the_Exponent/document/root.bib b/thys/Lifting_the_Exponent/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Lifting_the_Exponent/document/root.bib @@ -0,0 +1,6 @@ +@online{lte, + author = {Hossein Parvardi}, + title = {{Lifting The Exponent Lemma (LTE)}}, + url = {https://s3.amazonaws.com/aops-cdn.artofproblemsolving.com/resources/articles/lifting-the-exponent.pdf}, + year = {2011} +} diff --git a/thys/Lifting_the_Exponent/document/root.tex b/thys/Lifting_the_Exponent/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Lifting_the_Exponent/document/root.tex @@ -0,0 +1,65 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Lifting the Exponent} +\author{Jakub Kądziołka} +\maketitle + +\begin{abstract} + We formalize the \emph{Lifting the Exponent Lemma}, which shows how to find the largest + power of $p$ dividing $a^n \pm b^n$, for a prime $p$ and positive integers $a$ and $b$. + The proof follows~\cite{lte}. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{plainurl} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,603 +1,604 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations BTree Banach_Steinhaus Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties CSP_RefTK DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DOM_Components DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpreter_Optimizations Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaGeoCoq Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knuth_Bendix_Order Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option +Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_arithmetic_LLL_and_HNF_algorithms Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regression_Test_Selection Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Shadow_DOM Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL