Case 1: x ?ran r implies append(<x> ^ ?, r) = append (?, r)
Case 1: x ?ran r implies append(<x> ^ ?, r) = append (?, r)
ret (append (<x> ^ ?, r)) = (ret (<x>)^?)) ? (ret r)
ret (append(<x> ^ ?, r)) = ret (append (?, r))
ret (append(<x> ^ ?, r)) = (ret ?) ? (ret r) ? <ret ? = ran ? and ran(? ^ r)= ran ? ? ran r>
ret <x> ? ret ? ? ret r = (ret ?) ? (ret r)
{x} ? ret ? ? ret r = (ret ?) ? (ret r)
(ret ?) ? (ret r) = (ret ?) ? (ret r).