theorem DY.Example.ACME.WithoutDEO.owner_authentication (address : String) (oPk : Bytes) (time : Nat) (tr : ExecTrace) : Trace.Reachable reachability tr → Trace.EventLoggedAt (ACMEEvent.LetsEncryptAcceptAddress address oPk) time tr → have tr_before := Trace.prefix tr time; Trace.EventLogged (ACMEEvent.OwnerRegisterAddress address oPk) tr_before