FDL - Step of Proof: fincr_wf2

Step of Proof: fincr_wf2

Inference at * 1 3 1 0 1 1 1 0 1 3 1 2 1
Iof proof for Lemma fincr wf2:

.....upcase..... NILNIL

1. P :

2.

j:

. (

k:

. (k < j)

(P(k)))

(P(j))
3. zz :

4. 0 < zz
5.

n:

. (n < (zz - 1))

(P(n))

n:

. (n < zz)

(P(n))

by Id

1: .....upcase..... NILNIL

1:

n:

. (n < zz)

(P(n))

.