(format PTRS)
(fun leq 2)
(fun 0 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun ifLoop 3)
(fun stop 0)
(fun loop 2)
(prule (leq 0 x) ((true :prob 1 )))
(prule (leq (s x) (s y)) (((leq x y) :prob 1 )))
(prule (leq (s x) 0) ((false :prob 1 )))
(prule (ifLoop false x y) ((stop :prob 1 )))
(prule (ifLoop true x y) (((loop (s x) y) :prob 1 )))
(prule (loop x y) (((ifLoop (leq x y) x y) :prob 1 )))