def MeTTaIL.hasRedex (p : Presentation) : AST → Bool

Whether a base rewrite applies anywhere in the term: at the root, or recursively in a sexp argument or a Subst component.

Equations

• MeTTaIL.hasRedex p (MeTTaIL.AST.var x_1) = !(MeTTaIL.baseReducts p (MeTTaIL.AST.var x_1)).isEmpty
• MeTTaIL.hasRedex p (MeTTaIL.AST.sexp l args) = (!(MeTTaIL.baseReducts p (MeTTaIL.AST.sexp l args)).isEmpty || MeTTaIL.hasRedexList p args)
• MeTTaIL.hasRedex p (b.subst r v) = (!(MeTTaIL.baseReducts p (b.subst r v)).isEmpty || MeTTaIL.hasRedex p b || MeTTaIL.hasRedex p r)

def MeTTaIL.hasRedexList (p : Presentation) : List AST → Bool

Whether any element of the list has a redex.

Equations

• MeTTaIL.hasRedexList p [] = false
• MeTTaIL.hasRedexList p (a :: as) = (MeTTaIL.hasRedex p a || MeTTaIL.hasRedexList p as)

theorem MeTTaIL.oneStep_isSome_eq_hasRedex (p : Presentation) (t : AST) : (oneStep p t).isSome = hasRedex p t

Completeness: the executable reducer succeeds exactly when a base redex exists.

theorem MeTTaIL.oneStepList_isSome_eq_hasRedexList (p : Presentation) (args : List AST) : (oneStepList p args).isSome = hasRedexList p args

List version of completeness.

theorem MeTTaIL.isNormal_iff_hasRedex_false (p : Presentation) (t : AST) : IsNormal p t ↔ hasRedex p t = false

IsNormal means exactly that no base rewrite applies anywhere in the term.