(VAR x0 x1 x12 x2 x3 x4 x5 x6 x8 )
(STRATEGY INNERMOST)
(RULES 
        fold#3(insert_ord(x2),Nil) -> Nil
        fold#3(insert_ord(x6),Cons(x4,x2)) -> insert_ord#2(x6,x4,fold#3(insert_ord(x6),x2))
        cond_insert_ord_x_ys_1(True,x3,x2,x1) -> Cons(x3,Cons(x2,x1))
        cond_insert_ord_x_ys_1(False,x0,x5,x2) -> Cons(x5,insert_ord#2(leq,x0,x2))
        insert_ord#2(leq,x2,Nil) -> Cons(x2,Nil)
        insert_ord#2(leq,x6,Cons(x4,x2)) -> cond_insert_ord_x_ys_1(leq#2(x6,x4),x6,x4,x2)
        leq#2(0,x8) -> True
        leq#2(S(x12),0) -> False
        leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
        main(x3) -> fold#3(insert_ord(leq),x3)
        
)