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



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
4. 0 < zz
5. n:. (n < (zz - 1))  (P(n))
6. n : 
7. n < zz
8. n1:. (n1 < n)  (P(n1))
  P(n) 

latex

 by OnHyps [-2;-3;-3;-3] Thin 

latex

 1: 

 1: 3. n : 
 1: 4. n1:. (n1 < n)  (P(n1))
 1:   P(n)
 .

Definitions

n - m, #$n, , f(a), a < b, P  Q, x:A. B(x), , , x:AB(x)