instantiate parameter elem < rtc with heap by mapping : elem → heap; a → H; b → H0; c → H1 rename ^* → ^*; rtc → rtc; Pelem → PHH end instantiate