File ProofSystemSoundness

File Sorts_ProofSystem

File Subseteq_ProofSystem

File ContextualImplication

File Definedness_ProofSystem

File ModelExtension

File Sorts_Syntax

File Bool_Syntax

File Bool_ProofSystem

File ProductSort

File Definedness_Syntax

• Definedness

File SumSort_Syntax

File Bool_Semantics

File DeductionTheorem

File RecursiveSymbol

File ProductSortWithLookup

File Sorts_Semantics

File Nat_Syntax

File ProductSort_ProofSystem

File Definedness_Semantics

File FOEquality_ProofSystem

File DefaultModels

File PatternCtxApplicationCtx

File ApplicationCtxSubstitution

File FreshnessSubstitution

File FreshnessApplicationCtx

File Freshness

File SyntacticConstruct

• General substitutions
• Substitution type classes for the different syntacical cateories

File Syntax

File extralibrary

• Module extralibrary: library functions, theorems, and tactics
  • Arithmetic
  • Peano induction.

File stdpp_ext

File Surj

File Lattice

File IndexManipulation

File GenericModel

File OpmlPattern

File OpmlSignature

File OpmlAmlRelSpec

File OpmlModel

File OpmlExamples

File KPreludeSignatures

File Logic

File wftactics

File ProofSystem

File NamedAxioms

File FreshnessManager

File TEST_LocallyNameless

File TEST_proofmode_proof_size

File TEST_ProofMode_relative_completeness

File TEST_proofmode_example

File Semantics

• • Matching Logic Semantics

File StringSignature

File DerivedOperators_Semantics

File ProofInfo

File Propositional

File Revert_size

File Complex

File Rewrite

File Extractor

File Firstorder

File tutorial

File monotonic

File SumSort_ProofSystem

File Nat_ProofSystem

File Unification

File ProofModePattern

File PrePredicate

File Pattern

File ApplicationContext

File Propositional

File Misc

File Basics

File FixPoint

File Firstorder

File Reshaper

File MLPM

File ModelIsomorphism

File DerivedOperators_Syntax

File BasicProofSystemLemmas

File Substitution

File Signature

File PatternContext

File FixpointReasoning