10,828 Pages

## The gist

Iff we have a matrix such as

\(G\frown B_0\frown B_1\frown\cdots\frown B_n\)

which β-reduced from \(G\frown B\frown N\) , then it is holds that

\(B_k\frown N_k<_rB\frown N\)

\(N_k\) denotes a first sequence of \(B_{k+1}\) .

\(<_r\) is well-founded and defined for every bad part.

For hydra tree's property, that is sufficient condition of computability.

## The specific proof

This proof depends on Bashicu's definition;

B[n] is a n-th sequence in the bad part.

1.We add a value of Δ to each bad part from B[0].

2.We add a value of Δ to B[0] each line.

3.For a sequence of the bad part B[K] (K>0) which we add a value right now, we search for a first sequence B[L] from B[K] to left. B[L] has a smaller value in the line than B[K]'s in the same line. If B[L] is not found, we don't add to the line.

4.Comparing the value in B[K] with B[0] in the same line, B[K] has a bigger value than B[0] and B[L] has already been added a value of Δ, we add a value of Δ to the line.

It is supposed that \(G\frown B\) is computable. We organize compute process for every bad part and prove inductively. We divide whole proof as follows;

• The bad part is well-founded by \(<_r\) .
• The tree is well-founded.