Project Page Index Table of Contents
  • External Libraries
    • Proofs and definitions obtained from external sources
      • De Morgan laws
      • Lists
        • Decidability laws for lists
        • Membership
        • Disjointness
        • Inclusion
        • Setoid rewriting with list inclusion and list equivalence
        • Equivalence
        • Filter
        • Element removal
        • Cardinality
        • Duplicate-free lists
        • Power lists
    • Basic definitions of decidablility and Functions
      • Definition of useful tactics
      • Injectivity and surjectivity
      • Pure predicates
      • Proofs about equality
      • Decidablility of equality: Instance declarations
      • Functions creating an eqType from a type or a value
        • Definitions of corresponding eqTypes
        • Useful notations for cross product and option eqTypes
        • toeqType produces canonical instances
      • Definition of useful functions
      • Basic lemmas about functions
      • Cardinality Lemmas for lists
      • Various helpful Lemmas
    • Formalisation of finite types using canonical structures and type classes
      • Definition of finite Types
      • Properties of decidable Propositions
      • Completeness Lemmas for lists of basic types
        • Declaration of finTypeCs for base types as instances of the type class
        • Canonical structures declarations for finTypes of base types
        • Correctness of finTypes for basic types
        • Completeness lemma and Canonical Structure definition for cartesian product and option types
        • Definition of the actual finTypes for option types and cross products
        • Correctness proofs for the cross product and option type finTypes from above
      • Tests and Examples
        • Tests whether Type inference works correctly
        • Examples depending on type classes
      • Definition of sum Type as finType
      • Dupfreeness
      • Definition of vectors (extensional/ set theoretic functions)
        • Conversion between vectors and functions
      • Proofs about Cardinality
      • Dependent pairs
      • Subtypes
      • finTypes from Lists
      • Finite Closure Iteration
    • Proofs about DFA as a test for the finType library
      • Conversion between Props and bools
      • Definition of the alphabet, words and dfa
      • Reachability
      • Reach (set of all reachable states)
      • Nondeterministic finite automata (NFA)
      • Concatenation of two regular languages
      • Kleene Operator
  • Languages
  • Sequences
    • Basic Operations on Sequences
    • An element occuring infinitely often in a Sequence
    • Pointwise equiality of sequences
    • Decidability of bounded quantifiers on Sequences
  • Strings
    • Equality Relation on Strings
    • Simple Operations on Strings
    • Equality of results of some string operations
    • Languages of Strings
  • Strictly Monotone Sequences on nat
  • Operations on Sequences
    • Finding the next position at which a predicate holds in a sequence
    • Infinite Filter
    • History Filter
    • Infinite Concattenation
    • Composing String and Sequence Languages
      • String Languageω
      • Prepending a String on a Sequence Language
  • Nondeterminisic Finite Automata
    • Facts for valid Strings and Sequences of NFAs
      • Extensionality facts
      • Manipulations of valid paths and runs
      • Facts about Connectivity
      • Concatting and Splitting of Paths
    • String Language of an NFA
    • Decidability of Connectivity in NFAs
    • Necessary Assumption to formalize Buechi automata
      • Assumption 1: Sequences over Finite Types
      • Assumption 2: Given a XM equivalence relation with finite index on X, then for every
  • Buechi Acceptance for Sequences on NFAs
    • Simple Example: NFA recognizing the Buechi language (ab)^00
    • NFA with empty Buechi language
    • Closure under Union of Buechi languages
      • Definition of the union automaton
      • Proving Correctness
    • Closure under Intersection of Buechi languages
      • Definition of the intersection automaton
      • Show that given an accepting run of both automata, the intersection automaton accepts the sequence too.
        • aut1 accepts all sequences accepted by intersection_aut
        • aut2 acceepts all sequences accepted by intersection_aut
      • intersection_aut accepts all sequences accepted by aut1 and aut 2
  • Some Utilities
    • Finite type {n|n<=k}
      • Cardinality is S k
      • Decisions for this Type
    • Interpretation of {n|n<=k} as Prefix of Sequences
    • Duplicates in a String of a Finite Type
    • Maximum of finitely many Numbers
    • Two list are equal if nth_error is equal for all n
    • Constructive Choice for nat
  • Decidability of Buechi Language Emptyness
    • Decidability of Final Coaccessibility
    • Trimming of NFAs w.r.t. Buechi Languages
      • Trim automaton recognizes the same language
      • Decidability of language emptiness of a trim automaton
      • Informative Decision of Buechi Language Emptiness
  • Constructions on NFAs
    • General Facts of Infinite Concattenation and Prepending of Runs and Sequences on NFAs
      • Facts that Infinite Concattenation or Prepending are Valid and Buechi Final
      • Facts showing that Composing the Sequence carry over to the Run
  • Normalization of NFAs regarding String Languages
  • ω-Iteration of a NFA String Language
  • Prepending a String on a Buechi Language
  • Complementation of Buechi Languages
    • Equivalence Relation on Strings
      • Facts about ===> and =!=> for Concattenation
      • Definition of the Equivalence Relation ~~
      • Finite Type for Equivalence Classes of ~~
        • Equivalence classes can be recognized by NFAs
    • Compatibility of V o W ^00 with L_B aut
    • Totality V o W^00
      • Classical Proof using Ramsey
      • Equivalence Relation on indices of a Sequence w
      • Excluded Middle for ~~#
      • ~~# is of Finite Index
      • Construction of V and W
    • Definition of the Complement Buechi NFA
      • Correctness Lemmata
    • Decision Corallaries
Generated by coqdoc and improved with CoqdocJS