instantiate parameter elem < rtc with gref by mapping : elem → ref; a → r; b → r0; c → r1 rename ^* → ^*; rtc → rtc; Pelem → Pref end instantiate