Returns the general lexicographic extension of an arbitrary relation ord.

ord : 'a -> 'a -> bool

The input relation.

l1 : 'a list

The first input items to be compared.

l2 : 'a list

The second input items to be compared.

Returns: bool

true, if the input list are equally long and reading from left to right the items in the first list are not less then the second's and there is at least one greater;otherwise false.

Example

 lexord (>) [1;1;1;2] [1;1;1;1]  // true
 lexord (>) [1;1;2;1] [1;1;1;1]  // true
 lexord (>) [1;0;2;1] [1;1;1;1]  // false
 lexord (>) [1;1;1;1] [1;1;1;1]  // false
 lexord (>) [2;2;2;2] [1;1;1]    // false

Tests if a term is greater than an other based on a reflexive lexicographic path order.

• If \(t\) is a variable \(t\), \(s > t\) if \(s \neq t\) and \(x \in \text{FVT}(s)\).
• \(f(s_1,\ldots,s_m) > f(t_1,\ldots,t_m)\) if the sequence \(s_1,\ldots,s_n\) is lexicographically greater than \(t_1,\ldots,t_n\), i.e if \(s_i = t_i\) for all \(i < k \leq m\) and \(s_k > t_k\) under the same ordering;
• \(f(s_1,\ldots,s_n) > t\) when some \(s_i \geq t\);
• \(f(s_1,\ldots,s_m) > g(t_1,\ldots,t_n)\) according to the specified precedence ordering of the function symbols, without further analysis of the \(s_i\) and \(t_i\);
• \(f(s_1,\ldots,s_m) > g(t_1,\ldots,t_n)\) (whether or not \(f = g\)) only if in addition \(f(s_1,\ldots,s_m) > t_i\) for each \(1 \leq i \leq n\).

w : string * int -> string * int -> bool

The function that `weights' the function symbols.

s : term

The first input term supposed greater than the second.

t : term

The second input term to be compared.

Returns: bool

true, if the first input term is greater than the second based on the reflexive lexicographic path order parametrized by w.

Example

The second term is a variable contained in the free variables of the first.

 lpo_ge (weight []) !!!"f(x)" !!!"x"

Example

The second term is a variable not contained in the free variables of the first.

 lpo_ge (weight []) !!!"f(y)" !!!"x"

Example

The inputs are function terms with the same function symbol but the arguments sequence of the first is greater than that of the second:

 lpo_ge (weight ["0"; "1"]) !!!"f(0,1)" !!!"f(0,0)"

Example

The first term is a function term and at least one of its arguments is greater or equal than the second term

 lpo_ge (weight ["0"; "1"]) !!!"h(0,1)" !!!"1"

Example

The inputs are function terms and the function symbol of the first is greater than the second based on the precedence defined by the weighting function

 lpo_ge (weight ["g";"f"]) !!!"f(1)" !!!"g(1)"

Example

The input terms are function terms and all arguments of the first are greater than the whole second term.

 lpo_ge (weight ["0";"1";"g";"f"]) !!!"g(f(1))" !!!"f(0)"

Example

The input terms are the same

 lpo_ge (weight []) !!!"f(1)" !!!"f(1)"

Tests if a term is greater than an other based on a irreflexive lexicographic path order.

• If \(t\) is a variable \(t\), \(s > t\) if \(s \neq t\) and \(x \in \text{FVT}(s)\).
• \(f(s_1,\ldots,s_m) > f(t_1,\ldots,t_m)\) if the sequence \(s_1,\ldots,s_n\) is lexicographically greater than \(t_1,\ldots,t_n\), i.e if \(s_i = t_i\) for all \(i < k \leq m\) and \(s_k > t_k\) under the same ordering;
• \(f(s_1,\ldots,s_n) > t\) when some \(s_i \geq t\);
• \(f(s_1,\ldots,s_m) > g(t_1,\ldots,t_n)\) according to the specified precedence ordering of the function symbols, without further analysis of the \(s_i\) and \(t_i\);
• \(f(s_1,\ldots,s_m) > g(t_1,\ldots,t_n)\) (whether or not \(f = g\)) only if in addition \(f(s_1,\ldots,s_m) > t_i\) for each \(1 \leq i \leq n\).

w : string * int -> string * int -> bool

The function that `weights' the function symbols.

s : term

The first input term supposed greater than the second.

t : term

The second input term to be compared.

Returns: bool

true, if the first input term is greater than the second based on the irreflexive lexicographic path order parametrized by w.

Example

The second term is a variable contained in the free variables of the first.

 lpo_gt (weight []) !!!"f(x)" !!!"x"

Example

The second term is a variable not contained in the free variables of the first.

 lpo_gt (weight []) !!!"f(y)" !!!"x"

Example

The inputs are function terms with the same function symbol but the arguments sequence of the first is greater than that of the second:

 lpo_gt (weight ["0"; "1"]) !!!"f(0,1)" !!!"f(0,0)"

Example

The first term is a function term and at least one of its arguments is greater or equal than the second term

 lpo_gt (weight ["0"; "1"]) !!!"h(0,1)" !!!"1"

Example

The inputs are function terms and the function symbol of the first is greater than the second based on the precedence defined by the weighting function

 lpo_gt (weight ["g";"f"]) !!!"f(1)" !!!"g(1)"

Example

The input terms are function terms and all arguments of the first are greater than the whole second term.

 lpo_gt (weight ["0";"1";"g";"f"]) !!!"g(f(1))" !!!"f(0)"

Example

The input terms are the same

 lpo_gt (weight []) !!!"f(1)" !!!"f(1)"

Calculates the size of a term as the sum of the number of its variables and function symbols.

tm : term

The input term.

Returns: int

The sum of the number of variables and function symbols in the term.

Example

 termsize !!!"f(f(f(x)))"

Tests if the function symbol f,n is `bigger' than g,n based on a precedence defined in the lis argument or on their arities if they are the same symbol.

lis : 'a list

The list that defines the precedence of function symbols.

f : 'a

The first input function symbol, supposed bigger than the second.

n : 'b

The arity of the first function symbol.

g : 'a

The second input function symbol to be compared.

m : 'b

The arity of the second function symbol.

Returns: bool

true, if f comes after g in lis, or f and g are the same symbol but n > m; otherwise, false.

Example

 weight ["g";"f"] ("f",1) ("g",2) // true
 weight ["f";"f"] ("f",2) ("f",1) // true
 weight ["f";"g"] ("f",1) ("g",2) // false
 weight ["f";"f"] ("f",1) ("f",2) // false