fact: Definition interpret (φ ψ0 ψ1: valuation) (X: config) : option term := match X with | (A, B, x) => descend (ascend ψ0 ψ1 (φ (embed ([], [], x))) A) B end.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool