fact: Definition PWO_Seq_P2 (s : S_P') (r : RO) : Comp (DO * S_P') := match (snd s) with | inl s' => match (fst s) with | O => r <-$ P3 s' r; [d', s'] <-$2 PWO_P2.(P1) r; ret (d', (O, inr s')) | S q' => [d', s'] <-$2 P2 s' r; ret (d', (q', inl s')) end | inr s' => [d', s'] <-$2 P2 s' r; ret (d', (O, inr s')) end.
imports: FCF CompFold