fact: CoInductive compliant_semantics `{MayProvide ix i} `(c : contract i Ω) : Ω -> semantics ix -> Prop := | compliant_semantics_rec (sem : semantics ix) (ω : Ω) (o_callee : forall {α} (e : ix α), gen_caller_obligation c ω e -> gen_callee_obligation c ω e (eval_effect sem e)) (next : forall {α} (e : ix α), gen_caller_obligation c ω e -> compliant_semantics c (gen_witness_update c ω e (eval_effect sem e)) (exec_effect sem e)) : compliant_semantics c ω sem.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)