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



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
4. zz  0 
  n:. (n < zz)  (P(n)) 

latex

 by (\p.IntInd (get_int_arg `hn` p) p) 

latex

 1: .....downcase..... NILNIL

 1: 4. zz < 0
 1: 5. ((zz+1)  0 )  (n:. (n < (zz+1))  (P(n)))
 1:   (zz  0 )  (n:. (n < zz)  (P(n)))
 2: .....basecase..... NILNIL

 2: 2. j:. (k:. (k < j)  (P(k)))  (P(j))
 2:   (0  0 )  (n:. (n < 0)  (P(n)))
 3: .....upcase..... NILNIL

 3: 4. 0 < zz
 3: 5. ((zz - 1)  0 )  (n:. (n < (zz - 1))  (P(n)))
 3:   (zz  0 )  (n:. (n < zz)  (P(n)))
 .

Definitions

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