theory Scratch imports Main
begin
typedecl A
typedecl B
typedecl C

consts 
 u :: "A => C => B"
 v :: "C => A"
 w :: "C => B" 
 P :: "A => C => bool"
 size :: "A => nat"

axioms conditional_decrease: 
"P a c ==> size (v c) < size a"

declare conj_cong[fundef_cong]

function f :: "A => B set" where 
"f a = {u a c| c. P a c  \<and>  w c : f (v c)}"
by auto

termination
by (relation "measure size") (auto simp: conditional_decrease)