(* from Sereni: Size-Change Termination of Higher-Order Functional Programs; PRG-RR-04-20 *)

type nat = Zero | S of nat;;
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree
;;

let fix f =
  let rec x = lazy (Lazy.force (f x))
  in x
;;

let rec min a b =
  match a with
  | Zero -> Zero
  | S(a') ->
     match b with
     | Zero -> Zero
     | S(b') -> S(min a' b')
;;

let fst p = match p with | (a,b) -> a
and snd p = match p with | (a,b) -> b
;;

let rec rpm t m =
  match t with
  | Leaf(x) -> lazy (lazy(Leaf(Lazy.force m)), (lazy x))
  | Node(t1,t2) ->
     let p1 = Lazy.force (rpm t1 m)
     and p2 = Lazy.force (rpm t2 m)
     in lazy ((lazy (Node(Lazy.force (fst p1), Lazy.force (fst p2)))),
	       (lazy (min (Lazy.force (snd p1)) (Lazy.force (snd p2)))))
;;

let repmin t =
  let f p = rpm t (lazy (Lazy.force (snd (Lazy.force p)))) in
  Lazy.force (fst (Lazy.force (fix f)))
;;

let main t = repmin t;;