forall k{tv}[tv] {j{tv}[tv]}.
forall a{tv}[tv] b{tv}[tv] -> (){(w) tc}