diff --git a/metadata/authors.toml b/metadata/authors.toml
--- a/metadata/authors.toml
+++ b/metadata/authors.toml
@@ -1,6951 +1,6968 @@
 
 [abdulaziz]
 name = "Mohammad Abdulaziz"
 
 [abdulaziz.emails]
 
 [abdulaziz.emails.abdulaziz_email]
 user = [
   "mohammad",
   "abdulaziz",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [abdulaziz.emails.abdulaziz_email1]
 user = [
   "mohammad",
   "abdulaziz8",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [abdulaziz.homepages]
 abdulaziz_homepage = "http://home.in.tum.de/~mansour/"
 
 [adelsberger]
 name = "Stephan Adelsberger"
 
 [adelsberger.emails]
 
 [adelsberger.emails.adelsberger_email]
 user = [
   "stvienna",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [adelsberger.homepages]
 adelsberger_homepage = "http://nm.wu.ac.at/nm/sadelsbe"
 
 [aehlig]
 name = "Klaus Aehlig"
 
 [aehlig.emails]
 
 [aehlig.homepages]
 aehlig_homepage = "http://www.linta.de/~aehlig/"
 
 [aissat]
 name = "Romain Aissat"
 
 [aissat.emails]
 
 [aissat.homepages]
 
 [amani]
 name = "Sidney Amani"
 
 [amani.emails]
 
 [amani.emails.amani_email]
 user = [
   "sidney",
   "amani",
 ]
 host = [
   "data61",
   "csiro",
   "au",
 ]
 
 [amani.homepages]
 
 [ammer]
 name = "Thomas Ammer"
 
 [ammer.emails]
 
 [ammer.emails.ammer_email]
 user = [
   "thomas",
   "ammer",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [ammer.homepages]
 
 [andronick]
 name = "June Andronick"
 
 [andronick.emails]
 
 [andronick.homepages]
 
 [aransay]
 name = "Jesús Aransay"
 
 [aransay.emails]
 
 [aransay.emails.aransay_email]
 user = [
   "jesus-maria",
   "aransay",
 ]
 host = [
   "unirioja",
   "es",
 ]
 
 [aransay.homepages]
 aransay_homepage = "https://www.unirioja.es/cu/jearansa"
 
 [argyraki]
 name = "Angeliki Koutsoukou-Argyraki"
 
 [argyraki.emails]
 
 [argyraki.emails.argyraki_email]
 user = [
   "ak2110",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [argyraki.homepages]
 argyraki_homepage = "https://www.cl.cam.ac.uk/~ak2110/"
 argyraki_homepage2 = "https://www.cst.cam.ac.uk/people/ak2110"
 
 [armstrong]
 name = "Alasdair Armstrong"
 
 [armstrong.emails]
 
 [armstrong.homepages]
 
 [aspinall]
 name = "David Aspinall"
 
 [aspinall.emails]
 
 [aspinall.homepages]
 aspinall_homepage = "http://homepages.inf.ed.ac.uk/da/"
 
 [ausaf]
 name = "Fahad Ausaf"
 
 [ausaf.emails]
 
 [ausaf.homepages]
 ausaf_homepage = "http://kcl.academia.edu/FahadAusaf"
 
 [avigad]
 name = "Jeremy Avigad"
 
 [avigad.emails]
 
 [avigad.emails.avigad_email]
 user = [
   "avigad",
 ]
 host = [
   "cmu",
   "edu",
 ]
 
 [avigad.homepages]
 avigad_homepage = "http://www.andrew.cmu.edu/user/avigad/"
 
 [back]
 name = "Ralph-Johan Back"
 
 [back.emails]
 
 [back.homepages]
 back_homepage = "http://users.abo.fi/Ralph-Johan.Back/"
 
 [balbach]
 name = "Frank J. Balbach"
 
 [balbach.emails]
 
 [balbach.emails.balbach_email]
 user = [
   "frank-balbach",
 ]
 host = [
   "gmx",
   "de",
 ]
 
 [balbach.homepages]
 
 [ballarin]
 name = "Clemens Ballarin"
 
 [ballarin.emails]
 
 [ballarin.emails.ballarin_email]
 user = [
   "ballarin",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [ballarin.homepages]
 ballarin_homepage = "http://www21.in.tum.de/~ballarin/"
 
 [barsotti]
 name = "Damián Barsotti"
 
 [barsotti.emails]
 
 [barsotti.homepages]
 barsotti_homepage = "http://www.cs.famaf.unc.edu.ar/~damian/"
 
 [bauer]
 name = "Gertrud Bauer"
 
 [bauer.emails]
 
 [bauer.homepages]
 
 [bauereiss]
 name = "Thomas Bauereiss"
 
 [bauereiss.emails]
 
 [bauereiss.emails.bauereiss_email]
 user = [
   "thomas",
 ]
 host = [
   "bauereiss",
   "name",
 ]
 
 [bauereiss.homepages]
 
 [bayer]
 name = "Jonas Bayer"
 
 [bayer.emails]
 
 [bayer.emails.bayer_email]
 user = [
   "jonas",
   "bayer999",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bayer.homepages]
 
 [becker]
 name = "Heiko Becker"
 
 [becker.emails]
 
 [becker.emails.becker_email]
 user = [
   "hbecker",
 ]
 host = [
   "mpi-sws",
   "org",
 ]
 
 [becker.homepages]
 
 [beeren]
 name = "Joel Beeren"
 
 [beeren.emails]
 
 [beeren.homepages]
 
 [bella]
 name = "Giampaolo Bella"
 
 [bella.emails]
 
 [bella.emails.bella_email]
 user = [
   "giamp",
 ]
 host = [
   "dmi",
   "unict",
   "it",
 ]
 
 [bella.homepages]
 bella_homepage = "http://www.dmi.unict.it/~giamp/"
 
 [bengtson]
 name = "Jesper Bengtson"
 
 [bengtson.emails]
 
 [bengtson.homepages]
 bengtson_homepage = "http://www.itu.dk/people/jebe"
 
 [bentkamp]
 name = "Alexander Bentkamp"
 
 [bentkamp.emails]
 
 [bentkamp.emails.bentkamp_email]
 user = [
   "bentkamp",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bentkamp.emails.bentkamp_email1]
 user = [
   "a",
   "bentkamp",
 ]
 host = [
   "vu",
   "nl",
 ]
 
 [bentkamp.homepages]
 bentkamp_homepage = "https://www.cs.vu.nl/~abp290/"
 
 [benzmueller]
 name = "Christoph Benzmüller"
 
 [benzmueller.emails]
 
 [benzmueller.emails.benzmueller_email]
 user = [
   "c",
   "benzmueller",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [benzmueller.emails.benzmueller_email1]
 user = [
   "c",
   "benzmueller",
 ]
 host = [
   "fu-berlin",
   "de",
 ]
 
 [benzmueller.homepages]
 benzmueller_homepage = "http://christoph-benzmueller.de"
 benzmueller_homepage1 = "http://page.mi.fu-berlin.de/cbenzmueller/"
 
 [beresford]
 name = "Alastair R. Beresford"
 
 [beresford.emails]
 
 [beresford.emails.beresford_email]
 user = [
   "arb33",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [beresford.homepages]
 
 [berghofer]
 name = "Stefan Berghofer"
 
 [berghofer.emails]
 
 [berghofer.emails.berghofer_email]
 user = [
   "berghofe",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [berghofer.homepages]
 berghofer_homepage = "http://www.in.tum.de/~berghofe"
 
 [beringer]
 name = "Lennart Beringer"
 
 [beringer.emails]
 
 [beringer.emails.beringer_email]
 user = [
   "lennart",
   "beringer",
 ]
 host = [
   "ifi",
   "lmu",
   "de",
 ]
 
 [beringer.homepages]
 
 [bharadwaj]
 name = "Abhijith Bharadwaj"
 
 [bharadwaj.emails]
 
 [bharadwaj.homepages]
 
 [bhatt]
 name = "Bhargav Bhatt"
 
 [bhatt.emails]
 
 [bhatt.emails.bhatt_email]
 user = [
   "bhargav",
   "bhatt",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [bhatt.homepages]
 
 [biendarra]
 name = "Julian Biendarra"
 
 [biendarra.emails]
 
 [biendarra.homepages]
 
 [bisping]
 name = "Benjamin Bisping"
 
 [bisping.emails]
 
 [bisping.emails.bisping_email]
 user = [
   "benjamin",
   "bisping",
 ]
 host = [
   "campus",
   "tu-berlin",
   "de",
 ]
 
 [bisping.homepages]
 
 [blanchette]
 name = "Jasmin Christian Blanchette"
 
 [blanchette.emails]
 
 [blanchette.emails.blanchette_email]
 user = [
   "jasmin",
   "blanchette",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [blanchette.emails.blanchette_email1]
 user = [
   "j",
   "c",
   "blanchette",
 ]
 host = [
   "vu",
   "nl",
 ]
 
 [blanchette.homepages]
 blanchette_homepage = "http://www21.in.tum.de/~blanchet"
 blanchette_homepage1 = "https://www.cs.vu.nl/~jbe248/"
 
 [blasum]
 name = "Holger Blasum"
 
 [blasum.emails]
 
 [blasum.emails.blasum_email]
 user = [
   "holger",
   "blasum",
 ]
 host = [
   "sysgo",
   "com",
 ]
 
 [blasum.homepages]
 
 [blumson]
 name = "Ben Blumson"
 
 [blumson.emails]
 
 [blumson.emails.blumson_email]
 user = [
   "benblumson",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [blumson.homepages]
 blumson_homepage = "https://philpeople.org/profiles/ben-blumson"
 
 [bockenek]
 name = "Joshua Bockenek"
 
 [bockenek.emails]
 
 [bockenek.homepages]
 
 [boehme]
 name = "Sascha Böhme"
 
 [boehme.emails]
 
 [boehme.emails.boehme_email]
 user = [
   "boehmes",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [boehme.homepages]
 boehme_homepage = "http://www21.in.tum.de/~boehmes/"
 
 [bohrer]
 name = "Rose Bohrer"
 
 [bohrer.emails]
 
 [bohrer.emails.bohrer_email]
 user = [
   "rose",
   "bohrer",
   "cs",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bohrer.homepages]
 
 [bordg]
 name = "Anthony Bordg"
 
 [bordg.emails]
 
 [bordg.emails.bordg_email]
 user = [
   "apdb3",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [bordg.homepages]
 bordg_homepage = "https://sites.google.com/site/anthonybordg/"
 
 [borgstroem]
 name = "Johannes Borgström"
 
 [borgstroem.emails]
 
 [borgstroem.emails.borgstroem_email]
 user = [
   "johannes",
   "borgstrom",
 ]
 host = [
   "it",
   "uu",
   "se",
 ]
 
 [borgstroem.homepages]
 
 [bortin]
 name = "Maksym Bortin"
 
 [bortin.emails]
 
 [bortin.emails.bortin_email]
 user = [
   "maksym",
   "bortin",
 ]
 host = [
   "nicta",
   "com",
   "au",
 ]
 
 [bortin.emails.bortin_email1]
 user = [
   "mbortin",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bortin.homepages]
 
 [bottesch]
 name = "Ralph Bottesch"
 
 [bottesch.emails]
 
 [bottesch.emails.bottesch_email]
 user = [
   "ralph",
   "bottesch",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [bottesch.homepages]
 bottesch_homepage = "http://cl-informatik.uibk.ac.at/users/bottesch/"
 
 [boulanger]
 name = "Frédéric Boulanger"
 
 [boulanger.emails]
 
 [boulanger.emails.boulanger_email]
 user = [
   "frederic",
   "boulanger",
 ]
 host = [
   "centralesupelec",
   "fr",
 ]
 
 [boulanger.homepages]
 
 [bourke]
 name = "Timothy Bourke"
 
 [bourke.emails]
 
 [bourke.emails.bourke_email]
 user = [
   "tim",
 ]
 host = [
   "tbrk",
   "org",
 ]
 
 [bourke.homepages]
 bourke_homepage = "http://www.tbrk.org"
 
 [boutry]
 name = "Pierre Boutry"
 
 [boutry.emails]
 
 [boutry.emails.boutry_email]
 user = [
   "boutry",
 ]
 host = [
   "unistra",
   "fr",
 ]
 
 [boutry.homepages]
 
 [boyton]
 name = "Andrew Boyton"
 
 [boyton.emails]
 
 [boyton.emails.boyton_email]
 user = [
   "andrew",
   "boyton",
 ]
 host = [
   "nicta",
   "com",
   "au",
 ]
 
 [boyton.homepages]
 
 [bracevac]
 name = "Oliver Bračevac"
 
 [bracevac.emails]
 
 [bracevac.emails.bracevac_email]
 user = [
   "bracevac",
 ]
 host = [
   "st",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [bracevac.homepages]
 
 [brandt]
 name = "Felix Brandt"
 
 [brandt.emails]
 
 [brandt.homepages]
 brandt_homepage = "http://dss.in.tum.de/staff/brandt.html"
 
 [breitner]
 name = "Joachim Breitner"
 
 [breitner.emails]
 
 [breitner.emails.breitner_email]
 user = [
   "mail",
 ]
 host = [
   "joachim-breitner",
   "de",
 ]
 
 [breitner.emails.breitner_email1]
 user = [
   "joachim",
 ]
 host = [
   "cis",
   "upenn",
   "edu",
 ]
 
 [breitner.homepages]
 breitner_homepage = "http://pp.ipd.kit.edu/~breitner"
 
 [brien]
 name = "Nicolas Robinson-O'Brien"
 
 [brien.emails]
 
 [brien.homepages]
 
 [brinkop]
 name = "Hauke Brinkop"
 
 [brinkop.emails]
 
 [brinkop.emails.brinkop_email]
 user = [
   "hauke",
   "brinkop",
 ]
 host = [
   "googlemail",
   "com",
 ]
 
 [brinkop.homepages]
 
 [brodmann]
 name = "Paul-David Brodmann"
 
 [brodmann.emails]
 
 [brodmann.emails.brodmann_email]
 user = [
   "p",
   "brodmann",
 ]
 host = [
   "tu-berlin",
   "de",
 ]
 
 [brodmann.homepages]
 
 [brucker]
 name = "Achim D. Brucker"
 
 [brucker.emails]
 
 [brucker.emails.brucker_email]
 user = [
   "a",
   "brucker",
 ]
 host = [
   "exeter",
   "ac",
   "uk",
 ]
 
 [brucker.emails.brucker_email1]
 user = [
   "brucker",
 ]
 host = [
   "spamfence",
   "net",
 ]
 
 [brucker.emails.brucker_email2]
 user = [
   "adbrucker",
 ]
 host = [
   "0x5f",
   "org",
 ]
 
 [brucker.homepages]
 brucker_homepage = "https://www.brucker.ch/"
 
 [bruegger]
 name = "Lukas Brügger"
 
 [bruegger.emails]
 
 [bruegger.emails.bruegger_email]
 user = [
   "lukas",
   "a",
   "bruegger",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bruegger.homepages]
 
 [brun]
 name = "Matthias Brun"
 
 [brun.emails]
 
 [brun.emails.brun_email]
 user = [
   "matthias",
   "brun",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [brun.homepages]
 
 [brunner]
 name = "Julian Brunner"
 
 [brunner.emails]
 
 [brunner.emails.brunner_email]
 user = [
   "brunnerj",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [brunner.homepages]
 brunner_homepage = "http://www21.in.tum.de/~brunnerj/"
 
 [bulwahn]
 name = "Lukas Bulwahn"
 
 [bulwahn.emails]
 
 [bulwahn.emails.bulwahn_email]
 user = [
   "lukas",
   "bulwahn",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [bulwahn.homepages]
 
 [butler]
 name = "David Butler"
 
 [butler.emails]
 
 [butler.emails.butler_email]
 user = [
   "dbutler",
 ]
 host = [
   "turing",
   "ac",
   "uk",
 ]
 
 [butler.homepages]
 butler_homepage = "https://www.turing.ac.uk/people/doctoral-students/david-butler"
 
 [buyse]
 name = "Maxime Buyse"
 
 [buyse.emails]
 
 [buyse.emails.buyse_email]
 user = [
   "maxime",
   "buyse",
 ]
 host = [
   "polytechnique",
   "edu",
 ]
 
 [buyse.homepages]
 
 [caballero]
 name = "José Manuel Rodríguez Caballero"
 
 [caballero.emails]
 
 [caballero.emails.caballero_email]
 user = [
   "jose",
   "manuel",
   "rodriguez",
   "caballero",
 ]
 host = [
   "ut",
   "ee",
 ]
 
 [caballero.homepages]
 caballero_homepage = "https://josephcmac.github.io/"
 
 [caminati]
 name = "Marco B. Caminati"
 
 [caminati.emails]
 
 [caminati.homepages]
 
 [campo]
 name = "Alejandro del Campo"
 
 [campo.emails]
 
 [campo.emails.campo_email]
 user = [
   "alejandro",
   "del-campo",
 ]
 host = [
   "alum",
   "unirioja",
   "es",
 ]
 
 [campo.homepages]
 
 [chaieb]
 name = "Amine Chaieb"
 
 [chaieb.emails]
 
 [chaieb.homepages]
 
 [chapman]
 name = "Peter Chapman"
 
 [chapman.emails]
 
 [chapman.emails.chapman_email]
 user = [
   "pc",
 ]
 host = [
   "cs",
   "st-andrews",
   "ac",
   "uk",
 ]
 
 [chapman.homepages]
 
 [chen]
 name = "L. Chen"
 
 [chen.emails]
 
 [chen.homepages]
 
 [clouston]
 name = "Ranald Clouston"
 
 [clouston.emails]
 
 [clouston.emails.clouston_email]
 user = [
   "ranald",
   "clouston",
 ]
 host = [
   "cs",
   "au",
   "dk",
 ]
 
 [clouston.homepages]
 
 [cock]
 name = "David Cock"
 
 [cock.emails]
 
 [cock.emails.cock_email]
 user = [
   "david",
   "cock",
 ]
 host = [
   "nicta",
   "com",
   "au",
 ]
 
 [cock.homepages]
 
 [coghetto]
 name = "Roland Coghetto"
 
 [coghetto.emails]
 
 [coghetto.emails.coghetto_email]
 user = [
   "roland_coghetto",
 ]
 host = [
   "hotmail",
   "com",
 ]
 
 [coghetto.homepages]
 
 [coglio]
 name = "Alessandro Coglio"
 
 [coglio.emails]
 
 [coglio.emails.coglio_email]
 user = [
   "coglio",
 ]
 host = [
   "kestrel",
   "edu",
 ]
 
 [coglio.homepages]
 coglio_homepage = "http://www.kestrel.edu/~coglio"
 
 [cohen]
 name = "Ernie Cohen"
 
 [cohen.emails]
 
 [cohen.emails.cohen_email]
 user = [
   "ecohen",
 ]
 host = [
   "amazon",
   "com",
 ]
 
 [cohen.homepages]
 
 [cordwell]
 name = "Katherine Cordwell"
 
 [cordwell.emails]
 
 [cordwell.emails.cordwell_email]
 user = [
   "kcordwel",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [cordwell.homepages]
 cordwell_homepage = "https://www.cs.cmu.edu/~kcordwel/"
 
 [cousin]
 name = "Marie Cousin"
 
 [cousin.emails]
 
 [cousin.emails.cousin_email]
 user = [
   "marie",
   "cousin",
 ]
 host = [
   "grenoble-inp",
   "org",
 ]
 
 [cousin.homepages]
 
 [cremer]
 name = "Nils Cremer"
 
 [cremer.emails]
 
 [cremer.emails.cremer_email]
 user = [
   "nils",
   "cremer",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [cremer.homepages]
 
 [crighton]
 name = "Aaron Crighton"
 
 [crighton.emails]
 
 [crighton.emails.crighton_email]
 user = [
   "crightoa",
 ]
 host = [
   "mcmaster",
   "ca",
 ]
 
 [crighton.homepages]
 
 [dardinier]
 name = "Thibault Dardinier"
 
 [dardinier.emails]
 
 [dardinier.emails.dardinier_email]
 user = [
   "thibault",
   "dardinier",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [dardinier.homepages]
 dardinier_homepage = "https://dardinier.me/"
 
 [david]
 name = "Marco David"
 
 [david.emails]
 
 [david.emails.david_email]
 user = [
   "marco",
   "david",
 ]
 host = [
   "hotmail",
   "de",
 ]
 
 [david.homepages]
 
 [debrat]
 name = "Henri Debrat"
 
 [debrat.emails]
 
 [debrat.emails.debrat_email]
 user = [
   "henri",
   "debrat",
 ]
 host = [
   "loria",
   "fr",
 ]
 
 [debrat.homepages]
 
 [decova]
 name = "Sára Decova"
 
 [decova.emails]
 
 [decova.homepages]
 
 [derrick]
 name = "John Derrick"
 
 [derrick.emails]
 
 [derrick.emails.derrick_email]
 user = [
   "j",
   "derrick",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [derrick.homepages]
 
 [desharnais]
 name = "Martin Desharnais"
 
 [desharnais.emails]
 
 [desharnais.emails.desharnais_email]
 user = [
   "martin",
   "desharnais",
 ]
 host = [
   "unibw",
   "de",
 ]
 
 [desharnais.homepages]
 desharnais_homepage = "https://martin.desharnais.me"
 
 [diaz]
 name = "Javier Díaz"
 
 [diaz.emails]
 
 [diaz.emails.diaz_email]
 user = [
   "javier",
   "diaz",
   "manzi",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [diaz.homepages]
 
 [diekmann]
 name = "Cornelius Diekmann"
 
 [diekmann.emails]
 
 [diekmann.emails.diekmann_email]
 user = [
   "diekmann",
 ]
 host = [
   "net",
   "in",
   "tum",
   "de",
 ]
 
 [diekmann.homepages]
 diekmann_homepage = "http://net.in.tum.de/~diekmann"
 
 [dirix]
 name = "Stefan Dirix"
 
 [dirix.emails]
 
 [dirix.homepages]
 
 [dittmann]
 name = "Christoph Dittmann"
 
 [dittmann.emails]
 
 [dittmann.emails.dittmann_email]
 user = [
   "isabelle",
 ]
 host = [
   "christoph-d",
   "de",
 ]
 
 [dittmann.homepages]
 dittmann_homepage = "http://logic.las.tu-berlin.de/Members/Dittmann/"
 
 [divason]
 name = "Jose Divasón"
 
 [divason.emails]
 
 [divason.emails.divason_email]
 user = [
   "jose",
   "divason",
 ]
 host = [
   "unirioja",
   "es",
 ]
 
 [divason.homepages]
 divason_homepage = "https://www.unirioja.es/cu/jodivaso/"
 
 [doczkal]
 name = "Christian Doczkal"
 
 [doczkal.emails]
 
 [doczkal.emails.doczkal_email]
 user = [
   "doczkal",
 ]
 host = [
   "ps",
   "uni-saarland",
   "de",
 ]
 
 [doczkal.homepages]
 
 [dongol]
 name = "Brijesh Dongol"
 
 [dongol.emails]
 
 [dongol.emails.dongol_email]
 user = [
   "brijesh",
   "dongol",
 ]
 host = [
   "brunel",
   "ac",
   "uk",
 ]
 
 [dongol.homepages]
 
 [doty]
 name = "Matthew Doty"
 
 [doty.emails]
 
 [doty.emails.doty_email]
 user = [
   "matt",
 ]
 host = [
   "w-d",
   "org",
 ]
 
 [doty.homepages]
 
 [dubut]
 name = "Jérémy Dubut"
 
 [dubut.emails]
 
 [dubut.emails.dubut_email]
 user = [
   "dubut",
 ]
 host = [
   "nii",
   "ac",
   "jp",
 ]
 
 [dubut.homepages]
 dubut_homepage = "http://group-mmm.org/~dubut/"
 
 [dunaev]
 name = "Georgy Dunaev"
 
 [dunaev.emails]
 
 [dunaev.emails.dunaev_email]
 user = [
   "georgedunaev",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [dunaev.homepages]
 
 [dyckhoff]
 name = "Roy Dyckhoff"
 
 [dyckhoff.emails]
 
 [dyckhoff.homepages]
 dyckhoff_homepage = "https://rd.host.cs.st-andrews.ac.uk"
 
 [eberl]
 name = "Manuel Eberl"
 orcid = "0000-0002-4263-6571"
 
 [eberl.emails]
 
 [eberl.emails.eberl_email]
 user = [
   "manuel",
 ]
 host = [
   "pruvisto",
   "org",
 ]
 
 [eberl.emails.eberl_email1]
 user = [
   "manuel",
   "eberl",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [eberl.emails.eberl_email2]
 user = [
   "manuel",
   "eberl",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [eberl.homepages]
 eberl_homepage = "https://pruvisto.org/"
 eberl_homepage2 = "https://www.in.tum.de/~eberlm"
 
 [echenim]
 name = "Mnacho Echenim"
 
 [echenim.emails]
 
 [echenim.emails.echenim_email]
 user = [
   "mnacho",
   "echenim",
 ]
 host = [
   "univ-grenoble-alpes",
   "fr",
 ]
 
 [echenim.homepages]
 echenim_homepage = "https://lig-membres.imag.fr/mechenim/"
 
 [edmonds]
 name = "Chelsea Edmonds"
 
 [edmonds.emails]
 
 [edmonds.emails.edmonds_email]
 user = [
   "cle47",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [edmonds.homepages]
 edmonds_homepage = "https://www.cst.cam.ac.uk/people/cle47"
 
 [engelhardt]
 name = "Kai Engelhardt"
 
 [engelhardt.emails]
 
 [engelhardt.homepages]
 
 [eriksson]
 name = "Lars-Henrik Eriksson"
 
 [eriksson.emails]
 
 [eriksson.emails.eriksson_email]
 user = [
   "lhe",
 ]
 host = [
   "it",
   "uu",
   "se",
 ]
 
 [eriksson.homepages]
 
 [esparza]
 name = "Javier Esparza"
 
 [esparza.emails]
 
 [esparza.homepages]
 esparza_homepage = "https://www7.in.tum.de/~esparza/"
 
 [essmann]
 name = "Robin Eßmann"
 
 [essmann.emails]
 
 [essmann.emails.essmann_email]
 user = [
   "robin",
   "essmann",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [essmann.homepages]
 
 [felgenhauer]
 name = "Bertram Felgenhauer"
 
 [felgenhauer.emails]
 
 [felgenhauer.emails.felgenhauer_email]
 user = [
   "bertram",
   "felgenhauer",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [felgenhauer.emails.felgenhauer_email1]
 user = [
   "int-e",
 ]
 host = [
   "gmx",
   "de",
 ]
 
 [felgenhauer.homepages]
 
 [feliachi]
 name = "Abderrahmane Feliachi"
 
 [feliachi.emails]
 
 [feliachi.emails.feliachi_email]
 user = [
   "abderrahmane",
   "feliachi",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [feliachi.homepages]
 
 [fell]
 name = "Julian Fell"
 
 [fell.emails]
 
 [fell.emails.fell_email]
 user = [
   "julian",
   "fell",
 ]
 host = [
   "uq",
   "net",
   "au",
 ]
 
 [fell.homepages]
 
 [fernandez]
 name = "Matthew Fernandez"
 
 [fernandez.emails]
 
 [fernandez.homepages]
 
 [fiedler]
 name = "Ben Fiedler"
 
 [fiedler.emails]
 
 [fiedler.emails.fiedler_email]
 user = [
   "ben",
   "fiedler",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [fiedler.homepages]
 
 [fleuriot]
 name = "Jacques D. Fleuriot"
 
 [fleuriot.emails]
 
 [fleuriot.emails.fleuriot_email]
 user = [
   "Jacques",
   "Fleuriot",
 ]
 host = [
   "ed",
   "ac",
   "uk",
 ]
 
 [fleuriot.emails.fleuriot_email1]
 user = [
   "jdf",
 ]
 host = [
   "ed",
   "ac",
   "uk",
 ]
 
 [fleuriot.homepages]
 fleuriot_homepage = "https://www.inf.ed.ac.uk/people/staff/Jacques_Fleuriot.html"
 
 [fleury]
 name = "Mathias Fleury"
 
 [fleury.emails]
 
 [fleury.emails.fleury_email]
 user = [
   "fleury",
 ]
 host = [
   "mpi-inf",
   "mpg",
   "de",
 ]
 
 [fleury.emails.fleury_email1]
 user = [
   "mathias",
   "fleury",
 ]
 host = [
   "jku",
   "at",
 ]
 
 [fleury.homepages]
 fleury_homepage = "http://fmv.jku.at/fleury"
 
 [foster]
 name = "Michael Foster"
 
 [foster.emails]
 
 [foster.emails.foster_email]
 user = [
   "m",
   "foster",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [foster.homepages]
 
 [fosterj]
 name = "J. Nathan Foster"
 
 [fosterj.emails]
 
 [fosterj.homepages]
 fosterj_homepage = "http://www.cs.cornell.edu/~jnfoster/"
 
 [fosters]
 name = "Simon Foster"
 
 [fosters.emails]
 
 [fosters.emails.fosters_email]
 user = [
   "simon",
   "foster",
 ]
 host = [
   "york",
   "ac",
   "uk",
 ]
 
 [fosters.homepages]
 fosters_homepage = "https://www-users.cs.york.ac.uk/~simonf/"
 
 [fouillard]
 name = "Valentin Fouillard"
 
 [fouillard.emails]
 
 [fouillard.emails.fouillard_email]
 user = [
   "valentin",
   "fouillard",
 ]
 host = [
   "limsi",
   "fr",
 ]
 
 [fouillard.homepages]
 
 [friedrich]
 name = "Stefan Friedrich"
 
 [friedrich.emails]
 
 [friedrich.homepages]
 
 [from]
 name = "Asta Halkjær From"
 
 [from.emails]
 
 [from.emails.from_email]
 user = [
   "ahfrom",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [from.homepages]
 from_homepage = "https://people.compute.dtu.dk/ahfrom/"
 
 [fuenmayor]
 name = "David Fuenmayor"
 
 [fuenmayor.emails]
 
 [fuenmayor.emails.fuenmayor_email]
 user = [
   "davfuenmayor",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [fuenmayor.homepages]
 
 [furusawa]
 name = "Hitoshi Furusawa"
 
 [furusawa.emails]
 
 [furusawa.homepages]
 furusawa_homepage = "http://www.sci.kagoshima-u.ac.jp/~furusawa/"
 
 [gammie]
 name = "Peter Gammie"
 
 [gammie.emails]
 
 [gammie.emails.gammie_email]
 user = [
   "peteg42",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [gammie.homepages]
 gammie_homepage = "http://peteg.org"
 
 [gao]
 name = "Xin Gao"
 
 [gao.emails]
 
 [gao.homepages]
 
 [gaudel]
 name = "Marie-Claude Gaudel"
 
 [gaudel.emails]
 
 [gaudel.emails.gaudel_email]
 user = [
   "mcg",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [gaudel.homepages]
 
 [gay]
 name = "Richard Gay"
 
 [gay.emails]
 
 [gay.emails.gay_email]
 user = [
   "gay",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [gay.homepages]
 
 [georgescu]
 name = "George Georgescu"
 
 [georgescu.emails]
 
 [georgescu.homepages]
 
 [gheri]
 name = "Lorenzo Gheri"
 
 [gheri.emails]
 
 [gheri.emails.gheri_email]
 user = [
   "lor",
   "gheri",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [gheri.homepages]
 
 [ghourabi]
 name = "Fadoua Ghourabi"
 
 [ghourabi.emails]
 
 [ghourabi.emails.ghourabi_email]
 user = [
   "fadouaghourabi",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [ghourabi.homepages]
 
 [gioiosa]
 name = "Gianpaolo Gioiosa"
 
 [gioiosa.emails]
 
 [gioiosa.homepages]
 
 [glabbeek]
 name = "Rob van Glabbeek"
 
 [glabbeek.emails]
 
 [glabbeek.homepages]
 glabbeek_homepage = "http://theory.stanford.edu/~rvg/"
 
 [gomes]
 name = "Victor B. F. Gomes"
 
 [gomes.emails]
 
 [gomes.emails.gomes_email]
 user = [
   "victor",
   "gomes",
 ]
 host = [
   "cl",
   "cam",
   "ac",
   "uk",
 ]
 
 [gomes.emails.gomes_email2]
 user = [
   "victorborgesfg",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [gomes.emails.gomes_email4]
 user = [
   "vborgesferreiragomes1",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [gomes.homepages]
 gomes_homepage = "http://www.dcs.shef.ac.uk/~victor"
 
 [gonzalez]
 name = "Edgar Gonzàlez"
 orcid = "0000-0002-9169-0769"
 
 [gonzalez.emails]
 
 [gonzalez.emails.gonzalez_email]
 user = [
   "edgargip",
 ]
 host = [
   "google",
   "com",
 ]
 
 [gonzalez.homepages]
 
 [gore]
 name = "Rajeev Gore"
 
 [gore.emails]
 
 [gore.emails.gore_email]
 user = [
   "rajeev",
   "gore",
 ]
 host = [
   "anu",
   "edu",
   "au",
 ]
 
 [gore.homepages]
 
 [gouezel]
 name = "Sebastien Gouezel"
 
 [gouezel.emails]
 
 [gouezel.emails.gouezel_email]
 user = [
   "sebastien",
   "gouezel",
 ]
 host = [
   "univ-rennes1",
   "fr",
 ]
 
 [gouezel.homepages]
 gouezel_homepage = "http://www.math.sciences.univ-nantes.fr/~gouezel/"
 
 [grechuk]
 name = "Bogdan Grechuk"
 
 [grechuk.emails]
 
 [grechuk.emails.grechuk_email]
 user = [
   "grechukbogdan",
 ]
 host = [
   "yandex",
   "ru",
 ]
 
 [grechuk.homepages]
 
 [grewe]
 name = "Sylvia Grewe"
 
 [grewe.emails]
 
 [grewe.emails.grewe_email]
 user = [
   "grewe",
 ]
 host = [
   "cs",
   "tu-darmstadt",
   "de",
 ]
 
 [grewe.homepages]
 
 [griebel]
 name = "Simon Griebel"
 
 [griebel.emails]
 
 [griebel.emails.griebel_email]
 user = [
   "s",
   "griebel",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [griebel.homepages]
 
 [grov]
 name = "Gudmund Grov"
 
 [grov.emails]
 
 [grov.emails.grov_email]
 user = [
   "ggrov",
 ]
 host = [
   "inf",
   "ed",
   "ac",
   "uk",
 ]
 
 [grov.homepages]
 grov_homepage = "http://homepages.inf.ed.ac.uk/ggrov"
 
 [guerraoui]
 name = "Rachid Guerraoui"
 
 [guerraoui.emails]
 
 [guerraoui.emails.guerraoui_email]
 user = [
   "rachid",
   "guerraoui",
 ]
 host = [
   "epfl",
   "ch",
 ]
 
 [guerraoui.homepages]
 
 [guiol]
 name = "Hervé Guiol"
 
 [guiol.emails]
 
 [guiol.emails.guiol_email]
 user = [
   "herve",
   "guiol",
 ]
 host = [
   "univ-grenoble-alpes",
   "fr",
 ]
 
 [guiol.homepages]
 
 [gunther]
 name = "Emmanuel Gunther"
 
 [gunther.emails]
 
 [gunther.emails.gunther_email]
 user = [
   "gunther",
 ]
 host = [
   "famaf",
   "unc",
   "edu",
   "ar",
 ]
 
 [gunther.homepages]
 
 [gutkovas]
 name = "Ramunas Gutkovas"
 
 [gutkovas.emails]
 
 [gutkovas.emails.gutkovas_email]
 user = [
   "ramunas",
   "gutkovas",
 ]
 host = [
   "it",
   "uu",
   "se",
 ]
 
 [gutkovas.homepages]
 
 [guttmann]
 name = "Walter Guttmann"
 
 [guttmann.emails]
 
 [guttmann.emails.guttmann_email]
 user = [
   "walter",
   "guttmann",
 ]
 host = [
   "canterbury",
   "ac",
   "nz",
 ]
 
 [guttmann.homepages]
 guttmann_homepage = "https://www.cosc.canterbury.ac.nz/walter.guttmann/"
 
 [guzman]
 name = "Laura P. Gamboa Guzman"
 
 [guzman.emails]
 
 [guzman.emails.guzman_email]
 user = [
   "lpgamboa",
 ]
 host = [
   "iastate",
   "edu",
 ]
 
 [guzman.homepages]
 guzman_homepage = "https://sites.google.com/view/lpgamboa/home"
 
 [haftmann]
 name = "Florian Haftmann"
 
 [haftmann.emails]
 
 [haftmann.emails.haftmann_email]
 user = [
   "florian",
   "haftmann",
 ]
 host = [
   "informatik",
   "tu-muenchen",
   "de",
 ]
 
 [haftmann.homepages]
 haftmann_homepage = "http://isabelle.in.tum.de/~haftmann"
 
 [haslbeck]
 name = "Max W. Haslbeck"
 
 [haslbeck.emails]
 
 [haslbeck.emails.haslbeck_email]
 user = [
   "maximilian",
   "haslbeck",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [haslbeck.emails.haslbeck_email1]
 user = [
   "haslbecm",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [haslbeck.emails.haslbeck_email2]
 user = [
   "max",
   "haslbeck",
 ]
 host = [
   "gmx",
   "de",
 ]
 
 [haslbeck.homepages]
 haslbeck_homepage = "http://cl-informatik.uibk.ac.at/users/mhaslbeck/"
 
 [haslbeckm]
 name = "Maximilian P. L. Haslbeck"
 
 [haslbeckm.emails]
 
 [haslbeckm.emails.haslbeckm_email]
 user = [
   "haslbema",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [haslbeckm.homepages]
 haslbeckm_homepage = "http://in.tum.de/~haslbema/"
 
 [havle]
 name = "Oto Havle"
 
 [havle.emails]
 
 [havle.emails.havle_email]
 user = [
   "oha",
 ]
 host = [
   "sysgo",
   "com",
 ]
 
 [havle.homepages]
 
 [hayes]
 name = "Ian J. Hayes"
 
 [hayes.emails]
 
 [hayes.emails.hayes_email]
 user = [
   "ian",
   "hayes",
 ]
 host = [
   "itee",
   "uq",
   "edu",
   "au",
 ]
 
 [hayes.homepages]
 
 [he]
 name = "Yijun He"
 
 [he.emails]
 
 [he.emails.he_email]
 user = [
   "yh403",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [he.homepages]
 
 [heimes]
 name = "Lukas Heimes"
 
 [heimes.emails]
 
 [heimes.emails.heimes_email]
 user = [
   "heimesl",
 ]
 host = [
   "student",
   "ethz",
   "ch",
 ]
 
 [heimes.homepages]
 
 [helke]
 name = "Steffen Helke"
 
 [helke.emails]
 
 [helke.emails.helke_email]
 user = [
   "helke",
 ]
 host = [
   "cs",
   "tu-berlin",
   "de",
 ]
 
 [helke.homepages]
 
 [hellauer]
 name = "Fabian Hellauer"
 
 [hellauer.emails]
 
 [hellauer.emails.hellauer_email]
 user = [
   "hellauer",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [hellauer.homepages]
 
 [heller]
 name = "Armin Heller"
 
 [heller.emails]
 
 [heller.homepages]
 
 [henrio]
 name = "Ludovic Henrio"
 
 [henrio.emails]
 
 [henrio.emails.henrio_email]
 user = [
   "Ludovic",
   "Henrio",
 ]
 host = [
   "sophia",
   "inria",
   "fr",
 ]
 
 [henrio.homepages]
 
 [herzberg]
 name = "Michael Herzberg"
 
 [herzberg.emails]
 
 [herzberg.emails.herzberg_email]
 user = [
   "mail",
 ]
 host = [
   "michael-herzberg",
   "de",
 ]
 
 [herzberg.homepages]
 herzberg_homepage = "http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg"
 
 [hess]
 name = "Andreas V. Hess"
 
 [hess.emails]
 
 [hess.emails.hess_email]
 user = [
   "avhe",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [hess.emails.hess_email1]
 user = [
   "andreasvhess",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [hess.homepages]
 
 [hetzl]
 name = "Stefan Hetzl"
 
 [hetzl.emails]
 
 [hetzl.emails.hetzl_email]
 user = [
   "hetzl",
 ]
 host = [
   "logic",
   "at",
 ]
 
 [hetzl.homepages]
 hetzl_homepage = "http://www.logic.at/people/hetzl/"
 
 [hibon]
 name = "Quentin Hibon"
 
 [hibon.emails]
 
 [hibon.emails.hibon_email]
 user = [
   "qh225",
 ]
 host = [
   "cl",
   "cam",
   "ac",
   "uk",
 ]
 
 [hibon.homepages]
 
 [hirata]
 name = "Michikazu Hirata"
 
 [hirata.emails]
 
 [hirata.emails.hirata_email]
 user = [
   "hirata",
   "m",
   "ac",
 ]
 host = [
   "m",
   "titech",
   "ac",
   "jp",
 ]
 
 [hirata.homepages]
 
 [hoefner]
 name = "Peter Höfner"
 
 [hoefner.emails]
 
 [hoefner.emails.hoefner_email]
 user = [
   "peter",
 ]
 host = [
   "hoefner-online",
   "de",
 ]
 
 [hoefner.homepages]
 hoefner_homepage = "http://www.hoefner-online.de/"
 
 [hoelzl]
 name = "Johannes Hölzl"
 
 [hoelzl.emails]
 
 [hoelzl.emails.hoelzl_email]
 user = [
   "hoelzl",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [hoelzl.homepages]
 hoelzl_homepage = "http://home.in.tum.de/~hoelzl"
 
 [hofmann]
 name = "Martin Hofmann"
 
 [hofmann.emails]
 
 [hofmann.homepages]
 hofmann_homepage = "http://www.tcs.informatik.uni-muenchen.de/~mhofmann"
 
+[hofmeier]
+name = "Paul Hofmeier"
+
+[hofmeier.emails]
+
+[hofmeier.emails.hofmeier_email]
+user = [
+  "paul",
+  "hofmeier",
+]
+host = [
+  "tum",
+  "de",
+]
+
+[hofmeier.homepages]
+
 [holub]
 name = "Štěpán Holub"
 
 [holub.emails]
 
 [holub.emails.holub_email]
 user = [
   "holub",
 ]
 host = [
   "karlin",
   "mff",
   "cuni",
   "cz",
 ]
 
 [holub.homepages]
 holub_homepage = "https://www2.karlin.mff.cuni.cz/~holub/"
 
 [hosking]
 name = "Tony Hosking"
 
 [hosking.emails]
 
 [hosking.homepages]
 hosking_homepage = "https://www.cs.purdue.edu/homes/hosking/"
 
 [hou]
 name = "Zhe Hou"
 
 [hou.emails]
 
 [hou.emails.hou_email]
 user = [
   "zhe",
   "hou",
 ]
 host = [
   "ntu",
   "edu",
   "sg",
 ]
 
 [hou.homepages]
 
 [hu]
 name = "Shuwei Hu"
 
 [hu.emails]
 
 [hu.emails.hu_email]
 user = [
   "shuwei",
   "hu",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [hu.homepages]
 
 [huffman]
 name = "Brian Huffman"
 
 [huffman.emails]
 
 [huffman.emails.huffman_email]
 user = [
   "huffman",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [huffman.emails.huffman_email1]
 user = [
   "brianh",
 ]
 host = [
   "cs",
   "pdx",
   "edu",
 ]
 
 [huffman.homepages]
 huffman_homepage = "http://cs.pdx.edu/~brianh/"
 
 [hupel]
 name = "Lars Hupel"
 
 [hupel.emails]
 
 [hupel.emails.hupel_email]
 user = [
   "lars",
 ]
 host = [
   "hupel",
   "info",
 ]
 
 [hupel.homepages]
 hupel_homepage = "https://lars.hupel.info/"
 
 [ijbema]
 name = "Mark Ijbema"
 
 [ijbema.emails]
 
 [ijbema.emails.ijbema_email]
 user = [
   "ijbema",
 ]
 host = [
   "fmf",
   "nl",
 ]
 
 [ijbema.homepages]
 
 [immler]
 name = "Fabian Immler"
 
 [immler.emails]
 
 [immler.emails.immler_email]
 user = [
   "immler",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [immler.emails.immler_email1]
 user = [
   "fimmler",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [immler.homepages]
 immler_homepage = "https://home.in.tum.de/~immler/"
 
 [ito]
 name = "Yosuke Ito"
 
 [ito.emails]
 
 [ito.emails.ito_email]
 user = [
   "glacier345",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [ito.homepages]
 
 [iwama]
 name = "Fumiya Iwama"
 
 [iwama.emails]
 
 [iwama.emails.iwama_email]
 user = [
   "d1623001",
 ]
 host = [
   "s",
   "konan-u",
   "ac",
   "jp",
 ]
 
 [iwama.homepages]
 
 [jacobsen]
 name = "Frederik Krogsdal Jacobsen"
 
 [jacobsen.emails]
 
 [jacobsen.emails.jacobsen_email]
 user = [
   "fkjac",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [jacobsen.homepages]
 jacobsen_homepage = "http://people.compute.dtu.dk/fkjac/"
 
 [jaskelioff]
 name = "Mauro Jaskelioff"
 
 [jaskelioff.emails]
 
 [jaskelioff.homepages]
 jaskelioff_homepage = "http://www.fceia.unr.edu.ar/~mauro/"
 
 [jaskolka]
 name = "Jason Jaskolka"
 
 [jaskolka.emails]
 
 [jaskolka.emails.jaskolka_email]
 user = [
   "jason",
   "jaskolka",
 ]
 host = [
   "carleton",
   "ca",
 ]
 
 [jaskolka.homepages]
 jaskolka_homepage = "https://carleton.ca/jaskolka/"
 
 [jensen]
 name = "Alexander Birch Jensen"
 
 [jensen.emails]
 
 [jensen.emails.jensen_email]
 user = [
   "aleje",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [jensen.homepages]
 jensen_homepage = "https://people.compute.dtu.dk/aleje/"
 
 [jiang]
 name = "Nan Jiang"
 
 [jiang.emails]
 
 [jiang.emails.jiang_email]
 user = [
   "nanjiang",
 ]
 host = [
   "whu",
   "edu",
   "cn",
 ]
 
 [jiang.homepages]
 
 [jiangd]
 name = "Dongchen Jiang"
 
 [jiangd.emails]
 
 [jiangd.emails.jiangd_email]
 user = [
   "dongchenjiang",
 ]
 host = [
   "googlemail",
   "com",
 ]
 
 [jiangd.homepages]
 
 [joosten]
 name = "Sebastiaan J. C. Joosten"
 
 [joosten.emails]
 
 [joosten.emails.joosten_email]
 user = [
   "sebastiaan",
   "joosten",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [joosten.emails.joosten_email1]
 user = [
   "sjcjoosten",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [joosten.emails.joosten_email2]
 user = [
   "s",
   "j",
   "c",
   "joosten",
 ]
 host = [
   "utwente",
   "nl",
 ]
 
 [joosten.homepages]
 joosten_homepage = "https://sjcjoosten.nl/"
 
 [jungnickel]
 name = "Tim Jungnickel"
 
 [jungnickel.emails]
 
 [jungnickel.emails.jungnickel_email]
 user = [
   "tim",
   "jungnickel",
 ]
 host = [
   "tu-berlin",
   "de",
 ]
 
 [jungnickel.homepages]
 
 [kadzioka]
 name = "Maya Kądziołka"
 
 [kadzioka.emails]
 
 [kadzioka.emails.kadzioka_email]
 user = [
   "afp",
 ]
 host = [
   "compilercrim",
   "es",
 ]
 
 [kadzioka.homepages]
 
 [kaliszyk]
 name = "Cezary Kaliszyk"
 
 [kaliszyk.emails]
 
 [kaliszyk.emails.kaliszyk_email]
 user = [
   "cezary",
   "kaliszyk",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [kaliszyk.homepages]
 kaliszyk_homepage = "http://cl-informatik.uibk.ac.at/users/cek/"
 
 [kammueller]
 name = "Florian Kammüller"
 
 [kammueller.emails]
 
 [kammueller.emails.kammueller_email]
 user = [
   "flokam",
 ]
 host = [
   "cs",
   "tu-berlin",
   "de",
 ]
 
 [kammueller.emails.kammueller_email1]
 user = [
   "florian",
   "kammuller",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [kammueller.homepages]
 kammueller_homepage = "http://www.cs.mdx.ac.uk/people/florian-kammueller/"
 
 [kappelmann]
 name = "Kevin Kappelmann"
 
 [kappelmann.emails]
 
 [kappelmann.emails.kappelmann_email]
 user = [
   "kevin",
   "kappelmann",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [kappelmann.homepages]
 kappelmann_homepage = "https://www21.in.tum.de/team/kappelmk/"
 
 [karayel]
 name = "Emin Karayel"
 orcid = "0000-0003-3290-5034"
 
 [karayel.emails]
 
 [karayel.emails.karayel_email]
 user = [
   "me",
 ]
 host = [
   "eminkarayel",
   "de",
 ]
 
 [karayel.homepages]
 karayel_homepage = "https://orcid.org/0000-0003-3290-5034"
 
 [kastermans]
 name = "Bart Kastermans"
 
 [kastermans.emails]
 
 [kastermans.homepages]
 kastermans_homepage = "http://kasterma.net"
 
 [katovsky]
 name = "Alexander Katovsky"
 
 [katovsky.emails]
 
 [katovsky.emails.katovsky_email]
 user = [
   "apk32",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [katovsky.emails.katovsky_email1]
 user = [
   "alexander",
   "katovsky",
 ]
 host = [
   "cantab",
   "net",
 ]
 
 [katovsky.homepages]
 
 [kaufmann]
 name = "Daniela Kaufmann"
 
 [kaufmann.emails]
 
 [kaufmann.homepages]
 kaufmann_homepage = "http://fmv.jku.at/kaufmann"
 
 [keefe]
 name = "Greg O'Keefe"
 
 [keefe.emails]
 
 [keefe.homepages]
 keefe_homepage = "http://users.rsise.anu.edu.au/~okeefe/"
 
 [keinholz]
 name = "Jonas Keinholz"
 
 [keinholz.emails]
 
 [keinholz.homepages]
 
 [kerber]
 name = "Manfred Kerber"
 
 [kerber.emails]
 
 [kerber.emails.kerber_email]
 user = [
   "mnfrd",
   "krbr",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [kerber.homepages]
 kerber_homepage = "http://www.cs.bham.ac.uk/~mmk"
 
 [ketland]
 name = "Jeffrey Ketland"
 
 [ketland.emails]
 
 [ketland.emails.ketland_email]
 user = [
   "jeffreyketland",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [ketland.homepages]
 
 [kirchner]
 name = "Daniel Kirchner"
 
 [kirchner.emails]
 
 [kirchner.emails.kirchner_email]
 user = [
   "daniel",
 ]
 host = [
   "ekpyron",
   "org",
 ]
 
 [kirchner.homepages]
 
 [klein]
 name = "Gerwin Klein"
 
 [klein.emails]
 
 [klein.emails.klein_email]
 user = [
   "kleing",
 ]
 host = [
   "unsw",
   "edu",
   "au",
 ]
 
 [klein.homepages]
 klein_homepage = "http://www.cse.unsw.edu.au/~kleing/"
 
 [klenze]
 name = "Tobias Klenze"
 
 [klenze.emails]
 
 [klenze.emails.klenze_email]
 user = [
   "tobias",
   "klenze",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [klenze.homepages]
 
 [kleppmann]
 name = "Martin Kleppmann"
 
 [kleppmann.emails]
 
 [kleppmann.emails.kleppmann_email]
 user = [
   "martin",
   "kleppmann",
 ]
 host = [
   "cl",
   "cam",
   "ac",
   "uk",
 ]
 
 [kleppmann.homepages]
 
 [kobayashi]
 name = "Hidetsune Kobayashi"
 
 [kobayashi.emails]
 
 [kobayashi.homepages]
 
 [koerner]
 name = "Stefan Körner"
 
 [koerner.emails]
 
 [koerner.emails.koerner_email]
 user = [
   "s_koer03",
 ]
 host = [
   "uni-muenster",
   "de",
 ]
 
 [koerner.homepages]
 
 [kolanski]
 name = "Rafal Kolanski"
 
 [kolanski.emails]
 
 [kolanski.emails.kolanski_email]
 user = [
   "rafal",
   "kolanski",
 ]
 host = [
   "nicta",
   "com",
   "au",
 ]
 
 [kolanski.homepages]
 
 [koller]
 name = "Lukas Koller"
 
 [koller.emails]
 
 [koller.emails.koller_email]
 user = [
   "lukas",
   "koller",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [koller.homepages]
 
 [krauss]
 name = "Alexander Krauss"
 
 [krauss.emails]
 
 [krauss.emails.krauss_email]
 user = [
   "krauss",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [krauss.homepages]
 krauss_homepage = "http://www.in.tum.de/~krauss"
 
 [kreuzer]
 name = "Katharina Kreuzer"
 
 [kreuzer.emails]
 
 [kreuzer.emails.kreuzer_email]
 user = [
   "kreuzerk",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [kreuzer.emails.kreuzer_email1]
 user = [
   "k",
   "kreuzer",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [kreuzer.homepages]
 kreuzer_homepage = "https://www21.in.tum.de/team/kreuzer/"
 
 [kuncak]
 name = "Viktor Kuncak"
 
 [kuncak.emails]
 
 [kuncak.homepages]
 kuncak_homepage = "http://lara.epfl.ch/~kuncak/"
 
 [kuncar]
 name = "Ondřej Kunčar"
 
 [kuncar.emails]
 
 [kuncar.homepages]
 kuncar_homepage = "http://www21.in.tum.de/~kuncar/"
 
 [kurz]
 name = "Friedrich Kurz"
 
 [kurz.emails]
 
 [kurz.emails.kurz_email]
 user = [
   "friedrich",
   "kurz",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [kurz.homepages]
 
 [lachnitt]
 name = "Hanna Lachnitt"
 
 [lachnitt.emails]
 
 [lachnitt.emails.lachnitt_email]
 user = [
   "lachnitt",
 ]
 host = [
   "stanford",
   "edu",
 ]
 
 [lachnitt.homepages]
 
 [lallemand]
 name = "Joseph Lallemand"
 
 [lallemand.emails]
 
 [lallemand.emails.lallemand_email]
 user = [
   "joseph",
   "lallemand",
 ]
 host = [
   "loria",
   "fr",
 ]
 
 [lallemand.homepages]
 
 [lammich]
 name = "Peter Lammich"
 
 [lammich.emails]
 
 [lammich.emails.lammich_email]
 user = [
   "lammich",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [lammich.emails.lammich_email1]
 user = [
   "peter",
   "lammich",
 ]
 host = [
   "uni-muenster",
   "de",
 ]
 
 [lammich.homepages]
 lammich_homepage = "http://www21.in.tum.de/~lammich"
 
 [lange]
 name = "Christoph Lange"
 
 [lange.emails]
 
 [lange.emails.lange_email]
 user = [
   "math",
   "semantic",
   "web",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [lange.homepages]
 
 [langenstein]
 name = "Bruno Langenstein"
 
 [langenstein.emails]
 
 [langenstein.emails.langenstein_email]
 user = [
   "langenstein",
 ]
 host = [
   "dfki",
   "de",
 ]
 
 [langenstein.homepages]
 
 [lattuada]
 name = "Andrea Lattuada"
 
 [lattuada.emails]
 
 [lattuada.homepages]
 lattuada_homepage = "https://andrea.lattuada.me"
 
 [laursen]
 name = "Christian Pardillo-Laursen"
 
 [laursen.emails]
 
 [laursen.emails.laursen_email]
 user = [
   "christian",
   "laursen",
 ]
 host = [
   "york",
   "ac",
   "uk",
 ]
 
 [laursen.homepages]
 
 [lee]
 name = "Holden Lee"
 
 [lee.emails]
 
 [lee.emails.lee_email]
 user = [
   "holdenl",
 ]
 host = [
   "princeton",
   "edu",
 ]
 
 [lee.homepages]
 
 [leustean]
 name = "Laurentiu Leustean"
 
 [leustean.emails]
 
 [leustean.homepages]
 
 [lewis]
 name = "Corey Lewis"
 
 [lewis.emails]
 
 [lewis.emails.lewis_email]
 user = [
   "corey",
   "lewis",
 ]
 host = [
   "data61",
   "csiro",
   "au",
 ]
 
 [lewis.homepages]
 
 [li]
 name = "Wenda Li"
 
 [li.emails]
 
 [li.emails.li_email]
 user = [
   "wl302",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [li.emails.li_email1]
 user = [
   "liwenda1990",
 ]
 host = [
   "hotmail",
   "com",
 ]
 
 [li.homepages]
 li_homepage = "https://www.cl.cam.ac.uk/~wl302/"
 
 [lim]
 name = "Japheth Lim"
 
 [lim.emails]
 
 [lim.homepages]
 
 [lindenberg]
 name = "Christina Lindenberg"
 
 [lindenberg.emails]
 
 [lindenberg.homepages]
 
 [linker]
 name = "Sven Linker"
 
 [linker.emails]
 
 [linker.emails.linker_email]
 user = [
   "s",
   "linker",
 ]
 host = [
   "liverpool",
   "ac",
   "uk",
 ]
 
 [linker.homepages]
 
 [liu]
 name = "Junyi Liu"
 
 [liu.emails]
 
 [liu.homepages]
 
 [liut]
 name = "Tao Liu"
 
 [liut.emails]
 
 [liut.homepages]
 
 [liuy]
 name = "Yang Liu"
 
 [liuy.emails]
 
 [liuy.emails.liuy_email]
 user = [
   "yangliu",
 ]
 host = [
   "ntu",
   "edu",
   "sg",
 ]
 
 [liuy.homepages]
 
 [liy]
 name = "Yangjia Li"
 
 [liy.emails]
 
 [liy.homepages]
 
 [lochbihler]
 name = "Andreas Lochbihler"
 
 [lochbihler.emails]
 
 [lochbihler.emails.lochbihler_email]
 user = [
   "andreas",
   "lochbihler",
 ]
 host = [
   "digitalasset",
   "com",
 ]
 
 [lochbihler.emails.lochbihler_email1]
 user = [
   "mail",
 ]
 host = [
   "andreas-lochbihler",
   "de",
 ]
 
 [lochbihler.homepages]
 lochbihler_homepage = "http://www.andreas-lochbihler.de/"
 
 [lochmann]
 name = "Alexander Lochmann"
 
 [lochmann.emails]
 
 [lochmann.emails.lochmann_email]
 user = [
   "alexander",
   "lochmann",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [lochmann.homepages]
 
 [lohner]
 name = "Denis Lohner"
 
 [lohner.emails]
 
 [lohner.emails.lohner_email]
 user = [
   "denis",
   "lohner",
 ]
 host = [
   "kit",
   "edu",
 ]
 
 [lohner.homepages]
 lohner_homepage = "http://pp.ipd.kit.edu/person.php?id=88"
 
 [loibl]
 name = "Matthias Loibl"
 
 [loibl.emails]
 
 [loibl.homepages]
 
 [londono]
 name = "Alejandro Gómez-Londoño"
 
 [londono.emails]
 
 [londono.emails.londono_email]
 user = [
   "alejandro",
   "gomez",
 ]
 host = [
   "chalmers",
   "se",
 ]
 
 [londono.homepages]
 
 [losa]
 name = "Giuliano Losa"
 
 [losa.emails]
 
 [losa.emails.losa_email]
 user = [
   "giuliano",
   "losa",
 ]
 host = [
   "epfl",
   "ch",
 ]
 
 [losa.emails.losa_email1]
 user = [
   "giuliano",
 ]
 host = [
   "galois",
   "com",
 ]
 
 [losa.emails.losa_email2]
 user = [
   "giuliano",
 ]
 host = [
   "losa",
   "fr",
 ]
 
 [losa.homepages]
 
 [lutz]
 name = "Bianca Lutz"
 
 [lutz.emails]
 
 [lutz.emails.lutz_email]
 user = [
   "sowilo",
 ]
 host = [
   "cs",
   "tu-berlin",
   "de",
 ]
 
 [lutz.homepages]
 
 [lux]
 name = "Alexander Lux"
 
 [lux.emails]
 
 [lux.emails.lux_email]
 user = [
   "lux",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [lux.homepages]
 
 [makarios]
 name = "T. J. M. Makarios"
 
 [makarios.emails]
 
 [makarios.emails.makarios_email]
 user = [
   "tjm1983",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [makarios.homepages]
 
 [maletzky]
 name = "Alexander Maletzky"
 
 [maletzky.emails]
 
 [maletzky.emails.maletzky_email]
 user = [
   "alexander",
   "maletzky",
 ]
 host = [
   "risc",
   "jku",
   "at",
 ]
 
 [maletzky.emails.maletzky_email1]
 user = [
   "alexander",
   "maletzky",
 ]
 host = [
   "risc-software",
   "at",
 ]
 
 [maletzky.homepages]
 maletzky_homepage = "https://risc.jku.at/m/alexander-maletzky/"
 
 [mansky]
 name = "Susannah Mansky"
 
 [mansky.emails]
 
 [mansky.emails.mansky_email]
 user = [
   "sjohnsn2",
 ]
 host = [
   "illinois",
   "edu",
 ]
 
 [mansky.emails.mansky_email1]
 user = [
   "susannahej",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [mansky.homepages]
 
 [mantel]
 name = "Heiko Mantel"
 
 [mantel.emails]
 
 [mantel.emails.mantel_email]
 user = [
   "mantel",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [mantel.homepages]
 
 [margetson]
 name = "James Margetson"
 
 [margetson.emails]
 
 [margetson.homepages]
 
 [maric]
 name = "Ognjen Marić"
 
 [maric.emails]
 
 [maric.emails.maric_email]
 user = [
   "ogi",
   "afp",
 ]
 host = [
   "mynosefroze",
   "com",
 ]
 
 [maric.homepages]
 
 [maricf]
 name = "Filip Marić"
 
 [maricf.emails]
 
 [maricf.emails.maricf_email]
 user = [
   "filip",
 ]
 host = [
   "matf",
   "bg",
   "ac",
   "rs",
 ]
 
 [maricf.homepages]
 maricf_homepage = "http://www.matf.bg.ac.rs/~filip"
 
 [marmsoler]
 name = "Diego Marmsoler"
 
 [marmsoler.emails]
 
 [marmsoler.emails.marmsoler_email]
 user = [
   "diego",
   "marmsoler",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [marmsoler.emails.marmsoler_email1]
 user = [
   "d",
   "marmsoler",
 ]
 host = [
   "exeter",
   "ac",
   "uk",
 ]
 
 [marmsoler.homepages]
 marmsoler_homepage = "http://marmsoler.com"
 
 [matache]
 name = "Cristina Matache"
 
 [matache.emails]
 
 [matache.emails.matache_email]
 user = [
   "cris",
   "matache",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [matache.homepages]
 
 [matichuk]
 name = "Daniel Matichuk"
 
 [matichuk.emails]
 
 [matichuk.homepages]
 
 [matiyasevich]
 name = "Yuri Matiyasevich"
 
 [matiyasevich.emails]
 
 [matiyasevich.homepages]
 
 [maximova]
 name = "Alexandra Maximova"
 
 [maximova.emails]
 
 [maximova.emails.maximova_email]
 user = [
   "amaximov",
 ]
 host = [
   "student",
   "ethz",
   "ch",
 ]
 
 [maximova.homepages]
 
 [meis]
 name = "Rene Meis"
 
 [meis.emails]
 
 [meis.emails.meis_email]
 user = [
   "rene",
   "meis",
 ]
 host = [
   "uni-muenster",
   "de",
 ]
 
 [meis.emails.meis_email1]
 user = [
   "rene",
   "meis",
 ]
 host = [
   "uni-due",
   "de",
 ]
 
 [meis.homepages]
 
 [merz]
 name = "Stephan Merz"
 
 [merz.emails]
 
 [merz.emails.merz_email]
 user = [
   "Stephan",
   "Merz",
 ]
 host = [
   "loria",
   "fr",
 ]
 
 [merz.homepages]
 merz_homepage = "http://www.loria.fr/~merz"
 
 [messner]
 name = "Florian Messner"
 
 [messner.emails]
 
 [messner.emails.messner_email]
 user = [
   "florian",
   "g",
   "messner",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [messner.homepages]
 
 [michaelis]
 name = "Julius Michaelis"
 
 [michaelis.emails]
 
 [michaelis.emails.michaelis_email]
 user = [
   "isabelleopenflow",
 ]
 host = [
   "liftm",
   "de",
 ]
 
 [michaelis.emails.michaelis_email1]
 user = [
   "maintainafpppt",
 ]
 host = [
   "liftm",
   "de",
 ]
 
 [michaelis.emails.michaelis_email2]
 user = [
   "bdd",
 ]
 host = [
   "liftm",
   "de",
 ]
 
 [michaelis.emails.michaelis_email3]
 user = [
   "afp",
 ]
 host = [
   "liftm",
   "de",
 ]
 
 [michaelis.homepages]
 michaelis_homepage = "http://liftm.de/"
 
 [milehins]
 name = "Mihails Milehins"
 
 [milehins.emails]
 
 [milehins.emails.milehins_email]
 user = [
   "mihailsmilehins",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [milehins.homepages]
 
 [minamide]
 name = "Yasuhiko Minamide"
 
 [minamide.emails]
 
 [minamide.emails.minamide_email]
 user = [
   "minamide",
 ]
 host = [
   "is",
   "titech",
   "ac",
   "jp",
 ]
 
 [minamide.homepages]
 minamide_homepage = "https://sv.c.titech.ac.jp/minamide/index.en.html"
 
 [mitchell]
 name = "Neil Mitchell"
 
 [mitchell.emails]
 
 [mitchell.homepages]
 
 [mitsch]
 name = "Stefan Mitsch"
 
 [mitsch.emails]
 
 [mitsch.emails.mitsch_email]
 user = [
   "smitsch",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [mitsch.homepages]
 
 [moedersheim]
 name = "Sebastian Mödersheim"
 
 [moedersheim.emails]
 
 [moedersheim.emails.moedersheim_email]
 user = [
   "samo",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [moedersheim.homepages]
 moedersheim_homepage = "https://people.compute.dtu.dk/samo/"
 
 [moeller]
 name = "Bernhard Möller"
 
 [moeller.emails]
 
 [moeller.homepages]
 moeller_homepage = "https://www.informatik.uni-augsburg.de/en/chairs/dbis/pmi/staff/moeller/"
 
 [muendler]
 name = "Niels Mündler"
 
 [muendler.emails]
 
 [muendler.emails.muendler_email]
 user = [
   "n",
   "muendler",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [muendler.homepages]
 
 [mulligan]
 name = "Dominic P. Mulligan"
 
 [mulligan.emails]
 
 [mulligan.emails.mulligan_email]
 user = [
   "dominic",
   "p",
   "mulligan",
 ]
 host = [
   "googlemail",
   "com",
 ]
 
 [mulligan.emails.mulligan_email1]
 user = [
   "Dominic",
   "Mulligan",
 ]
 host = [
   "arm",
   "com",
 ]
 
 [mulligan.homepages]
 
 [munive]
 name = "Jonathan Julian Huerta y Munive"
 
 [munive.emails]
 
 [munive.emails.munive_email]
 user = [
   "jjhuertaymunive1",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [munive.emails.munive_email1]
 user = [
   "jonjulian23",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [munive.homepages]
 
 [murao]
 name = "H. Murao"
 
 [murao.emails]
 
 [murao.homepages]
 
 [murray]
 name = "Toby Murray"
 
 [murray.emails]
 
 [murray.emails.murray_email]
 user = [
   "toby",
   "murray",
 ]
 host = [
   "unimelb",
   "edu",
   "au",
 ]
 
 [murray.homepages]
 murray_homepage = "https://people.eng.unimelb.edu.au/tobym/"
 
 [nagashima]
 name = "Yutaka Nagashima"
 
 [nagashima.emails]
 
 [nagashima.emails.nagashima_email]
 user = [
   "Yutaka",
   "Nagashima",
 ]
 host = [
   "data61",
   "csiro",
   "au",
 ]
 
 [nagashima.homepages]
 
 [nagele]
 name = "Julian Nagele"
 
 [nagele.emails]
 
 [nagele.emails.nagele_email]
 user = [
   "julian",
   "nagele",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [nagele.homepages]
 
 [naraschewski]
 name = "Wolfgang Naraschewski"
 
 [naraschewski.emails]
 
 [naraschewski.homepages]
 
 [nedzelsky]
 name = "Michael Nedzelsky"
 
 [nedzelsky.emails]
 
 [nedzelsky.emails.nedzelsky_email]
 user = [
   "MichaelNedzelsky",
 ]
 host = [
   "yandex",
   "ru",
 ]
 
 [nedzelsky.homepages]
 
 [nemeti]
 name = "István Németi"
 
 [nemeti.emails]
 
 [nemeti.homepages]
 nemeti_homepage = "http://www.renyi.hu/~nemeti/"
 
 [nemouchi]
 name = "Yakoub Nemouchi"
 
 [nemouchi.emails]
 
 [nemouchi.emails.nemouchi_email]
 user = [
   "nemouchi",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [nemouchi.emails.nemouchi_email1]
 user = [
   "yakoub",
   "nemouchi",
 ]
 host = [
   "york",
   "ac",
   "uk",
 ]
 
 [nemouchi.homepages]
 
 [nestmann]
 name = "Uwe Nestmann"
 
 [nestmann.emails]
 
 [nestmann.homepages]
 nestmann_homepage = "https://www.mtv.tu-berlin.de/nestmann/"
 
 [neumann]
 name = "René Neumann"
 
 [neumann.emails]
 
 [neumann.emails.neumann_email]
 user = [
   "rene",
   "neumann",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [neumann.homepages]
 
 [nielsen]
 name = "Finn Nielsen"
 
 [nielsen.emails]
 
 [nielsen.emails.nielsen_email]
 user = [
   "finn",
   "nielsen",
 ]
 host = [
   "uni-muenster",
   "de",
 ]
 
 [nielsen.homepages]
 
 [nikiforov]
 name = "Denis Nikiforov"
 
 [nikiforov.emails]
 
 [nikiforov.emails.nikiforov_email]
 user = [
   "denis",
   "nikif",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [nikiforov.homepages]
 
 [nipkow]
 name = "Tobias Nipkow"
 orcid = "0000-0003-0730-515X"
 
 [nipkow.emails]
 
 [nipkow.emails.nipkow_email]
 user = [
   "nipkow",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [nipkow.homepages]
 nipkow_homepage = "https://www.in.tum.de/~nipkow/"
 
 [nishihara]
 name = "Toshiaki Nishihara"
 
 [nishihara.emails]
 
 [nishihara.homepages]
 
 [noce]
 name = "Pasquale Noce"
 
 [noce.emails]
 
 [noce.emails.noce_email]
 user = [
   "pasquale",
   "noce",
   "lavoro",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [noce.homepages]
 
 [nordhoff]
 name = "Benedikt Nordhoff"
 
 [nordhoff.emails]
 
 [nordhoff.emails.nordhoff_email]
 user = [
   "b",
   "n",
 ]
 host = [
   "wwu",
   "de",
 ]
 
 [nordhoff.emails.nordhoff_email1]
 user = [
   "b_nord01",
 ]
 host = [
   "uni-muenster",
   "de",
 ]
 
 [nordhoff.homepages]
 
 [noschinski]
 name = "Lars Noschinski"
 
 [noschinski.emails]
 
 [noschinski.emails.noschinski_email]
 user = [
   "noschinl",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [noschinski.homepages]
 noschinski_homepage = "http://www21.in.tum.de/~noschinl/"
 
 [obua]
 name = "Steven Obua"
 
 [obua.emails]
 
 [obua.emails.obua_email]
 user = [
   "steven",
 ]
 host = [
   "recursivemind",
   "com",
 ]
 
 [obua.homepages]
 
 [ogawa]
 name = "Mizuhito Ogawa"
 
 [ogawa.emails]
 
 [ogawa.homepages]
 
 [oldenburg]
 name = "Lennart Oldenburg"
 
 [oldenburg.emails]
 
 [oldenburg.homepages]
 
 [olm]
 name = "Markus Müller-Olm"
 
 [olm.emails]
 
 [olm.homepages]
 olm_homepage = "http://cs.uni-muenster.de/u/mmo/"
 
 [oosterhuis]
 name = "Roelof Oosterhuis"
 
 [oosterhuis.emails]
 
 [oosterhuis.emails.oosterhuis_email]
 user = [
   "roelofoosterhuis",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [oosterhuis.homepages]
 
 [oostrom]
 name = "Vincent van Oostrom"
 
 [oostrom.emails]
 
 [oostrom.homepages]
 
 [ortner]
 name = "Veronika Ortner"
 
 [ortner.emails]
 
 [ortner.homepages]
 
 [overbeek]
 name = "Roy Overbeek"
 
 [overbeek.emails]
 
 [overbeek.emails.overbeek_email]
 user = [
   "Roy",
   "Overbeek",
 ]
 host = [
   "cwi",
   "nl",
 ]
 
 [overbeek.homepages]
 
 [pagano]
 name = "Miguel Pagano"
 
 [pagano.emails]
 
 [pagano.emails.pagano_email]
 user = [
   "miguel",
   "pagano",
 ]
 host = [
   "unc",
   "edu",
   "ar",
 ]
 
 [pagano.homepages]
 pagano_homepage = "https://cs.famaf.unc.edu.ar/~mpagano/"
 
 [pal]
 name = "Abhik Pal"
 
 [pal.emails]
 
 [pal.homepages]
 
 [paleo]
 name = "Bruno Woltzenlogel Paleo"
 
 [paleo.emails]
 
 [paleo.homepages]
 paleo_homepage = "http://www.logic.at/staff/bruno/"
 
 [palmer]
 name = "Jake Palmer"
 
 [palmer.emails]
 
 [palmer.emails.palmer_email]
 user = [
   "jake",
   "palmer",
 ]
 host = [
   "ed",
   "ac",
   "uk",
 ]
 
 [palmer.homepages]
 
 [parkinson]
 name = "Matthew Parkinson"
 
 [parkinson.emails]
 
 [parkinson.homepages]
 parkinson_homepage = "http://research.microsoft.com/people/mattpark/"
 
 [parrow]
 name = "Joachim Parrow"
 
 [parrow.emails]
 
 [parrow.emails.parrow_email]
 user = [
   "joachim",
   "parrow",
 ]
 host = [
   "it",
   "uu",
   "se",
 ]
 
 [parrow.homepages]
 
 [parsert]
 name = "Julian Parsert"
 
 [parsert.emails]
 
 [parsert.emails.parsert_email]
 user = [
   "julian",
   "parsert",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [parsert.emails.parsert_email1]
 user = [
   "julian",
   "parsert",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [parsert.homepages]
 parsert_homepage = "http://www.parsert.com/"
 
 [paulson]
 name = "Lawrence C. Paulson"
 
 [paulson.emails]
 
 [paulson.emails.paulson_email]
 user = [
   "lp15",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [paulson.homepages]
 paulson_homepage = "https://www.cl.cam.ac.uk/~lp15/"
 
 [peltier]
 name = "Nicolas Peltier"
 
 [peltier.emails]
 
 [peltier.emails.peltier_email]
 user = [
   "Nicolas",
   "Peltier",
 ]
 host = [
   "imag",
   "fr",
 ]
 
 [peltier.homepages]
 peltier_homepage = "http://membres-lig.imag.fr/peltier/"
 
 [peters]
 name = "Kirstin Peters"
 
 [peters.emails]
 
 [peters.emails.peters_email]
 user = [
   "kirstin",
   "peters",
 ]
 host = [
   "tu-berlin",
   "de",
 ]
 
 [peters.homepages]
 
 [petrovic]
 name = "Danijela Petrovic"
 
 [petrovic.emails]
 
 [petrovic.homepages]
 petrovic_homepage = "http://www.matf.bg.ac.rs/~danijela"
 
 [pierzchalski]
 name = "Edward Pierzchalski"
 
 [pierzchalski.emails]
 
 [pierzchalski.homepages]
 
 [platzer]
 name = "André Platzer"
 
 [platzer.emails]
 
 [platzer.emails.platzer_email]
 user = [
   "aplatzer",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [platzer.homepages]
 platzer_homepage = "https://www.cs.cmu.edu/~aplatzer/"
 
 [pohjola]
 name = "Johannes Åman Pohjola"
 
 [pohjola.emails]
 
 [pohjola.homepages]
 
 [pollak]
 name = "Florian Pollak"
 
 [pollak.emails]
 
 [pollak.emails.pollak_email]
 user = [
   "florian",
   "pollak",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [pollak.homepages]
 
 [popescu]
 name = "Andrei Popescu"
 
 [popescu.emails]
 
 [popescu.emails.popescu_email]
 user = [
   "a",
   "popescu",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [popescu.emails.popescu_email1]
 user = [
   "uuomul",
 ]
 host = [
   "yahoo",
   "com",
 ]
 
 [popescu.emails.popescu_email2]
 user = [
   "a",
   "popescu",
 ]
 host = [
   "mdx",
   "ac",
   "uk",
 ]
 
 [popescu.homepages]
 popescu_homepage = "https://www.andreipopescu.uk"
 
 [porter]
 name = "Benjamin Porter"
 
 [porter.emails]
 
 [porter.homepages]
 
 [prathamesh]
 name = "T.V.H. Prathamesh"
 
 [prathamesh.emails]
 
 [prathamesh.emails.prathamesh_email]
 user = [
   "prathamesh",
 ]
 host = [
   "imsc",
   "res",
   "in",
 ]
 
 [prathamesh.homepages]
 
 [preoteasa]
 name = "Viorel Preoteasa"
 
 [preoteasa.emails]
 
 [preoteasa.emails.preoteasa_email]
 user = [
   "viorel",
   "preoteasa",
 ]
 host = [
   "aalto",
   "fi",
 ]
 
 [preoteasa.homepages]
 preoteasa_homepage = "http://users.abo.fi/vpreotea/"
 
 [pusch]
 name = "Cornelia Pusch"
 
 [pusch.emails]
 
 [pusch.homepages]
 
 [rabe]
 name = "Markus N. Rabe"
 
 [rabe.emails]
 
 [rabe.homepages]
 rabe_homepage = "http://www.react.uni-saarland.de/people/rabe.html"
 
 [raedle]
 name = "Jonas Rädle"
 
 [raedle.emails]
 
 [raedle.emails.raedle_email]
 user = [
   "jonas",
   "raedle",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [raedle.emails.raedle_email1]
 user = [
   "jonas",
   "raedle",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [raedle.homepages]
 
 [raska]
 name = "Martin Raška"
 
 [raska.emails]
 
 [raska.homepages]
 
 [raszyk]
 name = "Martin Raszyk"
 
 [raszyk.emails]
 
 [raszyk.emails.raszyk_email]
 user = [
   "martin",
   "raszyk",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [raszyk.emails.raszyk_email1]
 user = [
   "m",
   "raszyk",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [raszyk.homepages]
 
 [rau]
 name = "Martin Rau"
 
 [rau.emails]
 
 [rau.emails.rau_email]
 user = [
   "martin",
   "rau",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [rau.emails.rau_email1]
 user = [
   "mrtnrau",
 ]
 host = [
   "googlemail",
   "com",
 ]
 
 [rau.homepages]
 
 [rauch]
 name = "Nicole Rauch"
 
 [rauch.emails]
 
 [rauch.emails.rauch_email]
 user = [
   "rauch",
 ]
 host = [
   "informatik",
   "uni-kl",
   "de",
 ]
 
 [rauch.homepages]
 
 [raumer]
 name = "Jakob von Raumer"
 
 [raumer.emails]
 
 [raumer.emails.raumer_email]
 user = [
   "psxjv4",
 ]
 host = [
   "nottingham",
   "ac",
   "uk",
 ]
 
 [raumer.homepages]
 
 [ravindran]
 name = "Binoy Ravindran"
 
 [ravindran.emails]
 
 [ravindran.homepages]
 
 [rawson]
 name = "Michael Rawson"
 
 [rawson.emails]
 
 [rawson.emails.rawson_email]
 user = [
   "michaelrawson76",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [rawson.emails.rawson_email1]
 user = [
   "mr644",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [rawson.homepages]
 
 [raya]
 name = "Rodrigo Raya"
 
 [raya.emails]
 
 [raya.homepages]
 raya_homepage = "https://people.epfl.ch/rodrigo.raya"
 
 [regensburger]
 name = "Franz Regensburger"
 
 [regensburger.emails]
 
 [regensburger.emails.regensburger_email]
 user = [
   "Franz",
   "Regensburger",
 ]
 host = [
   "thi",
   "de",
 ]
 
 [regensburger.homepages]
 regensburger_homepage = "https://www.thi.de/suche/mitarbeiter/prof-dr-rer-nat-franz-regensburger"
 
 [reiche]
 name = "Sebastian Reiche"
 
 [reiche.emails]
 
 [reiche.homepages]
 reiche_homepage = "https://www.linkedin.com/in/sebastian-reiche-0b2093178"
 
 [reiter]
 name = "Markus Reiter"
 
 [reiter.emails]
 
 [reiter.homepages]
 
 [reynaud]
 name = "Alban Reynaud"
 
 [reynaud.emails]
 
 [reynaud.homepages]
 
 [ribeiro]
 name = "Pedro Ribeiro"
 
 [ribeiro.emails]
 
 [ribeiro.homepages]
 
 [richter]
 name = "Stefan Richter"
 
 [richter.emails]
 
 [richter.emails.richter_email]
 user = [
   "richter",
 ]
 host = [
   "informatik",
   "rwth-aachen",
   "de",
 ]
 
 [richter.homepages]
 richter_homepage = "http://www-lti.informatik.rwth-aachen.de/~richter/"
 
 [rickmann]
 name = "Christina Rickmann"
 
 [rickmann.emails]
 
 [rickmann.emails.rickmann_email]
 user = [
   "c",
   "rickmann",
 ]
 host = [
   "tu-berlin",
   "de",
 ]
 
 [rickmann.homepages]
 
 [ridge]
 name = "Tom Ridge"
 
 [ridge.emails]
 
 [ridge.homepages]
 
 [rizaldi]
 name = "Albert Rizaldi"
 
 [rizaldi.emails]
 
 [rizaldi.emails.rizaldi_email]
 user = [
   "albert",
   "rizaldi",
 ]
 host = [
   "ntu",
   "edu",
   "sg",
 ]
 
 [rizaldi.homepages]
 
 [rizkallah]
 name = "Christine Rizkallah"
 
 [rizkallah.emails]
 
 [rizkallah.homepages]
 rizkallah_homepage = "https://www.mpi-inf.mpg.de/~crizkall/"
 
 [robillard]
 name = "Simon Robillard"
 
 [robillard.emails]
 
 [robillard.homepages]
 robillard_homepage = "https://simon-robillard.net/"
 
 [roessle]
 name = "Ian Roessle"
 
 [roessle.emails]
 
 [roessle.homepages]
 
 [romanos]
 name = "Ralph Romanos"
 
 [romanos.emails]
 
 [romanos.emails.romanos_email]
 user = [
   "ralph",
   "romanos",
 ]
 host = [
   "student",
   "ecp",
   "fr",
 ]
 
 [romanos.homepages]
 
 [rosskopf]
 name = "Simon Roßkopf"
 
 [rosskopf.emails]
 
 [rosskopf.emails.rosskopf_email]
 user = [
   "rosskops",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [rosskopf.homepages]
 rosskopf_homepage = "http://www21.in.tum.de/~rosskops"
 
 [rowat]
 name = "Colin Rowat"
 
 [rowat.emails]
 
 [rowat.emails.rowat_email]
 user = [
   "c",
   "rowat",
 ]
 host = [
   "bham",
   "ac",
   "uk",
 ]
 
 [rowat.homepages]
 
 [sabouret]
 name = "Nicolas Sabouret"
 
 [sabouret.emails]
 
 [sabouret.homepages]
 
 [sachtleben]
 name = "Robert Sachtleben"
 
 [sachtleben.emails]
 
 [sachtleben.emails.sachtleben_email]
 user = [
   "rob_sac",
 ]
 host = [
   "uni-bremen",
   "de",
 ]
 
 [sachtleben.homepages]
 
 [saile]
 name = "Christian Saile"
 
 [saile.emails]
 
 [saile.homepages]
 saile_homepage = "http://dss.in.tum.de/staff/christian-saile.html"
 
 [sanan]
 name = "David Sanan"
 
 [sanan.emails]
 
 [sanan.emails.sanan_email]
 user = [
   "sanan",
 ]
 host = [
   "ntu",
   "edu",
   "sg",
 ]
 
 [sanan.homepages]
 
 [sato]
 name = "Tetsuya Sato"
 
 [sato.emails]
 
 [sato.emails.sato_email]
 user = [
   "tsato",
 ]
 host = [
   "c",
   "titech",
   "ac",
   "jp",
 ]
 
 [sato.homepages]
 sato_homepage = "https://sites.google.com/view/tetsuyasato/"
 
 [sauer]
 name = "Jens Sauer"
 
 [sauer.emails]
 
 [sauer.emails.sauer_email]
 user = [
   "sauer",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [sauer.homepages]
 
 [schaeffeler]
 name = "Maximilian Schäffeler"
 
 [schaeffeler.emails]
 
 [schaeffeler.emails.schaeffeler_email]
 user = [
   "schaeffm",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [schaeffeler.homepages]
 
 [scharager]
 name = "Matias Scharager"
 
 [scharager.emails]
 
 [scharager.emails.scharager_email]
 user = [
   "mscharag",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [scharager.homepages]
 
 [schimpf]
 name = "Alexander Schimpf"
 
 [schimpf.emails]
 
 [schimpf.emails.schimpf_email]
 user = [
   "schimpfa",
 ]
 host = [
   "informatik",
   "uni-freiburg",
   "de",
 ]
 
 [schimpf.homepages]
 
 [schirmer]
 name = "Norbert Schirmer"
 
 [schirmer.emails]
 
 [schirmer.emails.schirmer_email]
 user = [
   "norbert",
   "schirmer",
 ]
 host = [
   "web",
   "de",
 ]
 
 [schirmer.homepages]
 
 [schleicher]
 name = "Dierk Schleicher"
 
 [schleicher.emails]
 
 [schleicher.homepages]
 
 [schlichtkrull]
 name = "Anders Schlichtkrull"
 
 [schlichtkrull.emails]
 
 [schlichtkrull.emails.schlichtkrull_email]
 user = [
   "andschl",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [schlichtkrull.homepages]
 schlichtkrull_homepage = "https://people.compute.dtu.dk/andschl/"
 
 [schmaltz]
 name = "Julien Schmaltz"
 
 [schmaltz.emails]
 
 [schmaltz.emails.schmaltz_email]
 user = [
   "Julien",
   "Schmaltz",
 ]
 host = [
   "ou",
   "nl",
 ]
 
 [schmaltz.homepages]
 
 [schmidinger]
 name = "Lukas Schmidinger"
 
 [schmidinger.emails]
 
 [schmidinger.homepages]
 
 [schmoetten]
 name = "Richard Schmoetten"
 
 [schmoetten.emails]
 
 [schmoetten.emails.schmoetten_email]
 user = [
   "s1311325",
 ]
 host = [
   "sms",
   "ed",
   "ac",
   "uk",
 ]
 
 [schmoetten.homepages]
 
 [schneider]
 name = "Joshua Schneider"
 
 [schneider.emails]
 
 [schneider.emails.schneider_email]
 user = [
   "joshua",
   "schneider",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [schneider.homepages]
 
 [schoepe]
 name = "Daniel Schoepe"
 
 [schoepe.emails]
 
 [schoepe.emails.schoepe_email]
 user = [
   "daniel",
 ]
 host = [
   "schoepe",
   "org",
 ]
 
 [schoepe.homepages]
 
 [schoepf]
 name = "Jonas Schöpf"
 
 [schoepf.emails]
 
 [schoepf.emails.schoepf_email]
 user = [
   "jonas",
   "schoepf",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [schoepf.homepages]
 
 [scott]
 name = "Dana Scott"
 
 [scott.emails]
 
 [scott.homepages]
 scott_homepage = "http://www.cs.cmu.edu/~scott/"
 
 [sefidgar]
 name = "S. Reza Sefidgar"
 
 [sefidgar.emails]
 
 [sefidgar.emails.sefidgar_email]
 user = [
   "reza",
   "sefidgar",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [sefidgar.homepages]
 
 [seidl]
 name = "Benedikt Seidl"
 
 [seidl.emails]
 
 [seidl.emails.seidl_email]
 user = [
   "benedikt",
   "seidl",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [seidl.homepages]
 
 [seidler]
 name = "Henning Seidler"
 
 [seidler.emails]
 
 [seidler.emails.seidler_email]
 user = [
   "henning",
   "seidler",
 ]
 host = [
   "mailbox",
   "tu-berlin",
   "de",
 ]
 
 [seidler.homepages]
 
 [sewell]
 name = "Thomas Sewell"
 
 [sewell.emails]
 
 [sewell.homepages]
 
 [sickert]
 name = "Salomon Sickert"
 
 [sickert.emails]
 
 [sickert.emails.sickert_email]
 user = [
   "s",
   "sickert",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [sickert.homepages]
 sickert_homepage = "https://www7.in.tum.de/~sickert"
 
 [siek]
 name = "Jeremy Siek"
 
 [siek.emails]
 
 [siek.emails.siek_email]
 user = [
   "jsiek",
 ]
 host = [
   "indiana",
   "edu",
 ]
 
 [siek.homepages]
 siek_homepage = "http://homes.soic.indiana.edu/jsiek/"
 
 [simic]
 name = "Danijela Simić"
 
 [simic.emails]
 
 [simic.emails.simic_email]
 user = [
   "danijela",
 ]
 host = [
   "matf",
   "bg",
   "ac",
   "rs",
 ]
 
 [simic.homepages]
 simic_homepage = "http://poincare.matf.bg.ac.rs/~danijela"
 
 [sison]
 name = "Robert Sison"
 
 [sison.emails]
 
 [sison.homepages]
 
 [smaus]
 name = "Jan-Georg Smaus"
 
 [smaus.emails]
 
 [smaus.homepages]
 smaus_homepage = "http://www.irit.fr/~Jan-Georg.Smaus"
 
 [smola]
 name = "Filip Smola"
 
 [smola.emails]
 
 [smola.emails.smola_email]
 user = [
   "f",
   "smola",
 ]
 host = [
   "sms",
   "ed",
   "ac",
   "uk",
 ]
 
 [smola.homepages]
 
 [snelting]
 name = "Gregor Snelting"
 
 [snelting.emails]
 
 [snelting.homepages]
 snelting_homepage = "http://pp.info.uni-karlsruhe.de/personhp/gregor_snelting.php"
 
 [somaini]
 name = "Ivano Somaini"
 
 [somaini.emails]
 
 [somaini.homepages]
 
 [somogyi]
 name = "Dániel Somogyi"
 
 [somogyi.emails]
 
 [somogyi.homepages]
 
 [spasic]
 name = "Mirko Spasić"
 
 [spasic.emails]
 
 [spasic.emails.spasic_email]
 user = [
   "mirko",
 ]
 host = [
   "matf",
   "bg",
   "ac",
   "rs",
 ]
 
 [spasic.homepages]
 
 [spichkova]
 name = "Maria Spichkova"
 
 [spichkova.emails]
 
 [spichkova.emails.spichkova_email]
 user = [
   "maria",
   "spichkova",
 ]
 host = [
   "rmit",
   "edu",
   "au",
 ]
 
 [spichkova.homepages]
 
 [sprenger]
 name = "Christoph Sprenger"
 
 [sprenger.emails]
 
 [sprenger.emails.sprenger_email]
 user = [
   "sprenger",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [sprenger.homepages]
 
 [stannett]
 name = "Mike Stannett"
 
 [stannett.emails]
 
 [stannett.emails.stannett_email]
 user = [
   "m",
   "stannett",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [stannett.homepages]
 
 [stark]
 name = "Eugene W. Stark"
 
 [stark.emails]
 
 [stark.emails.stark_email]
 user = [
   "stark",
 ]
 host = [
   "cs",
   "stonybrook",
   "edu",
 ]
 
 [stark.homepages]
 
 [starosta]
 name = "Štěpán Starosta"
 
 [starosta.emails]
 
 [starosta.emails.starosta_email]
 user = [
   "stepan",
   "starosta",
 ]
 host = [
   "fit",
   "cvut",
   "cz",
 ]
 
 [starosta.homepages]
 starosta_homepage = "https://users.fit.cvut.cz/~staroste/"
 
 [steinberg]
 name = "Matías Steinberg"
 
 [steinberg.emails]
 
 [steinberg.emails.steinberg_email]
 user = [
   "matias",
   "steinberg",
 ]
 host = [
   "mi",
   "unc",
   "edu",
   "ar",
 ]
 
 [steinberg.homepages]
 
 [stephan]
 name = "Werner Stephan"
 
 [stephan.emails]
 
 [stephan.emails.stephan_email]
 user = [
   "stephan",
 ]
 host = [
   "dfki",
   "de",
 ]
 
 [stephan.homepages]
 
 [sternagel]
 name = "Christian Sternagel"
 
 [sternagel.emails]
 
 [sternagel.emails.sternagel_email]
 user = [
   "c",
   "sternagel",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [sternagel.emails.sternagel_email1]
 user = [
   "christian",
   "sternagel",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [sternagel.homepages]
 sternagel_homepage = "http://cl-informatik.uibk.ac.at/users/griff/"
 
 [sternagelt]
 name = "Thomas Sternagel"
 
 [sternagelt.emails]
 
 [sternagelt.homepages]
 
 [stevens]
 name = "Lukas Stevens"
 
 [stevens.emails]
 
 [stevens.emails.stevens_email]
 user = [
   "lukas",
   "stevens",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [stevens.homepages]
 stevens_homepage = "https://www21.in.tum.de/team/stevensl"
 
 [stock]
 name = "Benedikt Stock"
 
 [stock.emails]
 
 [stock.emails.stock_email]
 user = [
   "benedikt1999",
 ]
 host = [
   "freenet",
   "de",
 ]
 
 [stock.homepages]
 
 [stoeckl]
 name = "Bernhard Stöckl"
 
 [stoeckl.emails]
 
 [stoeckl.emails.stoeckl_email]
 user = [
   "stoeckl",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [stoeckl.homepages]
 
 [stricker]
 name = "Christian Stricker"
 
 [stricker.emails]
 
 [stricker.homepages]
 stricker_homepage = "http://dss.in.tum.de/staff/christian-stricker.html"
 
 [strnisa]
 name = "Rok Strniša"
 
 [strnisa.emails]
 
 [strnisa.emails.strnisa_email]
 user = [
   "rok",
 ]
 host = [
   "strnisa",
   "com",
 ]
 
 [strnisa.homepages]
 strnisa_homepage = "http://rok.strnisa.com/lj/"
 
 [struth]
 name = "Georg Struth"
 
 [struth.emails]
 
 [struth.emails.struth_email]
 user = [
   "g",
   "struth",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [struth.homepages]
 struth_homepage = "http://staffwww.dcs.shef.ac.uk/people/G.Struth/"
 
 [stueber]
 name = "Anke Stüber"
 
 [stueber.emails]
 
 [stueber.emails.stueber_email]
 user = [
   "anke",
   "stueber",
 ]
 host = [
   "campus",
   "tu-berlin",
   "de",
 ]
 
 [stueber.homepages]
 
 [stuewe]
 name = "Daniel Stüwe"
 
 [stuewe.emails]
 
 [stuewe.homepages]
 
 [sudbrock]
 name = "Henning Sudbrock"
 
 [sudbrock.emails]
 
 [sudbrock.emails.sudbrock_email]
 user = [
   "sudbrock",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [sudbrock.homepages]
 
 [sudhof]
 name = "Henry Sudhof"
 
 [sudhof.emails]
 
 [sudhof.emails.sudhof_email]
 user = [
   "hsudhof",
 ]
 host = [
   "cs",
   "tu-berlin",
   "de",
 ]
 
 [sudhof.homepages]
 
 [sulejmani]
 name = "Ujkan Sulejmani"
 
 [sulejmani.emails]
 
 [sulejmani.emails.sulejmani_email]
 user = [
   "ujkan",
   "sulejmani",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [sulejmani.emails.sulejmani_email1]
 user = [
   "ujkan99",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [sulejmani.homepages]
 
 [sylvestre]
 name = "Jeremy Sylvestre"
 
 [sylvestre.emails]
 
 [sylvestre.emails.sylvestre_email]
 user = [
   "jeremy",
   "sylvestre",
 ]
 host = [
   "ualberta",
   "ca",
 ]
 
 [sylvestre.emails.sylvestre_email1]
 user = [
   "jsylvest",
 ]
 host = [
   "ualberta",
   "ca",
 ]
 
 [sylvestre.homepages]
 sylvestre_homepage = "http://ualberta.ca/~jsylvest/"
 
 [taha]
 name = "Safouan Taha"
 
 [taha.emails]
 
 [taha.emails.taha_email]
 user = [
   "safouan",
   "taha",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [taha.homepages]
 
 [tan]
 name = "Yong Kiam Tan"
 
 [tan.emails]
 
 [tan.emails.tan_email]
 user = [
   "yongkiat",
 ]
 host = [
   "cs",
   "cmu",
   "edu",
 ]
 
 [tan.homepages]
 tan_homepage = "https://www.cs.cmu.edu/~yongkiat/"
 
 [tasch]
 name = "Markus Tasch"
 
 [tasch.emails]
 
 [tasch.emails.tasch_email]
 user = [
   "tasch",
 ]
 host = [
   "mais",
   "informatik",
   "tu-darmstadt",
   "de",
 ]
 
 [tasch.homepages]
 
 [taylor]
 name = "Ramsay G. Taylor"
 
 [taylor.emails]
 
 [taylor.emails.taylor_email]
 user = [
   "r",
   "g",
   "taylor",
 ]
 host = [
   "sheffield",
   "ac",
   "uk",
 ]
 
 [taylor.homepages]
 
 [terraf]
 name = "Pedro Sánchez Terraf"
 
 [terraf.emails]
 
 [terraf.emails.terraf_email]
 user = [
   "psterraf",
 ]
 host = [
   "unc",
   "edu",
   "ar",
 ]
 
 [terraf.homepages]
 terraf_homepage = "https://cs.famaf.unc.edu.ar/~pedro/home_en.html"
 
 [thiemann]
 name = "René Thiemann"
 
 [thiemann.emails]
 
 [thiemann.emails.thiemann_email]
 user = [
   "rene",
   "thiemann",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [thiemann.homepages]
 thiemann_homepage = "http://cl-informatik.uibk.ac.at/users/thiemann/"
 
 [thommes]
 name = "Joseph Thommes"
 
 [thommes.emails]
 
 [thommes.emails.thommes_email]
 user = [
   "joseph-thommes",
 ]
 host = [
   "gmx",
   "de",
 ]
 
 [thommes.homepages]
 
 [thomson]
 name = "Fox Thomson"
 
 [thomson.emails]
 
 [thomson.emails.thomson_email]
 user = [
   "foxthomson0",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [thomson.homepages]
 
 [tiu]
 name = "Alwen Tiu"
 
 [tiu.emails]
 
 [tiu.emails.tiu_email]
 user = [
   "ATiu",
 ]
 host = [
   "ntu",
   "edu",
   "sg",
 ]
 
 [tiu.homepages]
 tiu_homepage = "http://users.cecs.anu.edu.au/~tiu/"
 
 [toth]
 name = "Balazs Toth"
 
 [toth.emails]
 
 [toth.emails.toth_email]
 user = [
   "balazs",
   "toth",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [toth.homepages]
 
 [tourret]
 name = "Sophie Tourret"
 
 [tourret.emails]
 
 [tourret.emails.tourret_email]
 user = [
   "stourret",
 ]
 host = [
   "mpi-inf",
   "mpg",
   "de",
 ]
 
 [tourret.homepages]
 tourret_homepage = "https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/sophie-tourret/"
 
 [trachtenherz]
 name = "David Trachtenherz"
 
 [trachtenherz.emails]
 
 [trachtenherz.homepages]
 
 [traut]
 name = "Christoph Traut"
 
 [traut.emails]
 
 [traut.homepages]
 
 [traytel]
 name = "Dmitriy Traytel"
 
 [traytel.emails]
 
 [traytel.emails.traytel_email]
 user = [
   "traytel",
 ]
 host = [
   "in",
   "tum",
   "de",
 ]
 
 [traytel.emails.traytel_email1]
 user = [
   "traytel",
 ]
 host = [
   "inf",
   "ethz",
   "ch",
 ]
 
 [traytel.emails.traytel_email2]
 user = [
   "traytel",
 ]
 host = [
   "di",
   "ku",
   "dk",
 ]
 
 [traytel.homepages]
 traytel_homepage = "https://traytel.bitbucket.io/"
 
 [trelat]
 name = "Vincent Trélat"
 
 [trelat.emails]
 
 [trelat.emails.trelat_email]
 user = [
   "vincent",
   "trelat",
 ]
 host = [
   "depinfonancy",
   "net",
 ]
 
 [trelat.homepages]
 
 [tuerk]
 name = "Thomas Tuerk"
 
 [tuerk.emails]
 
 [tuerk.homepages]
 
 [tuong]
 name = "Frédéric Tuong"
 
 [tuong.emails]
 
 [tuong.emails.tuong_email]
 user = [
   "tuong",
 ]
 host = [
   "users",
   "gforge",
   "inria",
   "fr",
 ]
 
 [tuong.emails.tuong_email1]
 user = [
   "ftuong",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [tuong.homepages]
 tuong_homepage = "https://www.lri.fr/~ftuong/"
 
 [tuongj]
 name = "Joseph Tuong"
 
 [tuongj.emails]
 
 [tuongj.homepages]
 
 [tverdyshev]
 name = "Sergey Tverdyshev"
 
 [tverdyshev.emails]
 
 [tverdyshev.emails.tverdyshev_email]
 user = [
   "stv",
 ]
 host = [
   "sysgo",
   "com",
 ]
 
 [tverdyshev.homepages]
 
 [ullrich]
 name = "Sebastian Ullrich"
 
 [ullrich.emails]
 
 [ullrich.emails.ullrich_email]
 user = [
   "sebasti",
 ]
 host = [
   "nullri",
   "ch",
 ]
 
 [ullrich.homepages]
 
 [unruh]
 name = "Dominique Unruh"
 
 [unruh.emails]
 
 [unruh.emails.unruh_email]
 user = [
   "unruh",
 ]
 host = [
   "ut",
   "ee",
 ]
 
 [unruh.homepages]
 unruh_homepage = "https://www.ut.ee/~unruh/"
 
 [urban]
 name = "Christian Urban"
 
 [urban.emails]
 
 [urban.emails.urban_email]
 user = [
   "christian",
   "urban",
 ]
 host = [
   "kcl",
   "ac",
   "uk",
 ]
 
 [urban.homepages]
 urban_homepage = "https://nms.kcl.ac.uk/christian.urban/"
 
 [van]
 name = "Hai Nguyen Van"
 
 [van.emails]
 
 [van.emails.van_email]
 user = [
   "hai",
   "nguyenvan",
   "phie",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [van.homepages]
 
 [velykis]
 name = "Andrius Velykis"
 
 [velykis.emails]
 
 [velykis.homepages]
 velykis_homepage = "http://andrius.velykis.lt"
 
 [verbeek]
 name = "Freek Verbeek"
 
 [verbeek.emails]
 
 [verbeek.emails.verbeek_email]
 user = [
   "Freek",
   "Verbeek",
 ]
 host = [
   "ou",
   "nl",
 ]
 
 [verbeek.emails.verbeek_email1]
 user = [
   "freek",
 ]
 host = [
   "vt",
   "edu",
 ]
 
 [verbeek.homepages]
 
 [villadsen]
 name = "Jørgen Villadsen"
 
 [villadsen.emails]
 
 [villadsen.emails.villadsen_email]
 user = [
   "jovi",
 ]
 host = [
   "dtu",
   "dk",
 ]
 
 [villadsen.homepages]
 villadsen_homepage = "https://people.compute.dtu.dk/jovi/"
 
 [voisin]
 name = "Frederic Voisin"
 
 [voisin.emails]
 
 [voisin.homepages]
 
 [vytiniotis]
 name = "Dimitrios Vytiniotis"
 
 [vytiniotis.emails]
 
 [vytiniotis.homepages]
 vytiniotis_homepage = "http://research.microsoft.com/en-us/people/dimitris/"
 
 [wagner]
 name = "Max Wagner"
 
 [wagner.emails]
 
 [wagner.emails.wagner_email]
 user = [
   "max",
 ]
 host = [
   "trollbu",
   "de",
 ]
 
 [wagner.homepages]
 
 [waldmann]
 name = "Uwe Waldmann"
 
 [waldmann.emails]
 
 [waldmann.emails.waldmann_email]
 user = [
   "waldmann",
 ]
 host = [
   "mpi-inf",
   "mpg",
   "de",
 ]
 
 [waldmann.homepages]
 
 [wand]
 name = "Daniel Wand"
 
 [wand.emails]
 
 [wand.emails.wand_email]
 user = [
   "dwand",
 ]
 host = [
   "mpi-inf",
   "mpg",
   "de",
 ]
 
 [wand.homepages]
 
 [wang]
 name = "Shuling Wang"
 
 [wang.emails]
 
 [wang.homepages]
 
 [wassell]
 name = "Mark Wassell"
 
 [wassell.emails]
 
 [wassell.emails.wassell_email]
 user = [
   "mpwassell",
 ]
 host = [
   "gmail",
   "com",
 ]
 
 [wassell.homepages]
 
 [wasserrab]
 name = "Daniel Wasserrab"
 
 [wasserrab.emails]
 
 [wasserrab.homepages]
 wasserrab_homepage = "http://pp.info.uni-karlsruhe.de/personhp/daniel_wasserrab.php"
 
 [watt]
 name = "Conrad Watt"
 
 [watt.emails]
 
 [watt.emails.watt_email]
 user = [
   "caw77",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [watt.homepages]
 watt_homepage = "http://www.cl.cam.ac.uk/~caw77/"
 
 [weber]
 name = "Tjark Weber"
 
 [weber.emails]
 
 [weber.emails.weber_email]
 user = [
   "tjark",
   "weber",
 ]
 host = [
   "it",
   "uu",
   "se",
 ]
 
 [weber.homepages]
 weber_homepage = "http://user.it.uu.se/~tjawe125/"
 
 [weerwag]
 name = "Timmy Weerwag"
 
 [weerwag.emails]
 
 [weerwag.homepages]
 
 [weidner]
 name = "Arno Wilhelm-Weidner"
 
 [weidner.emails]
 
 [weidner.emails.weidner_email]
 user = [
   "arno",
   "wilhelm-weidner",
 ]
 host = [
   "tu-berlin",
   "de",
 ]
 
 [weidner.homepages]
 
 [wenzel]
 name = "Makarius Wenzel"
 
 [wenzel.emails]
 
 [wenzel.emails.wenzel_email]
 user = [
   "makarius",
 ]
 host = [
   "sketis",
   "net",
 ]
 
 [wenzel.homepages]
 wenzel_homepage = "https://sketis.net"
 
 [wickerson]
 name = "John Wickerson"
 
 [wickerson.emails]
 
 [wickerson.homepages]
 wickerson_homepage = "http://www.doc.ic.ac.uk/~jpw48"
 
 [willenbrink]
 name = "Sebastian Willenbrink"
 
 [willenbrink.emails]
 
 [willenbrink.emails.willenbrink_email]
 user = [
   "sebastian",
   "willenbrink",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [willenbrink.homepages]
 
 [wimmer]
 name = "Simon Wimmer"
 
 [wimmer.emails]
 
 [wimmer.emails.wimmer_email]
 user = [
   "simon",
   "wimmer",
 ]
 host = [
   "tum",
   "de",
 ]
 
 [wimmer.homepages]
 wimmer_homepage = "http://home.in.tum.de/~wimmers/"
 
 [wirt]
 name = "Kai Wirt"
 
 [wirt.emails]
 
 [wirt.homepages]
 
 [wolff]
 name = "Burkhart Wolff"
 
 [wolff.emails]
 
 [wolff.emails.wolff_email]
 user = [
   "burkhart",
   "wolff",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [wolff.homepages]
 wolff_homepage = "https://www.lri.fr/~wolff/"
 
 [wu]
 name = "Chunhan Wu"
 
 [wu.emails]
 
 [wu.homepages]
 
 [xu]
 name = "Jian Xu"
 
 [xu.emails]
 
 [xu.homepages]
 
 [yamada]
 name = "Akihisa Yamada"
 
 [yamada.emails]
 
 [yamada.emails.yamada_email]
 user = [
   "akihisa",
   "yamada",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [yamada.emails.yamada_email1]
 user = [
   "ayamada",
 ]
 host = [
   "trs",
   "cm",
   "is",
   "nagoya-u",
   "ac",
   "jp",
 ]
 
 [yamada.emails.yamada_email2]
 user = [
   "akihisa",
   "yamada",
 ]
 host = [
   "aist",
   "go",
   "jp",
 ]
 
 [yamada.emails.yamada_email3]
 user = [
   "akihisayamada",
 ]
 host = [
   "nii",
   "ac",
   "jp",
 ]
 
 [yamada.homepages]
 yamada_homepage = "http://group-mmm.org/~ayamada/"
 
 [ye]
 name = "Lina Ye"
 
 [ye.emails]
 
 [ye.emails.ye_email]
 user = [
   "lina",
   "ye",
 ]
 host = [
   "lri",
   "fr",
 ]
 
 [ye.homepages]
 
 [ying]
 name = "Shenggang Ying"
 
 [ying.emails]
 
 [ying.homepages]
 
 [yingm]
 name = "Mingsheng Ying"
 
 [yingm.emails]
 
 [yingm.homepages]
 
 [yu]
 name = "Lei Yu"
 
 [yu.emails]
 
 [yu.emails.yu_email]
 user = [
   "ly271",
 ]
 host = [
   "cam",
   "ac",
   "uk",
 ]
 
 [yu.homepages]
 
 [zankl]
 name = "Harald Zankl"
 
 [zankl.emails]
 
 [zankl.emails.zankl_email]
 user = [
   "Harald",
   "Zankl",
 ]
 host = [
   "uibk",
   "ac",
   "at",
 ]
 
 [zankl.homepages]
 zankl_homepage = "http://cl-informatik.uibk.ac.at/users/hzankl"
 
 [zee]
 name = "Karen Zee"
 
 [zee.emails]
 
 [zee.emails.zee_email]
 user = [
   "kkz",
 ]
 host = [
   "mit",
   "edu",
 ]
 
 [zee.homepages]
 zee_homepage = "http://www.mit.edu/~kkz/"
 
 [zeller]
 name = "Peter Zeller"
 
 [zeller.emails]
 
 [zeller.emails.zeller_email]
 user = [
   "p_zeller",
 ]
 host = [
   "cs",
   "uni-kl",
   "de",
 ]
 
 [zeller.homepages]
 
 [zeyda]
 name = "Frank Zeyda"
 
 [zeyda.emails]
 
 [zeyda.emails.zeyda_email]
 user = [
   "frank",
   "zeyda",
 ]
 host = [
   "york",
   "ac",
   "uk",
 ]
 
 [zeyda.homepages]
 
 [zhan]
 name = "Bohua Zhan"
 
 [zhan.emails]
 
 [zhan.emails.zhan_email]
 user = [
   "bzhan",
 ]
 host = [
   "ios",
   "ac",
   "cn",
 ]
 
 [zhan.homepages]
 zhan_homepage = "http://lcs.ios.ac.cn/~bzhan/"
 
 [zhang]
 name = "Yu Zhang"
 
 [zhang.emails]
 
 [zhang.homepages]
 
 [zhangx]
 name = "Xingyuan Zhang"
 
 [zhangx.emails]
 
 [zhangx.homepages]
 
 [zhann]
 name = "Naijun Zhan"
 
 [zhann.emails]
 
 [zhann.homepages]
diff --git a/metadata/entries/Combinatorial_Enumeration_Algorithms.toml b/metadata/entries/Combinatorial_Enumeration_Algorithms.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Combinatorial_Enumeration_Algorithms.toml
@@ -0,0 +1,30 @@
+title = "Combinatorial Enumeration Algorithms"
+date = 2022-11-11
+topics = [
+  "Mathematics/Combinatorics",
+  "Computer science/Algorithms",
+]
+abstract = "Combinatorial objects have configurations which can be enumerated by algorithms, but especially for imperative programs, it is difficult to find out if they produce the correct output and don’t generate duplicates. Therefore, for some of the most common combinatorial objects, namely n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions, Derangements and Trees, this entry formalizes efficient functional programs and verifies their correctness. In addition, it provides cardinality proofs for those combinatorial objects. Some cardinalities are verified using the enumeration functions and others are shown using existing libraries including other AFP entries."
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.hofmeier]
+email = "hofmeier_email"
+
+[authors.karayel]
+email = "karayel_email"
+
+[contributors]
+
+[notify]
+hofmeier = "hofmeier_email"
+
+[history]
+
+[extra]
+
+[related]
+dois = []
+pubs = []
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Combinatorial_Enumeration_Algorithms.thy b/thys/Combinatorial_Enumeration_Algorithms/Combinatorial_Enumeration_Algorithms.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Combinatorial_Enumeration_Algorithms.thy
@@ -0,0 +1,16 @@
+theory Combinatorial_Enumeration_Algorithms
+  imports
+    n_Sequences
+    n_Permutations
+    n_Subsets
+    Powerset
+    Integer_Partitions 
+    Integer_Compositions
+    Weak_Integer_Compositions
+    Derangements_Enum
+    Trees
+begin             
+
+(*library files: Common_Lemmas.thy, Filter_Bool_List.thy*)
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Common_Lemmas.thy b/thys/Combinatorial_Enumeration_Algorithms/Common_Lemmas.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Common_Lemmas.thy
@@ -0,0 +1,240 @@
+section"Injectivity for two argument functions"
+
+theory Common_Lemmas
+  imports
+  "HOL.List"
+  "HOL-Library.Tree"
+begin
+
+text \<open>This section introduces @{term "inj2_on"} which generalizes @{term "inj_on"} on curried
+functions with two arguments and contains subsequent theorems about such functions.\<close>
+
+text"
+We could use curried function directly with for example \<open>case_prod\<close>,
+but this way the proofs become simpler and easier to read."
+definition inj2_on :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where
+  "inj2_on f A B \<longleftrightarrow> (\<forall>x1\<in>A. \<forall>x2\<in>A. \<forall>y1\<in>B. \<forall>y2\<in>B. f x1 y1 = f x2 y2 \<longrightarrow> x1 = x2 \<and> y1 = y2)"
+
+abbreviation inj2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
+  "inj2 f \<equiv> inj2_on f UNIV UNIV"
+
+subsection \<open>Correspondence between @{term "inj2_on"} and @{term "inj_on"}\<close>
+
+lemma inj2_curried: "inj2_on (curry f) A B \<longleftrightarrow> inj_on f (A\<times>B)"
+  unfolding inj2_on_def inj_on_def by auto
+
+lemma inj2_on_all: "inj2 f \<Longrightarrow> inj2_on f A B"
+  unfolding inj2_on_def by simp
+
+lemma inj2_inj_first: "inj2 f \<Longrightarrow> inj f"
+  unfolding inj2_on_def inj_on_def by simp
+
+lemma inj2_inj_second: "inj2 f \<Longrightarrow> inj (f x)"
+  unfolding inj2_on_def inj_on_def by simp
+
+lemma inj2_inj_second_flipped: "inj2 f \<Longrightarrow> inj (\<lambda>x. f x y)"
+  unfolding inj2_on_def inj_on_def by simp
+
+
+subsection"Proofs with inj2"
+
+text\<open>Already existing for @{term "inj"}:\<close>
+thm distinct_map
+
+lemma inj2_on_distinct_map:
+  assumes "inj2_on f {x} (set xs)"
+  shows "distinct xs = distinct (map (f x) xs)"
+  using assms distinct_map by (auto simp: inj2_on_def inj_onI)
+
+lemma inj2_distinct_map:
+  assumes "inj2 f"
+  shows "distinct xs = distinct (map (f x) xs)"
+  using assms inj2_on_distinct_map inj2_on_all by fast
+
+lemma inj2_on_distinct_concat_map:
+  assumes "inj2_on f (set xs) (set ys)"
+  shows "\<lbrakk>distinct ys; distinct xs\<rbrakk> \<Longrightarrow> distinct [f x y. x \<leftarrow> xs, y \<leftarrow> ys]"
+using assms proof(induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  then have nin: "x \<notin> set xs"
+    by simp
+
+  then have "inj2_on f {x} (set ys)"
+    using Cons unfolding inj2_on_def by simp
+  then have 1: "distinct (map (f x) ys)"
+    using Cons inj2_on_distinct_map by fastforce
+
+  have 2: "distinct (concat (map (\<lambda>x. map (f x) ys) xs))"
+    using Cons unfolding inj2_on_def by simp
+
+  have 3: "\<lbrakk>xa \<in> set xs; xb \<in> set ys; f x xb = f xa xc; xc \<in> set ys\<rbrakk> \<Longrightarrow> False " for xa xb xc
+    using Cons(4) unfolding inj2_on_def
+    using nin by force 
+
+  from 1 2 3 show ?case
+    by auto
+qed
+
+lemma inj2_distinct_concat_map:
+  assumes "inj2 f"
+  shows "\<lbrakk>distinct ys; distinct xs\<rbrakk> \<Longrightarrow> distinct [f x y. x \<leftarrow> xs, y \<leftarrow> ys]"
+  using assms inj2_on_all inj2_on_distinct_concat_map by blast
+
+lemma inj2_distinct_concat_map_function:
+  assumes "inj2 f"
+  shows"\<lbrakk>\<forall> x \<in> set xs. distinct (g x); distinct xs\<rbrakk> \<Longrightarrow> distinct [f x y. x \<leftarrow> xs, y \<leftarrow> g x]"
+proof(induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  have 1: "distinct (map (f x) (g x))"
+    using Cons assms inj2_distinct_map by fastforce
+    
+  have 2: "distinct (concat (map (\<lambda>x. map (f x) (g x)) xs))"
+    using Cons by simp
+    
+  have 3: "\<And>xa xb xc. \<lbrakk>xa \<in> set xs; xb \<in> set (g x); f x xb = f xa xc; xc \<in> set (g xa)\<rbrakk>
+      \<Longrightarrow> False"
+    using Cons assms unfolding inj2_on_def by auto 
+    
+   show ?case using 1 2 3 
+    by auto
+qed
+
+lemma distinct_concat_Nil: "distinct (concat (map (\<lambda>y. []) xs))"
+  by(induct xs) auto
+
+lemma inj2_distinct_concat_map_function_filter:
+  assumes "inj2 f"
+  shows"\<lbrakk>\<forall> x \<in> set xs. distinct (g x); distinct xs\<rbrakk> \<Longrightarrow> distinct [f x y. x \<leftarrow> xs, y \<leftarrow> g x, h x]"
+proof(induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  have 1: "distinct (map (f x) (g x))"
+    using Cons assms inj2_distinct_map by fastforce
+    
+  have 2: "distinct (concat (map (\<lambda>x. concat (map (\<lambda>y. if h x then [f x y] else []) (g x))) xs))"
+    using Cons by simp
+
+  have 3: "\<And>xa xb xc.
+       \<lbrakk>h x; xa \<in> set (g x); xb \<in> set xs; f x xa = f xb xc; xc \<in> set (g xb); xc \<in> (if h xb then UNIV else {})\<rbrakk> \<Longrightarrow> False"
+    by (metis Cons.prems(2) assms distinct.simps(2) inj2_on_def iso_tuple_UNIV_I)
+
+  then have 4: "distinct (concat (map (\<lambda>y. []) (g x)))"
+    using distinct_concat_Nil by auto
+
+  show ?case using 1 2 3 4 by auto
+qed
+
+subsection\<open>Specializations of @{term "inj2"}\<close>
+
+subsubsection"Cons"
+
+lemma Cons_inj2: "inj2 (#)"
+  unfolding inj2_on_def by simp
+
+lemma Cons_distinct_concat_map: "\<lbrakk>distinct ys; distinct xs\<rbrakk> \<Longrightarrow> distinct [x#y. x \<leftarrow> xs, y \<leftarrow> ys]"
+  using inj2_distinct_concat_map Cons_inj2 by auto
+
+lemma Cons_distinct_concat_map_function:
+  "\<lbrakk>\<forall> x \<in> set xs. distinct (g x) ; distinct xs\<rbrakk> \<Longrightarrow> distinct [x # y. x \<leftarrow> xs, y \<leftarrow> g x]"
+  using inj2_distinct_concat_map_function Cons_inj2 by auto
+
+lemma Cons_distinct_concat_map_function_distinct_on_all:
+  "\<lbrakk>\<forall> x. distinct (g x) ; distinct xs\<rbrakk> \<Longrightarrow> distinct [x # y. x \<leftarrow> xs, y \<leftarrow> g x]"
+  using Cons_distinct_concat_map_function by (metis (full_types)) 
+
+
+subsubsection"Node right"
+
+lemma Node_right_inj2: "inj2 (\<lambda>l r. Node l e r)"
+  unfolding inj2_on_def by simp
+
+lemma Node_right_distinct_concat_map:
+  "\<lbrakk>distinct ys; distinct xs\<rbrakk> \<Longrightarrow> distinct [Node x e y. x \<leftarrow> xs, y \<leftarrow> ys]"
+  using inj2_distinct_concat_map Node_right_inj2 by fast
+
+
+subsubsection"Node left"
+
+lemma Node_left_inj2: "inj2 (\<lambda>r l. Node l e r)"
+  unfolding inj2_on_def by simp
+
+lemma Node_left_distinct_map: "distinct xs = distinct (map (\<lambda>l. \<langle>l, (), r\<rangle>) xs)"
+  using inj2_distinct_map Node_left_inj2 by fast
+
+subsubsection"Cons Suc"
+
+lemma Cons_Suc_inj2: "inj2 (\<lambda>x ys. Suc x # ys)"
+  unfolding inj2_on_def by simp
+
+lemma Cons_Suc_distinct_concat_map_function:
+  "\<lbrakk>\<forall> x \<in> set xs. distinct (g x) ; distinct xs\<rbrakk> \<Longrightarrow> distinct [Suc x # y. x \<leftarrow> xs, y \<leftarrow> g x]"
+  using inj2_distinct_concat_map_function Cons_Suc_inj2 by auto 
+
+
+section"Lemmas for cardinality proofs "
+
+lemma length_concat_map: "length [f x r . x \<leftarrow> xs, r \<leftarrow> ys] = length ys * length xs"
+  by(induct xs arbitrary: ys) auto
+
+text"An useful extension to \<open>length_concat\<close>"
+thm length_concat
+lemma length_concat_map_function_sum_list:
+  assumes "\<And> x. x \<in> set xs \<Longrightarrow> length (g x) = h x"
+  shows "length [f x r . x \<leftarrow> xs, r \<leftarrow> g x] = sum_list (map h xs)"
+  using assms by(induct xs) auto
+
+lemma sum_list_extract_last: "(\<Sum>x\<leftarrow>[0..<Suc n]. f x) = (\<Sum>x\<leftarrow>[0..<n]. f x) + f n"
+  by(induct n) (auto simp: add.assoc)
+
+lemma leq_sum_to_sum_list: "(\<Sum>x \<le> n. f x) = (\<Sum>x\<leftarrow>[0..<Suc n]. f x)"
+  by (metis atMost_upto sum_set_upt_conv_sum_list_nat)
+
+lemma less_sum_to_sum_list: "(\<Sum>x < n. f x) = (\<Sum>x\<leftarrow>[0..< n]. f x)"
+  by (simp add: atLeast_upt sum_list_distinct_conv_sum_set)
+
+
+section"Miscellaneous"
+
+text\<open>Similar to @{thm [source] "length_remove1"}:\<close>
+lemma Suc_length_remove1: "x \<in> set xs \<Longrightarrow> Suc (length (remove1 x xs)) = length xs"
+  by(induct xs) auto
+
+subsection"\<open>count_list\<close> and replicate"
+text"HOL.List doesn't have many lemmas about \<open>count_list\<close> (when not using multisets)"
+
+lemma count_list_replicate: "count_list (replicate x y) y = x" 
+  by (induct x) auto
+       
+lemma count_list_full_elem: "count_list xs y = length xs \<longleftrightarrow> (\<forall>x \<in> set xs. x = y)" 
+proof(induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons z xs)
+  have "\<lbrakk>count_list xs y = Suc (length xs); x \<in> set xs\<rbrakk> \<Longrightarrow> x = y" for x
+    by (metis Suc_n_not_le_n count_le_length)
+  then show ?case
+    using Cons by auto
+qed
+
+text\<open>The following lemma verifies the reverse of @{thm [source] "count_notin"}:\<close>
+thm count_notin
+lemma count_list_zero_not_elem: "count_list xs x = 0 \<longleftrightarrow> x \<notin> set xs" 
+  by(induct xs) auto
+
+lemma count_list_length_replicate: "count_list xs y = length xs \<longleftrightarrow> xs = replicate (length xs) y"
+  by (metis count_list_full_elem count_list_replicate replicate_length_same)
+
+lemma count_list_True_False: "count_list xs True + count_list xs False = length xs"
+  by(induct xs) auto
+
+
+end
\ No newline at end of file
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Derangements_Enum.thy b/thys/Combinatorial_Enumeration_Algorithms/Derangements_Enum.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Derangements_Enum.thy
@@ -0,0 +1,178 @@
+section"Derangements"
+theory Derangements_Enum
+  imports
+    "HOL-Combinatorics.Multiset_Permutations"
+    "Common_Lemmas"
+   (* "Derangements.Derangements" *)
+begin
+
+subsection"Definition"
+
+fun no_overlap :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "no_overlap _ [] = True"
+| "no_overlap [] _ = True"
+| "no_overlap (x#xs) (y#ys) = (x \<noteq> y \<and> no_overlap xs ys)"
+
+lemma no_overlap_nth: "length xs = length ys \<Longrightarrow> i < length xs \<Longrightarrow> no_overlap xs ys \<Longrightarrow> xs ! i \<noteq> ys ! i" 
+  by(induct xs ys arbitrary: i rule: list_induct2) (auto simp: less_Suc_eq_0_disj)
+
+lemma nth_no_overlap: "length xs = length ys \<Longrightarrow> \<forall> i < length xs. xs ! i \<noteq> ys ! i \<Longrightarrow> no_overlap xs ys"
+proof (induct xs ys rule: list_induct2)
+  case (Cons x xs y ys)
+  then show ?case using Suc_less_eq nth_Cons_Suc by fastforce
+qed simp 
+  
+definition derangements :: "'a list \<Rightarrow> 'a list set" where
+  "derangements xs = {ys. distinct ys \<and> length xs = length ys \<and> set xs = set ys \<and> no_overlap xs ys }"
+text "A derangement of a list is a permutation where every element changes its position,
+  assuming all elements are distinguishable."
+text \<open>An alternative definition exists in \<open>Derangements.Derangements\<close> \cite{AFPderan}.\<close>
+text "Cardinality: \<open>count_derangements (length xs)\<close> (from \<open>Derangements.Derangements\<close>)"
+text "Example: \<open>derangements [0,1,2] = {[1,2,0], [2,0,1]}\<close>"
+
+subsection"Algorithm"
+fun derangement_enum_aux :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+  "derangement_enum_aux [] ys = [[]]"
+| "derangement_enum_aux (x#xs) ys = [y#r . y \<leftarrow> ys, r \<leftarrow> derangement_enum_aux xs (remove1 y ys), y \<noteq> x]"
+
+fun derangement_enum :: "'a list  \<Rightarrow> 'a list list" where
+ "derangement_enum xs = derangement_enum_aux xs xs"
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+lemma derangement_enum_aux_elem_length: "zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> length xs = length zs"
+  by(induct xs arbitrary: ys zs) auto
+
+lemma derangement_enum_aux_not_in: "y \<notin> set ys \<Longrightarrow> zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> y \<notin> set zs"
+proof(induct xs arbitrary: ys zs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  then obtain z zs2 where ob: "zs = z#zs2"
+    by auto
+  have "zs2 \<in> set (derangement_enum_aux xs (remove1 z ys)) \<Longrightarrow> y \<notin> set zs2"
+    using Cons notin_set_remove1 by fast
+  then show ?case using Cons ob
+    by auto
+qed
+
+lemma derangement_enum_aux_in: "y \<in> set zs \<Longrightarrow> zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> y \<in> set ys"
+  using derangement_enum_aux_not_in by fast
+  
+lemma derangement_enum_aux_distinct_elem: "distinct ys \<Longrightarrow> zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> distinct zs"
+proof(induct xs arbitrary: ys zs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  obtain z zs2 where ob: "zs = z#zs2"
+    using Cons by auto
+  then have ev: "zs2 \<in> set (derangement_enum_aux xs (remove1 z ys))"
+    using Cons ob by auto
+
+  have "distinct zs2"
+    using ev Cons distinct_remove1 by fast
+  moreover have "z \<notin> set zs2"
+    using ev Cons(2) derangement_enum_aux_in by fastforce
+  ultimately show ?case using ob by simp
+qed
+
+lemma derangement_enum_aux_no_overlap: "zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> no_overlap xs zs"
+  by(induct xs arbitrary: zs ys) auto
+
+lemma derangement_enum_aux_set:
+  "length xs = length ys \<Longrightarrow> zs \<in> set (derangement_enum_aux xs ys) \<Longrightarrow> set zs = set ys"
+proof(induct xs ys arbitrary: zs rule: derangement_enum_aux.induct)
+  case (1 ys)
+  then show ?case by simp
+next
+  case (2 x xs ys)
+  obtain z zs2 where ob: "zs = z#zs2"
+    using 2 by auto
+  have ev1: "zs2 \<in> set (derangement_enum_aux xs (remove1 z ys))"
+    using 2 ob  by simp
+  have ev2:"z \<in> set ys"
+    using 2 ob by simp
+
+  have "length xs = length (remove1 z ys)"
+    using ev2 Suc_length_remove1 "2.prems"(1) by force
+  then have "set zs2 = set (remove1 z ys)"
+    using "2.hyps"[of z zs2] ev1 ev2  by simp
+
+  then show ?case
+    using ob notin_set_remove1 ev2 in_set_remove1 by fastforce
+qed
+
+lemma derangement_enum_correct_aux1:
+  "\<lbrakk>distinct zs;length ys = length zs; length ys = length xs; set ys = set zs; no_overlap xs zs\<rbrakk>
+   \<Longrightarrow> zs \<in> set (derangement_enum_aux xs ys)"
+proof(induct xs arbitrary: zs ys)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  obtain z zs2 where ob: "zs = z#zs2"
+    using Cons length_0_conv neq_Nil_conv by metis
+
+  have e1: "z \<noteq> x"
+    using Cons.prems(5) ob  by auto
+
+  have "distinct zs2"
+    using Cons.prems(1) ob by auto 
+  moreover have "length (remove1 z ys) = length zs2" using Cons.prems ob
+    by (simp add: length_remove1) 
+  moreover have "length (remove1 z ys) = length xs"
+    by (simp add: Cons.prems(3) Cons.prems(4) length_remove1 ob) 
+  moreover have "set (remove1 z ys) = set zs2"
+    using Cons ob by (metis distinct_card distinct_remdups length_remdups_eq remove1.simps(2) set_remdups set_remove1_eq)
+  moreover have "no_overlap xs zs2"
+    using Cons.prems(5) ob by fastforce 
+
+  ultimately have "zs2 \<in> set (derangement_enum_aux xs (remove1 z ys))"
+    using Cons.hyps[of zs2 "(remove1 z ys)"] by simp
+  then show ?case
+    using ob e1 Cons by simp 
+qed
+
+theorem derangement_enum_correct: "distinct xs \<Longrightarrow> derangements xs = set (derangement_enum xs)"
+proof(standard)
+  show "distinct xs \<Longrightarrow> derangements xs \<subseteq> set (derangement_enum xs)"
+    unfolding derangements_def using derangement_enum_correct_aux1 by auto 
+next
+  show "distinct xs \<Longrightarrow> set (derangement_enum xs) \<subseteq> derangements xs"
+    unfolding derangements_def
+    using derangement_enum_aux_set derangement_enum_aux_distinct_elem derangement_enum_aux_elem_length derangement_enum_aux_no_overlap
+    by auto
+qed
+
+subsubsection"Distinctness"
+
+lemma derangement_enum_aux_distinct: "distinct ys \<Longrightarrow> distinct (derangement_enum_aux xs ys)"
+proof(induct xs arbitrary: ys)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  show ?case
+    using inj2_distinct_concat_map_function_filter[of
+        "Cons"
+         ys
+         "\<lambda>y. derangement_enum_aux xs (remove1 y ys)"
+        "\<lambda>y. y \<noteq> x"
+      ]
+    using Cons Cons_inj2
+    by (simp)
+qed
+
+theorem derangement_enum_distinct: "distinct xs \<Longrightarrow> distinct (derangement_enum xs)"
+  using derangement_enum_aux_distinct by auto
+
+(*
+subsubsection"Cardinality"
+should be provable with Derangements.Derangements
+*)
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Filter_Bool_List.thy b/thys/Combinatorial_Enumeration_Algorithms/Filter_Bool_List.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Filter_Bool_List.thy
@@ -0,0 +1,111 @@
+theory Filter_Bool_List
+  imports
+  "HOL.List"
+begin
+
+text "A simple algorithm to filter a list by a boolean list. A different approach would be to filter
+by a set of indices, but this approach is faster, because lookups are slow in ML."
+
+fun filter_bool_list :: "bool list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "filter_bool_list [] _ = []"
+| "filter_bool_list _ [] = []"
+| "filter_bool_list (b#bs) (x#xs) =
+    (if b then x#(filter_bool_list bs xs) else (filter_bool_list bs xs))"
+
+text"The following could be an alternative definition, but the version above provides a nice computational induction rule."
+lemma "filter_bool_list bs xs = map snd (filter fst (zip bs xs))"
+  by(induct bs xs rule: filter_bool_list.induct) auto
+
+lemma filter_bool_list_in:
+  "n < length xs \<Longrightarrow> n < length bs \<Longrightarrow> bs!n \<Longrightarrow> xs!n \<in> set (filter_bool_list bs xs)"
+proof (induct bs xs arbitrary: n rule: filter_bool_list.induct)
+  case (3 b bs x xs)
+  then show ?case by(cases n) auto
+qed auto
+
+lemma filter_bool_list_not_elem: "x \<notin> set xs \<Longrightarrow> x \<notin> set (filter_bool_list bs xs)"
+  by(induct bs xs rule: filter_bool_list.induct) auto
+
+lemma filter_bool_list_elem: "x \<in> set (filter_bool_list bs xs) \<Longrightarrow> x \<in> set xs"
+  using filter_bool_list_not_elem by fast
+
+lemma filter_bool_list_not_in:
+  "distinct xs \<Longrightarrow> n < length xs\<Longrightarrow> n < length bs \<Longrightarrow> bs!n = False
+    \<Longrightarrow> xs!n \<notin> set (filter_bool_list bs xs)"
+proof (induct bs xs arbitrary: n rule: filter_bool_list.induct)
+  case (3 b bs x xs)
+  then show ?case proof(induct n)
+    case 0
+    then show ?case using filter_bool_list_not_elem
+      by force
+  qed auto
+qed auto
+
+lemma filter_bool_list_elem_nth:  "ys \<in> set (filter_bool_list bs xs)
+  \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs"
+proof(induct bs xs arbitrary: ys rule: filter_bool_list.induct)
+  case (1 xs)
+  then show ?case by simp
+next
+  case (2 b bs)
+  then show ?case by simp
+next
+  case (3 b bs y ys)
+  then show ?case 
+    by(cases b) (force)+
+qed 
+
+text"May be a useful conversion, since the algorithm could also be implemented with a list of indices."
+lemma filter_bool_list_set_nth:
+  "set (filter_bool_list bs xs) = {xs ! n |n. bs ! n \<and> n < length bs \<and> n < length xs}"
+  by (auto simp: filter_bool_list_in filter_bool_list_elem_nth)
+
+lemma filter_bool_list_exist_length: "A \<subseteq> set xs
+  \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs)"
+proof(induct xs arbitrary: A)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons x xs)
+  from Cons have "A - {x} \<subseteq> set xs"
+    by auto
+  from this Cons have 1: "\<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)"
+    by simp
+
+  then have "\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))"
+    by (metis Diff_empty Diff_insert0 insert_Diff_single insert_absorb list.simps(15) list.size(4) filter_bool_list.simps(3))
+  
+  then show ?case .
+qed
+
+lemma filter_bool_list_card:
+  "\<lbrakk>distinct xs; length xs = length bs\<rbrakk> \<Longrightarrow> card (set (filter_bool_list bs xs)) = count_list bs True" 
+  by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem)
+
+lemma filter_bool_list_exist_length_card_True: "\<lbrakk>distinct xs; A \<subseteq> set xs; n = card A\<rbrakk>
+   \<Longrightarrow> \<exists>bs. length bs = length xs \<and> count_list bs True = card A \<and> A = set (filter_bool_list bs xs)"
+  by (metis filter_bool_list_card filter_bool_list_exist_length)
+
+lemma filter_bool_list_distinct: "distinct xs \<Longrightarrow> distinct (filter_bool_list bs xs)"
+  by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem) 
+
+lemma filter_bool_list_inj_aux:
+  assumes "length bs1 = length xs"
+  and "length xs = length bs2"
+  and "distinct xs"
+shows "filter_bool_list bs1 xs = filter_bool_list bs2 xs \<Longrightarrow> bs1 = bs2"
+using assms proof(induct rule: list_induct3)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons b1 bs1 x xs b2 bs2)
+  then show ?case
+    by(cases b1; cases b2, auto) (metis list.set_intros(1) filter_bool_list_not_elem)+
+qed
+
+lemma filter_bool_list_inj:
+  "distinct xs \<Longrightarrow> inj_on (\<lambda>bs. filter_bool_list bs xs) {bs. length bs = length xs}"
+  unfolding inj_on_def using filter_bool_list_inj_aux by fastforce
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Integer_Compositions.thy b/thys/Combinatorial_Enumeration_Algorithms/Integer_Compositions.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Integer_Compositions.thy
@@ -0,0 +1,190 @@
+section "Integer Compositions"
+
+theory Integer_Compositions
+  imports
+    Common_Lemmas
+begin
+
+subsection"Definition"
+
+definition integer_compositions :: "nat \<Rightarrow> nat list set" where
+  "integer_compositions i = {xs. sum_list xs = i \<and> 0 \<notin> set xs}"
+text "Integer compositions are \<open>integer_partitions\<close> where the order matters."
+text "Cardinality: \<open>sum from n = 1 to i (binomial (i-1) (n-1)) = 2^(i-1)\<close>"
+text "Example: \<open>integer_compositions 3 = {[3], [2,1], [1,2], [1,1,1]}\<close>"
+
+subsection"Algorithm"
+
+fun integer_composition_enum :: "nat \<Rightarrow> nat list list" where
+  "integer_composition_enum 0 = [[]]"
+| "integer_composition_enum (Suc n) =
+    [Suc m #xs. m \<leftarrow> [0..< Suc n], xs \<leftarrow> integer_composition_enum (n-m)]"
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+lemma integer_composition_enum_tail_elem:
+  "x#xs \<in> set (integer_composition_enum n) \<Longrightarrow> xs \<in> set (integer_composition_enum (n - x))"
+  by(induct n) auto
+
+lemma integer_composition_enum_not_null_aux:
+  "x#xs \<in> set (integer_composition_enum n) \<Longrightarrow> x \<noteq> 0"
+  by(induct n) auto
+
+lemma integer_composition_enum_not_null: "xs \<in> set (integer_composition_enum n) \<Longrightarrow> 0 \<notin> set xs"
+proof(induct xs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons a xs)
+  then show ?case 
+    using integer_composition_enum_not_null_aux integer_composition_enum_tail_elem
+    by fastforce
+qed
+
+lemma integer_composition_enum_empty: "[] \<in> set (integer_composition_enum n) \<Longrightarrow> n = 0"
+  by(induct n) auto
+
+lemma integer_composition_enum_sum: "xs \<in> set (integer_composition_enum n) \<Longrightarrow> sum_list xs = n"
+proof(induct n arbitrary: xs rule: integer_composition_enum.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 x)
+  show ?case proof(cases xs)
+    case Nil
+    then show ?thesis using 2 by auto
+  next
+    case (Cons y ys)
+    have p1: "sum_list ys = Suc x - y" using 2 Cons
+      by auto
+
+    have "Suc x \<ge> y"
+      using 2 Cons by auto
+    then have p2: "sum_list ys = Suc x - y \<Longrightarrow> y + sum_list ys = Suc x"
+      by simp
+
+    show ?thesis
+      using p1 p2 Cons by simp
+  qed
+qed
+
+lemma integer_composition_enum_head_set:
+  assumes"x \<noteq> 0" and "x \<le> n"
+  shows" xs \<in> set (integer_composition_enum (n-x)) \<Longrightarrow> x#xs \<in> set (integer_composition_enum n)"
+using assms proof(induct n arbitrary: x xs)
+  case 0
+  then show ?case
+    by simp
+next
+  case c1: (Suc n)
+  from c1.prems have 1:
+    "\<forall>y\<in>{0..<n}. x = Suc y \<longrightarrow> xs \<notin> set (integer_composition_enum (n - y)) \<Longrightarrow> x = Suc n"
+    by(induct x) simp_all
+
+  then have 2: "\<forall>y\<in>{0..<n}. x = Suc y \<longrightarrow> xs \<notin> set (integer_composition_enum (n - y)) \<Longrightarrow> xs = []"
+    using c1.prems(1) by simp
+  show ?case using 1 2 by auto
+qed
+
+lemma integer_composition_enum_correct_aux:
+  "0 \<notin> set xs \<Longrightarrow> xs \<in> set (integer_composition_enum (sum_list xs))"
+  by(induct xs) (auto simp: integer_composition_enum_head_set) 
+
+theorem integer_composition_enum_correct: 
+  "set (integer_composition_enum n) = integer_compositions n"
+proof standard
+  show "set (integer_composition_enum n) \<subseteq> integer_compositions n"
+    unfolding integer_compositions_def
+    using integer_composition_enum_not_null integer_composition_enum_sum by auto
+next
+  show "integer_compositions n \<subseteq> set (integer_composition_enum n)"
+    unfolding integer_compositions_def
+    using integer_composition_enum_correct_aux by auto
+qed
+
+subsubsection"Distinctness"
+
+theorem integer_composition_enum_distinct:
+  "distinct (integer_composition_enum n)"
+proof(induct n rule: integer_composition_enum.induct)
+  case 1
+  then show ?case by auto
+next
+  case (2 n)
+
+  have h1: "x \<in> set [0..<Suc n] \<Longrightarrow> distinct (integer_composition_enum (n - x))" for x
+    using "2" by simp
+    
+  have h2: "distinct [0..<n]"
+    by simp
+
+  have "distinct [Suc m #xs. m \<leftarrow> [0..< n], xs \<leftarrow> integer_composition_enum (n-m)]"
+    using h1 h2 Cons_Suc_distinct_concat_map_function by simp
+  then show ?case by auto 
+qed
+
+subsubsection"Cardinality"
+
+lemma sum_list_two_pow_aux:
+  "(\<Sum>x\<leftarrow>[0..< n]. (2::nat) ^ (n - x)) + 2 ^ (0 - 1) + 2 ^ 0 = 2 ^ (Suc n)"
+proof(induct n)
+  case 0
+  then show ?case by simp
+next
+  case c1: (Suc n)
+
+  have "x \<le> n \<Longrightarrow> 2 ^ (Suc n - x) = 2 * 2^ (n - x)" for x
+    by (simp add: Suc_diff_le)
+  also have "x \<in> set [0..<Suc n] \<Longrightarrow> x \<le> n" for x
+    by auto
+  ultimately have "(\<Sum>x\<leftarrow>[0..<Suc n]. 2 ^ (Suc n - x)) = (\<Sum>x\<leftarrow>[0..<Suc n]. 2* 2 ^ (n - x))"
+     by (metis (mono_tags, lifting) map_eq_conv)
+  
+  also have "... = (\<Sum>x\<leftarrow>[0..< n]. 2* 2 ^ (n - x)) + 2* 2 ^ (0)"
+    using sum_list_extract_last by simp
+  
+  also have "(\<Sum>x\<leftarrow>[0..< n]. (2::nat)* (2::nat) ^ (n - x)) = 2*(\<Sum>x\<leftarrow>[0..< n]. 2 ^ (n - x))"
+    using sum_list_const_mult by fast
+
+  ultimately have "(\<Sum>x\<leftarrow>[0..<Suc n]. (2::nat) ^ (Suc n - x))
+      = 2*(\<Sum>x\<leftarrow>[0..< n]. 2 ^ (n - x)) + 2* 2 ^ (0)"
+    by metis
+
+  then show ?case using c1
+    by simp 
+qed
+
+lemma sum_list_two_pow:
+  "Suc (\<Sum>x\<leftarrow>[0..<n]. 2 ^ (n - Suc x)) = 2 ^ n"
+  using sum_list_two_pow_aux sum_list_extract_last by(cases n) auto
+
+lemma integer_composition_enum_length:
+  "length (integer_composition_enum n) = 2^(n-1)"
+proof(induct n rule: integer_composition_enum.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 n)
+  then have "length [Suc m #xs. m \<leftarrow> [0..< n], xs \<leftarrow> integer_composition_enum (n-m)]
+        = (\<Sum>x\<leftarrow>[0..<n]. 2 ^ (n - x - 1))"
+    using length_concat_map_function_sum_list [of
+        "[0..< n]"
+        "\<lambda> x. integer_composition_enum (n - x)"
+        "\<lambda> x. 2 ^ (n - x - 1)"
+        "\<lambda> m xs. Suc m #xs"]
+    by auto
+
+  then show ?case
+    using sum_list_two_pow
+    by simp
+qed
+
+theorem integer_compositions_card:
+  "card (integer_compositions n) = 2^(n-1)"
+  using integer_composition_enum_correct integer_composition_enum_length
+    integer_composition_enum_distinct distinct_card by metis
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Integer_Partitions.thy b/thys/Combinatorial_Enumeration_Algorithms/Integer_Partitions.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Integer_Partitions.thy
@@ -0,0 +1,216 @@
+section "Integer Paritions"
+
+theory Integer_Partitions
+  imports
+    "HOL-Library.Multiset"
+    Common_Lemmas
+    Card_Number_Partitions.Card_Number_Partitions
+begin
+
+subsection"Definition"
+
+definition integer_partitions :: "nat \<Rightarrow> nat multiset set" where
+  "integer_partitions i = {A. sum_mset A = i \<and> 0 \<notin># A}"
+text \<open>Cardinality: \<open>Partition i\<close> (from \<open>Card_Number_Partitions.Card_Number_Partitions\<close> \cite{AFPnumpat})\<close>
+text "Example: \<open>integer_partitions 4 = {{4}, {3,1}, {2,2} {2,1,1}, {1,1,1,1}}\<close>"
+
+subsection"Algorithm"
+
+fun integer_partitions_enum_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat list list" where
+  "integer_partitions_enum_aux 0 m = [[]]"
+| "integer_partitions_enum_aux n m =
+  [h#r . h \<leftarrow> [1..< Suc (min n m)], r \<leftarrow> integer_partitions_enum_aux (n-h) h]"
+
+fun integer_partitions_enum :: "nat \<Rightarrow> nat list list" where
+ "integer_partitions_enum n = integer_partitions_enum_aux n n"
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+lemma integer_partitions_empty: "[] \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> n = 0"
+  by(induct n) auto
+
+lemma integer_partitions_enum_aux_first:
+  "x # xs \<in> set (integer_partitions_enum_aux n m)
+    \<Longrightarrow> xs \<in> set (integer_partitions_enum_aux (n-x) x)"
+  by(induct n) auto
+
+lemma integer_partitions_enum_aux_max_n:
+  "x#xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> x \<le> n"
+  by (induct n) auto
+
+lemma integer_partitions_enum_aux_max_head:
+  "x#xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> x \<le> m"
+  by (induct n) auto
+
+(*not used, but nice to have nonetheless*)
+lemma integer_partitions_enum_aux_max:
+  "xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> x \<in> set xs \<Longrightarrow> x \<le> m"
+proof(induct xs arbitrary: n m x)
+  case Nil
+  then show ?case using integer_partitions_enum_aux_max_head by simp
+next
+  case (Cons y xs)
+  then show ?case 
+    using integer_partitions_enum_aux_max_head integer_partitions_enum_aux_first  
+    by fastforce                                         
+qed
+
+lemma integer_partitions_enum_aux_sum:
+  "xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> sum_list xs = n"
+proof(induct xs arbitrary: n m)
+  case Nil
+  then show ?case using integer_partitions_empty by simp
+next
+  case (Cons x xs)
+  then have "\<lbrakk>xs \<in> set (integer_partitions_enum_aux (n-x) x)\<rbrakk> \<Longrightarrow> sum_list xs = (n-x)"
+    by simp
+  moreover have "xs \<in> set (integer_partitions_enum_aux (n-x) x)"
+    using Cons integer_partitions_enum_aux_first by simp
+  moreover have "x \<le> n"
+    using Cons integer_partitions_enum_aux_max_n by simp
+  ultimately show ?case
+    by simp
+qed
+
+lemma integer_partitions_enum_aux_not_null_aux:
+  "x#xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> x \<noteq> 0"
+  by (induct n) auto
+
+lemma integer_partitions_enum_aux_not_null:
+  "xs \<in> set (integer_partitions_enum_aux n m) \<Longrightarrow> x \<in> set xs \<Longrightarrow> x \<noteq> 0"
+proof(induct xs arbitrary: x n m)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons y xs)
+  show ?case proof(cases "y = x")
+    case True
+    then show ?thesis
+      using Cons integer_partitions_enum_aux_not_null_aux by simp 
+  next
+    case False
+    then show ?thesis
+       using Cons integer_partitions_enum_aux_not_null_aux integer_partitions_enum_aux_first
+       by fastforce
+  qed
+qed
+
+lemma integer_partitions_enum_aux_head_minus:
+     "h \<le> m \<Longrightarrow> h > 0 \<Longrightarrow> n \<ge> h \<Longrightarrow>
+  ys \<in> set (integer_partitions_enum_aux (n-h) h)\<Longrightarrow> h#ys \<in> set (integer_partitions_enum_aux n m)"
+proof(induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  then have 1: "1 \<le> m" by simp
+
+  have 2: "(\<exists>x. (x = min (Suc n) m \<or> Suc 0 \<le> x \<and> x < Suc n \<and> x < m) \<and> h # ys
+      \<in> (#) x ` set (integer_partitions_enum_aux (Suc n - x) x))"
+    unfolding image_def using Suc by auto
+
+  from 1 2 have "Suc 0 \<le> m \<and>(\<exists>x. (x = min (Suc n) m \<or> Suc 0 \<le> x \<and> x < Suc n \<and> x < m)
+         \<and> h # ys \<in> (#) x ` set (integer_partitions_enum_aux (Suc n - x) x))"
+    by simp
+    
+  then show ?case by auto
+qed
+
+lemma integer_partitions_enum_aux_head_plus:
+  "h \<le> m \<Longrightarrow> h > 0 \<Longrightarrow> ys \<in> set (integer_partitions_enum_aux n h)
+    \<Longrightarrow> h#ys \<in> set (integer_partitions_enum_aux (h + n) m)"
+  using integer_partitions_enum_aux_head_minus by simp 
+
+lemma integer_partitions_enum_correct_aux1:
+  assumes "0 \<notin># A "
+  and "\<forall>x \<in># A. x \<le> m"
+shows" \<exists>xs\<in>set (integer_partitions_enum_aux (\<Sum>\<^sub># A) m). A = mset xs"
+using assms proof(induct A arbitrary: m rule: multiset_induct_max)
+  case empty
+  then show ?case by simp
+next
+  case (add h A)
+  have hc1: "h \<le> m"
+    using add by simp
+
+  have hc2: "h > 0"
+    using add by simp
+
+  obtain ys where o1: "ys \<in> set (integer_partitions_enum_aux (\<Sum>\<^sub># A) h)" and o2: " A = mset ys"
+    using add by force
+
+  have "h#ys \<in> set (integer_partitions_enum_aux (h + \<Sum>\<^sub># A) m)"
+    using integer_partitions_enum_aux_head_plus hc1 o1 hc2 by blast 
+
+  then show ?case
+    using o2 by force
+qed
+
+theorem integer_partitions_enum_correct:
+  "set (map mset (integer_partitions_enum n)) = integer_partitions n"
+proof(standard)
+  have "\<lbrakk>xs \<in> set (integer_partitions_enum_aux n n)\<rbrakk> \<Longrightarrow> \<Sum>\<^sub># (mset xs) = n" for xs
+    by (simp add: integer_partitions_enum_aux_sum sum_mset_sum_list)
+  moreover have "xs \<in> set (integer_partitions_enum_aux n n) \<Longrightarrow> 0 \<notin># mset xs" for xs
+    using integer_partitions_enum_aux_not_null by auto
+  ultimately show "set (map mset (integer_partitions_enum n)) \<subseteq> integer_partitions n"
+    unfolding integer_partitions_def by auto
+next
+  have "0 \<notin># A \<Longrightarrow> A \<in> mset ` set (integer_partitions_enum_aux (\<Sum>\<^sub># A) (\<Sum>\<^sub># A))" for A
+    unfolding image_def
+    using integer_partitions_enum_correct_aux1 by (simp add: sum_mset.remove)
+  then show "integer_partitions n \<subseteq> set (map mset (integer_partitions_enum n))"
+    unfolding integer_partitions_def by auto
+qed
+
+subsubsection"Distinctness"
+
+lemma integer_partitions_enum_aux_distinct:
+  "distinct (integer_partitions_enum_aux n m)"
+proof(induct n m rule:integer_partitions_enum_aux.induct)
+  case (1 m)
+  then show ?case by simp
+next
+  case (2 n m)
+  have "distinct [h#r . h \<leftarrow> [1..< Suc (min (Suc n) m)], r \<leftarrow> integer_partitions_enum_aux ((Suc n)-h) h]"
+    apply(subst Cons_distinct_concat_map_function)
+    using 2 by auto
+  then show ?case by simp
+qed
+
+theorem integer_partitions_enum_distinct:
+  "distinct (integer_partitions_enum n)"
+  using integer_partitions_enum_aux_distinct by simp
+
+subsubsection"Cardinality"
+
+lemma partitions_bij_betw_count:
+  "bij_betw count {N. count N partitions n} {p. p partitions n}"
+  by (rule bij_betw_byWitness[where f'="Abs_multiset"]) (auto simp: partitions_imp_finite_elements)
+
+lemma card_partitions_count_partitions:
+  "card {p. p partitions n} = card {N. count N partitions n}"
+  using bij_betw_same_card partitions_bij_betw_count by metis
+
+text"this sadly is not proven in \<open>Card_Number_Partitions.Card_Number_Partitions\<close>"
+lemma card_partitions_number_partition:
+  "card {p. p partitions n} = card {N. number_partition n N}"
+  using card_partitions_count_partitions count_partitions_iff by simp
+
+lemma integer_partitions_number_partition_eq:
+  "integer_partitions n = {N. number_partition n N}"
+  using integer_partitions_def number_partition_def by auto
+
+lemma integer_partitions_cardinality_aux:
+  "card (integer_partitions n) = (\<Sum>k\<le>n. Partition n k)"
+  using card_partitions_number_partition integer_partitions_number_partition_eq card_partitions
+  by simp
+
+theorem integer_partitions_cardinality:
+  "card (integer_partitions n) = Partition (2*n) n"
+  using integer_partitions_cardinality_aux Partition_sum_Partition_diff add_implies_diff le_add1 mult_2
+  by simp  
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Powerset.thy b/thys/Combinatorial_Enumeration_Algorithms/Powerset.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Powerset.thy
@@ -0,0 +1,97 @@
+section \<open>Powerset\<close>
+theory Powerset
+  imports
+    Main
+    n_Sequences
+    Common_Lemmas
+    Filter_Bool_List
+begin
+
+subsection"Definition"
+
+text "Pow A"
+text "Cardinality: \<open>2 ^ card A\<close>"
+text "Example: \<open>Pow {0,1} = {{}, {1}, {0}, {0, 1}}\<close>"
+
+subsection"Algorithm"
+
+fun all_bool_lists :: "nat \<Rightarrow> bool list list" where
+  "all_bool_lists 0 = [[]]"
+| "all_bool_lists (Suc x) = concat [[False#xs, True#xs] . xs \<leftarrow> all_bool_lists x]"
+
+fun powerset_enum where
+  "powerset_enum xs = [(filter_bool_list x xs) . x \<leftarrow> all_bool_lists (length xs)]"
+
+subsection"Verification"
+
+text "First we show the relevant theorems for \<open>all_bool_lists\<close>, then we'll transfer the
+results to the enumeration algorithm for powersets."
+
+lemma distinct_concat_aux: "distinct xs \<Longrightarrow> distinct (concat (map (\<lambda>xs. [False # xs, True # xs]) xs))"
+  by (induct xs) auto
+
+lemma distinct_all_bool_lists : "distinct (all_bool_lists x)"
+  by (induct x) (auto simp add: distinct_concat_aux)
+
+lemma all_bool_lists_correct: "set (all_bool_lists x) = {xs. length xs = x}"
+proof(standard)
+  show "set (all_bool_lists x) \<subseteq> {xs. length xs = x}"
+    by (induct x) auto
+next
+  show "{xs. length xs = x} \<subseteq> set (all_bool_lists x)"
+  proof(induct x)
+    case 0
+    then show ?case by simp
+  next
+    case (Suc x)
+    have "length ys = Suc x \<Longrightarrow> \<exists>xs. ys = False # xs \<or> ys = True # xs" for ys
+      by (metis (full_types) Suc_length_conv)
+    then show ?case using Suc
+      by fastforce
+  qed
+qed
+
+subsubsection"Correctness"
+
+theorem powerset_enum_correct: "set (map set (powerset_enum xs)) = Pow (set xs)"
+proof(standard)
+  show "set (map set (powerset_enum xs)) \<subseteq> Pow (set xs)"
+    using filter_bool_list_not_elem by fastforce
+next
+  have "\<And>x. x \<subseteq> set xs \<Longrightarrow> x \<in> (\<lambda>x. set (filter_bool_list x xs)) ` {zs. length zs = length xs}"
+    unfolding image_def using filter_bool_list_exist_length image_def by auto
+  then show "Pow (set xs) \<subseteq> set (map set (powerset_enum xs))"
+    using all_bool_lists_correct by auto
+qed
+  
+subsubsection"Distinctness"
+
+theorem powerset_enum_distinct_elem: "distinct xs \<Longrightarrow> ys \<in> set (powerset_enum xs) \<Longrightarrow> distinct ys"
+  using filter_bool_list_distinct by auto 
+
+theorem powerset_enum_distinct: "distinct xs \<Longrightarrow> distinct (powerset_enum xs)"
+proof -
+  assume dis: "distinct xs"
+  then have " distinct (map (\<lambda>x. filter_bool_list x xs) (all_bool_lists (length xs)))"
+    using distinct_map filter_bool_list_inj distinct_all_bool_lists
+    by (metis all_bool_lists_correct)
+  then show ?thesis
+    using dis by simp
+qed
+
+subsubsection"Cardinality"
+
+text "Cardinality for powersets is already shown in @{thm [source] card_Pow}."
+
+subsection"Alternative algorithm with \<open>n_sequence_enum\<close>"
+
+fun all_bool_lists2 :: "nat \<Rightarrow> bool list list" where
+  "all_bool_lists2 n = n_sequence_enum [True, False] n"
+
+lemma all_bool_lists2_distinct: "distinct (all_bool_lists2 n)"
+  by (auto simp add: n_sequence_enum_distinct)
+
+lemma all_bool_lists2_correct: "set (all_bool_lists n) = set (all_bool_lists2 n)"
+  by (auto simp: all_bool_lists_correct n_sequence_enum_correct n_sequences_def)
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/ROOT b/thys/Combinatorial_Enumeration_Algorithms/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/ROOT
@@ -0,0 +1,13 @@
+chapter AFP
+
+session Combinatorial_Enumeration_Algorithms (AFP) = "HOL-Library" +
+  options [timeout = 600]
+  sessions
+	"HOL-Combinatorics"
+	"Falling_Factorial_Sum"
+	"Card_Number_Partitions"
+  theories
+    Combinatorial_Enumeration_Algorithms
+  document_files
+    "root.tex"
+    "root.bib"
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Trees.thy b/thys/Combinatorial_Enumeration_Algorithms/Trees.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Trees.thy
@@ -0,0 +1,224 @@
+section "Trees"
+
+theory Trees
+imports
+    "HOL-Library.Tree"
+    Common_Lemmas
+    (* "Catalan_Numbers.Catalan_Numbers" very big *)
+begin
+
+subsection"Definition"
+
+text \<open>The set of trees can be defined with the pre-existing @{term "tree"} datatype:\<close>
+definition trees :: "nat \<Rightarrow> unit tree set" where
+  "trees n = {t. size t = n}"
+
+text "Cardinality: \<open>Catalan number of n\<close>"
+text "Example: \<open>trees 0 = {Leaf}\<close>"
+
+(*algorithm and cardinality proofs taken from what Tobias Nipkow send me*)
+
+subsection"Algorithm"
+fun tree_enum :: "nat \<Rightarrow> unit tree list" where
+"tree_enum 0 = [Leaf]" |
+"tree_enum (Suc n) = [\<langle>t1, (), t2\<rangle>. i \<leftarrow> [0..<Suc n], t1 \<leftarrow> tree_enum i, t2 \<leftarrow> tree_enum (n-i)]"
+
+subsection"Verification"
+
+subsubsection"Cardinality"
+
+lemma length_tree_enum:
+  "length (tree_enum(Suc n)) = (\<Sum>i\<le>n. length(tree_enum i) * length(tree_enum (n - i)))"
+  by (simp add: length_concat comp_def sum_list_triv atLeast_upt interv_sum_list_conv_sum_set_nat
+         flip: lessThan_Suc_atMost)
+(*
+lemma "length (tree_enum n) = catalan n"
+apply(induction n rule: catalan.induct)
+apply(auto simp: length_tree_enum catalan_Suc simp del: upt_Suc tree_enum.simps(2))
+done
+*)
+
+subsubsection"Correctness"
+
+lemma tree_enum_correct1: "t \<in> set (tree_enum n) \<Longrightarrow> size t = n"
+  by (induct n arbitrary: t rule: tree_enum.induct) (simp, fastforce)
+
+lemma tree_enum_correct2: "n = size t \<Longrightarrow> t \<in> set (tree_enum n)"
+proof (induct n arbitrary: t rule: tree_enum.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 n)
+  show ?case proof(cases t)
+    case Leaf
+    then show ?thesis
+      by (simp add: "2.prems") 
+  next
+    case (Node l e r)
+
+    have i1: "(size l) < Suc n" using "2.prems" Node by auto
+    have i2: "(size r) < Suc n" using "2.prems" Node by auto 
+
+    have t1: "l \<in> set (tree_enum (size l))"
+      apply(rule "2.hyps"(1) [of "(size l)"])
+      using i1 by auto
+
+    have t2: "r \<in> set (tree_enum (size r))"
+      apply(rule "2.hyps"(1) [of "(size r)"])
+      using i2 by auto
+
+    have "\<langle>l, (), r\<rangle> \<notin> (\<lambda>t1. \<langle>t1, (), \<langle>\<rangle>\<rangle>) ` set (tree_enum (size l + size r)) \<Longrightarrow>
+        \<exists>x\<in>{0..<size l + size r}. \<exists>xa\<in>set (tree_enum x). \<langle>l, (), r\<rangle> \<in> Node xa () ` set (tree_enum (size l + size r - x))"
+      using t1 t2 by fastforce
+    then have "\<langle>l, e, r\<rangle> \<in> set (tree_enum (size \<langle>l, e, r\<rangle>))"
+      by auto
+
+    then show ?thesis
+      using Node using "2.prems" by simp
+  qed
+qed
+
+theorem tree_enum_correct: "set(tree_enum n) = trees n"
+proof(standard)
+  show "set (tree_enum n) \<subseteq> trees n"
+    unfolding trees_def using tree_enum_correct1 by auto
+next
+  show "trees n \<subseteq> set (tree_enum n)"
+    unfolding trees_def using tree_enum_correct2 by auto
+qed
+
+subsubsection"Distinctness"
+
+lemma tree_enum_Leaf: "\<langle>\<rangle> \<in> set (tree_enum n) \<longleftrightarrow> (n = 0)"
+  by(cases n) auto
+
+lemma tree_enum_elem_injective: "n \<noteq> m \<Longrightarrow> x \<in> set (tree_enum n) \<Longrightarrow> y \<in> set (tree_enum m) \<Longrightarrow> x \<noteq> y"
+  using tree_enum_correct1 by auto
+
+lemma tree_enum_elem_injective2: "x \<in> set (tree_enum n) \<Longrightarrow> y \<in> set (tree_enum m) \<Longrightarrow> x = y \<Longrightarrow> n = m"
+  using tree_enum_elem_injective by auto
+
+lemma concat_map_Node_not_equal:
+  "xs \<noteq> [] \<Longrightarrow> xs2 \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> ys2 \<noteq> [] \<Longrightarrow> 
+  \<forall> x\<in> set xs. \<forall> y \<in> set ys . x \<noteq> y \<Longrightarrow> 
+  [\<langle>l, (), r\<rangle>. l \<leftarrow> xs2, r \<leftarrow> xs] \<noteq> [\<langle>l, (), r\<rangle>. l \<leftarrow> ys2, r \<leftarrow> ys]"
+proof(induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  then show ?case proof(induct ys)
+    case Nil
+    then show ?case by simp
+  next
+    case (Cons y ys)
+    obtain x2 x2s where o1: "xs2 = x2 # x2s"
+      by (meson Cons.prems(3) neq_Nil_conv)
+    obtain y2 y2s where o2: "ys2 = y2 # y2s"
+      by (meson Cons.prems(5) neq_Nil_conv)
+
+    have "[\<langle>l, (), r\<rangle>. l \<leftarrow> x2#x2s, r \<leftarrow> x # xs] \<noteq> [\<langle>l, (), r\<rangle>. l \<leftarrow> y2#y2s, r \<leftarrow> y # ys]"
+      using Cons.prems(6) by auto
+    then show ?case
+      using o1 o2 by simp  
+  qed
+qed
+
+lemma tree_enum_not_empty: "tree_enum n \<noteq> []"
+  by(induct n) auto
+
+lemma tree_enum_distinct_aux_outer:
+  assumes "\<forall>i \<le> n. distinct (tree_enum i)"
+  and "distinct xs"
+  and "\<forall> i \<in> set xs. i < n"
+  and "sorted_wrt (<) xs"
+  shows "distinct (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) xs)"
+using assms proof(induct xs arbitrary: n)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  have b1: "x < n" using Cons by auto
+
+  have "\<forall> i \<in> set xs . x < i"
+    using Cons.prems(4) strict_sorted_simps(2) by simp 
+  then have "\<forall> i \<in> set xs . (n - i) < (n - x)"
+    using b1 diff_less_mono2 by simp
+
+  then have "\<forall> i \<in> set xs. \<forall> t1\<in> set (tree_enum (n - x)). \<forall> t2 \<in> set (tree_enum (n - i)) . t1 \<noteq> t2"
+    using tree_enum_correct1 by (metis less_irrefl_nat) 
+  then have 1: "\<forall> i \<in> set xs. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum x, r \<leftarrow> tree_enum (n-x)] \<noteq>
+          [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]"
+    using concat_map_Node_not_equal tree_enum_not_empty by simp
+
+  have 2: "distinct (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) xs)"
+    using Cons by auto
+    
+  from 1 2 show ?case by auto
+qed
+  
+lemma tree_enum_distinct_aux_left:
+   "\<forall> i < n. distinct (tree_enum i) \<Longrightarrow> distinct ([\<langle>l, (), r\<rangle>. i \<leftarrow> [0..< n], l \<leftarrow> tree_enum i])"
+proof(induct "n")
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have 1:"distinct (tree_enum n)"
+    using Suc.prems by auto
+  have 2: "distinct ([\<langle>l, (), r\<rangle>. i \<leftarrow> [0..< n], l \<leftarrow> tree_enum i])"
+    using Suc by simp
+  have 3: "distinct (map (\<lambda>l. \<langle>l, (), r\<rangle>) (tree_enum n))"
+    using Node_left_distinct_map 1 by simp
+
+  have 4: "\<lbrakk>\<And>t n. t \<in> set (tree_enum n) \<Longrightarrow> size t = n; m < n; y \<in> set (tree_enum n); y \<in> set (tree_enum m)\<rbrakk> \<Longrightarrow> False" for m y
+    by blast
+    
+  from 1 2 3 4 tree_enum_correct1 show ?case
+    by fastforce
+qed
+
+theorem tree_enum_distinct: "distinct(tree_enum n)"
+proof(induct n rule: tree_enum.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 n)
+  then have Ir: "i < Suc n \<Longrightarrow> distinct (tree_enum i)" for i
+    by (metis atLeastLessThan_iff set_upt zero_le) 
+
+  have c1: "distinct (concat (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) [0..<n]))"
+  proof(rule distinct_concat)
+    show "distinct (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) [0..<n])"
+      apply(rule tree_enum_distinct_aux_outer)
+      using Ir by auto
+  next
+    have "\<And>x. x < n \<Longrightarrow> distinct ([\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum x, r \<leftarrow> tree_enum (n-x)])"
+      using Ir by (simp add: Node_right_distinct_concat_map)
+    then show "\<And>ys. ys \<in> set (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) [0..<n]) \<Longrightarrow> distinct ys"
+      by auto
+  next
+    have "\<lbrakk>[\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum x, r \<leftarrow> tree_enum (n-x)] \<noteq>
+        [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum z, r \<leftarrow> tree_enum (n-z)];
+        y \<in> set (tree_enum x); y \<in> set (tree_enum z)\<rbrakk>
+       \<Longrightarrow> False" for x z y
+      using tree_enum_elem_injective2 by auto
+    then show  "\<And>ys zs.
+       \<lbrakk>ys \<in> set (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) [0..<n]);
+        zs \<in> set (map (\<lambda>i. [\<langle>l, (), r\<rangle>. l \<leftarrow> tree_enum i, r \<leftarrow> tree_enum (n-i)]) [0..<n]); ys \<noteq> zs\<rbrakk>
+       \<Longrightarrow> set ys \<inter> set zs = {}"
+      by fastforce
+  qed
+
+  have "distinct (tree_enum n)"
+    using 2 by simp
+  then have c2: "distinct (map (\<lambda>t1. \<langle>t1, (), \<langle>\<rangle>\<rangle>) (tree_enum n))"
+    using Node_left_distinct_map by fastforce
+  
+  have c3: "\<And>xa xb. \<lbrakk>xa < n; xb \<in> set (tree_enum xa); xb \<in> set (tree_enum n); \<langle>\<rangle> \<in> set (tree_enum (n - xa))\<rbrakk> \<Longrightarrow> False"
+    by (simp add: tree_enum_Leaf) 
+
+  from c1 c2 c3 show ?case
+    by fastforce
+qed
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/Weak_Integer_Compositions.thy b/thys/Combinatorial_Enumeration_Algorithms/Weak_Integer_Compositions.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/Weak_Integer_Compositions.thy
@@ -0,0 +1,170 @@
+section "Weak Integer Compositions"
+
+theory Weak_Integer_Compositions
+  imports
+    "HOL-Combinatorics.Multiset_Permutations"
+    Common_Lemmas
+begin
+
+subsection"Definition"
+
+definition weak_integer_compositions :: "nat \<Rightarrow> nat \<Rightarrow> nat list set" where
+  "weak_integer_compositions i l = {xs. length xs = l \<and> sum_list xs = i}"
+text "Weak integer compositions are similar to integer compositions, with the trade-off that 0 is
+  allowed but the composition must have a fixed length."
+text "Cardinality: \<open>binomial (i + n - 1) i\<close>"
+text "Example: \<open>weak_integer_compositions 2 2 = {[2,0], [1,1], [0,2]}\<close>"
+
+subsection"Algorithm"
+
+fun weak_integer_composition_enum :: "nat \<Rightarrow> nat \<Rightarrow> nat list list" where
+  "weak_integer_composition_enum i 0 = (if i = 0 then [[]] else [])"
+| "weak_integer_composition_enum i (Suc 0) = [[i]]"
+| "weak_integer_composition_enum i l =
+  [h#r . h \<leftarrow> [0..< Suc i], r \<leftarrow> weak_integer_composition_enum (i-h) (l-1)]"
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+lemma weak_integer_composition_enum_length:
+  "xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l"
+proof(induct l arbitrary: xs i)
+  case 0
+  then show ?case by simp
+next
+  case (Suc l)
+  then show ?case by(cases l) auto 
+qed
+
+lemma weak_integer_composition_enum_sum_list:
+  "xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i"
+proof(induct l arbitrary: xs i)
+  case 0
+  then show ?case by simp
+next
+  case (Suc l)
+  then show ?case by(cases l) auto 
+qed
+  
+lemma weak_integer_composition_enum_head:
+  assumes "xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))"
+  shows "x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))"
+proof(cases "length xs")
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc y)
+
+  (*maybe this should be proven elsewhere*)
+  have 1: "\<lbrakk>n \<in> set xs; 0 < n\<rbrakk> \<Longrightarrow> 0 < sum_list xs" for n
+    using sum_list_eq_0_iff by fast
+
+
+  have 2: "xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs"
+    using Suc assms not_gr0 by fastforce
+
+  have "x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y))
+    \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))"
+   unfolding image_def using Suc assms 1 2 by auto
+    
+  from Suc this show ?thesis
+    by auto
+qed
+
+lemma weak_integer_composition_enum_correct_aux:
+  "xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))"
+  by (induct xs) (auto simp: weak_integer_composition_enum_head)
+
+theorem weak_integer_composition_enum_correct:
+  "set (weak_integer_composition_enum i l) = weak_integer_compositions i l"
+proof standard
+  show "set (weak_integer_composition_enum i l) \<subseteq> weak_integer_compositions i l"
+    unfolding weak_integer_compositions_def
+    using weak_integer_composition_enum_length weak_integer_composition_enum_sum_list
+    by auto
+next
+  show "weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)"
+    unfolding weak_integer_compositions_def
+    using weak_integer_composition_enum_correct_aux by auto
+qed
+
+subsubsection"Distinctness"
+
+theorem weak_integer_composition_enum_distinct: "distinct (weak_integer_composition_enum i l)"
+proof(induct rule: weak_integer_composition_enum.induct)
+  case (1 i)
+  then show ?case
+    by simp
+next
+  case (2 i)
+  then show ?case 
+    by simp
+next
+  case (3 i l)
+  have "distinct [h#r . h \<leftarrow> [0..< Suc i], r \<leftarrow> weak_integer_composition_enum (i-h) (Suc l)]"
+    apply(subst Cons_distinct_concat_map_function)
+    using 3 by auto
+  then show ?case by simp
+qed
+
+
+subsubsection"Cardinality"
+
+text \<open>The following is a generalization of the binomial coefficient to multisets. Sometimes it
+is called multiset coefficient. Here we call it "multichoose" \cite{stanleyenumerative}.\<close>
+
+definition multichoose:: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "multichoose" 65) where
+  "n multichoose k = (n + k -1) choose k"
+
+lemma weak_integer_composition_enum_zero: "length (weak_integer_composition_enum 0 (Suc n)) = 1"
+  by(induct n) auto
+
+lemma a_choose_equivalence: "Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k"
+proof -
+  have "m \<ge> k \<Longrightarrow> (\<Sum>x\<leftarrow>[0..< Suc k]. m - x choose (k - x)) = Suc m choose k" for m
+    using sum_choose_diagonal leq_sum_to_sum_list by metis
+  then have 1: "Suc (\<Sum>x\<leftarrow>[0..<k]. (n + k) - x choose (k - x)) = Suc (n + k) choose k"
+    by simp
+
+  have "Suc (\<Sum>x\<leftarrow>[0..<k]. (n + k) - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))"
+    by (metis (no_types, opaque_lifting) Nat.diff_add_assoc2 add.commute binomial_n_0 diff_is_0_eq' nle_le)
+  
+  then show ?thesis using 1 by simp 
+qed
+
+lemma composition_enum_length: "length (weak_integer_composition_enum i n) = n multichoose i"
+  unfolding multichoose_def
+proof(induct i n rule: weak_integer_composition_enum.induct)
+  case (1 i)
+  then show ?case by simp
+next
+  case (2 i)
+  then show ?case by simp
+next
+  case (3 i n)
+
+  then have "x \<in> set [0..< i] \<Longrightarrow>
+    length (weak_integer_composition_enum (i - x) (Suc n)) = n + (i - x) choose (i - x)" for x
+    by simp
+
+  then have ev: "length [h#r . h \<leftarrow> [0..< i], r \<leftarrow> weak_integer_composition_enum (i-h) (Suc n)] =
+     (\<Sum>x\<leftarrow>[0..< i]. n + (i - x) choose (i - x))"
+    using length_concat_map_function_sum_list [of
+      "[0..< i]"
+      "\<lambda>x. (weak_integer_composition_enum (i-x) (Suc n))"
+      "\<lambda>x. n + (i-x) choose (i-x)"
+      "\<lambda>h r. h#r"
+      ] by simp
+
+  have "Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i"
+    using a_choose_equivalence by simp
+
+  then show ?case using weak_integer_composition_enum_zero ev by auto
+qed
+
+theorem weak_integer_compositions_cardinality: "card (weak_integer_compositions n k) = k multichoose n"
+  using weak_integer_composition_enum_correct weak_integer_composition_enum_distinct composition_enum_length
+  distinct_card by metis
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/document/root.bib b/thys/Combinatorial_Enumeration_Algorithms/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/document/root.bib
@@ -0,0 +1,48 @@
+@article{AFPtwel,
+  author  = {Lukas Bulwahn},
+  title   = {The Twelvefold Way},
+  journal = {Archive of Formal Proofs},
+  month   = {December},
+  year    = {2016},
+  note    = {\url{https://isa-afp.org/entries/Twelvefold_Way.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{AFPnumpat,
+  author  = {Lukas Bulwahn},
+  title   = {Cardinality of Number Partitions},
+  journal = {Archive of Formal Proofs},
+  month   = {January},
+  year    = {2016},
+  note    = {\url{https://isa-afp.org/entries/Card_Number_Partitions.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{AFPderan,
+  author  = {Lukas Bulwahn},
+  title   = {Derangements Formula},
+  journal = {Archive of Formal Proofs},
+  month   = {June},
+  year    = {2015},
+  note    = {\url{https://isa-afp.org/entries/Derangements.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@book{stanleyenumerative,
+  title={Enumerative Combinatorics: Volume 1},
+  author={Stanley, R.P.},
+  isbn={9781139505369},
+  series={Cambridge Studies in Advanced Mathematics},
+  year={2011},
+  publisher={Cambridge University Press}
+}
+
+@book{stantonwhite,
+  title={Constructive Combinatorics},
+  author={Dennis Stanton and Dennis White},
+  year={1986},
+  publisher={Springer}
+}
diff --git a/thys/Combinatorial_Enumeration_Algorithms/document/root.tex b/thys/Combinatorial_Enumeration_Algorithms/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/document/root.tex
@@ -0,0 +1,51 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{Combinatorial Enumeration Algorithms}
+\author{Paul Hofmeier and Emin Karayel}
+\maketitle
+
+\begin{abstract}
+Combinatorial objects have configurations which can be enumerated by algorithms,
+but especially for imperative programs, it is difficult to find out if they produce the
+correct output and don't generate duplicates. Therefore, for some of the most common
+combinatorial objects, namely n\_Sequences, n\_Permutations, n\_Subsets, Powerset,
+Integer\_Compositions, Integer\_Partitions, Weak\_Integer\_Compositions, Derangements and Trees, this
+entry formalizes efficient functional programs and verifies their correctness.
+In addition, it provides cardinality proofs for those combinatorial objects.
+Some cardinalities are verified using the enumeration functions and others are
+shown using existing libraries including other AFP entries.
+\end{abstract}
+
+Related books on combinatorics include \cite{stanleyenumerative} and
+\cite{stantonwhite}. 
+Some of the cardinality theorems in this entry are also proved in another 
+AFP entry, The Twelvefold Way \cite{AFPtwel}. 
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/Combinatorial_Enumeration_Algorithms/n_Permutations.thy b/thys/Combinatorial_Enumeration_Algorithms/n_Permutations.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/n_Permutations.thy
@@ -0,0 +1,212 @@
+section "N-Permutations"
+
+theory n_Permutations
+  imports
+    "HOL-Combinatorics.Multiset_Permutations"
+    Common_Lemmas
+    "Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics"
+begin
+subsection"Definition"
+
+definition n_permutations :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set" where
+  "n_permutations A n = {xs. set xs \<subseteq> A \<and> distinct xs \<and> length xs = n}"
+text "Permutations with a maximum length. They are different from \<open>HOL-Combinatorics.Multiset_Permutations\<close>
+because the entries must all be distinct."
+text "Cardinality: \<open>'falling factorial' (card A) n\<close>"
+text "Example: \<open>n_permutations {0,1,2} 2 = {[0,1], [0,2], [1,0], [1,2], [2,0], [2,1]}\<close>"
+
+lemma "permutations_of_set A \<subseteq> n_permutations A (card A)"
+  by (simp add: length_finite_permutations_of_set n_permutations_def permutations_of_setD subsetI)
+
+
+subsection"Algorithm"
+(*algorithm for permutations with arbitrary length exists in HOL-Combinatorics.Multiset_Permutations*)
+fun n_permutation_enum :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list list" where
+  "n_permutation_enum xs 0 = [[]]"
+| "n_permutation_enum xs (Suc n) = [x#r . x \<leftarrow> xs, r \<leftarrow> n_permutation_enum (remove1 x xs) n]"
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+lemma n_permutation_enum_subset: "ys \<in> set (n_permutation_enum xs n) \<Longrightarrow> set ys \<subseteq> set xs "
+proof(induct n arbitrary: ys xs)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  obtain x where o1: "x\<in>set xs" and o2: " ys \<in> (#) x ` set (n_permutation_enum (remove1 x xs) n)"
+    using Suc by auto
+
+  have "y \<in> set (n_permutation_enum (remove1 x xs) n) \<Longrightarrow> set y \<subseteq> set xs" for y
+    using Suc set_remove1_subset by fast
+    
+  then show ?case using o1 o2
+    by fastforce
+qed
+
+lemma n_permutation_enum_length: "ys \<in> set (n_permutation_enum xs n) \<Longrightarrow> length ys = n"
+  by (induct n arbitrary: ys xs) auto
+
+lemma n_permutation_enum_elem_distinct: "distinct xs \<Longrightarrow> ys \<in> set (n_permutation_enum xs n) \<Longrightarrow> distinct ys"
+proof (induct n arbitrary: ys xs)
+  case 0
+  then show ?case 
+    by simp
+next
+  case (Suc n)
+  then obtain z zs where o: "ys = z # zs"
+    by auto
+  from this Suc have t: "zs \<in> set (n_permutation_enum (remove1 z xs) n)"
+    by auto
+
+  then have "distinct zs"
+    using Suc distinct_remove1 by fast
+
+  also have "z \<notin> set zs"
+    using o t n_permutation_enum_subset Suc by fastforce
+
+  ultimately show ?case
+    using o by simp
+qed
+
+lemma n_permutation_enum_correct1: "distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n"
+  unfolding n_permutations_def
+  using n_permutation_enum_subset n_permutation_enum_elem_distinct n_permutation_enum_length
+  by fast
+
+lemma n_permutation_enum_correct2: "ys \<in> n_permutations (set xs) n \<Longrightarrow> ys \<in> set (n_permutation_enum xs n)"
+proof(induct n arbitrary: xs ys)
+  case 0
+  then show ?case unfolding n_permutations_def by simp
+next
+  case (Suc n)
+  show ?case proof(cases ys)
+    case Nil
+    then show ?thesis using Suc
+      by (simp add: n_permutations_def) 
+  next
+    case (Cons z zs)
+
+    have z_in: "z \<in> set xs"
+      using Suc Cons unfolding n_permutations_def by simp
+    
+    have 1: "set zs \<subseteq> set xs"
+      using Suc Cons unfolding n_permutations_def by simp
+
+    have 2: "length zs = n"
+      using Suc Cons unfolding n_permutations_def by simp
+
+    have 3: "distinct zs"
+      using Suc Cons unfolding n_permutations_def by simp
+
+    show ?thesis proof(cases "z \<in> set zs")
+      case True
+      then have "zs \<in> set (n_permutation_enum (remove1 z xs) n)" 
+        using Suc Cons unfolding n_permutations_def by auto
+      then show ?thesis
+        using True Cons z_in by auto
+    next
+      case False
+      then have "x \<in> set zs \<Longrightarrow> x \<in> set (remove1 z xs)" for x
+        using 1 by(cases "x = z") auto
+
+      then have "zs \<in> n_permutations (set (remove1 z xs)) n"
+        unfolding n_permutations_def using 2 3 by auto
+      then have "zs \<in> set (n_permutation_enum (remove1 z xs) n)"
+        using Suc by simp
+      then have "\<exists>x\<in>set xs. z # zs \<in> (#) x ` set (n_permutation_enum (remove1 x xs) n)"
+        unfolding image_def using z_in by simp
+      then show ?thesis
+        using False Cons by simp
+    qed
+  qed 
+qed
+
+theorem n_permutation_enum_correct: "distinct xs \<Longrightarrow> set (n_permutation_enum xs n) = n_permutations (set xs) n"
+proof standard
+  show "distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n"
+    by (simp add: n_permutation_enum_correct1)
+next
+  show "distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)"
+    by (simp add: n_permutation_enum_correct2 subsetI)
+qed
+
+
+subsubsection"Distinctness"
+
+theorem n_permutation_distinct: "distinct xs \<Longrightarrow> distinct (n_permutation_enum xs n)"
+proof(induct n arbitrary: xs)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  let ?f = "\<lambda>x. (n_permutation_enum (remove1 x xs) n)"
+  from Suc have "distinct (?f x)" for x
+    by simp
+
+  from this Suc show ?case
+    by (auto simp: Cons_distinct_concat_map_function_distinct_on_all [of ?f xs])
+qed
+
+
+subsubsection"Cardinality"
+thm card_lists_distinct_length_eq
+theorem "finite A \<Longrightarrow> card (n_permutations A n) = ffact n (card A)"
+  unfolding n_permutations_def using card_lists_distinct_length_eq
+  by (metis (no_types, lifting) Collect_cong) 
+
+
+
+subsection"\<open>n_multiset\<close> extension (with remdups)"
+
+definition n_multiset_permutations :: "'a multiset \<Rightarrow> nat \<Rightarrow> 'a list set" where
+  "n_multiset_permutations A n = {xs. mset xs \<subseteq># A \<and> length xs = n}"
+
+fun n_multiset_permutation_enum :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list list" where
+  "n_multiset_permutation_enum xs n = remdups (n_permutation_enum xs n)"
+
+lemma "distinct (n_multiset_permutation_enum xs n)"
+  by auto
+
+lemma n_multiset_permutation_enum_correct1:
+  "mset ys \<subseteq># mset xs \<Longrightarrow> ys \<in> set (n_permutation_enum xs (length ys))" 
+proof(induct "ys" arbitrary: xs)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons y ys)
+  then have "y \<in> set xs"
+    by (simp add: insert_subset_eq_iff)
+  moreover have "ys \<in> set (n_permutation_enum (remove1 y xs) (length ys))"
+    using Cons by (simp add: insert_subset_eq_iff)
+  ultimately show ?case
+    using Cons by auto
+qed
+
+lemma n_multiset_permutation_enum_correct2:
+  "ys \<in> set (n_permutation_enum xs n) \<Longrightarrow> mset ys \<subseteq># mset xs"
+proof(induct "n" arbitrary: xs ys)
+  case 0
+  then show ?case
+    by simp
+next
+  case (Suc n)
+  then show ?case
+    using insert_subset_eq_iff mset_remove1 by fastforce
+qed
+
+lemma n_multiset_permutation_enum_correct:
+  "set (n_multiset_permutation_enum xs n) = n_multiset_permutations (mset xs) n"
+  unfolding n_multiset_permutations_def
+proof(standard)
+  show "set (n_multiset_permutation_enum xs n) \<subseteq> {xsa. mset xsa \<subseteq># mset xs \<and> length xsa = n}"
+    by (simp add: n_multiset_permutation_enum_correct2 n_permutation_enum_length subsetI) 
+next
+  show "{xsa. mset xsa \<subseteq># mset xs \<and> length xsa = n} \<subseteq> set (n_multiset_permutation_enum xs n)"
+    using n_multiset_permutation_enum_correct1 by auto
+qed
+
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/n_Sequences.thy b/thys/Combinatorial_Enumeration_Algorithms/n_Sequences.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/n_Sequences.thy
@@ -0,0 +1,91 @@
+section "N-Sequences"
+
+theory n_Sequences
+  imports
+    "HOL.List"
+    Common_Lemmas
+begin
+
+subsection"Definition"
+
+definition n_sequences :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set" where
+  "n_sequences A n = {xs. set xs \<subseteq> A \<and> length xs = n}"
+
+text"Cardinality: \<open>card A ^ n\<close>"
+text"Example: \<open>n_sequences {0, 1} 2 = {[0,0], [0,1], [1,0], [1,1]}\<close>"
+
+subsection"Algorithm"
+                            
+fun n_sequence_enum :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list list" where
+  "n_sequence_enum xs 0 = [[]]"
+| "n_sequence_enum xs (Suc n) = [x#r . x \<leftarrow> xs, r \<leftarrow> n_sequence_enum xs n]"
+
+
+text "An enumeration of n-sequences already exists: \<open>n_lists\<close>. This part of this AFP entry is mostly
+to establish the patterns used in the more complex combinatorial objects."
+
+lemma "set (n_sequence_enum xs n) = set (List.n_lists n xs)"
+  by(induct n) auto
+
+thm set_n_lists
+
+subsection"Verification"
+
+subsubsection"Correctness"
+
+theorem n_sequence_enum_correct: 
+  "set (n_sequence_enum xs n) = n_sequences (set xs) n"
+proof standard
+  show "set (n_sequence_enum xs n) \<subseteq> n_sequences (set xs) n"
+    unfolding n_sequences_def by (induct n) auto+
+next
+  show "n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)"
+  proof(induct n)
+    case 0
+    then show ?case
+      unfolding n_sequences_def by auto
+  next
+    case (Suc n)
+    
+    have "\<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set x \<subseteq> set xs; length x = Suc n\<rbrakk>
+      \<Longrightarrow> \<exists>xa\<in>set xs. x \<in> (#) xa ` set (n_sequence_enum xs n)" for x
+      unfolding n_sequences_def by (cases x) auto
+      
+    from this Suc show ?case
+      unfolding n_sequences_def by auto
+  qed
+qed
+
+subsubsection"Distinctness"
+
+theorem n_sequence_enum_distinct: 
+  "distinct xs \<Longrightarrow> distinct (n_sequence_enum xs n)"
+  by (induct n) (auto simp: Cons_distinct_concat_map)
+
+subsubsection"Cardinality"
+
+lemma n_sequence_enum_length: 
+  "length (n_sequence_enum xs n) = (length xs) ^ n "
+  by(induct n arbitrary: xs) (auto simp: length_concat_map) 
+
+text"of course \<open>card_lists_length_eq\<close> can directly proof it
+but we want to derive it from \<open>n_sequence_enum_length\<close>"
+thm card_lists_length_eq
+
+theorem n_sequences_card:
+  assumes "finite A"
+  shows "card (n_sequences A n) = card A ^ n"
+proof -
+  obtain xs where set: "set xs = A" and dis: "distinct xs"
+    using assms finite_distinct_list by auto
+  have "length (n_sequence_enum xs n) = (length xs) ^ n"
+    using n_sequence_enum_distinct n_sequence_enum_length by auto
+  then have "card (set (n_sequence_enum xs n)) = card (set xs) ^ n"
+    by (simp add: dis distinct_card n_sequence_enum_distinct)
+  then have "card (n_sequences (set xs) n) = card (set xs) ^ n"
+    by (simp add: n_sequence_enum_correct)
+  then show "card (n_sequences A n) = card A ^ n"
+    using set by simp
+qed
+
+end
diff --git a/thys/Combinatorial_Enumeration_Algorithms/n_Subsets.thy b/thys/Combinatorial_Enumeration_Algorithms/n_Subsets.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorial_Enumeration_Algorithms/n_Subsets.thy
@@ -0,0 +1,233 @@
+section "N-Subsets"
+
+theory n_Subsets
+  imports
+    Common_Lemmas
+    "HOL-Combinatorics.Multiset_Permutations"
+    Filter_Bool_List
+begin
+
+subsection"Definition"
+
+definition n_subsets :: "'a set \<Rightarrow> nat \<Rightarrow> 'a set set" where
+  "n_subsets A n = {B. B \<subseteq> A \<and> card B = n}"
+
+text "Cardinality: \<open>binomial (card A) n\<close>"
+text "Example: \<open>n_subsets {0,1,2} 2 = {{0,1}, {0,2}, {1,2}}\<close>"
+
+subsection"Algorithm"
+
+fun n_bool_lists :: "nat \<Rightarrow> nat \<Rightarrow> bool list list" where
+  "n_bool_lists n 0 = (if n > 0 then [] else [[]])"
+| "n_bool_lists n (Suc x) = (if n = 0 then [replicate (Suc x) False]
+    else if n = Suc x then [replicate (Suc x) True]
+    else if n > x then []
+    else [False#xs . xs \<leftarrow> n_bool_lists n x] @ [True#xs . xs \<leftarrow> n_bool_lists (n-1) x])"
+
+fun n_subset_enum :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list list" where
+  "n_subset_enum xs n = [(filter_bool_list bs xs) . bs \<leftarrow> (n_bool_lists n (length xs))]"
+
+subsection"Verification"
+                        
+subsubsection"n-bool-lists"
+
+lemma n_bool_lists_True_count: "xs \<in> set (n_bool_lists n x) \<Longrightarrow> count_list xs True = n"
+ by (induct x arbitrary: xs n) (auto split: if_splits simp: count_list_replicate)
+
+lemma n_bool_lists_length: "xs \<in> set (n_bool_lists n x) \<Longrightarrow> length xs = x"
+  by (induct x arbitrary: xs n) (auto split: if_splits)
+
+lemma n_bool_lists_distinct: "distinct (n_bool_lists n x)"
+proof(induct x arbitrary: n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc x)
+  then show ?case
+    using distinct_map by fastforce
+qed
+
+lemma replicate_True_not_False: "count_list ys True = 0 \<longleftrightarrow> ys = replicate (length ys) False"
+  using count_list_zero_not_elem count_list_full_elem count_list_length_replicate by fastforce
+
+lemma n_bool_lists_correct_aux:
+  "length xs = x \<Longrightarrow> count_list xs True = n \<Longrightarrow> xs \<in> set (n_bool_lists n x)"
+proof(induct x arbitrary: n xs)
+  case 0
+  then show ?case by auto
+next
+  case (Suc x)
+   show ?case proof(cases "n = 0")
+    case True
+    then show ?thesis
+      using Suc True replicate_True_not_False by auto
+  next
+    case c1: False
+    then show ?thesis proof(cases "n = Suc x")
+      case True
+      then have "xs = True # replicate x True "
+        using Suc.prems count_list_length_replicate replicate_Suc by metis
+      then show ?thesis
+        using True by simp
+    next
+      case c2: False
+      then show ?thesis proof(cases "n > x")
+        case True
+        then have "xs = []"
+          using Suc.prems c2 count_le_length by (metis Suc_lessI linorder_not_less)
+        then show ?thesis
+          using Suc by auto
+      next
+        case c3: False
+        then show ?thesis proof (cases xs)
+          case Nil
+          then show ?thesis
+            using Suc.prems(1) by auto 
+        next
+          case (Cons y ys)
+          then show ?thesis proof (cases y)
+            case True
+            then show ?thesis using Suc c1 c2 c3 Cons
+              by simp 
+          next
+            case False 
+            then show ?thesis using Suc c1 c2 c3 Cons
+              by simp
+          qed 
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma n_bool_lists_correct: "set (n_bool_lists n x) = {xs. length xs = x \<and> count_list xs True = n}"
+proof(standard)
+  show "set (n_bool_lists n x) \<subseteq> {xs. length xs = x \<and> count_list xs True = n}"
+  proof(cases x)
+    case 0
+    then show ?thesis by simp
+  next
+    case (Suc x)
+    then show ?thesis using n_bool_lists_True_count n_bool_lists_length
+      by blast
+  qed
+next
+  show "{xs. length xs = x \<and> count_list xs True = n} \<subseteq> set (n_bool_lists n x)"
+    using n_bool_lists_correct_aux by auto
+qed
+
+
+subsubsection"Correctness"
+
+lemma n_subset_enum_correct_aux1:
+  "\<lbrakk>distinct xs; length ys = length xs\<rbrakk>
+    \<Longrightarrow> set (filter_bool_list ys xs) \<in> n_subsets (set xs) (count_list ys True)"
+  unfolding n_subsets_def
+  by (auto simp: filter_bool_list_card filter_bool_list_elem)
+
+lemma n_subset_enum_correct_aux2:
+  "distinct xs \<Longrightarrow> n_subsets (set xs) n \<subseteq> set (map set (n_subset_enum xs n))"
+  unfolding n_subsets_def
+  by (auto simp: n_bool_lists_correct image_def filter_bool_list_exist_length_card_True)
+
+theorem n_subset_enum_correct:
+  "distinct xs \<Longrightarrow> set (map set (n_subset_enum xs n)) = n_subsets (set xs) n"
+proof(standard)
+  show "distinct xs \<Longrightarrow> set (map set (n_subset_enum xs n)) \<subseteq> n_subsets (set xs) n"
+    using n_subset_enum_correct_aux1 n_bool_lists_correct by auto
+next
+  show "distinct xs \<Longrightarrow> n_subsets (set xs) n \<subseteq> set (map set (n_subset_enum xs n))"
+    using n_subset_enum_correct_aux2 by auto
+qed
+
+subsubsection"Distinctness"
+
+theorem n_subset_enum_distinct_elem:
+  "distinct xs \<Longrightarrow> ys \<in> set (n_subset_enum xs n) \<Longrightarrow> distinct ys"
+  by(cases "length xs < n") (auto simp: filter_bool_list_distinct)
+
+theorem n_subset_enum_distinct: "distinct xs \<Longrightarrow> distinct (n_subset_enum xs n)"
+  by(auto simp: distinct_map n_bool_lists_distinct inj_on_def filter_bool_list_inj_aux n_bool_lists_length)
+
+subsubsection"Cardinality"
+
+text \<open>Cardinality of @{term "n_subsets"} is already shown in @{thm [source] "Binomial.n_subsets"}.\<close>
+
+subsection "Alternative using Multiset permutations"
+
+text "It would be possible to define \<open>n_bool_lists\<close> using \<open>permutations_of_multiset\<close> with the
+following definition:"
+
+fun n_bool_lists2 :: "nat \<Rightarrow> nat \<Rightarrow> bool list set" where
+  "n_bool_lists2 n x = (if n > x then {}
+    else permutations_of_multiset (mset (replicate n True @ replicate (x-n) False)))"
+
+subsection"\<open>mset_count\<close>"
+
+text"Correspondence between \<open>count_list\<close> and \<open>count (mset xs)\<close> and transfer of a few results
+for multisets to lists."
+
+lemma count_list_count_mset: "count_list ys T = n \<Longrightarrow> count (mset ys) T = n"
+  by(induct ys arbitrary: n) auto
+
+lemma count_mset_count_list: "count (mset ys) T = n \<Longrightarrow> count_list ys T = n"
+  by(induct ys arbitrary: n) auto
+
+lemma count_mset_replicate_aux1:
+  "\<lbrakk>\<not> x < n; mset ys = mset (replicate n True) + mset (replicate (x - n) False)\<rbrakk>
+    \<Longrightarrow> count (mset ys) True = n"
+  by (auto simp: count_list_count_mset count_mset)
+
+lemma  count_mset_replicate_aux2: 
+  assumes "\<not> length xs < count_list xs True"
+  shows "mset xs = mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)"
+proof -
+  have "count_list xs B =
+         count_list (replicate (count_list xs True) True) B + count_list (replicate (length xs - count_list xs True) False) B"
+    for B
+  proof(cases B)
+    case True
+    then show ?thesis
+      by (simp add: count_list_replicate)
+  next
+    case False
+
+    have "count_list xs False = count_list (replicate (length xs - count_list xs True) False) False"
+      by (metis count_list_True_False count_list_replicate diff_add_inverse)
+      
+    from this False show ?thesis
+      using assms by auto 
+  qed
+
+  then have "count (mset xs) B =
+         count (mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)) B"
+    for B
+    by (metis count_mset_count_list count_union)
+  
+  then show "mset xs = mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)"
+    using multiset_eqI by blast
+qed
+
+lemma n_bool_lists2_correct: "set (n_bool_lists n x) = n_bool_lists2 n x"
+proof(standard)
+  have "\<lbrakk>\<not> length ys < count_list ys True; x = length ys; n = count_list ys True\<rbrakk>
+          \<Longrightarrow> ys \<in> permutations_of_multiset
+                     (mset (replicate (count_list ys True) True) + mset (replicate (length ys - count_list ys True) False))"
+          for ys
+    using count_mset_replicate_aux2 permutations_of_multisetI by blast
+  
+  then show "set (n_bool_lists n x) \<subseteq> n_bool_lists2 n x"
+    unfolding n_bool_lists_correct
+    by (auto simp: count_le_length leD)
+next
+  have "\<lbrakk>\<not> x < n; ys \<in> permutations_of_multiset (mset (replicate n True) + mset (replicate (x - n) False))\<rbrakk>
+          \<Longrightarrow> count (mset ys) True = n " for ys
+    using count_mset_replicate_aux1 permutations_of_multisetD by blast
+  then have "\<lbrakk>\<not> x < n; ys \<in> permutations_of_multiset (mset (replicate n True) + mset (replicate (x - n) False))\<rbrakk>
+          \<Longrightarrow>  count_list ys True = n " for ys
+    by (simp add: count_list_count_mset) 
+  then show "n_bool_lists2 n x \<subseteq> set (n_bool_lists n x)" unfolding n_bool_lists_correct 
+    by (auto simp: length_finite_permutations_of_multiset)
+qed
+
+end
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,710 +1,711 @@
 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
 Ackermanns_not_PR
 Actuarial_Mathematics
 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
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 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
 Boolos_Curious_Inference
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRYSTALS-Kyber
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 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
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
+Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DPRM_Theorem
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 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
 Hahn_Jordan_Decomposition
 Hales_Jewett
 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
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 IsaNet
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Knights_Tour
 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
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Maximum_Segment_Sum
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multiset_Ordering_NPC
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 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
 Number_Theoretic_Transform
 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
 Package_logic
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Padic_Field
 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
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 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
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 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
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 SCC_Bloemen_Sequential
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sophomores_Dream
 Solidity
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 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
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL