Two Queues in Series

$ICDQ$ $Init$_E and $Init[1]$_M and $Init[2]$_M
and always [($Q$_E and <$q$₁, $q$₂, $z$>' = <$q$₁, $q$₂, $z$>)
   or ($Q[1]$_M and <$q$₂, $o$>' = <$q$₂, $o$>)
   or ($Q[2]$_M and <$q$₁, $i$>' = <$q$₁, $i$>)]$$_{<i, o, z, q1, q2>}
and $ICL[1]$ and $ICL[2]$
$CDQ$ exists $q$₁, q₂: $ICDQ$