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
  • Utilities
    • Propositions Satisfing XM
    • Variants of Constructive Choice for nat
    • Strictly Monotone Functions
    • Decidability of Bounded Quantification
    • Languages
    • Collections of other Lemmas
  • Finite Sets
  • Strings and Nonempty Strings
    • Basic Operations on Nonempty Strings
    • Conversion between Strings and Nonempty Strings
    • Decidability of Quantification over Strings of Bounded Length
    • Duplicates in Strings over Finite Types
  • Finite Semigroups
    • Idempotent Elements
  • Sequences
    • Abstract Sequences
    • Abstract Sequences with More Operations
      • Constant Sequence
      • Map and Zip
      • Zipping Finitely many Abstract Sequences
    • Sequences nat -> X
      • More Operations on Sequences
      • Flattening a Sequence of Nonempty Strings
      • Sequences Satisfying a Predicate Infinitely Often
      • Factorizing a Sequence by a Predicate that Holds Infinitely Often
      • ω-Iteration
      • Cutting a Seqs into Strings of Given Length
    • Languages (or Predicates) of Sequences
  • Ultimately Periodic (UP) Sequences
    • Basic Operations
    • Zipping Two UP Sequences
  • Nondeterminisic Finite Automata (NFAs)
    • Facts for Runs on Strings and Sequences
    • Relations ===> and =!=>
  • NFAs Accepting Regular Languages
    • Definition of Acceptance
    • NFAs Accepting Exactly One String
    • NFAs Accepting Symbols Satisfying a Predicate
    • NFAs Accepting Strings of Given Color in a Semigroup
  • Büchi Automata
    • Büchi Acceptance
    • Quasi Runs
    • Matches
    • Operations Implementing Closure Properties
      • Image and Preimage
      • Union
      • Intersection
      • ω-Iteration of a Regular Language
      • Prepending Regular Languages
    • Properties of UP Sequences
  • Ramseyan Factorizations
    • Definition of Ramseyan Factorizations
    • Ramseyan Factorizations of Idempotent Color
    • UP Sequences have Ramseyan Factorizations
    • Ramseyan Factorizations for Semigroup Homomorphisms
    • RF Implies IP and MP
  • Equivalence of RF and Additive Ramsey Theorem (RA)
    • Conversion of Factorisations to Infinite Boolean Sequences
    • Equivalence of RF and RA
  • Complementation of Büchi Automata
    • Semigroup of Colors
    • Kinds of Sequences
    • The Complement Automaton
  • Minimal S1S
    • Translation to Abstract Automata
    • Satisfiability is Deciable and Satisfaction satisfies XM
    • Büchi Automata as Abstract Automata
      • Operations on Büchi Automata
      • Instances for AS and UP semantics
    • Properties of Minimal S1S using Büchi Automata
  • Full S1S
    • Reduction from Full S1S to Minimal S1S
      • Singleton Sets
      • Reduction to Minimal S1S using Interpretations as Functions
      • Reduction to Minimal S1S using Interpretations as Sequences
    • Results for Full S1S
    • Derived Connectives and Formulas for S1S
    • Classical Reasoning given FX
  • Ramseyan Pigeonhole Principle
    • The Merging Relation
    • RPc holds
    • RP implies IP
    • Equivalence of RP and RF
  • Necessity of RF
    • AC (Existence of Complement Automata) is Equivalent to RF
    • AU (UP Equivalent Automata are Equivalent) is Equivalent to AC
    • FX (S1S Satisfaction satisfies XM) Implies RP
      • Encoding that a Substring has a given Color
      • Encoding of Merging and RP
    • AX (Büchi Acceptance Satisfies XM) Implies RP
      • Basic Automata for the Predicates
      • P1 Satisfies XM
      • P2 Satisfies XM
      • P3 Satisfies XM
Generated by coqdoc and improved with CoqdocJS