# 述語論理とバシク行列

## Definition

If a value at the first line of N is n+1, then go to left from the right end until you find a sequence T_0 that value at first line is n-1, not be found, S_0=T_0. In T_0T_1...S_{n-1}, S'_0 is a right-hand sequence which is the biggest sequence by lexicographic order and that first line has n. Worse part denotes S'_0S'_1...S_{n-1}.

In worse part, put a restriction on each sequence that first line has a bigger value than n+1 and that value not being 0 doesn't continue as N; in the same line, we don't add a value of Δ to the sequence U that value is not bigger than N's one or each sequences subsequent to the right and that value of first line is bigger than U's one at first line.



## Program

１行

$$\forall n \forall a \forall s' \forall b [$$

$$b<a$$

$$\land(((n+1)=b \to (n)=t_0)\to ((n+1)=0 \to (n)=t))$$

$$\land(((n+1)=a \to (n)=s_0)\to ((n+1)=0 \to (n)=s))$$

$$\land s'<s$$

$$\to s'+t<s]$$