Project Page Index Table of Contents
  • Base Library for ICL
    • Boolean propositions and decisions
    • Discrete types
    • Numbers
    • Lists
      • Decisions for lists
      • Membership
      • Disjointness
      • Inclusion
      • Setoid rewriting with list inclusion and list equivalence
      • Filter
      • Element removal
      • Cardinality
      • Duplicate-free lists
      • Power lists
    • Finite inductive predicates
    • Finite closure iteration
  • SAT Solver
    • SAT solver
    • Equivalence
    • Separability
    • Validity
    • Exercises
    • Shallow and deep Embedding
  • Axiomatic Equivalence
  • Strictly sorted lists are identical if they are equivalent
    • Insertion sort
    • Exercises
  • Preliminaries
  • Set Theory
    • Empty set and adjunction
    • Numerals
    • Finite sets
    • Hereditarily finite sets
    • Well-founded sets
    • HFT characterisation of numerals
    • Union
    • Replacement and Separation
      • Description
      • Projections
      • Cartesian products
      • Functions as sets
      • Subsets and XM
    • Diaconescu's Theorem
    • Power
    • Subsets of Finite Sets
    • Towers
    • Ordinals
    • WFT Characterisation of Ordinals
    • Finite Ordinals
    • Cumulative Hierarchy
    • Finite Stages
    • Closures and Infinity
    • Well-Ordering Theorem
    • Regularity
  • Complete Induction for Numbers
  • Well-Orderings on Types
  • Well-Founded Relations
Generated by coqdoc and improved with CoqdocJS