(STRATEGY
    INNERMOST)

(VAR
    x18 x32 x56 x16 x11 x224 x3 x2 x1 x4 x47 x39 x8 x6 x10 x12 x0)
(RULES
    walk_f#2(Nil(),x18) -> x18
    walk_f#2(Cons(Left(x32),x56),x16) -> walk_f#2(x56,Cons(Left(x32),x16))
    walk_f#2(Cons(Right(x11),x56),x224) -> walk_f#2(x56
                                                   ,Cons(Right(quicksort#2(x11))
                                                        ,x224))
    cond_quicksort_gt_xxs_1(Pair(x3,x2),x1) -> append#2(quicksort#2(x3)
                                                       ,Cons(x1
                                                            ,quicksort#2(x2)))
    quicksort#2(Nil()) -> Nil()
    quicksort#2(Cons(x4,x2)) ->
      cond_quicksort_gt_xxs_1(partition#2(quicksort_gt_xxs_2(x4),x2),x4)
    cond_partition_f_l_1(Pair(x47,x39),quicksort_gt_xxs_2(x4),x2) ->
      ite_b#2(leq#2(x4,x2),Pair(x47,Cons(x2,x39)),Pair(Cons(x2,x47),x39))
    partition#2(quicksort_gt_xxs_2(x1),Nil()) -> Pair(Nil(),Nil())
    partition#2(quicksort_gt_xxs_2(x3),Cons(x2,x1)) ->
      cond_partition_f_l_1(partition#2(quicksort_gt_xxs_2(x3),x1)
                          ,quicksort_gt_xxs_2(x3)
                          ,x2)
    append#2(Nil(),Cons(x2,x4)) -> Cons(x2,x4)
    append#2(Cons(x8,x6),Cons(x2,x4)) -> Cons(x8,append#2(x6,Cons(x2,x4)))
    ite_b#2(True(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) ->
      Pair(x8,Cons(x10,x12))
    ite_b#2(False(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) ->
      Pair(Cons(x2,x4),x6)
    leq#2(x4,0()) -> True()
    leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
    leq#2(0(),S(x12)) -> False()
    main(x0) -> walk_f#2(x0,Nil()))