(VAR F H K M X Y Z x )
(RULES 
        if(true, X, Y) -> X
        if(false, X, Y) -> Y
        lteq(s(M), o) -> false
        lteq(o, M) -> true
        lteq(s(M), s(K)) -> lteq(M, K)
        from(M, nil) -> nil
        from(M, cons(H, Z)) -> if(lteq(M, H), cons(H, Z), from(M, Z))
        chain(F, nil) -> nil
        chain(F, cons(H, Z)) -> cons(, chain(F, from(, Z)))
        incch(X) -> chain(, X)
        
)