Diffusion afp-devel 3261ff4818d4

merge from afp-2019
3261ff4818d4
Actions

Tags

None

Subscribers

None

Description

merge from afp-2019

Details

Provenance

Authored on

Parents

rAFP03e102ee12be: new entry Linear_Inequalities
rAFPec3ff55171a9: tuned

Branches

Unknown

Tags

Unknown

Event Timeline

Merged Changes

ec3ff55171a9 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
967caff984be a few corollaries
Author
traytel
Browse Repository
No Builds
No Audits
023d4c3c8ef8 typo
Author
Christian Sternagel
Browse Repository
No Builds
No Audits
1099e41870d8 even more appropriate fact name
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d91cf5dccf6a merged
Author
traytel
Browse Repository
No Builds
No Audits
76da667dfde4 tuned definition of value as suggested by an ITP reviewer
Author
traytel
Browse Repository
No Builds
No Audits
1c7ecec6a187 simplified proof
Author
nipkow
Browse Repository
No Builds
No Audits
c293c479d6b6 repaired proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a9d827f1c5b1 moved some theorems into HOL main corpus
Author
florian.haftmann
Browse Repository
No Builds
No Audits
65974f61a998 official fact collection sign_simps
Author
florian.haftmann
Browse Repository
No Builds
No Audits
415b7b57be74 dropped unused session references
Author
florian.haftmann
Browse Repository
No Builds
No Audits
0546343b94d3 clear separation of types for bits (False / True) and Z2 (0 / 1)
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ee7d766eb01a dropped weaker legacy alias;
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f6b91be1ab2d dropped former legacy input abbreviations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cf0914a2304e fix for previous commit
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
6197fe173c6f refactoring
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
ad3aff5eb868 minor adjustments to automata library
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
60862c9ef07b refactored degeneralization
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
dc3e35215567 updated basic theories
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
22263520f4c8 updated with guillemot syntax
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e6d3d109c89a updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
a5f6453144c6 fixed latex errors using babel
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fb851cb1ca27 replaced ceiling brackets by guillemots
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
79d06abed2e0 consistency is provable
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
5c9417f37470 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
a8e34b81e70f tuned timeout;
Author
makarius
Browse Repository
No Builds
No Audits
7149dd204040 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
87cfcf4d1dec update cartouches
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
ca143f3dbb79 LambdaAuth: remove lemmas moved to distribution
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
cd86f83a05bb merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
72f2f7d150d6 re-instate devel changeset 6edffc003761
Author
kleing
Browse Repository
No Builds
No Audits
753dc504efaf reset version to devel after release fork
Author
kleing
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (543)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

templates/

Groebner_Macaulay

Binomial_Int.thy

Cone_Decomposition.thy

Degree_Bound_Utils.thy

Degree_Section.thy

Dube_Prelims.thy

Groebner_Macaulay.thy

Groebner_Macaulay_Examples.thy

Hilbert_Function.thy

Monomial_Module.thy

IMP2_Binary_Heap

IMP2_Binary_Heap.thy

Linear_Inequalities

Basis_Extension.thy

Convex_Hull.thy

Decomposition_Theorem.thy

Farkas_Lemma.thy

Farkas_Minkowsky_Weyl.thy

Fundamental_Theorem_Linear_Inequalities.thy

Integer_Hull.thy

Integral_Bounded_Vectors.thy

Missing_Matrix.thy

Missing_VS_Connect.thy

Mixed_Integer_Solutions.thy

Normal_Vector.thy

Sum_Vec_Set.thy

Nullstellensatz

Algebraically_Closed_Fields.thy

Lex_Order_PP.thy

Nullstellensatz.thy

Nullstellensatz_Field.thy

Univariate_PM.thy

Abortable_Linearizable_Modules.html

Abs_Int_ITP2012.html

Abstract-Hoare-Logics.html

Abstract-Rewriting.html

Abstract_Completeness.html

Abstract_Soundness.html

Affine_Arithmetic.html

Aggregation_Algebras.html

Akra_Bazzi.html

Algebraic_Numbers.html

Algebraic_VCs.html

Allen_Calculus.html

Amortized_Complexity.html

Applicative_Lifting.html

Architectural_Design_Patterns.html

ArrowImpossibilityGS.html

Auto2_Imperative_HOL.html

AutoFocus-Stream.html

Automatic_Refinement.html

AxiomaticCategoryTheory.html

BNF_Operations.html

Bell_Numbers_Spivey.html

Berlekamp_Zassenhaus.html

Bertrands_Postulate.html

BinarySearchTree.html

Binding_Syntax_Theory.html

Binomial-Heaps.html

Binomial-Queues.html

Boolean_Expression_Checkers.html

Bounded_Deducibility_Security.html

Buchi_Complementation.html

Budan_Fourier.html

Buffons_Needle.html

BytecodeLogicJmlTypes.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

CISC-Kernel.html

Call_Arity.html

Card_Equiv_Relations.html

Card_Multisets.html

Card_Number_Partitions.html

Card_Partitions.html

Case_Labeling.html

Catalan_Numbers.html

Cayley_Hamilton.html

Certification_Monads.html

Chord_Segments.html

ClockSynchInst.html

Coinductive.html

Coinductive_Languages.html

Collections.html

Comparison_Sort_Lower_Bound.html

Compiling-Exceptions-Correctly.html

Completeness.html

ComponentDependencies.html

ConcurrentGC.html

ConcurrentIMP.html

Concurrent_Ref_Alg.html

Concurrent_Revisions.html

Consensus_Refined.html

Constructive_Cryptography.html

Constructor_Funs.html

Containers.html

Count_Complex_Roots.html

CryptoBasedCompositionalProperties.html

DFS_Framework.html

DPT-SAT-Solver.html

DataRefinementIBP.html

Datatype_Order_Generator.html

Decl_Sem_Fun_PL.html

Decreasing-Diagrams-II.html

Decreasing-Diagrams.html

Deep_Learning.html

Density_Compiler.html

Dependent_SIFUM_Refinement.html

Dependent_SIFUM_Type_Systems.html

Depth-First-Search.html

Derangements.html

Descartes_Sign_Rule.html

Dict_Construction.html

Differential_Dynamic_Logic.html

Dijkstra_Shortest_Path.html

Diophantine_Eqns_Lin_Hom.html

Dirichlet_L.html

Dirichlet_Series.html

DiscretePricing.html

Discrete_Summation.html

DynamicArchitectures.html

Dynamic_Tables.html

E_Transcendental.html

Echelon_Form.html

EdmondsKarp_Maxflow.html

Efficient-Mergesort.html

Elliptic_Curves_Group_Law.html

Encodability_Process_Calculi.html

Epistemic_Logic.html

Ergodic_Theory.html

Error_Function.html

Euler_MacLaurin.html

Euler_Partition.html

FOL-Fitting.html

FOL_Harrison.html

Factored_Transition_System_Bounding.html

Falling_Factorial_Sum.html

FeatherweightJava.html

Featherweight_OCL.html

FileRefinement.html

Finger-Trees.html

Finite_Automata_HF.html

First_Order_Terms.html

First_Welfare_Theorem.html

Fishburn_Impossibility.html

Fisher_Yates.html

Flow_Networks.html

Floyd_Warshall.html

Flyspeck-Tame.html

FocusStreamsCaseStudies.html

Formal_SSA.html

Formula_Derivatives.html

Free-Boolean-Algebra.html

Free-Groups.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Functional_Ordered_Resolution_Prover.html

GPU_Kernel_PL.html

Game_Based_Crypto.html

Gauss-Jordan-Elim-Fun.html

Gauss_Jordan.html

General-Triangle.html

Generic_Deriving.html

GewirthPGCProof.html

Girth_Chromatic.html

GraphMarkingIBP.html

Graph_Saturation.html

Graph_Theory.html

Groebner_Bases.html

Groebner_Macaulay.html

Gromov_Hyperbolicity.html

Group-Ring-Module.html

HOLCF-Prelude.html

HRB-Slicing.html

HereditarilyFinite.html

Hidden_Markov_Models.html

Higher_Order_Terms.html

Hoare_Time.html

HotelKeyCards.html

Hybrid_Multi_Lane_Spatial_Logic.html

IEEE_Floating_Point.html

IMP2_Binary_Heap.html

IP_Addresses.html

Imperative_Insertion_Sort.html

Impossible_Geometry.html

Incompleteness.html

Incredible_Proof_Machine.html

Inductive_Confidentiality.html

InfPathElimination.html

InformationFlowSlicing.html

InformationFlowSlicing_Inter.html

Integration.html

Iptables_Semantics.html

Irrationality_J_Hancl.html

Isabelle_Meta_Model.html

JinjaThreads.html

JiveDataStoreModel.html

Jordan_Hoelder.html

Jordan_Normal_Form.html

KAT_and_DRA.html

Key_Agreement_Strong_Adversaries.html

Kleene_Algebra.html

Knot_Theory.html

Knuth_Morris_Pratt.html

Koenigsberg_Friendship.html

Kuratowski_Closure_Complement.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LTL_Master_Theorem.html

LTL_to_DRA.html

LTL_to_GBA.html

Lam-ml-Normalization.html

LambdaAuth.html

Lambda_Free_EPO.html

Lambda_Free_KBOs.html

Lambda_Free_RPOs.html

Landau_Symbols.html

Latin_Square.html

LatticeProperties.html

Launchbury.html

Lazy-Lists-II.html

Lifting_Definition_Option.html

LightweightJava.html

LinearQuantifierElim.html

Linear_Inequalities.html

Linear_Recurrences.html

Liouville_Numbers.html

List-Index.html

List-Infinite.html

List_Interleaving.html

List_Inversions.html

List_Update.html

LocalLexing.html

Localization_Ring.html

Locally-Nameless-Sigma.html

Lowe_Ontological_Argument.html

Lower_Semicontinuous.html

MFMC_Countable.html

MSO_Regex_Equivalence.html

Markov_Models.html

Mason_Stothers.html

Matrix_Tensor.html

Max-Card-Matching.html

Median_Of_Medians_Selection.html

Minimal_SSA.html

Minkowskis_Theorem.html

Minsky_Machines.html

Modal_Logics_for_NTS.html

Modular_Assembly_Kit_Security.html

Monad_Memo_DP.html

Monad_Normalisation.html

MonoBoolTranAlgebra.html

MonoidalCategory.html

Monomorphic_Monad.html

MuchAdoAboutTwo.html

Multi_Party_Computation.html

Multirelations.html

Myhill-Nerode.html

Name_Carrying_Type_Inference.html

Nat-Interval-Logic.html

Native_Word.html

Nested_Multisets_Ordinals.html

Network_Security_Policy_Verification.html

Neumann_Morgenstern_Utility.html

No_FTL_observers.html

Noninterference_CSP.html

Noninterference_Concurrent_Composition.html

Noninterference_Generic_Unwinding.html

Noninterference_Inductive_Unwinding.html

Noninterference_Ipurge_Unwinding.html

Noninterference_Sequential_Composition.html

NormByEval.html

Nullstellensatz.html

Open_Induction.html

Optimal_BST.html

Orbit_Stabiliser.html

Order_Lattice_Props.html

Ordered_Resolution_Prover.html

Ordinals_and_Cardinals.html

Ordinary_Differential_Equations.html

POPLmark-deBruijn.html

PSemigroupsConvolution.html

Pairing_Heap.html

Paraconsistency.html

Parity_Game.html

Partial_Function_MR.html

Partial_Order_Reduction.html

Password_Authentication_Protocol.html

Perfect-Number-Thm.html

Perron_Frobenius.html

Pi_Calculus.html

Pi_Transcendental.html

Planarity_Certificates.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Pop_Refinement.html

Posix-Lexing.html

Possibilistic_Noninterference.html

Pratt_Certificate.html

Presburger-Automata.html

Prime_Distribution_Elementary.html

Prime_Harmonic_Series.html

Prime_Number_Theorem.html

Priority_Queue_Braun.html

Probabilistic_Noninterference.html

Probabilistic_Prime_Tests.html

Probabilistic_System_Zoo.html

Probabilistic_Timed_Automata.html

Probabilistic_While.html

Program-Conflict-Analysis.html

Projective_Geometry.html

Proof_Strategy_Language.html

Propositional_Proof_Systems.html

Prpu_Maxflow.html

PseudoHoops.html

Psi_Calculi.html

Ptolemys_Theorem.html

QR_Decomposition.html

Quaternions.html

Quick_Sort_Cost.html

RIPEMD-160-SPARK.html

Ramsey-Infinite.html

Random_BSTs.html

Random_Graph_Subgraph_Threshold.html

Randomised_BSTs.html

Randomised_Social_Choice.html

Rank_Nullity_Theorem.html

Recursion-Theory-I.html

Refine_Imperative_HOL.html

Refine_Monadic.html

RefinementReactive.html

Regex_Equivalence.html

Regular-Sets.html

Regular_Algebras.html

Relation_Algebra.html

Rep_Fin_Groups.html

Residuated_Lattices.html

Resolution_FOL.html

Rewriting_Z.html

Ribbon_Proofs.html

Robbins-Conjecture.html

Root_Balanced_Tree.html

Roy_Floyd_Warshall.html

SATSolverVerification.html

SDS_Impossibility.html

SIFUM_Type_Systems.html

Secondary_Sylow.html

Security_Protocol_Refinement.html

Selection_Heap_Sort.html

SenSocialChoice.html

Separation_Algebra.html

Separation_Logic_Imperative_HOL.html

SequentInvertibility.html

Shivers-CFA.html

ShortestPath.html

Signature_Groebner.html

Simple_Firewall.html

Smooth_Manifolds.html

Sort_Encodings.html

Source_Coding_Theorem.html

Special_Function_Bounds.html

Splay_Tree.html

Sqrt_Babylonian.html

Stable_Matching.html

Statecharts.html

Stern_Brocot.html

Stewart_Apollonius.html

Stirling_Formula.html

Stochastic_Matrices.html

Stone_Algebras.html

Stone_Kleene_Relation_Algebras.html

Stone_Relation_Algebras.html

Store_Buffer_Reduction.html

Stream-Fusion.html

Stream_Fusion_Code.html

Strong_Security.html

Sturm_Sequences.html

Sturm_Tarski.html

Stuttering_Equivalence.html

Subresultants.html

SumSquares.html

Surprise_Paradox.html

Symmetric_Polynomials.html

Tail_Recursive_Functions.html

Tarskis_Geometry.html

Taylor_Models.html

Timed_Automata.html

TortoiseHare.html

Transcendence_Series_Hancl_Rucki.html

Transformer_Semantics.html

Transition_Systems_and_Automata.html

Transitive-Closure-II.html

Transitive-Closure.html

Tree-Automata.html

Tree_Decomposition.html

Twelvefold_Way.html

Types_Tableaus_and_Goedels_God.html

UPF_Firewall.html

Universal_Turing_Machine.html

UpDown_Scheme.html

VectorSpace.html

Verified-Prover.html

VerifyThis2018.html

Vickrey_Clarke_Groves.html

VolpanoSmith.html

WHATandWHERE_Security.html

WebAssembly.html

Weight_Balanced_Trees.html

Well_Quasi_Orders.html

Winding_Number_Eval.html

WorkerWrapper.html

Zeta_Function.html

statistics.html

rAFP3261ff4818d4

metadata/metadata

metadata/release-dates

metadata/releases

metadata/templates/using.tpl

thys/Groebner_Macaulay/Binomial_Int.thy

thys/Groebner_Macaulay/Cone_Decomposition.thy

thys/Groebner_Macaulay/Degree_Bound_Utils.thy

thys/Groebner_Macaulay/Degree_Section.thy

thys/Groebner_Macaulay/Dube_Bound.thy

thys/Groebner_Macaulay/Dube_Prelims.thy

thys/Groebner_Macaulay/Groebner_Macaulay.thy

thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy

thys/Groebner_Macaulay/Hilbert_Function.thy

thys/Groebner_Macaulay/Monomial_Module.thy

thys/Groebner_Macaulay/Poly_Fun.thy

thys/Groebner_Macaulay/ROOT

thys/Groebner_Macaulay/document/root.bib

thys/Groebner_Macaulay/document/root.tex

thys/IMP2_Binary_Heap/IMP2_Binary_Heap.thy

thys/IMP2_Binary_Heap/ROOT

thys/IMP2_Binary_Heap/document/root.bib

thys/IMP2_Binary_Heap/document/root.tex

thys/Linear_Inequalities/Basis_Extension.thy

thys/Linear_Inequalities/Cone.thy

thys/Linear_Inequalities/Convex_Hull.thy

thys/Linear_Inequalities/Decomposition_Theorem.thy

thys/Linear_Inequalities/Dim_Span.thy

thys/Linear_Inequalities/Farkas_Lemma.thy

thys/Linear_Inequalities/Farkas_Minkowsky_Weyl.thy

thys/Linear_Inequalities/Fundamental_Theorem_Linear_Inequalities.thy

thys/Linear_Inequalities/Integer_Hull.thy

thys/Linear_Inequalities/Integral_Bounded_Vectors.thy

thys/Linear_Inequalities/Missing_Matrix.thy

thys/Linear_Inequalities/Missing_VS_Connect.thy

thys/Linear_Inequalities/Mixed_Integer_Solutions.thy

thys/Linear_Inequalities/Normal_Vector.thy

thys/Linear_Inequalities/ROOT

thys/Linear_Inequalities/Sum_Vec_Set.thy

thys/Linear_Inequalities/document/root.bib

thys/Linear_Inequalities/document/root.tex

thys/Nullstellensatz/Algebraically_Closed_Fields.thy

thys/Nullstellensatz/Lex_Order_PP.thy

thys/Nullstellensatz/Nullstellensatz.thy

thys/Nullstellensatz/Nullstellensatz_Field.thy

thys/Nullstellensatz/ROOT

thys/Nullstellensatz/Univariate_PM.thy

thys/Nullstellensatz/document/root.bib

thys/Nullstellensatz/document/root.tex

thys/ROOTS

web/entries/AODV.html

web/entries/AVL-Trees.html

web/entries/AWN.html

web/entries/Abortable_Linearizable_Modules.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Abstract-Rewriting.html

web/entries/Abstract_Completeness.html

web/entries/Abstract_Soundness.html

web/entries/Affine_Arithmetic.html

web/entries/Aggregation_Algebras.html

web/entries/Akra_Bazzi.html

web/entries/Algebraic_Numbers.html

web/entries/Algebraic_VCs.html

web/entries/Allen_Calculus.html

web/entries/Amortized_Complexity.html

web/entries/AnselmGod.html

web/entries/Applicative_Lifting.html

web/entries/Architectural_Design_Patterns.html

web/entries/ArrowImpossibilityGS.html

web/entries/Auto2_HOL.html

web/entries/Auto2_Imperative_HOL.html

web/entries/AutoFocus-Stream.html

web/entries/Automatic_Refinement.html

web/entries/AxiomaticCategoryTheory.html

web/entries/BDD.html

web/entries/BNF_CC.html

web/entries/BNF_Operations.html

web/entries/Bell_Numbers_Spivey.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Bernoulli.html

web/entries/Bertrands_Postulate.html

web/entries/BinarySearchTree.html

web/entries/Binding_Syntax_Theory.html

web/entries/Binomial-Heaps.html

web/entries/Binomial-Queues.html

web/entries/Bondy.html

web/entries/Boolean_Expression_Checkers.html

web/entries/Bounded_Deducibility_Security.html

web/entries/Buchi_Complementation.html

web/entries/Budan_Fourier.html

web/entries/Buffons_Needle.html

web/entries/Buildings.html

web/entries/BytecodeLogicJmlTypes.html

web/entries/CAVA_Automata.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CCS.html

web/entries/CISC-Kernel.html

web/entries/CRDT.html

web/entries/CYK.html

web/entries/CakeML.html

web/entries/Call_Arity.html

web/entries/Card_Equiv_Relations.html

web/entries/Card_Multisets.html

web/entries/Card_Number_Partitions.html

web/entries/Card_Partitions.html

web/entries/Cartan_FP.html

web/entries/Case_Labeling.html

web/entries/Catalan_Numbers.html

web/entries/Category.html

web/entries/Category2.html

web/entries/Category3.html

web/entries/Cauchy.html

web/entries/Cayley_Hamilton.html

web/entries/Certification_Monads.html

web/entries/Chord_Segments.html

web/entries/Circus.html

web/entries/ClockSynchInst.html

web/entries/CofGroups.html

web/entries/Coinductive.html

web/entries/Coinductive_Languages.html

web/entries/Collections.html

web/entries/Comparison_Sort_Lower_Bound.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Completeness.html

web/entries/Complx.html

web/entries/ComponentDependencies.html

web/entries/ConcurrentGC.html

web/entries/ConcurrentIMP.html

web/entries/Concurrent_Ref_Alg.html

web/entries/Concurrent_Revisions.html

web/entries/Consensus_Refined.html

web/entries/Constructive_Cryptography.html

web/entries/Constructor_Funs.html

web/entries/Containers.html

web/entries/CoreC++.html

web/entries/Core_DOM.html

web/entries/Count_Complex_Roots.html

web/entries/CryptHOL.html

web/entries/CryptoBasedCompositionalProperties.html

web/entries/DFS_Framework.html

web/entries/DPT-SAT-Solver.html

web/entries/DataRefinementIBP.html

web/entries/Datatype_Order_Generator.html

web/entries/Decl_Sem_Fun_PL.html

web/entries/Decreasing-Diagrams-II.html

web/entries/Decreasing-Diagrams.html

web/entries/Deep_Learning.html

web/entries/Density_Compiler.html

web/entries/Dependent_SIFUM_Refinement.html

web/entries/Dependent_SIFUM_Type_Systems.html

web/entries/Depth-First-Search.html

web/entries/Derangements.html

web/entries/Deriving.html

web/entries/Descartes_Sign_Rule.html

web/entries/Dict_Construction.html

web/entries/Differential_Dynamic_Logic.html

web/entries/Dijkstra_Shortest_Path.html

web/entries/Diophantine_Eqns_Lin_Hom.html

web/entries/Dirichlet_L.html

web/entries/Dirichlet_Series.html

web/entries/DiscretePricing.html

web/entries/Discrete_Summation.html

web/entries/DiskPaxos.html

web/entries/DynamicArchitectures.html

web/entries/Dynamic_Tables.html

web/entries/E_Transcendental.html

web/entries/Echelon_Form.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/Efficient-Mergesort.html

web/entries/Elliptic_Curves_Group_Law.html

web/entries/Encodability_Process_Calculi.html

web/entries/Epistemic_Logic.html

web/entries/Ergodic_Theory.html

web/entries/Error_Function.html

web/entries/Euler_MacLaurin.html

web/entries/Euler_Partition.html

web/entries/FFT.html

web/entries/FLP.html

web/entries/FOL-Fitting.html

web/entries/FOL_Harrison.html

web/entries/Factored_Transition_System_Bounding.html

web/entries/Falling_Factorial_Sum.html

web/entries/Farkas.html

web/entries/FeatherweightJava.html

web/entries/Featherweight_OCL.html

web/entries/Fermat3_4.html

web/entries/FileRefinement.html

web/entries/FinFun.html

web/entries/Finger-Trees.html

web/entries/Finite_Automata_HF.html

web/entries/First_Order_Terms.html

web/entries/First_Welfare_Theorem.html

web/entries/Fishburn_Impossibility.html

web/entries/Fisher_Yates.html

web/entries/Flow_Networks.html

web/entries/Floyd_Warshall.html

web/entries/Flyspeck-Tame.html

web/entries/FocusStreamsCaseStudies.html

web/entries/Formal_SSA.html

web/entries/Formula_Derivatives.html

web/entries/Free-Boolean-Algebra.html

web/entries/Free-Groups.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Functional_Ordered_Resolution_Prover.html

web/entries/GPU_Kernel_PL.html

web/entries/Gabow_SCC.html

web/entries/Game_Based_Crypto.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Gauss_Jordan.html

web/entries/GenClock.html

web/entries/General-Triangle.html

web/entries/Generic_Deriving.html

web/entries/GewirthPGCProof.html

web/entries/Girth_Chromatic.html

web/entries/GoedelGod.html

web/entries/GraphMarkingIBP.html

web/entries/Graph_Saturation.html

web/entries/Graph_Theory.html

web/entries/Green.html

web/entries/Groebner_Bases.html

web/entries/Groebner_Macaulay.html

web/entries/Gromov_Hyperbolicity.html

web/entries/Group-Ring-Module.html

web/entries/HOL-CSP.html

web/entries/HOLCF-Prelude.html

web/entries/HRB-Slicing.html

web/entries/Heard_Of.html

web/entries/HereditarilyFinite.html

web/entries/Hermite.html

web/entries/Hidden_Markov_Models.html

web/entries/Higher_Order_Terms.html

web/entries/Hoare_Time.html

web/entries/HotelKeyCards.html

web/entries/Huffman.html

web/entries/Hybrid_Multi_Lane_Spatial_Logic.html

web/entries/HyperCTL.html

web/entries/IEEE_Floating_Point.html

web/entries/IMAP-CRDT.html

web/entries/IMP2.html

web/entries/IMP2_Binary_Heap.html

web/entries/IP_Addresses.html

web/entries/Imperative_Insertion_Sort.html

web/entries/Impossible_Geometry.html

web/entries/Incompleteness.html

web/entries/Incredible_Proof_Machine.html

web/entries/Inductive_Confidentiality.html

web/entries/InfPathElimination.html

web/entries/InformationFlowSlicing.html

web/entries/InformationFlowSlicing_Inter.html

web/entries/Integration.html

web/entries/Iptables_Semantics.html

web/entries/Irrationality_J_Hancl.html

web/entries/Isabelle_Meta_Model.html

web/entries/Jinja.html

web/entries/JinjaThreads.html

web/entries/JiveDataStoreModel.html

web/entries/Jordan_Hoelder.html

web/entries/Jordan_Normal_Form.html

web/entries/KAD.html

web/entries/KAT_and_DRA.html

web/entries/KBPs.html

web/entries/KD_Tree.html

web/entries/Key_Agreement_Strong_Adversaries.html

web/entries/Kleene_Algebra.html

web/entries/Knot_Theory.html

web/entries/Knuth_Morris_Pratt.html

web/entries/Koenigsberg_Friendship.html

web/entries/Kruskal.html

web/entries/Kuratowski_Closure_Complement.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LOFT.html

web/entries/LTL.html

web/entries/LTL_Master_Theorem.html

web/entries/LTL_to_DRA.html

web/entries/LTL_to_GBA.html

web/entries/Lam-ml-Normalization.html

web/entries/LambdaAuth.html

web/entries/LambdaMu.html

web/entries/Lambda_Free_EPO.html

web/entries/Lambda_Free_KBOs.html

web/entries/Lambda_Free_RPOs.html

web/entries/Landau_Symbols.html

web/entries/Latin_Square.html

web/entries/LatticeProperties.html

web/entries/Launchbury.html

web/entries/Lazy-Lists-II.html

web/entries/Lazy_Case.html

web/entries/Lehmer.html

web/entries/Lifting_Definition_Option.html

web/entries/LightweightJava.html

web/entries/LinearQuantifierElim.html

web/entries/Linear_Inequalities.html

web/entries/Linear_Recurrences.html

web/entries/Liouville_Numbers.html

web/entries/List-Index.html

web/entries/List-Infinite.html

web/entries/List_Interleaving.html

web/entries/List_Inversions.html

web/entries/List_Update.html

web/entries/LocalLexing.html

web/entries/Localization_Ring.html

web/entries/Locally-Nameless-Sigma.html

web/entries/Lowe_Ontological_Argument.html

web/entries/Lower_Semicontinuous.html

web/entries/Lp.html

web/entries/MFMC_Countable.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/Mason_Stothers.html

web/entries/Matrix.html

web/entries/Matrix_Tensor.html

web/entries/Matroids.html

web/entries/Max-Card-Matching.html

web/entries/Median_Of_Medians_Selection.html

web/entries/Menger.html

web/entries/MiniML.html

web/entries/Minimal_SSA.html

web/entries/Minkowskis_Theorem.html

web/entries/Minsky_Machines.html

web/entries/Modal_Logics_for_NTS.html

web/entries/Modular_Assembly_Kit_Security.html

web/entries/Monad_Memo_DP.html

web/entries/Monad_Normalisation.html

web/entries/MonoBoolTranAlgebra.html

web/entries/MonoidalCategory.html

web/entries/Monomorphic_Monad.html

web/entries/MuchAdoAboutTwo.html

web/entries/Multi_Party_Computation.html

web/entries/Multirelations.html

web/entries/Myhill-Nerode.html

web/entries/Name_Carrying_Type_Inference.html

web/entries/Nat-Interval-Logic.html

web/entries/Native_Word.html

web/entries/Nested_Multisets_Ordinals.html

web/entries/Network_Security_Policy_Verification.html

web/entries/Neumann_Morgenstern_Utility.html

web/entries/No_FTL_observers.html

web/entries/Nominal2.html

web/entries/Noninterference_CSP.html

web/entries/Noninterference_Concurrent_Composition.html

web/entries/Noninterference_Generic_Unwinding.html

web/entries/Noninterference_Inductive_Unwinding.html

web/entries/Noninterference_Ipurge_Unwinding.html

web/entries/Noninterference_Sequential_Composition.html

web/entries/NormByEval.html

web/entries/Nullstellensatz.html

web/entries/Octonions.html

web/entries/OpSets.html

web/entries/Open_Induction.html

web/entries/Optics.html

web/entries/Optimal_BST.html

web/entries/Orbit_Stabiliser.html

web/entries/Order_Lattice_Props.html

web/entries/Ordered_Resolution_Prover.html

web/entries/Ordinal.html

web/entries/Ordinals_and_Cardinals.html

web/entries/Ordinary_Differential_Equations.html

web/entries/PCF.html

web/entries/PLM.html

web/entries/POPLmark-deBruijn.html

web/entries/PSemigroupsConvolution.html

web/entries/Pairing_Heap.html

web/entries/Paraconsistency.html

web/entries/Parity_Game.html

web/entries/Partial_Function_MR.html

web/entries/Partial_Order_Reduction.html

web/entries/Password_Authentication_Protocol.html

web/entries/Pell.html

web/entries/Perfect-Number-Thm.html

web/entries/Perron_Frobenius.html

web/entries/Pi_Calculus.html

web/entries/Pi_Transcendental.html

web/entries/Planarity_Certificates.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Pop_Refinement.html

web/entries/Posix-Lexing.html

web/entries/Possibilistic_Noninterference.html

web/entries/Pratt_Certificate.html

web/entries/Presburger-Automata.html

web/entries/Prime_Distribution_Elementary.html

web/entries/Prime_Harmonic_Series.html

web/entries/Prime_Number_Theorem.html

web/entries/Priority_Queue_Braun.html

web/entries/Probabilistic_Noninterference.html

web/entries/Probabilistic_Prime_Tests.html

web/entries/Probabilistic_System_Zoo.html

web/entries/Probabilistic_Timed_Automata.html

web/entries/Probabilistic_While.html

web/entries/Program-Conflict-Analysis.html

web/entries/Projective_Geometry.html

web/entries/Promela.html

web/entries/Proof_Strategy_Language.html

web/entries/PropResPI.html

web/entries/Propositional_Proof_Systems.html

web/entries/Prpu_Maxflow.html

web/entries/PseudoHoops.html

web/entries/Psi_Calculi.html

web/entries/Ptolemys_Theorem.html

web/entries/QHLProver.html

web/entries/QR_Decomposition.html

web/entries/Quantales.html

web/entries/Quaternions.html

web/entries/Quick_Sort_Cost.html

web/entries/RIPEMD-160-SPARK.html

web/entries/ROBDD.html

web/entries/RSAPSS.html

web/entries/Ramsey-Infinite.html

web/entries/Random_BSTs.html

web/entries/Random_Graph_Subgraph_Threshold.html

web/entries/Randomised_BSTs.html

web/entries/Randomised_Social_Choice.html

web/entries/Rank_Nullity_Theorem.html

web/entries/Real_Impl.html

web/entries/Recursion-Theory-I.html

web/entries/Refine_Imperative_HOL.html

web/entries/Refine_Monadic.html

web/entries/RefinementReactive.html

web/entries/Regex_Equivalence.html

web/entries/Regular-Sets.html

web/entries/Regular_Algebras.html

web/entries/Relation_Algebra.html

web/entries/Rep_Fin_Groups.html

web/entries/Residuated_Lattices.html

web/entries/Resolution_FOL.html

web/entries/Rewriting_Z.html

web/entries/Ribbon_Proofs.html

web/entries/Robbins-Conjecture.html

web/entries/Root_Balanced_Tree.html

web/entries/Routing.html

web/entries/Roy_Floyd_Warshall.html

web/entries/SATSolverVerification.html

web/entries/SDS_Impossibility.html

web/entries/SIFPL.html

web/entries/SIFUM_Type_Systems.html

web/entries/SPARCv8.html

web/entries/Safe_OCL.html

web/entries/Secondary_Sylow.html

web/entries/Security_Protocol_Refinement.html

web/entries/Selection_Heap_Sort.html

web/entries/SenSocialChoice.html

web/entries/Separata.html

web/entries/Separation_Algebra.html

web/entries/Separation_Logic_Imperative_HOL.html

web/entries/SequentInvertibility.html

web/entries/Shivers-CFA.html

web/entries/ShortestPath.html

web/entries/Show.html

web/entries/Signature_Groebner.html

web/entries/Simpl.html

web/entries/Simple_Firewall.html

web/entries/Simplex.html

web/entries/Skew_Heap.html

web/entries/Slicing.html

web/entries/Smooth_Manifolds.html

web/entries/Sort_Encodings.html

web/entries/Source_Coding_Theorem.html

web/entries/Special_Function_Bounds.html

web/entries/Splay_Tree.html

web/entries/Sqrt_Babylonian.html

web/entries/Stable_Matching.html

web/entries/Statecharts.html

web/entries/Stern_Brocot.html

web/entries/Stewart_Apollonius.html

web/entries/Stirling_Formula.html

web/entries/Stochastic_Matrices.html

web/entries/Stone_Algebras.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Stone_Relation_Algebras.html

web/entries/Store_Buffer_Reduction.html

web/entries/Stream-Fusion.html

web/entries/Stream_Fusion_Code.html

web/entries/Strong_Security.html

web/entries/Sturm_Sequences.html

web/entries/Sturm_Tarski.html

web/entries/Stuttering_Equivalence.html

web/entries/Subresultants.html

web/entries/SumSquares.html

web/entries/SuperCalc.html

web/entries/Surprise_Paradox.html

web/entries/Symmetric_Polynomials.html

web/entries/TLA.html

web/entries/Tail_Recursive_Functions.html

web/entries/Tarskis_Geometry.html

web/entries/Taylor_Models.html

web/entries/Timed_Automata.html

web/entries/Topology.html

web/entries/TortoiseHare.html

web/entries/Transcendence_Series_Hancl_Rucki.html

web/entries/Transformer_Semantics.html

web/entries/Transition_Systems_and_Automata.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/Treaps.html

web/entries/Tree-Automata.html

web/entries/Tree_Decomposition.html

web/entries/Triangle.html

web/entries/Trie.html

web/entries/Twelvefold_Way.html

web/entries/Tycon.html

web/entries/Types_Tableaus_and_Goedels_God.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/entries/UTP.html

web/entries/Universal_Turing_Machine.html

web/entries/UpDown_Scheme.html

web/entries/Valuation.html

web/entries/VectorSpace.html

web/entries/Verified-Prover.html

web/entries/VerifyThis2018.html

web/entries/Vickrey_Clarke_Groves.html

web/entries/VolpanoSmith.html

web/entries/WHATandWHERE_Security.html

web/entries/WebAssembly.html

web/entries/Weight_Balanced_Trees.html

web/entries/Well_Quasi_Orders.html

web/entries/Winding_Number_Eval.html

web/entries/Word_Lib.html

web/entries/WorkerWrapper.html

web/entries/XML.html

web/entries/Zeta_Function.html

web/entries/pGCL.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html

web/using.html