Cyclic Terms

In this file, we define when a PreGroundTerm is cyclic. This is exactly the case, when a function symbol contains twice in a nested fashion. For example $h(d, f(g(f(c))))$ is cyclic but $h(f(d), f(c))$ is not. Cyclic terms are mainly used to define MFA later.

The main result in this file then is cyclic_of_depth_too_big. That is, if a term exceeds a certain depth, then it is necessarily cyclic. This of course requires that only finitely many different function symbols are usable.

@[irreducible]

def PreGroundTerm.cyclic {sig : Signature} [DecidableEq sig.V] : FiniteTree (SkolemFS sig) sig.C → Bool

A PreGroundTerm is cyclic if one of its children contains_func the function symbol of the term or if one of its children is already cyclic. Constants are never cyclic.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.cyclic (FiniteTree.leaf a) = false

theorem PreGroundTerm.cyclic_of_depth_too_big {sig : Signature} [DecidableEq sig.V] [DecidableEq sig.C] (t : PreGroundTerm sig) (funcs : List (SkolemFS sig)) (nodup : funcs.Nodup) (funcs_in_t_from_funcs : ∀ (func : SkolemFS sig), func ∈ FiniteTree.innerLabels t → func ∈ funcs) : funcs.length + 2 ≤ FiniteTree.depth t → cyclic t = true

Consider a (deduplicated) list of possible function symbols and a term. If the depth of the term is at least the number of function symbols + 2, then the term must be cyclic.