Case 2: x ?ran r
ret (append (<x> ^ ?, r)) = (ret (<x>)^?)) ? (ret r)
ret(append(<x> ^ ?, r)) = ret (<x> ^ append (?, r))
ret (append(<x> ^ ?, r)) = ret <x> ? ret( append (?, r))
? <ret ? = ran ? and ran(? ^ r) = ran ? ? ran r>
ret (append(<x> ^ ?, r)) = ret <x> ? ret ? ? ret r
ret <x> ? ret ? ? ret r = ret <x> ? ret ? ? ret r
We have proved that append correctly models the behaviour of ? in the concrete model.