Project Page Index Table of Contents
  • Base Library for ICL
    • Boolean propositions and decisions
    • Discrete types
    • Lists
      • Decisions for lists
      • Membership
      • Inclusion
      • Setoid rewriting with list inclusion and list equivalence
      • Filter
      • Element removal
  • Names and permutations of names
    • Transpositions
  • Lists
    • Permutations on lists
    • Concat, nth, and map
    • Advanced list functions
    • Lists of natural numbers
    • Construction of Fresh Names Relative to Blocked Names
    • Replacement
  • Ranked trees
    • Definition
    • Action
  • Ranked Nu-trees
    • Definition
    • Depth
    • Names
    • Action
    • Equivariant functions
    • Language of Nu-tree
      • Definition
      • Equivariance
    • Structurally similar nu-trees
  • Equivalences Laws
    • Rho-Renamings
    • Empty bindings
    • Renaming of Nu's
    • Swapping successive Nu's
    • Pushing Nu's
  • Decision Procedure for the Nu-Tree Language
    • Structurally Similar Trees
    • Stronger Similarity predicate
    • Decision procedure
    • Correctness
  • Automaton Model for Nu-trees
    • Decision Procedure for NTA Languages
    • Correctness
    • Generalized Acceptance over Q
    • Generalized Acceptance over Phi
    • No Closure under Nu-Tree Equivalence
Generated by coqdoc and improved with CoqdocJS