Declare an SMT tuple sort per entry in the argument list. Each sort is defined as a function of the Int N, as the parametric sort TupleN parameterised on X, and a constructor "mkTupleN" with N fields named "tplN_i" for i ranging from 1 to N

Declare a ListX parametric Sort parameterised on X with 2 constructors: * a "nil" constructor * a "cons" constructor with 2 fields: + "head" of sort X + "tail" of sort "(ListX X)"

Construct a ListX from a '[Sting]' by chaining the appropriate sequence of "cons" and a "nil" adequately qualified

Define the "andReduce" SMT function operating on a "(ListX Bool)", reducing it using "and"

Define the "impliesReduce" SMT function operating on a "(ListX Bool)", reducing it using "=>" (implication)

Define the "init", "allDifferent" and "distinctFrom" family of functions on ListX parameterised on the provided sort. For a given sort S, the defined functions are: * "init_ListX_S" - return all but the last element of the list or nil for an empty list * "allDifferent_ListX_S" - return true if all elements of the list are distinct * "distinctFrom_ListX_S" - return true if the first argument is distinct from all the elements in the second argument

Define the repeated application of a function f of 2 arguments returning a pair where * the first argument of f is taken from an overall argument list * the second argument of f is an explicit argument of first invocation, and is the second member of the pair returned by the previous invocation on subsequent calls * the call depth is defined by the length of the explicit argument list * the overall return is a pair of reversed lists of individual returned values

Inlined chaining (avoiding recursion in SMT output)