Project Page Index Table of Contents
  • Finite Types Library
    • Proofs and definitions obtained from external sources
      • Lists
    • Basic definitions of decidablility and Functions
    • Formalisation of finite types using canonical structures and type classes
    • Proofs about DFAs and NFAs as a test for the finType library
  • Collection of Basic Definition and Lemmas
    • Languages
    • Constructive Choice for nat
  • Extensions to FinTypes Library
    • Finite type {n|n<=k}
    • Functions and Lemmas for Vectors
  • Sequences and Strings
    • Equivalence of sequences
    • Basic Operations on Sequences
    • Strings as Prefixes
      • Equivalence on Strings
      • Operations on Strings
    • Strictly Monotone Sequences on nat
    • ω-Concattenation
    • ω-Iteration of a String
    • Predicates Satsified Infinitely Often by a Sequence
    • ω-Filter
    • Ultimately Periodic Sequences
    • Sequences over Finite Alphabet
      • Cosntruction of Duplicates
      • Interpretation of {n|n<=k} as Prefix of Sequences
  • Languages of Strings and Sequences
    • Image and Preimage
    • ω-Iteration of a String Languages
    • Prepending a String on a Sequence Language
  • Ramseyan Properties
    • Finite Semigroups
    • Idempotent Elements
    • Equivalence of Additive Ramsey and Ramseyan Factorizations
    • Excluded Middle Implies Ramseyan Factorizations
    • Ramseyan Factorizations Imply Markov's Principle
  • Nondeterminisic Finite Automata
    • Facts for valid Strings and Sequences of NFAs
    • Reachability in NFA
    • Decidability of Reachability in NFAs
  • Regular Languages
    • Normalization of NFAs regarding String Languages
    • Closure Properties of Regular Languages
  • Büchi Automata
    • Büchi Acceptance
    • Decidability of Language Emptiness
    • Closure under Image and Preimage
    • Closure under Union
    • Closure under Intersection
    • ω-Iteration of a Regular Language
    • Closure under Prepending Regular Languages
    • Decidability of word problem for UP Sequences
  • Complementation of Buechi Automata
    • Büchi Equivalence Relation
      • Regularity of Equivalence Classes
    • Compatibility
    • Totality
    • Definition of Complement NFA
  • Admissible Sequence Structures
    • Closure Properties transfer to AS Structures
    • Correctness of Complementation
    • Decision Corallaries
    • Instatiations of AS Structures
      • ω-Structure
      • UP-Structure
  • Monadic Second Order Logic on the Successor Relation
    • Definition of MSO and MSO_0
      • Semantics of MSO_0
      • Semantics of MSO
    • Reduction from MSO to MSO_0
    • Derived Connectives and Formulas for MSO
    • More Connectives and Lemmas assumming Classical Behavior of MSO
    • Special Vector Operations
    • Vector Language of a Formula
    • Translation of Formulas to NFAs
    • Decidability and Classical Behavior of MSO_0 and MSO for AS Structures
    • ω-Structure and UP-Structure
    • Formulas for Covering or Partioning nat
  • Necessity of Additive Ramsey
    • Closure under Complement Implies Ramseyan Factorizations
    • Classical Behavior of S1S Implies Ramseyan Factorizations
    • Summary: Equivalence of AR, RF, BC, BU, and SL
    • Addition: XM Word Problem suffices to derive the IPP
Generated by coqdoc and improved with CoqdocJS