The nice thing on paper about both of these is that you've broken every
computation down into nice nameable bits; if you want to do some
analysis (e.g. abstract interpretation) over the programs, you can store
intermediate results as a map from names (like %4) to values.
The traditional downside of CPS is that requiring lambdas be nested in
order for things to be in scope can make some program transformations
require "reshuffling" terms around in a way SSA doesn't require.
The "cps soup" [0] approach used in Guile fixes this, but your terms
look like they violate lexical scoping rules!
It's very, very similar to single-static-assignment (SSA) style that will be more familiar to people coming from imperative languages.