Testing the Predecessor Function

Blindly following the development given in John Harrison’s Syllabus we find the predecessor of 6:

cons = (λab.(λf.(fab)))
(cons 3 5) = ((λab.(λf.(fab))) 3 5)
(car a) = (a K)
car = (λa.aK)
cdr = (λa.aH)
(car (cons 3 5)) = ((λa.aK)((λab.(λf.(fab))) 3 5))
(cdr (cons 3 5)) = ((λa.aH)((λab.(λf.(fab))) 3 5))
PREFN = (λfp.(cons H (((car p) (cdr p)) (f (cdr p)))))
(PRE n) = (λfx. (cdr (n (PREFN f ) (cons K x))))
     = (λfx. ((λa.aH) (n ((λfp.((λab.(λf.(fab))) H ((((λa.aK) p) ((λa.aH) p)) (f ((λa.aH) p))))) f) ((λab.(λf.(fab))) K x))))
PRE = (λnfx. ((λa.aH) (n ((λfp.((λab.(λf.(fab))) H
   ((((λa.aK) p) ((λa.aH) p)) (f ((λa.aH) p))))) f)
    ((λab.(λf.(fab))) K x))))
(pr (PRE 6)) = ((λn.((ni)0)) ((λnfx.((λa.aH)
    (n ((λfp.((λab.(λf.(fab))) H ((((λa.aK) p)
     ((λa.aH) p)) (f ((λa.aH) p))))) f)
     ((λab.(λf.(fab))) K x))))
     (λsz.s(s(s(s(s(sz))))))))

Using the instrumented interpreter, we see

((λn.((ni)0)) ((λnfx. ((λa.aH)
    (n ((λfp.((λab.(λf.(fab))) H ((((λa.aK) p)
         ((λa.aH) p)) (f ((λa.aH) p))))) f)
     ((λab.(λf.(fab))) K x)))) (λsz.s(s(s(s(s(sz))))))))
code =
fe 0b 00 ff fe 05 00 fe 01 00 00 06 fd 80 fe 68 00
ff ff ff fe 06 00 ff fe 01 00 00 05 fe 45 00 fe 01
00 02 fe 3d 00 ff ff fe 10 00 fe 0c 00 ff ff ff fe
05 00 fe 01 00 00 02 01 06 fe 17 00 fe 0a 00 fe 06
00 ff fe 01 00 00 06 00 fe 06 00 ff fe 01 00 00 07
00 fe 01 00 01 fe 06 00 ff fe 01 00 00 07 00 01 fe
10 00 fe 0c 00 ff ff ff fe 05 00 fe 01 00 00 02 01
03 00 ff ff fe 01 00 01 fe 01 00 01 fe 01 00 01 fe
01 00 01 fe 01 00 01 fe 01 00 01 00
ws = 235, lst = 16
var: 163
invoke prim fun: 6
invoke lam fun: 115
lambda: 73
numeral: 1
val = 5

And this indicates a cost of O(n) to find the predecessor of n.