Let us see what is the result of the translation of print!(double "soothe") [[print!(double "soothe")]] = (def c1 x1:/String = (def c2 x2:String = x1!x2 [[(double "soothe") → c2]]) [[print → c1]]) = (def c1 x1:/String = (def c2 x2:String = x1!x2 [[ double!["soothe" c2] ]]) c1!print) = (for simplicity's sake we translate [[ double!["soothe" c2] ]] directly in double!["soothe" c2] . We can assume the translation of Core PICT expressions or processes to be the identity) (def c1 x1:/String = (def c2 x2:String = x1!x2 double!["soothe" c2]) c1!print) To convince ourselves that the above process does exactly what double!["soothe" print] does, let us execute it (mind that there is the def of double that precedes all) (def c1 x1:/String = (def c2 x2:String = x1!x2 double!["soothe" c2]) c1!print) --> (def c1 x1:/String = (def c2 x2:String = x1!x2 double!["soothe" c2]) (def c2 x2:String = print!x2 double!["soothe" c2]) ) --> (def c1 x1:/String = (def c2 x2:String = x1!x2 double!["soothe" c2]) (def c2 x2:String = print!x2 +$!["soothe" "soothe" c2])) the string appending process will then execute the process c2!"soothesoothe" whose execution will cause the execution of print!"soothesoothe" che provoca la stampa di soothesoothe