fact: Definition mu_option_spec {X} {ENC : encodable X} {I : encInj ENC} s (b : X) : proc s -> (forall x : X, enc x <> lam 0) -> (forall n : nat, exists o : option X, s (enc n) == enc o) -> (forall b : X, forall m n : nat, s (enc n) == enc (Some b) -> m >= n -> s (enc m) == enc (Some b)) -> mu_option s == enc b <-> exists n : nat, s (enc n) == enc (Some b).
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible) Undecidability(LOptions)