fact: Definition Adversary_2_O_O_concrete_prod {D1 R1 D2 R2 DO RO} (A : Adversary_2_O_O_concrete D1 R1 D2 R2 DO RO) := (fun {SO : Set}{eqdSO : EqDec SO} (O : SO -> DO -> Comp (RO * SO)) d1 so => [s_O, p] <-$2 runPWO A.(A2OO_A1) d1 O so; [d_A, s_A] <-2 p; Ret (EqDec_dec (pair_EqDec (pair_EqDec eqdSO (RA1_EqDec A)) (A2OO_SA_EqDec _)) ) (s_O, d_A, s_A) , (fun {SO : Set}{eqdSO : EqDec SO}(s : A2OO_SA A) (x : D2) (O : SO -> DO -> Comp (RO * SO)) => runPWO (A2OO_A2 A) (s, x) O)).
imports: FCF CompFold Asymptotic